Unifying Theories of Parallel Programming

Woodcock, Jim and Hughes, Arthur (2002) Unifying Theories of Parallel Programming. In: Formal Methods and Software Engineering. Lecture Notes in Computer Science, 0302-9743 . Springer Berlin / Heidelberg, pp. 24-37. ISBN 978-3-540-00029-7. (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)
Official URL
http://dx.doi.org/10.1007/3-540-36103-0_5

Abstract

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: Book section
Additional information: Notes for Marktoberdorf Summer School
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: 23 May 2014 08:40
Resource URI: http://kar.kent.ac.uk/id/eprint/13663 (The current URI for this page, for reference purposes)
ORCiD (Woodcock, Jim):
ORCiD (Hughes, Arthur):
  • Depositors only (login required):