Towards an Algebra for Unifying Theories of Concurrent Programming (UTCP)

Unifying Theories of Concurrent Programming (UTCP) is a denotational semantics of shared-variable concurrency, expressed using the notation and methodology of Unifying Theories of Programming (UTP). A key feature is that it is compositional, in that the semantics of a composite is described in terms of the semantics of its sub-components. The underlying language used is that which is used to define a Concurrent Kleene Algebra (CKA). This includes the notions of skip, atomic actions, iteration, and non-deterministic, sequential, and parallel composition. This chapter makes progress toward proving that UTCP satisfies the CKA laws. We describe the methodology used, and give proofs for key ideas, as well as proofs and proof-sketches for many of the laws. We also discuss open issues, the most notable being the precise nature of miracle in this setting. The chapter finishes with a roadmap of how we might encode well-established UTP concepts such as Designs and Reactive Systems on top of UTCP.