Verified Incremental Development of Lock-Free Algorithms

David Déharbe, Loïc Fejoz, Pascal Fontaine and Stephan Merz
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

Stephan Merz