title: Detecting Pipeline Structural Hazards Quickly

authors:
Todd A. Proebsting
Christopher W. Fraser

abstract: This paper describes a method for detecting structural hazards 5--80 times faster than its predecessors, which generally have simulated the pipeline at compile time. It accepts a compact specification of the pipeline and creates a finitestate automaton that can detect structural hazards in one table lookup per instruction. The automaton maintains an integer state that encodes all potential structural hazards for all instructions in the pipe. It accepts an instruction type and a state and either reports a hazard or produces the state that folds in the new instruction and advances the pipeline by one cy-


venue: popl

title: Higher-Order Equational Logic Programming

abstract: Higher-order equational logic programming is a paradigm which combines first-order equational and higher-order logic programming, where higher-order logic programming is based on a subclass of simply typed l-terms, called higher-order patterns. Central to the notion of higher-order equational logic programming is the so-called higher-order equational unification. This paper extends several important classes of first-order equational unification algorithms to the higher-order setting: only problems of the extensions are discussed and first-order equational unifications are viewed as black boxes whenever possible.We first extend narrowing and show that the completeness of many higher-order narrowing strategies reduces to that of their underlying first-order counterparts. Then we propose an algorithm or higher-order equational unification of free higher-order patterns in an arbitrary equational theory. Finally a general approach to extend first-order unification combination algorithms is sketched informally. The termination property of the above higher-order extensions is considered in a uniform way.


title: An Incremental Algorithm for Maintaining the Dominator Tree of a Reducible Flowgraph

authors:
G. Ramalingam
Thomas W. Reps

abstract: We present a new incremental algorithm for the problem of maintaining the dominator tree of a reducible flowgraph as the flowgraph undergoes changes such as the insertion and deletion of edges. Such an algorithm has applications in incremental dataflow analysis and incremental compilation.


title: Correctness of Trap-Based Breakpoint Implementations

abstract: It is common for debuggers to implement breakpoints by a combination of planting traps and single stepping. When the target program contains multiple threads of execution, a debugger that is not carefully implemented may miss breakpoints. This paper gives a formal model of a breakpoint in a two-threaded program. The model describes correct and incorrect breakpoint implementations. Automatic search of the model's state space shows that the correct implementation does miss a breakpoint. The results apply even to debuggers like dbx and gdb, which are apparently for single-threaded programs; when the user evaluates an expression containing function calls, the debugger executes the call in the target address space, in effect creating a new thread.


title: Building Interpreters by Composing Monads

abstract: We exhibit a set of functions coded in Haskell that can be used as building blocks to construct a variety of interpreters for Lisp-like languages. The building blocks are joined merely through functional composition. Each building block contributes code to support a specific feature, such as numbers, continuations, functions calls, or nondeterminism. The result of composing some number of building blocks is a parser, an interpreter, and a printer that support exactly the expression forms and data types needed for the combined set of features, and no more.


title: Automated Synthesis of Interface Adapters for Reusable Classes

abstract: The need to fit together reusable components and system designs in spite of differences in protocol and representation choices occurs often in object-oriented software construction. It is therefore necessary to use adapters to achieve an exact fit between the available “socket” for a reusable part and the actual part. In this paper we discuss an approach to the construction of tools that largely automate the synthesis of adapter code. Such tools are important in reducing the effort involved in reuse since adapter synthesis can be challenging and error-prone in the complex type environment of an object-oriented language. Our approach is applicable to statically typed languages like C++ and Eiffel, and is based on a formal notion of adaptability which is related to but distinct from both subtyping and inheritance.


title: Implementation of the Typed Call-by-Value lambda-Calculus using a Stack of Regions

authors:
Mads Tofte
Jean-Pierre Talpin

abstract: We present a translation scheme for the polymorphically typed call-by-value λ-calculus. All runtime values, including function closures, are put into regions. The store consists of a stack of regions. Region inference and effect inference are used to infer where regions can be allocated and de-allocated. Recursive functions are handled using a limited form of polymorphic recursion. The translation is proved correct with respect to a store semantics, which models as a region-based run-time system. Experimental results suggest that regions tend to be small, that region allocation is frequent and that overall memory demands are usually modest, even without garbage collection.

awards: Most Influential POPL Paper (awarded 2004)


title: Selective and Lightweight Closure Conversion

authors:
Mitchell Wand
Paul Steckler

abstract: We consider the problem of selective and lightweight closure conversion, in which multiple procedure-calling protocols may coexist in the same code. Flow analysis is used to match the protocol expected by each procedure and the protocol used at each of its possible call sites. We formulate the flow analysis as the solution of a set of constraints, and show that any solution to the constraints justifies the resulting transformation. Some of the techniques used are suggested by those of abstract interpretation, but others arise out of alternative approaches.


title: Value Dependence Graphs: Representation without Taxation

authors:
Daniel Weise
Roger F. Crew
Michael D. Ernst
Bjarne Steensgaard

abstract: The value dependence graph (VDG) is a sparse dataflow-like representation that simplifies program analysis and transformation. It is a functional representation that represents control flow as data flow and makes explicit all machine quantities, such as stores and I/O channels. We are developing a compiler that builds a VDG representing a program, analyzes and transforms the VDG, then produces a control flow graph (CFG) [ASU86] from the optimized VDG. This framework simplifies transformations and improves upon several published results. For example, it enables more powerful code motion than [CLZ86, FOW87], eliminates as many redundancies as [AWZ88, RWZ88] (except for redundant loops), and provides important information to the code scheduler [BR91]. We exhibit a fast, one-pass method for elimination of partial redundancies that never performs redundant code motion [KFS92, DS93] and is simpler than the classical [MR79, Dha91] or SSA [RWZ88] methods. These results accrue from eliminating the CFG from the analysis/transformation phases and using demand dependences in preference to control dependences.


title: An Extended Form of Must Alias Analysis for Dynamic Allocation

authors:
Rita Z. Altucher
William Landi

abstract: The paper presents methods that we have implemented to improve the quality of the def-uses reported for dynamically allocated locations. The methods presented are based on the Ruggieri/Murtagh naming scheme for dynamically created locations. We expand upon this scheme to name dynamically allocated locations for some user written allocation routines. Using this expanded naming scheme, we introduce an inexpensive, non-iterative, and localized calculation of extended must alias analysis to handle dynamically allocated locations, and show how this information can be used to improve def-use information. This is the first attempt to specify must alias information for names which represent a set of dynamically allocated locations. Empirical results are presented to illustrate the usefulness of our method. We consider this work a step towards developing practical re-engineering tools for C.


title: The Call-by-Need Lambda Calculus

authors:
Zena M. Ariola
Matthias Felleisen
John Maraist
Martin Odersky
Philip Wadler

abstract: The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their evaluator in terms of source level syntax, and they cannot easily compare distinct implementations of different lazy strategies. In this paper we derive an equational characterization of call-by-need and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than the lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g., the call-by-need continuation passing transformation and the realization of sharing via assignments.


title: A Formal Model of Procedure Calling Conventions

authors:
Mark W. Bailey
Jack W. Davidson

abstract: Procedure calling conventions are used to provide uniform procedure-call interfaces. Applications, such as compilers and debuggers, which generate, or process procedures at the machine-language abstraction level require knowledge of the calling convention. In this paper, we develop a formal model for procedure calling conventions called P-FSA's. Using this model, we are able to ensure several completeness and consistency properties of calling conventions. Currently, applications that manipulate procedures implement conventions in an ad-hoc manner. The resulting code is complicated with details, difficult to maintain, and often riddled with errors. To alleviate the situation, we introduce a calling convention specification language, called CCL. The combination of CCL and P-FSA's facilitates the accurate specification of conventions that can be shown to be both consistent and complete.


title: Higher-Order Functors with Transparent Signatures

abstract: The programming language Standard ML provides first-order functors, i.e. modules parameterized by modules. First-order functors in the language have a simple and elegant static semantics. The type structure of higher-order modules, i.e. modules parameterized by functors, is well understood. But it is only in the recent past that we have seen an implementation of higher-order functors with a formally defined static semantics in a dialect of Standard ML, SML/NJ. A study of this static semantics shows it to be much more complicated than the static semantics of first-order functors. This paper investigates whether we can trade some semantic features in the module language to obtain a simpler static semantics, closer in spirit to that of first-order functors. This work helps in a conceptual understanding of the semantics of higher-order modules.


title: Structured Operational Semantics as a Specification Language

abstract: Standard specification languages have very limited abilities to define new operations on processes. We introduce the concept of a Protean specification language, with general definitional facilities supported by the appropriate theory. Protean languages allow elegant, readable, and useful specifications at all levels of abstraction. A good Protean specification language will admit methods of verifying that one specification is a refinement of another. We sketch a family of Protean specification languages (with references to the full details) which allow a vast amount of expressive power in defining operations, but nonetheless have all the essential theoretical and specification power of CCS and ACP.We illustrate these techniques by presenting several specifications of the job of protecting an arbitrary server by a checkpoint/backup scheme. The high-level specification of the protected server simply says, “It does everything it did before, and it doesn't crash.” The middle-level specification describes checkpointing cleanly and abstractly, without prescribing any particular implementation. The low-level specification is fairly close to an implementation. We show the high- and medium-level specifications equivalent by bisimulation relation techniques, and the medium- and low-level specifications equivalent by equational reasoning using automatically-generated equations. We also show that the operations expressing checkpointing behavior are not definable in standard process algebras.


title: Verifying Infinite State Processes with Sequential and Parallel Composition

authors:
Ahmed Bouajjani
Rachid Echahed
Peter Habermehl

abstract: We investigate the verification problem of infinite-state process w.r.t. logic-based specifications that express properties which may be nonregular. We consider the process algebra PA which integrates and strictly subsumes the algebras BPA (basic process algebra) and BPP (basic parallel processes), by allowing both sequential and parallel compositions as well as nondeterministic choice and recursion. Many relevant properties of PA processes are nonregular, and thus can be expressed neither by classical temporal logics nor by finite state ω-automata. Properties of particular interest are those involving constraints on numbers of occurrences of events. In order to express such properties, which are nonregular in general, we use the temporal logic PCTL which combines the branching-time temporal logic CTL with Presburger arithmetics. Then we tackle the verification problem of guarded PA processes w.r.t. PCTL formulas. We mainly prove that, while this problem is undecidable for the full PCTL, it is actually decidable for the class of guarded PA processes (and thus for the class of guarded BPA's and guarded BPP's), and a large fragment of PCTL called PCTL+.


title: Sequential Algorithms, Deterministic Parallelism, and Intensional Expressiveness

authors:
Stephen D. Brookes
Denis Dancanet

abstract: We call language L1 intensionally more expressive than L2 if there are functions which can be computed faster in L1 than in L2. We study the intensional expressiveness of several languages: the Berry-Curien programming language of sequential algorithms, CDS0, a deterministic parallel extension to it, named CDSP, and various parallel extensions to the functional programming language PCF. The paper consists of two parts.


title: A Language with Distributed Scope

abstract: Obliq is a lexically-scoped, untyped, interpreted language that supports distributed object-oriented computation. Obliq objects have state and are local to a site. Obliq computations can roam over the network, while maintaining network connections. Distributed lexical scoping is the key mechanism for managing distributed computation.

awards: Most Influential POPL Paper (awarded 2005)


title: Corrigendum: Decidable Bounded Quantification

authors:
Giuseppe Castagna
Benjamin C. Pierce

abstract: No abstract available.


title: Unification Factoring for Efficient Execution of Logic Programs

authors:
Steven Dawson
C. R. Ramakrishnan
I. V. Ramakrishnan
Konstantinos Sagonas
Steven Skiena
Terrance Swift
David Scott Warren

abstract: The efficiency of resolution-based logic programming languages, such as Prolog, depends critically on selecting and executing sets of applicable clause heads to resolve against subgoals. Traditional approaches to this problem have focused on using indexing to determine the smallest possible applicable set. Despite their usefulness, these approaches ignore the non-determinism inherent in many programming languages to the extent that they do not attempt to optimize execution after the applicable set theory has been determined.


title: Generic Polymorphism

authors:
Catherine Dubois
François Rouaix
Pierre Weis

abstract: We present the extensional polymorphism, a framework to type check ad hoc polymorphic functions. This formalism is compatible with parametric polymorphism, and supports a large class of functions defined by structural pattern matching on types.


title: Demand-driven Computation of Interprocedural Data Flow

authors:
Evelyn Duesterwald
Rajiv Gupta
Mary Lou Soffa

abstract: This paper presents a general framework for deriving demand-driven algorithms for interprocedural data flow analysis of imperative programs. The goal of demand-driven analysis is to reduce the time and/or space overhead of conventional exhaustive analysis by avoiding the collection of information that is not needed. In our framework, a demand for data flow information is modeled as a set of date flow queries. The derived demand-driven algorithms find responses to these queries through a partial reversal of the respective data flow analysis. Depending on whether minimizing time or space is of primary concern, result caching may be incorporated in the derived algorithm. Our framework is applicable to interprocedural data flow problems with a finite domain set. If the problem's flow functions are distributive, the derived demand algorithms provide as precise information as the corresponding exhaustive analysis. For problems with monotone but non-distributive flow functions the provided data flow solutions are only approximate. We demonstrate our approach using the example of interprocedural copy constant propagation.


title: Reasoning about Rings

authors:
E. Allen Emerson
Kedar S. Namjoshi

abstract: The ring is a useful means of structuring concurrent processes. Processes communicate by passing a token in a fixed direction; the process that possesses the token is allowed to make certain moves. Usually, correctness properties are expected to hold irrespective of the size of the ring. We show that the problem of checking many useful correctness properties for rings of all sizes can be reduced to checking them on a ring of small size. The results do not depend on the processes being finite state. We illustrate our results on examples.


title: Parametric Program Slicing

authors:
John Field
G. Ramalingam
Frank Tip

abstract: Program slicing is a technique for isolating computational threads in programs. In this paper, we show how to mechanically extract a family of practical algorithms for computing slices directly from semantic specifications. These algorithms are based on combining the notion of dynamic dependence tracking in term rewriting systems with a program representation whose behavior is defined via an equational logic. Our approach is distinguished by the fact that changes to the behavior of the slicing algorithm can be accomplished through simple changes in rewriting rules that define the semantics of the program representation. Thus, e.g., different notions of dependence may be specified, properties of language-specific datatypes can be exploited, and various time, space, and precision tradeoffs may be made. This flexibility enables us to generalize the traditional notions of static and dynamic slices to that of a constrained slice, where any subset of the inputs of a program may be supplied.


title: The Semantics of Future and Its Use in Program Optimizations

authors:
Cormac Flanagan
Matthias Felleisen

abstract: The future annotations of MultiLisp provide a simple method for taming the implicit parallelism of functional programs. Past research concerning futures has focused on implementation issues. In this paper, we present a series of operational semantics for an idealized functional language with futures with varying degrees of intensionality. We develop a set-based analysis algorithm from the most intensional semantics, and use that algorithm to perform touch optimization on programs. Experiments with the Gambit compiler indicates that this optimization substantially reduces program execution times. 1 Implicit Parallelism via Annotations Programs in functional languages offer numerous opportunities for executing program components in parallel. In a call-by-value language, for example, the evaluation of every function application could spawn a parallel thread for each sub-expression. However, if such a strategy were applied indiscriminately, the execution of a program would generate far t...


title: Compiling Polymorphism Using Intensional Type Analysis

authors:
Robert Harper
J. Gregory Morrisett

abstract: The views and conclusions contained in this document are those of the authors and should not be interpreted as


title: Lower Bounds on Type Inference with Subtypes

authors:
My Hoang
John C. Mitchell

abstract: We investigate type inference for programming languages with subtypes. As described in previous work, there are several type inference problems for any given expression language, depending on the form of the subtype partial order and the ability to define new subtypes in programs. Our first main result is that for any specific subtype partial order, the problem of determining whether a lambda term is typable is algorithmically (polynomial-time) equivalent to a form of satisfiability problem over the same partial order. This gives the first exact characterization of the problem that is independent of the syntax of expressions. In addition, since this form of satisfiability problem is PSPACE-hard over certain partial orders, this equivalence strengthens the previous lower bound of NP-hard to PSPACE-hard. Our second main result is a lower bound on the length of most general types when the subtype hierarchy may change as a result of additional type declarations within the program. More specifically, given any input expression, a type inference algorithm tries to find a most general (or principal) typing. The property of a most general typing is that it has all other possible typings as instances. However, there are several sound notions of instance in the presence of subtyping. Our lower bound is that no sound definition of instance would allow the set of additional subtyping hypotheses about a term to grow less than linearly in the size of the term.


title: Positive Subtyping

authors:
Martin Hofmann
Benjamin C. Pierce

abstract: The statement S≤T in a λ-calculus with subtyping is traditionally interpreted by a semantic coercion function of type [[S]]→[[T]] that extracts the “T part” of an element of S. If the subtyping relation is restricted to covariant positions, this interpretation may be enriched to include both the implicit coercion and an overwriting function put[S,T] ∈ [[S]]→[[T]]→[[S]] that updates the T part of an element of S. We give a realizability model and a sound equational theory for a second-order calculus of positive subtyping.


title: A Unified Treatment of Flow Analysis in Higher-Order Languages

authors:
Suresh Jagannathan
Stephen Weeks

abstract: We describe a framework for flow analysis in higher-order languages. It is both a synthesis and extension of earlier work in this area, most notably [20, 22]


title: Structuring Depth-First Search Algorithms in Haskell

authors:
David J. King
John Launchbury

abstract: Depth-first search is the key to a wide variety of graph algorithms. In this paper we express depth-first search in a lazy functional language, obtaining a linear-time implementation. Unlike traditional imperative presentations, we use the structuring methods of functional languages to construct algorithms from individual reusable components. This style of algorithm construction turns out to be quite amenable to formal proof, which we exemplify through a calculational-style proof of a far from obvious strongly-connected components algorithm.


title: Applicative Functors and Fully Transparent Higher-Order Modules

abstract: we present a variety of the Standard ML module system where parameterized abstract types (i.e. functors returning generative types) map provably equal arguments to compatible abstract types, instead of generating distinct types at each applications as in Standard ML. This extension solves the full transparency problem (how to give syntactic signatures for higher-order functors that express exactly their propagation of type equations), and also provides better support for non-closed code fragments.


title: Monad Transformers and Modular Interpreters

authors:
Sheng Liang
Paul Hudak
Mark P. Jones

abstract: We show how a set of building blocks can be used to construct programming language interpreters, and present implementations of such building blocks capable of supporting many commonly known features, including simple expressions, three different function call mechanisms (call-by-name, call-by-value and lazy evaluation), references and assignment, nondeterminism, first-class continuations, and program tracing.


title: The Geometry of Interaction Machine

abstract: We investigate implementation techniques arising directly from Girard's Geometry of Interaction semantics for Linear Logic, specifically for a simple functional programming language (PCF). This gives rise to a very simple, compact, compilation schema and run-time system. We analyse various properties of this kind of computation that suggest substantial optimisations that could make this paradigm of implementation not only practical, but potentially more efficient than extant paradigms.


title: A Type System Equivalent to Flow Analysis

authors:
Jens Palsberg
Patrick O'Keefe

abstract: Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis.


title: Obtaining Sequential Efficiency for Concurrent Object-Oriented Languages

authors:
John Plevyak
Xingbin Zhang
Andrew A. Chien

abstract: Concurrent object-oriented programming (COOP) languages focus the abstraction and encapsulation power of abstract data types on the problem of concurrency control. In particular, pure fine-grained concurrent object-oriented languages (as opposed to hybrid or data parallel) provides the programmer with a simple, uniform, and flexible model while exposing maximum concurrency. While such languages promise to greatly reduce the complexity of large-scale concurrent programming, the popularity of these languages has been hampered by efficiency which is often many orders of magnitude less than that of comparable sequential code. We present a sufficiency set of techniques which enables the efficiency of fine-grained concurrent object-oriented languages to equal that of traditional sequential languages (like C) when the required data is available. These techniques are empirically validated by the application to a COOP implementation of the Livermore Loops.


title: Optimizing an ANSI C Interpreter with Superoperators

abstract: This paper introduces superoperators, an optimization technique for bytecoded interpreters. Superoperators are virtual machine operations automatically synthesized from smaller operations to avoid costly per-operation overheads. Superoperators decrease executable size and can double or triple the speed of interpreted programs. The paper describes a simple and effective heuristic for inferring powerful superoperators from the usage patterns of simple operators.


title: Precise Interprocedural Dataflow Analysis via Graph Reachability

authors:
Thomas W. Reps
Susan Horwitz
Shmuel Sagiv

abstract: The paper shows how a large class of interprocedural dataflow-analysis problems can be solved precisely in polynomial time by transforming them into a special kind of graph-reachability problem. The only restrictions are that the set of dataflow facts must be a finite set, and that the dataflow functions must distribute over the confluence operator (either union or intersection). This class of probable problems includes—but is not limited to—the classical separable problems (also known as “gen/kill” or “bit-vector” problems)—e.g., reaching definitions, available expressions, and live variables. In addition, the class of problems that our techniques handle includes many non-separable problems, including truly-live variables, copy constant propagation, and possibly-uninitialized variables.


title: Using Functor Categories to Generate Intermediate Code

abstract: In the early 80's Oles and Reynolds devised a semantic model of Algol-like languages using a category of functors from a category of store shapes to the category of predomains. Here we will show how a variant of this idea can be used to define the translation of an Algol-like language to intermediate code in a uniform way that avoids unnecessary temporary variables, provides control-flow translation of boolean expressions, permits online expansion of procedures, and minimizes the storage overhead of calls of closed procedures. The basic idea is to replace continuations by instruction sequences and store shapes by descriptions of the structure of the run-time stack.


title: Isolating Side Effects in Sequential Languages

authors:
Jon G. Riecke
Ramesh Viswanathan

abstract: It is well known that adding side effects to functional languages changes the operational equivalences of the language. We develop a new language construct, encap, that forces imperative pieces of code to behave purely functionally, i.e., without any visible side effects. The coercion operator encap provides a means of extending the simple reasoning principles for equivalences of code in a functional language to a language with side effects. In earlier work [36], similar coercion operators were developed, but their correctness required the underlying functional language to include parallel operations. The coercion operators developed here are simpler and are proven correct for purely sequential languages. The sequential setting requires the construction of fully abstract models for sequential call-by-value languages and the formulation of a weak form of "monad" suitable for expressing the semantics of call-by-value languages with side effects. 1 Introduction Two pieces of code are...


title: Total Correctness by Local Improvement in Program Transformation

abstract: The goal of program transformation is to improve efficiency while preserving meaning. One of the best known transformation techniques is Burstall and Darlington's unfold-fold method. Unfortunately the unfold-fold method itself guarantees neither improvement in efficiency nor total-correctness. The correctness problem for unfold-fold is an instance of a strictly more general problem: transformation by locally equivalence-preserving steps does not necessarily preserve (global) equivalence.


title: Time and Space Profiling for Non-Strict Higher-Order Functional Languages

authors:
Patrick M. Sansom
Simon L. Peyton Jones

abstract: We present the first profiler for a compiled, non-strict, higher-order, purely functional language capable of measuring time as well as space usage. Our profiler is implemented in a production-quality optimising compiler for Haskell, has low overheads, and can successfully profile large applications.


title: Default Timed Concurrent Constraint Programming

authors:
Vijay A. Saraswat
Radha Jagadeesan
Vineet Gupta

abstract: We extend the model of [SJG94b] to express strong time-outs (and pre-emption): if an event A does not happen through time t, cause event B to happen at time t. Such constructs arise naturally in practice (e.g. in modeling transistors) and are supported in languages such as ESTEREL (through instantaneous watchdogs) and LUSTRE (through the “current” operator).


title: Separation Constraint Partitioning - A New Algorithm for Partitioning Non-strict Programs into Sequential Threads

authors:
Klaus E. Schauser
David E. Culler
Seth Copen Goldstein

abstract: In this paper we present substantially improved thread partitioning algorithms for modern implicitly parallel languages. We present a new block partitioning algorithm, separation constraint partitioning, which is both more powerful and more flexible than previous algorithms. Our algorithm is guaranteed to derive maximal threads. We present a theoretical framework for proving the correctness of our partitioning approach, and we show how separation constraint partitioning makes interprocedural partitioning viable.


title: A Linear Time Algorithm for Placing phi-nodes

authors:
Vugranam C. Sreedhar
Guang R. Gao

abstract: Dataflow analysis framework based on Static Single Assignment (SSA) form and Sparse Evaluation Graphs (SEGs) demand fast computation of program points where data flow information must be merged, the so-called φ-nodes. In this paper, we present a surprisingly simple algorithm for computing φ-nodes for arbitrary flowgraphs (reducible or irreducible) that runs in linear time. We employ a novel program representation—the DJ graph—by augmenting the dominator tree of a flowgraph with edges which may lead to a potential “merge” of dataflow information. In searching for φ-nodes we never visit an edge in the DJ-graph more than once by guiding the search of nodes by their levels in the dominator tree.


title: Structural Decidable Extensions of Bounded Quantification

abstract: We show how the subtype relation of the well-known system order theory of several successor functions (W)SnS.


title: An Interpretation of Objects and Object Types

authors:
Martín Abadi
Luca Cardelli
Ramesh Viswanathan

abstract: We present an interpretation of typed object-oriented concepts in terms of well-understood, purely procedural concepts. More precisely, we give a compositional subtype-preserving translation of a basic object calculus supporting method invocation, functional method update, and subtyping, into the polymorphic λ-calculus with recursive types and subtyping. The translation techniques apply also to an imperative version of the object calculus which includes in-place method update and object cloning. Finally, the translation easily extends to "Self types" and other interesting object-oriented constructs.


title: A Practical and Flexible Flow Analysis for Higher-Order Languages

abstract: A flow analysis collects data-flow and control-flow information about programs. A compiler can use this information to enable optimizations. The analysis described in this article unifies and extends previous work on flow analyses for higher-order languages supporting assignment and control operators. The analysis is abstract interpretation based and is parameterized over two polyvariance operators and a projection operator. These operators are used to regulate the speed and accuracy of the analysis. An implementation of the analysis is incorporated into and used in a production Scheme compiler. The analysis can process any legal Scheme program without modification. Others have demonstrated that a 0CFA analysis can enable optimizations, but a 0CFA analysis is O(n3). An O(n) instantiation of our analysis successfully enables the optimization of closure representations and procedure calls. Experiments with the cheaper instantiation show that it is as effective as 0CFA for these optimizations.


title: On the Complexity of Beta-Reduction

abstract: We prove that the complexity of Lamping's optimal graph reduction technique for the λ-calculus can be exponential in the number of Lévy's family reductions. Starting from this consideration, we propose a new measure for what could be considered as "the intrinsic complexity" of λ-terms.


title: From Region Inference to von Neumann Machines via Region Representation Inference

authors:
Lars Birkedal
Mads Tofte
Magnus Vejlstrup

abstract: Region Inference is a technique for implementing programming languages that are based on typed call-by-value lambda calculus, such as Standard ML. The mathematical runtime model of region inference uses a stack of regions, each of which can contain an unbounded number of values. This paper is concerned with mapping the mathematical model onto real machines. This is done by composing region inference with Region Representation Inference, which gradually refines region information till it is directly implementable on conventional von Neumann machines. The performance of a new region-based ML compiler is compared to the performance of Standard ML of New Jersey, a state-of-the-art ML compiler.


title: Trace-Based Program Analysis

authors:
Christopher Colby
Peter Lee

abstract: We present trace-based program analysis, a semantics-based framework for statically analyzing and transforming programs with loops, assignments, and nested record structures. Trace-based analyses are based on transfer transition systems, which define the small-step operational semantics of programming languages. Intuitively, transfer transition systems provide direct support for reasoning about the possible execution traces of a program, instead of just individual program states. The traces in a transfer transition system have many uses, including the finite representation of all possible terminating executions of a loop. Also, traces may be systematically "pieced together," thus allowing the composition of separately analyzed program fragments. The utility of the approach is demonstrated by showing three applications: software pipelining, loop-invariant removal, and data alias detection. 1 Introduction In this paper, we consider semantics-based program analysis for the purposes of s...


title: A General Approach for Run-Time Specialization and its Application to C

authors:
Charles Consel
François Noël

abstract: Specializing programs with respect to run-time invariants is an optimization technique that has shown to improve the performance of programs substantially. It allows a program to adapt to execution contexts that are valid for a limited time.Run-time specialization is being actively investigated in a variety of areas. For example, recently, major operating system research projects have been focusing on run-time specialization as a means to obtain efficiency from highly extensible and parameterized systems.This paper describes a general approach to run-time specialization. For a given program and a declaration of its run-time invariants, it automatically produces source templates at compile time, and transforms them so that they can be processed by a standard compiler. At run time, only minor operations need to be performed: selecting and copying templates, filling holes with run-time values, and relocating jump targets. As a consequence, run-time specialization is performed very efficiently and thus does not require the specialized code to be executed many times before its cost is amortized.Our approach improves on previous work in that: (1) templates are automatically produced from the source program and its invariants, (2) the approach is not machine dependent, (3) it is formally defined and proved correct, (4) it is efficient, as shown by our implementation for the C language.


title: Type-Directed Partial Evaluation

abstract: We present a strikingly simple partial evaluator, that is type-directed and reifies a compiled program into the text of a residual, specialized program. Our partial evaluator is concise (a few lines) and it handles the flagship examples of offline monovariant partial evaluation. Its source programs are constrained in two ways: they must be closed and monomorphically typable. Thus dynamic free variables need to be factored out in a "dynamic initial environment". Type-directed partial evaluation uses no symbolic evaluation for specialization, and naturally processes static computational effects.Our partial evaluator is the part of an offline partial evaluator that residualizes static values in dynamic contexts. Its restriction to the simply typed lambda-calculus coincides with Berger and Schwichtenberg's "inverse of the evaluation functional" (LICS'91), which is an instance of normalization in a logical setting. As such, type-directed partial evaluation essentially achieves lambda-calculus normalization. We extend it to produce specialized programs that are recursive and that use disjoint sums and computational effects. We also analyze its limitations: foremost, it does not handle inductive types.This paper therefore bridges partial evaluation and λ-calculus normalization through higher-order abstract syntax, and touches upon parametricity, proof theory, and type theory (including subtyping and coercions), compiler optimization, and rut-time code generation (including decompilation). It also offers a simple solution to denotational semantics-based compilation and compiler generation.


title: A Modal Analysis of Staged Computation

authors:
Rowan Davies
Frank Pfenning

abstract: We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of functional languages. Our main technical result is a conservative embedding of Nielson & Nielson's two-level functional language in our language Mini-ML, thus proving that binding-time correctness is equivalent to modal correctness on this fragment. In addition Mini-ML can also express immediate evaluation and sharing of code across multiple stages, thus supporting run-time code generation as well as partial evaluation.


title: C: A Language for High-Level, Efficient, and Machine-Independent Dynamic Code Generation

authors:
Dawson R. Engler
Wilson C. Hsieh
M. Frans Kaashoek

abstract: Dynamic code generation allows specialized code sequences to be created using runtime information. Since this information is by definition not available statically, the use of dynamic code generation can achieve performance inherently beyond that of static code generation. Previous attempts to support dynamic code generation have been low-level, expensive, or machine-dependent. Despite the growing use of dynamic code generation, no mainstream language provides flexible, portable, and efficient support for it.We describe 'C (Tick C), a superset of ANSI C that allows flexible, high-level. efficient, and machine-independent specification of dynamically generated code. 'C provides many of the performance benefits of pure partial evaluation, but in the context of a complex, statically typed, but widely used language. 'C examples illustrate the ease of specifying dynamically generated code and how it can be put to use. Experiments with a prototype compiler show that 'C enables excellent performance improvement (in some cases, more than an order of magnitude).


title: Revisiting Catamorphisms over Datatypes with Embedded Functions (or, Programs from Outer Space)

authors:
Leonidas Fegaras
Tim Sheard

abstract: We revisit the work of Paterson and of Meijer & Hutton, which describes how to construct catamorphisms for recursive datatype definitions that embed contravariant occurrences of the type being defined. Their construction requires, for each catamorphism, the definition of an anamorphism that has an inverse-like relationship to that catamorphism. We present an alternative construction, which replaces the stringent requirement that an inverse anamorphism be defined for each catamorphism with a more lenient restriction. The resulting construction has a more efficient implementation than that of Paterson, Meijer, and Hutton and the relevant restriction can be enforced by a Hindley-Milner type inference algorithm. We provide numerous examples illustrating our method.


title: The Reflexive CHAM and the Join-Calculus

authors:
Cédric Fournet
Georges Gonthier

abstract: By adding reflexion to the chemical machine of Berry and Boudol, we obtain a formal model of concurrency that is consistent with mobility and distribution. Our model provides the foundations of a programming language with functional and object-oriented features. It can also be seen as a process calculus, the join-calculus, which we prove equivalent to the π-calculus of Milner, Parrow and Walker.


title: Iterated Register Coalescing

authors:
Lal George
Andrew W. Appel

abstract: An important function of any register allocator is to target registers so as to eliminate copy instructions. Graph-coloring register allocation is an elegant approach to this problem. If the source and destination of a move instruction do not interfere, then their nodes can be coalesced in the interference graph. Chaitin's coalescing heuristic could make a graph uncolorable (i.e., introduce spills); Briggs et al. demonstrated a conservative coalescing heuristic that preserves colorability. But Briggs's algorithm is too conservative, and leaves too many move instructions in our programs. We show how to interleave coloring reductions with Briggs's coalescing heuristic, leading to an algorithm that is safe but much more aggressive.


title: Is it a Tree, a DAG, or a Cyclic Graph? A Shape Analysis for Heap-Directed Pointers in C

authors:
Rakesh Ghiya
Laurie J. Hendren

abstract: This paper reports on the design and implementation of a practical shape analysis for C. The purpose of the analysis is to aid in the disambiguation of heap-allocated data structures by estimating the shape (Tree, DAG, or Cyclic Graph) of the data structure accessible from each heap-directed pointer. This shape information can be used to improve dependence testing and in parallelization, and to guide the choice of more complex heap analyses.The method has been implemented as a context-sensitive interprocedural analysis in the McCAT conlpiler. Experimental results and observations are given for 16 benchmark programs. These results show that the analysis gives accurate and useful results for an important group of applications.


title: Bisimilarity for a First-Order Calculus of Objects with Subtyping

authors:
Andrew D. Gordon
Gareth D. Rees

abstract: Bisimilarity (also known as 'applicative bisimulation') has attracted a good deal of attention as an operational equivalence for λ-calculi. It approximates or even equals Morris-style contextual equivalence and admits proofs of program equivalence via co-induction. It has an elementary construction from the operational definition of a language. We consider bisimilarity for one of the typed object calculi of Abadi and Cardelli. By defining a labelled transition system for the calculus in the style of Crole and Gordon and using a variation of Howe's method we establish two central results: that bisimilarity is a congruence, and that it equals contextual equivalence. So two objects are bisimilarity no amount of programming can tell them apart. Our third contribution is to show that bisimilarity soundly models the equational theory of Abadi and Cardelli. This is the first study of contextual equivalence for an object calculus and the first application of Howe's method to subtyping. By these results, we intend to demonstrate that operational methods are a promising new direction for the foundations of object-oriented programming.


title: Optimization and Relaxation in Constraint Logic Languages

authors:
Kannan Govindarajan
Bharat Jayaraman
Surya Mantha

abstract: Optimization and relaxation are two important operations that naturally arise in many applications involving constraints, e.g., engineering design, scheduling, decision support, etc. In optimization, we are interested in finding the optimal (i.e., best) solutions to a set of constraints with respect to an objective function. In many applications, optimal solutions may be difficult or impossible to obtain, and hence we are interested in finding suboptimal solutions, by either relaxing the constraints or relaxing the objective function. The contribution of this paper lies in providing a logical framework for performing optimization and relaxation in a constraint logic programming language. Our proposed framework is called preference logic programming (PLP), and its use for optimization was discussed in [8]. Essentially, in PLP we can designate certain predicates as optimization predicates, and we can specify the objective function by stating preference criteria for determining the optimal solutions to these predicates. This paper extends the PLP paradigm with facilities to formulate relaxation problems in a natural manner. We introduce the concept of a relaxation goal, and discuss its use for preference relaxation. Our model-theoretic semantics of relaxation is based on simple concepts from modal logic: Essentially, each world in the possible-worlds semantics for a preference logic program is a model for the constraints of the program, and an ordering over these worlds is determined by the objective function. Optimization can then be expressed as truth in strongly optimal worlds, while relaxation becomes truth in suitably-defined suboptimal worlds. We also present an operational semantics for relaxation as well as correctness results. Our conclusion is that the concept of preference provides a unifying framework for formulating optimization as well as relaxation problems.


title: A Provably Time-Efficient Parallel Implementation of Full Speculation

authors:
John Greiner
Guy E. Blelloch

abstract: Speculative evaluation, including leniency and futures, is often used to produce high degrees of parallelism, Existing speculative implementations, however, may serialize computation because of their implementation of queues of suspended threads. We give a provably efficient parallel implementation of a speculative functional language on various machine models. The implementation includes proper parallelization of the necessary queuing operations on suspended threads. Our target machine models are a butterfly network, hypercube, and PRAM. To prove the efficiency of our implementation, we provide a cost model using a profiling semantics and relate the cost model to implementations on the parallel machine models.


title: Static Analysis to Reduce Synchronization Costs in Data-Parallel Programs

authors:
Manish Gupta
Edith Schonberg

abstract: For a program with sufficient parallelism, reducing synchronization costs is one of the most important objectives for achieving efficient execution on any parallel machine. This paper presents a novel methodology for reducing synchronization costs of programs compiled for SPMD execution. This methodology combines data flow analysis with communication analysis to determine the ordering between production and consumption of data on different processors, which helps in identifying redundant synchronization. The resulting framework is more powerful than any that have been previously presented, as it provides the first algorithm that can eliminate synchronization messages even from computations that need communication. We show that several commonly occurring computation patterns such as reductions and stencil computations with reciprocal producer-consumer relationship between processors lend themselves well to this optimization, an observation that is confirmed by an examination of some HPF benchmark programs. Our framework also recognizes situations where the synchronization needs for multiple data transfers can be satisfied by a single synchronization message. This analysis, while applicable to all shared memory machines as well, is especially useful for those with a flexible cache-coherence protocol, as it identifies efficient ways of moving data directly from producers to consumers, often without any extra synchronization.


title: Composing Processes

abstract: We present a theory of types for concurrency based on a simple notion of typed algebras, and discuss its applications. The basic idea is to determine a partial algebra of processes by a partial algebra of types, thus controlling process composability, just as types in a typed applicative structure [25] determine composability of elements of the underlying applicative structure. A class of typed algebras with a simple operator for process composition are introduced, which are shown to encompass a wide range of type disciplines for processes, placing extant theories such as Milner's sorting [22] and Lafont's typed nets [20] on a uniform technical footing, suggesting generalisations, and offering a secure basis for integration. We also prove that the class of typable operations in the underlying partial algebras is completely characterised by a certain modularity principle in process composition, which gives us the basic understanding on the nature of the type disciplines representable in the proposed construction.


title: Generating Machine Specific Optimizing Compilers

authors:
Roger Hoover
F. Kenneth Zadeck

abstract: Article Generating machine specific optimizing compilers Share on Authors: Roger Hoover Computer Science Department, IBM TJ Watson Research Center, PO Box 704, Yorktown Heights, NY Computer Science Department, IBM TJ Watson Research Center, PO Box 704, Yorktown Heights, NYView Profile , Kenneth Zadeck Computer Science Department, IBM TJ Watson Research Center, PO Box 704, Yorktown Heights, NY Computer Science Department, IBM TJ Watson Research Center, PO Box 704, Yorktown Heights, NYView Profile Authors Info & Claims POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1996 Pages 219–229https://doi.org/10.1145/237721.237779Published:01 January 1996 6citation31DownloadsMetricsTotal Citations6Total Downloads31Last 12 Months5Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access


title: Proving the Correctness of Reactive Systems Using Sized Types

authors:
John Hughes
Lars Pareto
Amr Sabry

abstract: We have designed and implemented a type-based analysis for proving some basic properties of reactive systems. The analysis manipulates rich type expressions that contain information about the sizes of recursively defined data structures. Sized types are useful for detecting deadlocks, nontermination, and other errors in embedded programs. To establish the soundness of the analysis we have developed an appropriate semantic model of sized types.


title: Faster Checking of Software Specifications by Eliminating Isomorphs

authors:
Daniel Jackson
Somesh Jha
Craig Damon

abstract: Both software specifications and their intended properties can be expressed in a simple relational language. The claim that a specification satisfies a property becomes a relational formula that can be checked automatically by enumerating the formula's interpretations. Because the number of interpretations is usually huge, this approach has not been thought to be practical. But by eliminating isomorphic interpretations, the enumeration can be reduced substantially, with a factor of roughly k! contributed by each type of k elements.


title: What Are Principal Typings and What Are They Good For?

abstract: We demonstrate the pragmatic value of the principal typing property, a property distinct from ML's principal type property, by studying a type system with principal typings. The type system is based on rank 2 intersection types and is closely related to ML. Its principal typing property provides elegant support for separate compilation, including "smartest recompilation" and incremental type inference. Moreover, it motivates a new rule for typing recursive definitions that can type some interesting examples of polymorphic recursion.


title: Using Parameterized Signatures to Express Modular Structure

abstract: Module systems are a powerful, practical tool for managing the complexity of large software systems. Previous attempts to formulate a type-theoretic foundation for modular programming have been based on existential, dependent, or manifest types. These approaches can be distinguished by their use of different quantifiers to package the operations that a module exports together with appropriate implementation types. In each case, the underlying type theory is simple and elegant, but significant and sometimes complex extensions are needed to account for features that are important in practical systems, such as separate compilation and propagation of type information between modules.This paper presents a simple type-theoretic framework for modular programming using parameterized signatures. The use of quantifiers is treated as a necessary, but independent concern. Using familiar concepts of polymorphism, the resulting module system is easy to understand and admits true separate compilation. It is also very powerful, supporting high-order, polymorphic, and first-class modules without further extension.


title: Concurrent Haskell

authors:
Simon L. Peyton Jones
Andrew D. Gordon
Sigbjørn Finne

abstract: No abstract available.


title: Linearity and the Pi-Calculus

authors:
Naoki Kobayashi
Benjamin C. Pierce
David N. Turner

abstract: The economy and flexibility of the pi-calculus make it attractive both as an object of theoretical study and as a basis for concurrent language design and implementation. However, such generality has a cost: encoding higher-level features like functional computation in pi-calculus throws away potentially useful information. We show how a linear type system can be used to recover important static information about a process's behaviour. In particular, we can guarantee that two processes communicating over a linear channel cannot interfere with other communicating processes. This enables more aggressive optimisation of communications over linear channels and allows useful refinements to the usual notions of process equivalence for pi-calculus.After developing standard results such as soundness of typing, we focus on equivalences, adapting the standard notion of barbed bisimulation to the linear setting and showing how reductions on linear channels induce a useful "partial confluence" of process behaviors.


title: Minimum Cost Interprocedural Register Allocation

authors:
Steven M. Kurlander
Charles N. Fischer

abstract: Past register allocators have applied heuristics to allocate registers at the local, global, and interprocedural levels. This paper presents a polynomial time interprocedural register allocator that models the cost of allocating registers to procedures and spilling registers across calls. To find the minimum cost allocation, our allocator maps solutions from a dual network flow problem that can be solved in polynomial time. Experiments show that our interprocedural register allocator can yield significant improvements in execution time.


title: Discovering Auxiliary Information for Incremental Computation

authors:
Yanhong A. Liu
Scott D. Stoller
Tim Teitelbaum

abstract: This paper presents program analyses and transformations that discover a general class of auxiliary information for any incremental computation problem. Combining these techniques with previous techniques for caching intermediate results, we obtain a systematic approach that transforms nonincremental programs into efficient incremental programs that use and maintain useful auxiliary information as well as useful intermediate results. The use of auxiliary information allows us to achieve a greater degree of incrementality than otherwise possible. Applications of the approach include strength reduction in optimizing compilers and finite differencing in transformational programming.


title: Typed Closure Conversion

authors:
Yasuhiko Minamide
J. Gregory Morrisett
Robert Harper

abstract: Closure conversion is a program transformation used by compilers to separate code from data. Previous accounts of closure conversion use only untyped target languages. Recent studies show that translating to typed target languages is a useful methodology for building compilers, because a compiler can use the types to implement efficient data representations, calling conventions, and tag-free garbage collection. Furthermore, type-based translations facilitate security and debugging through automatic type checking, as well as correctness arguments through the method of logical relations.We present closure conversion as a type-directed, and type-preserving translation for both the simply-typed and the polymorphic λ-calculus. Our translations are based on a simple "closures as objects" principle: higher-order functions are viewed as objects consisting of a single method (the code) and a single instance variable (the environment). In the simply-typed case, the Pierce-Turner model of object typing where objects are packages of existential type suffices. In the polymorphic case, more careful tracking of type sharing is required. We exploit a variant of the Harper-Lillibridge "translucent type" formalism to characterize the types of polymorphic closures.


title: Functional Computation as Concurrent Computation

abstract: Available from TIB Hannover: RR 1812(95-14) / FIZ - Fachinformationszzentrum Karlsruhe / TIB - Technische Informationsbibliothek


title: Putting Type Annotations to Work

authors:
Martin Odersky
Konstantin Läufer

abstract: We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields. More generally, all programs of the polymorphic lambda calculus can be encoded by a translation between typing derivations. We show that type reconstruction in this system can be reduced to the decidable problem of first-order unification under a mixed prefix.


title: Pure versus Impure LISP

abstract: 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 structures can be created by impure programs, but not by pure ones. In this sense, impure Lisp is more powerful than pure Lisp. If the inputs and outputs of programs are restricted to be sequences of atomic symbols, however, this difference in computability disappears. We shall show that if the temporal sequence of input and output operations must be maintained (that is, if computations must be online), then a difference in complexity remains: for a pure program to do what an impure program does in n steps, O(n log n) steps are sufficient, and in some cases Ω(n log n) steps are necessary.


title: Filter Fusion

authors:
Todd A. Proebsting
Scott A. Watterson

abstract: Article Free AccessFilter fusion Share on Authors: Todd A. Proebsting Department of Computer Science, University of Arizona, Tucson, AZ Department of Computer Science, University of Arizona, Tucson, AZView Profile , Scott A. Watterson Department of Computer Science, University of Arizona, Tucson, AZ Department of Computer Science, University of Arizona, Tucson, AZView Profile Authors Info & Claims POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1996 Pages 119–130https://doi.org/10.1145/237721.237760Online:01 January 1996Publication History 32citation32DownloadsMetricsTotal Citations32Total Downloads32Last 12 Months3Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Solving Shape-Analysis Problems in Languages with Destructive Updating

authors:
Shmuel Sagiv
Thomas W. Reps
Reinhard Wilhelm

abstract: This paper concerns the static analysis of programs that perform destructive updating on heap-allocated storage. We give an algorithm that conservatively solves this problem by using a finite shape-graph to approximate the possible "shapes" that heap-allocated structures in a program can take on. In contrast with previous work, our method is even accurate for certain programs that update cyclic data structures. For example, our method can determine that when the input to a program that searches a list and splices in a new element is a possibly circular list, the output is a possibly circular list.


title: Points-to Analysis in Almost Linear Time

abstract: We present an interprocedural flow-insensitive points-to analysis based on type inference methods with an almost linear time cost complexity To our knowledge, this is the asymptotically fastest non-trivial interprocedural points-to analysis algorithm yet described The algorithm is based on a non-standard type system. The type inferred for any variable represents a set of locations and includes a type which in turn represents a set of locations possibly pointed to by the variable. The type inferred for a function variable represents a set of functions It may point to and includes a type signature for these functions The results are equivalent to those of a flow-insensitive alias analysis (and control flow analysis) that assumes alias relations are reflexive and transitive.This work makes three contributions. The first is a type system for describing a universally valid storage shape graph for a program in linear space. The second is a constraint system which often leads to better results than the "obvious" constraint system for the given type system The third is an almost linear time algorithm for points-to analysis by solving a constraint system.

awards: Most Influential POPL Paper (awarded 2006)


title: Search and Imperative Programming

authors:
Krzysztof R. Apt
Andrea Schaerf

abstract: We augment the expressive power of imperative programming in order to make it a more attractive vehicle for problems that involve search. The proposed additions are limited yet powerful and are inspired by the logic programming paradigm. We illustrate their use by presenting solutions to a number of classical problems, including the straight search problem, the knapsack problem, and the 8 queens problem. These solutions are substantially simpler than their counterparts written in the conventional way and can be used for different purposes without any modification.The proposed language is an intermediate stage on the road towards a realization of a strongly typed constraint programming language that combines the advantages of the logic programming and imperative programming.


title: Parameterized Types for Java

authors:
Andrew C. Myers
Joseph A. Bank
Barbara Liskov

abstract: Java offers the real possibility that most programs can be written in a type-safe language. However, for Java to be broadly useful, it needs additional expressive power. This paper extends Java in one area where more power is needed: support for parametric polymorphism, which allows the definition and implementation of generic abstractions. We discuss both the rationale for our design decisions and the impact of the extension on other parts of Java, including arrays and the class library. We also describe optional extensions to the Java virtual machine to allow parameterized bytecodes, and how to verify them efficiently. We have extended the Java bytecode interpreter to provide good performance for parameterized code in both execution speed and code size, without slowing down non-parameterized code.


title: A Demand-Driven Set-Based Analysis

abstract: In this paper we present an analysis technique for isolating dead code in higher-order functional programs. First, we formalize what it means for a program fragment to contribute to the value returned by the program. Next, we provide a purely declarative specification of a subset of terms which constitute dead code. This is done by a refinement of the set-based semantics technique, developed by Nevin Heintze, by the introduction of a concept of demand. We then develop a demand-driven set-based analysis to compute dead code specified by the declarative specification. The demand-driven set-based analysis developed in this paper is polynomial time, in the size of the input program.


title: The Pi-calculus in Direct Style

abstract: We introduce a calculus which is a direct extension of both the λ and the π calculi. We give a simple type system for it, that encompasses both Curry's type inference for the λ-calculus, and Milner's sorting for the π-calculus as particular cases of typing. We observe that the various continuation passing style transformations for λ-terms, written in our calculus, actually correspond to encodings already given by Milner and others for evaluation strategies of λ-terms into the π-calculus. Furthermore, the associated sortings correspond to well-known double negation translations on types. Finally we provide an adequate CPS transform from our calculus to the π-calculus. This shows that the latter may be regarded as an "assembly language", while our calculus seems to provide a better programming notation for higher-order concurrency.


title: Type-Checking Higher-Order Polymorphic Multi-Methods

authors:
François Bourdoncle
Stephan Merz

abstract: We present a new predicative and decidable type system, called ML≤, suitable for languages that integrate functional programming and parametric polymorphism in the tradition of ML [21, 28], and class-based object-oriented programming and higher-order multimethods in the tradition of CLOS [12]. Instead of using extensible records as a foundation for object-oriented extensions of functional languages, we propose to reinterpret ML datatype declarations as abstract and concrete class declarations, and to replace pattern matching on run-time values by dynamic dispatch on run-time types. ML≤ is based on universally quantified polymorphic constrained types. Constraints are conjunctions of inequalities between monotypes built from type constructors organized into extensible and partially ordered classes. We give type checking rules for a small, explicitly typed functional language á la XML [20] with multi-methods, show that the resulting system has decidable minimal types, and discuss subject reduction. Finally, we propose a new object-oriented programming language based on the ML≤ type system.


title: Program Fragments, Linking, and Modularization

abstract: Module mechanisms have received considerable theoretical attention, but the associated concepts of separate compilation and linking have not been emphasized. Anomalous module systems have emerged in functional and object-oriented programming where software components are not separately typecheckable and compilable. In this paper we provide a context where linking can be studied, and separate compilability can be formally stated and checked. We propose a framework where each module is separately compiled to a self-contained entity called a linkset; we show that separately compiled, compatible modules can be safely linked together. 1 Introduction Program modularization arose from the necessity of splitting large programs into fragments in order to compile them. As system libraries grew in size, it became essential to compile the libraries separately from the user programs; libraries acquired interfaces that minimized compilation dependencies. A linker was used to patch compiled fragmen...


title: Determining the Idle Time of a Tiling

authors:
Karin Högstedt
Larry Carter
Jeanne Ferrante

abstract: This paper investigates the idle time associated with a parallel computation, that is, the time that processors are idle because they are either waiting for data from other processors or waiting to synchronize with other processors. We study doubly-nested loops corresponding to parallelogram- or trapezoidal-shaped iteration spaces that have been parallelized by the well-known tiling transformation. We introduce the notion of rise r, which relates the shape of the iteration space to that of the tiles. For parallelogram- shaped iteration spaces, we show that when r < -2, the idle time is linear in P, the number of processors, but when r > -1, it is quadratic in P. In the context of hierarchical tiling, where multiple levels of tiling are used, a good choice of rise can lead to less idle time and better performance. While idle time is not the only cost that should be considered in evaluating a tiling strategy, current architectural trends (of deeper memory hierarchies and multiple levels of parallelism) suggest it has increasing importance.


title: Rolling Your Own MADT - A Connection Between Linear Types and Monads

authors:
Chih-Ping Chen
Paul Hudak

abstract: A methodology is described whereby a linear ADT may be rigorously encapsulated within a state monad. A CPS-like translation from the original ADT axioms into monadic ones is also described and proven correct, so that reasoning can be accomplished at the monadic level without exposing the state. The ADT axioms are suitably constrained by a linear type system to make this translation possible. This constraint also allows the state to be "updated in place," a notion made precise via a graph-rewrite operational semantics. 1 Introduction In recent years, numerous proposals for I/O, destructive updates to data structures, mutable variables, nondeterminism, and concurrency have been put forth, all using monads to structure programs in such a way that details of the computation are effectively hidden and encapsulated [18, 20]. One of the most important uses of monads is in dealing with state, resulting in a style of programming referred to appropriately by Peyton Jones and Wadler as imperativ...


title: Types as Abstract Interpretations

abstract: Starting from a denotational semantics of the eager untyped lambda-calculus with explicit runtime errors, the standard collecting semantics is defined as specifying the strongest program properties. By a first abstraction, a new sound type collecting semantics is derived in compositional fix-point form. Then by successive (semi-dual) Galois connection based abstractions, type systems and/or type inference algorithms are designed as abstract semantics or abstract interpreters approximating the type collecting semantics. This leads to a hierarchy of type systems, which is part of the lattice of abstract interpretations of the untyped lambda-calculus. This hierarchy includes two new a la Church/Curry polytype systems. Abstractions of this polytype semantics lead to classical Milner/Mycroft and Damas/Milner polymorphic type schemes, Church/Curry monotypes and Hindley principal typing algorithm. This shows that types are abstract interpretations.


title: On the Complexity of Escape Analysis

abstract: Escape analysis is an abstract interpretation technique for statically optimizing storage management devised by Park & Goldberg [30]. The main application of escape analysis is the optimization of storage management and data locality in garbage-collected languages such as ML or JAVA.We improve the previously known exponential complexity bound of Park & Goldberg: we show that first-order escape analysis (EA1) can be solved in almost linear time, and that second-order escape analysis (EA2) is DEXPTIME-hard. We exhibit a fast, equational, path-compression based abstract interpretation algorithm for EA1. We prove that it is sound and complete, and that its time complexity is O(n log2 n).We sketch an extension of the analysis to higher-order functions and imperative operations that is approximate. Finally we briefly present some experimental evidence that escape analysis may be useful in practice.


title: Shape Types

authors:
Pascal Fradet
Daniel Le Métayer

abstract: Type systems currently available for imperative languages are too weak to detect a significant class of programming errors. For example, they cannot express the property that a list is doubly-linked or circular. We propose a solution to this problem based on a notion of shape types defined as context-free graph grammars. We define graphs in set-theoretic terms, and graph modifications as multiset rewrite rules. These rules can be checked statically to ensure that they preserve the structure of the graph specified by the grammar. We provide a syntax for a smooth integration of shape types in C. The programmer can still express pointer manipulations with the expected constant time execution and benefits from the additional guarantee that the property specified by the shape type is an invariant of the program.


title: Model Checking for Programming Languages using Verisoft

abstract: Verification by state-space exploration, also often referred to as "model checking", is an effective method for analyzing the correctness of concurrent reactive systems (e.g., communication protocols). Unfortunately, existing model-checking techniques are restricted to the verification of properties of models, i.e., abstractions, of concurrent systems.In this paper, we discuss how model checking can be extended to deal directly with "actual" descriptions of concurrent systems, e.g., implementations of communication protocols written in programming languages such as C or C++. We then introduce a new search technique that is suitable for exploring the state spaces of such systems. This algorithm has been implemented in VeriSoft, a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary C code. As an example of application, we describe how VeriSoft successfully discovered an error in a 2500-line C program controlling robots operating in an unpredictable environment.


title: Automatic Verification of Parameterized Linear Networks of Processes

authors:
David Lesens
Nicolas Halbwachs
Pascal Raymond

abstract: This paper describes a method to verify safety properties of parameterized linear networks of processes. The method is based on the construction of a network invariant, defined as a fixpoint. Such invariants can often be automatically computed using heuristics based on Cousot's widening techniques. These techniques have been implemented and some non-trivial examples are presented.


title: A Unified Computation Model for Functional and Logic Programming

abstract: We propose a new computation model which combines the operational principles of functional languages (reduction), logic languages (non-deterministic search for solutions), and integrated functional logic languages (residuation and narrowing). This computation model combines efficient evaluation principles of functional languages with the problem-solving capabilities of logic programming. Since the model allows the delay of function calls which are not sufficiently instantiated, it also supports a concurrent style of programming. We provide soundness and completeness results and show that known evaluation principles of functional logic languages are particular instances of this model. Thus, our model is a suitable basis for future declarative programming languages.


title: Polyp - A Polytypic Programming Language

authors:
Patrik Jansson
Johan Jeuring

abstract: Many functions have to be written over and over again for different datatypes, either because datatypes change during the development of programs, or because functions with similar functionality are needed on different datatypes. Examples of such functions are pretty printers, debuggers, equality functions, unifiers, pattern matchers, rewriting functions, etc. Such functions are called polytypic functions. A polytypic function is a function that is defined by induction on the structure of user-defined datatypes. This paper extends a functional language (a subset of Haskell) with a construct for writing polytypic functions. The extended language type checks definitions of polytypic functions, and infers the types of all other expressions using an extension of Jones' theories of qualified types and higher-order polymorphism. The semantics of the programs in the extended language is obtained by adding type arguments to functions in a dictionary passing style. Programs in the extended language are translated to Haskell.


title: First-class Polymorphism with Type Inference

abstract: Languages like ML and Haskell encourage the view of values as first-class entities that can be passed as arguments or results of functions, or stored as components of data structures. The same languages offer parametric polymorphism, which allows the use of values that behave uniformly over a range of different types. But the combination of these features is not supported-- polymorphic values are not first-class. This restriction is sometimes attributed to the dependence of such languages on type inference, in contrast to more expressive, explicitly typed languages, like System F, that do support first-class polymorphism.This paper uses relationships between types and logic to develop a type system, FCP, that supports first-class polymorphism, type inference, and also first-class abstract datatypes. The immediate result is a more expressive language, but there are also long term implications for language design.


title: Relational Parametricity and Units of Measure

abstract: Type systems for programming languages with numeric types can be extended to support the checking of units of measure. Quantification over units then introduces a new kind of parametric polymorphism with a corresponding Reynolds-style representation independence principle: that the behaviour of programs is invariant under changes to the units used. We prove this 'dimensional invariance' result and describe four consequences. The first is that the type of an expression can be used to derive equations which describe its properties with respect to scaling (akin to Wadler's 'theorems for free' for System F). Secondly there are certain types which are inhabited only by trivial terms. For example, we prove that a fully polymorphic square root function cannot be written using just the usual arithmetic primitives. Thirdly we exhibit interesting isomorphisms between types and for first-order types relate these to the central theorem of classical dimensional analysis. Finally we suggest that for any expression whose behaviour is dimensionally invariant there exists some equivalent expression whose type reflects this behaviour, a consequence of which would be a full abstraction result for a model of the language.


title: Maximizing Parallelism and Minimizing Synchronization with Affine Transforms

authors:
Amy W. Lim
Monica S. Lam

abstract: This paper presents the first algorithm to find the optimal affine transform that maximizes the degree of parallelism while minimizing the degree of synchronization in a program with arbitrary loop nestings and affine data accesses. The problem is formulated without the use of imprecise data dependence abstractions such as data dependence vectors. The algorithm presented subsumes previously proposed program transformation algorithms that are based on unimodular transformations, loop fusion, fission, scaling, reindexing and/or statement reordering.


title: Call by Need Computations to Root-Stable Form

abstract: The following theorem of Huet and Lévy forms the basis of all results on optimal reduction strategies for orthogonal term rewriting systems: every term not in normal form contains a needed redex, and repeated contraction of needed redexes results in the normal form, if the term under consideration has one. We generalize this theorem to computations to root-stable form and we argue that the resulting notion of root-neededness is more fundamental than (other variants of) neededness when it comes to infinitary normalization.


title: Proof-Carrying Code

abstract: This paper describes proof-carrying code (PCC), a mechanism by which a host system can determine with certainty that it is safe to execute a program supplied (possibly in binary form) by an untrusted source. For this to be possible, the untrusted code producer must supply with the code a safety proof that attests to the code's adherence to a previously defined safety policy. The host can then easily and quickly validate the proof without using cryptography and without consulting any external agents.In order to gain preliminary experience with PCC, we have performed several case studies. We show in this paper how proof-carrying code might be used to develop safe assembly-language extensions of ML programs. In the context of this case study, we present and prove the adequacy of concrete representations for the safety policy, the safety proofs, and the proof validation. Finally, we briefly discuss how we use proof-carrying code to develop network packet filters that are faster than similar filters developed using other techniques and are formally guaranteed to be safe with respect to a given operating system safety policy.

awards: Most Influential POPL Paper (awarded 2007)


title: Infinitary Control Flow Analysis: a Collecting Semantics for Closure Analysis

authors:
Hanne Riis Nielson
Flemming Nielson

abstract: Defining the collecting semantics is usually the first crucial step in adapting the general methodology of abstract interpretation to the semantic framework or programming language at hand. In this paper we show how to define a collecting semantics for control flow analysis: due to the generality of the formulation we need to appeal to coinduction (or greatest fixed points) in order to define the analysis. We then prove the semantic soundness of the collecting semantics and that all totally deterministic instantiations have a least solution; this incorporates k-CFA, polymorphic splitting and a new class of uniform-k-CFA analyses.


title: Pizza into Java: Translating Theory into Practice

authors:
Martin Odersky
Philip Wadler

abstract: Pizza is a strict superset of Java that incorporates three ideas from the academic community: parametric polymorphism, higher-order functions, and algebraic data types. Pizza is defined by translation into Java and compiles into the Java Virtual Machine, requirements which strongly constrain the design space. Nonetheless, Pizza fits smoothly to Java, with only a few rough edges.


title: A Curry-Howard Foundation for Functional Computation with Control

authors:
C.-H. Luke Ong
Charles A. Stewart

abstract: We introduce the type theory λμv, a call-by-value variant of Parigot's λμ-calculus, as a Curry-Howard representation theory of classical propositional proofs. The associated rewrite system is Church-Rosser and strongly normalizing, and definitional equality of the type theory is consistent, compatible with cut, congruent and decidable. The attendant call-by-value programming language μPCFv is obtained from λμv by augmenting it by basic arithmetic, conditionals and fixpoints. We study the behavioural properties of μPCFv and show that, though simple, it is a very general language for functional computation with control: it can express all the main control constructs such as exceptions and first-class continuations. Proof-theoretically the dual λμv-constructs of naming and μ-abstraction witness the introduction and elimination rules of absurdity respectively. Computationally they give succinct expression to a kind of generic (forward) "jump" operator, which may be regarded as a unifying control construct for functional computation. Our goal is that λμv and μPCFv respectively should be to functional computation with first-class access to the flow of control what λ-calculus and PCF respectively are to pure functional programming: λμv gives the logical basis via the Curry-Howard correspondence, and μPCFv is a prototypical language albeit in purified form.


title: High Level Reading and Data Structure Compilation

authors:
Robert Paige
Zhe Yang

abstract: In [Paige89], it was shown how to simulate a set machine in real-time on a RAM that provides cursor or even only pointer access to data. The underlying assumption was that the establishment of efficient data structures would be provided by some 'client' program. In the current paper, we fill in the gap by presenting a linear-time high level reading method that translates external input in string form into data structures that facilitate such real-time simulation. The algorithm builds the data structures for a much richer type system than what appeared in [Paige94], and is powerful enough to support our reading algorithm itself in an efficient way. Consequently, it equips a high level set-theoretic language with I/O, without the loss of computational transparency.This work alleviates the burden of creating low-level data structures manually, and builds the internal pointer-based inputs required by most pointer algorithms [Ben-Amram95] from the external string representation.


title: Comparing the Expressive Power of the Synchronous and the Asynchronous pi-calculus

abstract: The Asynchronous π-calculus, as recently proposed by Boudol and, independently, by Honda and Tokoro, is a subset of the π-calculus which contains no explicit operators for choice and output-prefixing. The communication mechanism of this calculus, however, is powerful enough to simulate output-prefixing, as shown by Boudol, and input-guarded choice, as shown recently by Nestmann and Pierce. A natural question arises, then, whether or not it is possible to embed in it the full π-calculus. We show that this is not possible, i.e. there does not exist any uniform, parallel-preserving, translation from the π-calculus into the asynchronous π-calculus, up to any "reasonable" notion of equivalence. This result is based on the incapablity of the asynchronous π-calculus of breaking certain symmetries possibly present in the initial communication graph. By similar arguments, we prove a separation result between the π-calculus and CCS.


title: Reducing Nondeterminism while Specializing Logic Programs

authors:
Alberto Pettorossi
Maurizio Proietti
Sophie Renault

abstract: Program specialization is a collection of program transformation techniques for improving program efficiency by exploiting some information available at compile-time about the input data. We show that current techniques for program specialization based on partial evaluation do not perform well on nondeterministic logic programs. We then consider a set of transformation rules which extend the ones used for partial evaluation, and we propose a strategy to direct the application of these extended rules so to derive very efficient specialized programs. The efficiency improvements which may even be exponential, are achieved because the derived programs are semi-deterministic and the operations which are performed by the initial programs in different branches of the computation trees, are performed in the specialized programs within single branches. We also make use of mode information to guide the unfolding process and to reduce nondeterminism. To exemplify our technique, we show that we can automatically derive very efficient semi-deterministic matching programs and semi-deterministic parsers for regular languages. The derivations we have performed could not have been done by previously known partial evaluation techniques.


title: Behavioral Equivalence in the Polymorphic Pi-calculus

authors:
Benjamin C. Pierce
Davide Sangiorgi

abstract: We investigate parametric polymorphism in message-based concurrent programming, focusing on behavioral equivalences in a typed process calculus analogous to the polymorphic lambda-calculus of Girard and Reynolds.Polymorphism constrains the power of observers by preventing them from directly manipulating data values whose types are abstract, leading to notions of equivalence much coarser than the standard untyped ones. We study the nature of these constraints through simple examples of concurrent abstract data types and develop basic theoretical machinery for establishing bisimilarity of polymorphic processes.We also observe some surprising interactions between polymorphism and aliasing, drawing examples from both the polymorphic pi-calculus and ML.


title: Is "Just in Time" = "Better Late than Never"?

authors:
Michael P. Plezbert
Ron Cytron

abstract: The World-Wide Web is emerging as a medium for distributing platform-independent, intermediate-form programs. Most Java vendors have recently announced plans to construct "just-in-time" systems, which translate the intermediate text into native code on demand. In this paper, we present experiments that show the benefits of just-in-time systems as compared with the traditional (compile prior to execution) systems. We introduce a new method--the continuous compiler-- that can outperform just-in-time systems by overlapping compilation with program interpretation and native execution. Based on those results, we then present a smart just-in-time system that blends interpretation with native-code execution, thereby obtaining improved performance.


title: Minimal Typings in Atomic Subtyping

abstract: This paper studies the problem of simplifying typings and the size-complexity of most general typings in typed programming languages with atomic subtyping. We define a notion of minimal typings relating all typings which are equivalent with respect to instantiation. The notion of instance is that of Fuh and Mishra [13], which supports many interesting simplifications. We prove that every typable term has a unique minimal typing, which is the logically most succinct among all equivalent typings. We study completeness properties, with respect to our notion of minimality, of well-known simplification techniques. Drawing upon these results, we prove a tight exponential lower bound for the worst case dag-size of constraint sets as well as of types in most general typings. To the best of our knowledge, the best previously proven lower bound was linear. 1 Introduction Subtyping is a fundamental idea in type systems for programming languages, which can in principle be integrated into standar...


title: Objective ML: A Simple Object-Oriented Extension of ML

authors:
Didier Rémy
Jerome Vouillon

abstract: Objective ML is a small practical extension of ML with objects and toplevel classes. It is fully compatible with ML; its type system is based on ML polymorphism, record types with polymorphic access, and a better treatment of type abbreviations. Objective ML allows for most features of object-oriented languages including multiple inheritance, methods returning self and binary methods as well as parametric classes. This demonstrates that objects can be added to strongly typed languages based on ML polymorphism.


title: Synchronization Transformations for Parallel Computing

authors:
Pedro C. Diniz
Martin C. Rinard

abstract: As parallel machines become part of the mainstream computing environment, compilers will need to apply synchronization optimizations to deliver efficient parallel software. This paper describes a new framework for synchronization optimizations and a new set of transformations for programs that implement critical sections using mutual exclusion locks. These transformations allow the compiler to move constructs that acquire and release locks both within and between procedures and to eliminate acquire and release constructs.The paper also presents a new synchronization algorithm, lock elimination, for reducing synchronization overhead. This optimization locates computations that repeatedly acquire and release the same lock, then uses the transformations to obtain equivalent computations that acquire and release the lock only once. Experimental results from a parallelizing compiler for object-based programs illustrate the practical utility of this optimization. For three benchmark programs the optimization dramatically reduces the number of times the computations acquire and release locks, which significantly reduces the amount of time processors spend acquiring and releasing locks. For one of the three benchmarks, the optimization always significantly improves the overall performance. Depending on the number of processors executing the computation, the optimized version runs between 2.11 and 1.83 times faster than the unoptimized version. For one of the other benchmarks, the optimized version runs between 1.13 and 0.96 times faster than the unoptimized version, with a mean of 1.08 times faster. For the final benchmark, the optimization reduces the overall performance.


title: Partitioning Dataflow Analyses Using Types

abstract: We present a simple method for partitioning a dataflow analysis problem into a series of related subproblems. We use type information (either declared by the programmer, or computed via nonstandard type inference) to conservatively approximate analysis-time data dependences between program quantities. This dependence information frees us from the need to model all program quantities simultaneously in a single, monolithic analysis. Instead, we can model quantities in any order, or even in parallel, so long as we respect the dependences. Our approach is independent of the means used to solve the subproblems, and enables the wider application of existing sparse approaches previously restricted to "separable" dataflow problems. Preliminary experiments applying our technique to flow-sensitive points-to analysis of C programs have achieved storage savings of 1.3-7.2x over existing methods.


title: Typing Algorithm in Type Theory with Inheritance

abstract: We propose and study a new typing algorithm for dependent type theory. This new algorithm typechecks more terms by using inheritance between classes. This inheritance mechanism turns out to be powerful: it supports multiple inheritance, classes with parameters and uses new abstract classes FUNCLASS and SORTCLASS (respectively classes of functions and sorts). We also defines classes as records, particularily suitable for the formal development of mathematical theories. This mechanism, implemented in the proof checker Coq, can be adapted to all typed -calculus. 1 Introduction In the last years, proof checkers based on type theory appeared as convincing systems to formalize mathematics (especially constructive mathematics) and to prove correctness of software and hardware. In a proof checker, one can interactively build definitions, statements and proofs. The system is then able to check automatically whether the definitions are well-formed and the proofs are correct. Modern systems ar...