Browse by author
Lookup NU author(s): Professor Ian Hayes, Emeritus Professor Cliff JonesORCiD
Interference is the essence of concurrency and it is what makes reasoning about concurrent programs difficult. The fundamental insight of rely-guarantee thinking is that stepwise design of concurrent programs can only be compositional in development methods that offer ways to record and reason about interference. In this way of thinking, a rely relation records assumptions about the behaviour of the environment, and a guarantee relation records commitments about the behaviour of the process. The standard application of these ideas is in the extension of Hoare-like inference rules to quintuples that accommodate rely and guarantee conditions. In contrast, in this paper, we embed rely-guarantee thinking into a refinement calculus for concurrent programs, in which programs are developed in (small) steps from an abstract specification. As is usual, we extend the implementation language with specification constructs (the extended language is sometimes called a wide-spectrum language), in this case adding (in addition to pre and postconditions) two new commands: a guarantee command guar(g)(c) whose valid behaviours are in accord with the command c but all of whose atomic steps also satisfy the relation g, and a rely command rely(r)(c) whose behaviours are like c provided any interference steps from the environment satisfy the relation r. The theory of concurrent program refinement is based on a theory of atomic program steps and more powerful refinement laws, most notably, a law for decomposing a specification into a parallel composition, are developed from a small set of more primitive lemmas, which are proved sound with respect to an operational semantics.
Author(s): Hayes IJ, Jones CB, Colvin RJ
Publication type: Report
Publication status: Published
Series Title: School of Computing Science Technical Report Series
Year: 2013
Pages: 66
Print publication date: 01/09/2013
Source Publication Date: September 2013
Report Number: 1395
Institution: Newcastle University
Place Published: Newcastle upon Tyne
URL: http://www.cs.ncl.ac.uk/publications/trs/papers/1395.pdf
