Lost in Interpretation: Navigating Challenges in Validating Persistency Models Amid Vague Specs and Stubborn Machines, All with a Sense of Humour

TL;DR

This work tackles the challenge of empirically validating memory persistency models Px86 and PArm on real machines, where traditional litmus testing cannot observe when data becomes persistent. It introduces an interposer-based approach using the FS2800 DDR Detective to log memory-bus writes and infer persist order, applied to Intel-x86 and Arm systems. Across both architectures, the study finds evidence of out-of-order writes entering memory, but conclusions are constrained by hardware specifics: Intel’s battery-backed WPQ obscures true persist order, while an Arm system exhibited loopholes and gaps in persistency guarantees. The results underscore the difficulty of independent vendor validation and motivate further hardware- and platform-specific validation methods, with future work targeting Arm platforms and embedded SOCs using alternative logging approaches. Overall, the paper demonstrates the feasibility of empirical persistency validation while revealing fundamental obstacles and a need for clarified Arm workflows and hardware that truly support durable, order-guaranteed persists.

Abstract

Memory persistency models provide a foundation for persistent programming by specifying which (and when) writes to non-volatile memory (NVM) become persistent. Memory persistency models for the Intel-x86 and Arm architectures have been formalised, but not empirically validated against real machines. Traditional validation methods %such as %extensive litmus testing used for memory \emph{consistency} models do not straightforwardly apply because a test program cannot directly observe when its data has become persistent: it cannot distinguish between reading data from a volatile cache and from NVM. We investigate addressing this challenge using a commercial off-the-shelf device that intercepts data on the memory bus and logs all writes in the order they reach the memory. Using this technique we conducted a litmus-testing campaign aimed at empirically validating the persistency guarantees of Intel-x86 and Arm machines. We observed writes propagating to memory out of order, and took steps to build confidence that these observations were not merely artefacts of our testing setup. However, despite gaining high confidence in the trustworthiness of our observation method, our conclusions remain largely negative. We found that the Intel-x86 architecture is not amenable to our approach, and on consulting Intel engineers discovered that there are currently no reliable methods of validating their persistency guarantees. For Arm, we found that even a machine recommended to us by a persistency expert at Arm did not match the formal Arm persistency model, due to a loophole in the specification.

Figures (11)

• Figure 1: In our empirical setup the interposer sits between the DIMM and the DIMM socket on the motherboard, and the attached DDR Detective logs specified memory accesses.
• Figure 2: Persistency in a typical Intel-x86 system
• Figure 3: Persistency in a typical Arm system
• Figure 4: DRAM addressing and spatial organisation
• Figure 5: Our flow for validating persistency models; a colour nested inside another denotes an embedded program within outer code; a hexagon allows the flow to continue if the condition inside is true.