Toggle Main Menu Toggle Search

ePrints

Reasoning about concurrent programs: Refining rely-guarantee thinking

Lookup NU author(s): Professor Ian Hayes, Professor Cliff Jones

Downloads


Abstract

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.


Publication metadata

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


Share