TSO to SC via Symbolic Execution
TSO to SC via Symbolic Execution
复制标题
通过符号执行从 TSO 到 SC
DOI：
10.1007/978-3-319-26287-1_7
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Oleg Travkin
中科院分区：
文献类型：
--
作者：
Heike Wehrheim;Oleg Travkin
配备了弱内存模型(如TSO)的现代多核处理器的执行-由于存储缓冲区-似乎重新排列了程序操作的顺序。因此，它们偏离了通常认为的顺序一致性(SC)语义。因此，并发程序的分析技术需要考虑重新排序。对于TSO，这通常是通过显式建模存储缓冲区来实现的。本文提出了一种方法，将并发程序(带隔离或无写循环)的TSO验证简化为SC验证，从而能够重用标准验证工具。为此，我们将给定的程序转换为SC-语义(互模拟-)等价于TSO-语义OFP的新程序。然而，转换仅针对存储缓冲区内容通过符号执行OFP进行。从这样获得的抽象OFP中，我们生成SC程序，然后可以将其作为标准分析工具的目标。
Modern multi-core processors equipped with weak memory models like TSO exhibit executions which – due to store buffers – seemingly reorder program operations. Thus, they deviate from the commonly assumedsequential consistency(SC) semantics. Analysis techniques for concurrent programs consequently need to take reorderings into account. For TSO, this is often accomplished by explicitly modelling store buffers.In this paper, we present an approach for reducing TSO-verification of concurrent programs (with fenced or write-free loops) to SC-verification, thereby being able to reuse standard verification tools. To this end, we transform a given programPinto a new programwhose SC-semantics is (bisimulation-) equivalent to the TSO-semantics ofP. The transformation proceeds via a symbolic execution ofP, however, only with respect to store buffer contents. Out of the thus obtained abstraction ofP, we generate the SC programwhich can then be the target of standard analysis tools.
登录
查看更多内容
从总存储顺序到顺序一致性：实用的归约定理
DOI：
10.1007/978-3-642-14052-5_28
发表时间：
2010
期刊：
Physical review. E
影响因子：
--
作者：
Ernie Cohen;Norbert Schirmer
通讯作者：
Norbert Schirmer
一种基于自动机的在宽松内存模型上验证程序的符号方法
DOI：
10.1007/978-3-642-16164-3_16
发表时间：
2010
期刊：
bioRxiv
影响因子：
--
作者：
A. Linden;P. Wolper
通讯作者：
P. Wolper
在机械化线性化证明中处理 TSO
DOI：
10.1007/978-3-319-13338-6_11
发表时间：
2014
期刊：
Concurrency and Computation: Practice and Experience
影响因子：
--
作者：
Oleg Travkin;H. Wehrheim
通讯作者：
H. Wehrheim
DOI：
10.1002/cpe.837
发表时间：
2005-04
期刊：
Concurrency and Computation: Practice and Experience
影响因子：
--
作者：
Yue Yang;G. Gopalakrishnan;G. Lindstrom
通讯作者：
Yue Yang;G. Gopalakrishnan;G. Lindstrom
DOI：
10.1007/978-3-642-37036-6_28
发表时间：
2012-07
期刊：
--
影响因子：
--
作者：
J. Alglave;D. Kroening;Vincent Nimal;Michael Tautschnig
通讯作者：
J. Alglave;D. Kroening;Vincent Nimal;Michael Tautschnig