检索结果-内蒙古大学图书馆

Probability Type Inference for Flexible Approximate programming

acm sigplan NOTICES 2015年第10期50卷 470-487页

作者： Boston, Brett Sampson, Adrian Grossman, Dan Ceze, Luis Univ Washington Seattle WA 98195 USA

In approximate computing, programs gain efficiency by allowing occasional errors. Controlling the probabilistic effects of this approximation remains a key challenge. We propose a new approach where programmers use a type system to communicate high-level constraints on the degree of approximation. A combination of type inference, code specialization, and optional dynamic tracking makes the system expressive and convenient. The core type system captures the probability that each operation exhibits an error and bounds the probability that each expression deviates from its correct value. Solver-aided type inference lets the programmer specify the correctness probability on only some variables-program outputs, for example-and automatically fills in other types to meet these specifications. An optional dynamic type helps cope with complex run-time behavior where static approaches are insufficient. Together, these features interact to yield a high degree of programmer control while offering a strong soundness guarantee. We use existing approximate-computing benchmarks to show how our language, DECAF, maintains a low annotation burden. Our constraint-based approach can encode hardware details, such as finite degrees of reliability, so we also use DECAF to examine implications for approximate hardware design. We find that multi-level architectures can offer advantages over simpler two-level machines and that solveraided optimization improves efficiency.

关键词： approximate computing type inference

来源：评论

学校读者我要写书评

暂无评论

Getting F-Bounded Polymorphism into Shape 14

Getting F-Bounded Polymorphism into Shape

引用

35th acm sigplan conference on programming language design and implementation (PLDI)

作者： Greenman, Ben Muehlboeck, Fabian Tate, Ross Cornell Univ Ithaca NY 14853 USA

ISBN: (纸本)9781450327848

We present a way to restrict recursive inheritance without sacrificing the benefits of F-bounded polymorphism. In particular, we distinguish two new concepts, materials and shapes, and demonstrate through a survey of 13.5 million lines of open-source generic-Java code that these two concepts never actually overlap in practice. With this Material-Shape Separation, we prove that even naive type-checking algorithms are sound and complete, some of which address problems that were unsolvable even under the existing proposals for restricting inheritance. We illustrate how the simplicity of our design reflects the design intuitions employed by programmers and potentially enables new features coming into demand for upcoming programming languages.

关键词： Algorithms design languages Materials Shapes Separation Subtyping F-Bounded Polymorphism Variance Decidability Joins Higher-Kinded Types

来源：评论

学校读者我要写书评

暂无评论

Code Completion with Statistical language Models 14

Code Completion with Statistical Language Models

引用

35th acm sigplan conference on programming language design and implementation (PLDI)

作者： Raychev, Veselin Vechev, Martin Yahav, Eran Swiss Fed Inst Technol Zurich Switzerland Technion Haifa Israel

ISBN: (纸本)9781450327848

We address the problem of synthesizing code completions for programs using APIs. Given a program with holes, we synthesize completions for holes with the most likely sequences of method calls. Our main idea is to reduce the problem of code completion to a natural-language processing problem of predicting probabilities of sentences. We design a simple and scalable static analysis that extracts sequences of method calls from a large codebase, and index these into a statistical language model. We then employ the language model to find the highest ranked sentences, and use them to synthesize a code completion. Our approach is able to synthesize sequences of calls across multiple objects together with their arguments. Experiments show that our approach is fast and effective. Virtually all computed completions typecheck, and the desired completion appears in the top 3 results in 90% of the cases.

关键词： Static analysis

来源：评论

学校读者我要写书评

暂无评论

Resugaring: Lifting Evaluation Sequences through Syntactic Sugar 14

Resugaring: Lifting Evaluation Sequences through Syntactic S...

引用

35th acm sigplan conference on programming language design and implementation (PLDI)

作者： Pombrio, Justin Krishnamurthi, Shriram Brown Univ Providence RI 02912 USA

ISBN: (纸本)9781450327848

Syntactic sugar is pervasive in language technology. It is used to shrink the size of a core language;to define domain-specific languages;and even to let programmers extend their language. Unfortunately, syntactic sugar is eliminated by transformation, so the resulting programs become unfamiliar to authors. Thus, it comes at a price: it obscures the relationship between the user's source program and the program being evaluated. We address this problem by showing how to compute reduction steps in terms of the surface syntax. Each step in the surface language emulates one or more steps in the core language. The computed steps hide the transformation, thus maintaining the abstraction provided by the surface language. We make these statements about emulation and abstraction precise, prove that they hold in our formalism, and verify part of the system in Coq. We have implemented this work and applied it to three very different languages.

关键词： programming languages Syntactic Sugar Macros Evaluation Debugging Resugaring

来源：评论

学校读者我要写书评

暂无评论

StreamJIT: A Commensal Compiler for High-Performance Stream programming

引用

acm sigplan NOTICES 2014年第10期49卷 177-195页

作者： Bosboom, Jeffrey Rajadurai, Sumanaruban Wong, Weng-Fai Amarasinghe, Saman MIT CSAIL Cambridge MA 02139 USA Natl Univ Singapore Singapore 117548 Singapore

There are many domain libraries, but despite the performance benefits of compilation, domain-specific languages are comparatively rare due to the high cost of implementing an optimizing compiler. We propose commensal compilation, a new strategy for compiling embedded domain-specific languages by reusing the massive investment in modern language virtual machine platforms. Commensal compilers use the host language's front-end, use host platform APIs that enable back-end optimizations by the host platform JIT, and use an autotuner for optimization selection. The cost of implementing a commensal compiler is only the cost of implementing the domain-specific optimizations. We demonstrate the concept by implementing a commensal compiler for the stream programming language StreamJIT atop the Java platform. Our compiler achieves performance 2.8 times better than the StreamIt native code (via GCC) compiler with considerably less implementation effort.

关键词： Domain-specific languages embedded domain-specific languages

来源：评论

学校读者我要写书评

暂无评论

Dynamic Enforcement of Determinism in a Parallel Scripting language 14

Dynamic Enforcement of Determinism in a Parallel Scripting L...

引用

35th acm sigplan conference on programming language design and implementation (PLDI)

作者： Lu, Li Ji, Weixing Scott, Michael L. Univ Rochester Rochester NY 14627 USA Beijing Inst Technol Beijing Peoples R China

ISBN: (纸本)9781450327848

Determinism is an appealing property for parallel programs, as it simplifies understanding, reasoning and debugging. It is particularly appealing in dynamic (scripting) languages, where ease of programming is a dominant design goal. Some existing parallel languages use the type system to enforce determinism statically, but this is not generally practical for dynamic languages. In this paper, we describe how determinism can be obtained-and dynamically enforced/verified-for appropriate extensions to a parallel scripting language. Specifically, we introduce the constructs of Deterministic Parallel Ruby (DPR), together with a run-time system (TARDIS) that verifies properties required for determinism, including correct usage of reductions and commutative operators, and the mutual independence (data-race freedom) of concurrent tasks. Experimental results confirm that DPR can provide scalable performance on multicore machines and that the overhead of TARDIS is low enough for practical testing. In particular, TARDIS significantly outperforms alternative data-race detectors with comparable functionality. We conclude with a discussion of future directions in the dynamic enforcement of determinism.

关键词： design languages Reliability Determinism deterministic parallelism data races scripting language

来源：评论

学校读者我要写书评

暂无评论

A Seamless, Client-Centric programming Model for Type Safe Web Applications

引用

acm sigplan NOTICES 2014年第12期49卷 79-89页

作者： Ekblad, Anton Claessen, Koen Chalmers Gothenburg Sweden

We propose a new programming model for web applications which is (1) seamless;one program and one language is used to produce code for both client and server, (2) client-centric;the programmer takes the viewpoint of the client that runs code on the server rather than the other way around, (3) functional and type-safe, and (4) portable;everything is implemented as a Haskell library that implicitly takes care of all networking code. Our aim is to improve the painful and error-prone experience of today's standard development methods, in which clients and servers are coded in different languages and communicate with each other using ad-hoc protocols. We present the design of our library called Haste. App, an example web application that uses it, and discuss the implementation and the compiler technology on which it depends.

关键词： web applications distributed systems network communication

来源：评论

学校读者我要写书评

暂无评论

FAST: a Transducer-Based language for Tree Manipulation 14

FAST: a Transducer-Based Language for Tree Manipulation

引用

35th acm sigplan conference on programming language design and implementation (PLDI)

作者： D'Antoni, Loris Veanes, Margus Livshits, Benjamin Molnar, David Univ Penn Philadelphia PA 19104 USA

ISBN: (纸本)9781450327848

Tree automata and tree transducers are used in a wide range of applications in software engineering, from XML processing to language type-checking. While these formalisms are of immense practical use, they can only model finite alphabets, and since many real-world applications operate over in finite domains such as integers, this is often a limitation. To overcome this problem we augment tree automata and transducers with symbolic alphabets represented as parametric theories. Admitting in finite alphabets makes these models more general and succinct than their classical counterparts. Despite this, we show how the main operations, such as composition and language equivalence, remain computable given a decision procedure for the alphabet theory. We introduce a high-level language called Fast that acts as a front-end for the above formalisms. Fast supports symbolic alphabets through tight integration with state-of-the art satisfiability modulo theory (SMT) solvers. We demonstrate our techniques on practical case studies, covering a wide range of applications.

关键词： Symbolic Tree Transducers FAST

来源：评论

学校读者我要写书评

暂无评论

First-class Runtime Generation of High-performance Types using Exotypes 14

First-class Runtime Generation of High-performance Types usi...

引用

35th acm sigplan conference on programming language design and implementation (PLDI)

作者： DeVito, Zachary Ritchie, Daniel Fisher, Matt Aiken, Alex Hanrahan, Pat Stanford Univ Stanford CA 94305 USA

ISBN: (纸本)9781450327848

We introduce exotypes, user-defined types that combine the flexibility of meta-object protocols in dynamically-typed languages with the performance control of low-level languages. Like objects in dynamic languages, exotypes are defined programmatically at runtime, allowing behavior based on external data such as a database schema. To achieve high performance, we use staged programming to define the behavior of an exotype during a runtime compilation step and implement exotypes in Terra, a low-level staged programming language. We show how exotype constructors compose, and use exotypes to implement high-performance libraries for serialization, dynamic assembly, automatic differentiation, and probabilistic programming. Each exotype achieves expressiveness similar to libraries written in dynamically-typed languages but implements optimizations that exceed the performance of existing libraries written in low-level statically-typed languages. Though each implementation is significantly shorter, our serialization library is 11 times faster than Kryo, and our dynamic assembler is 3-20 times faster than Google's Chrome assembler.

关键词： design Performance Lua Staged computation DSL

来源：评论

学校读者我要写书评

暂无评论

A Lightweight Symbolic Virtual Machine for Solver-Aided Host languages 14

A Lightweight Symbolic Virtual Machine for Solver-Aided Host...

引用

35th acm sigplan conference on programming language design and implementation (PLDI)

作者： Torlak, Emina Bodik, Rastislav Univ Calif Berkeley Berkeley CA 94608 USA

ISBN: (纸本)9781450327848

Solver-aided domain-specific languages (SDSLs) are an emerging class of computer-aided programming systems. They ease the construction of programs by using satisfiability solvers to automate tasks such as verification, debugging, synthesis, and non-deterministic execution. But reducing programming tasks to satisfiability problems involves translating programs to logical constraints, which is an engineering challenge even for domain-specific languages. We have previously shown that translation to constraints can be avoided if SDSLs are implemented by (traditional) embedding into a host language that is itself solver-aided. This paper describes how to implement a symbolic virtual machine (SVM) for such a host language. Our symbolic virtual machine is lightweight because it compiles to constraints only a small subset of the host's constructs, while allowing SDSL designers to use the entire language, including constructs for DSL embedding. This lightweight compilation employs a novel symbolic execution technique with two key properties: it produces compact encodings, and it enables concrete evaluation to strip away host constructs that are outside the subset compilable to constraints. Our symbolic virtual machine architecture is at the heart of ROSETTE, a solver-aided language that is host to several new SDSLs.

关键词： design languages Solver-Aided languages Symbolic Virtual Machine

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：