Technical reports
Explicit stabilisation for modular rely-guarantee reasoning
John Wickerson, Mike Dodds, Matthew Parkinson
March 2010, 29 pages
DOI: 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} }