Functional programminglanguages are well-suited for developing compilers, and compilers for functional languages are often themselves written in a functional language. Functional abstractions, such as monads, allow a...
详细信息
ISBN:
(纸本)9781450369817
Functional programminglanguages are well-suited for developing compilers, and compilers for functional languages are often themselves written in a functional language. Functional abstractions, such as monads, allow abstracting away some of the repetitive structure of a compiler, removing boilerplate code and making extensions simpler. Even so, functional languages are rarely used to implement compilers for languages of other paradigms. this paper reports on the experience of a four-year long project where we developed a compiler for a concurrent, object-oriented language using the functional language Haskell. the focus of the paper is the implementation of the type checker, but the design works well in static analysis tools, such as tracking uniqueness of variables to ensure data-race freedom. the paper starts from a simple type checker to which we add more complex features, such as type state, with minimal changes to the overall initial design.
JavaScript performance is paramount to a user's browsing experience. Browser vendors have gone to great lengths to improve JavaScript's steady-state performance. this has led to sophisticated web applications....
详细信息
ISBN:
(纸本)9781450367127
JavaScript performance is paramount to a user's browsing experience. Browser vendors have gone to great lengths to improve JavaScript's steady-state performance. this has led to sophisticated web applications. However, as users increasingly expect instantaneous page load times, another important goal for JavaScript engines is to attain minimal startup times. In this paper, we reduce the startup time of JavaScript programs by enhancing the reuse of compilation and optimization information across different executions. Specifically, we propose a new scheme to increase the startup performance of Inline Caching (IC), a key optimization for dynamic type systems. the idea is to represent a substantial portion of the IC information in an execution in a context-independent way, and reuse it in subsequent executions. We call our enhanced IC design Reusable Inline Caching (RIC). We integrate RIC into the state-of-the-art Google V8 JavaScript engine and measure its impact on the initialization time of popular JavaScript libraries. By recycling IC information collected from a previous execution, RIC reduces the average initialization time per library by 17%.
We derive a variant of quantum Hoare logic (QHL), called applied quantum Hoare logic (aQHL for short), by: (1) restricting QHL to a special class of preconditions and postconditions, namely projections, which can sign...
详细信息
ISBN:
(纸本)9781450367127
We derive a variant of quantum Hoare logic (QHL), called applied quantum Hoare logic (aQHL for short), by: (1) restricting QHL to a special class of preconditions and postconditions, namely projections, which can significantly simplify verification of quantum programs and are much more convenient when used in debugging and testing;and (2) adding several rules for reasoning about robustness of quantum programs, i.e. error bounds of outputs. the effectiveness of aQHL is shown by its applications to verify two sophisticated quantum algorithms: HHL (Harrow-Hassidim-Lloyd) for solving systems of linear equations and qPCA (quantum Principal Component Analysis).
We propose a new probabilistic programminglanguage for the design and analysis of perception systems, especially those based on machine learning. Specifically, we consider the problems of training a perception system...
详细信息
ISBN:
(纸本)9781450367127
We propose a new probabilistic programminglanguage for the design and analysis of perception systems, especially those based on machine learning. Specifically, we consider the problems of training a perception system to handle rare events, testing its performance under different conditions, and debugging failures. We show how a probabilistic programminglanguage can help address these problems by specifying distributions encoding interesting types of inputs and sampling these to generate specialized training and test sets. More generally, such languages can be used for cyber-physical systems and robotics to write environment models, an essential prerequisite to any formal analysis. In this paper, we focus on systems like autonomous cars and robots, whose environment is a scene, a configuration of physical objects and agents. We design a domain-specific language, Scenic, for describing scenarios that are distributions over scenes. As a probabilistic programminglanguage, Scenic allows assigning distributions to features of the scene, as well as declaratively imposing hard and soft constraints over the scene. We develop specialized techniques for sampling from the resulting distribution, taking advantage of the structure provided by Scenic's domain-specific syntax. Finally, we apply Scenic in a case study on a convolutional neural network designed to detect cars in road images, improving its performance beyond that achieved by state-of-the-art synthetic data generation methods.
To understand diverse natural language commands, virtual assistants today are trained with numerous labor-intensive, manually annotated sentences. this paper presents a methodology and the Genie toolkit that can handl...
详细信息
ISBN:
(纸本)9781450367127
To understand diverse natural language commands, virtual assistants today are trained with numerous labor-intensive, manually annotated sentences. this paper presents a methodology and the Genie toolkit that can handle new compound commands with significantly less manual effort. We advocate formalizing the capability of virtual assistants with a Virtual Assistant programminglanguage (VAPL) and using a neural semantic parser to translate natural language into VAPL code. Genie needs only a small realistic set of input sentences for validating the neural model. Developers write templates to synthesize data;Genie uses crowdsourced paraphrases and data augmentation, along withthe synthesized data, to train a semantic parser. We also propose design principles that make VAPL languages amenable to natural language translation. We apply these principles to revise thingTalk, the language used by the Almond virtual assistant. We use Genie to build the first semantic parser that can support compound virtual assistants commands with unquoted free-form parameters. Genie achieves a 62% accuracy on realistic user inputs. We demonstrate Genie's generality by showing a 19% and 31% improvement over the previous state of the art on a music skill, aggregate functions, and access control.
Adaptive software becomes more and more important as computing is increasingly context-dependent. Runtime adaptability can be achieved by dynamically selecting and applying context-specific code. Role-oriented program...
详细信息
ISBN:
(纸本)9781450369817
Adaptive software becomes more and more important as computing is increasingly context-dependent. Runtime adaptability can be achieved by dynamically selecting and applying context-specific code. Role-oriented programming has been proposed as a paradigm to enable runtime adaptive software by design. Roles change the objects' behavior at runtime and thus allow adapting the software to a given context. However, this increased variability and expressiveness has a direct impact on performance and memory consumption. We found a high overhead in the steady-state performance of executing compositions of adaptations. this paper presents a new approach to use run-time information to construct a dispatch plan that can be executed efficiently by the JVM. the concept of late binding is extended to dynamic function compositions. We evaluated the implementation with a benchmark for role-oriented programminglanguages leveraging context-dependent role semantics achieving a mean speedup of 2.79x over the regular implementation.
In a typical data-processing program, the representation of data in memory is distinct from its representation in a serialized form on disk. the former has pointers and arbitrary, sparse layout, facilitating easy mani...
详细信息
ISBN:
(纸本)9781450367127
In a typical data-processing program, the representation of data in memory is distinct from its representation in a serialized form on disk. the former has pointers and arbitrary, sparse layout, facilitating easy manipulation by a program, while the latter is packed contiguously, facilitating easy I/O. We propose a language, LoCal, to unify in-memory and serialized formats. LoCal extends a region calculus into a location calculus, employing a type system that tracks the byte-addressed layout of all heap values. We formalize LoCal and prove type safety, and show how LoCal programs can be inferred from unannotated source terms. We transform the existing Gibbon compiler to use LoCal as an intermediate language, withthe goal of achieving a balance between code speed and data compactness by introducing just enough indirection into heap layouts, preserving the asymptotic complexity of traditional representations, but working with mostly or completely serialized data. We show that our approach yields significant performance improvement over prior approaches to operating on packed data, without abandoning idiomatic programming with recursive functions.
Real-world cryptographic code is often written in a subset of C intended to execute in constant-time, thereby avoiding timing side channel vulnerabilities. this C subset eschews structured programming as we know it: i...
详细信息
ISBN:
(纸本)9781450367127
Real-world cryptographic code is often written in a subset of C intended to execute in constant-time, thereby avoiding timing side channel vulnerabilities. this C subset eschews structured programming as we know it: if-statements, looping constructs, and procedural abstractions can leak timing information when handling sensitive data. the resulting obfuscation has led to subtle bugs, even in widely-used high-profile libraries like OpenSSL. To address the challenge of writing constant-time cryptographic code, we present FaCT, a crypto DSL that provides high-level but safe language constructs. the FaCT compiler uses a secrecy type system to automatically transform potentially timing-sensitive high-level code into low-level, constant-time LLVM bitcode. We develop the language and type system, formalize the constant-time transformation, and present an empirical evaluation that uses FaCT to implement core crypto routines from several open-source projects including OpenSSL, libsodium, and curve25519-donna. Our evaluation shows that FaCT's design makes it possible to write readable, high-level cryptographic code, with efficient, constant-time behavior.
the proceedings contain 8 papers. the topics discussed include: fluid data structures;detecting unsatisfiable CSS rules in the presence of DTDs;towards compiling graph queries in relational engines;streaming saturatio...
ISBN:
(纸本)9781450367189
the proceedings contain 8 papers. the topics discussed include: fluid data structures;detecting unsatisfiable CSS rules in the presence of DTDs;towards compiling graph queries in relational engines;streaming saturation for large RDF graphs with dynamic schema information;arc: an IR for batch and stream programming;on the semantics of cypher’s implicit group-by;mixing set and bag semantics;and language-integrated provenance by trace analysis.
Recent advances in machine learning (ML) have produced KiloByte-size models that can directly run on constrained IoT devices. this approach avoids expensive communication between IoT devices and the cloud, thereby ena...
详细信息
ISBN:
(纸本)9781450367127
Recent advances in machine learning (ML) have produced KiloByte-size models that can directly run on constrained IoT devices. this approach avoids expensive communication between IoT devices and the cloud, thereby enabling energy-efficient real-time analytics. However, ML models are expressed typically in floating-point, and IoT hardware typically does not support floating-point. therefore, running these models on IoT devices requires simulating IEEE-754 floating-point using software, which is very inefficient. We present SeeDot, a domain-specific language to express ML inference algorithms and a compiler that compiles SeeDot programs to fixed-point code that can efficiently run on constrained IoT devices. We propose 1) a novel compilation strategy that reduces the search space for some key parameters used in the fixed-point code, and 2) new efficient implementations of expensive operations. SeeDot compiles state-of-the-art KB-sized models to various microcontrollers and low-end FPGAs. We show that SeeDot outperforms 1) software emulation of floating-point (Arduino), 2) high-bitwidth fixed-point (MATLAB), 3) post-training quantization (TensorFlow-Lite), and 4) floating- and fixed-point FPGA implementations generated using high-level synthesis tools.
暂无评论