Computer Science PhD Thesis Defense
Lea Wittie

Tuesday, June 29, 2004
Fairchild 101
2 p.m.

Type-Safe Operating System Abstractions

Operating systems and low-level applications are usually written in
languages like C, which provide access to low-level abstractions but are not
type-safe. This research focuses on safe language techniques for
building type-safe OS components, which cannot cause memory or IO
errors. I formalize the concurrency, locks, and system state needed by
the safety-critical areas of an Ethernet adapter driver. These formal
concepts are built into an abstract syntax and rules that guarantee
basic memory safety. The abstract machine is provably sound, which
means that well-typed programs will not violate the machine's
abstractions. 

I developed a small operating system and ported an Ethernet adapter
driver from C to Clay, a C-like type-safe language that uses a type
system powerful enough to enforce invariants about devices and
low-level data structures. The resulting driver works safely in a
multi-threaded environment. The driver is guaranteed to obtain locks
before using shared data. It cannot cause memory errors and it will
only call IO operations when invariants are satisfied. 

Committee members:
Dr. Chris Hawblitzel (Dept. of Computer Science, Dartmouth College),
Dr. Sean Smith (Dept. of Computer Science, Dartmouth College,
Dr. Doug McIlroy (Dept. of Computer Science, Dartmouth College),
Dr. Stefan Monnier (Dept. of Computer Science and Operations Research,
                    University of Montreal, Canada)