23 August 2000 Meeting

10:00am: Semantics-based Design and Correctness of Control-flow Analysis-based Program Transformations

Anindya Banerjee (Stevens Institute of Technology)

We show how control-flow-based program transformations in functional languages can be proven correct. The method relies upon "defunctionalization," a mapping from a higher-order language to a first-order language. We give methods for proving defunctionalization correct. Using this proof and common semantic techniques, we then show how two program transformations---flow-based inlining and lightweight defunctionalization---can be proven correct.

Joint with Nevin Heintze and Jon G. Riecke, Bell Laboratories

10:45am: Static Enforcement of Security with Types

Christian Skalka and Scott Smith (Johns Hopkins University)

A number of security systems for programming languages have recently appeared, including systems for enforcing some form of access control. The Java JDK 1.2 security architecture is one such system that is widely studied and used. While the architecture has many appealing features, access control checks are all implemented via dynamic method calls. This is a highly non-declarative form of specification which is hard to read, and which leads to additional run-time overhead. In this paper, we present a novel security type system that enforces the same security guarantees as Java Stack Inspection, but via a static type system with no additional run-time checks. The system allows security properties of programs to be clearly expressed within the types themselves. We also define and prove correct an inference algorithm for security types, meaning that the system has the potential to be layered on top of the existing Java architecture, without requiring new syntax.

11:30am: Lunch

12:45pm: Business meeting

1:00pm: Hot-Spot Compilation of Scheme48

Dino Oliva (NECI)

1:45pm: SSA in linear (input+output) time

Allen Leung (New York University)

We present an algorithm for constructing the minimal static single assignment form (SSA) of arbitrary flowgraphs in time linear in sizes of the input program and the SSA form output, under the assumption that there is at least one assignment in each basic block. As far as we know, this is the first optimal algorithm for SSA construction. The crucical data structure that we use is the compressed DJ-graph, a variant of the DJ-graph with ``short-cuts'', which allows online queries of IDF(N_\alpha) the iterated dominance frontier of a set N_\alpha, to complete in O(|N_\alpha| + \sum_{x \in IDF(N_\alpha)} indeg(x)) time. Compressed DJ-graph is not restricted to SSA computation and can be also used to speed up various compiler optimization problems which involve the computation of (iterated) dominance frontier, such as sparse evaluation graph construction.

2:30pm: Break

3:00pm: The CIL ML compiler: Flow Directed Specialized Representations

Allyn Dimock (Harvard University)

The CIL ML compiler uses intersection and union types, with flow information incorporated into the types, to facilitate using specialized data representations. We will present the latest empirical results from experimenting with using Steckler's "selective closure conversion" representation on a number of standard ML benchmarks.

4:00pm: Meeting ends