Local Rely-Guarantee Reasoning

Local Rely-Guarantee Reasoning, Xinyu Feng. Accepted for publication at POPL 2009.

Rely-Guarantee reasoning is a well-known method for verification of shared-variable concurrent programs. However, it is difficult for users to define rely/guarantee conditions, which specify threads' behaviors over the whole program state. Recent efforts to combine Separation Logic with Rely-Guarantee reasoning have made it possible to hide thread-local resources, but the shared resources still need to be globally known and specified. This greatly limits the reuse of verified program modules.

In this paper, we propose LRG, a new Rely-Guarantee-based logic that brings local reasoning and information hiding to concurrency verification. Our logic, for the first time, supports a frame rule over rely/guarantee conditions so that specifications of program modules only need to talk about the resources used locally, and the certified modules can be reused in different threads without redoing the proof. Moreover, we introduce a new hiding rule to hide the resources shared by a subset of threads from the rest in the system. The support of information hiding not only improves the modularity of Rely-Guarantee reasoning, but also enables the sharing of dynamically allocated resources, which requires adjustment of rely/guarantee conditions.

In the beginning there was Hoare logic, which taught us how to reason about sequential, imperative programs. Then, Owicki and Gries extended Hoare logic with some additional rules that enabled reasoning about some concurrent imperative programs. This was good, but there were a lot of "obviously correct" concurrent programs that it couldn't handle. So Owicki-Gries logic begat two children.

The elder child was Jones's introduction of the rely-guarantee method. The intuition here is that if you have two subprograms M1 and M2, and M1 will work in an environment with a working M2, and M2 will work in an environment with a working M1, then when you put the two together you have a working M1 and M2. This is a really powerful reasoning method, but unfortunately it's not terribly modular.

The younger child of Owicki-Gries was concurrent separation logic. The intuition behind it is that if you can divide the heap into disjoint (logical) pieces, and only let one process access each chunk at a time, then you can't have any race conditions. This is a very simple principle, and permits modular, compositional reasoning about concurrent programs -- even pointer programs. But there are programs that can't be proven in this style.

So the obvious thing to want is the ability to combine these two styles of reasoning. Unfortunately, this is hard -- there have been several logics proposed to do this, each of which does a bit better than the last. Feng's is the latest, and the best I've seen so far. (Though concurrency is not really my area.)

An interesting point is that these kinds of reasoning principles, while invented for the concurrent world, are also interesting for reasoning about modular sequential programs. This is because when you create imperative abstractions, it's helpful to be able to give up knowledge about exactly when state changes can happen. So you need the same sorts of techniques to handle this kind of conceptual nondeterminism that you need for the actual nondeterminism of parallel hardware.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

General RG Reasoning

For contrast, I recommend looking at the recent paper "A Unified Theory of Program Logics: an approach based on the pi-calculus" by Kohei Honda and Nobuko Yoshida, presented a few weeks ago at the BCS meeting in London and the ICALP 2008 publication "Completeness and Logical Full Abstraction in Modal Logics for Typed Mobile Processes" by the same authors, which is a very general account of rely-guarantee reasoning.


Is there a version of the "Unified Theory" paper available online somewhere? I have not been able to find one via BCS, or on either of the author's websites.

Maybe Mail The Authors.

The authors presented that paper at the BCS meeting. I'm sure they would be happy to mail you a copy: kohei@dcs.qmul.ac.uk.

BTW, congratulations to neelk, the author of the original post on his very nice POPL paper "Focusing on Pattern Matching".

Clojure Concurrency and Thread Safety Verification

Does a new language like Clojure with such powerful tools for constructing safe multi-threaded applications make these types of logics less vital (since developers can choose more thread-sane languages like Clojure now rather than using insane threading approaches and attempting to verify them)?

Owicki-Gries logic

Actually there are two Owicki-Gries logic:
An Axiomatic Proof Technique for Parallel Programs I
in Acta Informatica Vol. 6, 1976
Verifying Properties of Parallel Programs: An Axiomatic Approach.
in CACM 19(5), 1976.

I would say rely-guarantee is the child of the first logic, and CSL is the child of the second one :-)