IronFleet
| Autor: | Michael L. Roberts, Manos Kapritsos, Bryan Parno, Chris Hawblitzel, Srinath Setty, Jon Howell, Jacob R. Lorch, Brian Zill |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
General Computer Science
State machine replication Paxos Computer science 020204 information systems Distributed computing Scale (chemistry) Liveness 0202 electrical engineering electronic engineering information engineering 020206 networking & telecommunications Temporal logic 02 engineering and technology |
| Zdroj: | Communications of the ACM. 60:83-92 |
| ISSN: | 1557-7317 0001-0782 |
| DOI: | 10.1145/3068608 |
| Popis: | Distributed systems are notorious for harboring subtle bugs. Verification can, in principle, eliminate these bugs, but it has historically been difficult to apply at full-program scale, much less distributed system scale. We describe a methodology for building practical and provably correct distributed systems based on a unique blend of temporal logic of actions-style state-machine refinement and Hoare-logic verification. We demonstrate the methodology on a complex implementation of a Paxos-based replicated state machine library and a lease-based sharded key-value store. We prove that each obeys a concise safety specification as well as desirable liveness requirements. Each implementation achieves performance competitive with a reference system. With our methodology and lessons learned, we aim to raise the standard for distributed systems from "tested" to "correct." |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|