Verifying a Stack with Hazard Pointers in Temporal Logic

A significant problem of lock-free concurrent data structures in an environment without garbage collection, is to ensure safe memory reclamation of objects that are removed from the data structure. An elegant solution to this problem is Michael’s hazard pointers method, but the verification of a simple lock-free stack with hazard pointers is challenging. This work contributes to the formal verification of lock-free algorithms. Using the temporal logic framework of the interactive prover KIV, we verify correctness and liveness of a lock-free stack with hazard pointers. The proof exploits the algorithm’s symmetry and requires neither additional history variables nor temporal past operators to describe inter-process interference. Moreover, the verification shows a relation between hazard pointers and garbage collection, which makes it possible to reuse the verification conditions from the simpler proof under garbage collection.

Download PDF