A structural proof of the soundness of rely/guarantee rules (revised)
Joey W. Coleman, Cliff B. Jones · School of Computing Science Technical Report Series · 2007
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. © 2007 University of Newcastle upon Tyne. Printed and published by the University of Newcastle upon Tyne, Computing Science, Claremont Tower, Claremont Road, Newcastle upon Tyne, NE1 7RU, England. Bibliographical details COLEMAN, J. W., JONES, C. B. A structural proof of the soundness of rely/guarantee rules (revised) [By] J. W. Coleman, C. B. Jones. Newcastle upon Tyne: University of Newcastle upon Tyne: Computing Science, 2007. (University of Newcastle upon Tyne, Computing Science, Technical Report Series, No. CS-TR-1029)