Refining rely-guarantee thinking (2012)

Author(s): Hayes IJ, Jones CB, Colvin RJ

    Abstract: Reasoning about concurrent programs can be very difficult due to the possibility of interference. The fundamentalinsight of Rely-Guarantee thinking is that developing concurrent designs can only be made compositional if thedevelopment method offers ways to record and reason about the interference that is inherent in concurrency. Theoriginal presentation of rely-guarantee rules used keywords to mark the various predicates and even the read/writeframes of operations. Subsequent papers have moved to a more general message of “rely-guarantee thinking” butretained this VDM flavour and have typically presented a development style in terms of inference rules based onHoare-like triples, extended to quintuples to accommodate rely and guarantee conditions. Morgan’s refinementcalculus presents concise rules that lend themselves to algebraic arguments. This paper reports on a completereformulation of the key ideas of rely-guarantee reasoning in a refinement calculus style. As is shown, thisindicates new useful and intuitive manipulations of rely/guarantee specifications. The approach makes use of twonew commands: a guarantee command (guar g _ c) that behaves like the command c but also guarantees everyatomic step satisfies the relation g, and a rely command (rely r _ c) that behaves like c provided any interferencesteps from the environment satisfy the relation r or stutter. Further notational developments result from the use ofa more compact notation to indicate the read/write frame of a command. The new rules are justified with respect toan operational semantics presented in the Colvin style.

      • Date: May 2012
      • Series Title: School of Computing Science Technical Report Series
      • Pages: 35
      • Institution: School of Computing Science, University of Newcastle upon Tyne
      • Publication type: Report
      • Bibliographic status: Published

      Keywords: FORMAL METHODS CONCURRENCY RELY/GUARANTEE REASONING SPECIFICATION STATEMENTS INVARIANTS

      Staff

      Professor Ian Hayes
      Guest Member of Staff

      Professor Cliff Jones
      Professor

      • Telephone: +44 191 208 8183