A Marriage of Rely/Guarantee and Separation Logic

  • Matthew Parkinson | University of Cambridge

In the quest for tractable methods for reasoning about concurrent algorithms both rely/guarantee logic and separation logic have made great advances. They both seek to tame, or control, the complexity of concurrent interactions, but neither is the ultimate approach. Rely guarantee copes naturally with interference, but its specifications are complex because they describe the entire state. Conversely separation logic has difficulty dealing with interference, but its specifications are simpler because they describe only the relevant state that the program accesses.

We propose a combined system which marries the two approaches. We can describe interference naturally (using a relation as in rely/guarantee), and where there is no interference, we can reason locally (as in separation logic). We demonstrate the advantages of the combined approach by verifying a lock-coupling list algorithm, which actually disposes/frees removed nodes.

Speaker Details

Matthew Parkinson is a Royal Academy of Engineering and EPSRC Postdoctoral Research Fellow in the Computer Laboratory at the University of Cambridge. His fellowship aims to extend Separation Logic to mainstream programming languages such as concurrent Java. He previously working at Middlesex University with Professor Richard Bornat and extended Concurrent Separation logic to reason about non-blocking concurrency. He studied for his thesis at the University of Cambridge under the supervision of Dr. Gavin Bierman and Professor Andrew Pitts/ In October 2005, he successfully defended his thesis on “Local Reasoning in Java”, which extended separation logic to a sequential Java like setting.

Watch Next