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. # (please be patient with this one, as it takes longer to check) cargo run --release --example linearizable-register check 2
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
Stateright contains a general purpose model checker offering:
- Invariant checks via "always" properties.
- Nontriviality checks via "sometimes" properties.
- Liveness checks via "eventually" properties.
- A web browser UI for interactively exploring state space.
- Linearizability and sequential consistency testers.
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.
- 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.