A safety proof of a lazy concurrent list-based set implementation
Viktor Vafeiadis, Maurice P. Herlihy, Tony Hoare, Marc Shapiro · CL Technical Reports · 2021
We prove the safety of a practical concurrent list-based implementation due to Heller et al. It exposes an interface of an integer set with methods contains, add, and remove. The implementation uses a combination of fine-grain locking, optimistic and lazy synchronisation. Our proofs are hand-crafted. They use rely-guarantee reasoning and thereby illustrate its power and applicability, as well as some of its limitations. For each method, we identify the linearisation point, and establish its validity. Hence we show that the methods are safe, linearisable and implement a high-level specification. This report is a companion document to our PPoPP 2006 paper entitled “Proving correctness of highly-concurrent linearisable objects”.