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

Compiling Probabilistic Programs for Variable Elimination with Information Flow

PROCEEDINGS OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 1755-1780页

作者： Li, Jianlin Wang, Eric Zhang, Yizhou Univ Waterloo Waterloo ON Canada

A key promise of probabilistic programming is the ability to specify rich models using an expressive programming language. However, the expressive power that makes probabilistic programming languages enticing also poses challenges to inference, so much so that specialized approaches to inference ban language features such as recursion. We present an approach to variable elimination and marginal inference for probabilistic programs featuring bounded recursion, discrete distributions, and sometimes continuous distributions. A compiler eliminates probabilistic side effects, using a novel information-flow type system to factorize probabilistic computations and hoist independent subcomputations out of sums or integrals. For a broad class of recursive programs with dynamically recurring substructure, the compiler effectively decomposes a global marginal-inference problem, which may otherwise be intractable, into tractable subproblems. We prove the compilation correct by showing that it preserves denotational semantics. Experiments show that the compiled programs subsume widely used PTIME algorithms for recursive models and that the compilation time scales with the size of the inference problems. As a separate contribution, we develop a denotational, logical-relations model of information-flow types in the novel measure-theoretic setting of probabilistic programming;we use it to prove noninterference and consequently the correctness of variable elimination.

关键词： Probabilistic programming probabilistic inference information flow

来源：评论

学校读者我要写书评

暂无评论

Light: Replay via Tightly Bounded Recording 15

Light: Replay via Tightly Bounded Recording

引用

36th acm sigplan conference on programming language design and implementation

作者： Liu, Peng Zhang, Xiangyu Tripp, Omer Zheng, Yunhui Purdue Univ W Lafayette IN 47907 USA

ISBN: (纸本)9781450334686

Reproducing concurrency bugs is a prominent challenge. Existing techniques either rely on recording very fine grained execution information and hence have high runtime overhead, or strive to log as little information as possible but provide no guarantee in reproducing a bug. We present Light, a technique that features much lower overhead compared to techniques based on fine grained recording, and that guarantees to reproduce concurrent bugs. We leverage and formally prove that recording flow dependences is the necessary and sufficient condition to reproduce a concurrent bug. The flow dependences, together with the thread local orders that can be automatically inferred (and hence not logged), are encoded as scheduling constraints. An SMT solver is used to derive a replay schedule, which is guaranteed to exist even though it may be different from the original schedule. Our experiments show that Light has only 44% logging overhead, almost one order of magnitude lower than the state of the art techniques relying on logging memory accesses. Its space overhead is only 10% of those techniques. Light can also reproduce all the bugs we have collected whereas existing techniques miss some of them.

关键词： design Performance Reliability Concurrency Replay Thread Determinism Tight Bound Local Recording

来源：评论

学校读者我要写书评

暂无评论

An experimental analysis of self-adjusting computation 06

An experimental analysis of self-adjusting computation

引用

acm sigplan conference on programming language design and implementation, PLDI 2006 - PLAS 2006: 2006 programming languages and Analysis for Security Workshop

作者： Acar, Umut A. Blelloch, Guy E. Blume, Matthias Tangwongsan, Kanat Toyota Technological Institute Japan Carnegie Mellon University United States

ISBN: (纸本)1595933743

Dependence graphs and memoization can be used to efficiently update the output of a program as the input changes dynamically. Recent work has studied techniques for combining these approaches to effectively dynamize a wide range of applications. Toward this end various theoretical results were given. In this paper we describe the implementation of a library based on these ideas, and present experimental results on the efficiency of this library on a variety of applications. The results of the experiments indicate that the approach is effective in practice, often requiring orders of magnitude less time than recomputing the output from scratch. We believe this is the first experimental evidence that incremental computation of any type is effective in practice for a reasonably broad set of applications. Copyright © 2006 acm.

关键词： Dynamic programming

来源：评论

学校读者我要写书评

暂无评论

Unfold/fold transformations and loop optimization of logic programs 88

Unfold/fold transformations and loop optimization of logic p...

引用

acm sigplan conference on programming language design and implementation, PLDI 1988

作者： Debray, Saumya K. Department of Computer Science University of Arizona TucsonAZ85721 United States

ISBN: (纸本)0897912691

Programs typically spend much of their execution time in loops. This makes the generation of efficient code for loops essential for good performance. Loop optimization of logic programming languages is complicated by the fact that such languages lack the iterative constructs of traditional languages, and instead use recursion to express loops. In this paper, we examine the application of unfold/fold transformations to three kinds of loop optimization for logic programming languages: recursion removal, loop fusion and code motion out of loops. We describe simple unfold/fold transformation sequences for these optimizations that can be automated relatively easily. In the process, we show that the properties of unification and logical variables can sometimes be used to generalize, from traditional languages, the conditions under which these optimizations may be carried out. Our experience suggests that such source-level transformations may he used as an effective tool for the optimization of logic programs. © 1988 acm.

关键词： Logic programming

来源：评论

学校读者我要写书评

暂无评论

Using role components to implement collaboration-based designs 11

Using role components to implement collaboration-based desig...

引用

Proceedings of the 1996 conference on Object-Oriented programming Systems, languages & Applications

作者： VanHilst, Michael Notkin, David Univ of Washington Seattle United States

ISBN: (纸本)089791788X

In this paper we present a method of code implementation that works in conjunction with collaboration and responsibility based analysis modeling techniques to achieve better code reuse and resilience to change. Our approach maintains a closer mapping from responsibilities in the analysis model to entities in the implementation. In so doing, it leverages the features of flexible design and design reuse found in collaboration-based design models to provide similar adaptability and reuse in the implementation. Our approach requires no special development tools and uses only standard features available in the C++ language. In an earlier paper we described the basic mechanisms used by our approach and discussed its advantages in comparison to the framework approach. In this paper we show how our approach combines code and design reuse, describing specific techniques that can be used in the development of larger applications.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

A static analyzer for large safety-critical software 03

引用

conference on programming language design and implementation

作者： Blanchet, B Cousot, P Cousot, R Feret, J Mauborgne, L Miné, A Monniaux, D Rival, X CNRS F-75700 Paris France Ecole Normale Super Paris France Ecole Polytech F-91128 Palaiseau France

ISBN: (纸本)9781581136623

We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by refinement of a general purpose static analyzer and later adaptation to particular programs of the family by the end-user through parametrization. This is applied to the proof of soundness of data manipulation operations at the machine level for periodic synchronous safety critical embedded software. The main novelties are the design principle of static analyzers by refinement and adaptation through parametrization (Sect. 3 and 7), the symbolic manipulation of expressions to improve the precision of abstract transfer functions (Sect. 6.3), the octagon (Sect. 6.2.2), ellipsoid (Sect. 6.2.3), and decision tree (Sect. 6.2.4) abstract domains, all with sound handling of rounding errors in floating point computations, widening strategies (with thresholds: Sect. 7.1.2, delayed: Sect. 7.1.3) and the automatic determination of the parameters (parametrized packing: Sect. 7.2).

关键词： algorithms design experimentation reliability theory verification abstract interpretation abstract domains static analysis verification floating point embedded reactive real-time safety-critical software

来源：评论

学校读者我要写书评

暂无评论

Extensible language implementation with Object Algebras (Short Paper) 2014

Extensible Language Implementation with Object Algebras (Sho...

引用

13th conference on Generative programming - Concepts and Experiences (GPCE)

作者： Gouseti, Maria Peters, Chiel van der Storm, Tijs CWI NL-1009 AB Amsterdam Netherlands

ISBN: (纸本)9781450331616

Object Algebras are a recently introduced design pattern to make the implementation of recursive data types more extensible. In this short paper we report our experience in using Object Algebras in building a realistic domain- specific language (DSL) for questionnaires, called QL. This experience has led to a simple, yet powerful set of tools for the practical and flexible implementation of highly extensible languages.

关键词： Object Algebras extensibility interpreter design languages

来源：评论

学校读者我要写书评

暂无评论

Kill-safe synchronization abstractions

Kill-safe synchronization abstractions

引用

Proceedings of the 2004 acm sigplan conference on programming language design and implementation (PLDI'04)

作者： Flatt, Matthew Findler, Robert Bruce University of Utah United States University of Chicago United States

When an individual task can be forcefully terminated at any time, cooperating tasks must communicate carefully. For example, if two tasks share an object, and if one task is terminated while it manipulates the object, the object may remain in an inconsistent or frozen state that incapacitates the other task. To support communication among terminable tasks, language run-time systems (and operating systems) provide kill-safe abstractions for inter-task communication. No kill-safe guarantee is available, however, for abstractions that are implemented outside the run-time system. In this paper, we show how a run-time system can support new kill-safe abstractions without requiring modification to the run-time system, and without requiring the run-time system to trust any new code. Our design frees the run-time implementor to provide only a modest set of synchronization primitives in the trusted computing base, while still allowing tasks to communicate using sophisticated abstractions.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

The exo VM system for automatic VM and application reduction 07

The exo VM system for automatic VM and application reduction

引用

conference on programming language design and implementation

作者： Titzer, Ben L. Auerbach, Joshua Bacon, David F. Palsberg, Jens Univ Calif Los Angeles Compilers Grp Los Angeles CA 90025 USA

ISBN: (纸本)9781595936332

Embedded systems pose unique challenges to Java application developers and virtual machine designers. Chief among these challenges is the memory footprint of both the virtual machine and the applications that run within it. With the rapidly increasing set of features provided by the Java language, virtual machine designers are often forced to build custom implementations that make various tradeoffs between the footprint of the virtual machine and the subset of the Java language and class libraries that are supported. In this paper, we present the Exo VM, a system in which an application is initialized in a fully featured virtual machine, and then the code, data, and virtual machine features necessary to execute it are packaged into a binary image. Key to this process is feature analysis, a technique for computing the reachable code and data of a Java program and its implementation inside the VM simultaneously. The Exo VM reduces the need to develop customized embedded virtual machines by reusing a single VM infrastructure and automatically eliding the implementation of unused Java features on a per-program basis. We present a constraint-based instantiation of the analysis technique, an implementation in IBM's J9 Java VM, experiments evaluating our technique for the EEMBC benchmark suite, and some discussion of the individual costs of some of Java's features. Our evaluation shows that our system can reduce the non-heap memory allocation of the virtual machine by as much as 75%. We discuss VM and language design decisions that our work shows are important in targeting embedded systems, supporting the long-term goal of a common VM infrastructure spanning from motes to large servers.

关键词： pre-initialization embedded systems persistence dead code elimination static compilation static analysis VM design VM modularity feature analysis

来源：评论

学校读者我要写书评

暂无评论

Fast and flexible instruction selection with on-demand tree-parsing automata 06

Fast and flexible instruction selection with on-demand tree-...

引用

acm sigplan conference on programming language design and implementation, PLDI 2006 - PLAS 2006: 2006 programming languages and Analysis for Security Workshop

作者： Ertl, M. Anton Casey, Kevin Gregg, David TU Wien Austria Trinity College Dublin Ireland Institut für Computersprachen Technische Universität Wien Argentinierstraße 8 A-1040 Wien Austria

ISBN: (纸本)1595933743

Tree parsing as supported by code generator generators like BEG, burg, iburg, lburg and ml-burg is a popular instruction selection method. There are two existing approaches for implementing tree parsing: dynamic programming, and tree-parsing automata;each approach has its advantages and disadvantages. We propose a new implementation approach that combines the advantages of both existing approaches: we start out with dynamic programming at compile time, but at every step we generate a state for a tree-parsing automaton, which is used the next time a tree matching the state is found, turning the instruction selector into a fast tree-parsing automaton. We have implemented this approach in the Gforth code generator. The implementation required little effort and reduced the startup time of Gforth by up to a factor of 2.5. Copyright © 2006 acm.

关键词： Automatic programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：