Java Reference
In-Depth Information
program can perform an unbounded number of actions without performing any external ac-
tions.
A thread can be blocked in a variety of circumstances, such as when it is attempting to ac-
quire a lock or perform an external action (such as a read) that depends on external data.
An execution may result in a thread being blocked indefinitely and the execution's not ter-
minating. In such cases, the actions generated by the blocked thread must consist of all
actions generated by that thread up to and including the action that caused the thread to be
blocked, and no actions that would be generated by the thread after that action.
To reason about observable behaviors, we need to talk about sets of observable actions.
If
O
is a set of observable actions for an execution
E
, then set
O
must be a subset of
E
's
actions,
A
, and must contain only a finite number of actions, even if
A
contains an infinite
number of actions. Furthermore, if an action
y
is in
O
, and either
hb(x, y)
or
so(x, y)
, then
x
is in
O
.
Note that a set of observable actions are not restricted to external actions. Rather, only ex-
ternal actions that are in a set of observable actions are deemed to be observable external
actions.
A behavior
B
is an allowable behavior of a program
P
if and only if
B
is a finite set of ex-
ternal actions and either:
• There exists an execution
E
of
P
, and a set
O
of observable actions for
E
, and
B
is
the set of external actions in
O
(If any threads in
E
end in a blocked state and
O
contains all actions in
E
, then
B
may also contain a
hang
action); or
• There exists a set
O
of actions such that
B
consists of a
hang
action plus all the ex-
ternal actions in
O
and for all
k
≥ |
O
|, there exists an execution
E
of
P
with ac-
tions
A
, and there exists a set of actions
O
' such that:
♦ Both
O
and
O
' are subsets of
A
that fulfill the requirements for sets of observ-
able actions.
♦
O
?
O
' ?
A
♦ |
O
' | ≥
k
♦
O
' -
O
contains no external actions
Note that a behavior
B
does not describe the order in which the external actions
in
B
are observed, but other (internal) constraints on how the external actions
are generated and performed may impose such constraints.
