ISSE

Search

Proving linearizability of multiset with local proof obligations

O. Travkin, H. Wehrheim, G. Schellhorn

Proving linearizability of multiset with local proof obligations

Linearizability is a key correctness criterion for concurrent software. In our previous work, we introduced local proof obligations, which, by showing a refinement between an abstract specification and its implementation, imply linearizability of the implementation. The refinement is shown via a thread local backward simulation, which reduces the complexity of a backward simulation to an execution of two symbolic threads. In this paper, we present a correctness proof by applying those proof obligations to a lock-based implementation of a multiset. It is interesting for two reasons: First, one of its operations inserts two elements non-atomically. To show that it linearizes, we have to find one point, where the multiset is changed instantaneously, which is a counter-intuitive task. Second, another operation has non-fixed linearization points, i.e. the linearization points cannot be statically fixed, because the operation’s linearization may depend on other processes’ execution. This is a typical case to use backward simulation, where we could apply our thread local variant of it. All proofs were mechanized in the theorem prover KIV.

ECEASST-Link
published 2012 In Proc. of Automated Verification of Critical Systems (AVoCS)

Publisher: ECEASST, Vol. 53, ISSN 1863-2122, 2012