WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems
WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems
复制标题
WormSpace：简单、可验证的分布式系统的模块化基础
DOI：
10.1145/3357223.3362739
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Shao, Zhong
中科院分区：
文献类型：
--
作者：
Shin, Ji-Yong;Kim, Jieung;Honoré, Wolf;Vanzetto, Hernán;Radhakrishnan, Srihari;Balakrishnan, Mahesh;Shao, Zhong
我们提出了Write-Once Register （WOR）作为构建和验证分布式系统的抽象。WOR公开了一个简单的、以数据为中心的API：客户机可以捕获、写入和读取它。应用程序可以使用一个序列或一组WORs来获得耐久性、并发控制和故障原子性等属性。通过将分布式协调的逻辑隐藏在以数据为中心的API之下，WOR抽象支持在其之上构建的应用程序的简单、增量和可扩展的实现和验证。我们介绍了一个名为WormSpace的系统的设计、实现和验证，该系统为开发人员提供了一个WOR的地址空间，通过Paxos实例实现每个WOR。我们描述了基于WormSpace构建的三个应用程序：灵活、高效的Multi-Paxos实现；一个共享日志实现，具有比最先进的更低的追加延迟；以及使用最佳往返次数的容错事务协调器。我们展示了这些应用程序简单，易于验证，并且与未经验证的单片实现的性能相匹配。我们使用模块化分层验证方法将WormSpace、其应用程序和经过验证的操作系统的证明链接起来，从而产生从应用程序到操作系统的第一个经过验证的分布式系统堆栈。
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.
登录
查看更多内容
DOI：
--
发表时间：
2003
期刊：
--
影响因子：
--
作者：
R. Boichat;P. Dutta;Svend Frølund;R. Guerraoui
通讯作者：
R. Boichat;P. Dutta;Svend Frølund;R. Guerraoui
通过崩溃优化对文件系统进行一键式验证
DOI：
--
发表时间：
2016
期刊：
USENIX Annual Technical Conference
影响因子：
--
作者：
Helgi Sigurbjarnarson;James Bornholt;Nicolas Christin;L. Cranor
通讯作者：
L. Cranor
数字对象标识符 (DOI) 10.1007/s00446-002-0070-8 c ○ Springer-Verlag 2003 Disk Paxos
DOI：
--
发表时间：
2001
期刊：
影响因子：
--
作者：
Steven L. Alter
通讯作者：
Steven L. Alter
DOI：
--
发表时间：
1990
期刊：
Fault-Tolerant Distributed Computing
影响因子：
--
作者：
V. Hadzilacos
通讯作者：
V. Hadzilacos
影响因子：
--
作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock
通讯作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock