A Marriage of Rely/Guarantee and Separation Logic

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. The authors propose a combined system which marries the two approaches. They can describe interference naturally (using a relation as in rely/guarantee), and where there is no interference, they can reason locally (as in separation logic).