Sciweavers

Share
LOGCOM
2007

A Structural Proof of the Soundness of Rely/guarantee Rules

9 years 10 months ago
A Structural Proof of the Soundness of Rely/guarantee Rules
Various forms of rely/guarantee conditions have been used to record and reason about interference in ways that provide compositional development methods for concurrent programs. This paper illustrates such a set of rules and proves their soundness. The underlying concurrent language allows fine-grained interleaving and nested concurrency; it is defined by an operational semantics; the proof that the rely/guarantee rules are consistent with that semantics (including termination) is by a structural induction. A key lemma which relates the states which can arise from the extra interference that results from taking a portion of the program out of context makes it possible to do the proofs without having to perform induction over the computation history. This lemma also offers a way to think about expressibility issues around auxiliary variables in rely/guarantee conditions.
Joey W. Coleman, Cliff B. Jones
Added 16 Dec 2010
Updated 16 Dec 2010
Type Journal
Year 2007
Where LOGCOM
Authors Joey W. Coleman, Cliff B. Jones
Comments (0)
books