Generalised rely-guarantee concurrency: An algebraic foundation

TL;DR

This paper develops a generalized algebraic framework for rely-guarantee concurrency, extending traditional relation-based methods to process-based interference, and introduces new operators with algebraic properties.

Contribution

It introduces a process-based approach to rely-guarantee reasoning, generalizing existing relation-based laws with new operators and algebraic properties.

Findings

General rely-guarantee laws derived for process interference

Introduction of a weak conjunction operator for processes

Development of a rely quotient operator for processes

Abstract

The rely-guarantee technique allows one to reason compositionally about concurrent programs. To handle interference the technique makes use of rely and guarantee conditions, both of which are binary relations on states. A rely condition is an assumption that the environment performs only atomic steps satisfying the rely relation and a guarantee is a commitment that every atomic step the program makes satisfies the guarantee relation. In order to investigate rely-guarantee reasoning more generally, in this paper we allow interference to be represented by a process rather than a relation and hence derive more general rely-guarantee laws. The paper makes use of a weak conjunction operator between processes, which generalises a guarantee relation to a guarantee process, and introduces a rely quotient operator, which generalises a rely relation to a process. The paper focuses on the algebraic properties of the general rely-guarantee theory. The Jones-style rely-guarantee theory can be interpreted as a model of the general algebraic theory and hence the general laws presented here hold for that theory.