## Proof Methods and Pragmatics for Parallel Programming

**Chris Tofts**
*Abstract:* We define a parallel extension of a standard
imperative programming language, which we call CIMP. This language
has a semantics in the process calculus CCS. In order to
demonstrate that a sub-language of CIMP is deterministic the notion
of a *semi-confluent* process is defined. This process
structure is shown to be preserved by the appropriate equivalences
of CCS, and to have a set of operators which conserve it. We show
that a simple *syntactic* condition on the parallel components
of a program is sufficient to ensure its determinacy. Furthermore
we demonstrate that the deterministic sub-language of CIMP has a
simple functional semantics. We also show that there is a set of
simple transformation rules that can manipulate parallelism whilst
maintaining determinism.

Two proof systems for the language CIMP are studied, they are
based respectively on the approaches of Owicki-Gries and Jones.
These systems are shown to be sound with respect to an
interpretation of the proof rules in Hennessy-Milner logic. We
demonstrate that a knowledge of determinism can greatly ease the
proof burden in both of these methods.

We define a calculus, based on CCS, which permits reasoning
about the temporal properties of concurrent systems. This calculus
is shown to have natural notions of equality and order. Some
example systems are included, in particular a temporal analysis of
an *alternative bit protocol*. We use this calculus to provide
a *timed semantics* for the language CIMP, and examine a timed
proof system based on the system for sequential programs presented
by Nielson.

**PhD Thesis - price £8.00**

*LFCS report ECS-LFCS-91-140 (also published as
CST-74-91)*

Previous |

Index |

Next