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
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.
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.
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.
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+.