Checking system rules using system-specific, programmer-written compiler extensions

TLDR

Systems software must obey many rules for correctness and performance, yet adherence is largely unchecked, prompting the need for automatic checking. The paper aims to show that meta‑level compilation can automatically detect rule violations in systems software by applying it to Linux, OpenBSD, Xok, and FLASH. MC achieves this by integrating domain knowledge into compiler extensions that automatically check code for rule violations across multiple systems. The extensions uncovered about 500 errors, prompted many kernel patches, and were typically under 100 lines of code written by implementors with limited system knowledge.

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, 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.