An algebra of synchronous atomic steps
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.
Cite
@article{arxiv.1609.00118,
title = {An algebra of synchronous atomic steps},
author = {Ian J. Hayes and Robert Colvin and Larissa Meinicke and Kirsten Winter and Andrius Velykis},
journal= {arXiv preprint arXiv:1609.00118},
year = {2022}
}