总存储排序的加载缓冲区语义
A Load-Buffer Semantics for Total Store Ordering
AI总结：
本文提出一种等价但更高效的TSO内存模型加载缓冲区语义，简化安全性分析，提升可扩展性，并实现参数化验证，获得更通用的决策算法。
摘要：
我们解决了在总存储排序（TSO）内存模型上运行的并发程序的安全属性验证问题。已知的针对该模型的决策过程基于将存储缓冲区编码为有损通道的复杂编码。这些过程假设进程数量是固定的。然而，通常重要的是以参数化方式证明系统/算法的正确性，即进程数量任意大。在本文中，我们为TSO语义引入了一种替代（但等价）的经典语义，该语义更易于高效的算法验证，并便于扩展到参数化验证。为此，我们采用了一种双重观点，即使用加载缓冲区代替存储缓冲区。信息流现在从内存流向加载缓冲区。我们表明，这种新语义允许（1）大幅简化TSO下的安全性分析，（2）与现有过程相比，在效率和可扩展性方面获得显著提升，以及（3）轻松将决策过程扩展到参数化情况，这使我们能够获得新的可判定性结果，更重要的是，获得一个比有界实例更通用且在实践中更高效的验证算法。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
