P in Program
C in Command
E in Expression
B in Boolean-expr
I in Identifier
P ::= C.
C ::= I := E | C_1; C_2 | C1
|| C2
|
if B then C_1
else C_2 | while B do C
- Parallel evaluation operator ||.
- Assignment is non-interruptable.
- Exclusive access to store.
- Interleaving semantics
- Evaluation of C_1||C_2 interleaves assignments of
C_1 with those of C_2.
- Semantics of C_1||C_2 generates set of results of
all possible interleavings.