Abstract

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.