一句话：证明持久 x86-TSO（Px86）模型下程序可达性问题是可判定的，并给出等价的良结构系统模型。
本文研究在 Raad 等人于 POPL'20 提出的持久 Intel x86 形式模型 Px86 下运行的程序的可达性问题。作者证明该问题可判定：通过深入分析 Px86 各组件及其交互性质，构造出一个与 Px86 等价的新形式模型，并论证该模型构成良结构系统（well-structured system），从而可借助良结构迁移系统的判定理论得到可达性可判定性。该工作为持久内存并发程序的验证提供了理论基础，关键结果是 Px86 可达性可判定，而非提出具体工具或实验评估。
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}
}