Consider increment program inc(x) || inc(x), where inc(x) increments x atomically. It is difficult to show that, with pre-condition x = 0, the post-condition is x = 2. The Owicki-Gries method (1970s) proves this specification by adding auxillary variables y,z and invariant x = y+z. However, this work is not compositional since more threads require more auxilary variables. Rely-guarantee reasoning (1980s) provides a form of compositional reasoning, but the post-condition is (exists n>=1. x = n). Concurrent separation logic (2000s) is more compositional, providing local reasoning about the machine state with invariants constraining the use of shared state. For the increment program, the invariant (exists n >=0. x = n) is again too weak. Since this work, RGSep combined separation logic with rely-guarantee to reason about more fine-grained concurrent algorithms and CAP reasoning added abstraction. This talk provides an introduction to modern CAP reasoning, giving an overview of the strengths of current approaches and highlighting places where there is room for improvement. We can finally give a compositional proof of the strong specification of the increment program.

Track: ECOOP Summer School

Philippa Gardner is a professor in the Department of Computing at Imperial. Her current research focusses on program verification: in particular, reasoning about web programs (JavaScript and DOM) and reasoning about concurrent programs. She completed her PhD thesis, supervised by Professor Gordon Plotkin. She moved to Cambridge hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She is the Director of the Research Institute in Automated Program Analysis and Verification, funded by GCHQ in association with EPSRC.