title: A framework for call graph construction algorithms

authors:
David Grove
Craig Chambers

abstract: A large number of call graph construction algorithms for object-oriented and functional languages have been proposed, each embodying different tradeoffs between analysis cost and call graph precision. In this article we present a unifying framework for understanding call graph construction algorithms and an empirical comparison of a representative set of algorithms. We first present a general parameterized algorithm that encompasses many well-known and novel call graph construction algorithms. We have implemented this general algorithm in the Vortex compiler infrastructure, a mature, multilanguage, optimizing compiler. The Vortex implementation provides a "level playing field" for meaningful cross-algorithm performance comparisons. The costs and benefits of a number of call graph construction algorithms are empirically assessed by applying their Vortex implementation to a suite of sizeable (5,000 to 50,000 lines of code) Cecil and Java programs. For many of these applications, interprocedural analysis enabled substantial speed-ups over an already highly optimized baseline. Furthermore, a significant fraction of these speed-ups can be obtained through the use of a scalable, near-linear time call graph construction algorithm.


venue: toplas

title: Parallel execution of prolog programs: a survey

authors:
Gopal Gupta
Enrico Pontelli
Khayri A. M. Ali
Mats Carlsson
Manuel V. Hermenegildo

abstract: Since the early days of logic programming, researchers in the field realized the potential for exploitation of parallelism present in the execution of logic programs. Their high-level nature, the presence of nondeterminism, and their referential transparency, among other characteristics, make logic programs interesting candidates for obtaining speedups through parallel execution. At the same time, the fact that the typical applications of logic programming frequently involve irregular computations, make heavy use of dynamic data structures with logical variables, and involve search and speculation, makes the techniques used in the corresponding parallelizing compilers and run-time systems potentially interesting even outside the field. The objective of this article is to provide a comprehensive survey of the issues arising in parallel execution of logic programming languages along with the most relevant approaches explored to date in the field. Focus is mostly given to the challenges emerging from the parallel execution of Prolog programs. The article describes the major techniques used for shared memory implementation of Or-parallelism, And-parallelism, and combinations of the two. We also explore some related issues, such as memory management, compile-time analysis, and execution visualization.


title: Featherweight Java: a minimal core calculus for Java and GJ

authors:
Atsushi Igarashi
Benjamin C. Pierce
Philip Wadler

abstract: Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.


title: Error repair with validation in LR-based parsing

authors:
Ik-Soon Kim
Kwang-Moo Choe

abstract: When the compiler encounters an error symbol in an erroneous input, the local error-repair method repairs the input by either inserting a repair string before the error symbol or deleting the error symbol. Although the extended FMQ of Fischer et al. and the method of McKenzie et al. report the improved quality of diagnostic messages, they suffer from redundant parse stack configurations.This article proposes an efficient LR error-recovery method, with validation-removing repairs that give the same validation result as a previously considered, lower-cost repair. Moreover, its execution speed is proportional to the length of the stack configuration. The algorithm is implemented on a Bison, GNU LALR(1), parser generating system. Experimental results are presented.


title: Type elaboration and subtype completion for Java bytecode

authors:
Todd B. Knoblock
Jakob Rehof

abstract: Java source code is strongly typed, but the translation from Java source to bytecode omits much of the type information originally contained within methods. Type elaboration is a technique for reconstructing strongly typed programs from incompletely typed bytecode by inferring types for local variables. There are situations where, technically, there are not enough types in the original type hierarchy to type a bytecode program. Subtype completion is a technique for adding necessary types to an arbitrary type hierarchy to make type elaboration possible for all verifiable Java bytecode. Type elaboration with subtype completion has been implemented as part of the Marmot Java compiler.


title: Scheduling time-constrained instructions on pipelined processors

authors:
Allen Leung
Krishna V. Palem
Amir Pnueli

abstract: In this work we investigate the problem of scheduling instructions on idealized microprocessors with multiple pipelines, in the presence of precedence constraints, release-times, deadlines, and latency constraints. A latency of l ij specifies that there must be at least l ij time-steps between the completion time of instruction i and the start time of instruction j . A latency of l ij =−1 can be used to specify that j may be scheduled concurrently with i but not earlier. We present a generic algorithm that runs in O ( n 2 log n α( n )+ ne ) time, given n instructions and e edges in the precedence DAG, where α( n ) is the functional inverse of the Ackermann function. Our algorithm can be used to construct feasible schedules for various classes of instances, including instances with the following configurations: (1) one pipeline, with individual release-times and deadlines and where the latencies between instructions are restricted to 0 and 1; (2) m pipelines, with individual release-times and deadlines, and monotone-interval order precedences; (3) two pipelines with latencies of −1 or 0, and release-times and deadlines; (4) one pipeline, latencies of 0 or 1 and individual processing times that are at least one; (5) m pipelines, intree precedences, constant latencies, and deadlines; (6) m pipelines, outtree precedences, constant latencies, and release-times. For instances with deadlines, optimal schedules that minimize the maximal tardiness can be constructed using binary search, in O (log n ) iterations of our algorithm. We obtain our results using backward scheduling, a very general relaxation method, which extends, unifies, and clarifies many previous results on instruction scheduling for pipelined and parallel machines.


title: Efficient Java RMI for parallel programming

authors:
Jason Maassen
Rob van Nieuwpoort
Ronald Veldema
Henri E. Bal
Thilo Kielmann
Ceriel J. H. Jacobs
Rutger F. H. Hofman

abstract: Java offers interesting opportunities for parallel computing. In particular, Java Remote Method Invocation (RMI) provides a flexible kind of remote procedure call (RPC) that supports polymorphism. Sun's RMI implementation achieves this kind of flexibility at the cost of a major runtime overhead. The goal of this article is to show that RMI can be implemented efficiently, while still supporting polymorphism and allowing interoperability with Java Virtual Machines (JVMs). We study a new approach for implementing RMI, using a compiler-based Java system called Manta. Manta uses a native (static) compiler instead of a just-in-time compiler. To implement RMI efficiently, Manta exploits compile-time type information for generating specialized serializers. Also, it uses an efficient RMI protocol and fast low-level communication protocols.A difficult problem with this approach is how to support polymorphism and interoperability. One of the consequences of polymorphism is that an RMI implementation must be able to download remote classes into an application during runtime. Manta solves this problem by using a dynamic bytecode compiler, which is capable of compiling and linking bytecode into a running application. To allow interoperability with JVMs, Manta also implements the Sun RMI protocol (i.e., the standard RMI protocol), in addition to its own protocol.We evaluate the performance of Manta using benchmarks and applications that run on a 32-node Myrinet cluster. The time for a null-RMI (without parameters or a return value) of Manta is 35 times lower than for the Sun JDK 1.2, and only slightly higher than for a C-based RPC protocol. This high performance is accomplished by pushing almost all of the runtime overhead of RMI to compile time. We study the performance differences between the Manta and the Sun RMI protocols in detail. The poor performance of the Sun RMI protocol is in part due to an inefficient implementation of the protocol. To allow a fair comparison, we compiled the applications and the Sun RMI protocol with the native Manta compiler. The results show that Manta's null-RMI latency is still eight times lower than for the compiled Sun RMI protocol and that Manta's efficient RMI protocol results in 1.8 to 3.4 times higher speedups for four out of six applications.


title: Mechanizing a theory of program composition for UNITY

abstract: Compositional reasoning must be better understood if non-trivial concurrent programs are to be verified. Chandy and Sanders [2000] have proposed a new approach to reasoning about composition, which Charpentier and Chandy [1999] have illustrated by developing a large example in the UNITY formalism. The present paper describes extensive experiments on mechanizing the compositionality theory and the example, using the proof tool Isabelle. Broader issues are discussed, in particular, the formalization of program states. The usual representation based upon maps from variables to values is contrasted with the alternatives, such as a signature of typed variables. Properties need to be transferred from one program component's signature to the common signature of the system. Safety properties can be so transferred, but progress properties cannot be. Using polymorphism, this problem can be circumvented by making signatures sufficiently flexible. Finally the proof of the example itself is outlined.


title: A schema for interprocedural modification side-effect analysis with pointer aliasing

authors:
Barbara G. Ryder
William Landi
Phil Stocks
Sean Zhang
Rita Z. Altucher

abstract: The first interprocedural modification side-effects analysis for C (MOD C ) that obtains better than worst-case precision on programs with general-purpose pointer usage is presented with empirical results. The analysis consists of an algorithm schema corresponding to a family of MOD C algorithms with two independent phases: one for determining pointer-induced aliases and a subsequent one for propagating interprocedural side effects. These MOD C algorithms are parameterized by the aliasing method used. The empirical results compare the performance of two dissimilar MOD C algorithms: MOD C ( FSAlias ) uses a flow-sensitive, calling-context-sensitive interprocedural alias analysis; MOD C ( FIAlias uses a flow-insensitive, calling-context-insensitive alias analysis which is much faster, but less accurate. These two algorithms were profiled on 45 programs ranging in size from 250 to 30,000 lines of C code, and the results demonstrate dramatically the possible cost-precision trade-offs. This first comparative implementation of MOD C analyses offers insight into the differences between flow-/context-sensitive and flow-/context-insensitive analyses. The analysis cost versus precision trade-offs in side-effect information obtained are reported. The results show surprisingly that the precision of flow-sensitive side-effect analysis is not always prohibitive in cost, and that the precision of flow-insensitive analysis is substantially better than worst-case estimates and seems sufficient for certain applications. On average MOD C ( FSAlias ) for procedures and calls is in the range of 20% more precise than MOD C ( FIAlias ); however, the performance was found to be at least an order of magnitude slower than MOD C ( FIAlias ).


title: Lessons learned about one-way, dataflow constraints in the Garnet and Amulet graphical toolkits

authors:
Bradley T. Vander Zanden
Richard L. Halterman
Brad A. Myers
Richard G. McDaniel
Robert C. Miller
Pedro A. Szekely
Dario A. Giuse
David S. Kosbie

abstract: One-way, dataflow constraints are commonly used in graphical interface toolkits, programming environments, and circuit applications. Previous papers on dataflow constraints have focused on the design and implementation of individual algorithms. In contrast, this article focuses on the lessons we have learned from a decade of implementing competing algorithms in the Garnet and Amulet graphical interface toolkits. These lessons reveal the design and implementation tradeoffs for different one-way, constraint satisfaction algorithms. The most important lessons we have learned are that (1) mark-sweep algorithms are more efficient than topological ordering algorithms; (2) lazy and eager evaluators deliver roughly comparable performance for most applications; and (3) constraint satisfaction algorithms have more than adequate speed, except that the storage required by these algorithms can be problematic.


title: Compiling language definitions: the ASF+SDF compiler

authors:
Mark van den Brand
Jan Heering
Paul Klint
Pieter A. Olivier

abstract: The ASF+SDF Meta-Environment is an interactive language development environment whose main application areas are definition and implementation of domain-specific languages, generation of program analysis and transformation tools, and production of software renovation tools. It uses conditional rewrite rules to define the dynamic semantics and other tool-oriented aspects of languages, so the effectiveness of the generated tools is critically dependent on the quality of the rewrite rule implementation. The ASF+SDF rewrite rule compiler generates C code, thus taking advantage of C's portability and the sophisticated optimization capabilities of current C compilers as well as avoiding potential abstract machine interface bottlenecks. It can handle large (10,000+ rule) language definitions and uses an efficient run-time storage scheme capable of handling large (1,000,000+ node) terms. Term storage uses maximal subterm sharing (hash-consing), which turns out to be more effective in the case of ASF+SDF than in Lisp or SML. Extensive benchmarking has shown the time and space performance of the generated code to be as good as or better than that of the best current rewrite rule and functional language compilers.


title: The undecidability of associativity and commutativity analysis

abstract: Associativity is required for the use of general scans and reductions in parallel languages. Some systems also require functions used with scans and reductions to be commutative. We prove the undecidability of both associativity and commutativity. Thus, it is impossible in general for a compiler to check for those conditions. We also prove the stronger result that the resulting relations fail to be recursively enumerable. We prove that these results hold for the kind of function subprograms of practical interest in such a situation: function subprograms that, due to syntactical restrictions, are guaranteed to halt. Thus, our results are stronger than one can obtain from Rice's Theorem. We also obtain limitations concerning the construction of functions and limitations concerning compiler-generated run-time checks. In addition, we prove an undecidability result about programmer-constructed run-time checks.


title: Automatic derivation of compiler machine descriptions

abstract: We describe a method designed to significantly reduce the effort required to retarget a compiler to a new architecture, while at the same time producing fast and effective compilers. The basic idea is to use the native C compiler at compiler construction time to discover architectural features of the new architecture. From this information a formal machine description is produced. Given this machine description, a native code-generator can be generated by a back-end generator such as BEG or burg. A prototype automatic Architecture Discovery Tool (called ADT) has been implemented. This tool is completely automatic and requires minimal input from the user. Given the Internet address of the target machine and the command-lines by which the native C compiler, assembler, and linker are invoked, ADT will generate a BEG machine specification containing the register set, addressing modes, instruction set, and instruction timings for the architecture. The current version of ADT is general enough to produce machine descriptions for the integer instruction sets of common RISC and CISC architectures such as the Sun SPARC, Digital Alpha, MIPS, DEC VAX, and Intel x86.


title: Repairing syntax errors in LR parsers

authors:
Rafael Corchuelo
José Antonio Pérez
Antonio Ruiz Cortés
Miguel Toro

abstract: This article reports on an error-repair algorithm for LR parsers. It locally inserts, deletes or shifts symbols at the positions where errors are detected, thus modifying the right context in order to resume parsing on a valid piece of input. This method improves on others in that it does not require the user to provide additional information about the repair process, it does not require precalculation of auxiliary tables, and it can be easily integrated into existing LR parser generators. A Yacc-based implementation is presented along with some experimental results and comparisons with other well-known methods.


title: More dynamic object reclassification: Fickle||

authors:
Sophia Drossopoulou
Ferruccio Damiani
Mariangiola Dezani-Ciancaglini
Paola Giannini

abstract: Reclassification changes the class membership of an object at run-time while retaining its identity. We suggest language features for object reclassification, which extend an imperative, typed, class-based, object-oriented language.We present our proposal through the language Fickle ⋄⋄ . The imperative features, combined with the requirement for a static and safe type system, provided the main challenges. We develop a type and effect system for Fickle ⋄⋄ and prove its soundness with respect to the operational semantics. In particular, even though objects may be reclassified across classes with different members, there will never be an attempt to access nonexisting members.


title: Type-Safe linking with recursive DLLs and shared libraries

abstract: Component-based programming is an increasingly prevalent theme in software development, motivating the need for expressive and safe module interconnection languages. Dynamic linking is an important requirement for module interconnection languages, as exemplified by dynamic link libraries (DLLs) and class loaders in operating systems and Java, respectively. A semantics is given for a type-safe module interconnection language that supports shared libraries and dynamic linking, as well as circular import dependencies (recursive modules). The core language requirements of the module interconnection language are compatible with programming languages such as Java and C#.


title: Guest editorial

authors:
Kathleen Fisher
Benjamin C. Pierce

abstract: The Eighth International Workshop on Foundations of Object-Oriented Languages (FOOL 8) was held on January 20, 2001, colocated with the ACM Symposium on Principles of Programming Languages in London. Kathleen Fisher chaired the program committee. Six contributed papers were presented. After the workshop, extended versions of three were solicited for this special issue of TOPLAS ; the two articles that were ultimately submitted were reviewed, revised, and accepted following standard TOPLAS procedures.The special issue opens with Type-Preserving Compilation of Featherweight Java by Christopher League, Zhong Shao, and Valery Trifonov. The goal of the authors is to establish a foundation for certifying compilation of Java-like class-based languages. To this end, the authors give an encoding of core Java features in a typed intermediate language suitable for use within a type-preserving compiler. Because of its intended use, the authors focus on developing an efficient encoding. They show that the type erasure of their implementation matches the standard vtable self-application semantics of message sending.The authors use Featherweight Java (FJ), which models the core features of Java, as their source language. Their translation targets a variant of F ω , already implemented as part of the SML/NJ compiler, using its row polymorphism and existential and recursive types to encode FJ. The authors show that the translation from FJ to their target preserves types.In the issue's second article, More Dynamic Object Reclassification: Fickle II , Sophia Drossopoulou, Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, and Paola Giannini explore the issue of dynamic reclassification, by which an object changes its class membership at runtime while retaining its identity. This ability helps model real-world situations where an object has different roles over time---for example, a person who is first a student and then graduates to become a teacher.The authors focus their study on the design of a language, Fickle II , which extends an imperative, typed, class-based, object-oriented language with a reclassification operation. To specify the behavior of their language, the authors give an operational semantics. They then develop a type and effect system and show that the type system is sound, in the sense that a well-typed program cannot get stuck under the operational semantics.We would like to thank our colleagues who served on the FOOL 8 program committee and those who participated in the anonymous reviewing process for TOPLAS . Their efforts contributed greatly to the quality of this special issue.


title: Information flow vs. resource access in the asynchronous pi-calculus

authors:
Matthew Hennessy
James Riely

abstract: We propose an extension of the asynchronous π-calculus in which a variety of security properties may be captured using types. These are an extension of the input/output types for the π-calculus in which I/O capabilities are assigned specific security levels. The main innovation is a uniform typing system that, by varying slightly the allowed set of types, captures different notions of security.We first define a typing system that ensures that processes running at security level σ cannot access resources with a security level higher than σ. The notion of access control guaranteed by this system is formalized in terms of a Type Safety Theorem.We then show that, by restricting the allowed types, our system prohibits implicit information flow from high-level to low-level processes. We prove that low-level behavior can not be influenced by changes to high-level behavior. This is formalized as a noninterference theorem with respect to may testing.


title: An assume-guarantee rule for checking simulation

authors:
Thomas A. Henzinger
Shaz Qadeer
Sriram K. Rajamani
Serdar Tasiran

abstract: The simulation preorder on state transition systems is widely accepted as a useful notion of refinement, both in its own right and as an efficiently checkable sufficient condition for trace containment. For composite systems, due to the exponential explosion of the state space, there is a need for decomposing a simulation check of the form P ≤ s Q , denoting " P is simulated by Q ," into simpler simulation checks on the components of P and Q . We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q , we provide a procedure for constructing a witness relation for P ≤ s Q . We also extend our assume-guarantee rule to account for fairness constraints on transition systems.


title: On the usefulness of type and liveness accuracy for garbage collection and leak detection

authors:
Martin Hirzel
Amer Diwan
Johannes Henkel

abstract: The effectiveness of garbage collectors and leak detectors in identifying dead objects depends on theaccuracyof their reachability traversal. Accuracy has two orthogonal dimensions: (i) whether the reachability traversal can distinguish between pointers and nonpointers (type accuracy), and (ii) whether the reachability traversal can identify memory locations that will be dereferenced in the future (liveness accuracy). This article presents an experimental study of the importance of type and liveness accuracy for reachability traversals. We show that liveness accuracy reduces the reachable heap size by up to 62% for our benchmark programs. However, the simpler liveness schemes (e.g., intraprocedural analysis of local variables) are largely ineffective for our benchmark runs: one must analyze global variables using interprocedural analysis to obtain significant benefits. Type accuracy has an insignificant impact on a garbage collector's ability to find unreachable objects in our benchmark runs. We report results for programs written in C, C++, and Eiffel.


title: Register tiling in nonrectangular iteration spaces

authors:
Marta Jiménez
José M. Llabería
Agustín Fernández

abstract: Loop tiling is a well-known loop transformation generally used to expose coarse-grain parallelism and to exploit data reuse at the cache level. Tiling can also be used to exploit data reuse at the register level and to improve a program's ILP. However, previous proposals in the literature (as well as commercial compilers) are only able to perform multidimensional tiling for the register level when the iteration space is rectangular. In this article we present a new general algorithm to perform multidimensional tiling for the register level in both rectangular and nonrectangular iteration spaces. We also propose a simple heuristic to determine the tiling parameters at this level. Finally, we evaluate our method using as benchmarks typical linear algebra algorithms having nonrectangular iteration spaces and compare our proposal against hand-optimized vendor-supplied numerical libraries and against commercial compilers able to perform optimizing code transformations such as inner unrolling, unroll-and-jam, and software pipelining. Measurements were taken on three different superscalar microprocessors. Results will show that our method outperforms the native compilers (showing speedups of 2.5 in average) and matches the performance of vendor-supplied numerical libraries. The general conclusion is that compiler technology can make it possible for nonrectangular loop nests to achieve as high performance as hand-optimized codes.


title: Type-preserving compilation of Featherweight Java

authors:
Christopher League
Zhong Shao
Valery Trifonov

abstract: We present an efficient encoding of core Java constructs in a simple, implementable typed intermediate language. The encoding, after type erasure, has the same operational behavior as a standard implementation using vtables and self-application for method invocation. Classes inherit super-class methods with no overhead. We support mutually recursive classes while preserving separate compilation. Our strategy extends naturally to a significant subset of Java, including interfaces and privacy. The formal translation using Featherweight Java allows comprehensible type-preservation proofs and serves as a starting point for extending the translation to new features. Our work provides a foundation for supporting certifying compilation of Java-like class-based languages in a type-theoretic framework.


title: Automatic data and computation decomposition on distributed memory parallel computers

authors:
PeiZong Lee
Zvi M. Kedem

abstract: To exploit parallelism on shared memory parallel computers (SMPCs), it is natural to focus on decomposing the computation (mainly by distributing the iterations of the nested Do-Loops). In contrast, on distributed memory parallel computers (DMPCs), the decomposition of computation and the distribution of data must both be handled---in order to balance the computation load and to minimize the migration of data. We propose and validate experimentally a method for handling computations and data synergistically to minimize the overall execution time on DMPCs. The method is based on a number of novel techniques, also presented in this article. The core idea is to rank the "importance" of data arrays in a program and specify some of the dominant. The intuition is that the dominant arrays are the ones whose migration would be the most expensive. Using the correspondence between iteration space mapping vectors and distributed dimensions of the dominant data array in each nested Do-loop, allows us to design algorithms for determining data and computation decompositions at the same time. Based on data distribution, computation decomposition for each nested Do-loop is determined based on either the "owner computes" rule or the "owner stores" rule with respect to the dominant data array. If all temporal dependence relations across iteration partitions are regular, we use tiling to allow pipelining and the overlapping of computation and communication. However, in order to use tiling on DMPCs, we needed to extend the existing techniques for determining tiling vectors and tile sizes, as they were originally suited for SMPCs only. The overall method is illustrated on programs for the 2D heat equation, for the Gaussian elimination with pivoting, and for the 2D fast Fourier transform on a linear processor array and on a 2D processor grid.


title: Data abstraction and information hiding

authors:
K. Rustan M. Leino
Greg Nelson

abstract: This article describes an approach for verifying programs in the presence of data abstraction and information hiding, which are key features of modern programming languages with objects and modules. This article draws on our experience building and using an automatic program checker, and focuses on the property ofmodular soundness: that is, the property that the separate verifications of the individual modules of a program suffice to ensure the correctness of the composite program. We found this desirable property surprisingly difficult to achieve. A key feature of our methodology for modular soundness is a new specification construct: theabstraction dependency, which reveals which concrete variables appear in the representation of a given abstract variable, without revealing the abstraction function itself. This article discusses in detail two varieties of abstraction dependencies: static and dynamic. The article also presents a new technical definition of modular soundness as a monotonicity property of verifiability with respect to scope and uses this technical definition to formally prove the modular soundness of a programming discipline for static dependencies.


title: The apprentice challenge

authors:
J Strother Moore
George Porter

abstract: We describe a mechanically checked proof of a property of a small system of Java programs involving an unbounded number of threads and synchronization, via monitors. We adopt the output of the javac compiler as the semantics and verify the system at the bytecode level under an operational semantics for the JVM. We assume a sequentially consistent memory model and atomicity at the bytecode level. Our operational semantics is expressed in ACL2, a Lisp-based logic of recursive functions. Our proofs are checked with the ACL2 theorem prover. The proof involves reasoning about arithmetic; infinite loops; the creation and modification of instance objects in the heap, including threads; the inheritance of fields from superclasses; pointer chasing and smashing; the invocation of instance methods (and the concomitant dynamic method resolution); use of the start method on thread objects; the use of monitors to attain synchronization between threads; and consideration of all possible interleavings (at the bytecode level) over an unbounded number of threads. Readers familiar with monitor-based proofs of mutual exclusion will recognize our proof as fairly classical. The novelty here comes from (i) the complexity of the individual operations on the abstract machine; (ii) the dependencies between Java threads, heap objects, and synchronization; (iii) the bytecode-level interleaving; (iv) the unbounded number of threads; (v) the presence in the heap of incompletely initialized threads and other objects; and (vi) the proof engineering permitting automatic mechanical verification of code-level theorems. We discuss these issues. The problem posed here is also put forth as a benchmark against which to measure other approaches to formally proving properties of multithreaded Java programs.


title: Efficient and precise array access analysis

authors:
Yunheung Paek
Jay P. Hoeflinger
David A. Padua

abstract: A number of existing compiler techniques hinge on the analysis of array accesses in a program. The most important task in array access analysis is to collect the information about array accesses of interest and summarize it in some standard form. Traditional forms used in array access analysis are sensitive to the complexity of array subscripts; that is, they are usually quite accurate and efficient for simple array subscripting expressions, but lose accuracy or require potentially expensive algorithms for complex subscripts. Our study has revealed that in many programs, particularly numerical applications, many access patterns are simple in nature even when the subscripting expressions are complex. Based on this analysis, we have developed a new, general array region representational form, called the linear memory access descriptor (LMAD). The key idea of the LMAD is to relate all memory accesses to the linear machine memory rather than to the shape of the logical data structures of a programming language. This form helps us expose the simplicity of the actual patterns of array accesses in memory, which may be hidden by complex array subscript expressions. Our recent experimental studies show that our new representation simplifies array access analysis and, thus, enables efficient and accurate compiler analysis.


title: On loops, dominators, and dominance frontiers

abstract: This article explores the concept of loops and loop nesting forests of control-flow graphs, using the problem of constructing the dominator tree of a graph and the problem of computing the iterated dominance frontier of a set of vertices in a graph as guiding applications. The contributions of this article include: (1) An axiomatic characterization, as well as a constructive characterization, of a family of loop nesting forests that includes various specific loop nesting forests that have been previously defined. (2) The definition of a new loop nesting forest, as well as an efficient, almost linear-time, algorithm for constructing this forest. (3) An illustration of how loop nesting forests can be used to transform arbitrary (potentially irreducible) problem instances into equivalent acylic graph problem instances in the case of the two problems of (a) constructing the dominator tree of a graph, and (b) computing the iterated dominance frontier of a set of vertices in a graph, leading to new, almost linear-time, algorithms for these problems.


title: Parametric shape analysis via 3-valued logic

authors:
Shmuel Sagiv
Thomas W. Reps
Reinhard Wilhelm

abstract: Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This article presents a parametric framework for shape analysis that can be instantiated in different ways to create different shape-analysis algorithms that provide varying degrees of efficiency and precision. A key innovation of the work is that the stores that can possibly arise during execution are represented (conservatively) using 3-valued logical structures. The framework is instantiated in different ways by varying the predicates used in the 3-valued logic. The class of programs to which a given instantiation of the framework can be applied is not limited a priori (i.e., as in some work on shape analysis, to programs that manipulate only lists, trees, DAGS, etc.); each instantiation of the framework can be applied to any program, but may produce imprecise results (albeit conservative ones) due to the set of predicates employed.


title: Practical extraction techniques for Java

authors:
Frank Tip
Peter F. Sweeney
Chris Laffra
Aldo Eisma
David Streeter

abstract: Reducing application size is important for software that is distributed via the internet, in order to keep download times manageable, and in the domain of embedded systems, where applications are often stored in (Read-Only or Flash) memory. This paper explores extraction techniques such as the removal of unreachable methods and redundant fields, inlining of method calls, and transformation of the class hierarchy for reducing application size. We implemented a number of extraction techniques in Jax , an application extractor for Java, and evaluated their effectiveness on a set of large Java applications. We found that, on average, the class file archives for these benchmarks were reduced to 37.5% of their original size. Modeling dynamic language features such as reflection, and extracting software distributions other than complete applications requires additional user input. We present a uniform approach for supplying this input that relies on MEL, a modular specification language. We also discuss a number of issues and challenges associated with the extraction of embedded systems applications.


title: Handling irreducible loops: optimized node splitting versus DJ-graphs

authors:
Sebastian Unger
Frank Mueller

abstract: This paper addresses the question of how to handle irreducible regions during optimization, which has become even more relevant for contemporary processors since recent VLIW-like architectures highly rely on instruction scheduling. The contributions of this paper are twofold. First, a method of optimized node splitting to transform irreducible regions of control flow into reducible regions is formally defined and its correctness is shown. This method is superior to approaches previously published since it reduces the number of replicated nodes by comparison. Second, three methods that handle regions of irreducible control flow are evaluated with respect to their impact on compiler optimizations. First, traditional node splitting is evaluated. Second, optimized node splitting is implemented. Third, DJ-Graphs are utilized to recognize nesting of irreducible (and reducible) loops and apply common loop optimizations extended for irreducible loops. Experiments compare the performance of these approaches with unrecognized irreducible loops that cannot be subject to loop optimizations, which is typical for contemporary compilers. Measurements show improvements of 1 to 40% for these methods of handling irreducible loops over the unoptimized case. Optimized node splitting may be chosen to retrofit existing compilers since it has the advantage that it only requires few changes to an optimizing compiler while limiting the code growth of compiled programs compared to traditional node splitting. Recognizing loops via DJ-Graphs should be chosen for new compiler developments since it requires more changes to the optimizer but does not significantly change the code size of compiled programs while yielding comparable improvements. Handling irreducible loops should even yield more benefits for exploiting instruction-level parallelism of modern architectures in the context of global instruction scheduling and optimization techniques that may introduce irreducible loops, such as enhanced modulo scheduling.


title: Efficient and effective branch reordering using profile data

authors:
Minghui Yang
Gang-Ryung Uh
David B. Whalley

abstract: The conditional branch has long been considered an expensive operation. The relative cost of conditional branches has increased as recently designed machines are now relying on deeper pipelines and higher multiple issue. Reducing the number of conditional branches executed often results in a substantial performance benefit. This paper describes a code-improving transformation to reorder sequences of conditional branches that compare a common variable to constants. The goal is to obtain an ordering where the fewest average number of branches in the sequence will be executed. First, sequences of branches that can be reordered are detected in the control flow. Second, profiling information is collected to predict the probability that each branch will transfer control out of the sequence. Third, the cost of performing each conditional branch is estimated. Fourth, the most beneficial ordering of the branches based on the estimated probability and cost is selected. The most beneficial ordering often includes the insertion of additional conditional branches that did not previously exist in the sequence. Finally, the control flow is restructured to reflect the new ordering. The results of applying the transformation are on average reductions of about 8% fewer instructions executed and 13% branches performed, as well as about a 4% decrease in execution time.


title: The receptive distributed pi-calculus

authors:
Roberto M. Amadio
Gérard Boudol
Cédric Lhoussaine

abstract: We study an asynchronous distributed π-calculus, with constructs for localities and migration. We show that a static analysis ensures the receptiveness of channel names, which, together with a simple type system, guarantees the message deliverability property. This property states that any migrating message will find an appropriate receiver at its destination locality. We argue that this distributed, receptive calculus is still expressive enough while allowing for an effective type inference à la ML.


title: Jam - designing a Java extension with mixins

authors:
Davide Ancona
Giovanni Lagorio
Elena Zucca

abstract: In this paper we present Jam, an extension of the Java language supporting mixins , that is, parametric heir classes. A mixin declaration in Jam is similar to a Java heir class declaration, except that it does not extend a fixed parent class, but simply specifies the set of fields and methods a generic parent should provide. In this way, the same mixin can be instantiated on many parent classes, producing different heirs, thus avoiding code duplication and largely improving modularity and reuse. Moreover, as happens for classes and interfaces, mixin names are reference types, and all the classes obtained by instantiating the same mixin are considered subtypes of the corresponding type, and hence can be handled in a uniform way through the common interface. This possibility allows a programming style where different ingredients are "mixed" together in defining a class; this paradigm is somewhat similar to that based on multiple inheritance, but avoids its complication.The language has been designed with the main objective in mind to obtain, rather than a new theoretical language, a working and smooth extension of Java. That means, on the design side, that we have faced the challenging problem of integrating the Java overall principles and complex type system with this new notion; on the implementation side, it means that we have developed a Jam-to-Java translator which makes Jam sources executable on every Java Virtual Machine.


title: Escape analysis for JavaTM: Theory and practice

abstract: Escape analysis is a static analysis that determines whether the lifetime of data may exceed its static scope.This paper first presents the design and correctness proof of an escape analysis for Java TM . This analysis is interprocedural, context sensitive, and as flow-sensitive as the static single assignment form. So, assignments to object fields are analyzed in a flow-insensitive manner. Since Java is an imperative language, the effect of assignments must be precisely determined. This goal is achieved thanks to our technique using two interdependent analyses, one forward, one backward. We introduce a new method to prove the correctness of this analysis, using aliases as an intermediate step. We use integers to represent the escaping parts of values, which leads to a fast and precise analysis.Our implementation [Blanchet 1999], which applies to the whole Java language, is then presented. Escape analysis is applied to stack allocation and synchronization elimination. In our benchmarks, we stack allocate 13% to 95% of data, eliminate more than 20% of synchronizations on most programs (94% and 99% on two examples) and get up to 43% runtime decrease (21% on average). Our detailed experimental study on large programs shows that the improvement comes more from the decrease of the garbage collection and allocation times than from improvements on data locality, contrary to what happened for ML. This comes from the difference in the garbage collectors.


title: PolyTOIL: A type-safe polymorphic object-oriented language

authors:
Kim B. Bruce
Angela Schuett
Robert van Gent
Adrian Fiech

abstract: PolyTOIL is a new statically typed polymorphic object-oriented programming language that is provably typesafe. By separating the definitions of subtyping and inheritance, providing a name for the type of self, and carefully defining the type-checking rules, we have obtained a language that is very expressive while supporting modular type-checking of classes. Thematchingrelation on types, which is related to F-bounded quantification, is used both in stating type-checking rules and expressing the bounds on type parameters for polymorphism. The design of PolyTOIL is based on a careful formal definition of type-checking rules and semantics. A proof of type safety is obtained with the aid of a subject reduction theorem.


title: Stack allocation and synchronization optimizations for Java using escape analysis

authors:
Jong-Deok Choi
Manish Gupta
Mauricio J. Serrano
Vugranam C. Sreedhar
Samuel P. Midkiff

abstract: This article presents an escape analysis framework for Java to determine (1) if an object is not reachable after its method of creation returns, allowing the object to be allocated on the stack, and (2) if an object is reachable only from a single thread during its lifetime, allowing unnecessary synchronization operations on that object to be removed. We introduce a new program abstraction for escape analysis, the connection graph , that is used to establish reachability relationships between objects and object references. We show that the connection graph can be succinctly summarized for each method such that the same summary information may be used in different calling contexts without introducing imprecision into the analysis. We present an interprocedural algorithm that uses the above property to efficiently compute the connection graph and identify the nonescaping objects for methods and threads. The experimental results, from a prototype implementation of our framework in the IBM High Performance Compiler for Java, are very promising. The percentage of objects that may be allocated on the stack exceeds 70% of all dynamically created objects in the user code in three out of the ten benchmarks (with a median of 19%); 11% to 92% of all mutex lock operations are eliminated in those 10 programs (with a median of 51%), and the overall execution time reduction ranges from 2% to 23% (with a median of 7%) on a 333-MHz PowerPC workstation with 512 MB memory.


title: Extending Java for high-level Web service construction

authors:
Aske Simon Christensen
Anders Møller
Michael I. Schwartzbach

abstract: We incorporate innovations from the project into the Java language to provide high-level features for Web service programming. The resulting language, JWIG, contains an advanced session model and a flexible mechanism for dynamic construction of XML documents, in particular XHTML. To support program development we provide a suite of program analyses that at compile time verify for a given program that no runtime errors can occur while building documents or receiving form input, and that all documents being shown are valid according to the document type definition for XHTML 1.0.We compare JWIG with Servlets and JSP which are widely used Web service development platforms. Our implementation and evaluation of JWIG indicate that the language extensions can simplify the program structure and that the analyses are sufficiently fast and precise to be practically useful.


title: Rank 2 intersection types for local definitions and conditional expressions

abstract: We propose a rank 2 intersection type system with new typing rules for local definitions (let-expressions and letrec-expressions) and conditional expressions (if-expressions and match-expressions). This is a further step towards the use of intersection types in "real" programming languages.The technique for typing local definitions relies entirely on the principal typing property (i.e. it does not depend on particulars of rank 2 intersection), so it can be applied to any system with principal typings. The technique for typing conditional expressions, which is based on the idea of introducing metrics on types to "limit the use" of the intersection type constructor in the types assigned to the branches of the conditionals, is instead tailored to rank 2 intersection. However, the underlying idea might also be useful for other type systems.


title: Stack inspection: Theory and variants

authors:
Cédric Fournet
Andrew D. Gordon

abstract: Stack inspection is a security mechanism implemented in runtimes such as the JVM and the CLR to accommodate components with diverse levels of trust. Although stack inspection enables the fine-grained expression of access control policies, it has rather a complex and subtle semantics. We present a formal semantics and an equational theory to explain how stack inspection affects program behavior and code optimisations. We discuss the security properties enforced by stack inspection, and also consider variants with stronger, simpler properties.


title: Generating LR syntax error messages from examples

abstract: LR parser generators are powerful and well-understood, but the parsers they generate are not suited to provide good error messages. Many compilers incur extensive modifications to the source grammar to produce useful syntax error messages. Interpreting the parse state (and input token) at the time of error is a nonintrusive alternative that does not entangle the error recovery mechanism in error message production. Unfortunately, every change to the grammar may significantly alter the mapping from parse states to diagnostic messages, creating a maintenance problem. Merr is a tool that allows a compiler writer to associate diagnostic messages with syntax errors by example, avoiding the need to add error productions to the grammar or interpret integer parse states. From a specification of errors and messages, Merr runs the compiler on each example error to obtain the relevant parse state and input token, and generates a yyerror() function that maps parse states and input tokens to diagnostic messages. Merr enables useful syntax error messages in LR-based compilers in a manner that is robust in the presence of grammar changes.


title: Continuous program optimization: A case study

authors:
Thomas Kistler
Michael Franz

abstract: Much of the software in everyday operation is not making optimal use of the hardware on which it actually runs. Among the reasons for this discrepancy are hardware/software mismatches, modularization overheads introduced by software engineering considerations, and the inability of systems to adapt to users' behaviors.A solution to these problems is to delay code generation until load time. This is the earliest point at which a piece of software can be fine-tuned to the actual capabilities of the hardware on which it is about to be executed, and also the earliest point at wich modularization overheads can be overcome by global optimization.A still better match between software and hardware can be achieved by replacing the already executing software at regular intervals by new versions constructed on-the-fly using a background code re-optimizer. This not only enables the use of live profiling data to guide optimization decisions, but also facilitates adaptation to changing usage patterns and the late addition of dynamic link libraries.This paper presents a system that provides code generation at load-time and continuous program optimization at run-time. First, the architecture of the system is presented. Then, two optimization techniques are discussed that were developed specifically in the context of continuous optimization. The first of these optimizations continually adjusts the storage layouts of dynamic data structures to maximize data cache locality, while the second performs profile-driven instruction re-scheduling to increase instruction-level parallelism. These two optimizations have very different cost/benefit ratios, presented in a series of benchmarks. The paper concludes with an outlook to future research directions and an enumeration of some remaining research problems.The empirical results presented in this paper make a case in favor of continuous optimization, but indicate that it needs to be applied judiciously. In many situations, the costs of dynamic optimizations outweigh their benefit, so that no break-even point is ever reached. In favorable circumstances, on the other hand, speed-ups of over 120% have been observed. It appears as if the main beneficiaries of continuous optimization are shared libraries, which at different times can be optimized in the context of the currently dominant client application.


title: Mobile safe ambients

authors:
Francesca Levi
Davide Sangiorgi

abstract: Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences , which are similar to the interferences one finds in CCS and π-calculus; and grave interferences , which are more dangerous and may be regarded as programming errors. To control interferences, the MA movement primitives are modified; the resulting calculus is called Mobile Safe Ambients (SA).The modification also has computational significance. In the MA interaction rules, an ambient may enter, exit, or open another ambient. The second ambient undergoes the action; it has no control on when the action takes place. In SA this is rectified: any movement takes place only if both participants agree.Existing type systems for MA can be easily adapted to SA. The type systems for controlling mobility, however, appear to be more powerful in SA, in that (i) type systems for MA may give more precise information when transplanted onto SA , and (ii) new type systems may be defined. Two type systems are presented that remove all grave interferences.Other advantages of SA are: a useful algebraic theory; programs sometimes more robust (they require milder conditions for correctness) and/or simpler. All these points are illustrated in several examples.


title: Fractal symbolic analysis

authors:
Vijay Menon
Keshav Pingali
Nikolay Mateev

abstract: Modern compilers restructure programs to improve their efficiency. Dependence analysis is the most widely used technique for proving the correctness of such transformations, but it suffers from the limitation that it considers only the memory locations read and written by a statement without considering what is being computed by that statement. Exploiting the semantics of program statements permits more transformations to be proved correct, and is critical for automatic restructuring of codes such as LU with partial pivoting.One approach to exploiting the semantics of program statements is symbolic analysis and comparison of programs.In principle, this technique is very powerful, but in practice, it is intractable for all but the simplest programs.In this paper, we propose a new form of symbolic analysis and comparison of programs which is appropriate for use in restructuring compilers. Fractal symbolic analysis is an approximate symbolic analysis that compares a program and its transformed version by repeatedly simplifying these programs until symbolic analysis becomes tractable while ensuring that equality of the simplified programs is sufficient to guarantee equality of the original programs.Fractal symbolic analysis combines some of the power of symbolic analysis with the tractability of dependence analysis. We discuss a prototype implementation of fractal symbolic analysis, and show how it can be used to solve the long-open problem of verifying the correctness of transformations required to improve the cache performance of LU factorization with partial pivoting.


title: Information flow inference for ML

authors:
François Pottier
Vincent Simonet

abstract: This paper presents a type-based information flow analysis for a call-by-value λ-calculus equipped with references, exceptions and let-polymorphism, which we refer to as ML. The type system is constraint-based and has decidable type inference. Its noninterference proof is reasonably light-weight, thanks to the use of a number of orthogonal techniques. First, a syntactic segregation between values and expressions allows a lighter formulation of the type system. Second, noninterference is reduced to subject reduction for a nonstandard language extension. Lastly, a semi-syntactic approach to type soundness allows dealing with constraint-based polymorphism separately.


title: A transformational approach to binary translation of delayed branches

authors:
Norman Ramsey
Cristina Cifuentes

abstract: A binary translator examines binary code for a source machine and generates code for a target machine. Understanding what to do with delayed branches in binary code can involve tricky case analyses, for example, if there is a branch instruction in a delay slot. This article presents a disciplined method for deriving such case analyses. The method identifies problematic cases, shows the translations for the nonproblematic cases, and gives confidence that all cases are considered. The method supports such common architectures as SPARC, MIPS, and PA-RISC, and it should apply to any tool that analyzes machine instructions. We begin by writing a very simple interpreter for the source machine's code. We then transform the interpreter into an interpreter for a target machine without delayed branches. To maintain the semantics of the program being interpreted, we simultaneously transform the sequence of source-machine instructions into a sequence of target-machine instructions. The transformation of the instructions becomes our algorithm for binary translation.


title: A foundation for embedded languages

abstract: Recent work on embedding object languages into Haskell use "phantom types" (i.e., parameterized types whose parameter does not occur on the right-hand side of the type definition) to ensure that the embedded object-language terms are simply typed. But is it a safe assumption that only simply-typed terms can be represented in Haskell using phantom types? And conversely, can all simply-typed terms be represented in Haskell under the restrictions imposed by phantom types? In this article we investigate the conditions under which these assumptions are true: We show that these questions can be answered affirmatively for an idealized Haskell-like language and discuss to which extent Haskell can be used as a meta-language.


title: Eliminating synchronization bottlenecks using adaptive replication

authors:
Martin C. Rinard
Pedro C. Diniz

abstract: This article presents a new technique, adaptive replication, for automatically eliminating synchronization bottlenecks in multithreaded programs that perform atomic operations on objects. Synchronization bottlenecks occur when multiple threads attempt to concurrently update the same object. It is often possible to eliminate synchronization bottlenecks by replicating objects. Each thread can then update its own local replica without synchronization and without interacting with other threads. When the computation needs to access the original object, it combines the replicas to produce the correct values in the original object. One potential problem is that eagerly replicating all objects may lead to performance degradation and excessive memory consumption.Adaptive replication eliminates unnecessary replication by dynamically detecting contention at each object to find and replicate only those objects that would otherwise cause synchronization bottlenecks. We have implemented adaptive replication in the context of a parallelizing compiler for a subset of C++. Given an unannotated sequential program written in C++, the compiler automatically extracts the concurrency, determines when it is legal to apply adaptive replication, and generates parallel code that uses adaptive replication to efficiently eliminate synchronization bottlenecks.In addition to automatic parallelization and adaptive replication, our compiler also implements a lock coarsening transformation that increases the granularity at which the computation locks objects. The advantage is a reduction in the frequency with which the computation acquires and releases locks; the potential disadvantage is the introduction of new synchronization bottlenecks caused by increases in the sizes of the critical sections. Because the adaptive replication transformation takes place at lock acquisition sites, there is a synergistic interaction between lock coarsening and adaptive replication. Lock coarsening drives down the overhead of using adaptive replication, and adaptive replication eliminates synchronization bottlenecks associated with the overaggressive use of lock coarsening.Our experimental results show that, for our set of benchmark programs, the combination of lock coarsening and adaptive replication can eliminate synchronization bottlenecks and significantly reduce the synchronization and replication overhead as compared to versions that use none or only one of the transformations.


title: Pointer analysis for structured parallel programs

authors:
Radu Rugina
Martin C. Rinard

abstract: This paper presents a novel interprocedural, flow-sensitive, and context-sensitive pointer analysis algorithm for multithreaded programs that may concurrently update shared pointers. The algorithm is designed to handle programs with structured parallel constructs, including fork-join constructs, parallel loops, and conditionally spawned threads. For each pointer and each program point, the algorithm computes a conservative approximation of the memory locations to which that pointer may point. The algorithm correctly handles a wide range of programming language constructs, including recursive functions, recursively generated parallelism, function pointers, structures, arrays, nested structures and arrays, pointer arithmetic, casts between different pointer types, heap and stack allocated memory, shared global variables, and thread-private global variables. We have implemented the algorithm in the SUIF compiler system and used the implementation to analyze a set of multithreaded programs written in the Cilk programming language. Our experimental results show that the analysis has good precision and converges quickly for our set of Cilk programs.


title: Intensional analysis of quantified types

authors:
Bratin Saha
Valery Trifonov
Zhong Shao

abstract: Compilers for polymorphic languages can use run-time type inspection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data structures. Intensional type analysis is a type-theoretic framework for expressing and certifying such type-analyzing computations. Unfortunately, existing approaches to intensional analysis do not work well on quantified types such as existential or polymorphic types. This makes it impossible to code (in a type-safe language) applications such as garbage collection, persistency, or marshalling which must be able to examine the type of any run-time value. We present a typed intermediate language that supports the analysis of quantified types. In particular, we provide both type-level and term-level constructs for analyzing quantified types. Our system supports structural induction on quantified types yet type-checking remains decidable. We also show that our system is compatible with a type-erasure semantics.


title: Automatic program specialization for Java

authors:
Ulrik Pagh Schultz
Julia L. Lawall
Charles Consel

abstract: The object-oriented style of programming facilitates program adaptation and enhances program genericness, but at the expense of efficiency. We demonstrate experimentally that state-of-the-art Java compilers fail to compensate for the use of object-oriented abstractions in the implementation of generic programs, and that program specialization can eliminate a significant portion of these overheads. We present an automatic program specializer for Java, illustrate its use through detailed case studies, and demonstrate experimentally that it can significantly reduce program execution time. Although automatic program specialization could be seen as being subsumed by existing optimizing compiler technology, we show that specialization and compiler optimization are in fact complementary.


title: Class analyses as abstract interpretations of trace semantics

authors:
Fausto Spoto
Thomas P. Jensen

abstract: We use abstract interpretation to abstract a compositional trace semantics for a simple imperative object-oriented language into its projection over a set of program points called watchpoints . We say that the resulting watchpoint semantics is focused on the watchpoints. Every abstraction of the computational domain of this semantics induces an abstract, still compositional, and focused watchpoint semantics. This establishes a basis for developing static analyses obtaining information pertaining only to the watchpoints. As an example, we consider three domains for class analysis of object-oriented programs derived from three techniques present in the literature, namely, rapid type analysis, a simple dataflow analysis, and a constraint-based analysis. We obtain three static analyses which are provably correct and whose abstract operations are provably optimal. Moreover, we prove that our formalization of the constraint-based analysis is more precise than that of the other two analyses. We have implemented our watchpoint semantics and our three domains for class analysis. This implementation shows that the time and space costs of the analysis are actually proportional to the number of watchpoints, as a consequence of the focused nature of the watchpoint semantics.


title: Modular refinement of hierarchic reactive machines

authors:
Rajeev Alur
Radu Grosu

abstract: Scalable formal analysis of reactive programs demands integration of modular reasoning techniques with existing analysis tools. Modular reasoning principles such as abstraction, compositional refinement, and assume-guarantee reasoning are well understood for architectural hierarchy that describes the communication structure between component processes, and have been shown to be useful. In this paper, we develop the theory of modular reasoning for behavior hierarchy that describes control structure using hierarchic modes. From Statecharts to UML, behavior hierarchy has been an integral component of many software design languages, but only syntactically. We present the hierarchic reactive modules language that retains powerful features such as nested modes, mode reuse, exceptions, group transitions, history, and conjunctive modes, and yet has a semantic notion of mode hierarchy. We present an observational trace semantics for modes that provides the basis for mode refinement. We show the refinement to be compositional with respect to the mode constructors, and develop an assume-guarantee reasoning principle.


title: Synthesis of fault-tolerant concurrent programs

authors:
Paul C. Attie
Anish Arora
E. Allen Emerson

abstract: Methods for mechanically synthesizing concurrent programs from temporal logic specifications obviate the need to manually construct a program and compose a proof of its correctness. A serious drawback of extant synthesis methods, however, is that they produce concurrent programs for models of computation that are often unrealistic. In particular, these methods assume completely fault-free operation, that is, the programs they produce are fault-intolerant. In this paper, we show how to mechanically synthesize fault-tolerant concurrent programs for various fault classes. We illustrate our method by synthesizing fault-tolerant solutions to the mutual exclusion and barrier synchronization problems.


title: Modern concurrency abstractions for C#

authors:
Nick Benton
Luca Cardelli
Cédric Fournet

abstract: Polyphonic C ♯ is an extension of the C ♯ language with new asynchronous concurrency constructs, based on the join calculus. We describe the design and implementation of the language and give examples of its use in addressing a range of concurrent programming problems.


title: Access control for mobile agents: The calculus of boxed ambients

authors:
Michele Bugliesi
Giuseppe Castagna
Silvia Crafa

abstract: Boxed Ambients are a variant of Mobile Ambients that result from dropping the open capability and introducing new primitives for ambient communication. The new model of communication is faithful to the principles of distribution and location-awareness of Mobile Ambients, and complements the constructs in and out for mobility with finer-grained mechanisms for ambient interaction. We introduce the new calculus, study the impact of the new mechanisms for communication of typing and mobility, and show that they yield an effective framework for resource protection and access control in distributed systems.


title: Logic of global synchrony

authors:
Yifeng Chen
Jeff W. Sanders

abstract: An intermediate-level specification formalism (i.e., specification language supported by laws and a semantic model), Logs, is presented for PRAM and BSP styles of parallel programming. It extends pre-post sequential semantics to reveal states at points of global synchronization. The result is an integration of the pre-post and reactive-process styles of specification. The language consists of only six commands from which other useful commands can be derived. Parallel composition is simply logical conjunction and hence compositional. A simple predicative semantics and a complete set of algebraic laws are presented. Novel ingredients include the separation, in our reactive context, of the processes for nontermination and for abortion which coincide in standard programming models; the use of partitions, combining the terminating behavior of one program with the nonterminating behavior of another; and a fixpoint operator, the partitioned fixpoint. Our semantics benefits from the recent "healthiness function" approach for predicative semantics. Use of Logs, along with the laws for reasoning about it, is demonstrated on two problems: matrix multiplication (a terminating numerical computation) and the dining philosophers (a reactive computation). The style of reasoning is so close to programming practice that direct transformation from Logs specifications to real PRAM and BSP programs becomes possible.


title: Offline partial evaluation can be as accurate as online partial evaluation

authors:
Niels H. Christensen
Robert Glück

abstract: We show that the accuracy of online partial evaluation, or polyvariant specialization based on constant propagation, can be simulated by offline partial evaluation using a maximally polyvariant binding-time analysis. We point out that, while their accuracy is the same, online partial evaluation offers better opportunities for powerful generalization strategies. Our results are presented using a flowchart language with recursive procedures.


title: A tail-recursive machine with stack inspection

authors:
John Clements
Matthias Felleisen

abstract: Security folklore holds that a security mechanism based on stack inspection is incompatible with a global tail call optimization policy; that an implementation of such a language must allocate memory for a source-code tail call, and a program that uses only tail calls (and no other memory-allocating construct) may nevertheless exhaust the available memory. In this article, we prove this widely held belief wrong. We exhibit an abstract machine for a language with security stack inspection whose space consumption function is equivalent to that of the canonical tail call optimizing abstract machine. Our machine is surprisingly simple and suggests that tail calls are as easy to implement in a security setting as they are in a conventional one.


title: Hancock: A language for analyzing transactional data streams

authors:
Corinna Cortes
Kathleen Fisher
Daryl Pregibon
Anne Rogers
Frederick Smith

abstract: Massive transaction streams present a number of opportunities for data mining techniques. The transactions in such streams might represent calls on a telephone network, commercial credit card purchases, stock market trades, or HTTP requests to a web server. While historically such data have been collected for billing or security purposes, they are now being used to discover how the transactors, for example, credit-card numbers or IP addresses, use the associated services.Over the past 5 years, we have computed evolving profiles (called signatures ) of transactors in several very large data streams. The signature for each transactor captures the salient features of his or her behavior through time. Programs for processing signatures must be highly optimized because of the size of the data stream (several gigabytes per day) and the number of signatures to maintain (hundreds of millions). Originally, we wrote such programs directly in C, but because these programs often sacrificed readability for performance, they were difficult to verify and maintain.Hancock is a domain-specific language we created to express computationally efficient signature programs cleanly. In this paper, we describe the obstacles to computing signatures from massive streams and explain how Hancock addresses these problems. For expository purposes, we present Hancock using a running example from the telecommunications industry; however, the language itself is general and applies equally well to other data sources.


title: An interval constraint system for lattice domains

authors:
Antonio J. Fernández
Patricia M. Hill

abstract: We present a generic framework for defining and solving interval constraints on any set of domains (finite or infinite) that are lattices. The approach is based on the use of a single form of constraint similar to that of an indexical used by CLP for finite domains and on a particular generic definition of an interval domain built from an arbitrary lattice. We provide the theoretical foundations for this framework and a schematic procedure for the operational semantics. Examples are provided that illustrate how new (compound) constraint solvers can be constructed from existing solvers using lattice combinators and how different solvers (possibly on distinct domains) can communicate and hence, cooperate in solving a problem. We describe the language clp ( L ), which is a prototype implementation of this framework and discuss ways in which this implementation may be improved.


title: Natural semantics as a static program analysis framework

authors:
Sabine Glesner
Wolf Zimmermann

abstract: Natural semantics specifications have become mainstream in the formal specification of programming language semantics during the last 10 years. In this article, we set up sorted natural semantics as a specification framework which is able to express static semantic information of programming languages declaratively in a uniform way and allows one at the same time to generate corresponding analyses. Such static semantic information comprises context-sensitive properties which are checked in the semantic analysis phase of compilers as well as further static program analyses such as, for example, classical data and control flow analyses or type and effect systems. The latter require fixed-point analyses to determine their solutions. We show that, given a sorted natural semantics specification, we can generate the corresponding analysis. Therefore, we classify the solution of such an analysis by the notion of a proof tree. We show that a proof tree can be computed by solving an equivalent residuation problem. In case of the semantic analysis, this solution can be found by a basic algorithm. We show that its efficiency can be enhanced using solution strategies. We also demonstrate our prototype implementation of the basic algorithm which proves its applicability in practical situations. With the results of this article, we have established natural semantics as a framework which closes the gap between declarative and operational specification methods for static semantic properties as well as between specification frameworks for the semantic analysis. In particular, we show that natural semantics is expressive enough to define fixed-point program analyses.


title: Send-receive considered harmful: Myths and realities of message passing

abstract: During the software crisis of the 1960s, Dijkstra's famous thesis "goto considered harmful" paved the way for structured programming. This short communication suggests that many current difficulties of parallel programming based on message passing are caused by poorly structured communication, which is a consequence of using low-level send-receive primitives. We argue that, like goto in sequential programs, send-receive should be avoided as far as possible and replaced by collective operations in the setting of message passing. We dispute some widely held opinions about the apparent superiority of pairwise communication over collective communication and present substantial theoretical and empirical evidence to the contrary in the context of MPI (Message Passing Interface).


title: Polymorphic specialization for ML

authors:
Simon Helsen
Peter Thiemann

abstract: We present a framework for offline partial evaluation for call-by-value functional programming languages with an ML-style typing discipline. This includes a binding-time analysis which is (1) polymorphic with respect to binding times; (2) allows the use of polymorphic recursion with respect to binding times; (3) is applicable to a polymorphically typed term; and (4) is proven correct with respect to a novel small-step specialization semantics.The main innovation is to build the analysis on top of the region calculus of Tofte and Talpin [1994], thus leveraging the tools and techniques developed for it. Our approach factorizes the binding-time analysis into region inference and a subsequent constraint analysis. The key insight underlying our framework is to consider binding times as properties of regions.Specialization is specified as a small-step semantics, building on previous work on syntactic-type soundness results for the region calculus. Using similar syntactic proof techniques, we prove soundness of the binding-time analysis with respect to the specializer. In addition, we prove that specialization preserves the call-by-value semantics of the region calculus by showing that the reductions of the specializer are contextual equivalences in the region calculus.


title: The pattern calculus

abstract: There is a significant class of operations such as mapping that are common to all data structures. The goal of generic programming is to support these operations on arbitrary data types without having to recode for each new type. The pattern calculus and combinatory type system reach this goal by representing each data structure as a combination of names and a finite set of constructors. These can be used to define generic functions by pattern-matching programs in which each pattern has a different type. Evaluation is type-free. Polymorphism is captured by quantifying over type variables that represent unknown structures. A practical type inference algorithm is provided.


title: JR: Flexible distributed programming in an extended Java

authors:
Aaron W. Keen
Tingjian Ge
Justin T. Maris
Ronald A. Olsson

abstract: Java provides a clean object-oriented programming model and allows for inherently system-independent programs. Unfortunately, Java has a limited concurrency model, providing only threads and remote method invocation (RMI).The JR programming language extends Java to provide a rich concurrency model, based on that of SR. JR provides dynamic remote virtual machine creation, dynamic remote object creation, remote method invocation, asynchronous communication, rendezvous, and dynamic process creation. JR's concurrency model stems from the addition of operations (a generalization of procedures) and JR supports the redefinition of operations through inheritance. JR programs are written in an extended Java and then translated into standard Java programs. The JR run-time support system is also written in standard Java.This paper describes the JR programming language and its implementation. Some initial measurements of the performance of the implementation are also included.


title: A framework for the integration of partial evaluation and abstract interpretation of logic programs

abstract: Recently the relationship between abstract interpretation and program specialization has received a lot of scrutiny, and the need has been identified to extend program specialization techniques so as to make use of more refined abstract domains and operators. This article clarifies this relationship in the context of logic programming, by expressing program specialization in terms of abstract interpretation. Based on this, a novel specialization framework, along with generic correctness results for computed answers and finite failure under SLD-resolution, is developed.This framework can be used to extend existing logic program specialization methods, such as partial deduction and conjunctive partial deduction, to make use of more refined abstract domains. It is also shown how this opens up the way for new optimizations. Finally, as shown in the paper, the framework also enables one to prove correctness of new or existing specialization techniques in a simpler manner.The framework has already been applied in the literature to develop and prove correct specialization algorithms using regular types, which in turn have been applied to the verification of infinite state process algebras.


title: Automatic tiling of iterative stencil loops

authors:
Zhiyuan Li
Yonghong Song

abstract: Iterative stencil loops are used in scientific programs to implement relaxation methods for numerical simulation and signal processing. Such loops iteratively modify the same array elements over different time steps, which presents opportunities for the compiler to improve the temporal data locality through loop tiling. This article presents a compiler framework for automatic tiling of iterative stencil loops, with the objective of improving the cache performance. The article first presents a technique which allows loop tiling to satisfy data dependences in spite of the difficulty created by imperfectly nested inner loops. It does so by skewing the inner loops over the time steps and by applying a uniform skew factor to all loops at the same nesting level. Based on a memory cost analysis, the article shows that the skew factor must be minimized at every loop level in order to minimize cache misses. A graph-theoretical algorithm, which takes polynomial time, is presented to determine the minimum skew factor. Furthermore, the memory-cost analysis derives the tile size which minimizes capacity misses. Given the tile size, an efficient and general array-padding scheme is applied to remove conflict misses. Experiments were conducted on 16 test programs and preliminary results showed an average speedup of 1.58 and a maximum speedup of 5.06 across those test programs.


title: Traversals of object structures: Specification and Efficient Implementation

authors:
Karl J. Lieberherr
Boaz Patt-Shamir
Doug Orleans

abstract: Separation of concerns and loose coupling of concerns are important issues in software enginnering. In this paper we show how to separate traversal-related concerns from other concerns, how to loosely couple traversal-related concerns to the structural concern, and how to efficiently implement traversal-related concerns. The stress is on the detailed description of our algorithms and the traversal specifications they operate on.Traversal of object structures is a ubiquitous routine in most types of information processing. Ad hoc implementations of traversals lead to scattered and tangled code and in this paper we present a new approach, called traversal strategies, to succinctly modularize traversals. In our approach traversals are defined using a high-level directed graph description, which is compiled into a dynamic road map to assist run-time traversals. The complexity of the compilation algorithm is polynomial in the size of the traversal strategy graph and the class graph of the given application. Prototypes of the system have been developed and are being successfully used to implement traversals for Java and AspectJ [Kiczales et al. 2001] and for generating adapters for software components. Our previous approach, called traversal specifications [Lieberherr 1992; Palsberg et al. 1995], was less general and less succinct, and its compilation algorithm was of exponential complexity in some cases. In an additional result we show that this bad behavior is inherent to the static traversal code generated by previous implementations, where traversals are carried out by invoking methods without parameters.


title: Modular typechecking for hierarchically extensible datatypes and functions

authors:
Todd D. Millstein
Colin Bleckner
Craig Chambers

abstract: One promising approach for adding object-oriented (OO) facilities to functional languages like ML is to generalize the existing datatype and function constructs to be hierarchical and extensible, so that datatype variants simulate classes and function cases simulate methods. This approach allows existing datatypes to be easily extended with both new operations and new variants, resolving a longstanding conflict between the functional and OO styles. However, previous designs based on this approach have been forced to give upmodulartypechecking, requiring whole-program checks to ensure type safety. We describe Extensible ML (EML), an ML-like language that supports hierarchical, extensible datatypes and functions while preserving purely modular typechecking. To achieve this result,EML's type system imposes a few requirements on datatype and function extensibility, but EML is still able to express both traditional functional and OO idioms. We have formalized a core version of EML and proven the associated type system sound, and we have developed a prototype interpreter for the language.


title: First-class monadic schedules

authors:
Rajiv Mirani
Paul Hudak

abstract: Parallel functional languages often use meta-linguistic annotations to provide control over parallel evaluation. In this paper we explore a flexible mechanism to control when an expression is evaluated: first-class monadic schedules . We discuss the advantages of using such first-class values over traditional annotation-based systems. In particular, it is often desirable to make decisions about the operational behavior of parallel programs depending on the dynamic state of the system. For example, we may want to measure the system load before deciding to evaluate expressions in parallel. For this purpose, we show how monads can be used to access dynamic system parameters in a referentially transparent manner (up to termination).As a mechanism to reason about schedules, we present a set of algebraic properties that any implementation of schedules must satisfy. We also describe an implementation that translates schedules into a dialect of Scheme extended with futures . We prove that this implementation satisfies the given set of algebraic properties, and give performance results for a parallel solution to the n -body problem using the Barnes--Hut method.Although our ideas were developed specifically for nonstrict functional languages such as Haskell, we briefly discuss how they can be used with strict functional languages and imperative languages as well.


title: Guest editorial

authors:
Martin Odersky
Benjamin C. Pierce

abstract: No abstract available.


title: Optimistic register coalescing

authors:
Jinpyo Park
Soo-Mook Moon

abstract: Graph-coloring register allocators eliminate copies by coalescing the source and target nodes of a copy if they do not interfere in the interference graph. Coalescing, however, can be harmful to the colorability of the graph because it tends to yield a graph with nodes of higher degrees. Unlike aggressive coalescing , which coalesces any pair of noninterfering copy-related nodes, conservative coalescing or iterated coalescing perform safe coalescing that preserves the colorability. Unfortunately, these heuristics give up coalescing too early, losing many opportunities for coalescing that would turn out to be safe. Moreover, they ignore the fact that coalescing may even improve the colorability of the graph by reducing the degree of neighbor nodes that are interfering with both the source and target nodes being coalesced. This article proposes a new heuristic called optimistic coalescing which optimistically performs aggressive coalescing, thus exploiting the positive impact of coalescing aggressively, but when a coalesced node is to be spilled, it is split back into separate nodes. Since there is a better chance of coloring one of those splits, we can reduce the overall spill amount.


title: An unfold/fold transformation framework for definite logic programs

authors:
Abhik Roychoudhury
K. Narayan Kumar
C. R. Ramakrishnan
I. V. Ramakrishnan

abstract: Given a logic program P , an unfold/fold program transformation system derives a sequence of programs P = P 0 , P 1 , …, P n , such that P i +1 is derived from P i by application of either an unfolding or a folding step. Unfold/fold transformations have been widely used for improving program efficiency and for reasoning about programs. Unfolding corresponds to a resolution step and hence is semantics-preserving. Folding, which replaces an occurrence of the right hand side of a clause with its head, may on the other hand produce a semantically different program. Existing unfold/fold transformation systems for logic programs restrict the application of folding by placing (usually syntactic) conditions that are sufficient to guarantee the correctness of folding. These restrictions are often too strong, especially when the transformations are used for reasoning about programs. In this article we develop a transformation system (called SCOUT) for definite logic programs that is provably more powerful (in terms of transformation sequences allowed) than existing transformation systems. This extra power is needed for a novel use of logic program transformations: for the verification of a specific class of concurrent systems, called parameterized concurrent systems.Our transformation system is constructed by developing a framework, which is parameterized by a "measure space" and associated measure functions. This framework places no syntactic restriction on the application of folding, and it can be used to derive transformation systems (by fixing the measure space and functions). The power of the system is determined by the choice of the measure space and functions; thus the relative power of different transformation systems can be compared by considering their measure spaces and functions. The correctness of these transformation systems follows from the correctness of the framework. We show that various existing transformation systems can be obtained as instances of our framework. We extend the unfold/fold transformation framework with a goal replacement transformation that allows semantically equivalent conjunctions of atoms to be interchanged. We then derive a new transformation system SCOUT as an instance of the framework and show its power relative to the existing transformation systems. SCOUT has been used to inductively prove temporal properties of parameterized concurrent systems (infinite families of finite state concurrent systems). We demonstrate the use of the additional power of SCOUT in constructing such induction proofs.


title: Symmetry and reduced symmetry in model checking

authors:
A. Prasad Sistla
Patrice Godefroid

abstract: Symmetry reduction methods exploit symmetry in a system in order to efficiently verify its temporal properties. Two problems may prevent the use of symmetry reduction in practice: (1) the property to be checked may distinguish symmetric states and hence not be preserved by the symmetry, and (2) the system may exhibit little or no symmetry. In this article, we present a general framework that addresses both of these problems. We introduce "Guarded Annotated Quotient Structures" for compactly representing the state space of systems even when those are asymmetric. We then present algorithms for checking any temporal property on such representations, including non-symmetric properties.


title: Extensible objects without labels

abstract: Typed object calculi that permit adding new methods to existing objects must address the problem of name clashes: what happens if a new method is added to an object already having one with the same name but a different type? Most systems statically forbid such clashes by restricting the allowable subtypings. In contrast, by reconsidering the runtime meaning of object extension, the object calculus studied in the author's previous work with Jon Riecke allowed any object to be soundly extended with any method of any name, with unrestricted width subtyping. That language permitted a simple encoding of classes as object-generators. Because of width subtyping, subclasses could be typechecked and compiled with little knowledge of the class hierarchy and without any information about superclasses' private components; this made derived classes more robust to changes in the implementations of base classes. However, the system was not well suited for encoding mixins or by-name subtyping of objects.This article addresses those deficiencies by presenting the Calculus of Objects and Indices (COI), a lower-level typed object calculus in which extensible objects are more analogous to tuples than to records. An object is simply a finite sequence of unnamed components referenced by their index in the sequence. Names are then reintroduced by allowing these indices to be first-class values (analogous to pointers to members in C++) that can be bound to variables. Since variables---unlike record labels---freely alpha-vary, difficulties caused by statically undetectable name clashes disappear.By combining COI objects with standard type-theoretic mechanisms, one can encode mixins and classes having the by-name subtyping of languages like C++ or Java but with the robustness of the object-generator encodings. Using records, more standard extensible objects with named components can also be encoded.


title: A fast, memory-efficient register allocation framework for embedded systems

authors:
Sathyanarayanan Thammanur
Santosh Pande

abstract: In this work, we describe a "just-in-time," usage density-based register allocator geared toward embedded systems with a limited general-purpose register set wherein speed, code size, and memory requirements are of equal concern. The main attraction of the allocator is that it does not make use of the traditional live range and interval analysis nor does it perform advanced optimizations based on range splitting but results in very good code quality. We circumvent the need for traditional analysis by using a measure of usage density of a variable. The usage density of a variable at a program point represents both the frequency and the density of the uses. We contend that by using this measure we can capture both range and frequency information which is essentially used by the good allocators based on splitting. We describe a framework based on this measure which has a linear complexity in terms of the program size. We perform comparisons with the static allocators based on graph coloring and the ones targeted toward just-in-time compilation systems like linear scan of live ranges. Through comparisons with graph coloring (Brigg's style) and live range-based (linear scan) allocators, we show that the memory footprint and the size of our allocator are smaller by 20% to 30%. The speed of allocation is comparable and the speed of the generated code is better and its size smaller. These attributes make the allocator an attractive candidate for performing a fast, memory-efficient register allocation for embedded devices with a small number of registers.