Interrupt this thread.
Interrupt this thread.
Has this tester been interrupted?
Has this tester been interrupted?
Note that the solve method must detect that this variable has been set, and return Solver.Interrupted.
Make an invocation event.
Make an invocation event.
Make a return event.
Make a return event.
Run the linearization tester, assuming the log has already been generated.
Run the linearization tester, assuming the log has already been generated.
Solver.Success to indicate the linearization succeeded; Solver.OutOfSteam to indicate that the test gave up; or Solver.Failure to indicate that the linearization failed.
A linearization tester.
This is the tester referred to as the Wing & Gong Tree Search Algorithm in the paper Testing for Linearizability, Gavin Lowe. See that paper for more explanation of the technique.
The algorithm is based on Testing and Verifying Concurrent Objects, by Jeannette Wing and Chun Gong.
the type of sequential spedicifation objects