Computer Science Department
School of Computer Science, Carnegie Mellon University
A Simulator for Concurrent Objects
Jeannette M. Wing, Chun Gong
A @i 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.
*Readers may wish to read the companion Technical Report CMU-CS-90-151.