ISSE

Search

Formal Verification of a Lock-Free Stack with Hazard Pointers

B. Tofan, G. Schellhorn, and W. Reif

Formal Verification of a Lock-Free Stack with Hazard Pointers

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. The formal verification of concurrent algorithms with hazard pointers is yet challenging. This work presents a mechanized proof of the major correctness and progress aspects of a lock-free stack with hazard pointers.

Springerlink
published 2011 In Proc. of International Colloquium on Theoretical Aspects of Computing (ICTAC)

Publisher: Springer, LNCS, vol. 6916, pp. 239 - 255


Downloads: