A thread has invoked an operation described by msg, corresponding to operation op on the sequential object; this operation has not yet been linearized.
A thread has had an operation linearized, producing res, but this has not yet returned.
The type of states of threads.
A thread is not currently in any operation call
Can t's operation return?
Record t's operation as returned, returning previous state.
Fire t's operation if it produces the expected value.
Fire t's operation if it produces the expected value. Pre: t has a pending operation.
Either t's previous state (if successful) or the result produced (otherwise).
Try to return t's operation, firing it if it hasn't already been fired and produces the expected value.
Try to return t's operation, firing it if it hasn't already been fired and produces the expected value.
Either t's previous state (if successful) or the result produced (otherwise).
Does t have a pending operation?
Add that op is invoked by t.
Undo the last event, resetting t's state to prev.
Undo invocation of op by t.
A configuration, with undoing. Used in the JITLinUndoTester.