Deny-Guarantee Reasoning

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 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 pro...

• Type: Conference
• Year: 2009
• Where: ESOP
• Authors: Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis
• Keywords: ESOP 2009, Guarantee Permission, Parallel Composition, Programming Languages, Separation Logic