|
OSDI 2000 Abstract
Checking System Rules Using System-Specific,
Programmer-Written Compiler Extensions
Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem, Stanford University
Abstract
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 "message handlers
should free their buffers as quickly as possible to allow greater parallelism." Unfortunately, adherence
to these rules is largely unchecked.
This paper attacks this problem by showing how
system implementors can use meta-level compilation
(MC) to write simple, system-specific compiler extensions that automatically check their code for rule violations. By melding 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 paper demonstrates the effectiveness of the MC approach by applying it to four
complex, real systems: Linux, OpenBSD, the Xok
exokernel, and the FLASH machine's embedded software. MC extensions found roughly 500 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.
|
Need help? Use our Contacts page.
