An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models
An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models
复制标题
一种基于自动机的在宽松内存模型上验证程序的符号方法
DOI：
10.1007/978-3-642-16164-3_16
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
P. Wolper
中科院分区：
文献类型：
--
作者：
A. Linden;P. Wolper
本文解决了为现代处理器中实现的轻松记忆模型验证程序的问题。具体而言，它考虑了TSO（总商店订单）放松，这对应于商店缓冲区的使用。提出的方法通过使用有限自动机象征性地表示存储缓冲区的可能内容来进行。然后，将，加载和提交操作对应于这些有限自动机的操作。
这种方法的优点是它在（潜在的无限）缓冲区内容集上运行，而不是在单个缓冲区配置上运行。这提供了一种方法来驯服可能的缓冲型配置数量的爆炸，同时保留了分析的全部一般性。因此，甚至可以检查以异常方式利用放松记忆模型的设计。已经使用实验实现来验证该方法的可行性。
This paper addresses the problem of verifying programs for the relaxed memory models implemented in modern processors. Specifically, it considers the TSO (Total Store Order) relaxation, which corresponds to the use of store buffers. The proposed approach proceeds by using finite automata to symbolically represent the possible contents of the store buffers. Store, load and commit operations then correspond to operations on these finite automata.
The advantage of this approach is that it operates on (potentially infinite) sets of buffer contents, rather than on individual buffer configurations. This provides a way to tame the explosion of the number of possible buffer configurations, while preserving the full generality of the analysis. It is thus possible to check even designs that exploit the relaxed memory model in unusual ways. An experimental implementation has been used to validate the feasibility of the approach.