Handling localisation in rely/guarantee concurrency: An algebraic approach

TL;DR

This paper introduces an algebraic framework for handling local variables in rely/guarantee concurrency, enabling formal reasoning about shared-variable concurrent programs with local and shared states.

Contribution

It develops a synchronous concurrent refinement algebra with a primitive localisation operator to formalize local variables in rely/guarantee concurrency.

Findings

Proves properties of localisation and its interaction with rely and guarantee conditions.

Defines a small set of primitive commands and operators for the algebraic framework.

Supports mechanisation of rely/guarantee reasoning with local variables.

Abstract

The rely/guarantee approach of Jones extends Hoare logic with rely and guarantee conditions in order to allow compositional reasoning about shared-variable concurrent programs. This paper focuses on localisation in the context of rely/guarantee concurrency in order to support local variables. Because we allow the body of a local variable block to contain component processes that run in parallel, the approach needs to allow variables local to a block to become shared variables of its component parallel processes. To support the mechanisation of the rely/guarantee approach, we have developed a synchronous concurrent refinement algebra. Its foundation consists of a small set of primitive commands plus a small set of primitive operators from which all remaining constructs are defined. To support local variables we add a primitive localisation operator to our algebra that is used to define local variable blocks. From this we can prove properties of localisation, including its interaction with rely and guarantee conditions.