Verifying a high-performance distributed transaction system using permissioned state machines
TL;DR
The permissioned state machine (PSM) approach, which extends TLA-style protocol reasoning with ideas from concurrent separation logic, enables the developer to specify and verify complex protocols, such as Tulip, by breaking them down into smaller modules.
Abstract
Tulip is a high-performance distributed transaction system that uses sharding for scalability, replication within each shard for fault tolerance, and TAPIR-style inconsistent replication for high performance. Tulip comes with a machine-checked proof of correctness showing that its implementation meets a simple specification identical to a local strictly serializable transaction system, abstracting away implementation details such as crash recovery, multi-versioning, replication, sharding, and coordinator recovery. The contribution of this paper is the permissioned state machine (PSM) approach, which extends TLA-style protocol reasoning with ideas from concurrent separation logic. PSM enables the developer to specify and verify complex protocols, such as Tulip, by breaking them down into smaller modules. PSM makes all dependencies between modules explicit using permissions, which limits the ways these modules can interact, and thereby reduces proof effort. The prototype of Tulip consists of 3,956 lines of Go code, achieving performance competitive with that of TAPIR. Tulip's proof is decomposed into 10 types of modules; the majority of logical proof steps (“actions”) involve just one module, demonstrating that PSM enables local reasoning.