Reasoning about Concurrent Programs: Refining rely-guarantee thinking (2013)

Author(s): Hayes IJ, Jones CB, Colvin RJ

    Abstract: Interference is the essence of concurrency and it is what makesreasoning 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 thatoffer ways to record and reason about interference.In this way of thinking, a \emph{rely} relation records assumptions aboutthe behaviour of the \emph{environment}, and a \emph{guarantee} relation recordscommitments about the behaviour of the \emph{process}. The standardapplication 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 thinkinginto a refinement calculus for concurrent programs, in which programs aredeveloped in (small) steps from an abstract specification.As is usual, we extend the implementation language with specificationconstructs (the extended language is sometimes called a wide-spectrumlanguage), 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 morepowerful refinement laws, most notably, a law for decomposing aspecification into a parallel composition, are developed from a smallset of more primitive lemmas, which are proved sound with respect to anoperational semantics.

      • Journal: Transactions on Programming Languages and Systems
      • Publisher: ACM
      • Publication type: Article
      • Bibliographic status: Unpublished
        Staff

        Professor Cliff Jones
        Professor

        • Telephone: +44 191 208 8183