Refining rely-guarantee thinking
Ian J. Hayes, Cliff B. Jones, Robert J. Colvin · School of Computing Science Technical Report Series · 2012
Reasoning about concurrent programs can be very difficult due to the possibility of interference. The fundamental insight of Rely-Guarantee thinking is that developing concurrent designs can only be made compositional if the development method offers ways to record and reason about the interference that is inherent in concurrency. The original presentation of rely-guarantee rules used keywords to mark the various predicates and even the read/write frames of operations. Subsequent papers have moved to a more general message of “rely-guarantee thinking” but retained this VDM flavour and have typically presented a development style in terms of inference rules based on Hoare-like triples, extended to quintuples to accommodate rely and guarantee conditions. Morgan’s refinement calculus presents concise rules that lend themselves to algebraic arguments. This paper reports on a complete reformulation of the key ideas of rely-guarantee reasoning in a refinement calculus style. As is shown, this indicates new useful and intuitive manipulations of rely/guarantee specifications. The approach makes use of two new commands: a guarantee command (guar g _ c) that behaves like the command c but also guarantees every atomic step satisfies the relation g, and a rely command (rely r _ c) that behaves like c provided any interference steps from the environment satisfy the relation r or stutter. Further notational developments result from the use of a more compact notation to indicate the read/write frame of a command. The new rules are justified with respect to an operational semantics presented in the Colvin style.