A concurrent object is a data structure shared by concurrent processes. Since proving correctness of an implementation of a concurrent object can be a daunting task, we aim to provide users with a library of "verified" implementations. Users are then freed from having to design, implement, and verify commonly-used abstractions.

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.

22 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by [email protected]