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, September 2016. Available on-line from https://arxiv.org/pdf/1609.07546.pdf and from the CADP Web site in PDF or PostScript [Yang-Katoen-Lin-Wu-17] X. Yang, J-P. Katoen, H. Lin, and H. Wu. "Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation". CoRR abs/1701.06104, June 2017. Available on-line from https://arxiv.org/pdf/1701.06104 and from the CADP Web site in PDF or PostScript [Yang-Katoen-Lin-et-al-18] X. Yang, J-P. Katoen, H. Lin, G. Liu, and H. Wu. "Branching Bisimulation and Concurrent Object Verification". Proceedings of the 48th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN'2018), Luxembourg City, Luxembourg, pages 267-278, June 2017. Available on-line from https://ieeexplore.ieee.org/document/8416489 and from the CADP Web 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: [email protected]
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page