一句话：证明无界线程数下 k-alternation 有界 eTSO 参数化可达性可判定，并首次用 BQO 良结构系统验证无限状态程序。
论文研究 Intel x86 上线程数任意的并发程序可达性问题，采用 eTSO 形式模型。eTSO 涵盖多种内存类型与非临时写，复杂地结合 TSO 和 PSO 弱内存特性。已有工作证明一般 eTSO 不可判定，但在固定线程数且计算满足 k-alternation 界定时可判定。本文在参数化设置（线程数无界）下证明 k-alternation 有界的 eTSO 可达性可判定。核心困难是证明不能引用线程标识；作者将问题归约到 BQO（Better Quasi Order）域上的良结构系统可达性。该工作首次用基于 BQO 的良结构系统证明无限状态程序验证的可判定性。
We address the reachability problem for concurrent programs with an arbitrary number of threads running over the Intel x-86 architecture. We consider the formal model eTSO for Intel x-86 defined by Raad et al. in POPL 2022. This model takes into account multiple memory types and non-temporal writes, combining in a complex way features in the TSO and PSO weak memory models. In PLDI 2024, Abdulla et al. proved that this problem is undecidable for eTSO in general, but that it is decidable under k -alternation bounding when computations have, for some fixed bound k , at most k alternations of TSO segments (with TSO writes only) and PSO segments (with PSO writes only) for each thread. The proof of this result assumes that the number of threads is fixed, and relies crucially on referring to thread identities. In this paper, we prove the decidability of the k -alternation bounded reachability problem of eTSO in the parametrized setting when the number of threads is a parameter that can be arbitrarily high. The proof is nontrivial as it cannot refer to thread identities, their number being unbounded. We show that it is possible to overcome this difficulty using a novel and quite complex reduction to reachability in well-structured systems on domains that are BQOs (Better Quasi Orders). This is the first time that BQO-based well-structured systems are used to prove the decidability of verification of infinite state programs.
@article{AbdullaABKS26,
title = {Parametrised Verification of Intel-x86 Programs},
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 = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776680}
}