Java Reference
In-Depth Information
for the actions. Our memory model therefore needs a consistent way of determining
which reads can see writes early.
Examples such as the one found in
Table 17.6
demonstrate that the specification must
be careful when stating whether a read can see a write that occurs later in the execu-
tion (bearing in mind that if a read sees a write that occurs later in the execution, it
represents the fact that the write is actually performed early).
The memory model takes as input a given execution, and a program, and determines
whether that execution is a legal execution of the program. It does this by gradually
building a set of “committed” actions that reflect which actions were executed by the
program. Usually, the next action to be committed will reflect the next action that can
be performed by a sequentially consistent execution. However, to reflect reads that
need to see later writes, we allow some actions to be committed earlier than other ac-
tions that happen-before them.
Obviously, some actions may be committed early and some may not. If, for example,
one of the writes in
Table 17.6
were committed before the read of that variable, the
read could see the write, and the “out-of-thin-air” result could occur. Informally, we
allow an action to be committed early if we know that the action can occur without
assuming some data race occurs. In
Table 17.6
,
we cannot perform either write early,
because the writes cannot occur unless the reads see the result of a data race.
17.4.9. Observable Behavior and Nonterminating Executions
For programs that always terminate in some bounded finite period of time, their behavior
can be understood (informally) simply in terms of their allowable executions. For programs
that can fail to terminate in a bounded amount of time, more subtle issues arise.
The observable behavior of a program is defined by the finite sets of external actions that
the program may perform. A program that, for example, simply prints “Hello” forever is
described by a set of behaviors that for any non-negative integer
i
, includes the behavior of
printing “Hello”
i
times.
Termination is not explicitly modeled as a behavior, but a program can easily be extended
to generate an additional external action
executionTermination
that occurs when all threads
have terminated.
We also define a special
hang
action. If behavior is described by a set of external actions in-
cluding a
hang
action, it indicates a behavior where after the external actions are observed,
the program can run for an unbounded amount of time without performing any addition-
al external actions or terminating. Programs can hang if all threads are blocked or if the
