Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof.
This mapping of concrete states to non-empty sets of abstract states is closely related to the method of , employed by a number of manual proof efforts @cite_9 @cite_21 @cite_7 , and which @cite_7 recently showed to be a complete proof method for verifying linearizability. Similar to forward simulation proofs, backward simulation proofs, are monolithic in the sense that they prove linearizability directly by one big proof. Sadly, they are also not very intuitive and as a result often difficult to come up with. For instance, although the definition of their backward simulation relation for the HW queue is four lines long, @cite_7 devote two full pages to explain it.
@cite_9 @cite_21 @cite_7
2063798543 1592188038 27871822
We describe an approach to verifying concurrent data structures based on simulation between two Input Output Automata (IOAs), modelling the specification and the implementation. We explain how we used this approach in mechanically verifying a simple lock-free stack implementation using forward simulation, and briefly discuss our experience in verifying three other lock-free algorithms which all required the use of backward simulation. Optimistic and nonblocking concurrent algorithms are increasingly finding their way into practical use; an important example is software transactional memory implementations. Such algorithms are notoriously difficult to design and verify as correct, and we believe complete, formal, and machine-checked correctness proofs for such algorithms are critical. We have been studying the use of automated tools such as the PVS theorem proving system to model algorithms and their specifications using formalisms such as I O automata, and using simulation proof techniques to show the algorithms implement their specifications. While it has been relatively rare in the past, optimistic and nonblocking algorithms often require a special flavour of simulation proof, known as backward simulation. In this paper, we present what we believe is by far the most challenging backward simulation proof achieved to date; this proof was developed and completely checked using PVS. Linearisability is the standard correctness criterion for concurrent data structures. In this paper, we present a sound and complete proof technique for linearisability based on backward simulations. We exemplify this technique by a linearisability proof of the queue algorithm presented in Herlihy and Wing's landmark paper. Except for the manual proof by them, none of the many other current approaches to checking linearisability has successfully treated this intricate example. Our approach is grounded on complete mechanisation: the proof obligations for the queue are verified using the interactive prover KIV, and so is the general soundness and completeness result for our proof technique.