Testing and verifying concurrent objects (Q1803302)

A concurrent object is a data structure shared by concurrent processes. We present a two-pronged approach for establishing the correctness of implementations of concurrent objects. Our approach is based on a notion of correctness called linearizability: each concurrent object has a sequential specification, which describes how it behaves in sequential executions. Each concurrent execution is required to be equivalent to some sequential execution. We advocate using both testing and verification as complementary approaches for showing a concurrent object is linearizable. We first describe a simulation environment for simulating, testing, and analyzing implementations of concurrent objects. We can use the simulator to gain assurance that an implementation is correct or to detect errors in an incorrect one. The simulator provides a systematic way to testing implementations of any data type. Whereas testing is useful in practice, verification is more definitive. We provide a library of verified concurrent objects; specifically, we give the specifications, implementations, and proofs of correctness for the FIFO queue, semiqueue, and stuttering queue data types. Implementors of objects of other data types can use our library by following the patterns of design and proof that we give; at the same time, clients of our library need not reimplement commonly used abstractions from scratch and are freed from the tedium of their verification.