Checking System Rules Using System-Specific,
Programmer-Written Compiler Extensions
Dawson Engler
Stanford University
Systems software such as OS kernels, embedded systems, and libraries
must obey many rules for both correctness and performance. Common
examples include ``accesses to variable A must be guarded by lock B,''
``system calls must check user pointers for validity before using
them,'' and ``disabled interrupts must be re-enabled.'' Unfortunately,
adherence to these rules is largely unchecked.
This talk shows system implementors can use ``meta-level compilation''
(MC) to write simple, system-specific compiler extensions that
automatically check their code for rule violations. By combining
domain-specific knowledge with the automatic machinery of compilers, MC
brings the benefits of language-level checking and optimizing to the
higher, ``meta'' level of the systems implemented in these languages.
This talk presents results of applying MC to four real systems: Linux,
OpenBSD, the Xok exokernel, and the FLASH machine's embedded software.
MC extensions found over 600 errors in these systems and led to
numerous kernel patches. Most extensions were less than a hundred
lines of code and written by implementors who had a limited
understanding of the systems checked.