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.
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 . 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.
The proof hinges on a straightforward case distinction with respect to the formation of S.
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.
From this, and Lemma 112 we obtain the following result.