The Benefits of Duality in Verifying Concurrent Programs under TSO
The Benefits of Duality in Verifying Concurrent Programs under TSO
复制标题
DOI：
10.4230/lipics.concur.2016.5
复制
发表时间：
2017-01
期刊：
影响因子：
--
通讯作者：
P. Abdulla;M. Atig;A. Bouajjani;Ngo Tuan Phong
中科院分区：
文献类型：
--
作者：
P. Abdulla;M. Atig;A. Bouajjani;Ngo Tuan Phong
我们解决了验证通过TSO内存模型运行的并发程序的安全属性的问题。该模型的已知决策程序基于商店缓冲区的复杂编码作为有损通道。这些过程假定过程的数量是固定的。但是，一般来说，重要的是要以任意大量过程的参数方式证明系统/算法的正确性。在本文中，我们向TSO模型的经典语义介绍了一种替代性（但同等的）语义，该语义更适合有效算法验证，并扩展到参数验证。为此，我们采用了双重视图，其中使用负载缓冲区而不是商店缓冲区。信息流现在从内存到加载缓冲区。我们表明，这种新语义允许（1）与现有过程相比，（2）在TSO下的安全性分析大大简化，以获得效率和可伸缩性的巨大提高，并且（3）轻松将决策程序扩展到参数案例。 ，这允许获得新的可确定性结果，更重要的是，一种验证算法比在有限实例的实例上更一般，更有效。
We address the problem of verifying safety properties of concurrent programs running over the 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 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 model that is more amenable for efficient algorithmic verification and for 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 to obtain 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.