University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Higher Order Actions in Deny-Guarantee

Higher Order Actions in Deny-Guarantee

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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