title: A Study of the Applicability of Existing Exception-Handling Techniques to Component-Base Real-Time Software Technology

authors:
Jun Lang
David B. Stewart

abstract: This study focuses on the current state of error-handling technology and concludes with recommendations for further research in error handling for component-based real-time software. With real-time programs growing in size and complexity, the quality and cost of developing and maintaining them are still deep concerns to embedded software industries. Component-based software is a promising approach in reducing development cost while increasing quality and reliability. As with any other real-time software, component-based software needs exception detection and handling mechanisms to satisfy reliability requirements. The current lack of suitable error-handling techniques can make an application composed of reusable software nondeterministic and difficult to understand in the presence of errors.


venue: toplas

title: Proofs about a Folklore Let-Polymorphic Type Inference Algorithm

authors:
Oukseh Lee
Kwangkeun Yi

abstract: The Hindley/Milner let-polymorphic type inference system has two different algorithms: one is the de facto standard Algorithm 𝒲 that is bottom-up (or context-insensitive), and the other is a “folklore” algorithm that is top-down (or context-sensitive). Because the latter algorithm has not been formally presented with its soundness and completeness proofs, and its relation with the 𝒲 algorithm has not been rigorously investigated, its use in place of (or in combination with) 𝒲 is not well founded. In this article, we formally define the context-sensitive, top-down type inference algorithm (named “M”), prove its soundness and completeness, and show a distinguishing property that M always stops earlier than 𝒲 if the input program is ill typed. Our proofs can be seen as theoretical justifications for various type-checking strategies being used in practice.


title: Controlling Generalization amd Polyvariance in Partial Deduction of Normal Logic Programs

authors:
Michael Leuschel
Bern Martens
Danny De Schreye

abstract: Given a program and some input data, partial deduction computes a specialized program handling any remaining input more efficiently. However, controlling the process well is a rather difficult problem. In this article, we elaborate global control for partial deduction: for which atoms, among possibly infinitely many, should specialized relations be produced, meanwhile guaranteeing correctness as well as termination? Our work is based on two ingredients. First, we use the concept of a characteristic tree, encapsulating specialization behavior rather than syntactic structure, to guide generalization and polyvariance, and we show how this can be done in a correct and elegant way. Second, we structure combinations of atoms and associated characteristic trees in global trees registering “causal” relationships among such pairs. This allows us to spot looming nontermination and perform proper generalization in order to avert the danger, without having to impose a depth bound on characteristic trees. The practical relevance and benefits of the work are illustrated through extensive experiments. Finally, a similar approach may improve upon current (on-line) control strategies for program transformation in general such as (positive) supercompilation of functional programs. It also seems valuable in the context of abstract interpretation to handle infinite domains of infinite height with more precision.


title: Static Caching for Incremental Computation

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

abstract: A systematic approach is given for deriving incremental programs that exploit caching. The cache-and-prune method presented in the article consists of three stages: (I) the original program is extended to cache the results of all its intermediate subcomputations as well as the final result, (II)) the extended program is incrementalized so that computation on a new input can use all intermediate results on an old input, and (III) unused results cached by the extended program and maintained by the incremental program are pruned away, leaving a pruned extended program that caches only useful intermediate results and a pruned incremental program that uses and maintains only useful results. All three stages utilize static analyses and semantics-preserving transformations. Stages I and III are simple, clean, and fully automatable. The overall method has a kind of optimality with respect to the techniques used in Stage II. The method can be applied straightfowardly to provide a systematic approach to program improvement via caching.


title: Equality-based flow analysis versus recursive types

abstract: Equality-based control-flow analysis has been studied by Henglein, Bondorf and Jørgensen, DeFouw, Grove, and Chambers, and others. It is faster than the subset-based-0-CFA, but also more approximate. Heintze asserted in 1995 that a program can be safety checked with an equality-based control-flow analysis if and only if it can be typed with recursive types. In this article we falsify Heintze's assertion, and we present a type system equivalent to equality-based control-flow analysis. The new type system contains both recursive types and an unusual notion of subtyping. We have s ≤ t if s and t unfold to the same regular tree, and we have ⊥≤t≤⊤ where t is a function type. In particular, there is no nontrivial subtyping between function types.


title: Constraint-Based Array Dependence Analysis

authors:
William W. Pugh
David Wonnacott

abstract: Traditional array dependence analysis, which detects potential memory aliasing of array references is a key analysis technique for automatic parallelization. Recent studies of benchmark codes indicate that limitations of analysis cause many compilers to overlook large amounts of potential parallelism, and that exploiting this parallelism requires algorithms to answer new question about array references, not just get better answers to the old questions of aliasing. We need to ask about the flow of values in arrays, to check the legality of array privatization, and about the conditions under which a dependence exists, to obtain information about conditional parallelism. In some cases, we must answer these questions about code containing nonlinear terms in loop bounds or subscripts. This article describes techniques for phrasing these questions in terms of systems of contstraints. Conditional dependence analysis can be performed with a constraint operation we call the "gist" operation. When subscripts and loop bounds are affine, questions about the flow of values in array variables can be phrased in terms of Presburger Arithmetic. When the constraints describing a dependence are not affine, we introduce uninterpreted function symbols to represent the nonaffine terms. Our constraint language also provides a rich language for communication with the dependence analyzer, by either the programmer or other phases of the compiler. This article also documents our investigations of the praticality of our approach. The worst-case complexity of Presburger Arithmetic indicates that it might be unsuitable for any practical application. However, we have found that analysis of benchmark programs does not cause the exponential growth in the number of constraints that could occur in the worst case. We have studied the constraints produced during our aanalysis, and identified characteristics that keep our algorithms free of exponential behavior in practice.


title: "Maximal-munch" Tokenization in Linear Time

abstract: The lexical-analysis (or scanning) phase of a compiler attempts to partition an input string into a sequence of tokens. The convention in most languages is that the input is scanned left to right, and each token identified is a “maximal munch” of the remaining input—the longest prefix of the remaining input that is a token of the language. Although most of the standard compiler textbooks present a way to perform maximal-munch tokenization, the algorithm they describe is one that, for certain sets of token definitions, can cause the scanner to exhibit quadratic behavior in the worst case. In the article, we show that maximal-munch tokenization can always be performed in time linear in the size of the input.


title: The Design, Implementation, and Evaluation of Jade

authors:
Martin C. Rinard
Monica S. Lam

abstract: Jade is a portable, implicitly parallel language designed for exploiting task-level concurrency.Jade programmers start with a program written in a standard serial, imperative language, then use Jade constructs to declare how parts of the program access data. The Jade implementation uses this data access information to automatically extract the concurrency and map the application onto the machine at hand. The resulting parallel execution preserves the semantics of the original serial program. We have implemented Jade as an extension to C, and Jade implementations exist for s hared-memory multiprocessors, homogeneous message-passing machines, and heterogeneous networks of workstations. In this atricle we discuss the design goals and decisions that determined the final form of Jade and present an overview of the Jade implementation. We also present our experience using Jade to implement several complete scientific and engineering applications. We use this experience to evaluate how the different Jade language features were used in practice and how well Jade as a whole supports the process of developing parallel applications. We find that the basic idea of preserving the serial semantics simplifies the program development process, and that the concept of using data access specifications to guide the parallelization offers significant advantages over more traditional control-based approaches. We also find that the Jade data model can interact poorly with concurrency patterns that write disjoint pieces of a single aggregate data structure, although this problem arises in only one of the applications.


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

authors:
Shmuel Sagiv
Thomas W. Reps
Reinhard Wilhelm

abstract: This article concerns the static analysis of programs that perform destructive updating on heap-allocated storage. We give an algorithm that uses finite shape graphs to approximate conservatively the possible “shapes” that heap-allocated structures in a program can take on. For certain programs, our technique is able to determine such properties as (1) when the input to the program is a list, the output is also a list and (2) when the input to the program is a tree, the output is also a tree. For example, the method can determine that “listness” is preserved by (1) a program that performs list reversal via destructive updating of the input list and (2) a program that searches a list and splices a new element into the list. None of the previously known methods that use graphs to model the program's store are capable of determining that “listness” is preserved on these examples (or examples of similar complexity). In contrast with most previous work, our shape analysis algorithm is even accurate for certain programs that update cyclic data structures; that is, it is sometimes able to show that when the input to the program is a circular list, the output is also a circular list. For example, the shape-analysis algorithm can determine that an insertion into a circular list preserves “circular listness.”


title: An Abstract Machine for Tabled Execution of Fixed-Order Stratified Logic Programs

authors:
Konstantinos Sagonas
Terrance Swift

abstract: SLG resolution uses tabling to evaluate nonfloundering normal logic pr ograms according to the well-founded semantics. The SLG-WAM, which forms the engine of the XSB system, can compute in-memory recursive queries anorder of magnitute fasterthan current deductive databases. At the same time, the SLG-WAM tightly intergrates Prolog code with tabled SLG code, and executes Prolog code with minimal overhead compared to the WAM. As a result, the SLG-WAM brings to logic programming important termination and complexity properties of deductive databases. This article describes the architecture of the SLG-WAM for a powerful class of programs, the class offixed-order dynamically stratified programs. We offer a detailed description of the algorithms, data structures, and instructions that the SLG-WAM adds to the WAM, and a performance analysis of engine overhead due to the extensions.


title: A New Framework for Elimination-Based Data Flow Analysis Using DJ Graphs

authors:
Vugranam C. Sreedhar
Guang R. Gao
Yong-Fong Lee

abstract: In this article, we present a new framework for elimination-based exhaustive and incremental data flow analysis using the DJ graph representation of a program.Unlike previous approaches to elimination-based incremental data flow analysis, our approach can handle arbitrary structural and nonstructural changes to program flowgraphs, including irreducibility.We show how our approach is related to dominance frontiers, and we exploit this relationship to establish the complexity of our exhaustive analysis and to aid the design of our incremental analysis.


title: A Region Inference Algorithm

authors:
Mads Tofte
Lars Birkedal

abstract: Region Inference is a program analysis which infers lifetimes of values. It is targeted at a runtime model in which the store consists of a stack of regions and memory management predominantly consists of pushing and popping regions, rather than performing garbage collection. Region Inference has previously been specified by a set of inference rules which formalize when regions may be allocated and deallocated. This article presents an algorithm which implements the specification. We prove that the algorithm is sound with respect to the region inference rules and that it always terminates even though the region inference rules permit polymorphic recursion in regions. The algorithm is the result of several years of experiments with region inference algorithms in the ML Kit, a compiler from Standard ML to assembly language. We report on practical experience with the algorithm and give hints on how to implement it.


title: Efficient and Flexible Incremental Parsing

authors:
Tim A. Wagner
Susan L. Graham

abstract: Previously published algorithms for LR ( k ) incremental parsing are inefficient, unnecessarily restrictive, and in some cases incorrect. We present a simple algorithm based on parsing LR( k ) sentential forms that can incrementally parse an arbitrary number of textual and/or structural modifications in optimal time and with no storage overhead. The central role of balanced sequences in achieving truly incremental behavior from analysis algorithms is described, along with automated methods to support balancing during parse table generation and parsing. Our approach extends the theory of sentential-form parsing to allow for ambiguity in the grammar, exploiting it for notational convenience, to denote sequences, and to construct compact (“abstract”) syntax trees directly. Combined, these techniques make the use of automatically generated incremental parsers in interactive software development environments both practical and effective. In addition, we address information preservation in these environments: Optimal node reuse is defined; previous definitions are shown to be insufficient; and a method for detecting node reuse is provided that is both simpler and faster than existing techniques. A program representation based on self-versioning documents is used to detect changes in the program, generate efficient change reports for subsequent analyses, and allow the parsing transformation itself to be treated as a reversible modification in the edit log.


title: Polymorphic Splitting: An Effective Polyvariant Flow Analysis

authors:
Andrew K. Wright
Suresh Jagannathan

abstract: This article describes a general-purpose program analysis that computes global control-flow and data-flow information for higher-order, call-by-value languages. The analysis employs a novel form of polyvariance called polymorhic splitting that uses let-expressions as syntactic clues to gain precision. The information derived from the analysis is used both to eliminate run-time checks and to inline procedure. The analysis and optimizations have been applied to a suite of Scheme programs. Experimental results obtained from the prototype implementation indicate that the analysis is extremely precise and has reasonable cost. Compared to monovariant flow analyses such as 0CFA, or analyses based on type inference such as soft typing, the analysis eliminates significantly more run-time checks. Run-time check elimination and inlining together typically yield a 20 to 40% performance improvement for the benchmark suite, with some programs running four times as fast.


title: Space/Time-Efficient Scheduling and Execution of Parallel Irregular Computations

authors:
Tao Yang
Cong Fu

abstract: In this article we investigate the trade-off between time and space efficiency in scheduling and executing parallel irregular computations on distributed-memory machines. We employ acyclic task dependence graphs to model irregular parallelism with mixed granularity, and we use direct remote memory access to support fast communication. We propose new scheduling techniques and a run-time active memory management scheme to improve memory utilization while retaining good time efficiency, and we provide a theoretical analysis on correctness and performance. This work is implemented in the context of the RAPID system which uses an inspector/executor approach to parallelize irregular computations at run-ti me. We demostrate the effectiveness of the proposed techniques on several irregular applications such as sparse matrix code and the fast multipole method for particle simulation. Our experimental results on Cray-T3E show that problems large sizes can be solved under limited space capacity, and that the loss of execution efficiency caused by the extra memory management overhead is reasonable.


title: On Failure of the Pruning Technique in "Error Repair in Shift-Reduce Parsers"

authors:
Eberhard Bertsch
Mark-Jan Nederhof

abstract: A previous article presented a technique to compute the least-cost error repair by incrementally generating configurations that result from inserting and deleting tokens a syntactically incorrect input. An additional mechanism to improve the run-time efficiency of this algorithm by pruning some of the configurations was discussed as well. In this communication we show that the pruning mechanism may lead to suboptimal repairs or may block all repairs. Certain grammatical errors in a common construct of the Java programming language also lead to the above kind of failure.


title: Dependency analysis for Standard ML

abstract: Automatic dependency analysis is a useful addition to a system like CM, our compilation manager for Standard ML of New Jersey. It relieves the programmer from the tedious and error-prone task of having to specify compilation dependencies by hand and thereby makes its usage more user friendly. But dependency analysis is not easy, as the general problem for Standard ML is NP-complete. Therefore, CM has to impose certain restrictions on the programming language to recover tractability. We prove the NP-completeness result, discuss the restrictions on ML that are used by CM, and provide the resulting analysis algorithms.


title: Hierarchical modularity

authors:
Matthias Blume
Andrew W. Appel

abstract: To cope with the complexity of very large systems, it is not sufficient to divide them into simple pieces because the pieces themselves will either be too numerous or too large. A hierarchical modular structure is the natural solution. In this article we explain how that approach can be applied to software. Our compilation manager provides a language for specifying where individual modules fit into a hierarchy and how they are related semantically. We pay particular attention to the structure of the global name space of program identifiers that are used for module linkage because any potential for name clashes between otherwise unrelated parts of a program can negatively affect modularity. We discuss the theoretical issues in building software hierarchically, and we describe our implementation of CM, the compilation manager for Standard ML of New Jersey.


title: Specification and dialogue control of visual interaction through visual rewriting systems

authors:
Paolo Bottoni
Maria Francesca Costabile
Piero Mussio

abstract: Computers are increasingly being seen not only as computing tools but more so as communication tools, thus placing special emphasis on human-computer interaction (HCI). In this article, the focus is on visual HCI, where the messages exchanged between human and computer are images appearing on the computer screen, as usual in current popular user interfaces. We formalize interactive sessions of a human-computer dialogue as a structured set of legal visual sentences, i.e., as a visual language, and show how rewriting systems can be generalized to specify both the pictorial and the computational aspects of visual languages. To this end, Visual Conditional Attributed Rewriting (VCARW) systems are introduced, and use for specification of visual languages. These specifications are given as inputs to a procedure illustrated in the article as a system of algorithms, which automatically generates control mechanisms of the interaction, thus favoring the design of more reliable and usable systems.


title: Effectivness of Abstract Interpretation in Automatic Parallelization: A Case Study in Logic Programming

authors:
Francisco Bueno
Maria J. García de la Banda
Manuel V. Hermenegildo

abstract: We report on a detailed study of the application and effectiveness of program analysis based on abstract interpretation of automatic program parallelization. We study the case of parallelizing logic programs using the notion of strict independence. We first propose and prove correct a methodology for the application in the parallelization task of the information inferred by abstract interpretation, using a parametric domain. The methodology is generic in the sense of allowing the use of different analysis domains. A number of well-known approximation domains are then studied and the transformation into the parametric domain defined. The transformation directly illustrates the revelance and applicability of each abstract domain for the application. Both local and global analyzers are then built using these domains and embedded in a complete parallelizing compiler. Then, the performance of the domains in this context is assessed through a number of experiments. A comparatively wide range of aspects is studied, from the resources needed by the analyzers in terms of time and memory to the actual benefits obtained from the information inferred. Such benefits are evaluated both in terms of the characteristics of the parallelized code and of the actual speedups obtained from it. The results show that data flow analysis plays an important role in achieving efficient parallelizations, and that the cost of such analysis con be reasonable even for quite sophisticated abstract domains. Furthermore, the results also offer significant insight into the characteristics of the domains, the demands of the application, and the trade-offs involved.


title: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results

authors:
Tevfik Bultan
Richard Gerber
William W. Pugh

abstract: Model checking is a powerful technique for analyzing large, finite-state systems. In an infinite state system, however, many basic properties are undecidable. In this article, we present a new symbolic model checker which conservatively evaluates safety and liveness properties on programs with unbounded integer variables. We use Presburger formulas to symbolically encode a program's transition system, as well as its model-checking computations. All fixpoint calculations are executed symbolically, and their convergence is guaranteed by using approximation techniques. We demonstrate the promise of this technology on some well-known infinite-state concurrency problems.


title: Reasoning about Grover's quantum search algorithm using probabilistic wp

authors:
Michael J. Butler
Pieter H. Hartel

abstract: Grover's search algorithm is designed to be executed on a quantum-mechanical computer. In this article, the probabilistic wp -calculus is used to model and reason about Grover's algorithm. It is demonstrated that the calculus provides a rigorous programming notation for modeling this and other quantum algorithms and that it also provides a systematic framework of analyzing such algorithms.


title: Sharing and groundness dependencies in logic programs

authors:
Michael Codish
Harald Søndergaard
Peter J. Stuckey

abstract: We investigate Jacobs and Langen's Sharing domain, introduced for the analysis of variable sharing in logic programs, and show that it is isomorphic to Marriott and Søndergaard's Pos domain, introduced for the analysis of groundness dependencies. Our key idea is to view the sets of variables in a Sharing domain element as the models of a corresponding Boolean function. This leads to a recasting of sharing analysis in terms of the property of “not being affected by the binding of a single variable.” Such an “unaffectedness dependency” analysis has close connections with groundness dependency analysis using positive Boolean functions. This new view improves our understanding of sharing analysis, and leads to an elegant expression of its combination with groundness dependency analysis based on the reduced product of Sharing and Pos. It also opens up new avenues for the efficient implementation of sharing analysis, for example using reduced order binary decision diagrams, as well as efficient implementation of the reduced product, using domain factorizations.


title: Constraint-based termination analysis of logic programs

authors:
Stefaan Decorte
Danny De Schreye
Henk Vandecasteele

abstract: Current norm-based automatic termination analysis techniques for logic programs can be split up into different components: inference of mode or type information, derivation of models, generation of well-founded orders, and verification of the termination conditions themselves. Although providing high-precision results, these techniques suffer from an efficiency point of view, as several of these analyses are often performed through abstract interpretation. We present a new termination analysis which integrates the various components and produces a set of constraints that, when solvable, identifies successful termination proofs. The proposed method is both efficient and precise. The use of constraint sets enables the propagation on information over all different phases while the need for multiple analyses is considerably reduced.


title: Dynamic Typing for Distributed Programming in Polymorphic Languages

abstract: While static typing is widely accepted as being necessary for secure program execution, dynamic typing is also viewed as being essential in some applications, particularly for distributed programming environments. Dynamics have been proposed as a language construct for dynamic typing, based on experience with languages such as CLU, Cedar/Mesa, and Modula-3. However proposals for incorporating dynamic typing into languages with parametric polymorphism have serious shortcomings. A new approach is presented to extending polymorphic lnanguages with dynamic typing. At the heart of the approach is the use of dynamic type dispatch, where polymorphic functions may analyze the structure of their type arguments. This approach solves several open problems with the traditional approach to adding dynamic typing to polymorphic languages. An explicity typed language XML dyn is presented; this language uses refinement kinds to ensure that dynamic type dispatch does not fail at run-time. Safe dynamics are a new form of dynamics that use refinement kinds to statically check the use of run-time dynamic typing. Run-time errors are isolated to a separate construct for performing run-time type checks


title: Componential Set-Based Analysis

authors:
Cormac Flanagan
Matthias Felleisen

abstract: Set-based analysis (SBA) produces good predictions about the behavior of functional and object-oriented programs. The analysis proceeds by inferring constraints that characterize the data flow relationships of the analyzed program. Experiences with MrSpidey, a static debugger based on SBA, indicate that SBA can adequately deal with programs of up to a couple of thousand lines of code. SBA fails, however, to cope with larger programs because it generates systems of constraints that are at least linear, and possibility quadratic, in the size of the analyzed program. This article presents theoretical and practical results concerning methods for reducing the size of constraint systems. The theoretical results include of proof-theoretic characterization of the observable behavior of constraint systems for program components, and a complete algorithm for deciding the observable equivalence of constraint systems. In the course of this development we establish a close connection between the observable equivalence of constraint systems and the equivalence of regular-tree grammars. We then exploit this connection to adapt a variety of algoirthms for simplifying grammars to the problem of simplifying constraint systems. Based on the resulting algorithms, we have developed componential set-based analysis , a modular and polymorphic variant of SBA. Experimental results verify the effectiveness of the simplification algorithms and the componential analysis. The simplified constraint systems are typically an order of magnitude smaller than the original systems. These reductions in size produce significant gains in the speed of the analysis.


title: The type system for object initializatiion in the Jave bytecode language

authors:
Stephen N. Freund
John C. Mitchell

abstract: In the standard Java implementation, a Java language program is compiled to Java bytecode. This bytecode may be sent across the network to another site, where it is then executed by the Java Virtual Machine. Since bytecode may be written by hand, or corrupted during network transmission, the Java Virtual Machine contains a bytecode verifier that performs a number of consistency checks before code is run. These checks include type correctness and, as illus-trated by previous attacks on the Java Virtual Machine, are critical for system security. In order to analyze existing bytecode verifiers and to understand the properties that should be verified, we develop a precise specification of statically correct Java bytecode, in the form of a type system. Our focus in this article is a subset of the bytecode language dealing with object creation and initialization. For this subset, we prove, that, for every Java bytecode program that satisfies our typing constraints, every object is initialized before it is used. The type system is easily combined with a previous system developed by Stata and Abadi for bytecode subroutines. Our analysis of subroutines and object initialization reveals a previously unpub-lished bug in the Sun JDK bytecode verifier.


title: Cache miss equations: a compiler framework for analyzing and tuning memory behavior

authors:
Somnath Ghosh
Margaret Martonosi
Sharad Malik

abstract: With the ever-widening performance gap between processors and main memory, cache memory, which is used to bridge this gap, is becoming more and more significant. Caches work well for programs that exhibit sufficient locality. Other programs, however, have reference patterns that fail to exploit the cache, thereby suffering heavily from high memory latency. In order to get high cache efficiency and achieve good program performance, efficient memory accessing behavior is necessary. In fact, for many programs, program transformations or source-code changes can radically alter memory access patterns, significantly improving cache performance. Both hand-tuning and compiler optimization techniques are often used to transform codes to improve cache utilization. Unfortunately, cache conflicts are difficult to predict and estimate, precluding effective transformations. Hence, effective transformations require detailed knowledge about the frequency and causes of cache misses in the code. This article describes methods for generating and solving Cache Miss Equations (CMEs) that give a detailed representation of cache behavior, including conflict misses, in loop-oriented scientific code. Implemented within the SUIF compiler framework, our approach extends traditional compiler reuse analysis to generate linear Diophantine equations that summarize each loop's memory behavior. While solving these equations is in general difficult, we show that is also unnecessary, as mathematical techniques for manipulating Diophantine equations allow us to relatively easily compute and/or reduce the number of possible solutions, where each solution corresponds to a potential cache miss. The mathematical precision of CMEs allows us to find true optimal solutions for transformations such as blocking or padding. The generality of CMEs also allows us to reason about interactions between transformations applied in concert. The article also gives examples of their use to determine array padding and offset amounts that minimize cache misses, and to determine optimal blocking factors for tiled code. Overall, these equations represent an analysis framework that offers the generality and precision needed for detailed compiler optimizations.


title: Procedure placement using temporal-ordering information

authors:
Nicholas C. Gloy
Michael D. Smith

abstract: Instruction cache performance is important to instruction fetch efficiency and overall processor performance. The layout of an executable has a substantial effect on the cache miss rate and the instruction working set size during execution. This means that the performance of an executable can be improved by applying a code-placement algorithm that minimizes instruction cache conflicts and improves spatial locality. We describe an algorithm for procedure placement, one type of code placement, that signicantly differs from previous approaches in the type of information used to drive the placement algorithm. In particular, we gather temporal-ordering information that summarizes the interleaving of procedures in a program trace. Our algorithm uses this information along with cache configuration and procedure size information to better estimate the conflict cost of a potential procedure ordering. It optimizes the procedure placement for single level and multilevel caches. In addition to reducing instruction cache conflicts, the algorithm simultaneously minimizes the instruction working set size of the program. We compare the performance of our algorithm with a particularly successful procedure-placement algorithm and show noticeable improvements in the instruction cache behavior, while maintaining the same instruction working set size.


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. Understanding the performance characteristics of such evaluation, however, requires having a detailed understanding of the implementation. For example, the particular implementaion technique used to suspend and reactivate threads can have an asymptotic effect on performance. With the goal of giving the users some understanding of performance without requiring them to understand the implementation, we present a provable implementation bound for a language based on speculative evaluation. The idea is (1) to supply the users with a semantics for a language that defines abstract costs for measuring or analyzing the performance of computations, (2) to supply the users with a mapping of these costs onto runtimes on various machine models, and (3) to describe an implementation strategy of the language and prove that it meets these mappings. For this purpose we consider a simple language based on speculative evaluation. For every computation, the semantics of the language returns a directed acyclic graph (DAG) in which each node represents a unit of computation, and each edge represents a dependence. We then describe an implementation strategy of the language and show that any computation with w work (the number of nodes in the DAG) and d depth (the length of the longest path in the DAG) will run on a p -processor PRAM in O ( w / p + d log p ) time. The bounds are work efficient (within a constant factor of linear speedup) when there is sufficient parallelism, w / d ≥ p log p . These are the first time bounds we know of for languages with speculative evaluation. The main challenge is in parallelizing the necessary queuing operations on suspended threads.


title: Compile-time memory reuse in logic programming languages through update in place

authors:
Gudjon Gudjonsson
William H. Winsborough

abstract: Standard implementation techniques for single-assignment languages modify a data structure without destroying the original, which may subsequently be accessed. Instead a variant structure is created by using newly allocated cells to represent the changed portion and to replace any cell that references a newly allocated cell. The rest of the original structure is shared by the variant. The effort required to leave the original uncorrupted is unnecessary when the program will never reference the original again. This effort includes allocating and initializing new cells, as well as garbage collecting replaced cells. This article specifies a transformation system that introduces update-in-place operations, making Prolog programs update recursive data structures much as an imperative program would. The article introduces the notion of a reuse map, which formalizes reallocation decisions. Because optimal memory reuse is intractable, a heuristical method is presented that performs well in practice. Small Prolog programs that manipulate recursive data structures have their speed increased up to about five times (naive recurse), not counting any speedup obtained by avoiding garbage collection. Quicksort is about three times as fast, merge-sort about one and a half, matrix transposition about twice, and Gaussian elimination is about 1.2 times as fast.


title: Efficient logic variables for distributed computing

authors:
Seif Haridi
Peter Van Roy
Per Brand
Michael Mehl
Ralf Scheidhauer
Gert Smolka

abstract: We define a practical algorithm for distrubuted rational tree unification and prove its correctness in both the off-line and on-line cases. We derive the distributed algorithm from a centralized one, showing clearly the trade-offs between local and distributed execution. The algorithm is used to realize logic variables in the Mozart Programming System, which implements the Oz language (see http://www/mozart-oz.org). Oz appears to the programmer as a concurrent object-oriented language with dataflow synchronization. Logic variables implement the dataflow behavior. We show that lohgic variables can easily be added to the more restricted models of Java and ML, thus providing an alternative way to do concurent programming in these languages. We present common distributed programming idioms in a network-transparent way using logic variables. We show that in common cases the algorithm maintains the same message latency as explicit message passing. In addition, it is able to handle uncommon cases that arise from the properties of latency tolerance and third-party independence. This is evidence that using logic variables in distributed computing is beneficial at both the system and language levels. At the system level, they improve latency tolerance and third-party independence. At the language level, they help make network-transparent distribution practical.


title: Interprocedural pointer alias analysis

authors:
Michael Hind
Michael G. Burke
Paul R. Carini
Jong-Deok Choi

abstract: We present practical approximation methods for computing and representing interprocedural aliases for a program written in a language that includes pointers, reference parameters, and recursion. We present the following contributions: (1) a framework for interprocedural pointer alias analysis that handles function pointers by constructing the program call graph while alias analysis is being performed; (2) a flow-sensitive interprocedural pointer alias analysis algorithm; (3) a flow-insensitive interprocedural pointer alias analysis algorithm; (4) a flow-insensitive interprocedural pointer alias analysis algorithm that incorporates kill information to improve precision; (5) empirical measurements of the efficiency and precision of the three interprocedural alias analysis algorithms.


title: A global communication optimization technique based on data-flow analysis and linear algebra

authors:
Mahmut T. Kandemir
Prithviraj Banerjee
Alok N. Choudhary
J. Ramanujam
U. Nagaraj Shenoy

abstract: Reducing communication overhead is extremely important in distributed-memory message-passing architectures. In this article, we present a technique to improve communication that considers data access patterns of the entire program. Our approach is based on a combination of traditional data-flow analysis and a linear algebra framework, and it works on structured programs with conditional statements and nested loops but without arbitrary goto statements.The distinctive features of the solution are the accuracy in keeping communication set information, support for general alignments and distributions including block-cyclic distribu-tions, and the ability to simulate some of the previous approaches with suitable modifications. We also show how optimizations such as message vectorization, message coalescing, and redundancy elimination are supported by our framework. Experimental results on several benchmarks show that our technique is effective in reducing the number of messages (anaverage of 32% reduction), the volume of the data communicated (an average of 37%reduction), and the execution time (an average of 26% reduction).


title: Partial redundancy elimination in SSA form

authors:
Robert Kennedy
Sun Chan
Shin-Ming Liu
Raymond Lo
Peng Tu
Fred C. Chow

abstract: The SSAPRE algorithm for performing partial redundancy elimination based entirely on SSA form is presented. The algorithm is formulated based on a new conceptual framework, the factored redundancy graph, for analyzing redundancy, and representes the first sparse approach to the classical problem and on methods for its solution. With the algorithm description, theorems and their proofs are given showing that the algorithm produces the best possible code by the criteria of computational optimality and lifetime optimality of the introduced temporaries. In addition to the base algorithm, a practical implementation of SSAPRE that exhibits additional compile-time efficiencies is described. In closing, measurement statistics are provided that characterize the instances of the partial redundancy problem from a set of benchmark programs and compare optimization time spent by an implementation of SSAPRE aganist a classical partial redundancy elimination implementation. The data lend insight into the nature of partial redundancy elimination and demonstrate the expediency of this new approach.


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 an attractive object of theoretical study and a clean 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 behavior. In particular, we can guarantee that two processes communicating over a linear channel cannot interfere with other communicating processes. 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. For an extended example of the theory, we prove the validity of a tail-call optimization for higher-order functions represented as processes.


title: Should your specification language be typed

authors:
Leslie Lamport
Lawrence C. Paulson

abstract: Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language without types. This possibility, which has been widely overlooked, offers many advantages. Untyped set theory is simple and is more flexible than any simple typed formalism. Polymorphism, overloading, and subtyping can make a type system more powerful, but at the cost of increased somplexity, and such refinements can never attain the flexibility of having no types at all. Typed formalisms have advantages, too, stemming from the power of mechanical type checking. While types serve little purpose in hand proofs, they do help with mechanized proofs. In the absence of verificaiton, type checking can catch errors in specifications. It may be possible to have the best of both worlds by adding typing annotations to an untyped specification language. We consider only specification languages, not programming languages.


title: Specification and Verification of Fault-Tolerance, Timing, and Scheduling

authors:
Zhiming Liu
Mathai Joseph

abstract: Fault-tolerance and timing have often been considered to be implementation issues of a program, quite distinct from the functional safety and liveness properties. Recent work has shown how these non-functional and functional properties can be verified in a similar way. However, the more practical question of determining whether a real-time program will meet its deadlines, i.e., showing that there is a feasible schedule, is usually done using scheduling theory, quite separately from the verification of other properties of the program. This makes it hard to use the results of scheduling analysis in the design, or redesign, of fault-tolerant and real-time programs. This article shows how fault-tolerance, timing, and schedulability can be specified and verified using a single notation and model. This allows a unified view to be taken of the functional and nonfunctional properties of programs and a simple transformational method to be usedto combine these properties. It also permits results from scheduling theory to be interpreted and used within a formal proof framework. The notation and model are illustrated using a simple example.


title: Specificational functions

authors:
Joseph M. Morris
Alexander Bunkenburg

abstract: Mathematics supplies us with various operators for creating functions from relations, sets, known functions, and so on. Function inversion is a simple example. These operations are useful in specifying programs. However, many of them have strong constraints on their arguments to ensure that the result is indeed a function. For example, only functions that are bijective may be inverted. This is a serious impediment to their use in specifications, because at best it limits the specifier's expressive power, and at worst it imposes strong proof obligations on the programmer. We propose to loosen the definition of functions so that the constraints on operations such as inversion can be greatly relaxed. The specificational functions that emerge generalize traditional functions in that their application to some arguments may yield no good outcome, while for other arguments their application may yield any of several outcomes unpredictably. While these functions are not in general algorithmic, they can serve as specifications of traditional functions as embodied in programming languages. The idea of specificational functions is not new, but accommodating them in all their generality without falling foul of a myriad of anomalies has proved elusive. We investigate the technical problems that have hindered their use, and propose solutions. In particular, we develop a formal axiomatization for reasoning about specificational functions, and we prove its consistency by constructing a model.


title: From system F to typed assembly language

authors:
J. Gregory Morrisett
David Walker
Karl Crary
Neal Glew

abstract: We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratctions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violatet these abstractionsl In addition, the typing constructs admit many low-level compiler optimiztaions. Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.


title: Space-Efficient Scheduling of Nested Parallelism

authors:
Girija J. Narlikar
Guy E. Blelloch

abstract: Many of today's high-level parallel languages support dynamic, fine-grained parallelism. These languages allow the user to expose all the parallelism in the program, which is typically of a much higher degree than the number of processors. Hence an efficient scheduling algorithm is required to assign computations to processors at runtime. Besides having low overheads and good load balancing, it is important for the scheduling algorithm to minimize the space usage of the parallel program. This article presents an on-line scheduling algorithm that is provably space efficient and time efficient for nested-parallel languages. For a computation with depth D and serial space requirement S 1 , the algorithm generates a schedule that requires at most S 1 + O (K•D•p ) space (including scheduler space) on p processors. Here, K is a user-adjustable runtime parameter specifying the net amount of memory that a thread may allocate before it is preempted by the scheduler. Adjusting the value of K provides a trade-off between the running time and the memory requirement of a parallel computation. To allow the scheduler to scale with the number of processors we also parallelize the scheduler and analyze the space and time bounds of the computation to include scheduling costs. In addition to showing that the scheduling algorithm is space and time efficient in theory, we demonstrate that it is effective in practice. We have implemented a runtime system that uses our algorithm to schedule lightweight parallel threads. The results of executing parallel programs on this system show that our scheduling algorithm significantly reduces memory usage compared to previous techniques, without compromising performance.


title: 'C and tcc: A Language and Compiler for Dynamic Code Generation

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

abstract: Dynamic code generation allows programmers to use run-time information in order to achieve performance and expressiveness superior to those of static code. The 'C(Tick C) language is a superset of ANSI C that supports efficient and high-level use of dynamic code generation. 'C provides dynamic code generation at the level of C expressions and statements and supports the composition of dynamic code at run time. These features enable programmers to add dynamic code generation to existing C code incrementally and to write important applications (such as “just-in-time” compilers) easily. The article presents many examples of how 'C can be used to solve practical problems. The tcc compiler is an efficient, portable, and freely available implementation of 'C. tcc allows programmers to trade dynamic compilation speed for dynamic code quality: in some aplications, it is most important to generate code quickly, while in others code quality matters more than compilation speed. The overhead of dynamic compilation is on the order of 100 to 600 cycles per generated instruction, depending on the level of dynamic optimizaton. Measurements show that the use of dynamic code generation can improve performance by almost an order of magnitude; two- to four-fold speedups are common. In most cases, the overhead of dynamic compilation is recovered in under 100 uses of the dynamic code; sometimes it can be recovered within one use.


title: Linear scan register allocation

authors:
Massimiliano Poletto
Vivek Sarkar

abstract: We describe a new algorithm for fast global register allocation called linear scan . This algorithm is not based on graph coloring, but allocates registers to variables in a single linear-time scan of the variables' live ranges. The linear scan algorithm is considerably faster than algorithms based on graph coloring, is simple to implement, and results in code that is almost as efficient as that obtained using more complex and time-consuming register allocators based on graph coloring. The algorithm is of interest in applications where compile time is a concern, such as dynamic compilation systems, “just-in-time” compilers, and interactive development environments.


title: Identifying Loops in Almost Linear Time

abstract: Loop identification is an essential step in performing various loop optimizations and transformations. The classical algorithm for identifying loops is Tarjan's interval-finding algorithm, which is restricted to reducible graphs. More recently, serveral people have proposed extensions to Tarjan's algortihm to deal with irreducible graphs. Havlak presents one such extension, which constructs a loop-nesting forest for an arbitrary flow graph. We show that the running time of this algorithm is quadratic in the worst-case, and not almost linear as claimed. We then show how to modify the algorithm to make it run in almost linear time. We next consider the quadratic algorithm presented by Sreedhar et al. which constructs a loop-nesting forest different from the one constructed by Havlak algorithm. We show that this algorithm too can be adapted to run in almost linear time. We finally consider an algorithm due to Steensgaard, which constructs yet antoher loop-nesting forest. We show how this algorithm can be made more efficient by borrowing ideas from the other algorithms discussed earlier.


title: Techniques for the Translation of MATLAB Programs into Fortran 90

authors:
Luiz De Rose
David A. Padua

abstract: This article describes the main techiques developed for FALCON's MATLAB-to-Fortran 90 compiler. FALCON is a programming environment for the development of high-performance scientific programs. It combines static and dynamic inference methods to translate MATLAB programs into Fortran 90. The static inference is supported with advanced value propagation techniques and symbolic algorithms for subscript analysis. Experiments show that FALCON's MATLAB translator can generate code that performs more than 1000 times faster than the interpreted version of MATLAB and substantially faster than commercially available MATLAB compilers on one processor of an SGI Power Challenge. Futhermore, in most cases we have tested, the compiler-generated code is as fast as corresponding hand-written programs.


title: A Type System for Java Bytecode Subroutines

authors:
Raymie Stata
Martín Abadi

abstract: Java is typically compiled into an intermediate language, JVML, that is interpreted by the Java Virtual Machine. Because mobile JVML code is not always trusted, a bytecode verifier enforces static constraints that prevent various dynamic errors. Given the importance of the bytecode verifier for security, its current descriptions are inadequate. This article proposes using typing rules to describe the bytecode verifier because they are more precise than prose, clearer than code, and easier to reason about than either. JVML has a subroutine construct which is used for the compilation of Java's try-finally statement. Subroutines are a major source of complexity for the bytecode verifier because they are not obviously last-in/first-out and because they require a kind of polymorphism. Focusing on subroutines, we isolate an interesting, small subset of JVML. We give typing rules for this subset and prove their correctness. Our type system constitutes a sound basis for bytecode verification and a rational reconstruction of a delicate part of Sun's bytecode verifier.


title: Static correlated branch prediction

authors:
Cliff Young
Michael D. Smith

abstract: Recent work in history-based branch prediction uses novel hardware structures to capture branch correlation and increase branch prediction accuracy. Branch correlation occurs when the outcome of a conditional branch can be accurately predicted by observing the outcomes of previously executed branches in the dynamic instruction stream. In this article, we show how to instrument a program so that it is practical to collect run-time statistics that indicate where branch correlation occurs, and we then show how to use these statistics to transform the program so that its static branch prediction accuracy is improved. The run-time information that we gather is called a path profile , and it summarizes how often each executed sequence of program points occurs in the program trace. Our path proles are more general than those previously proposed. The code transformation that we present is called static correlated branch prediction (SCBP). It exhibits better branch prediction accuracy than previously thought possible for static prediction techniques. Furthermore, through the use of an overpruning heuristic, we show that it is possible to determine automatically an appropriate trade-off between code expansion and branch predictability so that our transformation improves the performance of multiple-issue, deeply pipelined microprocessors like those being built today.


title: The role of commutativity in constraint propagation algorithms

abstract: Constraing propagation algorithms form an important part of most of the constraint programming systems. We provide here a simple, yet very general framework that allows us to explain several constraint propagation algorithms in a systematic way. In this framework we proceed in two steps. First, we introduce a generic iteration algorithm on partial orderings and prove its correctness in an abstract setting. Then we instantiate this algorithm with specific partial orderings and functions to obtain specific constraint propagation algorithms. In particular, using the notions commutativity and semi-commutativity, we show that the AC-3, PC-2, DAC, and DPC algorithms for achieving (directional) arc consistency and (directional) path consistency are instances of a single generic algorithm. The work reported here extends and simplifies that of Apt [1999a].


title: Graph rewrite systems for program optimization

abstract: Graph rewrite systems can be used to specify and generate program optimizations. For termination of the systems several rule-based criteria are developed, defining exhaustive graph rewrite systems . For nondeterministic systems stratification is introduced which automatically selects single normal forms. To illustrate how far the methodology reaches, parts of the lazy code motion optimization are specified. The resulting graph rewrite system classes can be evaluated by a uniform algorithm, which forms the basis for the optimizer generator OPTIMIX. With this tool several optimizer components have been generated, and some numbers on their speed are presented.


title: Independence in CLP languages

authors:
Maria J. García de la Banda
Manuel V. Hermenegildo
Kim Marriott

abstract: Studying independence of goals has proven very useful in the context of logic programming. In particular, it has provided a formal basis for powerful automatic parallelization tools, since independence ensures that two goals may be evaluated in parallel while preserving correctness and efficiency. We extend the concept of independence to constraint logic programs (CLP) and prove that it also ensures the correctness and efficiency of the parallel evaluation of independent goals. Independence for CLP languages is more complex than for logic programming as search space preservation is necessary but no longer sufficient for ensuring correctness and efficiency. Two additional issues arise. The first is that the cost of constraint solving may depend upon the order constraints are encountered. The second is the need to handle dynamic scheduling. We clarify these issues by proposing various types of search independence and constraint solver independence, and show how they can be combined to allow different optimizations, from parallelism to intelligent backtracking. Suficient conditions for independence which can be evaluated “a priori” at run-time are also proposed. Our study also yields new insights into independence in logic programming languages. In particular, we show that search space preservation is not only a sufficient but also a necessary condition for ensuring correctness and efficiency of parallel execution.


title: Java bytecode compression for low-end embedded systems

authors:
Lars Ræder Clausen
Ulrik Pagh Schultz
Charles Consel
Gilles Muller

abstract: A program executing on a low-end embedded system, such as a smart-card, faces scarce memory resources and fixed execution time constraints. We demonstrate that factorization of common instruction sequences in Java bytecode allows the memory footprint to be reduced, on average, to 85% of its original size, with a minimal execution time penalty. While preserving Java compatibility, our solution requires only a few modifications which are straightforward to implement in any JVM used in a low-end embedded system.


title: Compiler techniques for code compaction

authors:
Saumya K. Debray
William S. Evans
Robert Muth
Bjorn De Sutter

abstract: In recent years there has been an increasing trend toward the incorpor ation of computers into a variety of devices where the amount of memory available is limited. This makes it desirable to try to reduce the size of applications where possible. This article explores the use of compiler techniques to accomplish code compaction to yield smaller executables. The main contribution of this article is to show that careful, aggressive, interprocedural optimization, together with procedural abstraction of repeated code fragments, can yield significantly better reductions in code size than previous approaches, which have generally focused on abstraction of repeated instruction sequences. We also show how “equivalent” code fragments can be detected and factored out using conventional compiler techniques, and without having to resort to purely linear treatments of code sequences as in suffix-tree-based approaches, thereby setting up a framework for code compaction that can be more flexible in its treatment of what code fragments are considered equivalent. Our ideas have been implemented in the form of a binary-rewriting tool that reduces the size of executables by about 30% on the average.


title: Sets and constraint logic programming

authors:
Agostino Dovier
Carla Piazza
Enrico Pontelli
Gianfranco Rossi

abstract: In this paper we present a study of the problem of handling constraints made by conjunctions of positive and negative literals based on the predicate symbols =, ∈,∪ and || (i.e., disjointness of two sets) in a (hybrid) universe of finite sets . We also review and compare the main techniques considered to represent finite sets in the context of logic languages. The resulting contraint algorithms are embedded in a Constraint Logic Programming (CLP) language which provides finite sets—along with basic set-theoretic operations—as first-class objects of the language. The language—called CLP( SET )—is an instance of the general CLP framework, and as such it inherits all the general features and theoretical results of this scheme. We provide, through programming examples, a taste of the expressive power offered by programming in CLP( SET ).


title: Lazy rewriting on eager machinery

authors:
Wan J. Fokkink
Jasper Kamperman
Pum Walters

abstract: The article introduces a novel notion of lazy rewriting. By annotating argument positions as lazy, redundant rewrite steps are avoided, and the termination behavior of a term-rewriting system can be improved. Some transformations of rewrite rules enable an implementation using the same primitives as an implementation of eager rewriting.


title: The benefits and costs of DyC's run-time optimizations

authors:
Brian Grant
Markus Mock
Matthai Philipose
Craig Chambers
Susan J. Eggers

abstract: DyC selectively dynamically compiles programs during their execution, utilizing the run-time-computed values of variables and data structures to apply optimizations that are based on partial evaluation. The dynamic optimizations are preplanned at static compile time in order to reduce their run-time cost; we call this staging . DyC's staged optimizations include (1) an advanced binding-time analysis that supports polyvariant specialization (enabling both single-way and multiway complete loop unrolling), polyvariant division, static loads, and static calls, (2) low-cost, dynamic versions of traditional global optimizations, such as zero and copy propagation and dead-assignment elimination, and (3) dynamic peephole optimizations, such as strength reduction. Because of this large suite of optimizations and its low dynamic compilation overhead, DyC achieves good performance improvements on programs that are larger and more complex than the kernels previously targeted by other dynamic compilation systems. This paper evaluates the benefits and costs of applying DyC's optimizations. We assess their impact on the performance of a variety of small to medium-sized programs, both for the regions of code that are actually transformed and for the entire application as a whole. Our study includes an analysis of the contribution to performance of individual optimizations, the performance effect of changing the applications' inputs, and a detailed accounting of dynamic compilation costs.


title: Syntactic type abstraction

authors:
Dan Grossman
J. Gregory Morrisett
Steve Zdancewic

abstract: Software developers often structure programs in such a way that different pieces of code constitute distinct principals . Types help define the protocol by which these principals interact. In particular, abstract types allow a principal to make strong assumptions about how well-typed clients use the facilities that it provides. We show how the notions of principals and type abstraction can be formalized within a language. Different principals can know the implementation of different abstract types. We use additional syntax to track the flow of values with abstract types during the evaluation of a program and demonstrate how this framework supports syntactic proofs (in the sytle of subject reduction) for type-abstraction properties. Such properties have traditionally required semantic arguments; using syntax aboids the need to build a model and recursive typesfor the language. We present various typed lambda calculi with principals, including versions that have mutable state and recursive types.


title: A balanced code placement framework

authors:
Reinhard von Hanxleden
Ken Kennedy

abstract: Give-N-Take is a code placement framework which uses a generic producer-consumer mechanism. An instance of this could be a communication step between a processor that computes (produces) some data, and other processors that subsequently reference (consume) these data in an expression. An advantage of Give-N-Take over traditional partial redundancy elimination techniques is its concept of production regions , instead of single locations, which can be beneficial for general latency hiding. Give-N-Take also guarantees balanced production, i.e., each production will be started and stopped exactly once. The framework can also take advantage of production coming “for free,” as induced by side effects, without disturbing balance. Give-N-Take can place production either before or after consumption, and it also provides the option to speculatively hoist code out of potentially zero-trip loop (nest) constructs. Give-N-Take uses a fast elimination method based on Tarjan intervals, with a complexity linear in the program size in most cases. We have implemented Give-N-Take as partof a Fortran D compiler prototype, where it solves various communication generation problems associated with compiling data-parallel languages onto distributed-memory architectures.


title: Incremental analysis of constraint logic programs

authors:
Manuel V. Hermenegildo
Germán Puebla
Kim Marriott
Peter J. Stuckey

abstract: Global analyzers traditionally read and analyze the entire program at once, in a nonincremental way. However, there are many situations which are not well suited to this simple model and which instead require reanalysis of certain parts of a program which has already been analyzed. In these cases, it appears inefficient to perform the analysis of the program again from scratch, as needs to be done with current systems. We describe how the fixed-point algorithms used in current generic analysis engines for (constraint) logic programming languages can be extended to support incremental analysis. The possible changes to a program are classified into three types: addition, deletion, and arbitrary change. For each one of these, we provide one or more algorithms for identifying the parts of the analysis that must be recomputed and for performing the actual recomputation. The potential benefits and drawbacks of these algorithms are discussed. Finally, we present some experimental results obtained with an implementation of the algorithms in the PLAI generic abstract interpretation framework. The results show significant benefits when using the proposed incremental analysis algorithms.


title: Automated data-member layout of help objects to improve memory-hierarchy performance

authors:
Thomas Kistler
Michael Franz

abstract: We present and evaluate a simple, yet efficient optimization technique that improves memory-hierarchy performance for pointer-centric applications by up to 24% and reduces cache misses by up to 35%. This is achieved by selecting an improved ordering for the data members of pointer-based data structures. Our optimization is applicable to all type-safe programming languages that completely abstract from physical storage layout; examples of such languages are Java and Oberon. Our technique does not involve programmers in the optimization process, but runs fully automatically, guided by dynamic profiling information that captures which paths through the program are taken with that frequencey. The algorithm first strives to cluster data members that are accessed closely after one another onto the same cache line, increasing spatial locality. Then, the data members that have been mapped to a particular cache line are ordered to minimize load latency in case of a cache miss.


title: An automata-theortetic approach to modular model checking

authors:
Orna Kupferman
Moshe Y. Vardi

abstract: In modular verification the specification of a module consists of two part. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is interacting. This is called the assume-guarantee paradigm. In this paper we consider assume-guarantee specifications in which the guarantee is specified by branching temporal formulas. We distinguish between two approaches. In the first approach, the assumption is specified by branching temporal formulas too. In the second approach, the assumption is specified by linear temporal logic. We consider guarantees in ∀CTL, and ∀CTL*. We develop two fundamental techniques: building maximal models for ∀CTL and ∀CTL* formulas and using alternating automata to obtain space-efficient algorithms for fair model checking. Using these techniques we classify the complexity of satisfiability, validity, implication, and modular verification for ∀CTL and ∀CTL*. We show that modular verification is PSPACE-complete for ∀CTL and is EXSPACE-complete for ∀CTL*. We prove that when the assumption is linear, these bounds hold also for guarantees in CTL and CTL*. On the other hand, the problem remains EXSPACE-hard even when we restrict the assumptions to LTL and take the guarantees as a fixed ∀CTL formula.


title: Type-based analysis of uncaught exceptions

authors:
Xavier Leroy
François Pessaux

abstract: This article presents a program analysis to estimate uncaught exceptions in ML programs. This analysis relies on unification-based type inference in a nonstandard type system, using rows to approximate both the flow of escaping exceptions (a la effect systems) and the flow of result values (a la control-flow analyses). The resulting analysis is efficient and precise; in particular, arguments carried by exceptions are accurately handled.


title: Fusion-based register allocation

authors:
Guei-Yuan Lueh
Thomas R. Gross
Ali-Reza Adl-Tabatabai

abstract: The register allocation phase of a compiler maps live ranges of a program to registers. If there are more candidates than there are physical registers, the register allocator must spill a live range (the home location is in memory) or split a live range (the live range occupies multiple locations). One of the challenges for a register allocator is to deal with spilling and splitting together. Fusion-based register allocation uses the structure of the program to make splitting and spilling decisions, with the goal to move overhead operations to infrequently executed parts of a program. The basic idea of fusion-based register allocation is to build up the interference graph. Starting with some base region (e.g., a basic block, a loop), the register allocator adds basic blocks to the region and incrementallly builds the interference graph. When there are more live ranges than registers, the register allocator selects live ranges to split; these live ranges are split along the edge that was most recently added to the region. This article describes fusion-based register allocation in detail and compares it with other approaches to register allocation. For programs from the SPEC92 suite, fusion-based register allocation can improve the execution time (of optimized programs, for the MIPS architecture) by up to 8.4% over Chaitin-style register allocation.


title: Extending Graham-Glanville techniques for optimal code generation

authors:
Maya Madhavan
Priti Shankar
Siddhartha Rai
U. Ramakrishna

abstract: We propose a new technique for constructing code-generator generators, which combines the advantages of the Graham-Glanville parsing technique and the bottom-up tree parsing approach. Machine descriptions are similar to Yacc specifications. The construction effectively generates a pushdown automaton as the matching device. This device is able to handle ambigious grammars, and can be used to generate locally optimal code without the use of heuristics. Cost computations are performed at preprocessing time. The class of regular tree grammars augmented with costs that can be handled by our system properly includes those that can be handled by bottom-up systems based on finite-state tree parsing automata. Parsing time is linear in the size of the subject tree. We have tested the system on specifications for some systems and report table sizes.


title: From flop to megaflops: Java for technical computing

authors:
José E. Moreira
Samuel P. Midkiff
Manish Gupta

abstract: Although there has been some experimentation with Java as a language for numerically intensive computing, there is a perception by many that the language is unsuited for such work because of performance deficiencies. In this article we show how optimizing array bounds checks and null pointer checks creates loop nests on which aggressive optimizations can be used. Applying these optimizations by hand to a simple matrix-multiply test case leads to Java-compliant programs whose performance is in excess of 500 Mflops on a four-processor 332MHz RS/6000 model F50 computer. We also report in this article the effect that various optimizations have on the performance of six floating-point-intensive benchmarks. Through these optimizations we have been able to achieve with Java at least 80% of the peak Fortran performance on the same benchmarks. Since all of these optimizations can be automated, we conclude that Java will soon be a serious contender for numerically intensive computing.


title: Local type inference

authors:
Benjamin C. Pierce
David N. Turner

abstract: We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes in the syntax tree, without long-distance constraints such as unification variables. One method infers type arguments in polymorphic applications using a local constraint solver. The other infers annotations on bound variables in function abstractions by propagating type constraints downward from enclosing application nodes. We motivate our design choices by a statistical analysis of the uses of type inference in a sizable body of existing ML code.


title: Standard fixpoint iteration for Java bytecode verification

abstract: Java bytecode verification forms the basis for Java-based Internet security and needs a rigorous description. One important aspect of bytecode verification is to check if a Java Virtual Machine (JVM) program is statically well-typed. So far, several formal specifications have been proposed to define what the static well-typedness means. This paper takes a step further and presents a chaotic fixpoint iteration, which represents a family of fixpoint computation strategies to compute a least type for each JVM program within a finite number of iteration steps. Since a transfer function in the iteration is not monotone, we choose to follow the example of a nonstandard fixpoint theorem, which requires that all transfer functions are increasing, and monotone in case the bigger element is already a fixpoint. The resulting least type is the artificial top element if and only if he JVM program is not statically well-typed. The iteration is standard and close to Sun's informal specification and most commercial bytecode verifiers.


title: Optimizing memory usage in the polyhedral model

authors:
Fabien Quilleré
Sanjay V. Rajopadhye

abstract: The polyhedral model provides a single unified foundation for systolic array synthesis and automatic parallelization of loop programs. We investigate the problem of memory reuse when compiling Alpha (a functional language based on this model). Direct compilation would require unacceptably large memory (for example O(n 3 ) for matrix multiplication). Researchers have previously addressed the problem of memory reuse, and the analysis that this entails for projective memory allocations. This paper addresses, for a given schedule, the choice of the projections so as to minimize the volume of the residual memory. We prove tight bounds on the number of linearly independent projection vectors. Our method is constructive, yielding an optimal memory allocation. We extend the method to modular functions, and deal with the subsequent problems of code generation. Our ideas are illustrated on a number of examples generated by the current version of the Alpha compiler.


title: Context-sensitive synchronization-sensitive analysis is undecidable

abstract: Static program analysis is concerned with the computation of approximations of the runtime behavior of programs. Precise information about a program's runtime behavior is, in general, uncomputable for various different reasons, and each reason may necessitate making certain approximations in the information computed. This article illustrates one source of difficulty in static analysis of concurrent programs. Specifically, the article shows that an analysis that is simultaneously both context-sensitive and synchronization-sensitive (that is, a context-sensitive analysis that precisely takes into account the constraints on execution order imposed by the synchronization statements in the program) is impossible even for the simplest of analysis problems.


title: Undecidability of context-sensitive data-independence analysis

abstract: A number of program-analysis problems can be tackled by transforming them into certain kinds of graph-reachability problems in labeled directed graphs. The edge labels can be used to filter out paths that are not interest: a path P from vertex s to vertex t only counts as a“valid connection” between s and t if the word spelled out by P is in a certain language. Often the languages used for such filtering purposes are languages of matching parantheses. In some cases, the matched-parenthesis condition is used to filter out paths with mismatched calls and returns. This leads to so-called “context- sensitive ” program analyses, such as context- sensitive interprocedural slicing and context- sensitive interprocedural dataflow analysis. In other cases, the matched-parenthesis condition is used to capture a graph-theoretic analog of McCarthy's rules: “car (cons(x,y)) = x” and “cdr(cons(x,y)) =y”. That is, in the code fragment c = cons(a,b); d = car(c); the fact that there is a “structure-transmitted data-dependence” from a to d, but not from b to d, is captured in a graph by (1) using a vertex for each variable, (2)an edge from vertex i to vertex j when i is used on the right-hand side of an assignment to j , (3) parentheses that match as the labels on the edges that run from a to c and c to d, and (4) parentheses that do not match as the labels on the edges that run from a to c and c to d. However, structure-transmitted data-dependence analysis is context- insensitive , because there are no constraints that filter out paths with mismatched calls and returns. Thus, a natural question is whether these two kinds of uses of parentheses can be combined to create a context- sensitive analysis for structure-transmitted data-dependences. This article answers the question in the negative: in general, the problem of context sensitive , structure-transmitted data-dependence analysis is undecidable. The results imply that in general, both context- sensitive set-based analysis and ∞-CFA (when data constructors and selectors and selectors are taken into account) are also undecidable.


title: Efficient and safe-for-space closure conversion

authors:
Zhong Shao
Andrew W. Appel

abstract: Modern compilers often implement function calls (or returns) in two steps: first, a “closure” environment is properly installed to provide access for free variables in the target program fragment; second, the control is transferred to the target by a “jump with arguments (for results).” Closure conversion—which decides where and how to represent closures at runtime—is a crucial step in the compilation of functional languages. This paper presents a new algorithm that exploits the use of compile-time control and data-flow information to optimize funtion calls. By extensive closure sharing and allocation by 36% and memory fetches for local and global variables by 43%; and improves the already efficient code generated by an earlier version of the Standard ML of New Jersey compiler by about 17% on a DECstation 5000. Moreover, unlike most other approaches, our new closure-allocation scheme the strong safe-for-space-complexity rule, thus achieving good asymptotic space usage.


title: Understanding class hierarchies using concept analysis

authors:
Gregor Snelting
Frank Tip

abstract: A new method is presented for analyzing and reengineering class hierarchies. In our approach, a class hierarchy is processed along with a set of applications that use it, and a fine-grained analysis of the access and subtype relationships between objects, variables, and class members is performed. The result of this analysis is again a class hierarchy, which is guaranteed to be behaviorally equivalent to the original hierarchy, but in which each object only contains the members that are required. Our method is semantically well-founded in concept analysis : the new class hierarchy is a minimal and maximally factorized concept lattice that reflects the access and subtype relationships between variables, objects and class members. The method is primarily intended as a tool for finding imperfections in the design of class hierarchies, and can be used as the basis for tools that largely automate the process of reengineering such hierachies. The method can also be used as a space-optimizing source-to-source transformation that removes redundant fields from objects. A prototype implementation for Java has been constructed, and used to conduct several case studies. Our results demonstrate that the method can provide valuable insights into the usage of a class hierarchy in a specific context, and lead to useful restructuring proposals.


title: Generation of LR parsers by partial evaluation

authors:
Michael Sperber
Peter Thiemann

abstract: The combination of modern programming languages and partial evaluation yields new approaches to old problems. In particular, the combination of functional programming and partial evaluation can turn a general parser into a parser generator. We use an inherently functional approach to implement general LR( k ) parsers and specialize them with respect to the input grammars using offline partial evaluation. The functional specification of LR parsing yields a concise implementation of the algorithms themselves. Furthermore, we demonstrate the elegance of the functional approach by incorporating on-the-fly attribute evaluation for S-attributed grammars and two schemes for error recovery, which lend themselves to natural and elegant implementation. The parser require only minor changes to achieve good specialization results. The generated parsers have production quality and match those produced by traditional parser generators in sped and compactness


title: Program transformation and runtime support for threaded MPI execution on shared-memory machines

authors:
Hong Tang
Kai Shen
Tao Yang

abstract: Parallel programs written in MPI have been widely used for developing high-performance applications on various platforms. Because of a restriction of the MPI computation model, conventional MPI implementations on shared-memory machines map each MPI node to an OS process, which can suffer serious performance degradation in the presence of multiprogramming. This paper studies compile-time and runtime techniques for enhancing performance portability of MPI code running on multiprogrammed shared-memory machines. The proposed techniques allow MPI nodes to be executed safety and efficiently as threads. Compile-time transformation eliminates global and static variables in C code using node-specific data. The runtime support includes an efficient and provably correct communication protocol that uses lock-free data structure and takes advantage of address space sharing among threads. The experiments on SGI Origin 2000 show that our MPI prototype called TMPI using the proposed techniques is competitive with SGI's native MPI implementation in a dedicated environment, and that it has significant performance advantages in a multiprogrammed environment.


title: Typed memory management via static capabilities

authors:
David Walker
Karl Crary
J. Gregory Morrisett

abstract: Region-based memory management is an alternative to standard tracing garbage collection that makes operation such as memory deallocation explicit but verifiably safe. In this article, we present a new compiler intermediate language, called the Capability Language (CL), that supports region-based memory management and enjoys a provably safe type systems. Unlike previous region-based type system, region lifetimes need not be lexically scoped, and yet the language may be checked for safety without complex analyses. Therefore, our type system may be deployed in settings such as extensible operating systems where both the performance and safety of untrusted code is important. The central novelty of the language is the use of static capabilities to specify the permissibility of various operations, such as memory access and deallocation. In order to ensure capabilities are relinquished properly, the type system tracks aliasing information using a form of bounded quantification. Moreover, unlike previous work on region-based type systems, the proof of soundness of our type system is relatively simple, employing only standard syntactic techniques. In order to show how our language may be used in practice, we show how to translate a variant of Tofte and Talpin's high-level type-and-effects system for region-based memory management into our language. When combined with known region inference algorithms, this translation provides a way to compile source-level languages to CL.


title: Integrating object-oriented programming and protected objects in Ada 95

authors:
Andy J. Wellings
Bob Johnson
Bo Ingvar Sandén
Jörg Kienzle
Thomas Wolf
Stephen Michell

abstract: Integrating concurrent and object-oriented programming has been an active research topic since the late 1980's. There is a now a plethora of methods for achieving this integration. The majority of approaches have taken a sequential object-oriented language and made it concurrent. A few approaches have taken a concurrent language and made it object-oriented. The most important of this latter class is the Ada 95 language, which is an extension to the object-based concurrent programming language Ada 83. Arguably, Ada 95 does not fully integrate its models of concurrency and object-oriented programming. For example, neither tasks nor protected objects are extensible. This article discusses ways in which protected objects can be made more extensible.


title: Model checking of hierarchical state machines

authors:
Rajeev Alur
Mihalis Yannakakis

abstract: Model checking is emerging as a practical tool for detecting logical errors in early stages of system design. We investigate the model checking of sequential hierarchical (nested) systems, i.e., finite-state machines whose states themselves can be other machines. This nesting ability is common in various software design methodologies, and is available in several commercial modeling tools. The straightforward way to analyze a hierarchical machine is to flatten it (thus incurring an exponential blow up) and apply a model-checking tool on the resulting ordinary FSM. We show that this flattening can be avoided. We develop algorithms for verifying linear-time requirements whose complexity is polynomial in the size of the hierarchical machine. We also address the verification of branching time requirements and provide efficient algorithms and matching lower bounds.


title: An indexed model of recursive types for foundational proof-carrying code

authors:
Andrew W. Appel
David A. McAllester

abstract: The proofs of "traditional" proof carrying code (PCC) are type-specialized in the sense that they require axioms about a specific type system. In contrast, the proofs of foundational PCC explicitly define all required types and explicitly prove all the required properties of those types assuming only a fixed foundation of mathematics such as higher-order logic. Foundational PCC is both more flexible and more secure than type-specialized PCC.For foundational PCC we need semantic models of type systems on von Neumann machines. Previous models have been either too weak (lacking general recursive types and first-class function-pointers), too complex (requiring machine-checkable proofs of large bodies of computability theory), or not obviously applicable to von Neumann machines. Our new model is strong, simple, and works either in λ-calculus or on Pentiums.


title: Synthesis of concurrent programs for an atomic read/write model of computation

authors:
Paul C. Attie
E. Allen Emerson

abstract: Methods for mechanically synthesizing concurrent programs for temporal logic specifications have been proposed by Emerson and Clarke and by Manna and Wolper. An important advantage of these synthesis methods is that they obviate the need to manually compose a program and manually construct a proof of its correctness. A serious drawback of these methods in practice, however, is that they produce concurrent programs for models of computation that are often unrealistic, involving highly centralized system architecture (Manna and Wolper), processes with global information about the system state (Emerson and Clarke), or reactive modules that can read all of their inputs in one atomic step (Anuchitanukul and Manna, and Pnueli and Rosner). Even simple synchronization protocols based on atomic read/write primitives such as Peterson's solution to the mutual exclusion problem have remained outside the scope of practical mechanical synthesis methods. In this paper, we show how to mechanically synthesize in more realistic computational models solutions to synchronization problems. We illustrate the method by synthesizing Peterson's solution to the mutual exclusion problem.


title: Semiring-based contstraint logic programming: syntax and semantics

authors:
Stefano Bistarelli
Ugo Montanari
Francesca Rossi

abstract: We extend the Constraint Logic Programming (CLP) formalism in order to handle semiring-based constraints. This allows us to perform in the same language both constraint solving and optimization. In fact, constraints based on semirings are able to model both classical constraint solving and more sophisticated features like uncertainty, probability, fuzziness, and optimization. We then provide this class of languages with three equivalent semantics: model-theoretic, fix-point, and proof-theoretic, in the style of classical CLP programs.


title: Operator strength reduction

authors:
Keith D. Cooper
L. Taylor Simpson
Christopher A. Vick

abstract: Operator strength reduction is a technique that improves compiler-generated code by reformulating certain costly computations in terms of less expensive ones. A common case arises in array addressing expressions used in loops. The compiler can replace the sequence of multiplies generated by a direct translation of the address expression with an equivalent sequence of additions. When combined with linear function test replacement, strength reduction can speed up the execution of loops containing array references. The improvement comes from two sources: a reduction in the number of operations needed to implement the loop and the use of less costly operations.This paper presents a new algorithm for operator strength reduction, called OSR. OSR improves upon an earlier algorithm of Allen, Cocke, and Kennedy [Allen et al. 1981]. OSR operates on the static single assignment (SSA) form of a procedure [Cytron et al. 1991]. By taking advantage of the properties of SSA form, we have derived an algorithm that is simple to understand, quick to implement, and, in practice, fast to run. Its asymptotic complexity is, in the worst case, the same as the Allen, Cocke,and Kennedy algorithm (ACK). OSR achieves optimization results that are equivalent to those obtained with the ACK algorithm. OSR has been implemented in several research and production compilers.


title: Using types to analyze and optimize object-oriented programs

authors:
Amer Diwan
Kathryn S. McKinley
J. Eliot B. Moss

abstract: Object-oriented programming languages provide many software engineering benefits, but these often come at a performance cost. Object-oriented programs make extensive use of method invocations and pointer dereferences, both of which are potentially costly on modern machines. We show how to use types to produce effective, yet simple, techniques that reduce the costs of these features in Modula-3, a statically typed, object-oriented language. Our compiler performs type-based alias analysis to disambiguate memory references. It uses the results of the type-based alias analysis to eliminate redundant memory references and to replace monomorphic method invocation sites with direct calls. Using limit, static, and running time evaluation, we demonstrate that these techniques are effective, and sometimes perfect for a set of Modula-3 benchmarks.


title: Transformations of CCP programs

authors:
Sandro Etalle
Maurizio Gabbrielli
Maria Chiara Meo

abstract: We introduce a transformation system for concurrent constraint programming (CCP). We define suitable applicability conditions for the transformations that guarantee the input/output CCP semantics is also preserved when distinguishing deadlocked computations from successful ones and when considering intermediate results of (possibly) nonterminating computations.The system allows us to optimize CCP programs while preserving their intended meaning: In addition to the usual benefits for sequential declarative languages, the transformation of concurrent programs can also lead to the elimination of communication channels and of synchronization points, to the transformation of nondeterministic computations into deterministic ones, and to the crucial saving of computational space. Furthermore, since the transformation system preserves the deadlock behavior of programs, it can be used for proving deadlock-freeness of a given program with respect to a class of queries. To this aim, it is sometimes sufficient to apply our transformations and to specialize the resulting program with respect to the given queries in such a way that the obtained program is trivially deadlock-free.