Wilcox, JR;
Sergey, I;
Tatlock, Z;
(2017)
Programming Language Abstractions for Modularly Verified Distributed Systems.
In: Lerner, BS and Bodik, R and Krishnamu, S, (eds.)
Proceedings of the 2nd Summit on Advances in Programming Languages (SNAPL 2017).
(pp. 19:1-19:12).
Schloss Dagstuhl: Dagstuhl, Germany.
Preview |
Text
LIPIcs-SNAPL-2017-19.pdf - Published Version Download (584kB) | Preview |
Abstract
Distributed systems are rarely developed as monolithic programs. Instead, like any software, these systems may consist of multiple program components, which are then compiled separately and linked together. Modern systems also incorporate various services interacting with each other and with client applications. However, state-of-the-art verification tools focus predominantly on verifying standalone, closed-world protocols or systems, thus failing to account for the compositional nature of distributed systems. For example, standalone verification has the drawback that when protocols and their optimized implementations evolve, one must re-verify the entire system from scratch, instead of leveraging compositionality to contain the reverification effort. In this paper, we focus on the challenge of modular verification of distributed systems with respect to high-level protocol invariants as well as for low-level implementation safety properties. We argue that the missing link between the two is a programming paradigm that would allow one to reason about both high-level distributed protocols and low-level implementation primitives in a single verification-friendly framework. Such a link would make it possible to reap the benefits from both the vast body of research in distributed computing, focused on modular protocol decomposition and consistency properties, as well as from the recent advances in program verification, enabling construction of provably correct systems implementations. To showcase the modular verification challenges, we present some typical scenarios of decomposition between a distributed protocol and its implementations. We then describe our ongoing research agenda, in which we are attempting to address the outlined problems by providing a typing discipline and a set of domain-specific primitives for specifying, implementing and verifying distributed systems. Our approach, mechanized within a proof assistant, provides the means of decomposition necessary for modular proofs about distributed protocols and systems.
| Type: | Proceedings paper |
|---|---|
| Title: | Programming Language Abstractions for Modularly Verified Distributed Systems |
| Event: | 2nd Summit on Advances in Programming Languages (SNAPL 2017) |
| Location: | Asilomar, CA, USA |
| Dates: | 07 May 2017 - 10 May 2017 |
| ISBN-13: | 978-3-95977-032-3 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.4230/LIPIcs.SNAPL.2017.19 |
| Publisher version: | http://doi.org/10.4230/LIPIcs.SNAPL.2017.19 |
| Language: | English |
| Additional information: | Copyright © James R. Wilcox, Ilya Sergey, and Zachary Tatlock; licensed under Creative Commons License CC-BY 2nd Summit on Advances in Programming Languages (SNAPL 2017). Editors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi; Article No. 19; pp. 19:1–19:12 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany |
| Keywords: | Distributed systems, program verification, distributed protocols, domainspecific languages, type systems, dependent types, program logics |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10030725 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
