1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375
//! 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](https://www.stateright.rs)."
//!
//! # 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](https://en.wikipedia.org/wiki/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](https://github.com/stateright/stateright/tree/master/examples)
//!
//! ```rust
//! 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](https://github.com/stateright/stateright/tree/master/examples)
//! in the Stateright repository.
//!
//! [`always`]: Property::always
//! [discover]: Checker::discoveries
//! [invariant]: https://en.wikipedia.org/wiki/Invariant_(computer_science)
//! [`Model`]: Model
//! [safety property]: https://en.wikipedia.org/wiki/Safety_property
//! [`sometimes`]: Property::sometimes
//! [spawn]: actor::spawn()
#[warn(anonymous_parameters)]
#[warn(missing_docs)]
mod checker;
mod job_market;
pub mod report;
use std::fmt::Debug;
use std::hash::{Hash, Hasher};
#[cfg(test)]
mod test_util;
pub mod actor;
pub use checker::*;
pub mod semantics;
pub mod util;
/// 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`] and [`actor::ActorModel`].
///
/// You can instantiate a model [`CheckerBuilder`] by calling [`Model::checker`].
pub trait Model: Sized {
/// The type of state upon which this model operates.
type State;
/// The type of action that transitions between states.
type Action;
/// Returns the initial possible states.
fn init_states(&self) -> Vec<Self::State>;
/// Collects the subsequent possible actions based on a previous state.
fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>);
/// Converts a previous state and action to a resulting state. [`None`] indicates that the action
/// does not change the state.
fn next_state(&self, last_state: &Self::State, action: Self::Action) -> Option<Self::State>;
/// Converts an action of this model to a more intuitive representation (e.g. for Explorer).
fn format_action(&self, action: &Self::Action) -> String
where
Self::Action: Debug,
{
format!("{:?}", action)
}
/// Converts a step of this model to a more intuitive representation (e.g. for Explorer).
fn format_step(&self, last_state: &Self::State, action: Self::Action) -> Option<String>
where
Self::State: Debug,
{
self.next_state(last_state, action)
.map(|next_state| format!("{:#?}", next_state))
}
/// Returns an [SVG](https://developer.mozilla.org/en-US/docs/Web/SVG) representation of a
/// [`Path`] for this model.
fn as_svg(&self, _path: Path<Self::State, Self::Action>) -> Option<String> {
None
}
/// Indicates the steps (action-state pairs) that follow a particular state.
fn next_steps(&self, last_state: &Self::State) -> Vec<(Self::Action, Self::State)> {
// Must generate the actions twice because they are consumed by `next_state`.
let mut actions1 = Vec::new();
let mut actions2 = Vec::new();
self.actions(last_state, &mut actions1);
self.actions(last_state, &mut actions2);
actions1
.into_iter()
.zip(actions2)
.filter_map(|(action1, action2)| {
self.next_state(last_state, action1)
.map(|state| (action2, state))
})
.collect()
}
/// Indicates the states that follow a particular state. Slightly more efficient than calling
/// [`Model::next_steps`] and projecting out the states.
fn next_states(&self, last_state: &Self::State) -> Vec<Self::State> {
let mut actions = Vec::new();
self.actions(last_state, &mut actions);
actions
.into_iter()
.filter_map(|action| self.next_state(last_state, action))
.collect()
}
/// Generates the expected properties for this model.
fn properties(&self) -> Vec<Property<Self>> {
Vec::new()
}
/// Looks up a property by name. Panics if the property does not exist.
fn property(&self, name: &'static str) -> Property<Self> {
if let Some(p) = self.properties().into_iter().find(|p| p.name == name) {
p
} else {
let available: Vec<_> = self.properties().iter().map(|p| p.name).collect();
panic!(
"Unknown property. requested={}, available={:?}",
name, available
);
}
}
/// Indicates whether a state is within the state space that should be model checked.
fn within_boundary(&self, _state: &Self::State) -> bool {
true
}
/// Instantiates a [`CheckerBuilder`] for this model.
fn checker(self) -> CheckerBuilder<Self>
where
Self: Send + Sync + 'static,
Self::State: Hash + Send + Sync,
{
CheckerBuilder::new(self)
}
}
/// 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).
pub struct Property<M: Model> {
pub expectation: Expectation,
pub name: &'static str,
pub condition: fn(&M, &M::State) -> bool,
}
impl<M: Model> Property<M> {
/// An invariant that defines a [safety
/// property](https://en.wikipedia.org/wiki/Safety_property). The model checker will try to
/// discover a counterexample.
pub fn always(name: &'static str, condition: fn(&M, &M::State) -> bool) -> Property<M> {
Property {
expectation: Expectation::Always,
name,
condition,
}
}
/// An invariant that defines a [liveness
/// property](https://en.wikipedia.org/wiki/Liveness). The model checker will try to
/// discover a counterexample path leading from the initial state through to a
/// terminal state.
///
/// Note that in this implementation `eventually` properties only work correctly on acyclic
/// paths (those that end in either states with no successors or checking boundaries). A path
/// ending in a cycle is not viewed as _terminating_ in that cycle, as the checker does not
/// differentiate cycles from DAG joins, and so an `eventually` property that has not been met
/// by the cycle-closing edge will ignored -- a false negative.
pub fn eventually(name: &'static str, condition: fn(&M, &M::State) -> bool) -> Property<M> {
Property {
expectation: Expectation::Eventually,
name,
condition,
}
}
/// Something that should be possible in the model. The model checker will try to discover an
/// example.
pub fn sometimes(name: &'static str, condition: fn(&M, &M::State) -> bool) -> Property<M> {
Property {
expectation: Expectation::Sometimes,
name,
condition,
}
}
}
impl<M: Model> Clone for Property<M> {
fn clone(&self) -> Self {
Property {
expectation: self.expectation.clone(),
name: self.name,
condition: self.condition,
}
}
}
/// Indicates whether a property is always, eventually, or sometimes true.
#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd, serde::Deserialize, serde::Serialize)]
pub enum Expectation {
/// The property is true for all reachable states.
Always,
/// The property is eventually true for all behavior paths.
Eventually,
/// The property is true for at least one reachable state.
Sometimes,
}
/// A state identifier. See [`fingerprint`].
type Fingerprint = std::num::NonZeroU64;
/// Converts a state to a [`Fingerprint`].
#[inline]
fn fingerprint<T: Hash>(value: &T) -> Fingerprint {
let mut hasher = stable::hasher();
value.hash(&mut hasher);
Fingerprint::new(hasher.finish()).expect("hasher returned zero, an invalid fingerprint")
}
/// Implemented only for rustdoc. Do not take a dependency on this. It will likely be removed in a
/// future version of this library.
#[doc(hidden)]
impl Model for () {
type State = ();
type Action = ();
fn init_states(&self) -> Vec<Self::State> {
vec![()]
}
fn actions(&self, _: &Self::State, actions: &mut Vec<Self::Action>) {
actions.push(())
}
fn next_state(&self, _: &Self::State, _: Self::Action) -> Option<Self::State> {
Some(())
}
}
// Helpers for stable hashing, wherein hashes should not vary across builds.
mod stable {
use std::hash::BuildHasher;
use ahash::{AHasher, RandomState};
const KEY1: u64 = 123_456_789_987_654_321;
const KEY2: u64 = 98_765_432_123_456_789;
// TODO: how to get these?
const KEY3: u64 = 0;
const KEY4: u64 = 0;
pub(crate) fn hasher() -> AHasher {
build_hasher().build_hasher()
}
pub(crate) fn build_hasher() -> RandomState {
RandomState::with_seeds(KEY1, KEY2, KEY3, KEY4)
}
}