We address the problem of verifying the reachability problem in programs running 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.

@article{paperbot1165,
  title = {Deciding reachability under persistent x86-TSO},
  author = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Ahmed Bouajjani and K. Narayan Kumar and Prakash Saivasan},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {POPL},
  year = {2021},
  doi = {10.1145/3434337}
}