IronFleet: Proving Safety and Liveness of Practical Distributed Systems.
Saved in:
| Title: | IronFleet: Proving Safety and Liveness of Practical Distributed Systems. |
|---|---|
| Authors: | Hawblitzel, Chris chrishaw@microsoft.com, Howell, Jon jonh@jonh.net, Kapritsos, Manos emkaprit@microsoft.com, Lorch, Jacob R. lorch@microsoft.com, Parno, Bryan parno@microsoft.com, Roberts, Michael L. mirobert@microsoft.com, Setty, Srinath srinath@microsoft.com, Zill, Brian bzill@microsoft.com |
| Source: | Communications of the ACM. Jul2017, Vol. 60 Issue 7, p83-92. 10p. 2 Diagrams, 7 Charts, 2 Graphs. |
| Subjects: | Distributed computing software, Systems software, Computer software, Finite state machines, Technical specifications, Standards, Paxos (Computer science) |
| Abstract: | 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". [ABSTRACT FROM AUTHOR] |
| Copyright of Communications of the ACM is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 123967782 AccessLevel: 6 PubType: Periodical PubTypeId: serialPeriodical PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: IronFleet: Proving Safety and Liveness of Practical Distributed Systems. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Hawblitzel%2C+Chris%22">Hawblitzel, Chris</searchLink><i> chrishaw@microsoft.com</i><br /><searchLink fieldCode="AR" term="%22Howell%2C+Jon%22">Howell, Jon</searchLink><i> jonh@jonh.net</i><br /><searchLink fieldCode="AR" term="%22Kapritsos%2C+Manos%22">Kapritsos, Manos</searchLink><i> emkaprit@microsoft.com</i><br /><searchLink fieldCode="AR" term="%22Lorch%2C+Jacob+R%2E%22">Lorch, Jacob R.</searchLink><i> lorch@microsoft.com</i><br /><searchLink fieldCode="AR" term="%22Parno%2C+Bryan%22">Parno, Bryan</searchLink><i> parno@microsoft.com</i><br /><searchLink fieldCode="AR" term="%22Roberts%2C+Michael+L%2E%22">Roberts, Michael L.</searchLink><i> mirobert@microsoft.com</i><br /><searchLink fieldCode="AR" term="%22Setty%2C+Srinath%22">Setty, Srinath</searchLink><i> srinath@microsoft.com</i><br /><searchLink fieldCode="AR" term="%22Zill%2C+Brian%22">Zill, Brian</searchLink><i> bzill@microsoft.com</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Communications+of+the+ACM%22">Communications of the ACM</searchLink>. Jul2017, Vol. 60 Issue 7, p83-92. 10p. 2 Diagrams, 7 Charts, 2 Graphs. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Distributed+computing+software%22">Distributed computing software</searchLink><br /><searchLink fieldCode="DE" term="%22Systems+software%22">Systems software</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software%22">Computer software</searchLink><br /><searchLink fieldCode="DE" term="%22Finite+state+machines%22">Finite state machines</searchLink><br /><searchLink fieldCode="DE" term="%22Technical+specifications%22">Technical specifications</searchLink><br /><searchLink fieldCode="DE" term="%22Standards%22">Standards</searchLink><br /><searchLink fieldCode="DE" term="%22Paxos+%28Computer+science%29%22">Paxos (Computer science)</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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". [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Communications of the ACM is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=123967782 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1145/3068608 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 10 StartPage: 83 Subjects: – SubjectFull: Distributed computing software Type: general – SubjectFull: Systems software Type: general – SubjectFull: Computer software Type: general – SubjectFull: Finite state machines Type: general – SubjectFull: Technical specifications Type: general – SubjectFull: Standards Type: general – SubjectFull: Paxos (Computer science) Type: general Titles: – TitleFull: IronFleet: Proving Safety and Liveness of Practical Distributed Systems. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Hawblitzel, Chris – PersonEntity: Name: NameFull: Howell, Jon – PersonEntity: Name: NameFull: Kapritsos, Manos – PersonEntity: Name: NameFull: Lorch, Jacob R. – PersonEntity: Name: NameFull: Parno, Bryan – PersonEntity: Name: NameFull: Roberts, Michael L. – PersonEntity: Name: NameFull: Setty, Srinath – PersonEntity: Name: NameFull: Zill, Brian IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 07 Text: Jul2017 Type: published Y: 2017 Identifiers: – Type: issn-print Value: 00010782 Numbering: – Type: volume Value: 60 – Type: issue Value: 7 Titles: – TitleFull: Communications of the ACM Type: main |
| ResultId | 1 |
