title: Efficient Counting Program Events with Support for On-Line Queries

abstract: The ability to count events in a program's execution is required by many program analysis applications. We represent an instrumentation method for efficiently counting events in a program's execution, with support for on-line queries of the event count. Event counting differs from basic block profiling in that an aggregate count of events is kept rather than a set of counters. Due to this difference, solutions to basic block profiling are not well suited to event counting. Our algorithm finds a subset of points in a program to instrument, while guaranteeing that accurate event counts can be obtained efficiently at every point in the execution.


venue: toplas

title: Optimally Profiling and Tracing Programs

authors:
Thomas Ball
James R. Larus

abstract: This paper describes algorithms for inserting monitoring code to profile and trace programs. These algorithms greatly reduce the cost of measuring programs with respect to the commonly used technique of placing code in each basic block. Program profiling counts the number of times each basic block in a program executes. Instruction tracing records the sequence of basic blocks traversed in a program execution. The algorithms optimize the placement of counting/tracing code with respect to the expected or measured frequency of each block or edge in a program's control-flow graph. We have implemented the algorithms in a profiling/tracing tool, and they substantially reduce the overhead of profiling and tracing. We also define and study the hierarchy of profiling problems. These problems have two dimensions: what is profiled (i.e., vertices (basic blocks) or edges in a control-flow graph) and where the instrumentation code is placed (in blocks or along edges). We compare the optimal solutions to the profiling problems and describe a new profiling problem: basic-block profiling with edge counters. This problem is important because an optimal solution to any other profiling problem (for a given control-flow graph) is never better than an optimal solution to this problem. Unfortunately, finding an optimal placement of edge counters for vertex profiling appears to be a hard problem in general. However, our work shows that edge profiling with edge counters works well in practice because it is simple and efficient and finds optimal counter placements in most cases. Furthermore, it yields more information than a vertex profile. Tracing also benefits from placing instrumentation code along edges rather than on vertices.


title: A Unified Model of Pointwise Equivalence of Procedural Computations

authors:
David G. Von Bank
Charles M. Shub
Robert W. Sebesta

abstract: The execution of a program on a processor is viewed as a representation of that program going through a sequence of states. Each state change is manifested by the execution of a single instruction. Models that depend on this perspective are presented. The first is a static model of a description of a procedural computation. This model formalizes the description of the information in an executable module. Following this dynamic model of a procedural computation is given. This second model describes how a computation transitions from state to state and how the states of a computation are represented. Next, the state of a procedural computation is defined at certain well-defined points in its progression. These points represent potential points of correspondence to another instance of the computation. Then, the equivalence of these well-defined computation states is described. This refinement eliminates the nonmatching potential correspondences. The remaining points describe where the two computations are in the same state. These are precisely the points of equivalence of procedural computations. This final model of pointwise equivalence can be applied to the problem of migrating a computation from one processor to another (possibly architecturally dissimilar) processor.


title: Recognizing Substrings of LR(k) Languages in Linear Time

authors:
Joseph Bates
Alon Lavie

abstract: LR parsing techniques have long been studied as being efficient and powerful methods for processing context-free languages. A linear-time algorithm for recognizing languages representable by LR(k) grammars has long been known. Recognizing substrings of a context-free language is at least as hard as recognizing full strings of the language, since the latter problem easily reduces to the former. In this article we present a linear-time algorithm for recognizing substrings of LR(k) languages, thus showing that the substring recognition problem for these languages is no harder than the full string recognition problem. An interesting data structure, the Forest-Structured Stack, allows the algorithm to track all possible parses of a substring without loosing the efficiency of the original LR parser. We present the algorithm, prove its correctness, analyze its complexity, and mention several applications that have been constructed.


title: Strictness Optimization for Graph Reduction Machines (Why id Might Not Be Strict)

abstract: Strictness optimizations in the implementation of lazy functional languages are not always valid. In nonoptimized graph reduction, evaluation always takes place at the request of case analysis or a primitive operation. Hence, the result of a reduction is always a data value and never a function. This implies that in an implementation no argument satisfaction check is required. But in the presence of strict arguments, “premature” reduction may take place outside the scope of a case or primitive operation. This causes problems in graph reducers that use an aggressive take . Two solutions are presented, one based on a run-time argument satisfaction check, the other on a weakened strictness analyzer. Experimental results are used to compare the two solutions and show that the cost of the aggressive take can be arbitrarily high for specific programs. The experimental results enable a trade-off to be made by the reduction machine designer.


title: Software Merge: Semantics of Combining Changes to Programs

abstract: We present a language-independent semantic model of the process of combining changes to programs. This model extends the domains used in denotational semantics (complete partial orders) to Boolean algebras, and represents incompatible modifications as well as compatible extensions. The model is used to define the intended semantics of change-merging operations on programs and to establish some general properties of software merging. We determine conditions under which changes to subprograms of a software system can be merged independently and illustrate cases where this is not possible.


title: Path Analysis and the Optimization of Nonstrict Functional Programs

abstract: The functional programming style is increasingly popular in the research world, but functional languages still execute slowly relative to imperative languages. This is largely because the power and flexibility of functional languages restrict the amount of information readily available to the compiler, hindering its ability to generate good code. This article demonstrates that information aboutorder of evaluation of expressionscan be statically inferred for nonstrict functional programs and that optimizations based on this information can provide substantial speedups at runtime. We present an exact, nonstandard semantics calledpath semanticsthat models order of evaluation in a nonstrict, sequential functional language, and its computable abstraction,path analysis. We show how the information inferred by path analysis can be used to implement destructive aggregate updating, in which updates on functional aggregates that are provably not live are done destructively. We also demonstrate a new approach to strictness analysis and show that strictness analysis is subsumed by path analysis. Benchmarks are presented.


title: Two Issues in Parallel Language Design

authors:
A. P. Wim Böhm
R. R. Oldehoeft

abstract: In this article, we discuss two programming language features that have value for expressibility and efficiency: nonstrictness and nondeterminism. Our work arose while assessing ways to enhance a currently successful language, SISAL [McGraw et al. 1985]. The questions of how best to include these features, if at all, has led not to conclusions but to an impetus to explore the answers in an objective way. We will retain strictness for efficiency reasons and explore the limits it may impose, and we will experiment with a carefully controlled form of nondeterminism to assess its expressive power.


title: Transforming Acyclic Programs

authors:
Annalisa Bossi
Sandro Etalle

abstract: An unfold/fold transformation system is a source-to-source rewriting methodology devised to improve the efficiency of a program. Any such transformation should preserve the main properties of the initial program: among them, termination. In the field of logic programming, the class of acyclic programs plays an important role in this respect, since it is closely related to the one of terminating programs. The two classes coincide when negation is not allowed in the bodies of the clauses. We prove that the Unfold/Fold transformation system defined by Tamaki and Sato preserves the acyclicity of the initial program. From this result, it follows that when the transformation is applied to an acyclic program, then the finite failure set for definite programs is preserved; in the case of normal programs, all major declarative and operational semantics are preserved as well. These results cannot be extended to the class of left-terminating programs without modifying the definition of the transformation.


title: Single-Pass Generation of Static Single-Assignment Form for Structured Languages

authors:
Marc M. Brandis
Hanspeter Mössenböck

abstract: this paper we present a technique for generating SSA form in a single pass directly from the source text of a program. It can be applied to structured programs, i.e., to programs that contain only assignments and structured statements (such as IF, CASE, WHILE, REPEAT, or FOR) but no goto statements. For such programs the join nodes and thus the places where to insert f-assignments are immediately known so that f-assignments can be generated on the fly during parsing. This is useful for languages such as Simula[3], Modula-2 [13] or Oberon [14] that lack goto statements at all. If language independence is desired our algorithm can also be applied to control flow graphs instead of source programs. The advantage of generating SSA form directly during parsing is that it saves an intermediate step. Instead of building a high-level representation of a program and then transforming it, we directly generate machine-specific instructions in SSA form ready for optimizations. This saves time and memory. However, the same technique could be used for generating a machine-independent representation as well. We do not deal here with alias problems caused by assignments to array elements, to parameters 4 passed by reference, and to variables that are referenced via pointers. These problems can be dealt with in the same way as described in [5]. While Cytron's method requires the construction of the dominator tree---itself a non-trivial step--- our method does not need such a data structure. However, the dominator tree is useful in subsequent optimizations so that it is worth showing that for structured programs it can be built in a single pass during parsing, too. Section 2 of this paper explains our algorithm for generating SSA form while Section 3 shows how to build the dominator tre...


title: Decompilation: The Enumeration of Types and Grammars

authors:
Peter T. Breuer
Jonathan P. Bowen

abstract: While a compiler produces low-level object code from high-level source code, a decompiler produces high-level code from low-level code and has applications in the testing and validation of safety-critical software. The decompilation of an object code provides an independent demonstration of correctness that is hard to better for industrial purposes (an alternative is to prove the compiler correct). But, although compiler compilers are in common use in the software industry, a decompiler compiler is much more unusual. It turns out that a data type specification for a programming-language grammar can be remolded into a functional program that enumerates all of the abstract syntax trees of the grammar. This observation is the springboard for a general method for compiling decompilers from the specifications of (nonoptimizing) compilers. This paper deals with methods and theory, together with an application of the technique. The correctness of a decompiler generated from a simple occam-like compiler specification is demonstrated. The basic problem of enumerating the syntax trees of grammars, and then stopping, is shown to have no recursive solution, but methods of abstract interpretation can be used to guarantee the adequacy and completeness of our technique in practical instances, including the decompiler for the language presented here.


title: Improvements to Graph Coloring Register Allocation

authors:
Preston Briggs
Keith D. Cooper
Linda Torczon

abstract: We describe two improvements to Chaitin-style graph coloring register allocators. The first, optimistic coloring , uses a stronger heuristic to find a k -coloring for the interference graph. The second extends Chaitin's treatment of rematerialization to handle a larger class of values. These techniques are complementary. Optimistic coloring decreases the number of procedures that require spill code and reduces the amount of spill code when spilling is unavoidable. Rematerialization lowers the cost of spilling some values. This paper describes both of the techniques and our experience building and using register allocators that incorporate them. It provides a detailed description of optimistic coloring and rematerialization. It presents experimental data to show the performance of several versions of the register allocator on a suite of FORTRAN programs. It discusses several insights that we discovered only after repeated implementation of these allocators.


title: Modular Logic Programming

authors:
Antonio Brogi
Paolo Mancarella
Dino Pedreschi
Franco Turini

abstract: Modularity is a key issue in the design of modern programming languages. When designing modular features for declarative languages in general, and for logic programming languages in particular, the challenge lies in avoiding the superimposition of a complex syntactic and semantic structure over the simple structure of the basic language. The modular framework defined here for logic programming consists of a small number of operations over modules which are (meta-) logically defined and semantically justified in terms of the basic logic programming semantics. The operations enjoy a number of algebraic properties, thus yielding an algebra of modules. Despite its simplicity, the suite of operations is shown capable of capturing the core features of modularization: information hiding, import/export relationships, and construction of module hierarchies. A metalevel implementation and a compilation-oriented implementation of the operations are provided and proved sound with respect to the semantics. The compilation-oriented implementation is based on manipulation of name spaces and provides the basis for an efficient implementation.


title: Adding Fair Choice to Dijkstra's Calculus

authors:
Manfred Broy
Greg Nelson

abstract: The paper studies the incorporation of a fair nondeterministic choice operator into a generalization of Dijkstra's calculus of guarded commands. The generalization drops the law of the excluded miracle to allow commands that correspond to partial relations. Because of fairness, the new operator is not monotonic for the orderings that are generally used for proving the existence of least fixed points for recursive definitions. To prove the existence of fixed points it is necessary to consider several orderings at once, and to restrict the class of recursive definitions.


title: Improving the Ratio of Memory Operations to Floating-Point Operations in Loops

authors:
Steve Carr
Ken Kennedy

abstract: Over the past decade, microprocessor design strategies have focused on increasing the computational power on a single chip. Because computations often require more data from cache per floating-point operation than a machine can deliver and because operations are pipelined, idle computational cycles are common when scientific applications are executed. To overcome these bottlenecks, programmers have learned to use a coding style that ensures a better balance between memory references and floating-point operations. In our view, this is a step in the wrong direction because it makes programs more machine-specific. A programmer should not be required to write a new program version for each new machine; instead, the task of specializing a program to a target machine should be left to the compiler. But is our view practical? Can a sophisticated optimizing compiler obviate the need for the myriad of programming tricks that have found their way into practice to improve the performance of the memory hierarchy? In this paper we attempt to answer that question. To do so, we develop and evaluate techniques that automatically restructure program loops to achieve high performance on specific target architectures. These methods attempt to balance computation and memory accesses and seek to eliminate or reduce pipeline interlock. To do this, they estimate statically the balance between memory operations and floating-point operations for each loop in a particular program and use these estimates to determine whether to apply various loop transformations. Experiments with our automatic techniques show that integer-factor speedups are possible on kernels. Additionally, the estimate of the balance between memory operations and computation, and the application of the estimate are very accurate—experiments reveal little difference between the balance achieved by our automatic system that is made possible by hand optimization.


title: Experimental Evaluation of a Generic Abstract Interpretation Algorithm for PROLOG

authors:
Baudouin Le Charlier
Pascal Van Hentenryck

abstract: Abstract interpretation of PROLOG programs has attracted many researchers in recent years, partly because of the potential for optimization in PROLOG compilers and partly because of the declarative nature of logic programming languages that make them more amenable to optimization than procedural languages. Most of the work, however, has remained at the theoretical level, focusing on the developments of frameworks and the definition of abstract domains. This paper reports our effort to verify experimentally the practical value of this area of research. It describes the design and implementation of the generic abstract interpretation algorithm GAIA that we originally proposed in Le Charlier et al. [1991], its instantiation to a sophisticated abstract domain (derived from Bruynooghe and Janssens [1988]) containing modes, types, sharing, and aliasing, and its evaluation both in terms of performance and accuracy. The overall implementation (over 5000 lines of Pascal) has been systematically analyzed on a variety of programs and compared with the complexity analysis of Le Charlie et al. [1991] and the specific analysis systems of Hickey and Mudambi [1989], Taylor [1989; 1990], Van Roy and Despain [1990], and Warren et al. [1988].


title: Static Slicing in the Presence of Goto Statements

authors:
Jong-Deok Choi
Jeanne Ferrante

abstract: A static program slice is an extract of a program which can help our understanding of the behavior of the program; it has been proposed for use in debugging, optimization, parallelization, and integration of programs. This article considers two types of static slices: executable and nonexecutable. Efficient and well-founded methods have been developed to construct executable slices for programs without goto statements; it would be tempting to assume these methods would apply as well in programs with arbitrary goto statements. We show why previous methods do not work in this more general setting, and describe our solutions that correctly and efficiently compute executable slices for programs even with arbitrary goto statements. Our conclusion is that goto statements can be accommodated in generating executable static slices.


title: Model Checking and Abstraction

authors:
Edmund M. Clarke
Orna Grumberg
David E. Long

abstract: We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a program representing a pipelined ALU circuit with over 10 1300 states.


title: Suspension Analyses for Concurrent Logic Programs

authors:
Michael Codish
Moreno Falaschi
Kim Marriott

abstract: Concurrent logic languages specify reactive systems which consist of collections of communicating processes. The presence of unintended suspended computations is a common programming error which is difficult to detect using standard debugging and testing techniques. We develop a number of analyses, based on abstract interpretation, which succeed if a program is definitely suspension free. If an analysis fails, the program may, or may not, be suspension free. Examples demonstrate that the analyses are practically useful. They are conceptually simple and easy to justify because they are based directly on the transition system semantics of concurrent logic programs. A naive analysis must consider all scheduling policies . However, it is proven that for our analyses it suffices to consider only one scheduling policy, allowing for efficient implementation.


title: Debugging Optimized Code Without Being Misled

abstract: Correct optimization can change the behavior of an incorrect program; therefore at times it is necessary to debug optimized code. However, optimizing compilers produce code that impedes source-level debugging. Optimization can cause an inconsistency between where the user expects a breakpoint to be located and the breakpoint's actual location. This article describes a mapping between statements and breakpoint locations that ameliorates this problem. The mapping enables debugger behavior on optimized code that approximates debugger behavior on unoptimized code sufficiently closely for the user to use traditional debugging strategies. Optimization can also cause the value of a variable to be noncurrent —to differ from the value that would be predicted by a close reading of the source code. This article presents a method of determining when this has occurred, and shows how a debugger can describe the relevant effects of optimization. The determination method is more general than previously published methods; it handles global optimization and many flow graph transformations, and it is not tightly coupled to optimizations performed by a particular compiler. Necessary compiler support is also described.


title: Parallel Programming with Control Abstraction

authors:
Lawrence A. Crowl
Thomas J. LeBlanc

abstract: Parallel programming involves finding the potential parallelism in an application and mapping it to the architecture at hand. Since a typical application has more potential parallelism than any single architecture can exploit effectively, programmers usually limit their focus to the parallelism that the available control constructs express easily and that the given architecture exploits efficiently. This approach produces programs that exhibit much less parallelism that exists in the application, and whose performance depends critically on the underlying hardware and software. We argue for an alternative approach based oncontrol abstraction. Control abstraction is the process by which programmers define new control constructs, specifying constraints on statement ordering separately from an implementation of that ordering. With control abstraction programmers can define and use a rich variety of control constructs to represent an algorithm's potential parallelism. Since control abstraction separates the definition of a construct from its implementation, a construct may have several different implementations, each exploiting a different subset of the parallelism admitted by the construct. By selecting an implementation for each control construct using annotations, a programmer can vary the parallelism in a program to best exploit the underlying hardware without otherwise changing the source code. This approach produces programs that exhibit most of the potential parallelism in an algorithm, and whose performance can be tuned simply by choosing among the various implementations for the control constructs in use.


title: A Compiler Approach to Scalable Concurrent-Program Design

authors:
Ian T. Foster
Stephen Taylor

abstract: We describe a compilation system for the concurrent programming language Program Composition Notation (PCN). This notation provides a single-assignment programming model that permits concurrent-programming concerns such as decomposition, communication, synchronization, mapping, granularity, and load balancing to be addressed separately in a design. PCN is also extensible with programmer-defined operators , allowing common abstractions to be encapsulated and reused in different contexts. The compilation system incorporates a concurrent-transformation system that allows abstractions to be defined through concurrent source-to-source transformations; these convert programmer-defined operators into a core notation. Run-time techniques allow the core notation to be compiled into a simple concurrent abstract machine which can be implemented in a portable fashion using a run-time library. The abstract machine provides a uniform treatment of single-assignment and mutable data structures, allowing data sharing between concurrent and sequential program segments and permitting integration of sequential C and Fortran code into concurrent programs. This compilation system forms part of a program development toolkit that operates on a wide variety of networked workstations, multicomputers, and shared-memory multiprocessors. The toolkit has been used both to develop substantial applications and to teach introductory concurrent-programming classes, including a freshman course at Caltech.


title: Avoidance and Suppression of Compensation Code in a Trace Scheduling Compiler

authors:
Stefan M. Freudenberger
Thomas R. Gross
P. Geoffrey Lowney

abstract: Trace scheduling is an optimization technique that selects a sequence of basic blocks as a trace and schedules the operations from the trace together. If an operation is moved across basic block boundaries, one or more compensation copies may be required in the off-trace code. This article discusses the generation of compensation code in a trace scheduling compiler and presents techniques for limiting the amount of compensation code: avoidance (restricting code motion so that no compensation code is required) and suppression (analyzing the global flow of the program to detect when a copy is redundant). We evaluate the effectiveness of these techniques based on measurements for the SPEC89 suite and the Livermore Fortran Kernels, using our implementation of trace scheduling for a Multiflow Trace 7/300. The article compares different compiler models contrasting the performance of trace scheduling with the performance obtained from typical RISC compilation techniques. There are two key results of this study. First, the amount of compensation code generated is not large. For the SPEC89 suite, the average code size increase due to trace scheduling is 6%. Avoidance is more important than suppression, although there are some kernels that benefit significantly from compensation code suppression. Since compensation code is not a major issue, a compiler can be more aggressive in code motion and loop unrolling. Second, compensation code is not critical to obtain the benefits of trace scheduling. Our implementation of trace scheduling improves the SPEC mark rating by 30% over basic block scheduling, but restricting trace scheduling so that no compensation code is required improves the rating by 25%. This indicates that most basic block scheduling techniques can be extended to trace scheduling without requiring any complicated compensation code bookkeeping.


title: TransformGen: Automating the Maintenance of Structure-Oriented Environments

authors:
David Garlan
Charles W. Krueger
Barbara Staudt Lerner

abstract: A serious problem for programs that use persistent data is that information created and maintained by the program becomes invalid if the persistent types used in the program are modified in a new release. Unfortunately, there has been little systematic treatment of the problem; current approaches are manual, ad hoc, and time consuming both for programmers and users. In this article we present a new approach. Focusing on the special case of managing abstract syntax trees in structure-oriented environments, we show how automatic transformers can be generated in terms of an implementor's changes to the grammar of these environments.


title: Model Checking and Modular Verification

authors:
Orna Grumberg
David E. Long

abstract: We describe a framework for compositional verification of finite-state processes. The framework is based on two ideas: a subset of the logic CTL for which satisfaction is preserved under composition, and a preorder on structures which captures the relation between a component and a system containing the component. Satisfaction of a formula in the logic corresponds to being below a particular structure (a tableau for the formula) in the preorder. We show how to do assume-guarantee-style reasoning within this framework. Additionally, we demonstrate efficient methods for model checking in the logic and for checking the preorder in several special cases. We have implemented a system based on these methods, and we use it to give a compositional verification of a CPU controller.


title: Efficient Register Allocation via Coloring Using Clique Separators

authors:
Rajiv Gupta
Mary Lou Soffa
Denise Ombres

abstract: Although graph coloring is widely recognized as an effective technique for register allocation, memory demands can become quite high for large interference graphs that are needed in coloring. In this paper we present an algorithm that uses the notion of clique separators to improve the space overhead of coloring. The algorithm, based on a result by R. Tarjan regarding the colorability of graphs, partitions program code into code segments using clique separators. The interference graphs for the code partitions are constructed one at a time and colored independently. The colorings for the partitions are combined to obtain a register allocation for the entire program. This approach can be used to perform register allocation in a space-efficient manner. For straight-line code (e.g., local register allocation), an optimal allocation can be obtained from optimal allocations for individual code partitions. Experimental results are presented demonstrating memory demand reductions for interference graphs when allocating registers using clique separators.


title: Composing First-Class Transactions

authors:
Nicholas Haines
Darrell Kindred
J. Gregory Morrisett
Scott Nettles
Jeannette M. Wing

abstract: \Ve describe the design of a transaction facilit y for a language that supports higher-order functions.tVe factor transactions into four separable features: persistence, undoability, locking, and threads.Then, relying on function composition, we show how we can put them together again.Our modular approach toward building transactions enables us to construct a model of concurrent, nested, multi threaded transactions, as well as other nontradi tional models where not all features of traditional transactions are present.Key to our approach is the use of higher-order functions to make transactions first-class.Not only do we get clean composability of transactional features, but also we avoid the need to introduce special control General


title: Operational Semantics-Directed Compilers and Machine Architectures

abstract: We consider the task of automatically constructing intermediate-level machine architectures and compilers generating code for these architectures, given operational semantics for source languages. We use operational semantics in the form of abstract machines given by rewrite systems in which the rewrite rules operate on terms representing states of computations. To construct compilers and new architectures we employ a particular strategy called pass separation, a form of staging transformation, that takes a program p and constructs a pair of programs p 1 , p 2 such that p(x, y) = p 2 (p 1 (x), y) ) for all x,y . If p represents an operational semantics for a language, with arguments x and y denoting a source program and its input data, then pass separation constructs programs p 1 and p 2 corresponding to a compiler and an executor. The compiler translates the source language into an intermediate-level target language, and the executor provides the definition for this language. Our use of pass separation supports the automatic definition of target languages or architectures, and the structure of these architectures is directed by the structure of the given source semantics. These architectures resemble abstract machine languages found in hand-crafted compilers. Our method is restricted to a limited class of abstract machines given as term-rewriting systems, but we argue that this class encompasses a large set of language definitions derived from more natural operational semantics. We provide two examples of our method by constructing compilers and target architectures for a simple functional language and a simple imperative language. Though we construct these architectures automatically, they bear a striking resemblance to existing architectures constructed by hand.


title: Efficient Computation of Interprocedural Definition-Use Chains

authors:
Mary Jean Harrold
Mary Lou Soffa

abstract: The dependencies that exist among definitions and uses of variables in a program are required by many language-processing tools. This paper considers the computation of definition-use and use-definition chains that extend across procedure boundaries at call and return sites. Intraprocedural definition and use information is abstracted for each procedure and is used to construct an interprocedural flow graph. This intraprocedural data-flow information is then propagated throughout the program via the interprocedural flow graph to obtain sets of reaching definitions and/or reachable uses for reach interprocedural control point, including procedure entry, exit, call, and return. Interprocedural definition-use and/or use-definition chains are computed from this reaching information. The technique handles the interprocedural effects of the data flow caused by both reference parameters and global variables, while preserving the calling context of called procedures. Additionally, recursion, aliasing, and separate compilation are handled. The technique has been implemented using a Sun-4 Workstation and incorporated into an interprocedural data-flow tester. Results from experiments indicate the practicality of the technique, both in terms of the size of the interprocedural flow graph and the size of the data-flow sets.


title: Lazy and Incremental Program Generation

authors:
Jan Heering
Paul Klint
J. Rekers

abstract: Current program generators usually operate in a greedy manner in the sense that a program must be generated in its entirety before it can be used. If generation time is scarce, or if the input to the generator is subject to modification, it may be better to be more cautious and to generate only those parts of the program that are indispensable for processing the particular data at hand. We call this lazy program generation . Another, closely related strategy is incremental program generation . When its input is modified, an incremental generator will try to make a corresponding modification in its output rather than generate a completely new program. It may be advantageous to use a combination of both strategies in program generators that have to operate in a highly dynamic and/or interactive environment.


title: Metalevel Building Blocks for Modular Systems

abstract: The formal definition of any namespace device found in a programming language can be given in terms of transformations on a semantic environment. It is worthwhile, therefore, to consider the implications of incorporating environments as bona fide data objects in a programming system. In this article, we propose a treatment of environments and the mechanism by which they are reified and manipulated, that addresses these concerns. The language described below (Rascal) permits environments to be reified into data structures, and data structures to be reflected into environments, but gives users great flexibility to constrain the extent and scope of these processes. We argue that the techniques and operators developed define a cohesive basis for building large-scale modular systems using reflective programming techniques.


title: Compositional Specification and Verification of Distributed Systems

abstract: We present a method for specification and verification of distributed systems that communicate via asynchronous message passing. The method handles both safety and liveness properties. It is compositional, i.e., a specification of a composite system can be obtained from specifications of its components. Specifications are given as labeled transition systems with fairness properties, using a program-like notation with guarded multiple assignments. Compositionality is attained by partitioning the labels of a transition system into input events, which intuitively denote message receptions, and output events, which intuitively denote message transmissions. A specification denotes a set of allowed sequences of message transmissions and receptions, in analogy with the way finite automata are used as acceptors of finite strings. A lower-level specification implements a higher-level one. We present a verification technique which reduces the problem of verifying the correctness of an implementation to classical verification conditions. Safety properties are verified by establishing a simulation relation between transition systems. Liveness properties are verified using methods for proving termination under fairness assumptions. Since specifications can be given at various levels of abstraction, the method is suitable in a development process where a detailed implementation is developed from an abstract specification through a sequence of refinement steps. As an application of the method, an algorithm by Thomas for updating a distributed database is specified and verified.


title: Coordinating First-Order Multiparty Interactions

authors:
Yuh-Jzer Joung
Scott A. Smolka

abstract: A first-order multiparty interaction is an abstraction mechanism that defines communication among a set of formal process roles . Actual processes participate in a first-order interaction by enroling into roles, and execution of the interaction can proceed when all roles are filled by distinct processes. As in CSP, enrolement statements can serve as guards in alternative commands. The enrolement guard-scheduling problem then is to enable the execution of first-order interactions through the judicious scheduling of roles to processes that are currently ready to execute enrolement guards. We present a fully distributed and message-efficient algorithm for the enrolement guard-scheduling problem, the first such solution of which we are aware. We also describe several extensions of the algorithm, including: generic roles; dynamically changing environments , where processes can be created and destroyed at run time; and nested-enrolement , which allows interactions to be nested.


title: On the Adequacy of Graph Rewriting for Simulating Term Rewriting

authors:
Richard Kennaway
Jan Willem Klop
M. Ronan Sleep
Fer-Jan de Vries

abstract: Several authors have investigatedthe correspondence between graph rewriting and term rewriting.Almost invariably they have considered only acyclic graphs.Yet cyclic graphs naturally arise from certain optimizations in implementing functional languages.They correspond to infinite terms, and their reductions correspond to transfinite term-reduction sequences, which have recently received detailed attention.We formalize the close correspondence between finitary cyclic graph rewriting and a restricted form of infinitary term rewriting, called rational term rewriting.This subsumes the known relation between finitary acyclic graph rewriting and finitary term rewriting.Surprisingly, the correspondence breaks down for general infinitary rewriting.We present an example showing that infinitary term rewriting is strictly more powerful than infinitary graph .


title: A Generalized Theory of Bit Vector Data Flow Analysis

authors:
Uday P. Khedker
Dhananjay M. Dhamdhere

abstract: The classical theory of data flow analysis, which has its roots in unidirectional flows, is inadequate to characterize bidirectional data flow problems. We present a generalized theory of bit vector data flow analysis which explains the known results in unidirectional and bidirectional data flows and provides a deeper insight into the process of data flow analysis. Based on the theory, we develop a worklist-based generic algorithm which is uniformly applicable to unidirectional and bidirectional data flow problems. It is simple, versatile, and easy to adapt for a specific problem. We show that the theory and the algorithm are applicable to all bounded monotone data flow problems which possess the property of the separability of solution. The theory yields valuable information about the complexity of data flow analysis. We show that the complexity of worklist-based iterative analysis is the same for unidirectional and bidirectional problems. We also define a measure of the complexity of round-robin iterative analysis. This measure, called width , is uniformly applicable to unidirectional and bidirectional problems and provides a tighter bound for unidirectional problems than the traditional measure of depth . Other applications include explanation of isolated results in efficient solution techniques and motivation of new techniques for bidirectional flows. In particular, we discuss edge splitting and edge placement and develop a feasibility criterion for decomposition of a bidirectional flow into a sequence of unidirectional flows.


title: Optimal Code Motion: Theory and Practice

authors:
Jens Knoop
Oliver Rüthing
Bernhard Steffen

abstract: An implementation-oriented algorithm for lazy code motion is presented that minimizes the number of computations in programs while suppressing any unnecessary code motion in order to avoid superfluous register pressure. In particular, this variant of the original algorithm for lazy code motion works on flowgraphs whose nodes are basic blocks rather than single statements, since this format is standard in optimizing compilers. The theoretical foundations of the modified algorithm are given in the first part, where t -refined flowgraphs are introduced for simplifying the treatment of flow graphs whose nodes are basic blocks. The second part presents the “basic block” algorithm in standard notation and gives directions for its implementation in standard compiler environments.


title: The Temporal Logic of Actions

abstract: The temporal logic of actions (TLA) is a logic for specifying and reasoning about concurrent systems. Systems and their properties are represented in the same logic, so the assertion that a system meets its specification and the assertion that one system implements another are both expressed by logical implication. TLA is very simple; its syntax and complete formal semantics are summarized in about a page. Yet, TLA is not just a logician's toy; it is extremely powerful, both in principle and in practice. This report introduces TLA and describes how it is used to specify and verify concurrent algorithms. The use of TLA to specify and reason about open systems will be described elsewhere.


title: Polymorphic Type Inference and Abstract Data Types

authors:
Konstantin Läufer
Martin Odersky

abstract: Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned to variables, passed as function parameters, or returned as function results. Several higher-order functional languages feature strong and static type systems, parametric polymorphism, algebraic data types, and explicit type variables. Most of them rely on Hindley-Milner type inference instead of requiring explicit type declarations for identifiers. Although some of these languages support abstract data types, it appears that none of them directly provides light-weight abstract data types whose implementations are first-class values. We show how to add significant expressive power to statically typed functional languages with explicit type variables by incorporating first-class abstract types as an extension of algebraic data types. Furthermore, we extend record types to allow abstract components. The components of such abstract records are selected using the dot notation. Following Mitchell and Plotkin, we formalize abstract types in terms of existentially quantified types. We give a syntactically sound and complete type inference algorithm and prove that our type system is semantically sound with respect to standard denotational semantics.


title: A Behavioral Notion of Subtyping

authors:
Barbara Liskov
Jeannette M. Wing

abstract: The use of hierarchy is an important component of object-oriented design. Hierarchy allows the use of type families, in which higher level supertypes capture the behavior that all of their subtypes have in common. For this methodology to be effective, it is necessary to have a clear understanding of how subtypes and supertypes are related. This paper takes the position that the relationship should ensure that any property proved about supertype objects also holds for its subtype objects. It presents two ways of defining the subtype relation, each of which meets this criterion, and each of which is easy for programmers to use. The subtype relation is based on the specifications of the sub- and supertypes; the paper presents a way of specifying types that makes it convenient to define the subtype relation. The paper also discusses the ramifications of this notion of subtyping on the design of type families.


title: Denotational Abstract Interpretation of Logic Programs

authors:
Kim Marriott
Harald Søndergaard
Neil D. Jones

abstract: Logic-programming languages are based on a principle of separation “logic” and “control.”. This means that they can be given simple model-theoretic semantics without regard to any particular execution mechanism (or proof procedure, viewing execution as theorem proving). Although the separation is desirable from a semantical point of view, it makes sound, efficient implementation of logic-programming languages difficult. The lack of “control information” in programs calls for complex data-flow analysis techniques to guide execution. Since data-flow analysis furthermore finds extensive use in error-finding and transformation tools, there is a need for a simple and powerful theory of data-flow analysis of logic programs. This paper offers such a theory, based on F. Nielson's extension of P. Cousot and R. Cousot's abstract interpretation . We present a denotational definition of the semantics of definite logic programs. This definition is of interest in its own right because of its compactness. Stepwise we develop the definition into a generic data-flow analysis that encompasses a large class of data-flow analyses based on the SLD execution model. We exemplify one instance of the definition by developing a provably correct groundness analysis to predict how variables may be bound to ground terms during execution. We also discuss implementation issues and related work.


title: Extending Attribute Grammars to Support Programming-in-the-Large

authors:
Josephine Micallef
Gail E. Kaiser

abstract: Attribute grammars add specification of static semantic properties to context-free grammars, which, in turn, describe the syntactic structure of program units. However, context-free grammars cannot express programming-in-the-large features common in modern programming languages, including unordered collections of units, included units, and sharing of included units. We present extensions to context-free grammars, and corresponding extensions to attribute grammars, suitable for defining such features. We explain how batch and incremental attribute-evaluation algorithms can be adapted to support these extensions, resulting in a uniform approach to intraunit and interunit static semantic analysis and translation of multiunit programs.


title: Powerlist: A Structure for Parallel Recursion

abstract: Many data-parallel algorithms—Fast Fourier Transform, Batcher's sorting schemes, and the prefix-sum—exhibit recursive structure. We propose a data structure called powerlist that permits succinct descriptions of such algorithms, highlighting the roles of both parallelism and recursion. Simple algebraic properties of this data structure can be explotied to derive properties of these algorithms and to establish equivalence of different algorithms that solve the same problem.


title: Live-Structure Dataflow Analysis for Prolog

authors:
Anne Mulkers
William H. Winsborough
Maurice Bruynooghe

abstract: For the class of applicative programming languages, efficient methods for reclaiming the memory occupied by released data structures constitute an important aspect of current implementations. The present article addresses the problem of memory reuse for logic programs through program analysis rather than by run-time garbage collection. The aim is to derive run-time properties that can be used at compile time to specialize the target code for a program according to a given set of queries and to automatically introduce destructive assignments in a safe and transparent way so that fewer garbage cells are created. The dataflow analysis is constructed as an application of abstract interpretation for logic programs. An abstract domain for describing structure-sharing and liveness properties is developed as are primitive operations that guarantee a sound and terminating global analysis. We explain our motivation for the design of the abstract domain, make explicit the underlying implementation assumptions, and discuss the precision of the results obtained by a prototype analyzer.


title: Program Optimization and Parallelization Using Idioms

authors:
Shlomit S. Pinter
Ron Y. Pinter

abstract: Programs in languages such as Fortran, Pascal, and C were designed and written for a sequential machine model. During the last decade, several methods to vectorize such programs and recover other forms of parallelism that apply to more advanced machine architectures have been developed (particularly for Fortran, due to its pointer-free semantics). We propose and demonstrate a more powerful translation technique for making such programs run efficiently on parallel machines which support facilities such as parallel prefix operations as well as parallel and vector capabilities. This technique, which is global in nature and involves a modification of the traditional definition of the program dependence graph (PDG), is based on the extraction of parallelizable program structures (“idioms”) from the given (sequential) program. The benefits of our technique extend beyond the above-mentioned architectures and can be viewed as a general program optimization method, applicable in many other situations. We show a few examples in which our method indeed outperforms existing analysis techniques.


title: Static Analysis of Upper and Lower Bounds on Dependences and Parallelism

authors:
William W. Pugh
David Wonnacott

abstract: Existing compilers often fail to parallelize sequential code, even when a program can be manually transformed into parallel form by a sequence of well-understood transformations (as in the case for many of the Perfect Club Benchmark programs). These failures can occur for several reasons: the code transformations implemented in the compiler may not be sufficient to produce parallel code, the compiler may not find the proper sequence of transformations, or the compiler may not be able to prove that one of the necessary transformations is legal. When a compiler fails to extract sufficient parallelism from a program, the programmer may try to extract additional parallelism. Unfortunately, the programmer is typically left to search for parallelism without significant assistance. The compiler generally does not give feedback about which parts of the program might contain additional parallelism, or about the types of transformations that might be needed to realize this parallelism. Standard program transformations and dependence abstractions cannot be used to provide this feedback. In this paper, we propose a two-step approach to the search for parallelism in sequential programs. In the first step, we construct several sets of constraints that describe, for each statement, which iterations of that statement can be executed concurrently. By constructing constraints that correspond to different assumptions about which dependences might be eliminated through additional analysis, transformations, and user assertions, we can determine whether we can expose parallelism by eliminating dependences. In the second step of our search for parallelism, we examine these constraint sets to identify the kinds of transformations needed to exploit scalable parallelism. Our tests will identify conditional parallelism and parallelism that can be exposed by combinations of transformations that reorder the iteration space (such as loop interchange and loop peeling). This approach lets us distinguish inherently sequential code from code that contains unexploited parallelism. It also produces information about the kinds of transformations needed to parallelize the code, without worrying about the order of application of the transformations. Furthermore, when our dependence test is inexact we can identify which unresolved dependences inhibit parallelism by comparing the effects of assuming dependence or independence. We are currently exploring the use of this information in programmer-assisted parallelization.


title: The POLYLITH Software Bus

abstract: We describe a system called POLYLITH that helps programmers prepare and interconnect mixed-language software components for execution in heterogeneous environments. POLYLITH's principal benefit is that programmers are free to implement functional requirements separately from their treatment of interfacing requirements; this means that once an application has been developed for use in one execution environment (such as a distributed network) it can be adapted for reuse in other environments (such as a shared-memory multiprocessor) by automatic techniques. This flexibility is provided without loss of performance. We accomplish this by creating a new run-time organization for software. An abstract decoupling agent, called thesoftware bus, is introduced between the system components. Heterogeneity in language and architecture is accommodated since program units are prepared to interface directly to the bus and not to other program units. Programmers specify application structure in terms of a module interconnection language (MIL); POLYLITH uses this specification to guidepackaging(static interfacing activities such as stub generation, source program adaptation, compilation, and linking). At run time, an implementation of the bus abstraction may assist in message delivery, name service, or system reconfiguration.


title: The Undecidability of Aliasing

abstract: Alias analysis is a prerequisite for performing most of the common program analyses such as reaching-definitions analysis or live-variables analysis. Landi [1992] recently established that it is impossible to compute statically precise alias information—either may-alias or must-alias—in languages with if statements, loops, dynamic storage, and recursive data structures: more precisely, he showed that the may-alias relation is not recursive, while the must-alias relation is not even recursively enumerable. This article presents simpler proofs of the same results.


title: Reasoning about Probabilistic Parallel Programs

abstract: The use of randomization in the design and analysis of algorithms promises simple and efficient algorithms to difficult problems, some of which may not have a deterministic solution. This gain in simplicity, efficiency, and solvability results in a trade-off of the traditional notion of absolute correctness of algorithms for a more quantitative notion: correctness with a probability between 0 and 1. The addition of the notion of parallelism to the already unintuitive idea of randomization makes reasoning about probabilistic parallel programs all the more tortuous and difficult. In this paper we address the problem of specifying and deriving properties of probabilistic parallel programs that either hold deterministically or with probability 1. We present a proof methodology based on existing proof systems for probabilistic algorithms, the theory of the predicate transformer, and the theory of UNITY. Although the proofs of probabilistic programs are slippery at best, we show that such programs can be derived with the same rigor and elegance that we have seen in the derivation of sequential and parallel programs. By applying this methodology to derive probabilistic programs, we hope to develop tools and techniques that would make randomization a useful paradigm in algorithm design.


title: How to Securely Replicate Services

authors:
Michael K. Reiter
Kenneth P. Birman

abstract: We present a method for constructing replicated services that retain their availability and integrity despite several servers and clients being corrupted by an intruder, in addition to others failing benignly. We also address the issue of maintaining a causal order among client requests. We illustrate a security breach resulting from an intruder's ability to effect a violation of causality in the sequence of requests processed by the service and propose an approach to counter this attack. An important and novel feature of our techniques is that the client need not be able to identify or authenticate even a single server. Instead, the client is required to possess only a single public key for the service. We demonstrate the performance of our techniques with a service we have implemented using one of our protocols.


title: Controlled Grammatic Ambiguity

abstract: A new approach to ambiguity of context-free grammars is presented, and within this approach the LL and LR techniques are generalized to solve the following problems for large classes of ambiguous grammars: The user may control the parser generation so as to get a parser which finds some specific parse trees for the sentences. The generalized LL and LR techniques will still guarantee that the resulting parser accepts all sentences and terminates in linear time on all input.


title: Determinacy Testing for Nondeterminate Logic Programming Languages

authors:
Evan Tick
Mark Korsloot

abstract: This paper describes an algorithm for the code generation of determinacy testing for nondeterminate flat concurrent logic programming languages. Languages such as Andorra and Pandora require that procedure invocations suspend if there is more than one candidate clause potentially satisfying the goal. The algorithm described has been developed specifically for a variant of flat Pandora based on FGHC, although the concepts are general. We have extended Kliger and Shapiro's decision-graph construction algorithm to compile “don't-know” procedures that must suspend for nondeterminate goal invocation. The determinacy test is compiled into a decision graph quite different from those of committed-choice procedures: They are more similar to decision trees optimized by code sharing. We present both empirical data of compilation results (code size and graph characteristics), and a correctness proof for our code-generation algorithm.


title: Cliché-Based Program Editors

abstract: article Free Access Share on Cliché-based program editors Author: Richard C. Waters Mitsubishi Electric Labs, Cambridge, MA Mitsubishi Electric Labs, Cambridge, MAView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 16Issue 1Jan. 1994 pp 102–150https://doi.org/10.1145/174625.174628Online:01 January 1994Publication History 4citation475DownloadsMetricsTotal Citations4Total Downloads475Last 12 Months7Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Automatic Isolation of Compiler Errors

abstract: This paper describes a tool called vpoiso that was developed to isolate errors automatically in the vpo compiler system. The two general types of compiler errors isolated by this tool are optimization and nonoptimization errors. When isolating optimization errors, vpoiso relies on the vpo optimizer to identify sequences of changes, referred to as transformations, that result in semantically equivalent code and to provide the ability to stop performing improving (or unnecessary) transformations after a specified number have been performed. A compilation of a typical program by vpo often results in thousands of improving transformations being performed. The vpoiso tool can automatically isolate the first improving transformation that causes incorrect output of the execution of the compiled programs by using a binary search that varies the number of improving transformation performed. Not only is the illegal transformation automatically isolated, but vpoiso also identifies the location and instant the transformation is performed in vpo . Nonoptimization errors occur from problems in the front end, code generator, and necessary transformations in the optimizer. If another compiler is available that can produce correct (but perhaps more inefficient) code, then vpoiso can isolate nonoptimization errors to a single function. Automatic isolation of compiler errors facilitates retargeting a compiler to a new machine, maintenance of the compiler, and supporting experimentation with new optimizations.


title: The Definition of Dependence Distance

abstract: Several definitions of dependence distance can be found in the literature. A single coherent definition is the vector distance between the iteration vectors of two iterations involved in a dependence relation. Different ways to associate iteration vectors with iterations can give different dependence distances to the same program, and have different advantages.


title: A Linear-Time Scheme for Version Reconstruction

authors:
Lin Yu
Daniel J. Rosenkrantz

abstract: An efficient scheme to store and reconstruct versions of sequential files is presented. The reconstruction scheme involves building a data structure representing a complete version, and then successively modifying this data structure by applying a sequence of specially formatted differential files to it. Each application of a differential file produces a representation of an intermediate version, with the final data structure representing the requested version. The scheme uses a linked list to represent an intermediate version, instead of a sequential array, as is used traditionally. A new format for differential files specifying changes to this linked list data structure is presented. The specification of each change points directly to where the change is to take place, thereby obviating a search. Algorithms are presented for using such a new format differential file to transform the representation of a version, and for reconstructing a requested version. Algorithms are also presented for generating the new format differential files, both for the case of a forward differential specifying how to transform the representation of an old version to the representation of a new version, and for the case of a reverse differential specifying how to transform the representation of a new version to the representation of an old version. The new version reconstruction scheme takes time linear in the sum of the size of the initial complete version and the sizes of the file differences involved in reconstructing the requested version. In contrast, the classical scheme for reconstructing versions takes time proportional to the sum of the sizes of the sequence of versions involved in the reconstruction, and therefore has a worst-case time that is quadratic in the sum of the size of the initial complete version and the sizes of the file differences. The time cost of the new differential file generation scheme is comparable to the time cost of the classical differential file generation scheme.


title: Time-Constrained Buffer Specifications in CSP+T and Timed CSP

abstract: A finite buffer with time constraints on the rate of accepting inputs, producing outputs, and message latency is specified using both Timed CSP and a new real-time specification language, CSP + T, which adds expressive power to some of the sequential aspects of CSP and allows the description of complex event timings from within a single sequential process. On the other hand, Timed CSP encourages event-timing descriptions to be built up in a constraint-oriented manner with the parallel composition of several processes. Although these represent two complementary specification styles, both provide valuable insights into the specification of complex event timings.


title: Conjoining Specifications

authors:
Martín Abadi
Leslie Lamport

abstract: We show how to specify components of concurrent systems. The specification of a system is the conjunction of its components' specifications. Properties of the system are proved by reasoning about its components. We consider both the decomposition of a given system into parts, and the composition of given parts to form a system.


title: Safe: A Semantic Technique for Transforming Programs in the Presence of Errors

authors:
Alexander Aiken
John H. Williams
Edward L. Wimmers

abstract: Language designers and implementors have avoided specifying and preserving the meaning of programs that produce errors. This is apparently because being forced to preserve error behavior limits severely the scope of program optimization, even for correct programs. However, error behavior preservation is desirable for debugging, and error behavior must be preserved in any language that permits user-generated errors (i.e., exceptions). This article presents a technique for expressing general program transformations for languages that possess a rich collection of distinguishable error values. This is accomplished by defining a higher-order function called Safe , which can be used to annotate those portions of a program that are guaranteed not to produce errors. It is shown that this facilitates the expression of very general program transformations, effectively giving program transformations in a language with many error values the same power and generality as program transformations in a language with only a single error value. Using the semantic properties of Safe , it is possible to provide some useful sufficient conditions for establishing the correctness of transformations in the presence of errors. In particular, a Substitutability theorem is proven, which can be used to justify “in-context” optimizations: transformations that alter the meanings of subexpressions without changing the meaning of the whole program. Finally, the effectiveness of the technique is demonstrated by some examples of its use in an optimizing compiler.


title: Matching-Based Incremental Evaluators for Hierarchical Attribute Grammar Dialects

authors:
Alan Carle
Lori L. Pollock

abstract: Although attribute grammars have been very effective for defining individual modules of language translators, they have been rather ineffective for specifying large program-transformational systems. Recently, several new attribute grammar “dialects” have been developed that support the modular specification of these systems by allowing modules, each described by an attribute grammar, to be composed to form a complete system. Acceptance of these new hierarchical attribute grammar dialects requires the availability of efficient batch and incremental evaluators for hierarchical specifications. This paper addresses the problem of developing efficient incremental evaluators for hierarchical specifications. A matching-based approach is taken in order to exploit existing optimal change propagation algorithms for nonhierarchical attribute grammars. A sequence of four new matching algorithms is presented, each increasing the number of previously computed attribute values that are made available for reuse during the incremental update.


title: Type Checking Concurrent I/O

abstract: In parallel programming languages multityped data structures may be shared by two or more processes. Process I/O to these structures is assumed to be physically interleaved but logically parallel. This article addresses a syntactic mechanism to specify a type for such structures and extends an example language and its type-checking algorithm to these structures.


title: Covariance and Contravariance: Conflict without a Cause

abstract: In type-theoretic research on object-oriented programming, the issue of “covariance versus contravariance” is a topic of continuing debate. In this short note we argue that covariance and contravariance appropriately characterize two distinct and independent mechanisms. The so-called contravariance rule correctly captures thesubtypingrelation (that relation which establishes which sets of functions can replace another given set inevery context). A covariant relation, instead, characterizes thespecializationof code (i.e., the definition of new code which replaces old definitionsin some particular cases). Therefore, covariance and contravariance are not opposing views, but distinct concepts that each have their place in object-oriented systems. Both can (and should) be integrated in a type-safe manner in object-oriented languages. We also show that the independence of the two mechanisms is not characteristic of a particular model but is valid in general, since covariant specialization is present in record-based models, although it is hidden by a deficiency of all existing calculi that realize this model. As an aside, we show that the λ&-calculus can be taken as the basic calculus for both an overloading-based and a record-based model. Using this approach, one not only obtains a more uniform vision of object-oriented type theories, but in the case of the record-based approach, one also gains multiple dispatching, a feature that existing record-based models do not capture


title: Higher-Order Distributed Objects

authors:
Henry Cejtin
Suresh Jagannathan
Richard Kelsey

abstract: We describe a distributed implementation of Scheme that permits efficient transmission of higher-order objects such as closures and continuations. The integration of distributed communication facilities within a higher-order programming language engenders a number of new abstractions and paradigms for distributed computing. Among these are user-specified load-balancing and migration policies for threads, incrementally linked distributed computations, and parameterized client-server applications. To our knowledge, this is the first distributed dialect of Scheme (or a related language) that addresses lightweight communication abstractions for higher-order objects.


title: Typechecking and Modules for Multimethods

authors:
Craig Chambers
Gary T. Leavens

abstract: Two major obstacles that hinder the wider acceptance of multimethods are (1) concerns over the lack of encapsulation and modularity and (2) the absence of static typechecking in existing multimethod-based languages.This article addresses both of these problems.We present a polynomial-time, static typechecking algorithm that checks the conformance, completeness, and consistency of a group of method implementations with respect to declared message signatures.This algorithm improves on previous algorithms by handling separate type and inheritance hierarchies, abstract classes, and graph-based method lookup semantics.We also present a module system that enables independently developed code to be fully encapsulated and statically typechecked on a per-module basis.To guarantee that potential conflicts between independently developed modules have been resolved, a simple well-formedness condition on the modules comprising a program is checked at link-time.The typechecking algorithm and module system are applicable to a range of multimethod-based languages, but the article uses the Cecil language as a concrete example of how they can be applied.


title: Local and Temporal Predicates In Distributed Systems

authors:
Bernadette Charron-Bost
Carole Delporte-Gallet
Hugues Fauconnier

abstract: The definitions of the predicates Possibly φ and Definitely φ, where φ is a global predicate of a distributed computation, lead to the definitions of two predicate transformers P and D . We show that P plays the same role with respect to time as the predicate transformers K i in knowledge theory play with respect to space . Pursuing this analogy, we prove that local predicates are exactly the fixed points of the K i 's while the stable predicates are the fixed points of P . In terms of the predicate transformers P and D , we define a new class of predicates that we call observer-independent predicates and for which the detection of Possibly φ and Definitely φ is quite easy. Finally, we establish a temporal counterpart to the knowledge change theorem of Chandy and Misra which formally proves that the global view of a distributed system provided by its various observations does not differ too much from its truth behavior.


title: Optimal Evaluation of Array Expressions on Massively Parallel Machines

authors:
Siddhartha Chatterjee
John R. Gilbert
Robert Schreiber
Shang-Hua Teng

abstract: We investigate the problem of evaluating Fortran 90-style array expressions on massively parallel distributed-memory machines. On such a machine, an elementwise operation can be performed in constant time for arrays whose corresponding elements are in the same processor. If the arrays are not aligned in this manner, the cost of aligning them is part of the cost of evaluating the expression tree. The choice of where to perform the operation then affects this cost. We describe the communication cost of the parallel machine theoretically as a metric space; we model the alignment problem as that of finding a minimum-cost embedding of the expression tree into this space. We present algorithms based on dynamic programming that solve the embedding problem optimally for several communication cost metrics: multidimensional grids and rings, hypercubes, fat-trees, and the discrete metric. We also extend our approach to handle operations that change the shape of the arrays.


title: A Reexamination of "Optimization of Array Subscript Range Checks"

authors:
Wie-Ngan Chin
Eak-Khoon Goh

abstract: Jonathan Asuru proposed recently an enhanced method for optimizing array subscript range checks. The proposed method is however unsafe and may generate optimized programs whose behavior is different from the original program. Two main flaws in Asuru's method are described, together with suggested remedies and improvements.


title: Efficient Fault-Tolerant Algorithms for Distributed Resource Allocation

authors:
Manhoi Choy
Ambuj K. Singh

abstract: Solutions to resource allocation problems and other related synchronization problems in distributed systems are examined with respect to the measures ofresponse time, message complexity,andfailure locality. Response time measures the time it takes for an algorithm to respond to the requests of a process; message complexity measures the number of messages sent and received by a process; and failure locality characterizes the size of the network that is affected by the failure of a single process. An algorithm for the resource allocation problem that achieves a constant failure locality of four along with a quadratic response time and a quadratic message complexity is presented. Applications of the algorithm to other process synchronization problems in distributed systems are also demonstrated.


title: Combining Analyses, Combining Optimizations

authors:
Cliff Click
Keith D. Cooper

abstract: Modern optimizing compilers use several passes over a program's intermediate representation to generate good code. Many of these optimizations exhibit a phase-ordering problem. Getting the best code may require iterating optimizations until a fixed point is reached. Combining these phases can lead to the discovery of more facts about the program, exposing more opportunities for optimization. This article presents a framework for describing optimizations. It shows how to combine two such frameworks and how to reason about the properties of the resulting framework. The structure of the frame work provides insight into when a combination yields better results. To make the ideas more concrete, this article presents a framework for combining constant propagation, value numbering, and unreachable-code elimination. It is an open question as to what other frameworks can be combined in this way.


title: Improving Abstract Interpretations by Combining Domains

authors:
Michael Codish
Anne Mulkers
Maurice Bruynooghe
Maria J. García de la Banda
Manuel V. Hermenegildo

abstract: This article considers static analysis based on abstract interpretation of logic programs over combined domains. It is known that analyses over combined domains provide more information potentially than obtained by the independent analyses. However, the construction of a combined analysis often requires redefining the basic operations for the combined domain. A practical approach to maintain precision in combined analyses of logic programs which reuses the individual analyses and does not redefine the basic operations is illustrated. The advantages of the approach are that (1) proofs of correctness for the new domains are not required and (2) implementations can be reused. The approach is demonstrated by showing that a combined sharing analysis—constructed from “old” proposals—compares well with other “new” proposals suggested in recent literature both from the point of view of efficiency and accuracy.


title: Efficientlty Computing Phi-Nodes On-The-Fly

authors:
Ron Cytron
Jeanne Ferrante

abstract: Recently, Static Single-Assignment Form and Sparse Evaluation Graphs have been advanced for the efficient solution of program optimization problems. Each method is provided with an initial set of flow graph nodes that inherently affect a problem's solution. Other relevant nodes are those where potentially disparate solutions must combine. Previously, these so-called φ-nodes were found by computing the iterated dominance frontiers of the initial set of nodes, a process that could take worst-case quadratic time with respect to the input flow graph. In this article we present an almost-linear algorithm for determining exactly the same set of φ-nodes.


title: On the Complexity of Dataflow Analysis of Logic Programs

abstract: It is widely held that there is a correlation between complexity and precision in dataflow analysis, in the sense that the more precise an analysis algorithm, the more computationally expensive it must be. The details of this relationship, however, appear to not have been explored extensively. This article reports some results on this correlation in the context of logic programs. A formal notion of the “precision” of an analysis algorithm is proposed, and this is used to characterize the worst-case computational complexity of a number of dataflow analyses with different degrees of precision. While this article considers the analysis of logic programs, the technique proposed, namely the use of “exactness sets” to study relationships between complexity and precision of analyses, is not specific to logic programming in any way, and is equally applicable to flow analyses of other language families.


title: Influence of Cross-Interferences on Blocked Loops: A Case Study with Matric-Vector Multiply

authors:
Christine Fricker
Olivier Temam
William Jalby

abstract: State-of-the art data locality optimizing algorithms are targeted for local memories rather than for cache memories. Recent work on cache interferences seems to indicate that these phenomena can severely affect blocked algorithms cache performance. Because of cache conflicts, it is not possible to know the precise gain brought by blocking. It is even difficult to determine for which problem sizes blocking is useful. Computing the actual optimal block size is difficult because cache conflicts are highly irregular. In this article, we illustrate the issue of precisely evaluating cross-interferences in blocked loops with blocked matrix-vector multiply. Most significant interference phenomena are captured because unusual parameters such as array base addresses are being considered. The techniques used allow us to compute the precise improvement due to blocking and the threshold value of problem parameters for which the blocked loop should be preferred. It is also possible to derive an expression of the optimal block size as a function of problem parameters. Finally, it is shown that a precise rather than an approximate evaluation of cache conflicts is sometimes necessary to obtain near-optimal performance.


title: Beyond Induction Variables: Detecting and Classifying Sequences Using a Demand-Driven SSA

authors:
Michael P. Gerlek
Eric Stoltz
Michael Wolfe

abstract: Linear induction variable detection is usually associated with the strength reduction optimization. For restructuring compilers, effective data dependence analysis requires that the compiler detect and accurately describe linear and nonlinear induction variables as well as more general sequences. In this article we present a practical technique for detecting a broader class of linear induction variables than is usually recognized, as well as several other sequence forms, including periodic, polynomial, geometric, monotonic, and wrap-around variables. Our method is based on Factored Use-Def (FUD) chains, a demand-driven representation of the popular Static Single Assignment (SSA) form. In this form, strongly connected components of the associated SSA graph correspond to sequences in the source program: we describe a simple yet efficient algorithm for detecting and classifying these sequences. We have implemented this algorithm in Nascent, our restructuring Fortran 90+ compiler, and we present some results showing the effectiveness of our approach.


title: Extracting Task-Level Parallelism

authors:
Milind Girkar
Constantine D. Polychronopoulos

abstract: Automatic detection of task-level parallelism (also referred to as functional, DAG, unstructured, or thread parallelism) at various levels of program granularity is becoming increasingly important for parallelizing and back-end compilers. Parallelizing compilers detect iteration-level or coarser granularity parallelism which is suitable for parallel computers; detection of parallelism at the statement-or operation-level is essential for most modern microprocessors, including superscalar and VLIW architectures. In this article we study the problem of detecting, expressing, and optimizing task-level parallelism, where “task” refers to a program statement of arbitrary granularity. Optimizing the amount of functional parallelism (by allowing synchronization between arbitrary nodes) in sequential programs requires the notion of precedence in terms of paths in graphs which incorporate control and data dependences. Precedences have been defined before in a different context; however, the definition was dependent on the ideas of parallel execution and time. We show that the problem of determining precedences statically is NP-complete. Determining precedence relationships is useful in finding the essential data dependences. We show that there exists a unique minimum set of essential data dependences; finding this minimum set is NP-hard and NP-easy. We also propose a heuristic algorithm for finding the set of essential data dependences. Static analysis of a program in the Perfect Benchmarks was done, and we present some experimental results.


title: Backtracking without Trailing in CLP(R-lin)

authors:
Pascal Van Hentenryck
Viswanath Ramachandran


title: Efficient Instruction Scheduling for Delayed-Load Architectures

authors:
Steven M. Kurlander
Todd A. Proebsting
Charles N. Fischer

abstract: A fast, optimal code-scheduling algorithm for processors with a delayed load of one instruction cycle is described. The algorithm minimizes both execution time and register use and runs in time proportional to the size of the expression-tree. An extension that spills registers when too few registers are available is also presented. The algorithm also performs very well for delayed loads of greater than one instruction cycle. A heuristic that schedules DAGs and is based on our optimal expression-tree-scheduling algorithm is presented and compared with Goodman and Hsu's algorithm Integrated Prepass Scheduling (IPS). Both schedulers perform well on benchmarks with small basic blocks, but on large basic blocks our scheduler outperforms IPS and is significantly faster.


title: Optimal Incremental Parsing

abstract: This communication sets the problem of incremental parsing in the context of a complete incremental compiling system. It turns out that, according to the incrementally paradigm of the attribute evaluator and data-flow analyzer to be used, two definitions of optimal incrementality in a parser are possible. Algorithms for achieving both forms of optimality are given, both of them based on ordinary LALR(1) parse tables. Optimality and correctness proofs, which are merely outlined in this communication, are made intuitive thanks to the concept of awell-formed list of threaded trees, a natural extension of the concept ofthreaded treefound in earlier works on incremental parsing.


title: Lattice Frameworks for Multiscore and Bidirectional Data Flow Problems

authors:
Stephen P. Masticola
Thomas J. Marlowe
Barbara G. Ryder

abstract: Multisource data flow problems involve information which may enter nodes independently through different classes of edges. In some cases, dissimilar meet operations appear to be used for different types of nodes. These problems include bidirectional and flow-sensitive problems as well as many static analyses of concurrent programs with synchronization. K-tuple frameworks , a type of standard data flow framework, provide a natural encoding for multisource problems using a single meet operator. Previously, the solution of these problems has been described as the fixed point of a set of data flow equations. Using our k -tuple representation, we can access the general results of standard data flow frameworks concerning convergence time and solution precision for these problems. We demonstrate this for the bidirectional component of partial redundancy suppression and two problems on the program summary graph. An interesting subclass of k -tuple frameworks, the join-of-meets frameworks, is useful for reachability problems, especially those stemming from analyses of explicitly parallel programs. We give results on function space properties for join-of-meets frameworks that indicate precise solutions for most of them will be difficult to obtain.


title: Error Repair in Shift-Reduce Parsers

authors:
Bruce J. McKenzie
Corey Yeatman
Lorraine De Vere

abstract: Local error repair of strings during CFG parsing requires the insertion and deletion of symbols in the region of a syntax error to produce a string that is error free. Rather than precalculating tables at parser generation time to assist in finding such repairs, this article shows how such repairs can be found during shift-reduce parsing by using the parsing tables themselves. This results in a substantial space saving over methods that require precalculated tables. Furthermore, the article shows how the method can be integrated with lookahead to avoid finding repairs that immediately result in further syntax errors. The article presents the results of experiments on a version of the LALR(1)-based parser generator Bison to which the algorithm was added.


title: A Polymorphic Record Calculus and Its Compilation

abstract: The motivation of this work is to provide a type-theoretical basis for developing a practical polymorphic programming language with labeled records and labeled variants.Our goal is to establish both a polymorphic type discipline and an efficient compilation method for a calculus with those labeled data structures.We define a second-order, polymorphic record calculus as an extension of Girard-Reynolds polymorphic lambda calculus.We then develop an ML-style type inference algorithm for a predicative subset of the second-order record calculus.The soundness of the type system and the completeness of the type inference algorithm are shown.These results extend Milner's type inference algorithm, Damas and Milner's account of ML's let polymorphism, and Harper and Mitchell's analysis on XML To establish an efficient compilation method for the polymorphic record calculus, we first define an implementation calculus, where records are represented as vectors whose elements are accessed by direct indexing, and variants are represented as values tagged with a natural number indicating the position in the vector of functions m a switch statement.We then develop an algorithm to translate the polymorphic record calculus into the implementation calculus using type reformation obtained by the type inference algorithm.The correctness of the compilation algorithm is proved, that is, the compdation algorithm is shown to preserve both typing and the operational behavior of a program.Based on these results, Standard ML has been extended with labeled records, and its compiler has been implemented.


title: Closure Analysis in Constraint Form

abstract: Flow analyses of untyped higher-order functional programs have in the past decade been presented by Ayers, Bondorf, Consel, Jones, Heintze, Sestoft, Shivers, Steckler, Wand, and others. The analyses are usually defined as abstract interpretations and are used for rather different tasks such as type recovery, globalization, and binding-time analysis. The analyses all contain a global closure analysis that computes information about higher-order control-flow. Sestoft proved in 1989 and 1991 that closure analysis is correct with respect to call-by-name and call-by-value semantics, but it remained open if correctness holds for arbitrary beta-reduction. This article answers the question; both closure analysis and others are correct with respect to arbitrary beta-reduction. We also prove a subject-reduction result: closure information is still valid after beta-reduction. The core of our proof technique is to define closure analysis using a constraint system. The constraint system is equivalent to the closure analysis of Bondorf, which in turn is based on Sestoft's.


title: A Type System Equivalent to Flow Analysis

authors:
Jens Palsberg
Patrick O'Keefe

abstract: Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis. In this article we prove that Amadio and Cardelli's type system with subtyping and recursive types accepts the same programs as a certain safety analysis. The proof involves mappings from types to flow information and back. As a result, we obtain an inference algorithm for the type system, thereby solving an open problem.


title: Efficient Implementation of Adaptive Software

authors:
Jens Palsberg
Cun Xiao
Karl J. Lieberherr

abstract: Adaptive programs compute with objects, just like object-oriented programs. Each task to be accomplished is specified by a so-called propagation pattern which traverses the receiver object. The object traversal is a recursive descent via the instance variables where information is collected or propagated along the way. A propagation pattern consists of (1) a name for the task, (2) a succinct specification of the parts of the receiver object that should be traversed, and (3) code fragments to be executed when specific object types are encountered. The propagation patterns need to be complemented by a class graph which defines the detailed object structure. The separation of structure and behavior yields a degree of flexibility and understandability not present in traditional object-oriented languages. For example, the class graph can be changed without changing the adaptive program at all. We present an efficient implementation of adaptive programs. Given an adaptive program and a class graph, we generate an efficient object-oriented program, for example, in C++. Moreover, we prove the correctness of the core of this translation. A key assumption in the theorem is that the traversal specifications are consistent with the class graph. We prove the soundness of a proof system for conservatively checking consistency, and we show how to implement it efficiently.


title: BURS Automata Generation

abstract: A simple and efficient algorithm for generating bottom-up rewrite system (BURS) tables is described. A small code-generator generator implementation produces BURS tables efficiently, even for complex instruction set descriptions. The algorithm does not require novel data structures or complicated algorithmic techniques. Previously published methods for on-the-fly elimination of states are generalized and simplified to create a new method, triangle trimming, that is employed in the algorithm. A prototype implementation, burg, generates BURS tables very efficiently.


title: Supporting Dynamic Data Structures on Distributed-Memory Machines

authors:
Anne Rogers
Martin C. Carlisle
John H. Reppy
Laurie J. Hendren

abstract: Compiling for distributed-memory machines has been a very active research area in recent years. Much of this work has concentrated on programs that use arrays as their primary data structures. To date, little work has been done to address the problem of supporting programs that use pointer-based dynamic data structures. The techniques developed for supporting SPMD execution of array-based programs rely on the fact that arrays are statically defined and directly addressable. Recursive data structures do not have these properties, so new techniques must be developed. In this article, we describe an execution model for supporting programs that use pointer-based dynamic data structures. This model uses a simple mechanism for migrating a thread of control based on the layout of heap-allocated data and introduces parallelism using a technique based on futures and lazy task creation. We intend to exploit this execution model using compiler analyses and automatic parallelization techniques. We have implemented a prototype system, which we callOlden, that runs on the Intel iPSC/860 and the Thinking Machines CM-5. We discuss our implementation and report on experiments with five benchmarks.


title: Fast Strictness Analysis Based on Demand Propagation

authors:
R. Sekar
I. V. Ramakrishnan

abstract: Strictnessanalysis is a well-known technique used in compilers for optimization of sequential and '90..


title: Notes on "A Methodology for Implementing Highly Concurrent Data Objects"

abstract: No abstract available.


title: An Evaluation of an Automatically Generated Compiler

abstract: Compilers or language translators can be generated using a variety of formal specification techniques. Whether generation is worthwhile depends on the effort required to specify the translation task and the quality of the generated compiler. A systematic comparison was conducted between a hand-coded translator for the Icon programming language and one generated by the Eli compiler construction system. A direct comparison could be made since the generated program performs the same translation as the hand-coded program. The results of the comparison show that efficient compilers can be generated from specifications that are much smaller and more problem oriented than the equivalent source code. We also found that further work must be done to reduce the dynamic memory usage of the generated compilers.


title: Deducing Fairness Properties in UNITY Logic - A New Completeness Result

authors:
Yih-Kuen Tsay
Rajive L. Bagrodia

abstract: We explore the use of UNITY logic in specifying and verifying fairness properties of UNITY and UNITY-like programs whose semantics can be modeled by weakly fair transition systems. For such programs, strong fairness properties in the form of “if p holds infinitely often then q also holds infinitely often □◊p⇒□◊q, can be expressed as conditional UNITY properties of the form of “Hypothesis: true→p Conclusion:true→q”. We show that UNITY logic is relatively complete for proving such properties; in the process, a simple inference rule is derived. Specification and verification of weak fairness properties are also discussed.