Volume
LIPIcs, Volume 136
3rd Summit on Advances in Programming Languages (SNAPL 2019)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Summit on Advances in Programming Languages (SNAPL)
Event
SNAPL 2019, May 16-17, 2019, Providence, RI, USAEditors
Publication Details
- published at: 2019-07-11
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-113-9
- DBLP: db/conf/snapl/snapl2019
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 136, SNAPL'19, Complete Volume
Abstract
LIPIcs, Volume 136, SNAPL'19, Complete Volume
Cite as
3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Proceedings{lerner_et_al:LIPIcs.SNAPL.2019,
title = {{LIPIcs, Volume 136, SNAPL'19, Complete Volume}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019},
URN = {urn:nbn:de:0030-drops-108657},
doi = {10.4230/LIPIcs.SNAPL.2019},
annote = {Keywords: Software and its engineering, General programming languages, Semantics}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{lerner_et_al:LIPIcs.SNAPL.2019.0,
author = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {0:i--0:viii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.0},
URN = {urn:nbn:de:0030-drops-105439},
doi = {10.4230/LIPIcs.SNAPL.2019.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Overparameterization: A Connection Between Software 1.0 and Software 2.0
Abstract
A new ecosystem of machine-learning driven applications, titled Software 2.0, has arisen that integrates neural networks into a variety of computational tasks. Such applications include image recognition, natural language processing, and other traditional machine learning tasks. However, these techniques have also grown to include other structured domains, such as program analysis and program optimization for which novel, domain-specific insights mate with model design. In this paper, we connect the world of Software 2.0 with that of traditional software - Software 1.0 - through overparameterization: a program may provide more computational capacity and precision than is necessary for the task at hand.
In Software 2.0, overparamterization - when a machine learning model has more parameters than datapoints in the dataset - arises as a contemporary understanding of the ability for modern, gradient-based learning methods to learn models over complex datasets with high-accuracy. Specifically, the more parameters a model has, the better it learns.
In Software 1.0, the results of the approximate computing community show that traditional software is also overparameterized in that software often simply computes results that are more precise than is required by the user. Approximate computing exploits this overparameterization to improve performance by eliminating unnecessary, excess computation. For example, one - of many techniques - is to reduce the precision of arithmetic in the application.
In this paper, we argue that the gap between available precision and that that is required for either Software 1.0 or Software 2.0 is a fundamental aspect of software design that illustrates the balance between software designed for general-purposes and domain-adapted solutions. A general-purpose solution is easier to develop and maintain versus a domain-adapted solution. However, that ease comes at the expense of performance.
We show that the approximate computing community and the machine learning community have developed overlapping techniques to improve performance by reducing overparameterization. We also show that because of these shared techniques, questions, concerns, and answers on how to construct software can translate from one software variant to the other.
Cite as
Michael Carbin. Overparameterization: A Connection Between Software 1.0 and Software 2.0. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 1:1-1:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{carbin:LIPIcs.SNAPL.2019.1,
author = {Carbin, Michael},
title = {{Overparameterization: A Connection Between Software 1.0 and Software 2.0}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {1:1--1:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.1},
URN = {urn:nbn:de:0030-drops-105440},
doi = {10.4230/LIPIcs.SNAPL.2019.1},
annote = {Keywords: Approximate Computing, Machine Learning, Software 2.0}
}
Document
Blame Tracking and Type Error Debugging
Abstract
In this work, we present an unexpected connection between gradual typing and type error debugging. Namely, we illustrate that gradual typing provides a natural way to defer type errors in statically ill-typed programs, providing more feedback than traditional approaches to deferring type errors. When evaluating expressions that lead to runtime type errors, the usefulness of the feedback depends on blame tracking, the defacto approach to locating the cause of such runtime type errors. Unfortunately, blame tracking suffers from the bias problem for type error localization in languages with type inference. We illustrate and formalize the bias problem for blame tracking, present ideas for adapting existing type error debugging techniques to combat this bias, and outline further challenges.
Cite as
Sheng Chen and John Peter Campora III. Blame Tracking and Type Error Debugging. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.SNAPL.2019.2,
author = {Chen, Sheng and Campora III, John Peter},
title = {{Blame Tracking and Type Error Debugging}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {2:1--2:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.2},
URN = {urn:nbn:de:0030-drops-105451},
doi = {10.4230/LIPIcs.SNAPL.2019.2},
annote = {Keywords: Blame tracking, type error debugging, gradual typing, type inference}
}
Document
What is a Secure Programming Language?
Abstract
Our most sensitive and important software systems are written in programming languages that are inherently insecure, making the security of the systems themselves extremely challenging. It is often said that these systems were written with the best tools available at the time, so over time with newer languages will come more security. But we contend that all of today’s mainstream programming languages are insecure, including even the most recent ones that come with claims that they are designed to be "secure". Our real criticism is the lack of a common understanding of what "secure" might mean in the context of programming language design. We propose a simple data-driven definition for a secure programming language: that it provides first-class language support to address the causes for the most common, significant vulnerabilities found in real-world software. To discover what these vulnerabilities actually are, we have analysed the National Vulnerability Database and devised a novel categorisation of the software defects reported in the database. This leads us to propose three broad categories, which account for over 50% of all reported software vulnerabilities, that as a minimum any secure language should address. While most mainstream languages address at least one of these categories, interestingly, we find that none address all three.
Looking at today’s real-world software systems, we observe a paradigm shift in design and implementation towards service-oriented architectures, such as microservices. Such systems consist of many fine-grained processes, typically implemented in multiple languages, that communicate over the network using simple web-based protocols, often relying on multiple software environments such as databases. In traditional software systems, these features are the most common locations for security vulnerabilities, and so are often kept internal to the system. In microservice systems, these features are no longer internal but external, and now represent the attack surface of the software system as a whole. The need for secure programming languages is probably greater now than it has ever been.
Cite as
Cristina Cifuentes and Gavin Bierman. What is a Secure Programming Language?. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{cifuentes_et_al:LIPIcs.SNAPL.2019.3,
author = {Cifuentes, Cristina and Bierman, Gavin},
title = {{What is a Secure Programming Language?}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {3:1--3:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.3},
URN = {urn:nbn:de:0030-drops-105466},
doi = {10.4230/LIPIcs.SNAPL.2019.3},
annote = {Keywords: memory safety, confidentiality, integrity}
}
Document
From Theory to Systems: A Grounded Approach to Programming Language Education
Abstract
I present a new approach to teaching a graduate-level programming languages course focused on using systems programming ideas and languages like WebAssembly and Rust to motivate PL theory. Drawing on students' prior experience with low-level languages, the course shows how type systems and PL theory are used to avoid tricky real-world errors that students encounter in practice. I reflect on the curricular design and lessons learned from two years of teaching at Stanford, showing that integrating systems ideas can provide students a more grounded and enjoyable education in programming languages. The curriculum, course notes, and assignments are freely available: http://cs242.stanford.edu/f18/
Cite as
Will Crichton. From Theory to Systems: A Grounded Approach to Programming Language Education. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 4:1-4:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{crichton:LIPIcs.SNAPL.2019.4,
author = {Crichton, Will},
title = {{From Theory to Systems: A Grounded Approach to Programming Language Education}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {4:1--4:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.4},
URN = {urn:nbn:de:0030-drops-105472},
doi = {10.4230/LIPIcs.SNAPL.2019.4},
annote = {Keywords: programming languages, programming language education}
}
Document
From Macros to DSLs: The Evolution of Racket
Abstract
The Racket language promotes a language-oriented style of programming. Developers create many domain-specific languages, write programs in them, and compose these programs via Racket code. This style of programming can work only if creating and composing little languages is simple and effective. While Racket’s Lisp heritage might suggest that macros suffice, its design team discovered significant shortcomings and had to improve them in many ways. This paper presents the evolution of Racket’s macro system, including a false start, and assesses its current state.
Cite as
Ryan Culpepper, Matthias Felleisen, Matthew Flatt, and Shriram Krishnamurthi. From Macros to DSLs: The Evolution of Racket. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{culpepper_et_al:LIPIcs.SNAPL.2019.5,
author = {Culpepper, Ryan and Felleisen, Matthias and Flatt, Matthew and Krishnamurthi, Shriram},
title = {{From Macros to DSLs: The Evolution of Racket}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {5:1--5:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.5},
URN = {urn:nbn:de:0030-drops-105482},
doi = {10.4230/LIPIcs.SNAPL.2019.5},
annote = {Keywords: design principles, macros systems, domain-specific languages}
}
Document
The Dynamic Practice and Static Theory of Gradual Typing
Abstract
We can tease apart the research on gradual types into two `lineages': a pragmatic, implementation-oriented dynamic-first lineage and a formal, type-theoretic, static-first lineage. The dynamic-first lineage’s focus is on taming particular idioms - `pre-existing conditions' in untyped programming languages. The static-first lineage’s focus is on interoperation and individual type system features, rather than the collection of features found in any particular language. Both appear in programming languages research under the name "gradual typing", and they are in active conversation with each other.
What are these two lineages? What challenges and opportunities await the static-first lineage? What progress has been made so far?
Cite as
Michael Greenberg. The Dynamic Practice and Static Theory of Gradual Typing. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{greenberg:LIPIcs.SNAPL.2019.6,
author = {Greenberg, Michael},
title = {{The Dynamic Practice and Static Theory of Gradual Typing}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {6:1--6:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.6},
URN = {urn:nbn:de:0030-drops-105495},
doi = {10.4230/LIPIcs.SNAPL.2019.6},
annote = {Keywords: dynamic typing, gradual typing, static typing, implementation, theory, challenge problems}
}
Document
A Golden Age of Hardware Description Languages: Applying Programming Language Techniques to Improve Design Productivity
Abstract
Leading experts have declared that there is an impending golden age of computer architecture. During this age, the rate at which architects will be able to innovate will be directly tied to the design and implementation of the hardware description languages they use. Thus, the programming languages community stands on the critical path to this new golden age. This implies that we are also on the cusp of a golden age of hardware description languages. In this paper, we discuss the intellectual challenges facing researchers interested in hardware description language design, compilers, and formal methods. The major theme will be identifying opportunities to apply programming language techniques to address issues in hardware design productivity. Then, we present a vision for a multi-language system that provides a framework for developing solutions to these intellectual problems. This vision is based on a meta-programmed host language combined with a core embedded hardware description language that is used as the basis for the research and development of a sea of domain-specific languages. Central to the design of this system is the core language which is based on an abstraction that provides a general mechanism for the composition of hardware components described in any language.
Cite as
Lenny Truong and Pat Hanrahan. A Golden Age of Hardware Description Languages: Applying Programming Language Techniques to Improve Design Productivity. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{truong_et_al:LIPIcs.SNAPL.2019.7,
author = {Truong, Lenny and Hanrahan, Pat},
title = {{A Golden Age of Hardware Description Languages: Applying Programming Language Techniques to Improve Design Productivity}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {7:1--7:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.7},
URN = {urn:nbn:de:0030-drops-105508},
doi = {10.4230/LIPIcs.SNAPL.2019.7},
annote = {Keywords: Hardware Description Languages}
}
Document
Version Control Is for Your Data Too
Abstract
Programmers regularly use distributed version control systems (DVCS) such as Git to facilitate collaborative software development. The primary purpose of a DVCS is to maintain integrity of source code in the presence of concurrent, possibly conflicting edits from collaborators. In addition to safely merging concurrent non-conflicting edits, a DVCS extensively tracks source code provenance to help programmers contextualize and resolve conflicts. Provenance also facilitates debugging by letting programmers see diffs between versions and quickly find those edits that introduced the offending conflict (e.g., via git blame).
In this paper, we posit that analogous workflows to collaborative software development also arise in distributed software execution; we argue that the characteristics that make a DVCS an ideal fit for the former also make it an ideal fit for the latter. Building on this observation, we propose a distributed programming model, called carmot that views distributed shared state as an entity evolving in time, manifested as a sequence of persistent versions, and relies on an explicitly defined merge semantics to reconcile concurrent conflicting versions. We show examples demonstrating how carmot simplifies distributed programming, while also enabling novel workflows integral to modern applications such as blockchains. We also describe a prototype implementation of carmot that we use to evaluate its practicality.
Cite as
Gowtham Kaki, KC Sivaramakrishnan, and Suresh Jagannathan. Version Control Is for Your Data Too. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{kaki_et_al:LIPIcs.SNAPL.2019.8,
author = {Kaki, Gowtham and Sivaramakrishnan, KC and Jagannathan, Suresh},
title = {{Version Control Is for Your Data Too}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.8},
URN = {urn:nbn:de:0030-drops-105516},
doi = {10.4230/LIPIcs.SNAPL.2019.8},
annote = {Keywords: replication, distributed systems, version control}
}
Document
The Next 700 Semantics: A Research Challenge
Abstract
Modern systems consist of large numbers of languages, frameworks, libraries, APIs, and more. Each has characteristic behavior and data. Capturing these in semantics is valuable not only for understanding them but also essential for formal treatment (such as proofs). Unfortunately, most of these systems are defined primarily through implementations, which means the semantics needs to be learned. We describe the problem of learning a semantics, provide a structuring process that is of potential value, and also outline our failed attempts at achieving this so far.
Cite as
Shriram Krishnamurthi, Benjamin S. Lerner, and Liam Elberty. The Next 700 Semantics: A Research Challenge. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{krishnamurthi_et_al:LIPIcs.SNAPL.2019.9,
author = {Krishnamurthi, Shriram and Lerner, Benjamin S. and Elberty, Liam},
title = {{The Next 700 Semantics: A Research Challenge}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {9:1--9:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.9},
URN = {urn:nbn:de:0030-drops-105522},
doi = {10.4230/LIPIcs.SNAPL.2019.9},
annote = {Keywords: Programming languages, desugaring, semantics, testing}
}
Document
Toward Domain-Specific Solvers for Distributed Consistency
Abstract
To guard against machine failures, modern internet services store multiple replicas of the same application data within and across data centers, which introduces the problem of keeping geo-distributed replicas consistent with one another in the face of network partitions and unpredictable message latency. To avoid costly and conservative synchronization protocols, many real-world systems provide only weak consistency guarantees (e.g., eventual, causal, or PRAM consistency), which permit certain kinds of disagreement among replicas.
There has been much recent interest in language support for specifying and verifying such consistency properties. Although these properties are usually beyond the scope of what traditional type checkers or compiler analyses can guarantee, solver-aided languages are up to the task. Inspired by systems like Liquid Haskell [Vazou et al., 2014] and Rosette [Torlak and Bodik, 2014], we believe that close integration between a language and a solver is the right path to consistent-by-construction distributed applications. Unfortunately, verifying distributed consistency properties requires reasoning about transitive relations (e.g., causality or happens-before), partial orders (e.g., the lattice of replica states under a convergent merge operation), and properties relevant to message processing or API invocation (e.g., commutativity and idempotence) that cannot be easily or efficiently carried out by general-purpose SMT solvers that lack native support for this kind of reasoning.
We argue that domain-specific SMT-based tools that exploit the mathematical foundations of distributed consistency would enable both more efficient verification and improved ease of use for domain experts. The principle of exploiting domain knowledge for efficiency and expressivity that has borne fruit elsewhere - such as in the development of high-performance domain-specific languages that trade off generality to gain both performance and productivity - also applies here. Languages augmented with domain-specific, consistency-aware solvers would support the rapid implementation of formally verified programming abstractions that guarantee distributed consistency. In the long run, we aim to democratize the development of such domain-specific solvers by creating a framework for domain-specific solver development that brings new theory solver implementation within the reach of programmers who are not necessarily SMT solver internals experts.
Cite as
Lindsey Kuper and Peter Alvaro. Toward Domain-Specific Solvers for Distributed Consistency. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{kuper_et_al:LIPIcs.SNAPL.2019.10,
author = {Kuper, Lindsey and Alvaro, Peter},
title = {{Toward Domain-Specific Solvers for Distributed Consistency}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {10:1--10:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.10},
URN = {urn:nbn:de:0030-drops-105530},
doi = {10.4230/LIPIcs.SNAPL.2019.10},
annote = {Keywords: distributed consistency, SMT solving, theory solvers}
}
Document
A Tour of Gallifrey, a Language for Geodistributed Programming
Abstract
Programming efficient distributed, concurrent systems requires new abstractions that go beyond traditional sequential programming. But programmers already have trouble getting sequential code right, so simplicity is essential. The core problem is that low-latency, high-availability access to data requires replication of mutable state. Keeping replicas fully consistent is expensive, so the question is how to expose asynchronously replicated objects to programmers in a way that allows them to reason simply about their code. We propose an answer to this question in our ongoing work designing a new language, Gallifrey, which provides orthogonal replication through _restrictions_ with _merge strategies_, _contingencies_ for conflicts arising from concurrency, and _branches_, a novel concurrency control construct inspired by version control, to contain provisional behavior.
Cite as
Mae Milano, Rolph Recto, Tom Magrino, and Andrew C. Myers. A Tour of Gallifrey, a Language for Geodistributed Programming. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{milano_et_al:LIPIcs.SNAPL.2019.11,
author = {Milano, Mae and Recto, Rolph and Magrino, Tom and Myers, Andrew C.},
title = {{A Tour of Gallifrey, a Language for Geodistributed Programming}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.11},
URN = {urn:nbn:de:0030-drops-105549},
doi = {10.4230/LIPIcs.SNAPL.2019.11},
annote = {Keywords: programming languages, distributed systems, weak consistency, linear types}
}
Document
Formal Verification vs. Quantum Uncertainty
Abstract
Quantum programming is hard: Quantum programs are necessarily probabilistic and impossible to examine without disrupting the execution of a program. In response to this challenge, we and a number of other researchers have written tools to verify quantum programs against their intended semantics. This is not enough. Verifying an idealized semantics against a real world quantum program doesn't allow you to confidently predict the program’s output. In order to have verification that works, you need both an error semantics related to the hardware at hand (this is necessarily low level) and certified compilation to the that same hardware. Once we have these two things, we can talk about an approach to quantum programming where we start by writing and verifying programs at a high level, attempt to verify properties of the compiled code, and repeat as necessary.
Cite as
Robert Rand, Kesha Hietala, and Michael Hicks. Formal Verification vs. Quantum Uncertainty. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 12:1-12:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{rand_et_al:LIPIcs.SNAPL.2019.12,
author = {Rand, Robert and Hietala, Kesha and Hicks, Michael},
title = {{Formal Verification vs. Quantum Uncertainty}},
booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)},
pages = {12:1--12:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-113-9},
ISSN = {1868-8969},
year = {2019},
volume = {136},
editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.12},
URN = {urn:nbn:de:0030-drops-105558},
doi = {10.4230/LIPIcs.SNAPL.2019.12},
annote = {Keywords: Formal Verification, Quantum Computing, Programming Languages, Quantum Error Correction, Certified Compilation, NISQ}
}