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

Abstract

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 Concur- rent Kleene Algebra (CKA). This includes the notions of skip, atomic actions, iteration, and non-deterministic, sequential, and parallel compo- sition. 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.