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

42nd acm sigplan International conference on programming language design and implementation (PLDI)

作者： Baudart, Guillaume Burroni, Javier Hirzel, Martin Mandel, Louis Shinnar, Avraham PSL Univ Ecole Normale Super INRIA Paris Paris France UMass Amherst Amherst MA USA IBM Res MIT IBM Watson AI Lab Armonk NY USA

ISBN: (纸本)9781450383912

Stan is a probabilistic programming language that is popular in the statistics community, with a high-level syntax for expressing probabilistic models. Stan differs by nature from generative probabilistic programming languages like Church, Anglican, or Pyro. This paper presents a comprehensive compilation scheme to compile any Stan model to a generative language and proves its correctness. We use our compilation scheme to build two new backends for the Stanc3 compiler targeting Pyro and NumPyro. Experimental results show that the NumPyro backend yields a 2.3x speedup compared to Stan in geometric mean over 26 benchmarks. Building on Pyro we extend Stan with support for explicit variational inference guides and deep probabilistic models. That way, users familiar with Stan get access to new features without having to learn a fundamentally new language.

关键词： Probabilistic programming Semantics Stan Pyro

来源：评论

学校读者我要写书评

暂无评论

The Essence of Bluespec A Core language for Rule-Based Hardware design 2020

The Essence of Bluespec A Core Language for Rule-Based Hardw...

引用

41st acm sigplan conference on programming language design and implementation (PLDI)

作者： Bourgeat, Thomas Pit-Claudel, Clement Chlipala, Adam Arvind MIT CSAIL 77 Massachusetts Ave Cambridge MA 02139 USA

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.

关键词： HDL Semantics Compiler Correctness

来源：评论

学校读者我要写书评

暂无评论

Defining the Undefinedness of C 15

Defining the Undefinedness of C

引用

36th acm sigplan conference on programming language design and implementation

作者： Hathhorn, Chris Ellison, Chucky Rosu, Grigore Univ Missouri Columbia MO 65211 USA Univ Illinois Urbana IL 61801 USA

ISBN: (纸本)9781450334686

We present a "negative" semantics of the C11 language-a semantics that does not just give meaning to correct programs, but also rejects undefined programs. We investigate undefined behavior in C and discuss the techniques and special considerations needed for formally specifying it. We have used these techniques to modify and extend a semantics of C into one that captures undefined behavior. The amount of semantic infrastructure and effort required to achieve this was unexpectedly high, in the end nearly doubling the size of the original semantics. From our semantics, we have automatically extracted an undefinedness checker, which we evaluate against other popular analysis tools, using our own test suite in addition to a third-party test suite. Our checker is capable of detecting examples of all 77 categories of core language undefinedness appearing in the C11 standard, more than any other tool we considered. Based on this evaluation, we argue that our work is the most comprehensive and complete semantic treatment of undefined behavior in C, and thus of the C language itself.

关键词： Undefined behavior programming language semantics C11 K Framework

来源：评论

学校读者我要写书评

暂无评论

Jedd:: A BDD-based relational extension of Java

Jedd:: A BDD-based relational extension of Java

引用

conference on programming language design and implementation

作者： Lhoták, O Hendren, L McGill Univ Sch Comp Sci Sable Res Grp Montreal PQ Canada

In this paper we present Jedd, a language extension to Java that supports a convenient way of programming with Binary Decision Diagrams (BDDs). The Jedd language abstracts BDDs as database-style relations and operations on relations, and provides static type rules to ensure that relational operations are used correctly. The paper provides a description of the Jedd language and reports on the design and implementation of the Jedd translator and associated runtime system. Of particular interest is the approach to assigning attributes from the high-level relations to physical domains in the underlying BDDs, which is done by expressing the constraints as a SAT problem and using a modern SAT solver to compute the solution. Further, a runtime system is defined that handles memory management issues and supports a browsable profiling tool for tuning the key BDD operations. The motivation for designing Jedd was to support the development of whole program analyses based on BDDs, and we have used Jedd to express five key interrelated whole program analyses in our Soot compiler framework. We provide some examples of this application and discuss our experiences using Jedd.

关键词： binary decision diagrams relations language design Java program analysis Boolean formula satisfiability

来源：评论

学校读者我要写书评

暂无评论

Associated Effects Flexible Abstractions for Effectful programming

引用

proceedings OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 394-416页

作者： Lutze, Matthew Madsen, Magnus Aarhus Univ Aarhus Denmark

We present associated effects, a programming language feature that enables type classes to abstract over the effects of their function signatures, allowing each type class instance to specify its concrete effects. Associated effects significantly increase the flexibility and expressive power of a programming language that combines a type and effect system with type classes. In particular, associated effects allow us to (i) abstract over total and partial functions, where partial functions may throw exceptions, (ii) abstract over immutable data structures and mutable data structures that have heap effects, and (iii) implement adaptors that combine type classes with algebraic effects. We implement associated effects as an extension of the Flix programming language and refactor the Flix Standard Library to use associated effects, significantly increasing its flexibility and expressive power. Specifically, we add associated effects to 11 type classes, which enables us to add 28 new type class instances.

关键词： effect systems associated effects associated types generic programming type classes type functions ad-hoc polymorphism

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Semantics Driven Hardware design, implementation, and Verification with ReWire 15

Semantics Driven Hardware Design, Implementation, and Verifi...

引用

acm sigplan/SIGBED conference on languages, Compilers and Tools for Embedded Systems (LCTES 15)

作者： Procter, Adam Harrison, William L. Graves, Ian Becchi, Michela Allwein, Gerard Univ Missouri Columbia MO 65211 USA US Naval Res Lab Stennis Space Ctr MS USA

ISBN: (纸本)9781450332576

There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential, because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This paper presents ReWire, a functional programming language providing a suitable foundation for formal verification of hardware designs, and a compiler for that language that translates high-level, semantics-driven designs directly into working hardware. ReWire's design and implementation are presented, along with a case study in the design of a secure multicore processor, demonstrating both ReWire's expressiveness as a programming language and its power as a framework for formal, high-level reasoning about hardware systems.

关键词： Formal verification

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

A study of concurrent real-time garbage collectors 08

A study of concurrent real-time garbage collectors

引用

acm sigplan conference on programming language design and implementation

作者： Pizlo, Filip Petrank, Erez Steensgaard, Bjarne Purdue Univ W Lafayette IN 47907 USA Microsoft Res Redmond WA 98052 USA

ISBN: (纸本)9781595938602

Concurrent garbage collection is highly attractive for real-time systems, because offloading the collection effort from the executing threads allows faster response, allowing for extremely short deadlines at the microseconds level. Concurrent collectors also offer much better scalability over incremental collectors. The main problem with concurrent real-time collectors is their complexity. The first concurrent real-time garbage collector that can support fine synchronization, STOPLESS, has recently been presented by Pizlo et al. In this paper, we propose two additional ( and different) algorithms for concurrent real-time garbage collection: CLOVER and CHICKEN. Both collectors obtain reduced complexity over the first collector STOPLESS, but need to trade a benefit for it. We study the algorithmic strengths and weaknesses of CLOVER and CHICKEN and compare them to STOPLESS. Finally, we have implemented all three collectors on the Bartok compiler and runtime for C# and we present measurements to compare their efficiency and responsiveness.

关键词： algorithms design performance reliability

来源：评论

学校读者我要写书评

暂无评论

Dynamo: A transparent dynamic optimization system

Dynamo: A transparent dynamic optimization system

引用

acm sigplan' 00 conference on programming language design and implementation (PLDI)

作者： Bala, V Duesterwald, E Banerjia, S Hewlett Packard Labs Cambridge MA 02142 USA

We describe the design and implementation of Dynamo, a software dynamic optimization system that is capable of transparently improving the performance of a native instruction stream as it executes on the processor. The input native instruction stream to Dynamo can be dynamically generated (by a JIT for example), or it can come from the execution of a statically compiled native binary. This paper evaluates the Dynamo system in the latter, more challenging situation, in order to emphasize the limits, rather than the potential, of the system. Our experiments demonstrate that even statically optimized native binaries can be accelerated Dynamo, and often by a significant degree. For example, the average performance of -O optimized SpecInt95 benchmark binaries created by the HP product C compiler is improved to a level comparable to their -O4 optimized version running without Dynamo. Dynamo achieves this by focusing its efforts on optimization opportunities that tend to manifest only at runtime, and hence opportunities that might be difficult for a static compiler to exploit. Dynamo's operation is transparent in the sense that it does not depend on any user annotations or binary instrumentation, and does not require multiple runs, or any special compiler, operating system or hardware support. The Dynamo prototype presented here is a realistic implementation running on an HP PA-8000 workstation under the HPUX 10.20 operating system.

关键词： Computer systems programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：