Abstract

Rely-guarantee (RG) is a compositional method that extends Hoare-style reasoning to concurrent programs. A fundamental tenet is that any assertion we write must be stable, that is, invariant under any interference from concurrently-running threads. One can consider stabilising an assertion, by weakening it (or strengthening it) until it becomes stable. In this talk, I will develop an extension to the RG method, in which stabilisation is not a meta-level operator, but exists within the syntax of assertions. I will show how this can eliminate many side-conditions from the RG proof rules, and, in particular, lead to an elegant proof rule for conditional statements whose tests are evaluated non-atomically. I will further show how explicit stabilisation might improve the modularity of the RG method, thus allowing the verification of libraries.

This talk describes joint work with Matthew Parkinson.