Verified Incremental Development of Lock-Free Algorithms

David Déharbe, Loïc Fejoz, Pascal Fontaine and Stephan Merz

Abstract

Mutual exclusion locks have traditionally been used for synchronizing the access of multiple processes to shared data structures. Multi-processor architectures offer new synchronization primitives that have given rise to algorithms for optimistic concurrency and non-blocking implementations. These algorithms are quite subtle and raise the need for formal verification. We propose a refinement-based method for designing and verifying non-blocking, and in particular lock-free, algorithms. We achieve good success in automatically discharging the verification conditions generated by this method, relying on first-order and SMT provers, augmented by a simple but useful instantiation heuristic. We present our method using a non-trivial running example due to Harris et al.

Available as: PDF