Computer Science Department
School of Computer Science, Carnegie Mellon University


Landslide: Systematic Dynamic
Race Detection in Kernel Space

Ben Blum

May 2012

M.S. Thesis


Keywords: Concurrency, kernel debugging, race conditions, runtime verification

Systematic exploration is an approach to finding race conditions by deterministically executing every possible interleaving of thread transitions and identifying which ones expose bugs. Current systematic exploration techniques are suitable for testing user-space programs, but are inadequate for testing kernels, where the testing framework's control over concurrency is more complicated.

We present Landslide, a systematic exploration tool for finding races in kernels. Landslide targets Pebbles, the kernel specification that students implement in the undergraduate Operating Systems course at Carnegie Mellon University (15-410). We discuss the techniques Landslide uses to address the general challenges of kernel-level concurrency, and we evaluate its effectiveness and usability as a debugging aid. We show that our techniques make systematic testing in kernel-space feasible and that Landslide is a useful tool for doing so in the context of 15-410.

88 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by