Java Reference
In-Depth Information
5.
The execution obeys synchronization-order consistency.
For all volatile reads
r
in
A
, it is not the case that either
so(r, W(r))
or that there ex-
ists a write
w
in
A
such that
w.v
=
r.v
and
so(W(r), w)
and
so(w, r)
.
17.4.8. Executions and Causality Requirements
We use
f
|
d
to denote the function given by restricting the domain of
f
to
d
. For all
x
in
d
,
f
|
d
(
x
) =
f
(
x
), and for all
x
not in
d
,
f
|
d
(
x
) is undefined.
We use
p
|
d
to represent the restriction of the partial order
p
to the elements in
d
. For
all
x
,
y
in
d
,
p
(
x
,
y
) if and only if
p
|
d
(
x
,
y
). If either
x
or
y
are not in
d
, then it is not the
case that
p
|
d
(
x
,
y
).
A well-formed execution
E
= <
P, A, po, so, W, V, sw, hb
> is validated by
committing
actions from
A
. If all of the actions in
A
can be committed, then the execution satisfies the
causality requirements of the Java programming language memory model.
Starting with the empty set as
C
0
, we perform a sequence of steps where we take actions
from the set of actions
A
and add them to a set of committed actions
C
i
to get a new set
of committed actions
C
i+1
. To demonstrate that this is reasonable, for each
C
i
we need to
demonstrate an execution
E
containing
C
i
that meets certain conditions.
Formally, an execution
E satisfies the causality requirements of the Java programming lan-
guage memory model
if and only if there exist:
• Sets of actions
C
0
,
C
1
, ... such that:
♦
C
0
is the empty set
♦
C
i
is a proper subset of
C
i+1
♦
A
=
∪
(
C
0
,
C
1
, ...)
If
A
is finite, then the sequence
C
0
,
C
1
, ... will be finite, ending in a set
C
n
=
A
.
If
A
is infinite, then the sequence
C
0
,
C
1
, ... may be infinite, and it must be the case
that the union of all elements of this infinite sequence is equal to
A
.
• Well-formed executions
E
1
, ..., where
E
i
= <
P, A
i
, po
i
, so
i
, W
i
, V
i
, sw
i
, hb
i
>.
Given these sets of actions
C
0
, ... and executions
E
1
, ... , every action in
C
i
must be one of
the actions in
E
i
. All actions in
C
i
must share the same relative happens-before order and
synchronization order in both
E
i
and
E
. Formally:
1.
C
i
is a subset of
A
i
2.
hb
i
|
C
i
=
hb
|
C
i
