Crate stateright
source ·Expand description
A library for model checking systems, with an emphasis on distributed systems.
Most of the docs are here, but a short book is being written to provide a gentler introduction: “Building Distributed Systems With Stateright.”
§Introduction to Model Checking
Model
implementations indicate how a system evolves, such as a set of actors
executing a distributed protocol on an IP network. Incidentally, that scenario
is so common for model checking that Stateright includes an actor::ActorModel
,
and unlike many model checkers, Stateright is also able to spawn these
actors on a real network.
Models of a system are supplemented with always
and sometimes
properties.
An always
Property
(also known as a safety property or invariant) indicates that a
specific problematic outcome is not possible, such as data inconsistency. A
sometimes
property on the other hand is used to ensure a particular outcome
is reachable, such as the ability for a distributed system to process a write
request.
A Checker
will attempt to discover a counterexample
for every always
property and an example for every sometimes
property,
and these examples/counterexamples are indicated by sequences of system steps
known as Path
s (also known as traces or behaviors). The presence of an
always
discovery or the absence of a sometimes
discovery indicate that
the model checker identified a problem with the code under test.
§Example
A toy example that solves a sliding puzzle
follows. This simple example leverages only a sometimes
property,
but in most cases for a real system you would have an always
property at
a minimum. The imagined use case is one in which we must ensure that a particular
configuration of the puzzle has a solution.
TIP: see the actor
module documentation for an actor system example.
More sophisticated examples
are available in the examples/
directory of the repository
use stateright::*;
#[derive(Clone, Debug, Eq, PartialEq)]
enum Slide { Down, Up, Right, Left }
struct Puzzle([u8; 9]);
impl Model for Puzzle {
type State = [u8; 9];
type Action = Slide;
fn init_states(&self) -> Vec<Self::State> {
vec![self.0]
}
fn actions(&self, _state: &Self::State, actions: &mut Vec<Self::Action>) {
actions.append(&mut vec![
Slide::Down, Slide::Up, Slide::Right, Slide::Left
]);
}
fn next_state(&self, last_state: &Self::State, action: Self::Action) -> Option<Self::State> {
let empty = last_state.iter().position(|x| *x == 0).unwrap();
let empty_y = empty / 3;
let empty_x = empty % 3;
let maybe_from = match action {
Slide::Down if empty_y > 0 => Some(empty - 3), // above
Slide::Up if empty_y < 2 => Some(empty + 3), // below
Slide::Right if empty_x > 0 => Some(empty - 1), // left
Slide::Left if empty_x < 2 => Some(empty + 1), // right
_ => None
};
maybe_from.map(|from| {
let mut next_state = *last_state;
next_state[empty] = last_state[from];
next_state[from] = 0;
next_state
})
}
fn properties(&self) -> Vec<Property<Self>> {
vec![Property::<Self>::sometimes("solved", |_, state| {
let solved = [0, 1, 2,
3, 4, 5,
6, 7, 8];
state == &solved
})]
}
}
let checker = Puzzle([1, 4, 2,
3, 5, 8,
6, 7, 0])
.checker().spawn_bfs().join();
checker.assert_properties();
checker.assert_discovery("solved", vec![
Slide::Down,
// ... results in:
// [1, 4, 2,
// 3, 5, 0,
// 6, 7, 8]
Slide::Right,
// ... results in:
// [1, 4, 2,
// 3, 0, 5,
// 6, 7, 8]
Slide::Down,
// ... results in:
// [1, 0, 2,
// 3, 4, 5,
// 6, 7, 8]
Slide::Right,
// ... results in:
// [0, 1, 2,
// 3, 4, 5,
// 6, 7, 8]
]);
§What to Read Next
The actor
and semantics
submodules will be of particular interest to
most individuals.
Also, as mentioned earlier, you can find more examples in the Stateright repository.
Modules§
- This module provides an Actor trait, which can be model checked using
ActorModel
. You can alsospawn()
the actor in which case it will communicate over a UDP socket. - 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.
- Utilities such as
HashableHashSet
andHashableHashMap
. Those two in particular are useful because the correspondingHashSet
andHashMap
do not implementHash
, meaning they cannot be used directly in models.
Structs§
- A path of states including actions. i.e.
state --action--> state ... --action--> state
. - A
CheckerVisitor
that records paths visited by the model checker. - A named predicate, such as “an epoch sometimes has no leader” (for which the the model checker would find an example) or “an epoch always has at most one leader” (for which the model checker would find a counterexample) or “a proposal is eventually accepted” (for which the model checker would find a counterexample path leading from the initial state through to a terminal state).
- A
RewritePlan<R>
is derived from a data structure instance and indicates how values of typeR
(short for “rewritten”) should be rewritten. When that plan is recursively applied viaRewrite
, the resulting data structure instance will be behaviorally equivalent to the original data structure under a symmetry equivalence relation, enabling symmetry reduction. - A
CheckerVisitor
that records states evaluated by the model checker. Does not record generated states that are still pending property evaluation. - A chooser that makes uniform choices.
Enums§
- The classification of a property discovery.
- Indicates whether a property is always, eventually, or sometimes true.
Traits§
- Implementations perform
Model
checking. - Choose transitions in the model.
- This is the primary abstraction for Stateright. Implementations model a nondeterministic system’s evolution. If you are using Stateright’s actor framework, then you do not need to implement this interface and can instead leverage
actor::Actor
andactor::ActorModel
. - This trait is used to reduce the state space when checking a model with
CheckerBuilder::symmetry
. The trait indicates the ability to generate a representative from a symmetry equivalence class for each state inModel::State
. - Implementations can rewrite their instances of the “rewritten” type
R
based on a specifiedRewritePlan
.