oraclewalid/stateright

A model checker for implementing distributed systems.

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.

Getting Started

1. Please see the book, "Building Distributed Systems With Stateright."
2. A video introduction is also available.
3. Stateright also has detailed API docs.
4. Consider also joining the Stateright Discord server for Q&A or other feedback.

Examples

Stateright includes a variety of examples, such as a Single Decree Paxos cluster and an abstract two phase commit model.

Passing a 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

Passing an 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

Passing a 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

Features

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.

Contribution

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.

License

Stateright is copyright 2018 Jonathan Nadal and other contributors. It is made available under the MIT License.

To avoid the need for a Javascript package manager, the Stateright repository includes code for the following Javascript dependency used by Stateright Explorer:

• KnockoutJS is copyright 2010 Steven Sanderson, the Knockout.js team, and other contributors. It is made available under the MIT License.