This library provides code to define and verify the correctness of an object or system based on how it responds to a collection of potentially concurrent (i.e. partially ordered) operations.

Defining Correctness Via A Reference Implementation

SequentialSpec is a trait for defining correctness via a "reference implementation" (e.g. "this system should behave like a queue"). This library includes reusable implementations such as Register for register-like semantics and for the standard library's [Vec] for stack-like semantics. Implementing the trait yourself is also straightforward -- just define two enums for invocations and returns. Then associate these (as SequentialSpec::Op and SequentialSpec::Ret respectively) with a state type that implements SequentialSpec::invoke.

Verifying Concurrent System Implementations

A concurrent system can be verified against an implementation of the SequentialSpec trait by using a ConsistencyTester for an expected consistency model, such as LinearizabilityTester. In that case, operations are sequential (think blocking I/O) with respect to an abstract thread-like caller, which is identified by a distinct "thread ID" (sometimes called a "process ID" in the literature, but these are assumed to be single-threaded, so thread ID arguably provides better intuition for most developers).

Additional Reading

For more background on specifying the semantics of concurrent systems, see publications such as:

• "Consistency in Non-Transactional Distributed Storage Systems" by Viotti and Vukolić
• "Principles of Eventual Consistency" by Burckhardt
• "Software Foundations Volume 2: Programming Language Foundations" by Pierce et al.