UTCP: Compositional semantics for shared-variable concurrency

Abstract

We present a Unifying Theories of Programming (UTP) semantics of shared variable concurrency that is fully compositional. Previous work was based on mapping such programs, using labelling of decision points and atomic actions, to action systems, which themselves were provided with a UTP semantics. The translation to action systems was largely compositional, but their dynamic semantics was based on having all the actions collected together. Here we take a more direct approach, albeit inspired by the action-systems view, based on an abstract notion of label generation, that then exploits the standard use of substitution in UTP, to obtain a fully compositional semantics.