November 22, 1996 Meeting

10:00am Tom Ball: Efficient Path Profiling

A path profile determines how many times each acyclic path in a routine executes. This type of profiling subsumes the more common basic block and edge profiling, which only approximate path frequencies. Path profiles have many potential uses in program performance tuning, profile-directed compilation, and software test coverage.

We describe a new algorithm for path profiling. This simple, fast algorithm selects and places profile instrumentation to minimize run-time overhead. Instrumented programs run with overhead comparable to the best previous profiling techniques. On the SPEC95 benchmarks, path profiling overhead averaged 31%, as compared to 16% for efficient edge profiling. Path profiling also identifies longer paths than a previous technique, which predicted paths from edge profiles (average of 88, versus 34 instructions). Moreover, profiling shows that the SPEC95 *train* input datasets covered most of the paths executed in the *ref* datasets.

This is joint work with James Larus of the University of Wisconsin--Madison. A paper on the work will appear in MICRO-29 and is available at ftp://ftp.cs.wisc.edu/wwt/micro96.ps.

11:30am Drew Dean: The Security of Static Typing with Dynamic Linking

Dynamic linking is a requirement for portable executable content. Executable content cannot know, ahead of time, where it is going to be executed, nor know the proper operating system interface. This imposes a requirement for dynamic linking. At the same time, we would like languages supporting executable content to be statically typable, for increased efficiency and security. Static typing and dynamic linking interact in a security-relevant way. This interaction is the subject of this talk. One solution is modeled in PVS, and formally proven to be safe.

1:45pm Anindya Banerjee: A Modular, Polyvariant, and Type-based Closure Analysis

Closure analysis is of crucial importance for compiler optimisations of higher-order functional languages and has several application areas: two notable ones are partial evaluation, and escape analysis for the stack-based memory management for higher-order languages. Palsberg and Schwartzbach showed a relationship between control-flow analysis and type systems, relating the safety property of the analysis to type safety. Palsberg and O'Keefe subsequently showed that Amadio and Cardelli's type system with recursive types and subtyping is equivalent to the afore-mentioned ``safety analysis''. The following question, formulated by Palsberg and O'Keefe, is open: ``How can we directly compute control-flow information from Amadio and Cardelli's type system without a reduction to safety analysis''?

We answer this question for another very expressive type system, namely, the rank 2 intersection type system. Trevor Jim, in POPL '96, has shown that this system can type more terms than ML while retaining the same complexity of type inference. This makes it an attractive tool for type-based program analysis. We show that for the rank 2 intersection type system with subtyping, and with types augmented by effects (i.e., control-flow information), there exists a sound and complete type inference algorithm that can compute control-flow information directly from the structure of the program text. Subtyping is used to orient flow information; the principal typing property of the type system lends modularity to the analysis, so that program fragments with free variables can be separately analysed; and the polymorphism inherent in the type system renders the analysis polyvariant, so that the same function can be specified to have different behaviours at its different uses.

3:00pm Andrew Wright: Type-Respecting Flow Analysis

In its simplest form, a flow analysis associates abstract values denoting sets of exact values with each subexpression of a program. While the information provided by types is less intensional in nature, types can also be viewed as denoting sets of values. Hence it is reasonable to expect the abstract values computed for a typed program to agree with its types. That is, if the flow analysis assigns abstract value a to an expression and the type system assigns type t to the same expression, we expect [a] subset [t], where [.] denotes a set of values. We say that such a flow analysis respects types. Respecting types avoids discarding type information provided by the programmer, provides a way to characterize the precision of analyses, and may lead to more powerful analyses.

We describe a polyvariant flow analysis framework for Fpred, the predicative fragment of system F. Our framework characterizes a broad class of analyses, and we prove that any analysis in this class is correct. We then exhibit an uncomputable analysis that respects types. Crucially, this analysis uses types to control polyvariance. We show, however, that our analysis is computable for a subset of Fpred sufficient to express the core of ML. Finally, we provide a formal characterization of the precision of an analysis, and show that the product of a type-respecting analysis with any sound analysis still respects types.

To our knowledge, this is the first presentation of a polyvariant flow analysis framework for a polymorphic language that uses type information to characterize and control precision.

This is joint work with Suresh Jagannathan and Steve Weeks.

3:30pm Jim Philbin: Thread Scheduling for Cache Locality

We describe a method that improves the cache locality of sequential programs by scheduling fine-grained threads. The algorithm relies upon hints provided at the time of thread creation to determine a thread execution order likely to reduce cache misses. This technique may be particularly valuable when compiler-directed tiling is not feasible. Experiments with several application programs, on two systems with different cache structures, show that our thread scheduling method can improve program performance by reducing second-level cache misses.

This is joint work with Jan Edler, Otto Anshus, Craig Douglas, and Kai Li.