Department of Computer Science and Technology

Technical reports

A marriage of rely/guarantee and separation logic

Viktor Vafeiadis, Matthew Parkinson

June 2007, 31 pages

DOI: 10.48456/tr-687

Abstract

In the quest for tractable methods for reasoning about concurrent algorithms both rely/guarantee logic and separation logic have made great advances. They both seek to tame, or control, the complexity of concurrent interactions, but neither is the ultimate approach. Rely-guarantee copes naturally with interference, but its specifications are complex because they describe the entire state. Conversely separation logic has difficulty dealing with interference, but its specifications are simpler because they describe only the relevant state that the program accesses.

We propose a combined system which marries the two approaches. We can describe interference naturally (using a relation as in rely/guarantee), and where there is no interference, we can reason locally (as in separation logic). We demonstrate the advantages of the combined approach by verifying a lock-coupling list algorithm, which actually disposes/frees removed nodes.

Full text

PDF (0.4 MB)

BibTeX record

@TechReport{UCAM-CL-TR-687,
  author =	 {Vafeiadis, Viktor and Parkinson, Matthew},
  title = 	 {{A marriage of rely/guarantee and separation logic}},
  year = 	 2007,
  month = 	 jun,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-687.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-687},
  number = 	 {UCAM-CL-TR-687}
}