Verifying lock-freedom using well-founded orders

Abstract

Lock-free algorithms are designed to improve the performance of concurrent programs by maximising the potential for processes to operate in parallel. Lock-free algorithms guarantee that within the system as a whole, some process will eventually complete its operation (as opposed to guaranteeing that all operations will eventully complete). Since lock-free algorithms potentially allow a high degree of interference between concurrent processes, and because their progress property is non-trivial, it is difficult to be assured of their correctness without a formal, machine-checked verification. In this paper we describe a method for proving the lock-free progress property. The approach is based on the construction of a well-founded ordering on the set of processes. The method is demonstrated using a well-known lock-free stack algorithm as an example, and we describe how the proof was checked using a theorem prover. © Springer-Verlag Berlin Heidelberg 2007.