Deny-Guarantee Reasoning Mike Dodds',Xinyu Feng2,Matthew Parkinson,and Viktor Vafeiadis3 1 University of Cambridge,UK 2 Toyota Technological Institute at Chicago,USA 3 Microsoft Research Cambridge,UK Abstract.Rely-guarantee is a well-established approach to reasoning about con- current 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 spec- ifies 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. 1 Introduction Rely-guarantee [10]is a well-established compositional proof method for reasoning about concurrent programs that use parallel composition.Parallel composition provides a structured form of concurrency:the lifetime of each thread is statically scoped,and therefore interference between threads is also statically known.In real systems,how- ever,concurrency is not structured like this.Instead,threads are started by a 'fork'and collected with'join'commands.The lifetime of such a thread is dynamically scoped in a similar way to the lifetime of heap-allocated data. In this paper,we introduce deny-guarantee reasoning,a reformulation of rely-guar- antee that enables reasoning about such dynamically scoped concurrency.We build on ideas from separation logic to allow interference to be dynamically split and recom- bined,in a similar way that separation logic splits and joins heaps. In rely-guarantee,interference is described using two binary relations:the rely,R, and the guarantee,G.Specifications of programs consist of a precondition,a post- condition and an interference specification.This setup is sufficient to reason about lexically-scoped parallel composition,but not about dynamically-scoped threads.With dynamically-scoped threads,the interference at the end of the program may be quite different from the interference at the beginning of the program,because during execu- tion other threads may have been forked or joined.Therefore,just as in Hoare logicDeny-Guarantee Reasoning Mike Dodds1 , Xinyu Feng2 , Matthew Parkinson1 , and Viktor Vafeiadis3 1 University of Cambridge, UK 2 Toyota Technological Institute at Chicago, USA 3 Microsoft Research Cambridge, UK Abstract. Rely-guarantee is a well-established approach to reasoning about con￾current 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 spec￾ifies 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. 1 Introduction Rely-guarantee [10] is a well-established compositional proof method for reasoning about concurrent programs that use parallel composition. Parallel composition provides a structured form of concurrency: the lifetime of each thread is statically scoped, and therefore interference between threads is also statically known. In real systems, how￾ever, concurrency is not structured like this. Instead, threads are started by a ‘fork’ and collected with ‘join’ commands. The lifetime of such a thread is dynamically scoped in a similar way to the lifetime of heap-allocated data. In this paper, we introduce deny-guarantee reasoning, a reformulation of rely-guar￾antee that enables reasoning about such dynamically scoped concurrency. We build on ideas from separation logic to allow interference to be dynamically split and recom￾bined, in a similar way that separation logic splits and joins heaps. In rely-guarantee, interference is described using two binary relations: the rely, R, and the guarantee, G. Specifications of programs consist of a precondition, a post￾condition and an interference specification. This setup is sufficient to reason about lexically-scoped parallel composition, but not about dynamically-scoped threads. With dynamically-scoped threads, the interference at the end of the program may be quite different from the interference at the beginning of the program, because during execu￾tion other threads may have been forked or joined. Therefore, just as in Hoare logic