Programming language tools
offer powerful mechanisms for improving the safety and reliability of
systems code. This talk presents Deputy, a type system and compiler for
enforcing type and memory safety in real-world C programs such as Linux
device drivers and the Linux kernel itself. Deputy's type system uses
dependent types, a language mechanism that allows programmers to
describe common C idioms in an intuitive fashion.
The Deputy project offers
contributions to both systems and programming languages. From a systems
perspective, Deputy is attractive because it can provide fine-grained
safety guarantees in a modular and incremental fashion; for example,
Deputy can be used to enforce type and memory safety in Linux device
drivers without requiring changes to the kernel. The SafeDrive recovery
system for Linux device drivers uses Deputy for isolation and failure
detection, and as a result, it is both simpler and faster than previous
systems for isolating software extensions. From a language perspective,
Deputy shows how to reason about dependent types in imperative code.
Deputy has fewer restrictions on mutation than previous systems, and it
uses run-time checks and several inference techniques to ensure
decidability and usability.
Biography: Jeremy Condit is
a graduate student who is currently completing his Ph.D. at the
University of California, Berkeley. His research interests focus on
using programming language tools and techniques to address the
challenges of building large software systems. He received his A.B.
summa cum laude from Harvard University, and he received his M.S. from
the University of California, Berkeley. He is a recipient of the NSF
Graduate Research Fellowship, and he received the Best Paper Award at
ETAPS 2005 from the European Association for Programming Languages and
Systems.