Operational semantics

The semantics for the atomic region reflects our intention to treat atomic regions as uninterruptable. This is achieved by the transition rule below.

To interpret the execution of atomic regions as one-step program executions serves the aim of preventing other subprograms for intervening in the computation of the atomic region. The properties of absence of blocking and of determinism stated in the previous chapter can be stated only with modifications here. The absence of blocking remains valid however.

Lemma 110. Let S be shared variable parallel program different from the empty program, let . Then there exists and such that .

Contrary to the previous chapter we do not have the disjointness condition now. This suggests that the Church-Rosser property is not valid in this case, as the following trivial example already shows this.

Example 111. Consider the programs of Example 108. Let . Then there are and such that

with and

with . Thus is not confluent.

A statement asserting a property little weaker than nondeterminism can be formulated in this case, though. Without proofs we assert some lemmas and, finally, the lemma of bounded nondeterminism as a corollary of them.

Lemma 112. (Finiteness) For every parallel program S and state s, the configuration has only finitely many successors.

The proof hinges on a straightforward case distinction with respect to the formation of S.

Definition 113. A tree is finitely branching of every node has only finitely many successors.

Thus, Lemma 112 states that for every program S and state s the tree depicting the computations starting from is finitely branching. The next lemma is the well-known König’s lemma.

Lemma 114. (König) Every finitely branching tree is either finite or possesses an infinite branch.

From this, and Lemma 112 we obtain the following result.

Lemma 115. (Bounded nondeterminism) Let S be a parallel program and . Then either the tree representing all the computations starting from is finite or it has an infinite branch.