Crate consistency_model
source ·Expand description
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 enum
s 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
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.SequentialSpec
.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
Register
, resulting in a
RegisterRet
RegisterOp
invoked upon a Register
.Traits
SequentialSpec
. The interface for doing so involves
recording operation invocations and returns.