An algebra of synchronous atomic steps

TL;DR

This paper introduces an abstract algebra of atomic steps that models synchronous composition, simplifying rely/guarantee reasoning and unifying various process algebra mechanisms, with formalization in Isabelle/HOL.

Contribution

It presents a novel algebra of atomic steps with synchronous composition, enhancing reasoning simplicity and unification of process algebra concepts.

Findings

Core properties for rely/guarantee reasoning hold in the abstract algebra.

The algebra can interpret standard process algebra mechanisms like CSP and CCS.

The algebra has been formalized in Isabelle/HOL for tool support.

Abstract

This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an interpretation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. Moreover, the realisation that the synchronisation mechanisms of standard process algebras, such as CSP and CCS/SCCS, can be interpreted in our abstract algebra gives evidence of its unifying power. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support.