Authors
Ji-Yong Shin
Jieung Kim
Wolf Honore
Hernán Vanzetto
Srihari Radhakrishnan
Mahesh Balakrishnan
Zhong Shao
Abstract
We propose the Write-Once Register (WOR) as an abstraction for
building and verifying distributed systems. A WOR exposes a simple,
data-centric API: clients can capture, write, and read it. Applications
can use a sequence or a set of WORs to obtain properties such as
durability, concurrency control, and failure atomicity. By hiding the
logic for distributed coordination underneath a data-centric API, the
WOR abstraction enables easy, incremental, and extensible
implementation and verification of applications built above it. We
present the design, implementation, and verification of a system called
WormSpace that provides developers with an address space of WORs,
implementing each WOR via a Paxos instance. We describe three
applications built over WormSpace: a flexible, efficient Multi-Paxos
implementation; a shared log implementation with lower append latency
than the state-of-the-art; and a fault-tolerant transaction
coordinator that uses an optimal number of round-trips. We show that
these applications are simple, easy to verify, and match the
performance of unverified monolithic implementations. We use a
modular layered verification approach to link the proofs for WormSpace,
its applications, and a verified operating system to produce the first
verified distributed system stack from the application to the operating
system.
Published
In
Proc. 2019 ACM Symposium on Cloud Computing (SOCC'19),
Santa Cruz, California. Pages 299-311, November 2019.