Two approaches for proving linearizability of multiset

• Two approaches for verifying linearizability.
• Mechanized verification of local proof obligations.
• Challenging case study of a multiset implementation with fine-grained locking.
• Rely–Guarantee reasoning for a Temporal Logic with Programs.

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.