Deny-Guarantee Reasoning

Michael David Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 relyguarantee 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.
Original languageEnglish
Title of host publicationProgramming Languages and Systems, 18th European Symposium on Programming
Subtitle of host publicationESOP 2009
Place of PublicationSpringer New York
Number of pages15
ISBN (Electronic)978-3-642-00590-9
ISBN (Print)978-3-642-00589-3
Publication statusPublished - 2009
EventProgramming Languages and Systems : 18th European Symposium on Programming - York (UK), United Kingdom
Duration: 22 Mar 200929 Mar 2009

Publication series

NameLecture Notes in Computer Science


ConferenceProgramming Languages and Systems : 18th European Symposium on Programming
Country/TerritoryUnited Kingdom
CityYork (UK)

Cite this