Abstract

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.