1,205 papers · page 34 of 61
Determining aliases is one of the foundamental static analysis problems, in part because the precision with which this problem is solved can affect the precision of other analyses such as live variables, available expressions, and constant propagation. Previous work has investiga…
It has been attracting much attention to make use of list homomorphisms in parallel programming because they ideally suit the divide-and-conquer parallel paradigm. However, they have been usually treated rather informally and ad hoc in the development of efficient parallel progra…
Several compiler optimizations, such as data flow analysis, the exploitation of instruction-level parallelism (ILP), loop transformations, and memory disambiguation, require programs with reducible control flow graphs. However, not all programs satisfy this property. A new method…
We describe how binding-time, data-flow, and strictness analyses for languages with higher-order functions and algebraic data types can be obtained by instantiating a generic program logic and axiomatization of the properties analyzed for. A distinctive feature of the analyses is…
We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program can …
Instruction-level parallelism (ILP) in nonnumerical code is regarded as scarce and hard to exploit due to its irregularity. In this article, we introduce a new code-scheduling technique for irregular ILP called “selective scheduling” which can be used as a component for superscal…
The control dependence relation plays a fundamental role in program restructuring and optimization. The usual representation of this relation is the control dependence graph (CDG), but the size of the CDG can grow quadratically with the input programs, even for structured program…
The aspect of purity versus impurity that we address involves the absence versus presence of mutation: the use of primitives (RPLACA and RPLACD in Lisp, set-car! and set-cdr! in Scheme ) that change the state of pairs without creating new pairs.It is well known that cyclic list s…
We design a system with six Basic Combinators and prove that it is powerful enough to embed the full asynchronous π-calculus, including replication. Our theory for constructing Combinatory Versions of concurrent languages is based on a method, used by Quine and Bernays, for the g…
We present SLED, a specification language for Encoding and Decoding, which describes, abstract, binary, and assembly-language representations of machine instructions. Guided by a SLED specification, the New Jersey Machine-Code Toolkit generates bit-manipulating code for use in ap…
This article presents a new analysis technique, commutativity analysis, for automatically parallelizing computations that manipulate dynamic, pointer-based data structures. Commutativity analysis views the computation as composed of operations on objects. It then analyzes the pro…
Some of the most difficult questions to answer when designing a distributed application are related to mobility: what information to transfer between sites and when and how to transfer it. Network-transparent distribution, the property that a program's behavior is independent of …
One way to model a sound and complete translation from a source calculus into a target calculus is with an adjoint or a Galois connection . In the special case of a reflection , one also has that the target calculus is isomorphic to a subset of the source. We show that three wide…
We present the first source-level profiler for a compiled, nonstrict, higher-order, purely functional language capable of measuring time as well as space usage. Our profiler is implemented in a production-quality optimizing compiler for Haskell and can successfully profile large …
In this article, we present a new algorithm for incrementally maintaining the dominator tree of an arbitrary flowgraph.Previous work most relevant to this article includes only the Carroll-Ryder algorithm and the Ramalingam-Reps algorithm.Both these methods are restricted to redu…
We consider the problem of lightweight closure conversion, in which multiple procedure call protocols may coexist in the same code. A lightweight closure omits bindings for some of the free variables of the procedure that is represents. Flow analysis is used to match the protocol…
Although code transformations are routinely applied to improve the performance of programs for both scalar and parallel machines, the properties of code-improving transformations are not well understood. In this article we present a framework that enables the exploration, both an…
Asoft type systeminfers types for the procedures and data structures of dynamically typed programs. Like conventional static types, soft types express program invariants and thereby provide valuable information for program optimization and debugging. A soft typecheckeruses the ty…
In this article, we consider symbolic model checking for event-driven real-time systems.We first propose a Synchronous Real-Time Event Logic (SREL) for capturing the formal semantics of synchronous, event-driven real-time systems.The concrete syntax of these systems is given in t…
In this article we examine the augmentation of application interfaces with enhanced specifications that include sequencing constraints called protocols.Protocols make explicit the relationship between messages (methods) supported by the application.These relationships are usually…