Department of Computer Science and Technology

Technical reports

Explicit stabilisation for modular rely-guarantee reasoning

John Wickerson, Mike Dodds, Matthew Parkinson

March 2010, 29 pages

DOIhttps://doi.org/10.48456/tr-774

Abstract

We propose a new formalisation of stability for Rely-Guarantee, in which an assertion’s stability is encoded into its syntactic form. This allows two advances in modular reasoning. Firstly, it enables Rely-Guarantee, for the first time, to verify concurrent libraries independently of their clients’ environments. Secondly, in a sequential setting, it allows a module’s internal interference to be hidden while verifying its clients. We demonstrate our approach by verifying, using RGSep, the Version 7 Unix memory manager, uncovering a twenty-year-old bug in the process.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-774,
  author =	 {Wickerson, John and Dodds, Mike and Parkinson, Matthew},
  title = 	 {{Explicit stabilisation for modular rely-guarantee
         	   reasoning}},
  year = 	 2010,
  month = 	 mar,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-774.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-774},
  number = 	 {UCAM-CL-TR-774}
}