Technical reports

Deny-guarantee reasoning

Mike Dodds, Xinyu Feng, Matthew Parkinson, Viktor Vafeiadis

January 2009, 82 pages

DOI: 10.48456/tr-736

Abstract

Rely-guarantee is a well-established approach to reasoning about concurrent programs that use parallel composition. However, parallel composition is not how concurrency is structured in real systems. Instead, threads are started by ‘fork’ and collected with ‘join’ commands. This style of concurrency cannot be reasoned about using rely-guarantee, as the life-time of a thread can be scoped dynamically. With parallel composition the scope is static.

In this paper, we introduce deny-guarantee reasoning, a reformulation of rely-guarantee that enables reasoning about dynamically scoped concurrency. We build on ideas from separation logic to allow interference to be dynamically split and recombined, in a similar way that separation logic splits and joins heaps. To allow this splitting, we use deny and guarantee permissions: a deny permission specifies that the environment cannot do an action, and guarantee permission allow us to do an action. We illustrate the use of our proof system with examples, and show that it can encode all the original rely-guarantee proofs. We also present the semantics and soundness of the deny-guarantee method.

Full text

PDF (0.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-736,
  author =	 {Dodds, Mike and Feng, Xinyu and Parkinson, Matthew and
          	  Vafeiadis, Viktor},
  title = 	 {{Deny-guarantee reasoning}},
  year = 	 2009,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-736.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-736},
  number = 	 {UCAM-CL-TR-736}
}