Java Reference
In-Depth Information
♦
Lock
. Locking a monitor
♦
Unlock
. Unlocking a monitor.
♦ The (synthetic) first and last action of a thread.
♦ Actions that start a thread or detect that a thread has terminated (§
17.4.4
).
•
External Actions
. An external action is an action that may be observable outside of
an execution, and has a result based on an environment external to the execution.
•
Thread divergence actions
(§
17.4.9
). A thread divergence action is only performed
by a thread that is in an infinite loop in which no memory, synchronization, or ex-
ternal actions are performed. If a thread performs a thread divergence action, it will
be followed by an infinite number of thread divergence actions.
Thread divergence actions are introduced to model how a thread may cause all
other threads to stall and fail to make progress.
This specification is only concerned with inter-thread actions. We do not need to concern
ourselves with intra-thread actions (e.g., adding two local variables and storing the result in
a third local variable). As previously mentioned, all threads need to obey the correct intra-
thread semantics for Java programs. We will usually refere to inter-thread actions more
succinctly as simply
actions
.
An action
a
is described by a tuple <
t
,
k
,
v
,
u
>, comprising:
•
t
- the thread performing the action
•
k
- the kind of action
•
v
- the variable or monitor involved in the action.
For lock actions,
v
is the monitor being locked; for unlock actions,
v
is the monitor
being unlocked.
If the action is a (volatile or non-volatile) read,
v
is the variable being read.
If the action is a (volatile or non-volatile) write,
v
is the variable being written.
•
u
- an arbitrary unique identifier for the action
An external action tuple contains an additional component, which contains the results of
the external action as perceived by the thread performing the action. This may be informa-
tion as to the success or failure of the action, and any values read by the action.
Parameters to the external action (e.g., which bytes are written to which socket) are not part
of the external action tuple. These parameters are set up by other actions within the thread
