Proving Linearizability of Multiset with Local Proof Obligations
Abstract
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.
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.
Full Text:
PDFDOI: http://dx.doi.org/10.14279/tuj.eceasst.53.795
DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.53.795.793
Hosted By Universitätsbibliothek TU Berlin.