Higher Order Actions in Deny-Guarantee

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

• Mike Dodds (University of Cambridge)
• Monday 29 June 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Sam Staton.

Describing interactions between threads is the key to understanding concurrent algorithms. In rely-guarantee reasoning, interactions between threads are modelled abstractly by relations describing interference on the shared state. Using relations simplifies reasoning, but makes it difficult to specify temporal properties where interference changes over time.

Deny-guarantee is an extension of rely-guarantee that uses a separation-logic to dynamically partition interference between threads. We have used deny-guarantee to define actions which can rewrite interference. Hence, we consider our actions to be higher-order. Our actions can capture temporal properties of interference, and so they allow more state to be thread-local and often avoid the need for auxiliary state. Our approach permits proofs that are more elegant than the equivalent proofs in rely-guarantee.

Joint work with Matthew Parkinson.

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
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• de239's list

Note that ex-directory lists are not shown.