consistency_model/
lib.rs

1//! This library provides code to define and verify the correctness of
2//! an object or system based on how it responds to a collection of potentially
3//! concurrent (i.e. partially ordered) operations.
4//!
5//! # Defining Correctness Via A Reference Implementation
6//!
7//! [`SequentialSpec`] is a trait for defining correctness via a "reference implementation"
8//! (e.g.  "*this system should behave like a queue*").  This library includes reusable
9//! implementations such as [`Register`] for register-like semantics and for the standard
10//! library's [`Vec`] for stack-like semantics.  Implementing the trait yourself is also
11//! straightforward -- just define two `enum`s for invocations and returns. Then associate
12//! these (as [`SequentialSpec::Op`] and [`SequentialSpec::Ret`] respectively) with a state
13//! type that implements [`SequentialSpec::invoke`].
14//!
15//! # Verifying Concurrent System Implementations
16//!
17//! A concurrent system can be verified against an implementation of the [`SequentialSpec`] trait
18//! by using a [`ConsistencyTester`] for an expected [consistency model],  such as
19//! [`LinearizabilityTester`]. In that case, operations are sequential (think blocking I/O) with
20//! respect to an abstract thread-like caller, which is identified by a distinct "thread ID"
21//! (sometimes called a "process ID" in the literature, but these are assumed to be
22//! single-threaded, so thread ID arguably provides better intuition for most developers).
23//!
24//! # Additional Reading
25//!
26//! For more background on specifying the semantics of concurrent systems, see
27//! publications such as:
28//!
29//! - ["Consistency in Non-Transactional Distributed Storage
30//!   Systems"](http://vukolic.com/consistency-survey.pdf) by Viotti and Vukolić
31//! - ["Principles of Eventual
32//!   Consistency"](https://www.microsoft.com/en-us/research/publication/principles-of-eventual-consistency/)
33//!   by Burckhardt
34//! - ["Software Foundations Volume 2: Programming Language
35//!   Foundations"](https://softwarefoundations.cis.upenn.edu/plf-current/index.html)
36//!   by Pierce et al.
37//!
38//! [consistency model]: https://en.wikipedia.org/wiki/Consistency_model
39
40mod consistency_tester;
41mod linearizability;
42mod register;
43mod sequential_consistency;
44mod vec;
45
46pub use consistency_tester::ConsistencyTester;
47pub use linearizability::LinearizabilityTester;
48pub use register::{Register, RegisterOp, RegisterRet};
49pub use sequential_consistency::SequentialConsistencyTester;
50pub use vec::{VecOp, VecRet};
51
52/// An implementation of this trait can serve as a sequential "reference object"
53/// (in the sense of an operational specification, not a Rust reference)
54/// against which to validate the [operational semantics] of a more complex
55/// system, such as a distributed system.
56///
57/// This library includes the following [`ConsistencyTester`]s for verifying that a concurrent system
58/// adheres to an expected [consistency model]:
59///
60/// - [`LinearizabilityTester`]
61/// - [`SequentialConsistencyTester`]
62///
63/// [consistency model]: https://en.wikipedia.org/wiki/Consistency_model
64/// [operational semantics]: https://en.wikipedia.org/wiki/Operational_semantics
65pub trait SequentialSpec: Sized {
66    /// The type of operators. Often an enum.
67    type Op;
68
69    /// The type of values return by the operators. Often an enum or
70    /// [`Option`].
71    type Ret: PartialEq;
72
73    /// Invokes an operation on this reference object.
74    fn invoke(&mut self, op: &Self::Op) -> Self::Ret;
75
76    /// Indicates whether invoking a specified operation might result
77    /// in a specified return value. Includes a default implementation that
78    /// calls `invoke`, but a manual implementation may be provided for
79    /// efficiency purposes (e.g. to avoid a `clone()` call).
80    fn is_valid_step(&mut self, op: &Self::Op, ret: &Self::Ret) -> bool {
81        &self.invoke(op) == ret
82    }
83
84    /// Indicates whether a sequential history of operations and corresponding
85    /// return values is valid for this reference object.
86    fn is_valid_history(&mut self, ops: impl IntoIterator<Item = (Self::Op, Self::Ret)>) -> bool {
87        ops.into_iter()
88            .all(|(op, ret)| self.is_valid_step(&op, &ret))
89    }
90}
consistency_model/lib.rs

consistency_model/
lib.rs
