Institute of Software, Chinese Academy of Sciences, Beijing (CHINA)
RWTH Aachen University (GERMANY)
CADP (Construction and Analysis of Distributed Processes)
about one billion states.
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.
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.
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
Prof. Dr. Ir. Joost-Pieter Katoen, PDEng
RWTH Aachen University
LS2: Software Modeling and Verification
Tel: +49 (241) 8021200
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|