一句话：研究 Intel-x86 持久性语义下的可达性，给出持久性归约、一致性不可判定性与有界交替可判定性结果。
本文研究 Raad 等人提出的 Intel-x86 完整语义（融合 SC、TSO、PSO 以刻画持久性指令集）下的可达性问题，其一致性与持久性均涉及无界操作重排。作者首先证明：该模型的可达性可归约到不含持久性组件的模型，方法是构造有限状态协议与程序并行运行来模拟持久性语义。其次，证明即使不考虑崩溃与持久性，Intel-x86 一致性模型下的可达性也不可判定；当一个线程同时使用 TSO 变量和两个 PSO 变量时即不可判定。最后，对 TSO 写回与 PSO 非临时写之间交替次数给定任意固定界，可达性问题可判定，从而给出可用于缺陷发现的有界近似分析参数化方案。
The full semantics of the Intel-x86 architecture has been defined by Raad et al in POPL 2022, extending the earlier formalization based on the TSO memory model incorporating persistency. This new semantics involves an intricate combination of the SC, TSO, and PSO models to account for the diverse features of the enlarged instruction set. In this paper we investigate the reachability problem under this semantics, including both its consistency and persistency aspects each of which requires reasoning about unbounded operation reorderings. Our first contribution is to show that reachability under this model can be reduced to reachability under a model without the persistency component. This is achieved by showing that the persistency semantics can be simulated by a finite-state protocol running in parallel with the program. Our second contribution is to prove that reachability under the consistency model of Intel-x86 (even without crashes and persistency) is undecidable. Undecidability is obtained as soon as one thread in the program is allowed to use both TSO variables and two PSO variables. The third contribution is showing that for any fixed bound on the alternation between TSO writes (write-backs), and PSO writes (non-temporal writes), the reachability problem is decidable. This defines a complete parametrized schema for under-approximate analysis that can be used for bug finding.
@article{AbdullaABKS24,
title = {Verification under Intel-x86 with Persistency},
author = {Parosh Abdulla and Mohamed Faouzi Atig and Ahmed Bouajjani and K. Narayan Kumar and Prakash Saivasan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656425}
}