Chapter 5. Synchronization

Table of Contents

Syntax
Semantics
Proof rules for partial correctness
Mutual exclusion

Syntax

There are parallel programs which cannot be described only with communication by shared variables. We also need a construct which enables us to formulate programs the parts of which being able to synchronize with each other. In other words, the components are able to suspend their execution, and wait for a certain condition to be fulfilled. This is achieved by the await construct of Owicki and Gries. Parallel programs with synchronization are formed exactly like parallel programs of the previous two chapters with the additional await construct

Here S is a loop free sequential program not containing any await constructs. A parallel component consists of the constituents of a while program of Chapter 1 and the await construct. Again, nested parallelism is not allowed, but parallel composition can occur inside sequential composition, conditional statements and while loops. The informal explanation for the execution of the await construct is as follows: should the control reach an subprogram in a command the following two cases can happen. If B evaluates to true, then S is executed uninterruptedly as an atomic region. Otherwise, the whole component stalls, and it is allowed to resume execution only if B evaluates to true due to the change of the values of the variables in B by some other components. Of this never happens, then the component remains blocked forever. We introduce two abbreviations:

and

Thus, atomic regions are simply specially formed await statements form now on. In accordance with this, we call a subprogram normal, if it does not lie within an await statement.