Refining rely-guarantee thinking

  1. Lookup NU author(s)
  2. Professor Ian Hayes
  3. Professor Cliff Jones
Author(s)Hayes IJ, Jones CB, Colvin RJ
Publication type Report
Series TitleSchool of Computing Science Technical Report Series
Year2012
DateMay 2012
Report Number1334
Pages35
Full text is available for this publication:
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.
InstitutionSchool of Computing Science, University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
URLhttp://www.cs.ncl.ac.uk/publications/trs/papers/1334.pdf
ActionsLink to this publication