Deny-guarantee reasoning

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

• Mike Dodds (University of Cambridge)
• Monday 03 November 2008, 12:45-14:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Computer Laboratory talks
• FW26
• School of Technology
• Semantics Lunch (Computer Laboratory)
• de239's list

Note that ex-directory lists are not shown.