Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges

An algebra for rely/guarantee concurrency has been constructed via a hierarchy of algebraic theories starting from basic theories like lattices through to theories of synchronous behaviour of atomic steps and a theory to support localisation. The algebra is supported by a model based on Aczel traces. We examine the role of these theories in developing a mechanised theory for deriving concurrent programs and outline some of the challenges remaining.