Model checking simulation rules for linearizability

Abstract

Linearizability is the standard notion of correctness for concurrent objects. A number of approaches have been developed for proving linearizability along with associated tool support. In this paper, we extend the tool support for an existing simulation-based method. We complement the current theorem-prover support with model checking to allow a means of quickly finding problems with an implementation before attempting a full verification. Our model checking approach is novel in that it is used to verify the simulation rules, rather than directly trying to check an object being accessed by a number of threads. As a consequence, verification can be done for an arbitrary number of accessing threads; something that is not possible with existing approaches based on model checking.