The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems

Last modified: Fri Sep 20 22:26:04 2019 GMT.

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. Applica- tions 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 (to appear), November 2019.
  • Conference Paper [PDF]

  • Copyright © 1996-2019 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon