27 February 2001 Meeting

10:00am: ESP: A language for Programming Devices

Sanjeev Kumar (Princeton University)

I will describe the design and implementation of Event-driven State-machine Programming (ESP)---a language for programming network devices. In traditional languages, like C, using event-driven state-machine forces a tradeoff by giving up ease of development and reliability to achieve high performance. ESP is designed to provide all three.

ESP provides a compact yet comprehensive set of features to support development of efficient and reliable concurrent programs which execute on a single processor. The ESP compiler compiles the concurrent programs into two targets---a C file that can be used to generate efficient firmware for the network devices; and a specification that can be used by a verifier like SPIN to extensively test the system.

As a case study, we implemented the core functionality of the VMMC firmware that runs on Myrinet network interface cards. We found that ESP simplifies the task of programming with event-driven state machines. It required an order of magnitude less lines of code than the previous implementation. We also found that model-checking verifiers like SPIN can be used to extensively test the system. The effort involved can be greatly reduced when the specification for the verifier is automatically generated by the compiler. Finally, our measurements indicate that the performance overhead of using ESP is relatively small.

This is joint work with Yitzhak Mandelbaum, Xiang Yu, and Kai Li

10:45am: Break

11:15am: Heap bounded assembly language

Adriana Compagnoni (Stevens Institute of Technology)

We present a typed assembly language, HBAL (Heap Bounded Assembly Language), which has a type system with features for managing space usage. In contrast to other typed assembly languages, our assembly language allows memory areas to be reused for values of differing types. We ensure type safety by using a type system with linearity constraints to prevent aliasing of heap locations, together with special pseudo-instructions for altering types at isolated points in the code. The reuse discipline is controlled by compilation from a high-level language, and we demonstrate a compilation from a prototypical first-order functional language, HBFL (Heap Bounded Functional Language), due to Hofmann. HBFL has a special resource type called diamond, which represents a unit of reusable space that can be manipulated by the programmer.

Joint work with David Aspinall from Edinburgh.

12:00pm: Lunch

1:00pm: Business meeting

1:15pm: Tag Elimination and Jones-optimality

Walid Taha (Yale University)

Tag elimination is a program transformation for removing unnecessary tagging and untagging operations from automatically generated programs. Tag elimination was recently proposed as having immediate applications in implementations of domain specific languages (where it can give a two-fold speedup), and may provide a solution to the long standing problem of Jones-optimal specialization in the typed setting. This paper explains in more detail the role of tag elimination in the implementation of domain-specific languages, presents a number of significant simplifications and a high-level, higher-order, typed self-applicable interpreter. We show how tag elimination achieves Jones-optimality.

2:00pm: Dynamic Software Updating

Michael Hicks (University of Pennsylvania)

Many important applications must run continuously and without interruption, yet must be changed to fix bugs or upgrade functionality. To date, no existing dynamic updating system has achieved a practical balance between flexibility, correctness, ease-of-use, and low overhead. We present a new approach that provides type-safe dynamic updating of native code in an extremely flexible manner (functions and types may be updated, and at any time) and permits the use of automated tools to aid the programmer in the updating process. Our system is based around dynamic patches made up of proof-carrying code that both contain the updated code and the code needed to transition from the old version to the new. We discuss how patches are generated using a semiautomatic tool, how they are applied using dynamic-linking technology, and how code is compiled to make it updateable. To concretely illustrate our system, we have implemented a dynamically-updateable web server, FlashEd. We discuss our experience building and maintaining FlashEd. Performance experiments show that updateable FlashEd runs between 2 and 6 slower than a static one.

2:45pm: Break

3:15pm: The Regular World Assumption

Carsten Schuermann (Yale University)

In the first-order simply typed setting there is a close connection between datatypes, definitions of functions by cases and recursion on the one hand, and strong induction principles on the other. This connection however breaks down if we consider functions that range over higher-order, possibly dependently typed objects.

In my talk I will present a solution to this problem by generalizing the closed world assumption that typically underlies induction principles to the regular world assumption. I will motivate the idea of regular worlds by examples, and describe a suitable type theory which is called M2+.

4:00pm: Meeting ends