*captionUnsupported document class

#  Witcher: Detecting Crash Consistency Bugs in Non-volatile Memory Programs

Xinwei Fu Wook-Hee Kim Ajay Paddayuru Shreepathi$\dagger$
Mohannad Ismail Sunny Wadkar Changwoo Min Dongyoon Lee$\dagger$
Virginia Tech $\dagger$Stony Brook University

###### 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.

##  1 Introduction

Non-volatile main memory (NVM) technologies, such as the recently
commercialized Intel Optane DC Persistent Memory [11, 50], provide persistence
of storage along with traditional DRAM characteristics such as byte
addressability and low access latency. NVMs are attached to processors via a
memory bus so that programs can access the NVMs using regular load and store
instructions. The ability to directly access NVMs provides a new opportunity
to build _crash-consistent_ software without paying storage stack overhead.
Programs can recover a consistent state from a potentially-inconsistent
persistent NVM state in the event of an application or a system crash, or a
sudden power loss (hereafter crash for brevity).

However, designing and implementing a correct crash-consistent program is
challenging. NVM data on a processor’s volatile cache may not be persisted
after a crash. This implies that the completion of a store instruction does
not guarantee the persistence of memory. Furthermore, a processor cache can
evict cache lines in an arbitrary order so that the NVM memory locations may
not be persisted in the same order as the program (store) order. Lastly, the
current ISA does not provide an atomic instruction to update multiple NVM
locations.

Therefore, ensuring crash consistency requires a developer to explicitly add a
cache line flush and store fence instructions (e.g., clwb and sfence in x86
architecture) and to devise a custom mechanism to ensure ordering and
atomicity guarantee, making NVM programming hard and error-prone.

Recently, several solutions for detecting crash consistency bugs have been
proposed, but they are not satisfactory. One line of tools [42, 32, 55]
attempts to test all possible inconsistent states exhaustively, leading to a
scalability issue. For instance, Yat [42] reports that a program execution
with 14K cache line flushes leads to 789 million combinations to test, which
will take roughly 5.2 years. Another family [46, 45] asks developers to
annotate correctness conditions manually. Annotating a large NVM program is
challenging, potentially resulting in both false negatives (missing
annotation) and false positives (incorrect annotation) depending on the
quality of annotations.

This paper presents Witcher, a new crash consistency bug detector for NVM
software. Witcher is (1) scalable – it does not suffer from test space
explosion, (2) automatic – it does not require manual source code annotations,
and (3) precise – it does not produce false positives. We build Witcher based
on the following two key insights.

First, Witcher automatically infers a set of _likely program invariants_ that
are believed to be true to be crash-consistent by analyzing source codes and
execution traces, with a hypothesis that programmers leave some hints on what
they want to ensure. Witcher then tests only for those likely invariants,
instead of relying on exhaustive testing or user’s manual annotation. For
example, for NVM addresses X and Y, from the source code where the write of Y
is control-dependent on the read of X (e.g., if(X){Y=3}), Witcher infers a
likely invariant that “X should be persisted before Y”, assuming that
developers would not want to update persistent data Y based on unpersisted
data X. Then it checks the persistence ordering between X and Y, but not
between X and another irrelevant Z, saving the testing time.

Second, we also automatically validate those likely invariants (i.e., to check
if a violation of those invariants is a true crash consistency bug) by
performing _output equivalence checking_. If a program is crash-consistent, it
should produce the same output (e.g., query(k)) between two executions with
and without a crash. Based on this observation, Witcher composes a set of
crash NVM images, each of which simulates a potentially inconsistent
(crashing) state violating a likely invariant. Then it runs a randomly
generated test case (e.g., a sequence of mixed insert, delete, and query), and
compares the output of program executions with and without a simulated crash.
Any mismatch (e.g., one leads to a fault, or produces a different output) is a
definite clue of a bug.

Witcher considers two forms of likely invariants ensuring (1) persistence
ordering (e.g., X should be persisted before Y) and (2) persistence atomicity
(e.g., X and Y should be persisted atomically). Then it tests if persistence
primitives (e.g., cache line flush and store fence instructions) are used
properly to ensure them. This approach allows Witcher to detect crash
consistency bugs in both _low-level_ NVM programs, which use the assembly-
level persistence primitives, and _transactional_ NVM programs, which rely on
a logging logic in a transaction library (e.g., Intel’s Persistent Memory
Development Kit (PMDK) [30]), in a unified manner. Under the hood, such
transactional libraries use the same flush and fence primitives for
persistence. Witcher traces and analyzes PMDK internals such as persistence
heap allocation and transactional undo logging logics, validating both the
PMDK library itself and transactional NVM programs using them. Also, Witcher
supports both single-threaded and multi-threaded testing.

We evaluated Witcher with 17 NVM programs consisted of 92K lines of code
(LOC), which include ten highly-optimized persistent data structures (appeared
in top-tier systems conferences), two server applications Redis [5] and
Memcached [4] that are ported with PMDK, and five example code included in
PMDK. Using randomly generated test cases, Witcher detected 37 (32 new) crash
consistency bugs in 13 programs, all of which are confirmed by the developers.
One new bug was found in the PMDK’s persistent pool/heap management library.

We make the following contributions in this paper:

  * •

We propose a _likely invariant-based approach_ to infer likely correct
conditions to detect crash consistency bugs without manual annotations or
exhaustive testing.

  * •

We present an _output equivalence-based technique_ to identify an incorrect
execution without user-provided consistency checkers or annotations.

  * •

We implement Witcher that detects crash consistency bugs in a scalable,
automatic, and precise manner using likely invariant inference and output
equivalence checking.

  * •

Our evaluation shows that Witcher detects 37 (32 new) confirmed bugs and
outperforms existing solutions: it discovered more bugs in a scalable and
automatic manner. All the bugs reported were true positives.

##  2 Motivation

This section first demonstrates the types of crash consistency bugs along with
real-world examples that Witcher found in an NVM-optimized resizable hash
table, Level Hashing [72]. Then, we discuss the limitations of existing
testing techniques.

###  2.1 Crash Consistency Bugs

Figure 1:  Using the likely invariants inferred from (a), Witcher detects two
crash consistency bugs (b) and (c) in Level Hashing.

(1) Persistence ordering violations.(1) Persistence ordering violations(1)
Persistence ordering violations. A buggy NVM program may not maintain proper
_persistence ordering_ when updating multiple NVM locations. A processor cache
can evict cache lines in an arbitrary order, and a processor can re-order a
cache line flush instruction. As a result, the program order among multiple
stores may mismatch with the persistence order. If a developer wants to ensure
that one store becomes persisted before another, she has to explicitly add a
cache line flush followed by a store fence instruction (e.g., clwb and sfence
in x86 architecture) between them. We consider a missing persistence primitive
bug (used in XFDetector [45] and RECIPE [44]) as a kind of persistence
ordering bugs because it voids an ordering guarantee.

We found ten persistence ordering bugs (§ 6) in Level Hashing [72]. For
performance, Level Hashing introduces _log-free_ write operations. It
maintains a flag token for each key-value slot where token 0 denotes the
corresponding key-value slot is empty and token 1 denotes non-empty. Figure
1(b) shows the levelinsert function. It intends to update the key-value slot
(Lines 14, 15) before updating token (Line 18). However, if a crash happens
after the token’s cache line is evicted (thus persisted) but before the key-
value slot’s cache line is not (before Line 20), an inconsistent state could
occur – the token indicates that the corresponding key-value slot is non-
empty, but the slot is never written to NVM. Thus, the garbage value can be
read (as in Figure 3(h)), implying that the insert operation failed to provide
an atomic (all or nothing) semantic upon a crash. The persistent barrier at
Lines 20-23 should be moved before updating the token at Line 18.

(2) Persistence atomicity violations.(2) Persistence atomicity violations(2)
Persistence atomicity violations. A buggy NVM program may not correctly
enforce _persistence atomicity_ among multiple NVM updates. If a program
crashes in the middle of a sequence of NVM updates, an inconsistent state may
occur. We found 16 atomicity bugs in seven NVM programs (§ 6).

Figure 1(c) shows a persistence atomicity bug found in Level Hashing’s
levelupdate function. Level Hashing opportunistically performs a log-free
update. If there is an empty slot in the bucket storing the old key-value
slot, a new slot is stored to the empty slot (Lines 34, 35), and then the old
and new tokens are modified (Lines 38, 39). Since the new slot is not
overwritten to the old slot, Level Hashing can avoid the costly logging
operations. However, the code incorrectly assumes that updating two tokens is
atomic. If a crash happens right after turning off the old token (Line 38) and
the cache line of the old token is evicted (persisted), the crash consistency
problem happens. Since the old token is persisted with 0 but the new token
(Line 39) is not turned on, we permanently lose the updating key. To solve
this bug, we have to persist two tokens atomically. In this example, we can
place two tokens in an 8-byte word using bit representation and update them
with a single 8-byte store to update two tokens atomically.

###  2.2 Limitations of Existing Solutions

(1) Huge testing space.(1) Huge testing space(1) Huge testing space.
_Exhaustive testing approach_ [42, 32, 55] attempts to permute all possible
persistent states on a crash. Then, for each crashed state, they rely on a
user-provided consistency checker to validate whether NVM data is consistent.
However, they often do not scale. For instance, the testing space of Yat [42]
explodes exponentially in the number of store instructions. For example,
testing Level Hashing with 2000 (random) operations, the Yat tests $10^{77}$
total permutations (see the detailed discussion in § 6.5).

(2) Manual annotation burden.(2) Manual annotation burden(2) Manual annotation
burden. The test space explosion problem motivated the recent _annotation-
based approach_ , such as PMTest [46] and XFDetector [45]. Although these
approaches are fast without exhaustive testing, it puts a significant
annotation burden on the developers, raising soundness, completeness, and
scalability concerns. A missing annotation may miss crash consistency bugs
(false negatives). The wrong annotation may produce false bugs (false
positives). Annotating a large NVM software soundly and precisely is very
challenging. Lastly, we note that PMTest lacks support for detecting
persistence atomicity violations such as Figure 1(c), and XFDetector cannot
support low-level NVM programs that do not rely on logging such as Level
Hashing.

Figure 2:  The architecture of Witcher.

(3) Correctness validation after a crash.(3) Correctness validation after a
crash(3) Correctness validation after a crash. Validating the correctness
(crash consistency) after a crash is another challenge. The first approach
relies on a user-provided consistency checker (e.g., Yat [42], PMReorder
[32]). However, the correctness of a manually-written checker is often a
concern; a recent study [37] reports that even checkers (fsck) of the
production-grade file systems (ext4, F2FS, and btrfs) cannot recover 16% of
failures. The second approach relies on user-annotated invariant checkers
(e.g., PMTest [46]). As discussed earlier, the soundness, completeness, and
scalability of user annotations is a concern. The last relies on the user’s
manual investigation without providing automatic validation (e.g., XFDetector
[45]). That would waste a lot of developer’s time with a high false-positive
rate.

##  3 Our Approach

###  3.1 Inference of Likely Invariants

We propose a novel _likely invariant-based_ approach to detect NVM crash
consistency bugs scalably and automatically. Our key observation is that
programmers often left some hints on what they want to ensure in the source
codes. Thus we can infer a set of likely-correctness conditions, which we
refer to as _likely invariants_ (hereafter invariants for short), by analyzing
source codes and execution traces.

Using the Level Hashing example as mentioned earlier, let us demonstrate how
we can infer an invariant from the query (or lookup) function
level_static_query in Figure 1(a), and apply it to find the crash consistency
bugs in level_insert and level_update in Figure 1(b) and (c).
level_static_query reads the key/value only if the token is non-empty. In
other words, there is a control dependency between the read of a token and a
key-value pair (Lines 3-7): e.g., we denote it as
R(slot[j].key)$\xrightarrow[]{\text{cd}}$R(token[j]). We analyze the
implication of this control dependency as follows.

We first refer to the common NVM programming pattern that uses a flag (token)
to ensure the persistence atomicity of data (key/value) as _guarded
protection_. We have observed this guarded protection pattern in many NVM
programs including key-value stores [1, 66, 49], logging implementations [65,
26, 12, 36, 27], persistent data structures [17, 57, 43, 28, 19, 53, 44],
memory allocators [61, 13, 30, 56], and file systems [18, 21, 67, 38, 20]. The
guarded protection follows the following reader-writer pattern around a flag
variable, which we call _“guardian”_ : (1) The writer ensures that both key
and value are “persisted before” the flag is persisted (Figure 1(b)). (2) The
reader checks if the flag is set before reading the key and value, which we
call _“guarded read”_ (Figure 1(a)). The persistence ordering (for the writer
side) and the guarded read (for the reader side) together ensure that the
reader reads atomic (both old or both new) states of key and value.

From the guarded read pattern in Figure 1(a), we infer the first _persistence
ordering invariant_ : a key-value pair should be persisted before a token
(i.e., P(slot[j].key/value)$\xrightarrow[]{\text{hb}}$W(token[j])). We then
extend it to the second _persistence atomicity invariant_ : the updates of two
or more guardians should be atomic. Otherwise, an atomic update of multiple
key-value slots cannot be guaranteed (i.e., AP(token[j],token[k])).

Later we find that level_insert violates the persistence ordering invariant at
Line 18, and level_update violates the persistence atomicity invariant at Line
39. Witcher tests only NVM states that violate the inferred invariants. For
example, in level_insert we test only one case that a token is persisted but a
key-value pair is not persisted, which violates the writer pattern in the
guarded protection. Similarly, in level_update we test two cases that one
token is persisted and another token is not. In this way, we can significantly
reduce testing space without the developer’s manual annotation.

In § 4.3, we present more generalized meta-rules to infer likely invariants
beyond guarded protection. Note that Witcher does not require prior knowledge
of truth and does not assume invariants are always correct: if two invariants
contradict, we test both cases to discern which one is correct.

###  3.2 Output Equivalence Checking

We propose an _output equivalence checking_ approach to validate if an NVM
state that violates an inferred invariant is indeed inconsistent, indicating a
crash consistency bug. The key insight is that we can construct an oracle (a
correct execution) to compare with to discern whether a given NVM state is
inconsistent by leveraging atomic (all or nothing) semantics of (correct)
crash-consistent NVM programs. Hence we do not need to rely on a user-provided
consistency checker or a code annotation for validation (as in existing
works).

Suppose that we perform the following four operations on Level Hashing:
insert(k,v0), delete(k), insert(k,v1), and query(k) (see Figure 3(a)). If the
program crashes while executing the third insert(k,v1), it should behave as if
the operation either did happen or did not. After the resumption, we know two
possible, correct outputs of the following query(k) are either v1 or null. If
a program starting from an invariant-violating NVM state produces output that
is different from these two oracles, then we can confidently conclude that the
program is not crash-consistent, and the invariant violation is indeed a true
crash consistency bug.

Note that our oracles rely on test cases, and thus some crash consistency bugs
may not be detected if they do not produce visible symptoms (e.g.,
segmentation fault, different output, etc.) on the given test cases. This
implies that we may have false negatives. However, any detected output
divergence is indeed an indicator of a true crash consistency bug: i.e., we do
not have false positives.

##  4 Design of Witcher

Figure 3: An example of Witcher’s crash consistency bug detection steps.

We describe the detailed design of Witcher. Figure 2 illustrates Witcher’s
six-stage architecture. As a dynamic systematic testing tool, Witcher starts
by generating a random test case (§ 4.1). Witcher instruments an NVM program
and runs the test case to collect a memory trace (§ 4.2), from which Witcher
infers invariants (§ 4.3). Then, from the same trace, Witcher constructs a set
of legal crash NVM images violating the inferred invariants (§ 4.4) and
performs output equivalence checking to validate them (§ 4.5). Last, Witcher
reports the crash consistency bugs after clustering similar cases (§ 4.6) to
ease developers’ root cause analysis. Witcher supports both single-threaded
and multi-threaded testing. We explain single-threaded testing in this
section. Then we present our extension for multi-threading later in § 4.7.

###  4.1 Generating Test Cases

Witcher requires a deterministic test case such that its output is
deterministic for a given input for output equivalence checking. Any
deterministic test case with a good code coverage would suffice. An ideal
crash consistency testing tool should explore the three dimensions of testing
space: (1) program input, (2) thread interleaving, and (3) NVM state
(persistence). Witcher focuses on exploring the (3) persistence space in a
systematic and scalable manner. We leave a smarter test case generation for
program input and thread interleaving and their test space reduction as future
work, and instead use random testing in this work.

By default, Witcher supports random test case generation of index structures,
providing standard APIs such as insert, delete, update, query, and scan.
Witcher randomly generates a list of operations, keys, and values. For
operation parameters, in order to make some dependent operations (e.g., get,
delete, update) more meaningful, we assign a higher probability to generate a
key used before in earlier operations.

###  4.2 Tracing Memory Accesses

Witcher uses an NVM program execution trace to infer invariant (§ 4.3) and
construct crash NVM images (§ 4.4) to validate later. We instrument an NVM
program using an LLVM compiler pass and then execute the instrumented NVM
binary with a test case to collect the execution trace. We trace load, store
(including the updated value), branch, call/return, flush (i.e., clflush,
clflushopt, and clwb) and memory fence (i.e., sfence and mfence) instructions.
We order the instructions in a trace by protecting our tracing code using a
global mutex so we can easily analyze traces of multi-threaded programs.

Suppose we trace Level Hashing in Figure 1 using the test case with four
operations in Figure 3(a). Figure 3(b) shows the trace of the last
laststaticquery operation. Each trace includes a unique Trace ID (TID), a
Static Instruction ID (SID), which is essentially the instruction location in
the binary, and instruction type. For load and store, Witcher additionally
traces its address, length (not shown), and data (for store), and whether
accessing DRAM (white) or NVM (gray).

###  4.3 Inferring Likely Invariants

In this step, Witcher performs a program dependency analysis and infers a set
of likely invariants from the memory trace. We first describe a set of meta-
rules designed to infer (1) persistence ordering invariants and (2)
persistence atomicity invariants (§ 4.3.1). Then we explain how Witcher uses
program dependence analysis to apply the meta-rules and infers the
corresponding invariants from the memory trace (§ 4.3.2).

####  4.3.1 Meta-Rules for Ordering and Atomicity Invariants

At a high level, each rule looks for control and/or data dependencies between
NVM locations X and Y, and infers a likely invariant that “X should be
persisted before Y” (ordering invariant) or “X and Y should be persisted
atomically” (atomic invariant). From the invariant, Witcher later constructs
an NVM state that violates it – e.g., “Y is persisted, but X is not” (§ 4.4)
and tests if this invariant violation produces a wrong output (§ 4.5). Another
way to explain the benefit of invariant inference is that for two NVM
addresses X and Y, if Witcher does not detect any dependency, it does not test
such cases involving X and Y and saves the test time (assuming that
independent NVM objects do not lead to an inconsistent state). Table 1
summarizes meta-rules for inferring invariants:

RO1. Data dependency implies persistence ordering..RO1. Data dependency
implies persistence ordering.RO1. Data dependency implies persistence
ordering.. Suppose a developer writes a code “Y=X+3” where the write of Y is
data-dependent on the read of X (which we denote
W(Y)$\xrightarrow[]{\text{dd}}$R(X)). From the data dependency, we hypothesize
that the developer would want X to be persisted before updating Y (i.e.,
P(X)$\xrightarrow[]{\text{hb}}$W(Y)) so that she does not update an NVM state
Y based on “unpersisted” X. Otherwise, an inconsistent state may be generated
when a program crashes after Y becomes persisted, but X is not. The first
meta-rule RO1 in Table 1 is based on this reasoning: for two memory locations
X and Y in NVM, if we find the Condition W(Y)$\xrightarrow[]{\text{dd}}$R(X),
we infer the Likely Invariant P(X)$\xrightarrow[]{\text{hb}}$W(Y). From the
invariant we later create a crash NVM image where Y is persisted and X is
unpersisted, if such state is legal in program execution.

RO2. Control dependency implies persistence ordering..RO2. Control dependency
implies persistence ordering.RO2. Control dependency implies persistence
ordering.. Consider a code “if(X) Y=3” where the write of Y is control-
dependent on the read of X. Similar to RO1, we hypothesize that a developer
would want to make X persisted before updating Y so that she does not update Y
based on “unpersisted” X. More formally, RO2 says: for two memory locations X
and Y in NVM, if we find the Condition W(Y)$\xrightarrow[]{\text{cd}}$R(X), we
infer the Likely Invariant P(X)$\xrightarrow[]{\text{hb}}$W(Y). From the
invariant, we simulate a state where Y is persisted but X is not if such state
is legal.

RO3. Guarded read implies persistence ordering..RO3. Guarded read implies
persistence ordering.RO3. Guarded read implies persistence ordering.. As
discussed in § 3.1, guarded protection is a common NVM programming pattern. It
achieves the atomicity of data using the writer-side persistence ordering and
the reader-side guarded read. Based on this observation, if we see the reader-
side guarded read pattern, we infer the likely invariant on the writer-side
persistence ordering. In other words, RO3 says: for two memory locations X and
Y in NVM, if we find the Condition R(Y)$\xrightarrow[]{\text{cd}}$R(X), we
infer the Likely Invariant P(Y)$\xrightarrow[]{\text{hb}}$W(X). We then
validate the invariant from the NVM state such that X is persisted but Y is
not. Note that here X is a guardian in the guarded read pattern (e.g., token
in Figure 1) and thus it should be persisted last (after key and value).

RA1. Guardian implies persistence atomicity..RA1. Guardian implies persistence
atomicity.RA1. Guardian implies persistence atomicity.. As in the RO3 ordering
invariant, we can find a set of guardians – e.g., token[j] and token[k] in
Figure 1. A program state could be inconsistent if they are not updated
atomically. Based on this observation, we infer the likely invariant on
persistence atomicity such that two or more guardians should be atomically
updated. RA1 in Table 1 says: for two guardians X and Y from RO3, we infer the
Likely Invariant AP(X,Y) that X and Y should be atomically persisted. We
simulate NVM states such that only one guardian is persisted. This approach
allows us to reduce testing space significantly because we will not test
persistence atomicity for well-guarded NVM data. For example, if a program
applies the guarded read patterns on key and value in all places (using token
as a guardian), then we do not test persistence atomicity between them.

# | Condition | Likely Invariant | NVM Image
---|---|---|---
Example | Rule | Example | Rule |  $\mathbb{P}$ | $\mathbb{U}$
RO1 | Y=X+3; | W(Y)$\xrightarrow[]{\text{dd}}$R(X) | X=...;Y=...; | P(X)$\xrightarrow[]{\text{hb}}$W(Y) | Y | X
RO2 | if(X){Y=3;} | W(Y)$\xrightarrow[]{\text{cd}}$R(X) | X=...;Y=...; | P(X)$\xrightarrow[]{\text{hb}}$W(Y) | Y | X
RO3 | if(X){Z=Y+3;} | R(Y)$\xrightarrow[]{\text{cd}}$R(X) | Y=...;X=...; | P(Y)$\xrightarrow[]{\text{hb}}$W(X) | X | Y
RA1 | if(X){M=N+3;} | R(N)$\xrightarrow[]{\text{cd}}$R(X) | X=...;Y=...; | AP(X,Y) | X | Y
if(Y){K=J+3;} | R(J)$\xrightarrow[]{\text{cd}}$R(Y) | Y | X

R(X): read X W(X): write X P(X): persist X $\mathbb{P}$: persisted
$\mathbb{U}$: unpersisted
E1 $\xrightarrow[]{\text{cd}}$ E2: E1 is control dependent on E2 E1
$\xrightarrow[]{\text{dd}}$ E2: E1 is data dependent on E2
E1 $\xrightarrow[]{\text{hb}}$ E2: E1 should happen before E2 AP(X,Y): X and Y
persisted atomically

Table 1:  Three meta-rules RO1–RO3 for persistence ordering invariants and one
meta-rule RA1 for atomicity invariants.

####  4.3.2 Program Analysis for Invariant Inference

Witcher performs program dependence analysis to infer likely invariant from
the source codes and execution traces. Witcher first constructs Program
Dependence Graph (PDG) [23, 54, 25] where a node represents a traced
instruction, and an edge represents data or control dependency. Then, Witcher
simplifies the PDG into what we called Persistence Program Dependence Graph
(PPDG) that captures dependencies between NVM accesses to make it easy to
apply the invariant inference meta-rules. For example, Figure 3(c) shows the
PDG of the trace (b), and (d) shows the PPDG.

Witcher uses a mix of static and dynamic trace analysis to construct a PDG.
When instrumenting the source code for tracing (§ 4.2), it performs static
analysis to capture register-level data and control dependency. Then it
extracts memory-level data dependence by analyzing memory-level data-flow in
the collected trace. This dynamic memory-level data dependency analysis
improves PDG’s precision compared to static-only analysis which suffers from
the imprecision of pointer analysis. The static instruction IDs (binary
address) are used to map static and dynamic information.

Witcher converts a PDG to a PPDG as follows. Initially, the PPDG has only
(gray) NVM nodes. Witcher traverses the PDG from one NVM node to another NVM
node. If there is at least one control-flow edge along the path, it adds a
control-flow edge in the PPDG. If a path includes only data-flow edges, it
adds a data-flow edge in the PPDG. No path implies no dependency.

Given the PPDG, Witcher then applies the meta-rules in Table 1 to infer likely
invariants. For each edge and two nodes in the PPDG, Witcher considers the
type of edge (control vs. data) and the type of instructions (store vs. load).
When Witcher finds a Condition, it records the corresponding Likely Invariant.
For example, the PPDG in Figure 3(d) shows that
R(key)$\xrightarrow[]{\text{cd}}$R(token). Based on RO3, we infer the
invariant I1: P(key)$\xrightarrow[]{\text{hb}}$W(token) in (e). Similarly, we
can infer the persistence ordering invariants I2 and I3. Moreover, as token
and key are guardians for guarded reads, based on RA4, we infer the
persistence atomicity invariant I4: AP(token,key).

###  4.4 Generating Crash NVM Images

The next step after inferring invariants is to generate a set of crash NVM
images111 In PMDK, an NVM image is a regular file containing an NVM heap state
created, loaded, and closed by PMDK APIs [34]. that violate the invariants.
Later in § 4.5, we will describe how Witcher loads these NVM images and uses
output equivalence checking for validation.

At a high level, Witcher generates crash NVM images as follows. Witcher takes
as input the same trace used to collect invariants and performs cache and NVM
simulations along the trace. During the simulation, Witcher cross-checks if
there is an invariant violation. Each invariant-violating NVM state forms a
crash NVM image. Witcher produces a set of crash NVM images for further
validation.

####  4.4.1 Simulating Cache and NVM States

The goal of the cache/NVM simulations is to generate only feasible NVM states
that violate likely invariants but still obey the semantics of a persistence
control at a cache line granularity (e.g., the effects of a flush
instruction). Starting from the empty cache and NVM states, Witcher simulates
the effects of store, flush, and fence instructions along the trace while
honoring the memory (consistency) model of a processor. In particular, Witcher
supports Intel’s x86-64 architecture model, as in Yat [42]. The following two
rules are, in particular, relevant to the cache/NVM simulations:

  * •

A fence instruction guarantees that all the prior flush-ed stores are
persisted.

  * •

A processor does not reorder two store instructions in the same cache line
(following the x86-TSO memory consistency model [62, 35]). Suppose that X and
Y are in the same cache line and a program executes two stores W(X) and W(Y)
in order. In this case, the valid NVM states are: (1) nothing persisted, (2)
only X is persisted, and (3) both X and Y are persisted. Note that the case
that only Y is persisted is _not_ valid since it violates the program order.

Consider the trace of Level Hashing’s levelinsert code in Figure 3(f). After
simulating the first three store instructions (TID 200-202), there could be
multiple valid cache/NVM states. For example, the data ‘‘k’’ for key could
either remain in a cache (unpersisted) or could be evicted (persisted). The
same is true for the val and token. However, after finishing the execution of
the last fence instruction (TID 205), key and val are guaranteed to be
persisted (due to flush and fence). Still, token could be either unpersisted
or persisted.

####  4.4.2 Checking Invariants Violations

During the simulation, Witcher checks if there could be an NVM state that
violates a likely invariant before executing each fence instruction because
the fence ensures a persistent state change. Witcher considers all possible
persisted/unpersisted states while honoring the above cache/NVM simulation
rules.

Consider the trace of Level Hashing’s levelinsert code in Figure 3(f) again.
Before we execute the last fence instruction (TID 205), we check the four
invariants against the trace as shown in (e). For instance, I1 says that
P(key)$\xrightarrow[]{\text{hb}}$W(token). The invariant violating state is
the one that token is persisted, but key is not. We check if this invariant
violating case is feasible in this code region (before the fence). The answer
is yes – a program crashes between the TID 202 store and the TID 203 flush
instructions, and the cache line for token is evicted (persisted) but not for
key and val (unpersisted). This forms the first crash NVM image IMG1 in (g).
Similarly, we can find that IMG1 is also the state that I3 and I4 are
violated. We can also find the second IMG2 in (g) violating I2 and I4.

Each crash NVM image is indeed represented as a pair of a fence ID and a store
ID, which specifies where to crash and which store to be persisted,
respectively. Witcher repeats the process along the trace and generates a set
of crash NVM images that will be validated in the next step.

###  4.5 Output Equivalence Checking

Witcher validates the invariant-violating crash NVM images and detects crash
consistency bugs using output equivalence checking. The key idea is that if
the NVM program is crash-consistent, after a recovery from a crash, it should
behave as if the operation where the crash occurred is either fully executed
(committed) or not at all executed (rollbacked). And thus, after the crash,
the program should produce the output of one of these two executions, which we
call _oracles_.

Consider the example in Figure 3 again. Using the test case insert(k,v0),
delete(k,v0), insert(k,v1), and query(k) in (a), we analyzed the trace of the
third insert(k,v1) operation in (f) to generate two crash NVM images in (g).
The first IMG1 reflects an NVM state that the first two operations,
insert(k,v0) and delete(k,v0), are correctly performed, and the program
crashes in the middle of the third insert(k,v1) where only token is persisted,
and key and value remain unpersisted – i.e., IMG1 has the old value v0.

Witcher generates two oracles to compare. The first oracle reflects an
execution where the crashed operation is committed – thus we run the test case
insert(k,v0), delete(k,v0), insert(k,v1), and query(k) (no crash) and records
v1 (the new value) as the output of query(k). The second oracle mimics an
execution where the crashed operation is rollbacked – we run the same test
case without the third insert(k,v1) and log null as the output of query(k).
Altogether, the oracles say that the correct output of the last query(k) is
either v1 or null.

For output equivalence checking, Witcher loads a crash NVM image, runs a
recovery code (if exists), executes the rest of the test cases, records their
outputs, and compares them with the oracles. For example with IMG1, query(k)
returns the old value v0 (as neither the deletion of k nor the insertion of
new value v1 was not persisted) – Witcher detects the mismatch and reports the
test case and the crash NVM image information (the crash location as the fence
TID, and the persistence state as the persisted store ID). On the other hand,
a similar analysis with the second IMG2 shows that the output (null) matches
the oracles, so Witcher does not report them.

###  4.6 Clustering Bug Reports

One key benefit of the prior output equivalence checking is that all the
reported cases indeed reflect buggy inconsistent states (no false positives).
Nonetheless, many cases may share the same root cause: e.g., a bug in insert
operation may repeatedly appear if the test case has many insert calls.

To help programmers finding the root causes, Witcher clusters the bug reports
according to operation type (e.g., insert, delete) and execution path (a
sequence of basic blocks) that appeared in the trace. We found that our
clustering scheme helps the root cause analysis significantly because after
one root cause is found, reasoning about the redundant cases along the same
program path is relatively simpler. Multiple clusters may share the same root
cause.

###  4.7 Extension for Multi-threaded NVM Programs

Comparing two oracles is sufficient for testing single-threaded NVM program.
However, for multithreaded cases, output equivalence checking should consider
more oracles as a program may crash while M concurrent operations are running.
Each per-thread operation has two legal states (all or nothing), and we also
need to consider different permutations of a linearization order. Thus, the
number of oracles is $P(M,0)+P(M,1)+...+P(M,M-1)+P(M,M)$, where
$P(m,k)=\nicefrac{{m!}}{{(m-k)!}}$. For example, we need 5 oracles for 2
threads and 65 oracles for 4 threads. As discussed in § 4.1, Witcher focuses
on exploring the persistence space in a systematic and scalable manner, and we
leave thread-interleaving space reduction as future work.

| Application | Description | Design |  Concu- rrency | LOC | Likly Invariant Inference | Output Equivalence Checking | # bugs
---|---|---|---|---|---|---|---|---
|  # ordering invariants |  # atomicity invariants |  execution time |  # crash NVM images |  # images w/ output mismatch |  # clusters |  execution time |  # PO |  # PA
Persistent Data Structures | WOART [43] | radix tree | LL-ASM | ST | 835 | 33428 | 5027 | 1m51s | 13364 | 22 | 5 | 2m33s | 0 | 1
WORT [43] | radix tree | LL-ASM | ST | 498 | 21248 | 4709 | 53s | 18886 | 0 | 0 | 2m42s | 0 | 0
Fast Fair [28] | B+tree | LL-ASM | LB | 1083 | 468865 | 1318 | 3m58s | 59270 | 46866 | 104 | 12m21s | 1 | 2(1)
Level Hash [72] | hash table | LL-ASM | ST | 1008 | 27941 | 1653 | 6m41s | 52678 | 43177 | 29 | 1h40m | 10 | 7
CCEH [53] | hash table | LL-ASM | LB | 989 | 8960 | 1842 | 3m17s | 18697 | 490 | 5 | 30m3s | 0 | 2(1)
P-ART [44] | radix tree | LL-ASM | LB | 2356 | 2065 | 1389 | 2h | 16454 | 36 | 4 | 3m27s | 0 | 2
P-BwTree [44] | B+tree | LL-ASM | LF | 4860 | 35135 | 5400 | 47m53s | 41662 | 5137 | 85 | 1h11m | 2 | 0
P-CLHT [44] | hash table | LL-ASM | LB | 4461 | 3065 | 806 | 2m2s | 6086 | 2 | 1 | 9m33s | 1 | 0
P-HOT [44] | trie | LL-ASM | LB | 10463 | 31435 | 18608 | 4h | 72998 | 1253 | 111 | 25m26s | 3 | 0
P-Masstree [44] | B tree + trie | LL-ASM | LB | 1975 | 22662 | 4119 | 10m33s | 75234 | 76 | 10 | 12m | 0 | 1
Micro | Array | array | LL-PMDK | ST | 405 | 3208 | 488 | 6m35s | 488 | 487 | 2 | 30s | 0 | 1(1)
B-Tree | B tree | TX-PMDK | ST | 493 | 1143 | 130 | 28m46s | 97590 | 21551 | 50 | 20m57s | 1* | 1(1)
C-Tree | crit-bit trie | TX-PMDK | ST | 293 | 9752 | 704 | 58m49s | 23875 | 0 | 0 | 16m31s | 0 | 0
RB-Tree | red-black tree | TX-PMDK | ST | 416 | 15337 | 725 | 37m15s | 256470 | 4785 | 64 | 46m16s | 0 | 1(1)
Hashmap-TX | hash table | TX-PMDK | ST | 353 | 8979 | 801 | 1h | 25997 | 3 | 2 | 27m4s | 1 | 0
Real | Memcached | key-val store | LL-PMDK | LB | 17731 | 11228 | 2708 | 14m40s | 11493 | 0 | 0 | 48h28m | 0 | 0
Redis | key-val store | TX-PMDK | ST | 44642 | 5659 | 942 | 1h35m | 174610 | 0 | 0 | 72h45m | 0 | 0
| Total | - | - | - | 92861 | 710110 | 51369 | 12h19m | 965852 | 123885 | 472 | 127h34m | 19 | 18(5)

LL-ASM: low-level persistence primitives (asm) TX-PMDK: PMDK transaction LL-
PMDK: low-level persistence primitives (PMDK)

ST: single-threaded LB: lock-based LF: lock-free PO: persistence ordering bug
PA: persistence atomicity bug (#): number of known bugs *: bug in PMDK library

Table 2:  The tested NVM programs, the detailed statistics of Witcher bug
finding, and the number of detected bugs.

##  5 Implementation

All Witcher components except tracing and program dependency analysis are
written in 4400 lines of Python code. We built tracing and program dependency
analysis based on Giri [60], a dynamic program slicing tool implemented in
LLVM [6]. Our Giri modification comprises of around 3600 lines of C++ code and
includes the following three extensions. First, we ported Giri from LLVM v3.4
to v9.0.1. Second, we extended its program slicing component to generate PDG
and PPDG. Third, we modeled library function calls and assembly instructions
that have the semantics of load/store (e.g., atomic.store) and persistence
(e.g., clwb, sfence).

Our current prototype supports an NVM program built on PMDK libpmem or
libpmemobj libraries to create/load an NVM image from/to disk. To ensure the
virtual address of mmap-ed NVM heap the same across different executions, we
set PMEMMMAPHINT environment variable. Witcher runs PPDG construction, crashed
NVM image generation, and output equivalence checking in parallel.

The current prototype does not support kernel-level NVM programs. Tracing a
kernel execution and inferring invariants can be supported. More engineering
efforts, however, are required to support checkpointing (or rollback)
kernel/NVM states and resuming from a clean state for output equivalence
checking. Systematic testing of a kernel-level program (e.g., using
virtualization like Yat) is left as future work.

##  6 Evaluation

###  6.1 Evaluation Methodology

NVM Programs..NVM Programs.NVM Programs.. Table 2 shows the three groups of 17
NVM programs that we used to evaluate Witcher. The first group includes ten
state-of-the-art persistent data structures highly optimized for NVM and
published at top-tier systems conferences. For high performance, they all used
_low-level_ (LL) persistence primitives such as flush and fence instructions.
Some (e.g., FAST-FAIR [28]) incorporate inconsistency tolerable design where a
naive crash consistency bug detection approach would lead to false positives.

We found that they are not properly written to use persistent heap and locks
for NVM. They were all _emulated with volatile memory_. Thus, we made the
following source code changes to make them actually use NVM. First, they all
used either regular _volatile_ memory allocator (i.e., malloc, free) or PMDK’s
libvmmalloc allocator [33], which do not guarantee crash consistency of the
NVM heap metadata. To faithfully construct an NVM image including the NVM heap
state, we ported them to use PMDK’s libpmemobj allocator [31]. Second, for
lock-based data structures, we added a recovery code to release locks when
loaded from an NVM image to avoid deadlock. We made 5041 lines of code and
script changes in total. With the advent of real NVM hardware (e.g., Intel’s
Optane memory), we believe all reasonable (future) applications should use a
proper persistence library (e.g., PMDK). For applications that are already
implemented with NVM/PMDK in the following groups, we did not make any change.

The second group includes four relatively-simple (300–500 LOC) persistent data
structures that appeared in the PMDK library as example codes. They used
PMDK’s low-level (LL) or _transactional_ (TX) persistence programming model.
We included them mainly to compare Witcher with prior works which only test
them and do not evaluate the first group. For TX-PMDK applications, Witcher
traces and analyzes PMDK internals such as persistence heap allocation and
transactional undo logging logics, validating both the PMDK library itself and
transactional NVM programs using them.

The last group includes PMDK-based two server programs Memcached and Redis
using PMDK’s LL and TX persistence APIs, respectively.

Test case.Test caseTest case. We run the NVM programs with a test case
consisting of 2000 randomly generated operations. They provide a different but
mostly similar set of APIs (e.g., insert, delete, query). The server programs
were also tested with the client generating the same number (2000) of random
key-value requests over network. As discussed in § 4.1, Witcher does not focus
on exploring program input test space, and simply relies on a random testing.
We found that 2000 operations are large enough to achieve a reasonable and
stable code coverage (50%-80%). Missing code coverages are due to unused
features (e.g., garbage collection) and debugging codes.

Experimental setup.Experimental setupExperimental setup. We ran all
experiments on a 64-bit Fedora 29 machine with two 16-core Intel Xeon Gold
5218 processors (2.30GHz), 192 GB DRAM, and 512 GB NVM.

###  6.2 Detected Crash Consistency Bugs

Witcher detected 37 (32 new) bugs from 13 programs. There were 19 persistence
ordering bugs and 18 persistence atomicity bugs. All the bugs were confirmed
by the developers. See the last two columns of Table 2.

The detected bugs have diverse impacts: lost, unexpected, duplicated key-value
pairs; unexpected operation failure; and inconsistent structure. For example,
a crash in the middle of rehashing operation in Level Hashing may lead to
lost, unexpected, duplicated key-value pairs since the metadata is not
consistent with the stored key-value pairs. In FAST-FAIR, if a crash happens
in splitting the root node and right before setting the new root node, the
B+tree will be in an illegal state; the root node connects to a sibling node.
Any further operation on the B+tree will lead to a program crash or
performance degradation.

Many detected bugs are not shallow. For instance, the bug in CLHT only occurs
when a program crashes at a specific moment during rehashing while leaving a
specific set of stores unpersisted. Our study reveals that it is hard for a
developer to reason about all possible NVM states (as reasoning about all
possible thread interleaving is difficult for multithreaded programming).

The bug appeared in B-Tree was indeed a persistence ordering bug inside of
PMDK’s persistent pool/heap allocation function pmemobj_tx_zalloc [2]. The bug
did not manifest in other TX-PMDK applications as it resides in a code path
that requires a large-size object allocation.

Comparison with RECIPE.Comparison with RECIPEComparison with RECIPE. Our
results show that Witcher’s approach is effective in discovering new crash
consistency bugs in NVM programs. In particular, all the tested low-level
persistent data structures (except for WOART and WORT) have been heavily
tested by RECIPE [44], but Witcher is still able to report 30 new bugs. RECIPE
only reported four bugs, two of which are overlapped with Witcher. The other
two bugs are due to missing persistence primitives in root node
initialization. We found and fixed these two bugs while we ported the test
data structures to use PMDK’s memory allocator, so we did not count them as
the bugs that Witcher found.

###  6.3 Statistics of Witcher Bug Finding

Table 2 also presents the detailed statistics of each major step in Witcher.
Across 17 NVM programs, when tested with 2,000 operations, Witcher infers in
total 710K (42K on average) ordering invariants and 51K (3K) atomicity
invariants. Witcher generated 966K (57K) crash NVM images, 124K of which
failed output equivalence checking.

Witcher finally reported 472 clustered bugs. We found that bug clustering
significantly reduces manual efforts in root cause analysis. Witcher also
provides sufficient information for root cause analysis including execution
trace, crash location, persisted and unpersisted writes, and a crash NVM image
which can be loaded for further gdb debugging. Two graduate students performed
root cause analysis. It took about 7 hours to investigate the 472 bug
clusters.

We found that Witcher prototype is fast enough for practical use. Invariant
inference took a few minutes to four hours. Output equivalence checking took a
few minutes to two hours, except for two servers. The overhead of output
equivalence checking is proportional to the number of crash NVM images and the
cost of each test run. As server programs, Memcached and Redis require live
networking-based testing, which made output equivalence checking slower than
the others. Its high overhead stems from server start/shutdown and client
connection setup cost for each test run. The pure execution overhead was
indeed small as in other applications. Moreover, the current prototype does
not parallelize output equivalence checking for server programs.

###  6.4 Comparison with Annotation-Based Approaches

| App | Design | Bugs detected by | Bug Description
---|---|---|---|---
|  Witcher? | Others?
Micro | B-Tree | TX-PMDK | ✓ | ✓ | Modify without logging
C-Tree | TX-PMDK | $\times$ | $\times$ | N/A
RB-Tree | TX-PMDK | ✓ | ✓ | Modify without logging
Hashmap-TX | TX-PMDK | $\times$ | $\times$ | N/A
Real | Memcached | LL-PMDK | $\times$ | $\times$ | N/A
Redis | TX-PMDK | $\times$ | ✓(Benign) | Modify outside TX

TX-PMDK: PMDK transaction LL-PMDK: PMDK low-level persistence primitives

Table 3:  Comparison between Witcher and two annotation-based approaches,
PMTest [46] and XFDetector [45].

This section compares Witcher with two annotation-based approaches, PMTest
[46] and XFDetector [45]. PMTest provides two primitives: isPersist and
isOrderedBefore, but does not support one for persistence atomicity.
Hypothetically, assuming correct/full annotations, PMTest would be able to
detect 19 ordering bugs but miss 18 atomicity bugs in Table 2. XFDetector
targets logging-based (e.g., UNDO, REDO) NVM programs. XFDetector cannot be
applied to the 12 low-level programs. Besides, a developer should annotate
“commit variable” to prune benign cases.

Actually, 6 of 17 programs in Table 2 were tested by PMTest and XFDetector as
well. Table 3 lists those six programs that consist of four micro-benchmarks
from PMDK examples and two servers (Redis and Memcached). More precisely,
PMTest and XFDetector tested one and two more programs: HashMap-Atomic and
PMFS. We did not test HashMap-Atomic because it relies on PMDK’s persistent
linked-list library, which we did not instrument and trace. We also did not
test PMFS, an in-kernel file system, because Witcher currently only supports
user-space applications and the PMFS code [29] has not been maintained for
real NVM. We expect that Witcher should be able to detect bugs in HashMap-
Atomic and PMFS by extending the prototype because they share the same
characteristics as the bugs detected in other tested programs.

Detected bugs.Detected bugsDetected bugs. Table 3 shows that among the three
bugs that PMTest/XFDetector found, Witcher also detects two of them in B-Tree
and RB-Tree. Both are due to missing logging inside a transaction. Note that
Witcher detected another bug in the PDMK library while testing B-Tree, which
was missed by them.

Missed bug.Missed bugMissed bug. Witcher missed one bug in Redis reported by
PMTest/XFDetector. In theory, Witcher may have false negatives for two
reasons: (1) Witcher may not be able to infer the relevant likely invariants
from the trace. (2) The test case may not reveal the symptom of inconsistent
behavior during output equivalence checking. Upon further investigation, we
found that it is none of the two cases. Interestingly, it turns out that the
bug was benign. The bug is in the server initialization code. After allocating
a PMDK root object, Redis initializes the root object to zero “outside” of a
PMDK transaction. PMTest/XFDetector detects this unprotected update as a bug.
However, this is benign – it does not lead to an inconsistent state. The root
object was allocated using POBJROOT() [3], which already zeroed out the newly
allocated object. Both the old and new values are zero. Therefore, it does not
matter if the new zero update is persisted or not. Witcher actually detected
this store violating an atomicity invariant, and performed output equivalence
checking. But it does not show any visible divergence. This example
particularly shows the benefit of our output equivalence checking, pruning
false positives.

###  6.5 Comparison with Exhaustive Testing Approaches

$10^{0}$$10^{6}$$10^{12}$$10^{18}$$10^{24}$$10^{30}$

$0$

$500$

$1000$

$1500$

$2000$

$10^{0}$$10^{6}$$10^{12}$$10^{18}$$10^{24}$$10^{30}$

$0$

$500$

$1000$

$1500$

$2000$

$10^{0}$$10^{6}$$10^{12}$$10^{18}$$10^{24}$$10^{30}$

$0$

$500$

$1000$

$1500$

$2000$

# tests

# opsLevel Hashing# opsFAST-FAIRWitcherPMReorderYat# opsCCEH Figure 4:  Test
space comparison for 2000 random operations.

Lastly, we compare Witcher with two existing exhaustive-testing-based tools
Yat [42] and PMReorder [32] to show how effectively our likely invariant-based
approach can reduce the testing space. In particular, we compare the number of
crash states that each tool will validate using the same trace with 2000
random operations as in § 6.2. We simulate Yat and PMReorder algorithms to
calculate the numbers of test cases.

Figure 4 shows the representative results for Level Hashing, FAST-FAIR, and
CCEH programs. The test space of Yat and PMReorder is several orders larger
than Witcher. Sudden spikes happen in Yat when there is a rehashing in Level
Hashing and CCEH or a node split/merge in FAST-FAIR. That is because rehashing
and node split/merge require many key-value movements, and Yat tests all
possible crash states due to its exhaustive approach. On the other hand,
Witcher only tests when there is an invariant violation, significantly
reducing the number of test cases (yet detecting many bugs).

PMReorder behaves much worse than Yat particularly in FAST-FAIR and Level
Hashing because it does not perform cache line granularity analysis. As a
result, PMReorder may test many infeasible crash states violating the memory
model, hinting potential false positives. PMReorder behaves better than Yat in
CCEH before 1278 operations because it only tests those stores that are
explicitly flushed at each fence instruction, indicating potential false
negatives.

##  7 Related Work

Likely-invariants based testing.Likely-invariants based testingLikely-
invariants based testing. A concept of likely-invariants has been used to
detect program bugs [22, 41, 48, 71, 39, 51], to verify the network [47], and
to detect resource leak [64]. Notably, Engler et al.’s version (called
beliefs) [22] enables automatic analysis of likely correctness conditions
without in-depth knowledge. To the best of our knowledge, Witcher is the first
work that infers likely invariant in the context of crash consistency testing
for NVM programs.

Output-equivalence based testing.Output-equivalence based testingOutput-
equivalence based testing. Burckhardt et al. [14] and Pradel et al. [58]
detect thread-safety violations, comparing the concurrent execution to
linearizable executions of a test. Witcher’s output equivalence checking
shares some idea of these two works in the sense that they all compare an
observed execution with “oracles”, but is uniquely designed to detect for NVM
crash consistency bugs.

Crash consistency testing in file systems.Crash consistency testing in file
systemsCrash consistency testing in file systems. There has been a long line
of research in testing and guaranteeing crash consistency in file systems [52,
70, 69, 24, 59, 16, 15, 63, 68, 40]. In-situ model checking approaches such as
EXPLODE [69] and FiSC [70] systematically test every legal action of a file
system with minimal modification. B3 [52] performs exhaustive testing within a
bounded space, which is heuristically decided based on the bug study of real
file systems. Witcher reduces test space by using inferred invariants, unlike
limiting testing space in B3. Feedback-driven File system fuzzers, such as
Janus [68] and Hydra [40], mutate both disk images and file operations to
thoroughly explore file system states. We believe Witcher’s test case
generation can be further improved by adopting feedback-driven fuzzing
techniques.

##  8 Conclusion

We present Witcher, a scalable, automatic, and precise crash consistency bug
detector for NVM software. Witcher infers _likely invariants_ that are
believed to be true to be crash-consistent from source codes and program
traces, and performs _output equivalence checking_ to validate likely
invariant violations. This approach allows Witcher to detect crash consistency
bugs without manual annotations, user-provided consistency checker, or
exhaustive testing. We evaluated Witcher on 17 NVM programs and found 37 crash
consistency bugs, including 32 new ones. We will open-source Witcher for NVM
programmers to use and extend it.

## References

  * [1] Key/Value Datastore for Persistent Memory.  URL: https://github.com/pmem/pmemkv.
  * [2] PMDK issue to fix reported bug in allocation.  URL: https://github.com/pmem/pmdk/issues/4945.
  * [3] PMDK Root Object APIs.  URL: https://pmem.io/pmdk/manpages/linux/master/libpmemobj/pmemobj_root.3.
  * [4] Pmem-Memcached.  https://github.com/lenovo/memcached-pmem.
  * [5] Pmem-Redis.  https://github.com/pmem/redis/tree/3.2-nvml.
  * [6] The LLVM Compiler Infrastructure.  URL: https://llvm.org/.
  * [7] Proceedings of the 40th International Conference on Very Large Data Bases (VLDB), Hangzhou, China, September 2014.
  * [8] Proceedings of the 41st International Conference on Very Large Data Bases (VLDB), Hawaii, USA, September 2015.
  * [9] Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Carlsbad, CA, October 2018.
  * [10] Proceedings of the 2018 USENIX Annual Technical Conference (ATC), Boston, MA, July 2018.
  * [11] Anandtech.  Intel Launches Optane DIMMs Up To 512GB: Apache Pass Is Here!, 2018\.  URL: https://www.anandtech.com/show/12828/intel-launches-optane-dimms-up-to-512gb-apache-pass-is-here.
  * [12] Joy Arulraj, Matthew Perron, and Andrew Pavlo.  Write-behind Logging.  In Proceedings of the 42nd International Conference on Very Large Data Bases (VLDB), New Delhi, India, March 2016.
  * [13] Kumud Bhandari, Dhruva R. Chakrabarti, and Hans-J. Boehm.  Makalu: Fast recoverable allocation of non-volatile memory.  In Proceedings of the 27th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 677–694, Amsterdam, Netherlands, October 2016. ACM.
  * [14] Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, and Roy Tan.  Line-up: a complete and automatic linearizability checker.  In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 330–340, Toronto, Canada, June 2010.
  * [15] Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay İleri, Adam Chlipala, M Frans Kaashoek, and Nickolai Zeldovich.  Verifying a high-performance crash-safe file system using a tree specification.  In Proceedings of the 26th Symposium on Operating Systems Principles, pages 270–286, 2017.
  * [16] Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M Frans Kaashoek, and Nickolai Zeldovich.  Using crash hoare logic for certifying the fscq file system.  In Proceedings of the 25th Symposium on Operating Systems Principles, pages 18–37, 2015.
  * [17] Shimin Chen and Qin Jin.  Persistent B+-trees in Non-volatile Main Memory.  In Proceedings of the 41st International Conference on Very Large Data Bases (VLDB) [8].
  * [18] Jeremy Condit, Edmund B. Nightingale, Christopher Frost, Engin Ipek, Benjamin Lee, Doug Burger, and Derrick Coetzee.  Better i/o through byte-addressable, persistent memory.  In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), Big Sky, MT, October 2009.
  * [19] Tudor David, Aleksandar Dragojevic, Rachid Guerraoui, and Igor Zablotchi.  Log-free concurrent data structures.  In Proceedings of the 2018 USENIX Annual Technical Conference (ATC) [10].
  * [20] Mingkai Dong, Heng Bu, Jifei Yi, Benchao Dong, and Haibo Chen.  Performance and protection in the zofs user-space nvm file system.  In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP ’19, page 478–493, New York, NY, USA, 2019. Association for Computing Machinery.  doi:10.1145/3341301.3359637.
  * [21] Subramanya R. Dulloor, Sanjay Kumar, Anil Keshavamurthy, Philip Lantz, Dheeraj Reddy, Rajesh Sankaran, and Jeff Jackson.  System software for persistent memory.  In Proceedings of the 9th European Conference on Computer Systems (EuroSys), Amsterdam, The Netherlands, April 2014.
  * [22] Dawson Engler, David Yu Chen, Seth Hallem, Andy Chou, and Benjamin Chelf.  Bugs As Deviant Behavior: A General Approach to Inferring Errors in Systems Code.  In Proceedings of the 18th ACM Symposium on Operating Systems Principles (SOSP), pages 57–72, Chateau Lake Louise, Banff, Canada, October 2001\.
  * [23] Jeanne Ferrante, Karl J Ottenstein, and Joe D Warren.  The program dependence graph and its use in optimization.  In Proceedings of the ACM Transactions on Programming Languages and Systems, 1987.
  * [24] Haryadi S. Gunawi, Cindy Rubio-González, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dussea, and Ben Liblit.  EIO: Error handling is occasionally correct.  In Proceedings of the 6th USENIX Conference on File and Storage Technologies (FAST), pages 14:1–14:16, 2008.
  * [25] Mary Jean Harrold, Brian Malloy, and Gregg Rothermel.  Efficient construction of program dependence graphs.  ACM SIGSOFT Software Engineering Notes, 18(3):160–170, 1993.
  * [26] Jian Huang, Karsten Schwan, and Moinuddin K. Qureshi.  NVRAM-aware Logging in Transaction Systems.  [7], pages 389–400.
  * [27] Yihe Huang, Matej Pavlovic, Virendra Marathe, Margo Seltzer, Tim Harris, and Steve Byan.  Closing the Performance Gap Between Volatile and Persistent Key-Value Stores Using Cross-Referencing Logs.  In Proceedings of the 2018 USENIX Annual Technical Conference (ATC) [10].
  * [28] Deukyeon Hwang, Wook-Hee Kim, Youjip Won, and Beomseok Nam.  Endurable Transient Inconsistency in Byte-addressable Persistent B+-tree.  In Proceedings of the 16th USENIX Conference on File and Storage Technologies (FAST), pages 187–200, Oakland, California, USA, February 2018\.
  * [29] INTEL.  Persistent Memory File System, 2015.  URL: https://github.com/linux-pmfs/pmfs.
  * [30] INTEL.  Persistent Memory Development Kit, 2019.  URL: http://pmem.io/.
  * [31] INTEL.  PMDK man page: pmemobjalloc, 2019.  URL: http://pmem.io/pmdk/manpages/linux/v1.5/libpmemobj/pmemobj_alloc.3.
  * [32] Intel.  pmreorder, 2019.  URL: https://pmem.io/pmdk/manpages/linux/master/pmreorder/pmreorder.1.html.
  * [33] INTEL.  PMDK man page: libvmmalloc - general purpose volatile memory allocation library, 2020.  URL: https://pmem.io/vmem/manpages/linux/master/libvmmalloc/libvmmalloc.7.html.
  * [34] INTEL.  PMDK man page: pmemobjopen, 2020.  URL: https://pmem.io/pmdk/manpages/linux/master/libpmemobj/pmemobj_open.3.
  * [35] Intel Corporation.  Intel 64 and IA-32 Architectures Software Developer’s Manual, 2019.  https://software.intel.com/en-us/articles/intel-sdm.
  * [36] Joseph Izraelevitz, Terence Kelly, and Aasheesh Kolli.  Failure-Atomic Persistent Memory Updates via JUSTDO Logging.  In Proceedings of the 21st ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Atlanta, GA, April 2016.
  * [37] Shehbaz Jaffer, Stathis Maneas, Andy Hwang, and Bianca Schroeder.  Evaluating file system reliability on solid state drives.  In Proceedings of the 2019 USENIX Annual Technical Conference (ATC), pages 783–798, Renton, WA, July 2019.
  * [38] Rohan Kadekodi, Se Kwon Lee, Sanidhya Kashyap, Taesoo Kim, Aasheesh Kolli, and Vijay Chidambaram.  Splitfs: reducing software overhead in file systems for persistent memory.  In Proceedings of the 27th ACM Symposium on Operating Systems Principles, pages 494–508, 2019.
  * [39] Samantha Syeda Khairunnesa, Hoan Anh Nguyen, Tien N. Nguyen, and Hridesh Rajan.  Exploiting implicit beliefs to resolve sparse usage problem in usage-based specification mining.  Proc. ACM Program. Lang., 1(OOPSLA), October 2017.  doi:10.1145/3133907.
  * [40] Seulbae Kim, Meng Xu, Sanidhya Kashyap, Jungyeon Yoon, Wen Xu, and Taesoo Kim.  Finding semantic bugs in file systems with an extensible fuzzing framework.  In Proceedings of the 27th ACM Symposium on Operating Systems Principles, pages 147–161, 2019.
  * [41] Ted Kremenek, Paul Twohey, Godmar Back, Andrew Ng, and Dawson Engler.  From uncertainty to belief: Inferring the specification within.  In Proceedings of the 7th symposium on Operating systems design and implementation, pages 161–176, 2006.
  * [42] Philip Lantz, Subramanya Dulloor, Sanjay Kumar, Rajesh Sankaran, and Jeff Jackson.  Yat: A validation framework for persistent memory software.  In Proceedings of the 2014 USENIX Annual Technical Conference (ATC), Philadelphia, PA, June 2014.
  * [43] Se Kwon Lee, K. Hyun Lim, Hyunsub Song, Beomseok Nam, and Sam H. Noh.  WORT: Write Optimal Radix Tree for Persistent Memory Storage Systems.  In Proceedings of the 15th USENIX Conference on File and Storage Technologies (FAST), Santa Clara, California, USA, February–March 2017.
  * [44] Se Kwon Lee, Jayashree Mohan, Sanidhya Kashyap, Taesoo Kim, and Vijay Chidambaram.  RECIPE: Converting Concurrent DRAM Indexes to Persistent-Memory Indexes.  In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), Ontario, Canada, October 2019.
  * [45] Sihang Liu, Korakit Seemakhupt, Yizhou Wei, Thomas Wenisch, Aasheesh Kolli, and Samira Khan.  Cross-Failure Bug Detection in Persistent Memory Programs.  In Proceedings of the 25th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), page 1187–1202, Lausanne, Switzerland, April 2020.
  * [46] Sihang Liu, Yizhou Wei, Jishen Zhao, Aasheesh Kolli, and Samira Khan.  PMTest: A Fast and Flexible Testing Framework for Persistent Memory Programs.  In Proceedings of the 24th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 411–425, Providence, RI, April 2019.
  * [47] Nuno P. Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, and George Varghese.  Checking beliefs in dynamic networks.  In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI), pages 499–512, Oakland, CA, May 2015. USENIX Association.  URL: https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/lopes.
  * [48] Shan Lu, Soyeon Park, Chongfeng Hu, Xiao Ma, Weihang Jiang, Zhenmin Li, Raluca A. Popa, and Yuanyuan Zhou.  Muvi: Automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs.  In Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, SOSP ’07, page 103–116, New York, NY, USA, 2007. Association for Computing Machinery.  doi:10.1145/1294261.1294272.
  * [49] Virendra J. Marathe, Margo Seltzer, Steve Byan, and Tim Harris.  Persistent Memcached: Bringing Legacy Code to Byte-Addressable Persistent Memory.  In Proceedings of the 17th Workshop on Hot Topics in Storage and File Systems, Santa Clara, CA, July 2017.
  * [50] Micro.  3D XPoint Technology, 2019.  URL: https://www.micron.com/products/advanced-solutions/3d-xpoint-technology.
  * [51] Changwoo Min, Sanidhya Kashyap, Byoungyoung Lee, Chengyu Song, and Taesoo Kim.  Cross-checking semantic correctness: The case of finding file system bugs.  In Proceedings of the 25th Symposium on Operating Systems Principles, pages 361–377, 2015.
  * [52] Jayashree Mohan, Ashlie Martinez, Soujanya Ponnapalli, Pandian Raju, and Vijay Chidambaram.  Finding Crash-Consistency Bugs with Bounded Black-Box Crash Testing.  In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI) [9], page 33–50.
  * [53] Moohyeon Nam, Hokeun Cha, Young-ri Choi, Sam H Noh, and Beomseok Nam.  Write-Optimized Dynamic Hashing for Persistent Memory.  In Proceedings of the 17th USENIX Conference on File and Storage Technologies (FAST), Boston, MA, February 2019.
  * [54] Karl J Ottenstein and Linda M Ottenstein.  The program dependence graph in a software development environment.  volume 19, pages 177–184. ACM, 1984.
  * [55] Ismail Oukid, Daniel Booss, Adrien Lespinasse, and Wolfgang Lehner.  On Testing Persistent-memory-based Software.  In Proceedings of the International Workshop on Data Management on New Hardware, pages 5:1–5:7, San Francisco, California, June 2016.
  * [56] Ismail Oukid, Daniel Booss, Adrien Lespinasse, Wolfgang Lehner, Thomas Willhalm, and Grégoire Gomes.  Memory Management Techniques for Large-scale Persistent-main-memory Systems.  In Proceedings of the 43rd International Conference on Very Large Data Bases (VLDB), TU Munich, Germany, August 2017.
  * [57] Ismail Oukid, Johan Lasperas, Anisoara Nica, Thomas Willhalm, and Wolfgang Lehner.  FPTree: A Hybrid SCM-DRAM Persistent and Concurrent B-Tree for Storage Class Memory.  In Proceedings of the 2015 ACM SIGMOD/PODS Conference, San Francisco, CA, USA, June 2016.
  * [58] Michael Pradel and Thomas R. Gross.  Fully automatic and precise detection of thread safety violations.  SIGPLAN Not., 47(6):521–530, June 2012.  doi:10.1145/2345156.2254126.
  * [59] Cindy Rubio-González, Haryadi S. Gunawi, Ben Liblit, Remzi H. Arpaci-Dusseau, and Andrea C. Arpaci-Dusseau.  Error propagation analysis for file systems.  In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 270–280, Dublin, Ireland, June 2009.
  * [60] Swarup Kumar Sahoo, John Criswell, Chase Geigle, and Vikram Adve.  Using likely invariants for automated software fault localization.  In Proceedings of the 18th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 139–152, Houston, TX, March 2013.
  * [61] David Schwalb, Tim Berning, Martin Faust†, Markus Dreseler, and Hasso Plattner†.  nvm malloc: Memory Allocation for NVRAM.  In Proceedings of the 41st International Conference on Very Large Data Bases (VLDB) [8].
  * [62] Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O Myreen.  x86-tso: a rigorous and usable programmer’s model for x86 multiprocessors.  Communications of the ACM, 53(7):89–97, 2010.
  * [63] Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang.  Push-button verification of file systems via crash refinement.  In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 1–16, 2016.
  * [64] Emina Torlak and Satish Chandra.  Effective interprocedural resource leak detection.  In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 1, pages 535–544, 2010.
  * [65] Tianzheng Wang and Ryan Johnson.  Scalable Logging Through Emerging Non-volatile Memory.  In Proceedings of the 40th International Conference on Very Large Data Bases (VLDB) [7].
  * [66] Fei Xia, Dejun Jiang, Jin Xiong, and Ninghui Sun.  HiKV: A Hybrid Index Key-Value Store for DRAM-NVM Memory Systems.  In Proceedings of the 2017 USENIX Annual Technical Conference (ATC), Santa Clara, CA, July 2017.
  * [67] Jian Xu and Steven Swanson.  NOVA: A log-structured file system for hybrid volatile/non-volatile main memories.  In Proceedings of the 14th USENIX Conference on File and Storage Technologies (FAST), Santa Clara, California, USA, February 2016.
  * [68] Wen Xu, Hyungon Moon, Sanidhya Kashyap, Po-Ning Tseng, and Taesoo Kim.  Fuzzing file systems via two-dimensional input space exploration.  In 2019 IEEE Symposium on Security and Privacy (SP), pages 818–834. IEEE, 2019.
  * [69] Junfeng Yang, Can Sar, and Dawson Engler.  explode: A lightweight, general system for finding serious storage system errors.  In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 10–10, Seattle, WA, November 2006.
  * [70] Junfeng Yang, Paul Twohey, and Dawson.  Using model checking to find serious file system errors.  In Proceedings of the 6th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 273–288, San Francisco, CA, December 2004.
  * [71] Insu Yun, Changwoo Min, Xujie Si, Yeongjin Jang, Taesoo Kim, and Mayur Naik.  Apisan: Sanitizing $\\{$API$\\}$ usages through semantic cross-checking.  In 25th USENIX Security Symposium (USENIX Security), pages 363–378, 2016.
  * [72] Pengfei Zuo, Yu Hua, and Jie Wu.  Write-Optimized and High-Performance Hashing Index Scheme for Persistent Memory.  In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI) [9].