Java Reference
In-Depth Information
•
po
- program order, which for each thread
t
, is a total order over all actions per-
formed by
t
in
A
•
so
- synchronization order, which is a total order over all synchronization actions
in
A
•
W
- a write-seen function, which for each read
r
in
A
, gives
W(r)
, the write action
seen by
r
in
E
.
•
V
- a value-written function, which for each write
w
in
A
, gives
V(w)
, the value
written by
w
in
E
.
•
sw
- synchronizes-with, a partial order over synchronization actions
•
hb
- happens-before, a partial order over actions
Note that the synchronizes-with and happens-before elements are uniquely determined by
An execution is
happens-before consistent
if its set of actions is
happens-before consistent
17.4.7. Well-Formed Executions
We only consider well-formed executions. An execution
E
= <
P, A, po, so, W, V, sw, hb
>
is well formed if the following conditions are true:
1.
Each read sees a write to the same variable in the execution.
All reads and writes of volatile variables are volatile actions. For all reads
r
in
A
,
we have
W(r)
in
A
and
W(r).v
=
r.v
. The variable
r.v
is volatile if and only if
r
is a
volatile read, and the variable
w.v
is volatile if and only if
w
is a volatile write.
2.
The happens-before order is a partial order.
The happens-before order is given by the transitive closure of synchronizes-with
edges and program order. It must be a valid partial order: reflexive, transitive and
antisymmetric.
3.
The execution obeys intra-thread consistency.
For each thread
t
, the actions performed by
t
in
A
are the same as would be gener-
ated by that thread in program-order in isolation, with each write
w
writing the
value
V(w)
, given that each read
r
sees the value
V(W(r))
. Values seen by each read
are determined by the memory model. The program order given must reflect the
program order in which the actions would be performed according to the intra-
thread semantics of
P
.
