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}
}