Technical reports

Automatically proving linearizability

Viktor Vafeiadis

September 2016, 19 pages

DOI: 10.48456/tr-778

Abstract

This technical report presents a practical automatic verification procedure for proving linearizability (i.e., atomicity and functional correctness) of concurrent data structure implementations. The procedure uses a novel instrumentation to verify logically pure executions, and is evaluated on a number of standard concurrent stack, queue and set algorithms.

Full text

PDF (0.4 MB)

BibTeX record

@TechReport{UCAM-CL-TR-778,
  author =	 {Vafeiadis, Viktor},
  title = 	 {{Automatically proving linearizability}},
  year = 	 2016,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-778.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-778},
  number = 	 {UCAM-CL-TR-778}
}