Proving Linearizability via Branching Bisimulation
Programming Languages
2016-10-03 v5 Logic in Computer Science
Abstract
Linearizability and progress properties are key correctness notions for concurrent objects. However, model checking linearizability has suffered from the PSPACE-hardness of the trace inclusion problem. This paper proposes to exploit branching bisimulation, a fundamental semantic equivalence relation developed for process algebras which can be computed efficiently, in checking these properties. A quotient construction is provided which results in huge state space reductions. We confirm the advantages of the proposed approach on more than a dozen benchmark problems.
Cite
@article{arxiv.1609.07546,
title = {Proving Linearizability via Branching Bisimulation},
author = {Xiaoxiao Yang and Joost-Pieter Katoen and Huimin Lin and Hao Wu},
journal= {arXiv preprint arXiv:1609.07546},
year = {2016}
}
Comments
In this paper, we conducted the experiment on 13 popular concurrent data structures yielding promising results