PDL Abstract

Landslide: Systematic Dynamic Race Detection in Kernel Space

Carnegie Mellon University School of Computer Science MS Thesis CMU-CS-12-118, May 2012.

Ben Blum

School of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213

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.

KEYWORDS: concurrency, kernel debugging, race conditions, runtime verification