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

Computing Repair Alternatives for Malformed Programs using Constraint Attribute Grammars

ACM SIGPLAN NOTICES 2016年第10期51卷 711-730页

作者： Steimann, Friedrich Hagemann, Joerg Ulke, Bastian Fernuniv Lehrgebiet Programmiersyst Hagen Germany

Attribute grammars decorate the nodes of a program's parse tree with attributes whose values are defined by equations encoding the (static) semantics of a programming language. We show how replacing the equations of an attribute grammar with equivalent constraints that can be solved by a constraint solver allows us to compute repairs of a malformed program solely from a specification that was originally designed for checking its well-formedness. We present two repair modes - shallow and deep fixing - whose computed repair alternatives are guaranteed to repair every error on which they are invoked. While shallow fixing may introduce new errors, deep fixing never does;to make it tractable, we implement it using neighborhood search. We demonstrate the feasibility of our approach by implementing it on top of ExtendJ, an attribute grammar based Java compiler, and by applying it to an example from the Java EE context, detecting and fixing well-formedness errors (both real and injected) in a body of 14 open-source subject programs.

关键词： attribute grammars constraints repair languages Algorithms

来源：评论

学校读者我要写书评

暂无评论

Type Inference for Static Compilation of JavaScript

引用

ACM SIGPLAN NOTICES 2016年第10期51卷 410-429页

作者： Chandra, Satish Gordon, Colin S. Jeannin, Jean-Baptiste Schlesinger, Cole Sridharan, Manu Tip, Frank Choi, Youngil Samsung Res Amer Mountain View CA 94043 USA Drexel Univ Philadelphia PA 19104 USA Northeastern Univ Boston MA 02115 USA Samsung Elect Suwon South Korea

We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is expressive enough to accommodate several standard benchmarks with only minor workarounds. The invariants enforced by the types enable an ahead-of-time compiler to carry out optimizations typically beyond the reach of static compilers for dynamic languages. Unlike previous inference techniques for prototype inheritance, our algorithm uses a combination of lower and upper bound propagation to infer types and discover type errors in all code, including uninvoked functions. The inference is expressed in a simple constraint language, designed to leverage off-the-shelf fixed point solvers. We prove soundness for both the type system and inference algorithm. An experimental evaluation showed that the inference is powerful, handling the aforementioned benchmarks with no manual type annotation, and that the inferred types enable effective static compilation.

关键词： object-oriented type systems type inference JavaScript

来源：评论

学校读者我要写书评

暂无评论

Semantics-Based Program Verifiers for All languages

引用

ACM SIGPLAN NOTICES 2016年第10期51卷 74-91页

作者： Stefanescu, Andrei Park, Daejun Yuwen, Shijiao Li, Yilong Rosu, Grigore Univ Illinois Urbana IL 61801 USA Runtime Verificat Inc Urbana IL USA

We present a language-independent verification framework that can be instantiated with an operational semantics to automatically generate a program verifier. The framework treats both the operational semantics and the program correctness specifications as reachability rules between matching logic patterns, and uses the sound and relatively complete reachability logic proof system to prove the specifications using the semantics. We instantiate the framework with the semantics of one academic language, KERNELC, as well as with three recent semantics of real-world languages, C, JAVA, and JAVASCRIPT, developed independently of our verification infrastructure. We evaluate our approach empirically and show that the generated program verifiers can check automatically the full functional correctness of challenging heap-manipulating programs implementing operations on list and tree data structures, like AVL trees. This is the first approach that can turn the operational semantics of real-world languages into correct-by-construction automatic verifiers.

关键词： reachability logic matching logic K framework languages Theory Verification

来源：评论

学校读者我要写书评

暂无评论

A Compiler for Throughput Optimization of Graph Algorithms on GPUs

引用

ACM SIGPLAN NOTICES 2016年第10期51卷 1-19页

作者： Pai, Sreepathi Pingali, Keshav Univ Texas Austin Austin TX 78712 USA

Writing high-performance GPU implementations of graph algorithms can be challenging. In this paper, we argue that three optimizations called throughput optimizations are key to high-performance for this application class. These optimizations describe a large implementation space making it unrealistic for programmers to implement them by hand. To address this problem, we have implemented these optimizations in a compiler that produces CUDA code from an intermediate-level program representation called IrGL. Compared to state-of-the-art handwritten CUDA implementations of eight graph applications, code generated by the IrGL compiler is up to 5.95x times faster (median 1.4x) for five applications and never more than 30% slower for the others. Throughput optimizations contribute an improvement up to 4.16x (median 1.4x) to the performance of unoptimized IrGL code.

关键词： Graph applications amorphous data-parallelism GPUs compilers optimization throughput

来源：评论

学校读者我要写书评

暂无评论

Modeling and Analysis of Remote Memory Access programming

引用

ACM SIGPLAN NOTICES 2016年第10期51卷 129-144页

作者： Dan, Andrei Marian Lam, Patrick Hoefler, Torsten Vechev, Martin Swiss Fed Inst Technol Zurich Switzerland Univ Waterloo Waterloo ON N2L 3G1 Canada

Recent advances in networking hardware have led to a new generation of Remote Memory Access (RMA) networks in which processors from different machines can communicate directly, bypassing the operating system and allowing higher performance. Researchers and practitioners have proposed libraries and programming models for RMA to enable the development of applications running on these networks, However, the memory models implied by these RMA libraries and languages are often loosely specified, poorly understood, and differ depending on the underlying network architecture and other factors. Hence, it is difficult to precisely reason about the semantics of RMA programs or how changes in the network architecture affect them. We address this problem with the following contributions: (i) a coreRMA language which serves as a common foundation, formalizing the essential characteristics of RMA programming;(ii) complete axiomatic semantics for that language;(iii) integration of our semantics with an existing constraint solver, enabling us to exhaustively generate coreRMA programs (litmus tests) up to a specified bound and check whether the tests satisfy their specification;and (iv) extensive validation of our semantics on real-world RMA systems. We generated and ran 7,441 litmus tests using each of the low-level RMA network APIs: DMAPP, VPI Verbs, and Portals 4. Our results confirmed that our model successfully captures behaviors exhibited by these networks. Moreover, we found RMA programs that behave inconsistently with existing documentation, confirmed by network experts. Our work provides an important step towards understanding existing RMA networks, thus influencing the design of future RMA interfaces and hardware.

关键词： Memory Model

来源：评论

学校读者我要写书评

暂无评论

The Chemical Approach to Typestate-oriented programming 2015

The Chemical Approach to Typestate-Oriented Programming

引用

ACM SIGPLAN International conference on object-oriented programming, systems, languages, and applications (oopsla)

作者： Crafa, Silvia Padovani, Luca Univ Padua I-35100 Padua Italy Univ Turin I-10124 Turin Italy

ISBN: (纸本)9781450336895

We study a novel approach to typestate-oriented programming based on the chemical metaphor: state and operations on objects are molecules of messages and state transformations are chemical reactions. This approach allows us to investigate typestate in an inherently concurrent setting, whereby objects can be accessed and modified concurrently by several processes, each potentially changing only part of their state. We introduce a simple behavioral type theory to express in a uniform way both the private and the public interfaces of objects, to describe and enforce structured object protocols consisting of possibilities, prohibitions, and obligations, and to control object sharing.

关键词： Typestate concurrency behavioral types join calculus

来源：评论

学校读者我要写书评

暂无评论

Gentrification Gone too Far? Affordable 2nd-Class Values for Fun and (Co-)Effect

引用

ACM SIGPLAN NOTICES 2016年第10期51卷 234-251页

作者： Osvald, Leo Essertel, Gregory Wu, Xilun Gonzalez-Alayon, Lilliam I. Rompf, Tiark Purdue Univ W Lafayette IN 47907 USA

First-class functions dramatically increase expressiveness, at the expense of static guarantees. In ALGOL or PASCAL, functions could be passed as arguments but never escape their defining scope. Therefore, function arguments could serve as temporary access tokens or capabilities, enabling callees to perform some action, but only for the duration of the call. In modern languages, such programming patterns are no longer available. The central thrust of this paper is to re-introduce second-class functions and other values alongside first-class entities in modern languages. We formalize second-class values with stack-bounded lifetimes as an extension to simply-typed lambda calculus, and for richer type systems such as F-<: and systems with path-dependent types. We generalize the binary first-vs second-class distinction to arbitrary privilege lattices, with the underlying type lattice as a special case. In this setting, abstract types naturally enable privilege parametricity. We prove type soundness and lifetime properties in Coq. We implement our system as an extension of Scala, and present several case studies. First, we modify the Scala Collections library and add privilege annotations to all higher-order functions. Privilege parametricity is key to retain the high degree of code-reuse between sequential and parallel as well as lazy and eager collections. Second, we use scoped capabilities to introduce a model of checked exceptions in the Scala library, with only few changes to the code. Third, we employ second-class capabilities for memory safety in a region-based off-heap memory library.

关键词： first-class second-class types effects capabilities object lifetimes

来源：评论

学校读者我要写书评

暂无评论

Ringer: Web Automation by Demonstration

引用

ACM SIGPLAN NOTICES 2016年第10期51卷 748-764页

作者： Barman, Shaon Chasins, Sarah Bodik, Rastislav Gulwani, Sumit Univ Calif Berkeley Berkeley CA 94720 USA Univ Washington Seattle WA 98195 USA Microsoft Res Cambridge MA USA

With increasing amounts of data available on the web and a diverse range of users interested in programmatically accessing that data, web automation must become easier. Automation helps users complete many tedious interactions, such as scraping data, completing forms, or transferring data between websites. However, writing web automation scripts typically requires an expert programmer because the writer must be able to reverse engineer the target webpage. We have built a record and replay tool, Ringer, that makes web automation accessible to non-coders. Ringer takes a user demonstration as input and creates a script that interacts with the page as a user would. This approach makes Ringer scripts more robust to webpage changes because user-facing interfaces remain relatively stable compared to the underlying webpage implementations. We evaluated our approach on benchmarks recorded on real webpages and found that it replayed 4x more benchmarks than a state-of-the-art replay tool.

关键词： Record-Replay Automation Javascript Browser Design languages

来源：评论

学校读者我要写书评

暂无评论

Incremental Forest: A DSL for Efficiently Managing Filestores

引用

ACM SIGPLAN NOTICES 2016年第10期51卷 252-271页

作者： DiLorenzo, Jonathan Zhang, Richard Menzies, Erin Fisher, Kathleen Foster, Nate Cornell Univ Ithaca NY 14853 USA Univ Penn Philadelphia PA 19104 USA Tufts Univ Medford MA 02155 USA

File systems are often used to store persistent application data, but manipulating file systems using standard APIs can be difficult for programmers. Forest is a domain-specific language that bridges the gap between the on-disk and in-memory representations of file system data. Given a high-level specification of the structure, contents, and properties of a collection of directories, files, and symbolic links, the Forest compiler generates tools for loading, storing, and validating that data. Unfortunately, the initial implementation of Forest offered few mechanisms for controlling cost-e.g., the run-time system could load gigabytes of data, even if only a few bytes were needed. This paper introduces Incremental Forest (iForest), an extension to Forest with an explicit delay construct that programmers can use to precisely control costs. We describe the design of iForest using a series of running examples, present a formal semantics in a core calculus, and define a simple cost model that accurately characterizes the resources needed to use a given specification. We propose skins, which allow programmers to modify the delay structure of a specification in a compositional way, and develop a static type system for ensuring compatibility between specifications and skins. We prove the soundness and completeness of the type system and a variety of algebraic properties of skins. We describe an OCaml implementation and evaluate its performance on applications developed in collaboration with watershed hydrologists.

关键词： Data description languages file systems file-stores domain-specific languages ad hoc data laziness

来源：评论

学校读者我要写书评

暂无评论

Call Graphs for languages with Parametric Polymorphism

引用

ACM SIGPLAN NOTICES 2016年第10期51卷 394-409页

作者： Petrashko, Dmitry Ureche, Vlad Lhotak, Ondrej Odersky, Martin Ecole Polytech Fed Lausanne Lausanne Switzerland Univ Waterloo Waterloo ON N2L 3G1 Canada

The performance of contemporary object oriented languages depends on optimizations such as devirtualization, inlining, and specialization, and these in turn depend on precise call graph analysis. Existing call graph analyses do not take advantage of the information provided by the rich type systems of contemporary languages, in particular generic type arguments. Many existing approaches analyze Java bytecode, in which generic types have been erased. This paper shows that this discarded information is actually very useful as the context in a context- sensitive analysis, where it significantly improves precision and keeps the running time small. Specifically, we propose and evaluate call graph construction algorithms in which the contexts of a method are (i) the type arguments passed to its type parameters, and (ii) the static types of the arguments passed to its term parameters. The use of static types from the caller as context is effective because it allows more precise dispatch of call sites inside the callee. Our evaluation indicates that the average number of contexts required per method is small. We implement the analysis in the Dotty compiler for Scala, and evaluate it on programs that use the type- parametric Scala collections library and on the Dotty compiler itself. The context- sensitive analysis runs 1.4x faster than a context- insensitive one and discovers 20% more monomorphic call sites at the same time. When applied to method specialization, the imprecision in a context- insensitive call graph would require the average method to be cloned 22 times, whereas the context-sensitive call graph indicates a much more practical 1.00 to 1.50 clones per method. We applied the proposed analysis to automatically specialize generic methods. The resulting automatic transformation achieves the same performance as state-of-the-art techniques requiring manual annotations, while reducing the size of the generated bytecode by up to 5x.

关键词： call graphs parametric polymorphism static analysis specialization

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：