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

Adding delimited and composable control to a production programming environment

acm sigplan NOTICES 2007年第9期42卷 165-176页

作者： Flatt, Matthew Yu, Gang Findler, Robert Bruce Felleisen, Matthias Univ Utah Salt Lake City UT 84112 USA Chinese Acad Sci Inst Software Beijing 100864 Peoples R China Univ Chicago Chicago IL 60637 USA Northeastern Univ Boston MA 02115 USA

Operators for delimiting control and for capturing composable continuations litter the landscape of theoretical programming language research. Numerous papers explain their advantages, how the operators explain each other (or don't), and other aspects of the operators' existence. Production programming languages, however, do not support these operators, partly because their relationship to existing and demonstrably useful constructs-such as exceptions and dynamic binding-remains relatively unexplored. In this paper, we report on our effort of translating the theory of delimited and composable control into a viable implementation for a production system. The report shows how this effort involved a substantial design element, including work with a formal model, as well as significant practical exploration and engineering. The resulting version of PLT Scheme incorporates the expressive combination of delimited and composable control alongside dynamic-wind, dynamic binding, and exception handling. None of the additional operators subvert the intended benefits of existing control operators, so that programmers can freely mix and match control operators.

关键词： design languages

来源：评论

学校读者我要写书评

暂无评论

A certified type-preserving compiler from lambda calculus to assembly language

引用

acm sigplan NOTICES 2007年第6期42卷 54-65页

作者： Chlipala, Adam Univ Calif Berkeley Berkeley CA 94720 USA

We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. We demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge large parts of our proof obligations automatically.

关键词： languages verification compiler verification interactive proof assistants dependent types denotational semantics

来源：评论

学校读者我要写书评

暂无评论

Mace: language support for building distributed systems

引用

acm sigplan NOTICES 2007年第6期42卷 179-188页

作者： Killian, Charles Anderson, James W. Braud, Ryan Jhala, Ranjit Vahdat, Amin Univ Calif San Diego La Jolla CA 92093 USA

Building distributed systems is particularly difficult because of the asynchronous, heterogeneous, and failure-prone environment where these systems must run. Tools for building distributed systems must strike a compromise between reducing programmer effort and increasing system efficiency. We present Mace, a C++ language extension and source-to-source compiler that translates a concise but expressive distributed system specification into a C++ implementation. Mace overcomes the limitations of low-level languages by providing a unified framework for networking and event handling, and the limitations of high-level languages by allowing programmers to write program components in a controlled and structured manner in C++. By imposing structure and restrictions on how applications can be written, Mace supports debugging at a higher level, including support for efficient model checking and causal-path debugging. Because Mace programs compile to C++, programmers can use existing C++ tools, including optimizers, profilers, and debuggers to analyze their systems.

关键词： languages reliability performance Mace domain specific languages model checking debugging distributed systems concurrency event driven programming

来源：评论

学校读者我要写书评

暂无评论

Thread-modular shape analysis

引用

acm sigplan NOTICES 2007年第6期42卷 266-277页

作者： Gotsman, Alexey Berdine, Josh Cook, Byron Sagiv, Mooly Univ Cambridge Cambridge CB2 1TN England Microsoft Corp Redmond WA 98052 USA

We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource invariant associated with each lock that describes the part of the heap protected by the lock. This allows us to use a sequential shape analysis on each thread. We show that resource invariants of a certain class can be characterized as least fixed points and computed via repeated applications of shape analysis only on each individual thread. Based on this approach, we have implemented a thread-modular shape analysis tool and applied it to concurrent heap-manipulating code from Windows device drivers.

关键词： abstract interpretation concurrent programming shape analysis static analysis

来源：评论

学校读者我要写书评

暂无评论

The JastAdd Extensible Java Compiler

引用

acm sigplan NOTICES 2007年第10期42卷 1-17页

作者： Ekman, Torbjorn Hedin, Gorel Univ Oxford Programming Tools Grp Oxford England Lund Univ Dept Comp Sci S-22100 Lund Sweden

The JastAdd Extensible Java Compiler is a high quality Java compiler that is easy to extend in order to build static analysis tools for Java, and to extend Java with new language constructs. It is built modularly, with a Java 1.4 compiler that is extended to a Java 5 compiler. Example applications that are built as extensions include an alternative backend that generates Jimple, an extension of Java with AspectJ constructs, and the implementation of a pluggable type system for non-null checking and inference. The system is implemented using JastAdd, a declarative Java-like language. We describe the compiler architecture, the major design ideas for building and extending the compiler, in particular, for dealing with complex extensions that affect name and type analysis. Our extensible compiler compares very favorably concerning quality, speed and size with other extensible Java compiler frameworks. It also compares favorably in quality and size compared with traditional non-extensible Java compilers, and it runs within a factor of three compared to javac.

关键词： design languages OOP compilers extensibility declarative frameworks modularity Java

来源：评论

学校读者我要写书评

暂无评论

Automatic inversion generates divide-and-conquer parallel programs

引用

acm sigplan NOTICES 2007年第6期42卷 146-155页

作者： Morita, Kazutaka Morihata, Akimasa Matsuzaki, Kiminori Hu, Zhenjiang Takeichi, Masato Univ Tokyo Grad Sch Informat Sci & Technol Tokyo Japan

Divide-and-conquer algorithms are suitable for modern parallel machines, tending to have large amounts of inherent parallelism and working well with caches and deep memory hierarchies. Among others, list homomorphisms are a class of recursive functions on lists, which match very well with the divide-and-conquer paradigm. However, direct programming with list homomorphisms is a challenge for many programmers. In this paper, we propose and implement a novel system that can automatically derive cost-optimal list homomorphisms from a pair of sequential programs, based on the third homomorphism theorem. Our idea is to reduce extraction of list homomorphisms to derivation of weak right inverses. We show that a weak right inverse always exists and can be automatically generated from a wide class of sequential programs. We demonstrate our system with several nontrivial examples, including the maximum prefix sum problem, the prefix sum computation, the maximum segment sum problem, and the line-of-sight problem. The experimental results show practical efficiency of our automatic parallelization algorithm and good speedups of the generated parallel programs.

关键词： algorithms design languages divide-and-conquer parallelism inversion program transformation third homomorphism theorem

来源：评论

学校读者我要写书评

暂无评论

Valgrind: A framework for heavyweight dynamic binary instrumentation

引用

acm sigplan NOTICES 2007年第6期42卷 89-100页

作者： Nethercote, Nicholas Seward, Julian Natl ICT Australia Melbourne Vic Australia OpenWorks LLP Cambridge England

Dynamic binary instrumentation (DBI) frameworks make it easy to build dynamic binary analysis (DBA) tools such as checkers and profilers. Much of the focus on DBI frameworks has been on performance;little attention has been paid to their capabilities. As a result, we believe the potential of DBI has not been fully exploited. In this paper we describe Valgrind, a DBI framework designed for building heavyweight DBA tools. We focus on its unique support for shadow values - a powerful but previously little-studied and difficult-to-implement DBA technique, which requires a tool to shadow every register and memory value with another value that describes it. This support accounts for several crucial design features that distinguish Valgrind from other DBI frameworks. Because of these features, lightweight tools built with Valgrind run comparatively slowly, but Valgrind can be used to build more interesting, heavyweight tools that are difficult or impossible to build with other DBI frameworks such as Pin and DynamoRIO.

关键词： design performance experimentation Valgrind Memcheck dynamic binary instrumentation dynamic binary analysis shadow values

来源：评论

学校读者我要写书评

暂无评论

The exo VM system for automatic VM and application reduction

引用

acm sigplan NOTICES 2007年第6期42卷 352-362页

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

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

来源：评论

学校读者我要写书评

暂无评论

iTasks: Executable specifications of interactive work flow systems for the web

引用

acm sigplan NOTICES 2007年第9期42卷 141-152页

作者： Plasmeijer, Rinus Achten, Peter Koopman, Pieter Radboud Univ Nijmegen Inst Comp & Informat Sci Software Technol Dept NL-6525 ED Nijmegen Netherlands

In this paper we introduce the iTask system: a set of combinators to specify work flows in a pure functional language at a very high level of abstraction. Work flow systems are automated systems in which tasks are coordinated that have to be executed by humans and computers. The combinators that we propose support work flow patterns commonly found in commercial work flow systems. Compared with most of these commercial systems, the iTask system offers several advantages: tasks are statically typed, tasks can be higher order, the combinators are fully compositional, dynamic and recursive work flows can be specified, and last but not least, the specification is used to generate an executable web-based multi-user work flow application. With the iTask system, useful work flows can be defined which cannot be expressed in other systems: work can be interrupted and subsequently directed to other workers for further processing. The implementation is special as well. It is based on the Clean iData toolkit which makes it possible to create fully dynamic, interactive, thin client web applications. Thanks to the generic programming techniques used in the iData toolkit, the programming effort is reduced significantly: state handling, form rendering, user interaction, and storage management is handled automatically. The iTask system allows a task to be regarded as a special kind of persistent redex being reduced by the application user via task completion. The combinators control the order in which these redexes are made available to the application user. The system rewrites the persistent task redexes in a similar way as functions are rewritten in lazy functional languages.

关键词： design languages clean iData iTask

来源：评论

学校读者我要写书评

暂无评论

Sketching stencils

引用

acm sigplan NOTICES 2007年第6期42卷 167-178页

作者： Solar-Lezama, Armando Arnold, Gilad Tancau, Liviu Bodik, Rastislav Saraswat, Vijay Seshia, Sanjit IBM Corp TJ Watson Res Ctr Armonk NY 10504 USA Univ Calif Berkeley Berkeley CA 94720 USA

Performance of stencil computations can be significantly improved through smart implementations that improve memory locality, computation reuse, or parallelize the computation. Unfortunately, efficient implementations are hard to obtain because they often involve non-traditional transformations, which means that they cannot be produced by optimizing the reference stencil with a compiler. In fact, many stencils are produced by code generators that were tediously handcrafted. In this paper, we show how stencil implementations can be produced with sketching. Sketching is a software synthesis approach where the programmer develops a partial implementation a sketch-and a separate specification of the desired functionality given by a reference (unoptimized) stencil. The synthesizer then completes the sketch to behave like the specification, filling in code fragments that are difficult to develop manually. Existing sketching systems work only for small finite programs, i.e., programs that can be represented as small Boolean circuits. In this paper, we develop a sketching synthesizer that works for stencil computations, a large class of programs that, unlike circuits, have unbounded inputs and outputs, as well as an unbounded number of computations. The key contribution is a reduction algorithm that turns a stencil into a circuit, allowing us to synthesize stencils using an existing sketching synthesizer.

关键词： languages design performance sketching stencil SAT

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：