  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.
