Module stateright::semantics
source · [−]Expand description
This module 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”). Stateright includes reusable implementations such
as register for register-like semantics and 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).
An actor::Id for instance can serve as a thread ID as long as the
actor does not invoke a second operation in parallel with the first. This
restriction only exists for the purposes of verifying consistency semantics,
and actors need not sequence their operations to a concurrent
system outside of that use case. Alternatively, a single actor could maintain
its own ConsistencyTester with local thread IDs for multiple concurrent
invocations.
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.
Modules
Implements SequentialSpec for Register operational semantics.
Implements SequentialSpec for Vec operational semantics.
Implements SequentialSpec for “write-once register” operational semantics.
Structs
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.
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).
Traits
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.
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.