  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.
