A library of concurrent objects and their proofs of correctness

Abstract: "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. The 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."