Technical reports
A safety proof of a lazy concurrent list-based set implementation
Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro
January 2006, 19 pages
DOI: 10.48456/tr-659
Abstract
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”.
Full text
PDF (0.2 MB)
BibTeX record
@TechReport{UCAM-CL-TR-659, author = {Vafeiadis, Viktor and Herlihy, Maurice and Hoare, Tony and Shapiro, Marc}, title = {{A safety proof of a lazy concurrent list-based set implementation}}, year = 2006, month = jan, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-659.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-659}, number = {UCAM-CL-TR-659} }