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

programming with Enumerable Sets of Structures

acm sigplan NOTICES 2015年第10期50卷 37-56页

作者： Kuraj, Ivan Kuncak, Viktor Jackson, Daniel MIT CSAIL Cambridge MA 02139 USA Ecole Polytech Fed Lausanne Lausanne Switzerland

We present an efficient, modular, and feature-rich framework for automated generation and validation of complex structures, suitable for tasks that explore a large space of structured values. Our framework is capable of exhaustive, incremental, parallel, and memoized enumeration from not only finite but also infinite domains, while providing fine-grained control over the process. Furthermore, the framework efficiently supports the inverse of enumeration (checking whether a structure can be generated and fast-forwarding to this structure to continue the enumeration) and lazy enumeration (achieving exhaustive testing without generating all structures). The foundation of efficient enumeration lies in both direct access to encoded structures, achieved with well-known and new pairing functions, and dependent enumeration, which embeds constraints into the enumeration to avoid backtracking. Our framework defines an algebra of enumerators, with combinators for their composition that preserve exhaustiveness and efficiency. We have implemented our framework as a domain-specific language in Scala. Our experiments demonstrate better performance and shorter specifications by up to a few orders of magnitude compared to existing approaches.

关键词： Algorithms languages Verification Dependent enumeration data generation invariant pairing function algebra exhaustive testing random testing lazy evaluation program inversion DSL SciFe

来源：评论

学校读者我要写书评

暂无评论

Automating Grammar Comparison

引用

acm sigplan NOTICES 2015年第10期50卷 183-200页

作者： Madhavan, Ravichandhran Mayer, Mikael Gulwani, Sumit Kuncak, Viktor Ecole Polytech Fed Lausanne Lausanne Switzerland Microsoft Res Redmond WA USA

We consider from a practical perspective the problem of checking equivalence of context-free grammars. We present techniques for proving equivalence, as well as techniques for finding counter-examples that establish non-equivalence. Among the key building blocks of our approach is a novel algorithm for efficiently enumerating and sampling words and parse trees from arbitrary context-free grammars;the algorithm supports polynomial time random access to words belonging to the grammar. Furthermore, we propose an algorithm for proving equivalence of context-free grammars that is complete for LL grammars, yet can be invoked on any context-free grammar, including ambiguous grammars. Our techniques successfully find discrepancies between different syntax specifications of several real-world languages, and are capable of detecting fine-grained incremental modifications performed on grammars. Our evaluation shows that our tool improves significantly on the existing available state of the art tools. In addition, we used these algorithms to develop an online tutoring system for grammars that we then used in an undergraduate course on computer language processing. On questions involving grammar constructions, our system was able to automatically evaluate the correctness of 95% of the solutions submitted by students: it disproved 74% of cases and proved 21% of them.

关键词： languages Theory Verification Context-free grammars equivalence counter-examples proof system tutoring system

来源：评论

学校读者我要写书评

暂无评论

Use at Your Own Risk: The Java Unsafe API in the Wild

引用

acm sigplan NOTICES 2015年第10期50卷 695-710页

作者： Mastrangelo, Luis Ponzanelli, Luca Mocci, Andrea Lanza, Michele Hauswirth, Matthias Nystrom, Nathaniel USI Fac Informat Lugano Switzerland

Java is a safe language. Its runtime environment provides strong safety guarantees that any Java application can rely on. Or so we think. We show that the runtime actually does not provide these guarantees-for a large fraction of today's Java code. Unbeknownst to many application developers, the Java runtime includes a "backdoor" that allows expert library and framework developers to circumvent Java's safety guarantees. This backdoor is there by design, and is well known to experts, as it enables them to write high-performance "systems-level" code in Java. For much the same reasons that safe languages are preferred over unsafe languages, these powerful-but unsafe-capabilities in Java should be restricted. They should be made safe by changing the language, the runtime system, or the libraries. At the very least, their use should be restricted. This paper is a step in that direction. We analyzed 74 GB of compiled Java code, spread over 86, 479 Java archives, to determine how Java's unsafe capabilities are used in real-world libraries and applications. We found that 25% of Java bytecode archives depend on unsafe third-party Java code, and thus Java's safety guarantees cannot be trusted. We identify 14 different usage patterns of Java's unsafe capabilities, and we provide supporting evidence for why real-world code needs these capabilities. Our long-term goal is to provide a foundation for the design of new language features to regain safety in Java.

关键词： Design languages Measurement unsafe patterns mining Java Maven Central Stack Overflow

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Runtime Pointer Disambiguation

引用

acm sigplan NOTICES 2015年第10期50卷 589-606页

作者： Alves, Pericles Gruber, Fabian Doerfert, Johannes Lamprineas, Alexandros Grosser, Tobias Rastello, Fabrice Quintao Pereira, Fernando Magno Univ Fed Minas Gerais Belo Horizonte MG Brazil INRIA Paris France Univ Saarland D-66123 Saarbrucken Germany Swiss Fed Inst Technol Dep Comp Sci Zurich Switzerland

To optimize code effectively, compilers must deal with memory dependencies. However, the state-of-the-art heuristics available in the literature to track memory dependencies are inherently imprecise and computationally expensive. Consequently, the most advanced code transformations that compilers have today are ineffective when applied on real-world programs. The goal of this paper is to solve this conundrum through dynamic disambiguation of pointers. We provide different ways to determine at runtime when two memory locations can overlap. We then produce two versions of a code region: one that is aliasing-free - hence, easy to optimize - and another that is not. Our checks let us safely branch to the optimizable region. We have applied these ideas on Polly-LLVM, a loop optimizer built on top of the LLVM compilation infrastructure. Our experiments indicate that our method is precise, effective and useful: we can disambiguate every pair of pointer in the loop intensive PolyBench benchmark suite. The result of this precision is code quality: the binaries we generate are 10% faster than those that Polly-LLVM produces without our optimization, at the -O3 optimization level of LLVM.

关键词： languages Performance Experimentation Alias analysis dynamic guards optimization

来源：评论

学校读者我要写书评

暂无评论

Synthesis of Layout Engines from Relational Constraints

引用

acm sigplan NOTICES 2015年第10期50卷 74-88页

作者： Hottelier, Thibaud Bodik, Rastislav Univ Calif Berkeley Berkeley CA 94720 USA Univ Washington Seattle WA 98195 USA

We present an algorithm for synthesizing efficient document layout engines from compact relational specifications. These specifications are compact in that a single specification can produce multiple engines, each for a distinct layout situation, i.e., a different combination of known vs. unknown attributes. Technically, our specifications are relational attribute grammars, while our engines are functional attribute grammars. By synthesizing functions from relational constraints, we obviate the need for constraint solving at runtime, because functional attribute grammars can be easily evaluated according to a fixed schedule, sidestepping the backtracking search performed by constraint solvers. Our experiments show that we can generate layout engines for non-trivial data visualizations, and that our synthesized engines are between 39- and 200-times faster than general-purpose constraint solvers. Relational specifications of layout give rise to synthesis problems that have previously proved intractable. Our algorithm exploits the hierarchical, grammar-based structure of the specification, decomposing the specification into smaller subproblems, which can be tackled with off-the-shelf synthesis procedures. The new synthesis problem then becomes the composition of the functions thus generated into a correct attribute grammar, which might be recursive. We show how to solve this problem by efficient reduction to an SMT problem.

关键词： languages Algorithms Performance Program Synthesis Attribute Grammars Layout

来源：评论

学校读者我要写书评

暂无评论

Comparative Evaluation of the Stochastic Simplex Bisection Algorithm and the *** Module

Comparative Evaluation of the Stochastic Simplex Bisection A...

引用

3rd international conference on Innovative Network systems and Applications (iNetSApp) held in conjunction with Federated conference on Computer Science and Information systems (FedCSIS)

作者： Samuelsson, Christer German Res Ctr Artificial Intelligence Osnabruck Germany

ISBN: (纸本)9788360810668

The stochastic simplex bisection (SSB) algorithm is evaluated against the collection of optimizers in the Python *** module on a prominent test set. The SSB algorithm greatly outperforms all SciPy optimizers, save one, in exactly half the cases. It does slightly worse on quadratic functions, but excels at trigonometric ones, highlighting its multimodal prowess. Unlike the SciPy optimizers, it sustains a high success rate. The SciPy optimizers would benefit from a more informed metaheuristic strategy and the SSB algorithm would profit from quicker local convergence and better multidimensional capabilities. Conversely, the local convergence of the SciPy optimizers is impressive and the multimodal capabilities of the SSB algorithm in separable dimensions are uncanny.

关键词： convergence genetic algorithms mathematics computing object-oriented languages Python SciPy-optimize module SSB algorithm quadratic function stochastic simplex bisection algorithm Algorithm design and analysis Amplitude modulation Convergence Linear programming Optimization Partitioning algorithms Presses

来源：评论

学校读者我要写书评

暂无评论

Performance Problems You Can Fix: A Dynamic Analysis of Memoization Opportunities

引用

acm sigplan NOTICES 2015年第10期50卷 607-622页

作者： Della Toffola, Luca Pradel, Michael Gross, Thomas R. Swiss Fed Inst Technol Dept Comp Sci Zurich Switzerland Tech Univ Darmstadt Dept Comp Sci Darmstadt Germany

Performance bugs are a prevalent problem and recent research proposes various techniques to identify such bugs. This paper addresses a kind of performance problem that often is easy to address but difficult to identify: redundant computations that may be avoided by reusing already computed results for particular inputs, a technique called memoization. To help developers find and use memoization opportunities, we present MemoizeIt, a dynamic analysis that identifies methods that repeatedly perform the same computation. The key idea is to compare inputs and outputs of method calls in a scalable yet precise way. To avoid the overhead of comparing objects at all method invocations in detail, MemoizeIt first compares objects without following any references and iteratively increases the depth of exploration while shrinking the set of considered methods. After each iteration, the approach ignores methods that cannot benefit from memoization, allowing it to analyze calls to the remaining methods in more detail. For every memoization opportunity that MemoizeIt detects, it provides hints on how to implement memoization, making it easy for the developer to fix the performance issue. Applying MemoizeIt to eleven real-world Java programs reveals nine profitable memoization opportunities, most of which are missed by traditional CPU time profilers, conservative compiler optimizations, and other existing approaches for finding performance bugs. Adding memoization as proposed by MemoizeIt leads to statistically significant speedups by factors between 1.04x and 12.93x.

关键词： Algorithms Experimentation languages Performance Measurement Memoization caching profiling performance bugs

来源：评论

学校读者我要写书评

暂无评论

Remote-Scope Promotion: Clarified, Rectified, and Verified

引用

acm sigplan NOTICES 2015年第10期50卷 731-747页

作者： Wickerson, John Batty, Mark Beckmann, Bradford M. Donaldson, Alastair F. Univ London Imperial Coll Sci Technol & Med London SW7 2AZ England Univ Kent Canterbury CT2 7NZ Kent England Adv Micro Devices Inc Sunnyvale CA 94088 USA

Modern accelerator programming frameworks, such as OpenCL (TM), organise threads into work-groups. Remote-scope promotion (RSP) is a language extension recently proposed by AMD researchers that is designed to enable applications, for the first time, both to optimise for the common case of intra-work-group communication (using memory scopes to provide consistency only within a work-group) and to allow occasional inter-work-group communication (as required, for instance, to support the popular load-balancing idiom of work stealing). We present the first formal, axiomatic memory model of OpenCL extended with RSP. We have extended the HERD memory model simulator with support for OpenCL kernels that exploit RSP, and used it to discover bugs in several litmus tests and a work-stealing queue, that have been used previously in the study of RSP. We have also formalised the proposed GPU implementation of RSP. The formalisation process allowed us to identify bugs in the description of RSP that could result in well-synchronised programs experiencing memory inconsistencies. We present and prove sound a new implementation of RSP that incorporates bug fixes and requires less non-standard hardware than the original implementation. This work, a collaboration between academia and industry, clearly demonstrates how, when designing hardware support for a new concurrent language feature, the early application of formal tools and techniques can help to prevent errors, such as those we have found, from making it into silicon.

关键词： Formal methods graphics processing unit (GPU) Isabelle OpenCL programming language implementation weak memory models work stealing

来源：评论

学校读者我要写书评

暂无评论

From object Algebras to Attribute Grammars 14

From Object Algebras to Attribute Grammars

引用

2014 acm international conference on object-oriented-programming-systems-languages-and-Applications (OOPSLA 14)

作者： Rendel, Tillmann Brachthaeuser, Jonathan Immanuel Ostermann, Klaus Univ Marburg D-35032 Marburg Germany

ISBN: (纸本)9781450325851

Oliveira and Cook (2012) and Oliveira et al. (2013) have recently introduced object algebras as a program structuring technique to improve the modularity and extensibility of programs. We analyze the relationship between object algebras and attribute grammars (AGs), a formalism to augment context-free grammars with attributes. We present an extension of the object algebra technique with which the full class of L-attributed grammars - an important class of AGs that corresponds to one-pass compilers - can be encoded in Scala. The encoding is modular (attributes can be defined and type-checked separately), scalable (the size of the encoding is linear in the size of the AG specification) and compositional (each AG artifact is represented as a semantic object of the host language). To evaluate these claims, we have formalized the encoding and re-implemented a one-pass compiler for a subset of C with our technique. We also discuss how advanced features of modern AG systems, such as higher-order and parameterized attributes, reference attributes, and forwarding can be supported.

关键词： object Algebras Visitor Pattern Attribute Grammars Church-encoding Embedded Domain-Specific languages Modularity One-Pass Compilers Scala

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：