Chapter 4. Shared variable parallelism

Table of Contents

The syntax of shared variable parallel programs
Operational semantics
Deduction system
Soundness and completeness
Case study

The syntax of shared variable parallel programs

Disjoint parallelism appeared to be a restricted form of parallelism, it is closer to applications if we assume that the components of a parallel programs have resources, messages, data, etc. to share. Shared variable parallelism means that there can be common variables which can be modified by several components of the program, accomplishing in this way a method of data exchange and communication. The design of shared variable parallel programs needs more care than that of disjoint parallel programs: parallel components can interfere now with each other, and some of these actions may be unwanted. The introduction of the notion of atomicity handles this phenomenon. This interference also has its effect on the device of inference rules, we have to make sure by parallel execution that none of the components invalidates the inferences made for the other components, to this end we stipulate the property interference freedom for the parallel components. To illustrate the problem mentioned in this paragraph we consider the simple example below ([1]). The syntax of shared variable parallel programs is the same as that of disjoint parallel programs, except for some minor changes which we are going to introduce later.

Example 108. Let

Then the value of X upon termination of can be either 0 or 2. On the other hand, the value of X when has terminated can either be 0, or 1, or 2. The difference can be attributed to the fact that although and behave the same as parallel programs, when composed with the execution of can be interrupted while the execution of cannot.

A solution for this problem is the introduction of the notion of atomicity. We consider a component indivisible or atomic, if, during the execution of which, the other components may not change its variables. Thus a parallel computation in this setting can be considered as a subsequent execution of atomic actions lying in the various components. The execution process is asynchronous: no assumption is made about the time needed by the components for the execution of the atomic actions. Syntactically, we distinguish atomic actions by angle brackets.

Definition 109. Let be a loop-free program and without inner atomic regions. Then is the atomic region consisting of .

The formation rules for parallel programs are thus augmented with the rule for forming atomic regions. As before, besides explicitly defined atomic regions we consider boolean expression and commands and assignments as atomic steps. A subprogram of S is called normal, if it does not occur within an atomic region of S. In what follows, by parallel program we mean shared variable parallel program unless stated otherwise.