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 talk, we will describe deny-guarantee reasoning, a reformulation of rely-guarantee that enables reasoning about dynamically scoped concurrency. Deny-guarantee builds 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, the rely is inverted to give a deny, specifying what the environment cannot do. We illustrate the use of our proof system with examples, and show that it can encode all the original rely-guarantee proofs.

Joint work with Xinyu Feng, Matthew Parkinson and Viktor Vafeiadis.