Java Reference
In-Depth Information
Therefore, a data race cannot cause incorrect behavior such as returning the wrong
length for an array.
A program is
correctly synchronized
if and only if all sequentially consistent executions
are free of data races.
If a program is correctly synchronized, then all executions of the program will appear to be
This is an extremely strong guarantee for programmers. Programmers do not need to
reason about reorderings to determine that their code contains data races. Therefore
they do not need to reason about reorderings when determining whether their code is
correctly synchronized. Once the determination that the code is correctly synchron-
ized is made, the programmer does not need to worry that reorderings will affect his
or her code.
A program must be correctly synchronized to avoid the kinds of counterintuitive be-
haviors that can be observed when code is reordered. The use of correct synchroniz-
ation does not ensure that the overall behavior of a program is correct. However, its
use does allow a programmer to reason about the possible behaviors of a program in a
simple way; the behavior of a correctly synchronized program is much less dependent
on possible reorderings. Without correct synchronization, very strange, confusing and
counterintuitive behaviors are possible.
We say that a read
r
of a variable
v
is allowed to observe a write
w
to
v
if, in the
happens-
before
partial order of the execution trace:
•
r
is not ordered before
w
(i.e., it is not the case that
hb(r, w)
), and
• there is no intervening write
w
' to
v
(i.e. no write
w
' to
v
such that
hb(w, w')
and
hb(w', r)
).
Informally, a read
r
is allowed to see the result of a write
w
if there is no
happens-before
ordering to prevent that read.
A set of actions
A
is
happens-before consistent
if for all reads
r
in
A
, where
W(r)
is the
write action seen by
r
, it is not the case that either
hb(r, W(r))
or that there exists a write
w
in
A
such that
w.v
=
r.v
and
hb(W(r), w)
and
hb(w, r)
.
In a
happens-before consistent
set of actions, each read sees a write that it is allowed to see
by the
happens-before
ordering.
