Modelling and verifying non-blocking algorithms that use dynamically allocated memory

Abstract

This thesis presents techniques for the machine-assisted verification of an important class of concurrent algorithms, called non-blocking algorithms. The notion of linearizability is used as a correctness condition for concurrent implementations of sequential datatypes and the use of forward simulation relations as a proof method for showing linearizability is described. A detailed case study is presented: the attempted verification of a concurrent double-ended queue implementation, the Snark algorithm, using the theorem proving system PVS. This case study allows the exploration of the difficult problem of verifying an algorithm that uses low-level pointer operations over a dynamic data-structure in the presence of concurrent access by multiple processes. During the verification attempt, a previously undetected bug was found in the Snark algorithm. Two possible corrections to this algorithm are presented and their merits discussed. The verification of one of these corrections would require the use of a backward simulation relation. The thesis concludes by describing the reason for this extention to the verification methodology and the use of a hierarchical proof structure to simplify verifications that require backward simulations.