OSDI '20 - AGAMOTTO: How Persistent Is Your Persistent Memory Application?

Why It Matters

By automating detection of durability and performance bugs without code changes, Agamoto lowers the barrier to reliable persistent‑memory deployment, protecting data integrity and enabling faster, more efficient applications.

Key Takeaways

• Persistent memory needs explicit flush and fence for durability.
• Missing or redundant persistence instructions cause correctness and performance bugs.
• Agamoto uses symbolic execution to detect bugs without source modifications.
• Study found 90% of bugs follow two application‑independent patterns.
• Agamoto uncovered 84 new bugs, outperforming prior tools dramatically.

Summary

The presentation introduced Agamoto, a symbolic‑execution framework designed to automatically uncover persistency bugs in applications that use Intel’s emerging persistent‑memory (PM) technology. By mapping PM directly into a process’s address space, developers can avoid file‑system overhead, but they must also manage explicit flush and fence instructions to guarantee durability.

A survey of 63 real‑world PM bugs revealed two dominant, application‑independent patterns: missing flush/fence sequences (≈80% of cases) and redundant durability calls (≈11%). Leveraging these patterns, Agamoto augments the CLE symbolic executor with a three‑state PM model (clean, dirty, flushed) and injects bug‑oracles that fire on illegal state transitions, eliminating the need for hand‑written test suites or source‑code changes.

The tool demonstrated its efficacy by discovering 84 previously unknown bugs across a range of open‑source PM libraries, dwarfing the three to four bugs found by competing tools such as PM‑Test and XF‑Detector. Developers confirmed many of the findings, and a follow‑up study showed that fixing identified performance‑related bugs could boost application throughput by up to 47%.

Agamoto’s high‑coverage, low‑overhead approach promises to accelerate the adoption of persistent memory by providing developers with a turnkey debugging solution that catches both correctness and performance defects, reducing data‑loss risk and unlocking the technology’s latency‑close, non‑volatile benefits.

Original Description

AGAMOTTO: How Persistent is your Persistent Memory Application?

Ian Neal, Ben Reeves, Ben Stoler, and Andrew Quinn, University of Michigan; Youngjin Kwon, KAIST; Simon Peter, University of Texas at Austin; Baris Kasikci, University of Michigan

Persistent Memory (PM) can be used by applications to directly and quickly persist any data structure, without the overhead of a file system. However, writing PM applications that are simultaneously correct and efficient is challenging. As a result, PM applications contain correctness and performance bugs. Prior work on testing PM systems has low bug coverage as it relies primarily on extensive test cases and developer annotations.

In this paper we aim to build a system for more thoroughly testing PM applications. We inform our design using a detailed study of 63 bugs from popular PM projects. We identify two application-independent patterns of PM misuse which account for the majority of bugs in our study and can be detected automatically. The remaining application-specific bugs can be detected using compact custom oracles provided by developers.

We then present AGAMOTTO, a generic and extensible system for discovering misuse of persistent memory in PM applications. Unlike existing tools that rely on extensive test cases or annotations, AGAMOTTO symbolically executes PM systems to discover bugs. AGAMOTTO introduces a new symbolic memory model that is able to represent whether or not PM state has been made persistent. AGAMOTTO uses a state space exploration algorithm, which drives symbolic execution towards program locations that are susceptible to persistency bugs. AGAMOTTO has so far identified 84 new bugs in 5 different PM applications and frameworks while incurring no false positives.

View the full OSDI '20 program at https://www.usenix.org/conference/osdi20/technical-sessions