A simulator for concurrent objects

Abstract: "A concurrent object is a data structure shared by concurrent processes. This paper describes in detail a simulation package for simulating, testing, and analyzing implementations of concurrent objects. We use linearizability as our fundamental correctness condition, thereby exploiting the semantics of the object's type to enhance the degree of concurrency allowed. The simulator determines for a finite history of operations executed on a concurrent object whether the history is linearizable. The user can give the simulator a finite set of input test histories or let the simulator generate and test an unbounded number."