Non-Volatile Random Access Memories, or Persistent Memories (PM), is an emerging technology offering both efficiency of DRAMs and persistency of data across failures. However, while they allow recovering some data, recovery states are not always consistent, and programmers must provide adequate recovery code ensuring the level of consistency they need. This task is hard and error prone, and therefore, being able to reason formally about concurrent programs running on PMs and verifying their correctness is extremely important.

In this paper, we address the problem of verifying the reachability problem in programs under the formal model Px86 defined recently by Raad et al. in POPL’20 for the persistent Intel x86 architecture. We prove that this problem is decidable. To achieve that, we provide a new formal model that is equivalent to Px86 and that has the feature of being a well-structured system. Deriving this new model is the result of a deep investigation of the properties of Px86 and the interplay of its components.