Towards an Algebra for Unifying Theories of Concurrent Programming (UTCP) - Butterfield, Andrew (Springer Nature, 2024)
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.
LNCS
The Application of Formal Methods
PUBLISHED
Invited paper
University of York, UK
Keywords: Unifying Theories of Concurrent Programming, Concurrent Kleene Algebra, Denotational Semantics