The proceedings contain 77 papers. The topics discussed include: data-driven inference of representation invariants;type error feedback via analytic program repair;synthesizing structured CAD models with equality satu...
ISBN:
(纸本)9781450376136
The proceedings contain 77 papers. The topics discussed include: data-driven inference of representation invariants;type error feedback via analytic program repair;synthesizing structured CAD models with equality saturation and inverse transformations;compiler and runtime support for continuation marks;from folklore to fact: comparing implementations of stacks and continuations;learning nonlinear loop invariants with gated continuous logic networks;blended, precise semantic program embeddings;and BlankIt library debloating: getting what you want instead of cutting what you don't.
We present ***, a synchronous reactive language that adds synchronous concurrency and preemption to JavaScript. Inspired from Esterel, *** simplifies the programming of non-trivial temporal behaviors as found in compl...
详细信息
ISBN:
(纸本)9781450376136
We present ***, a synchronous reactive language that adds synchronous concurrency and preemption to JavaScript. Inspired from Esterel, *** simplifies the programming of non-trivial temporal behaviors as found in complex web interfaces or IoT controllers and the cooperation between synchronous and asynchronous activities. *** is compiled into plain sequential JavaScript and executes on unmodified runtime environments. We use three examples to present and discuss ***: a simple web login form to introduce the language and show how it differs from JavaScript, and two real life examples, a medical prescription pillbox and an interactive music system that show why concurrency and preemption help programming such temporal applications.
We present lambda PSI, the first probabilistic programminglanguage and system that supports higher-order exact inference for probabilistic programs with first-class functions, nested inference and discrete, continuou...
详细信息
ISBN:
(纸本)9781450376136
We present lambda PSI, the first probabilistic programminglanguage and system that supports higher-order exact inference for probabilistic programs with first-class functions, nested inference and discrete, continuous and mixed random variables. lambda PSI's solver is based on symbolic reasoning and computes the exact distribution represented by a program. We show that lambda PSI is practically effective-it automatically computes exact distributions for a number of interesting applications, from rational agents to information theory, many of which could so far only be handled approximately.
Existing quantum languages force the programmer to work at a low level of abstraction leading to unintuitive and cluttered code. A fundamental reason is that dropping temporary values from the program state requires e...
详细信息
ISBN:
(纸本)9781450376136
Existing quantum languages force the programmer to work at a low level of abstraction leading to unintuitive and cluttered code. A fundamental reason is that dropping temporary values from the program state requires explicitly applying quantum operations that safely uncompute these values. We present Silq, the first quantum language that addresses this challenge by supporting safe, automatic uncomputation. This enables an intuitive semantics that implicitly drops temporary values, as in classical computation. To ensure physicality of Silq's semantics, its type system leverages novel annotations to reject unphysical programs. Our experimental evaluation demonstrates that Silq programs are not only easier to read and write, but also significantly shorter than equivalent programs in other quantum languages (on average -46% for Q#, -38% for Quipper), while using only half the number of quantum primitives.
The Bluespec hardware-description language presents a significantly higher-level view than hardware engineers are used to, exposing a simpler concurrency model that promotes formal proof, without compromising on perfo...
详细信息
ISBN:
(纸本)9781450376136
The Bluespec hardware-description language presents a significantly higher-level view than hardware engineers are used to, exposing a simpler concurrency model that promotes formal proof, without compromising on performance of compiled circuits. Unfortunately, the cost model of Bluespec has been unclear, with performance details depending on a mix of user hints and opaque static analysis of potential concurrency conflicts within a design. In this paper we present Koika, a derivative of Bluespec that preserves its desirable properties and yet gives direct control over the scheduling decisions that determine performance. Koika has a novel and deterministic operational semantics that uses dynamic analysis to avoid concurrency anomalies. Our implementation includes Coq definitions of syntax, semantics, key metatheorems, and a verified compiler to circuits. We argue that most of the extra circuitry required for dynamic analysis can be eliminated by compile-time BSV-style static analysis.
Synchronous modeling is at the heart of programminglanguages like Lustre, Esterel, or SCADE used routinely for implementing safety critical control software, e.g., fly-by-wire and engine control in planes. However, t...
详细信息
ISBN:
(纸本)9781450376136
Synchronous modeling is at the heart of programminglanguages like Lustre, Esterel, or SCADE used routinely for implementing safety critical control software, e.g., fly-by-wire and engine control in planes. However, to date these languages have had limited modern support for modeling uncertainty - probabilistic aspects of the software's environment or behavior - even though modeling uncertainty is a primary activity when designing a control system. In this paper we present ProbZelus the first synchronous probabilistic programminglanguage. ProbZelus conservatively provides the facilities of a synchronous language to write control software, with probabilistic constructs to model uncertainties and perform inference-in-the-loop. We present the design and implementation of the language. We propose a measure-theoretic semantics of probabilistic stream functions and a simple type discipline to separate deterministic and probabilistic expressions. We demonstrate a semantics-preserving compilation into a first-order functional language that lends itself to a simple presentation of inference algorithms for streaming models. We also redesign the delayed sampling inference algorithm to provide efficient streaming inference. Together with an evaluation on several reactive applications, our results demonstrate that ProbZelus enables the design of reactive probabilistic applications and efficient, bounded memory inference.
The efficient implementation of function calls and non-local control transfers is a critical part of modern languageimplementations and is important in the implementation of everything from recursion, higher-order fu...
详细信息
ISBN:
(纸本)9781450376136
The efficient implementation of function calls and non-local control transfers is a critical part of modern languageimplementations and is important in the implementation of everything from recursion, higher-order functions, concurrency and coroutines, to task-based parallelism. In a compiler, these features can be supported by a variety of mechanisms, including call stacks, segmented stacks, and heap-allocated continuation closures. An implementor of a high-level language with advanced control features might ask the question lwhat is the best choice for my implementation?z Unfortunately, the current literature does not provide much guidance, since previous studies suffer from various flaws in methodology and are outdated for modern hardware. In the absence of recent, well-normalized measurements and a holistic overview of their implementation specifics, the path of least resistance when choosing a strategy is to trust folklore, but the folklore is also suspect. This paper attempts to remedy this situation by providing an lapples-to-applesz comparison of six different approaches to implementing call stacks and continuations. This comparison uses the same source language, compiler pipeline, LLVM-backend, and runtime system, with the only differences being those required by the differences in implementationstrategy. We compare the implementation challenges of the different approaches, their sequential performance, and their suitability to support advanced control mechanisms, including supporting heavily threaded code. In addition to the comparison of implementationstrategies, the paper's contributions also include a number of useful implementation techniques that we discovered along the way.
Network misconfiguration has caused a raft of high-profile outages over the past decade, spurring researchers to develop a variety of network analysis and verification tools. Unfortunately, developing and maintaining ...
详细信息
ISBN:
(纸本)9781450376136
Network misconfiguration has caused a raft of high-profile outages over the past decade, spurring researchers to develop a variety of network analysis and verification tools. Unfortunately, developing and maintaining such tools is an enormous challenge due to the complexity of network configuration languages. Inspired by work on intermediate languages for verification such as Boogie and Why3, we develop NV, an intermediate language for verification of network control planes. NV carefully walks the line between expressiveness and tractability, making it possible to build models for a practical subset of real protocols and their configurations, and also facilitate rapid development of tools that outperform state-of-the-art simulators (seconds vs minutes) and verifiers (often 10x faster). Furthermore, we show that it is possible to develop novel analyses just by writing new NV programs. In particular, we implement a new fault-tolerance analysis that scales to far larger networks than existing tools.
We introduce Gillian, a platform for developing symbolic analysis tools for programminglanguages. Here, we focus on the symbolic execution engine at the heart of Gillian, which is parametric on the memory model of th...
详细信息
ISBN:
(纸本)9781450376136
We introduce Gillian, a platform for developing symbolic analysis tools for programminglanguages. Here, we focus on the symbolic execution engine at the heart of Gillian, which is parametric on the memory model of the target language. We give a formal description of the symbolic analysis and a modular implementation that closely follows this description. We prove a parametric soundness result, introducing restriction on abstract states, which generalises path conditions used in classical symbolic execution. We instantiate Gillian to obtain trusted symbolic testing tools for JavaScript and C, and use these tools to find bugs in real-world code, thus demonstrating the viability of our parametric approach.
The real numbers are pervasive, both in daily life, and in mathematics. students spend much time studying their properties. Yet computers and programminglanguages generally provide only an approximation geared toward...
详细信息
ISBN:
(纸本)9781450376136
The real numbers are pervasive, both in daily life, and in mathematics. students spend much time studying their properties. Yet computers and programminglanguages generally provide only an approximation geared towards performance, at the expense of many of the nice properties we were taught in high school. Although this is entirely appropriate for many applications, particularly those that are sensitive to arithmetic performance in the usual sense, we argue that there are others where it is a poor choice. If arithmetic computations and result are directly exposed to human users who are not floating point experts, floating point approximations tend to be viewed as bugs. For applications such as calculators, spreadsheets, and various verification tasks, the cost of precision sacrifices is high, and the performance benefit is often not critical. We argue that previous attempts to provide accurate and understandable results for such applications using the recursive reals were great steps in the right direction, but they do not suffice. Comparing recursive reals diverges if they are equal. In many cases, comparison of numbers, including equal ones, is both important, particularly in simple cases, and intractable in the general case. We propose an API for a real number type that explicitly provides decidable equality in the easy common cases, in which it is often unnatural not to. We describe a surprisingly compact and simple implementation in detail. The approach relies heavily on classical number theory results. We demonstrate the utility of such a facility in two applications: testing floating point functions, and to implement arithmetic in Google's Android calculator application.
暂无评论