Crate consistency_model

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.

Structs

LinearizabilityTester

This tester captures a potentially concurrent history of operations and validates that it adheres to a SequentialSpec based on the linearizability consistency model. This model requires that operations be applied atomically and that sequenced (non-concurrent) operations are applied in order.

Register

A simple register used to define reference operational semantics via SequentialSpec.

SequentialConsistencyTester

This tester captures a potentially concurrent history of operations and validates that it adheres to a SequentialSpec based on the sequential consistency model. This model requires that operations be applied atomically and that operations within a thread are sequential (they have a total order within the thread).

Enums

RegisterOp

An operation that can be invoked upon a Register, resulting in a RegisterRet

RegisterRet

A return value for a RegisterOp invoked upon a Register.

VecOp

An operation that can be invoked upon a Vec, resulting in a VecRet.

VecRet

A return value for a VecOp invoked upon a Vec.

Traits

ConsistencyTester

An implementation of this trait tests the consistency of a concurrent system with respect to a “reference sequential specification” SequentialSpec. The interface for doing so involves recording operation invocations and returns.

SequentialSpec

An implementation of this trait can serve as a sequential “reference object” (in the sense of an operational specification, not a Rust reference) against which to validate the operational semantics of a more complex system, such as a distributed system.