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 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: 2014
Pages: 66
Print publication date: 14/07/2014
Source Publication Date: July 2014
Report Number: 1425
Institution: School of Computing Science, University of Newcastle upon Tyne
Place Published: Newcastle upon Tyne
URL: http://www.cs.ncl.ac.uk/publications/trs/papers/1425.pdf
