This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input-output examples to prune...
详细信息
ISBN:
(纸本)9781450334686
This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input-output examples to prune the search space. The algorithm uses refinement trees, a data structure that succinctly represents constraints on the shape of generated code. We evaluate the algorithm by using a prototype implementation to synthesize more than 40 benchmarks and several non-trivial larger examples. Our results demonstrate that the approach meets or outperforms the state-of-the-art for this domain, in terms of synthesis time or attainable size of the generated programs.
This paper presents a simple, powerful and flexible technique for reasoning about and translating the goal-directed evaluation of programminglanguage constructs that either succeed (and generate sequences of values) ...
详细信息
This paper presents a simple, powerful and flexible technique for reasoning about and translating the goal-directed evaluation of programminglanguage constructs that either succeed (and generate sequences of values) or fail. The technique generalizes the Byrd Box, a well-known device for describing Prolog backtracking.
Contemporary compiler systems such as GCC,. NET, and LLVM incorporate profile-guided optimizations (PGOs) on low-level intermediate code and basic blocks, with impressive results over purely static heuristics. Recent ...
详细信息
ISBN:
(纸本)9781450334686
Contemporary compiler systems such as GCC,. NET, and LLVM incorporate profile-guided optimizations (PGOs) on low-level intermediate code and basic blocks, with impressive results over purely static heuristics. Recent work shows that profile information is also useful for performing source-to-source optimizations via meta-programming. For example, using profiling information to inform decisions about data structures and algorithms can potentially lead to asymptotic improvements in performance. We present a design for profile-guided meta-programming in a general-purpose meta-programming system. Our design is parametric over the particular profiler and meta-programming system. We implement this design in two different meta-programming systems-the syntactic extensions systems of Chez Scheme and Racket- and provide several profile-guided meta-programs as usability case studies.
Computer designs are shifting from 32-bit architectures to 64-bit architectures, while most of the programs available today are still designed for 32-bit architectures, Java(TM), for example, specifies the frequently ...
详细信息
ISBN:
(纸本)9781581134636
Computer designs are shifting from 32-bit architectures to 64-bit architectures, while most of the programs available today are still designed for 32-bit architectures, Java(TM), for example, specifies the frequently used "int" as a 32-bit data type. If such Java programs are executed on a 64-bit architecture, many 32-bit values must be sign-extended to 64-bit values for integer operations. This causes serious performance overhead. In this paper, we present a fast and effective algorithm for eliminating sign extensions. We implemented this algorithm in the IBM Java Just-in-Time (JIT) compiler for IA-64(TM). Our experimental results show that our algorithm effectively eliminates the majority of sign extensions, They also show that it significantly improves performance, while it increases JIT compilation time by only 0.11%. We implemented our algorithm for programs in Java, but it can be applied to any language requiring sign extensions.
This paper presents the techniques used for the compilation of the data-flow, synchronous language SIGNAL. The key feature of the compiler is that it performs formal calculus on systems of boolean equations. The origi...
详细信息
We develop Propane/AT, a system to synthesize provablycorrect BGP (border gateway protocol) configurations for large, evolving networks from high-level specifications of topology, routing policy, and fault-tolerance r...
详细信息
ISBN:
(纸本)9781450349888
We develop Propane/AT, a system to synthesize provablycorrect BGP (border gateway protocol) configurations for large, evolving networks from high-level specifications of topology, routing policy, and fault-tolerance requirements. Propane/AT is based on new abstractions for capturing parameterized network topologies and their evolution, and algorithms to analyze the impact of topology and routing policy on fault tolerance. Our algorithms operate entirely on abstract topologies. We prove that the properties established by our analyses hold for every concrete instantiation of the given abstract topology. Propane/AT also guarantees that only incremental changes to existing device configurations are required when the network evolves to add or remove devices and links. Our experiments with real-world topologies and policies show that our abstractions and algorithms are effective, and that, for large networks, Propane/AT synthesizes configurations two orders of magnitude faster than systems that operate on concrete topologies.
There is an increasing interest in extensible languages, (domain-specific) language extensions, and mechanisms for their specification and implementation. One challenge is to develop tools that allow non-expert progra...
详细信息
ISBN:
(纸本)9781605583921
There is an increasing interest in extensible languages, (domain-specific) language extensions, and mechanisms for their specification and implementation. One challenge is to develop tools that allow non-expert programmers to add an eclectic set of language extensions to a host language. We describe mechanisms for composing and analyzing concrete syntax specifications of a host language and extensions to it. These specifications consist of context-free grammars with each terminal symbol mapped to a regular expression, from which a slightly-modified LR parser and context-aware scanner are generated. Traditionally, conflicts are detected when a parser is generated from the composed grammar, but this comes too late since it is the non-expert programmer directing the composition of independently developed extensions with the host language. The primary contribution of this paper is a modular analysis that is performed independently by each extension designer on her extension ( composed alone with the host language). If each extension passes this modular analysis, then the language composed later by the programmer will compile with no conflicts or lexical ambiguities. Thus, extension writers can verify that their extension will safely compose with others and, if not, fix the specification so that it will. This is possible due to the context-aware scanner's lexical disambiguation and a set of reasonable restrictions limiting the constructs that can be introduced by an extension. The restrictions ensure that the parse table states can be partitioned so that each state can be attributed to the host language or a single extension.
The proceedings contains 35 papers from the proceedings of the 2004 acmsigplanconference on programminglanguagedesign and implementation (PLDI'04). Topics discussed include: effective stream-based and executio...
详细信息
The proceedings contains 35 papers from the proceedings of the 2004 acmsigplanconference on programminglanguagedesign and implementation (PLDI'04). Topics discussed include: effective stream-based and execution-based data prefetching;enhancing data cache reliability by the addition of a small fully-associative replication cache;inter-reference gap distribution replacement: an improved replacement algorithm for set-associative caches;parallel algorithms for mining frequent structural motifs in scientific data;and impact of far-field interactions on performance of multipole-based preconditioners for sparse linear systems.
Many macro systems, especially for Lisp and Scheme, allow macro transformers to perform general computation. Moreover, the language for implementing compile-time macro transformers is usually the same as the language ...
详细信息
Many macro systems, especially for Lisp and Scheme, allow macro transformers to perform general computation. Moreover, the language for implementing compile-time macro transformers is usually the same as the language for implementing run-time functions. As a side effect of this sharing, implementations tend to allow the mingling of compile-time values and rum-time values, as well as values from separate compilations. Such mingling breaks programming tools that must parse code without executing it. Macro implementors avoid harmful mingling by obeying certain macro-definition protocols and by inserting phase-distinguishing annotations into the code. However, the annotations are fragile, the protocols are not enforced, and programmers can only reason about the result in terms of the compiler's implementation. MzScheme-the language of the PLT Scheme tool suite-addresses the problem through a macro system that separates compilation without sacrificing the expressiveness of macros.
Graphical user interfaces (GUIs) mediate many of our interactions with computers. Functional Reactive programming (FRP) is a promising approach to GUI design, providing high-level, declarative, compositional abstracti...
详细信息
ISBN:
(纸本)9781450320146
Graphical user interfaces (GUIs) mediate many of our interactions with computers. Functional Reactive programming (FRP) is a promising approach to GUI design, providing high-level, declarative, compositional abstractions to describe user interactions and time-dependent computations. We present Elm, a practical FRP language focused on easy creation of responsive GUIs. Elm has two major features: simple declarative support for Asynchronous FRP;and purely functional graphical layout. Asynchronous FRP allows the programmer to specify when the global ordering of event processing can be violated, and thus enables efficient concurrent execution of FRP programs;long-running computation can be executed asynchronously and not adversely affect the responsiveness of the user interface. Layout in Elm is achieved using a purely functional declarative framework that makes it simple to create and combine text, images, and video into rich multimedia displays. Together, Elm's two major features simplify the complicated task of creating responsive and usable GUIs.
暂无评论