University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Deny-guarantee reasoning

Deny-guarantee reasoning

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Matthew Parkinson.

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.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity