WITCHER : Detecting Crash Consistency Bugs in Non-volatile Memory Programs

TL;DR

WITCHER is a scalable, automatic, and precise tool for detecting crash consistency bugs in non-volatile memory software by analyzing invariants and comparing program outputs under simulated crashes.

Contribution

WITCHER introduces a novel invariant-based approach that automatically detects crash bugs without false positives or manual annotations.

Findings

Discovered 37 crash bugs, including 32 new ones.

Outperformed existing tools in detection accuracy.

Validated all identified bugs.

Abstract

The advent of non-volatile main memory (NVM) enables the development of crash-consistent software without paying storage stack overhead. However, building a correct crash-consistent program remains very challenging in the presence of a volatile cache. This paper presents WITCHER, a crash consistency bug detector for NVM software, that is (1) scalable -- does not suffer from test space explosion, (2) automatic -- does not require manual source code annotations, and (3) precise -- does not produce false positives. WITCHER first infers a set of "likely invariants" that are believed to be true to be crash consistent by analyzing source codes and NVM access traces. WITCHER automatically composes NVM images that simulate those potentially inconsistent (crashing) states violating the likely invariants. Then WITCHER performs "output equivalence checking" by comparing the output of program executions with and without a simulated crash. It validates if a likely invariant violation under test is a true crash consistency bug. Evaluation with ten persistent data structures, two real-world servers, and five example codes in Intel's PMDK library shows that WITCHER outperforms state-of-the-art tools. WITCHER discovers 37 (32 new) crash consistency bugs, which were all confirmed.