Unifying Theories of Parallel Programming

Woodcock, Jim (2002) Unifying Theories of Parallel Programming. In: ICFEM 2002: 4th International Conference on Formal Engineering Methods, October 21-25, 2002, Shanghai China. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)


We are developing a shared-variable refinement calculus in the style of the sequential calculi of Back, Morgan, and Morris. As part of this work, we’re studying different theories of shared-variable programming. Using the concepts and notations of Hoare & He’s unifying theories of programming (UTP), we give a formal semantics to a programming language that contains sequential composition, conditional statements, while loops, nested parallel composition, and shared variables. We first give a UTP semantics to labelled action systems, and then use this to give the semantics of our programs. Labelled action systems have a unique normal form that allows a simple formalisation and validation of different logics for reasoning about shared-variable programs. In this paper, we demonstrate how this is done for Lamport’s Concurrent Hoare Logic.

Item Type: Conference or workshop item (Paper)
Additional information: Keynote speech.
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Systems Architecture Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 17:59
Last Modified: 25 Jun 2014 13:34
Resource URI: http://kar.kent.ac.uk/id/eprint/13680 (The current URI for this page, for reference purposes)
ORCiD (Woodcock, Jim):
  • Depositors only (login required):