Two Approaches for Proving Linearizability of Multiset

B. Tofan, O. Travkin, G. Schellhorn, H. Wehrheim

Two Approaches for Proving Linearizability of Multiset

Linearizability is a key correctness criterion for concurrent software. In our previous work, we have 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 process local simulation. We have incorporated the approach of verifying linearizability based on refinement in two rather different proof systems: a predicate logic based approach performing a simulation for two processes and second, an approach based on temporal logic that shows a refinement for an individual process using rely-guarantee reasoning and symbolic execution. To compare both proof techniques, we use an implementation of a multiset as running example. Moreover, we show how ownership annotations have helped us to reduce the proof effort. All proofs are mechanized in the theorem prover KIV.
published 2014 Science of Computer Programming Journal, vol. 96, Part 3, pp. 297–314

Publisher: Elsevier