Generalised rely-guarantee concurrency: an algebraic foundation

DOI10.1007/S00165-016-0384-0MaRDI QIDQ333330zbMATH OpenOpenAlexFDO

Publication date 28 October 2016

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.01776

program verification concurrent Kleene algebra concurrent programming program algebra rely-guarantee concurrency

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

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.

Recommendations

Cites work

Cited in

(18)

This page was built for publication: Generalised rely-guarantee concurrency: an algebraic foundation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q333330)