Module stateright::semantics

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

SequentialSpec is a trait for defining correctness, and Stateright includes reusable implementations such as register and vec. More implementations will be added to cover common data types emulated by distributed systems.

Verifying Concurrent System Implementations

A concurrent system can be verified against an implementation of the SequentialSpec trait by using a tester such as LinearizabilityTester for an expected consistency model. 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.

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

register	Implements SequentialSpec for Register operational semantics.
vec	Implements SequentialSpec for Vec operational semantics.

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.
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).

Traits

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.