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

TL;DR

This paper explores the challenges of empirically validating memory persistency models on real hardware, revealing discrepancies between formal specifications and actual machine behavior, and highlighting the difficulties in verification methods.

Contribution

It introduces a novel approach using bus-intercept hardware for validation and uncovers significant gaps between formal models and real-world machine behavior.

Findings

Intel-x86 architecture resists validation with current methods

Arm machines do not fully adhere to formal persistency models

Validation of persistency guarantees remains a significant challenge

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.