IronFleet: Proving Safety and Liveness of Practical Distributed Systems.
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 distribu...
| Publicado en: | Communications of the ACM Vol. 60; no. 7; pp. 83 - 93 |
|---|---|
| Autores principales: | , , , , , , , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Jul2017
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=123967782&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 123967782 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Jul2017 vid: 60 iid: 7 pid: 68 pub: Association for Computing Machinery artinfo: ui: 123967782 10.1145/3068608 ppf: 83 ppct: 10 formats: tig: atl: IronFleet: Proving Safety and Liveness of Practical Distributed Systems. aug: au: Hawblitzel, Chris Howell, Jon Kapritsos, Manos Lorch, Jacob R. Parno, Bryan Roberts, Michael L. Setty, Srinath Zill, Brian su: Distributed computing software Systems software Computer software Finite state machines Technical specifications Standards Paxos (Computer science) sug: subj: Distributed computing software Systems software Computer software Finite state machines Technical specifications Standards Paxos (Computer science) ab: 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". pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2017 holdings: @attributes: islocal: N |
|---|