Title: Model Checking Distributed Systems using TraceForge

Abstract:

In this tutorial, we will describe stateless model checking, a way to systematically explore the space of interleavings of a concurrent or distributed program. We will use TraceForge, a stateless model checker for Rust programs, as a specific example. We will describe the key data structures and algorithms, such as execution graphs, partial-order reduction, and inbox semantics, that allows TraceForge to scale to large Rust implementations. We will also describe the current research questions in this field. In the hands-on portion, we will ask participants to write small distributed protocols using TraceForge’s API and get experience with stateless model checking.