## User login## Navigation |
## Local Rely-Guarantee ReasoningLocal Rely-Guarantee Reasoning, Xinyu Feng. Accepted for publication at POPL 2009.
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 |
## Browse archives## Active forum topics |

## Recent comments

25 min 1 sec ago

27 min 8 sec ago

59 min 40 sec ago

2 hours 25 min ago

4 hours 59 min ago

7 hours 16 min ago

8 hours 52 min ago

9 hours 24 min ago

10 hours 6 min ago

11 hours 50 min ago