A structural proof of the soundness of rely/guarantee rules (revised)

  1. Lookup NU author(s)
  2. Dr Joey Coleman
  3. Professor Cliff Jones
Author(s)Coleman JW, Jones CB
Publication type Report
Series TitleSchool of Computing Science Technical Report Series
Source Publication DateJune 2007
Report Number1029
Full text is available for this publication:
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.
InstitutionSchool of Computing Science, University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
ActionsLink to this publication