Database of Case Studies Achieved Using CADP

Proving Linearizability via Branching Bisimulation

Organisation: Institute of Software, Chinese Academy of Sciences, Beijing (CHINA)
RWTH Aachen University (GERMANY)

Method: LNT

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Concurrent Programming.

Period: 2016

Size: about one billion states.

Description: A concurrent data structure, or a concurrent object, provides a set of methods that allow client threads to simultaneously access and manipulate a shared object. Linearizablity is a widely accepted correctness criterion for implementations of concurrent objects. Intuitively, an implementation of a concurrent object is linearizable with respect to a sequential specification if every method call appears to take effect, i.e., changes the state of the object, instantaneously at some time point between its invocation and its response, behaving as defined by the specification. Linearizability can be verified by trace inclusion, which is infeasible in practice because checking trace inclusion is PSPACE-hard.

This paper proposes an efficient method for deciding linearizability, based on branching bisimulation minimization. It is shown that the branching bisimulation quotient of an LTS representing a concurrent system preserves linearizability. Similarly, progress properties are preserved by divergence-sensitive branching bisimulation (divbranching) quotienting. As opposed to checking trace inclusion, (div)branching bisimulation minimization benefits from efficient algorithms, such as those implemented in the BCG_MIN and BCG_CMP tools of CADP.

The effectiveness and efficiency of the proposed techniques for proving linearizability and progress properties are shown by experiments conducted on 13 practical concurrent algorithms, including 4 queues (3 lock-free, 1 lock-based), 4 lists (1 lock-free, 3 lock-based), 3 (lock-free) stacks and 2 extended CAS (compare-and-swap) operations, some of which are used in the java.util.concurrent package. The experiments were carried out using CADP. In contrast to proof techniques for linearizability and progress, the approach is able to generate counterexamples in an automated manner. The verification experiments spotted a previously unknown violation of lock-freedom in the revised Treiber stack. This bug was found by an automatically generated counterexample of divbranching bisimilarity checking by CADP with just two concurrent threads.

Conclusions: Branching bisimulation quotient construction yields state-space savings of up to four orders of magnitude in the best cases, and to two to three orders for most cases. In general, for the non-blocking implementations of the concurrent data structures, the larger the system the higher the state space reduction factor. Verifying linearizability directly on the concrete state space would be practically infeasible.

Publications: [Yang-Katoen-Lin-Wu-16] X. Yang, J-P. Katoen, H. Lin, and H. Wu. "Proving Linearizability via Branching Bisimulation". CoRR, vol abs/1609.07546, 2016.
Available on-line from https://arxiv.org/pdf/1609.07546.pdf
and from the VASY FTP site in PDF or PostScript
Contact:
Prof. Dr. Ir. Joost-Pieter Katoen, PDEng
RWTH Aachen University
LS2: Software Modeling and Verification
D-52056 Aachen
GERMANY
Tel: +49 (241) 8021200
Email: katoen@cs.rwth-aachen.de



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Thu Oct 26 17:01:28 2017.


Back to the CADP case studies page