Laddie: Language for Automated Device Drivers

Lea Wittie (Bucknell University), 
Chris Hawblitzel (Microsoft Research),
Derrin Pierret (Bucknell University)

Device drivers are known to be a main source of OS bugs.
Several research groups have created driver specification languages
that dynamically check pre- and postconditions on the IO operations 
of a device driver. Low level type safe languages exist that can 
statically check function pre- and postconditions. However, these 
low level languages are too general to make the specific task of 
driver writing simple. This research presents Clay, a low level type 
safe language that has the facilities to statically check the safety
of a device driver, and Laddie, a device driver specification language
which compiles to Clay thus leveraging its static safety checking
while remaining simple to use.

Clay, developed at Dartmouth, is a C-like language which dependent 
types, like those of DML, to track program values statically. It
builds on the linear logic of Girard to produce linear capabilities 
which guard access to memory and to logical system state and prevent 
aliasing errors. Clay also incorporates the arithmetic constraints of 
Xi and Pfenning into function pre- and postconditions to produce Hoare 
Triples, {P} f {Q} where P and Q are pre- and postconditions on function f.
Clay statically enforces linear access to memory and statically checks all
pre- and post conditions on function calls. When successfully type
checked, a Clay program then compiles to C++.

There are several existing specification languages for device drivers
including Devil, NDL, and Hail. All of these perform dynamic safety 
checks. To move the safety checks to compile time, we created Laddie, 
a language for specifying the IO communication between a driver and
its device. Devices are typically accessed via a set of locations
called registers. Each register has rules governing how and when it
can be accessed. These rules may depend on the logical state of the
device, which is not usually stored in driver memory. (This state
might include the status of device interrupts). Laddie uses syntax
similar to that of Hail to allow a simple encoding of the complex
rules and logical device state into pre- and postconditions on access
to registers. Laddie compiles to Clay which checks the pre- and
postconditions statically.