ESP: A Language for Programmable Devices (Thesis)

Abstract:

This thesis presents the design and implementation of Event-driven
State-machines Programming (ESP)---a language for programmable
devices. In traditional languages, like C, using event-driven
state machines forces a tradeoff that requires giving up ease of
programming and reliability to achieve high performance. ESP is
designed to provide all of these three properties simultaneously.

ESP provides a comprehensive set of features to support development of
compact and modular programs. The ESP compiler compiles the programs
into two targets---a C file that can be used to generate efficient
firmware for the device; and a model that can be used by a
model-checking verifier like Spin to extensively test the firmware.

As a case study, we reimplemented VMMC firmware that runs on Myrinet
network interface cards using ESP. We found that ESP simplifies the
task of programming with event-driven state machines. It required an
order of magnitude fewer lines of code than the earlier
implementation. We also found that model-checking verifiers like Spin
can be used to effectively debug the firmware. Our measurements show
that the performance impact on applications of using ESP is small.