Home · ASPLOS 2022 · Compilers & Programming Languages

Yashme: detecting persistency races

Hamed Gorjiara, Guoqing Harry Xu and Brian Demsky

Conference
ASPLOS 2022
Published
2022
Pages
830-845
Citations
18

Persistent memory keeps its contents after a power failure, so programmers write code that flushes data carefully and reasons about what state a crash could leave behind — but this paper (UC Irvine and UCLA) shows they are reasoning about the wrong program, because the C and C++ standards permit a compiler to implement one ordinary assignment as SEVERAL store instructions, or to replace a group of assignments with a memory-copy call, which is invisible in normal programs but means a crash can land in the middle of a single assignment and make half of it permanent; the authors name this new bug class the PERSISTENCY RACE, observe that it involves three events rather than a data race's two and can occur even in single-threaded code, and build Yashme to find them — the hard part is that a crash must land in a tiny window between a store and its flush, so instead of hunting for the perfect crash the tool runs the program ONCE and then reasons about all the alternative executions that would have produced the same post-crash behaviour, detecting races in executions it never actually runs; that trick finds 5 times more races than crashing before every memory fence, and Yashme reported 24 previously unknown races in well-tested code including Intel's PMDK, Memcached and Redis, which the developers confirmed and fixed.

The argument in one glance

  1. Problem

    Crash-consistency reasoning is done on code the machine never runs

    Persistent memory keeps its contents through a power failure, so a program's data structures survive a crash. That creates a hard correctness problem — CRASH CONSISTENCY. A crash can strike at any instant, so a developer must reason about every intermediate state the data structure could be left in, and must place cache-flush instructions to control what actually reaches the persistent device and in what order. All of that reasoning is done on the SOURCE code. But the source code is not what runs. The C and C++ standards assume a program has no data races, and that assumption lets a compiler implement one ordinary assignment using several store instructions, invent extra stores to hold temporary values, or rewrite a group of neighbouring assignments into a memory-copy call that promises no atomicity at all. In ordinary volatile memory none of this is observable. With persistent memory it is.

  2. What people did

    Check that every store is flushed, and in the right order

    A substantial family of tools already tests persistent memory programs. Some let developers annotate ordering rules and check them, some rewrite the binary to count stores that were never made persistent, some use symbolic execution to explore the program before the crash, and some are model checkers that enumerate many possible cache states. They have found many real bugs, and they are the reason libraries such as Intel's PMDK are as solid as they are.

  3. Why it fell short

    Every existing tool assumes a source-level store is atomic

    Those tools all check the same kind of property — was this store flushed, and did these stores reach the device in the required order — which silently assumes that one assignment in the source becomes one indivisible store in the hardware. That assumption is exactly what the compiler is permitted to break. The closest prior work finds loads that read locations not persisted before a failure, but it too treats ordinary stores as effectively atomic and never considers that one could be made PARTIALLY permanent. Tools that inspect the binary can see the individual store instructions, but cannot tell whether two of them came from one source-level assignment, nor which assignments were atomic in the source, so they cannot identify the bug either — and they can give no warning at all about a store that today's compiler leaves intact but a future one may split. A model checker could in principle find these bugs by treating every store as a series of single-byte stores, at the cost of an exponential blow-up in executions to explore.

  4. This paper's idea

    Name the bug class, then expand one execution instead of hunting for the perfect crash

    This paper (UC Irvine and UCLA — Gorjiara, Xu, Demsky) names a new bug class, the PERSISTENCY RACE, and builds Yashme, the first detector for it. A persistency race occurs when code running after a crash reads from a non-atomic store made before the crash that was never guaranteed to be fully persisted. Unlike a data race, which involves two memory operations, it involves THREE events — the racing store, the crash it races against, and the load after the crash that observes the damage — and it can occur in a completely single-threaded program. Detecting one is brutally hard because the crash must land in the narrow window between the store and the flush that persists it, and real programs flush promptly. Yashme's key idea is to stop hunting for that crash. It runs the program once, takes the pre-crash execution it observed, and reasons about every ALTERNATIVE execution that would have produced the same post-crash behaviour — detecting races in executions it never actually runs. That single change finds 5 times more races than crashing before every memory fence, and it uncovered 24 previously unknown races in heavily tested code including PMDK, Memcached and Redis, which the developers confirmed and fixed.

Why this problem is worth solving

Persistent memory changes what a crash means for a program, and the whole discipline built around it rests on an assumption that turns out to be false — so it is worth being precise about the setting first.

PERSISTENT MEMORY (also called non-volatile memory, and sold commercially as Intel Optane) is memory that keeps its contents when power is lost. A program can therefore hold its data structures directly in memory and expect them to still be there after a power failure, with no separate save step. That promise creates a hard obligation called CRASH CONSISTENCY — because a crash can occur at any instant, the developer must ensure that every state the crash could leave behind is one the recovery code can make sense of. The difficulty is that writes do not reach the persistent device when the program performs them. They land first in the processor cache, which is VOLATILE, so anything still sitting there when power fails is simply lost, and the hardware writes cache lines back at unpredictable moments when it needs the space. To control this, developers use explicit CACHE FLUSH instructions that force a specific cache line out to persistent memory, plus fences that constrain the order. Getting this right means reasoning carefully about which stores have definitely persisted at every point where a crash could happen
— and that reasoning is performed against the source code the developer wrote.

The problem is that the source code is not the program that executes. A compiler is granted freedoms that ordinarily nobody can observe.

A NON-ATOMIC STORE is an ordinary assignment in C or C++ — writing a field, setting an integer — as opposed to an explicitly ATOMIC operation. The language standards assume programs are free of data races, which means no other thread may observe a non-atomic store until the program performs a synchronization operation. That assumption gives the compiler enormous freedom. It may implement a single non-atomic store using SEVERAL store instructions, which is called STORE TEARING (on one processor family a 64-bit assignment is compiled into a pair of separate stores). It may INVENT stores that the program never wrote, for instance to park a temporary value in memory when it runs out of registers. And most commonly, it rewrites a group of neighbouring assignments into a call to a memory-copy or memory-set routine, which guarantees no atomicity whatsoever. In ordinary volatile memory none of this can be detected, because by the time another thread is allowed to look, the writes are complete. With persistent memory a crash can occur between the pieces, freezing a half-written value permanently
. That is the collision at the centre of this paper.

What people did before, and where it broke

  • Annotation-based checkers. Developers mark ordering rules and the tool verifies them against the execution. Effective, but the developer must know and state the property, and the properties expressible are about flushing and ordering, not about a single store being split apart.
  • Binary-rewriting checkers. Tools that instrument the compiled program count stores never made persistent and detect overwrites. They see the real instructions, but cannot tell whether two adjacent stores came from one source-level assignment or two, nor which assignments were atomic in the source, so they cannot identify the bug.
  • Symbolic execution of the pre-crash program. One tool explores the program before the crash and tracks the state of each persistent object and cache line. But a persistency race is a relationship BETWEEN the pre-crash and post-crash executions, and a tool that only explores the pre-crash side cannot see it.
  • Cross-failure race detection. The closest prior work finds loads that read locations which were not persisted before the failure. Genuinely related, but it models ordinary stores as effectively atomic, does not model the effect of cache coherence, and examines only the one execution it was given.
  • Model checkers and fuzzers for persistent memory. These explore many cache states and crash points automatically, and are the strongest baseline. But whether they observe a race still depends on the thread schedule they happen to explore, and finding this bug requires the crash to land in a window that a different schedule simply closes.
  • The gap. Every one of these validates that stores were flushed or ordered, which presumes one source assignment equals one indivisible hardware store. That presumption is precisely what the compiler may break, so none of them could detect this class of bug at all. That is the gap Yashme fills.

How Yashme finds a bug that almost never manifests

Simulate the real persistency model, define the race, then expand one execution into many

  1. Developers reason about stores the machine never performs

    Crash-consistency arguments are made about source-level assignments, but the compiler may split one assignment into several store instructions, invent extra stores, or turn a group of assignments into a memory-copy call. A crash can then make one assignment partially permanent, and the code that runs after the crash reads a value stitched together from two different writes.

  2. Simulate the processor persistency model faithfully new

    Yashme instruments the compiler intermediate representation so the program calls into a library that simulates the formal x86 persistency semantics — per-core store buffers, a volatile cache written back at unpredictable times, and the precise reordering rules of each flush instruction. Bug hunting requires modelling what the hardware may actually do, not what the manual suggests.

  3. Define the race with four precise conditions new

    A load after the crash that reads a pre-crash store is a persistency race when the store is non-atomic, no later atomic release store to the same cache line was read first, no flush instruction of that cache line happened after the store, and no write-back plus fence pair did either. Each condition rules out one way the store could have been guaranteed complete.

  4. Track what was genuinely persisted new

    Two maps do the accounting. One records, for each store, the flush that came after it, so a flushed store is never reported. The other records, for each cache line, the earliest point it could have been written back — because if the post-crash code reads a LATER atomic store to the same line, cache coherence guarantees the earlier store completed first.

  5. Expand the observed execution into all consistent ones new

    This is the key move. Rather than hunting for a crash inside the narrow window, Yashme takes the execution it observed and computes every prefix of it that is still consistent with the post-crash behaviour. If some consistent prefix would not have executed a given flush, that flush is ignored when checking for races — because a real execution exists that skips it and produces the same post-crash result.

  6. Report the racing variable, and fix it almost for free new

    Each report names the specific field whose store races, which is what a developer needs to reason about the scenario. The fix is to declare that field atomic and store it with release ordering — on this processor family that compiles to the very same move instruction, so it costs nothing at run time, but the compiler is now forbidden to tear it.

Built on an existing constraint-based execution engine for persistent memory, with a full simulation of the formal x86 persistency semantics. Yashme runs in an exhaustive model-checking mode for small programs and a random mode for large ones.

The idea

Name the bug class before trying to find it. The paper’s first contribution is not an algorithm but a definition. Existing tools all asked “was this store flushed, and were these stores ordered correctly?”, which quietly assumes a source-level assignment is indivisible. By naming the persistency race and defining it precisely — a post-crash load reading a non-atomic pre-crash store that four separate conditions confirm was never guaranteed complete — the authors make visible a whole category of bug that the previous question could not express. It is also a genuinely different shape of bug: a data race is two memory operations racing with each other, while a persistency race has THREE participants, with the crash itself as one of them, which is why it occurs even in single-threaded programs. Recognising that the abstraction everyone reasons with has quietly stopped matching the substrate underneath is the same the-ground-moved-under-the-assumption insight covered elsewhere on this site, in the pages where a design that was correct on the previous generation of hardware becomes wrong on the new one, and in the memory-safety pages where a guarantee developers relied on turns out to hold only under conditions that no longer apply.

When the event you need is too rare to catch, stop trying to catch it. The detection problem looks hopeless stated directly. To witness the race, the crash must strike between the store and the flush that persists it, and real persistent memory programs flush promptly, so that window is minuscule. Injecting crashes everywhere and exploring every thread schedule is impractical. Yashme inverts the problem: it runs the program once, keeps the execution it observed, and then reasons about the whole SET of alternative executions that would have yielded the same post-crash behaviour — checking them for races without ever running them. Reasoning over a set of possibilities simultaneously, rather than enumerating them by execution, is the same move covered elsewhere on this site in the compiler super-optimizer that keeps every equivalent version of a program in one structure instead of committing to a search path, and in the pages that replace brute-force sampling with an analysis of what could occur. One real execution becomes evidence about many.

Judge the program against the contract, not against today’s binary. A tempting objection is that the compiler in front of you might not actually tear that store, so the bug is theoretical. The paper rejects this, and the argument is the most practically important thing in it. The optimizations are all standards-compliant, so whether a race manifests depends on the compiler version, the target architecture, the library implementation, and even unrelated edits such as adding a field to a structure and changing an alignment. A latent race can therefore be woken by a routine compiler upgrade, in recovery code, in a storage system, causing total data loss. So Yashme reports what the language PERMITS rather than what one binary happens to do. Validating against the specification instead of the current implementation is the same test-the-contract-not-the-artefact discipline covered elsewhere on this site, and Intel’s own persistent memory developers make the point in the paper — they validate compiled binaries extensively, but say plainly that they do not want to depend on compiler-defined behaviour if they can avoid it.

Tearing a key in a persistent hash table

One assignment, split by the compiler, frozen by a crash

The paper's own example from a persistent-memory hash table. Numbers from the evaluation.

Step 1 of 5

The data structure's careful design

A persistent hash table inserts an entry by locking a slot with an atomic compare-and-swap, writing the value field, executing a memory fence, and then writing the key field. Writing the key is what COMMITS the insertion, and the design relies on key and value sharing a cache line so the value cannot reach persistent memory after the key.

the caller flushes both stores to persistent memory afterwards
the reasoning is careful and correct at the level of source-code assignments

Why it works

  • The compiler may split one source assignment into several stores → with persistent memory a crash can land between them and freeze the result → a post-crash load can read bytes mixed from two different writes, which no flush-and-order checker was even asking about.
  • A persistency race needs the crash inside a tiny window between store and flush → Yashme derives, from one observed execution, every prefix still consistent with the post-crash behaviour → races are detected in executions that were never run, so the narrow window stops being the bottleneck.
  • If a consistent prefix exists that never performed a given flush → then a real execution exists producing the same post-crash result without it → the flush can be soundly ignored when checking, which is exactly what widens the detection window by a factor of 5.
  • Cache coherence orders stores to one cache line → so if the post-crash code reads a later atomic store on that line, every earlier store to it must have completed → tracking the earliest possible write-back per cache line eliminates those false reports without extra execution.
  • The dangerous optimizations are standards-compliant → so a race that is dormant under today’s compiler can be woken by an upgrade or an unrelated edit → reporting what the language permits, rather than what one binary does, catches the bug before it detonates.

What it costs (trade-offs and scope)

  • It is a dynamic tool, so it only sees what it runs. Yashme reports races in executions derived from ones it observed, driven by test programs the authors wrote or adapted. Code paths the tests never reach are not checked, and it offers no proof that a program is race-free.
  • The exhaustive mode does not scale. Model-checking mode explores all executions and suits small programs; the larger real systems had to be run in random mode instead, which trades completeness for tractability.
  • It models one persistency model, in simulation. The implementation simulates the formal x86 semantics. The authors argue persistency races are a general phenomenon on other persistency models, but the tool as built targets this one, and results come from a simulation of the memory system rather than from failing real hardware.
  • Reports need human judgement. Race reports were deduplicated by hand and inspected manually, since one variable can appear in several buggy scenarios. And some real races were in a memory allocator already known to be crash-inconsistent, which the developers will not fix because the component is being replaced — genuine findings, but not actionable ones.
  • The bugs are real but their manifestation is conditional. Whether a given race actually tears depends on the compiler, the architecture, the library and field alignment. That conditionality is the paper’s argument FOR fixing them, but it does mean a report is not a demonstration of present-day failure, and a developer must accept a specification-level argument.

The evaluation

Yashme was evaluated on an Ubuntu machine with a 4-core Intel Xeon processor, using two compilers, against persistent-memory systems already used to evaluate earlier bug-finding tools — a suite of persistent indexes, a cache-conscious hash table, a fault-tolerant tree, Intel’s PMDK library through its example data structures, the persistent-memory ports of Memcached, and Redis. The comparison is against every prior class of tool (none of which can detect this bug class at all), and internally against the same detector run without the prefix-expansion idea.

Detecting crash-consistency bugs in persistent memory

PropertyFlush-and-order checkersCrash injection at every fenceYashme (this work)
Treats a source store as
Can find persistency races
Executions examined
Races found per run
Cost
Yashme found 24 previously unreported persistency races — 19 in persistent index data structures and 5 in PMDK, Memcached and Redis — in code that prior tools had already been run against. Developers of the index suite and of persistent Memcached confirmed the reports and published fixes; PMDK's developers confirmed the one reported there.Underlined values explain themselves when clicked.

Check yourself

Check your understanding

  1. 1. A persistency race can occur in a completely single-threaded program, unlike a data race. Predict what makes that possible.

  2. 2. To witness a persistency race the crash must land between a store and the flush that persists it, and real programs flush promptly. Predict how Yashme detects these races anyway.

  3. 3. Someone objects that their current compiler does not actually tear the store, so the reported race is only theoretical. Predict how the paper answers.

  4. 4. Yashme tracks, for each cache line, the earliest point it could have been written back to persistent memory. Predict why that map is needed.

Sources

Related papers on Compilers & Programming Languages

See all 162 →