一句话：提出 TSO 的 load-buffer 等价语义，简化安全性验证并支持参数化验证与高效算法。
论文研究 Total Store Ordering (TSO) 内存模型下并发程序的安全性验证。已有判定过程通常将 store buffer 编码为有损通道，并假设进程数固定，难以进行参数化验证。作者提出一种与经典 TSO 等价的 load-buffer 语义：信息从内存流向 load buffer，而非从进程写入 store buffer。基于该语义，安全性分析被大幅简化，验证效率和可扩展性显著优于现有过程，并能自然扩展到进程数任意大的参数化情形，从而得到新的可判定性结果和比有界实例更通用、更高效的验证算法。
We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove the correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes. In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO semantics that is more amenable to efficient algorithmic verification and for the extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows obtaining a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.Comment: Logic in computer science
@article{paperbot431,
title = {A Load-Buffer Semantics for Total Store Ordering},
author = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Ahmed Bouajjani and Tuan Phong Ngo},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:9)2018}
}