Beastie In For Checkup: Analyzing FreeBSD with LockDoc

Abstract

LockDoc is an approach to extract locking rules for kernel data structures, based on a dynamic execution trace. The recorded trace can e.g. be used to verify existing locking documentation. LockDoc results for Linux indicated that only 53 % of all examined data types were accessed consistently with their respective locking documentation [5]: Linux systematically elides locks for performance reasons, and the existing documentation is partially outdated or inconsistent. Without a solid “ground truth”, it is impossible to reliably attribute LockDoc’s findings to bugs in Linux, or to issues with the LockDoc approach itself. Therefore, in this paper we present results from applying LockDoc to a much more straightforwardly and “cleanly” implemented operating system: FreeBSD offers sophisticated locking documentation – e.g. for many data structures, each individual field is annotated with a precise locking rule. We report that, for four centrally documented data types, FreeBSD adheres to the documented locking rules in 72.4 % of all dynamic data-structure accesses. Investigating the remaining rule-violating accesses, we already triggered two commits for the FreeBSD kernel fixing unprotected accesses, and nudge this value to 73.6 %.