Java Reference
In-Depth Information
3.
so
i
|
C
i
=
so
|
C
i
The values written by the writes in
C
i
must be the same in both
E
i
and
E
. Only the reads in
C
i-1
need to see the same writes in
E
i
as in
E
. Formally:
4.
V
i
|
C
i
=
V
|
C
i
5.
W
i
|
C
i-1
=
W
|
C
i-1
All reads in
E
i
that are not in
C
i-1
must see writes that happen-before them. Each read
r
in
C
i
-
C
i-1
must see writes in
C
i-1
in both
E
i
and
E
, but may see a different write in
E
i
from
the one it sees in
E
. Formally:
6.
For any read
r
in
A
i
-
C
i-1
, we have
hb
i
(W
i
(r), r)
7.
For any read
r
in (
C
i
-
C
i-1
), we have
W
i
(r)
in
C
i-1
and
W(r)
in
C
i-1
Given a set of sufficient synchronizes-with edges for
E
i
, if there is a release-acquire pair
in all
E
j
, where
j
≥
i
. Formally:
8.
Let
ssw
i
be the
sw
i
edges that are also in the transitive reduction of
hb
i
but not in
po
. We call
ssw
i
the
sufficient synchronizes-with edges for
E
i
. If
ssw
i
(x, y)
and
hb
i
(y, z)
and
z
in
C
i
, then
sw
j
(x, y)
for all
j
≥
i
.
If an action
y
is committed, all external actions that happen-before
y
are also com-
mitted.
9.
If
y
is in
C
i
,
x
is an external action and
hb
i
(x, y)
, then
x
in
C
i
.
Example 17.4.8-1. Happens-before Consistency Is Not Sufficient
Happens-before consistency is a necessary, but not sufficient, set of constraints.
Merely enforcing happens-before consistency would allow for unacceptable behavi-
ors - those that violate the requirements we have established for programs. For ex-
ample, happens-before consistency allows values to appear “out of thin air”. This can
be seen by a detailed examination of the trace in
Table 17.6
.
