42 releases (23 breaking)
|0.30.1||Aug 27, 2023|
|0.30.0||May 28, 2023|
|0.29.0||Mar 19, 2022|
|0.28.0||May 22, 2021|
#43 in Concurrency
240 downloads per month
Used in concorde
Correctly implementing distributed algorithms such as the Paxos and Raft consensus protocols is notoriously difficult due to inherent nondetermism such as message reordering by network devices. Stateright is a Rust actor library that aims to solve this problem by providing an embedded model checker, a UI for exploring system behavior (demo), and a lightweight actor runtime. It also features a linearizability tester that can be run within the model checker for more exhaustive test coverage than similar solutions such as Jepsen.
- Please see the book, "Building Distributed Systems With Stateright."
- A video introduction is also available.
- Stateright also has detailed API docs.
- Consider also joining the Stateright Discord server for Q&A or other feedback.
check CLI argument causes each example to validate itself using
Stateright's model checker:
# Two phase commit with 3 resource managers. cargo run --release --example 2pc check 3 # Paxos cluster with 3 clients. cargo run --release --example paxos check 3 # Single-copy (unreplicated) register with 3 clients. cargo run --release --example single-copy-register check 3 # Linearizable distributed register (ABD algorithm) with 2 clients # assuming ordered channels between actors. cargo run --release --example linearizable-register check 2 ordered
explore CLI argument causes each example to spin up the Stateright
Explorer web UI locally on port 3000, allowing you to browse system behaviors:
cargo run --release --example 2pc explore cargo run --release --example paxos explore cargo run --release --example single-copy-register explore cargo run --release --example linearizable-register explore
spawn CLI argument to the examples leveraging the actor
functionality will cause each to spawn actors using the included runtime,
transmitting JSON messages over UDP:
cargo run --release --example paxos spawn cargo run --release --example single-copy-register spawn cargo run --release --example linearizable-register spawn
bench.sh script runs all the examples with various settings for
benchmarking the performance impact of changes to the library.
Stateright contains a general purpose model checker offering:
- Invariant checks via "always" properties.
- Nontriviality checks via "sometimes" properties.
- Liveness checks via "eventually" properties (experimental/incomplete).
- A web browser UI for interactively exploring state space.
- Linearizability and sequential consistency testers.
- Support for symmetry reduction to reduce state spaces.
Stateright's actor system features include:
- An actor runtime that can execute actors outside the model checker in the "real world."
- A model for lossy/lossless duplicating/non-duplicating networks with the ability to capture actor message history to check an actor system against an expected consistency model.
- Pluggable network semantics for model checking, allowing you to choose between fewer assumptions (e.g. "lossy unordered duplicating") or more assumptions (speeding up model checking; e.g. "lossless ordered").
- An optional network adapter that provides a lossless non-duplicating ordered virtual channel for messages between a pair of actors.
In contrast with other actor libraries, Stateright enables you to formally verify the correctness of your implementation, and in contrast with model checkers such as TLC for TLA+, systems implemented using Stateright can also be run on a real network without being reimplemented in a different language.
Contributions are welcome! Please fork the library, push changes to your fork, and send a pull request. All contributions are shared under an MIT license unless explicitly stated otherwise in the pull request.
Stateright is copyright 2018 Jonathan Nadal and other contributors. It is made available under the MIT License.
- KnockoutJS is copyright 2010 Steven Sanderson, the Knockout.js team, and other contributors. It is made available under the MIT License.