Computer Science Department
School of Computer Science, Carnegie Mellon University
A Library of Concurrent Objects and Their Proofs of Correctness
Jeannette M. Wing, Chun Gong
This paper presents a library of concurrent objects of different data types: FIFO queues, priority queues, semiqueues, stuttering queues, sets, multiple sets, and registers. For each different kind of concurrent object, we provide a (sequential) specification written in Larch, an implementation in C, and a proof of correctness. We use linearizability as our basic correctness condition.
*Readers may wish to read the companion Technical Report CMU-CS-90-150.