When we cast each of these analyses as type-based program analyses, the elimination rule says that the property of the constructor being destructed "infects" the result of the computation. In this sense, the result at a particular program point depends on the properties of all the constructors that have been destructed.
We show how to formalise such dependency analyses in the computational lambda calculus.
This is work in progress with Martin Abadi, Nevin Heintze and Jon Riecke.
We study the problem of analyzing implementations of open systems --- systems in which only some of the components are present. We present an algorithm for automatically closing an open concurrent reactive system with its most general environment, i.e., the environment that can provide any input at any time to the system. The result is a nondeterministic closed (i.e., self-executable) system which can exhibit all the possible reactive behaviors of the original open system. These behaviors can then be analyzed using VeriSoft, an existing tool for systematically exploring the state spaces of closed systems composed of multiple (possibly nondeterministic) processes executing arbitrary code. We have implemented the techniques introduced in this paper in a prototype tool for automatically closing open programs written in the C programming language. We discuss preliminary experimental results obtained with a large telephone-switching software application developed at Lucent Technologies.
This is joint work with Christopher Colby and Lalita Jagadeesan.
PATH (Programmer Assistant for Transforming Haskell) is a program transformation system for the language Haskell. Rather than attempting to provide full automation, PATH is interactive and programmer directed.
In this talk, I will describe the program transformation rules of PATH and the advantages of this system over the Unfold/Fold system. I will also give examples of program derivations which can be done in PATH but are problematic for other systems.
This is joint work with Paul Hudak.
The need for an operating system to adapt to a changing environment is becoming increasingly important in areas such as mobile computing, interactive multimedia, and large distributed databases. Program specialization, i.e. optimizing a program with respect to its context of use, plays a key role in obtaining such an adaptive system. Toward this end, we have developed Tempo, a partial evaluator designed to specialize systems code. This talk gives an overview of Tempo and an in depth presentation of its static analyses, which contain a number of key features that enable Tempo to automatically and effectively exploit specialization opportunities. Experimental results show significant speedups are obtained by specializing system components, such as Sun RPC.
Destructive array update optimization is critical for writing scientific codes in functional languages. We present set constraints for an interprocedural update optimization that runs in polynomial time. This is a highly non-trivial optimization, involving interprocedural flow analyses for aliasing and liveness. We characterize the soundness of these analyses using small-step operational semantics. We have shown that all solutions to our set constraints are sound. We have also proved that any sound liveness analysis induces a correct program transformation.
This is joint work with Will Clinger.
A module system ought to enable ``assembly-line programming'' using separate compilation and an expressive linking language. Separate compilation allows programmers to develop parts of a program independently. A linking language gives programmers precise control over the assembly of parts into a whole. This paper presents models of program units, MzScheme's module language for assembly-line programming. Units support separate compilation, independent module reuse, cyclic dependencies, hierarchical structuring, and dynamic linking. The models explain how to integrate units with untyped and typed languages such as Scheme and ML.
Dino Oliva / Bell Laboratories / oliva@research.bell-labs.com