Building Distributed Systems With Stateright

Stateright is a model checker for distributed systems. It is provided as a Rust library, and it allows you to verify systems implemented in Rust. It is openly available on GitHub and the developer, Jon Nadal, is looking for contributors and new users.  

On Tuesday Jon gave a presentation to us on Zoom. He made his presentation slides available here. We have also recorded Jon's presentation and the Q&A and demo sessions in entirety.

  

The highlights of Stateright are:



The model trait has state, init_states, actions, next_state, and properties.


Similarly there is an actor trait you can implement, and model check as follows.

The Rust book for Stateright gives examples of model checking ABD protocol in Rust and the chapter on Paxos protocol is coming soon. 

To improve the performance of model checking, the checker fingerprints states and digests states into 64 bit integers. Rust is also a fast language because it does not do much pointer hopping. Jon said he will try to implement dynamic partial order reduction to improve the performance of model checking further. The model checker is already parallel, but running on many machines in a distributed fashion can also be added.

Comments

Popular posts from this blog

Hints for Distributed Systems Design

Learning about distributed systems: where to start?

Making database systems usable

Looming Liability Machines (LLMs)

Foundational distributed systems papers

Advice to the young

Linearizability: A Correctness Condition for Concurrent Objects

Scalable OLTP in the Cloud: What’s the BIG DEAL?

Understanding the Performance Implications of Storage-Disaggregated Databases

Designing Data Intensive Applications (DDIA) Book