Software Verification for Weak Memory via Program Transformation
Software Verification for Weak Memory via Program Transformation
复制标题
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
多处理器实现弱内存模型，但程序验证者通常假设顺序一致性（SC），因此可能会由于弱内存而错过错误。我们建议对验证程序进行合理的改造，使 SC 工具能够执行验证。 记忆力弱。我们提供了针对各种模型（从 x86-TSO 到 Power）和大量验证工具的实验，量化了转换的额外成本，并强调了我们可以大幅减少成本的情况。我们的基准测试包括来自 PostgreSQL 的工作队列管理代码。
Multiprocessors implement weak memory models, but program verifiers often assumeSequential Consistency(SC), and thus may miss bugs due to weak memory. We propose a sound transformation of the program to verify, enabling SC tools to perform verification w.r.t. weak memory. We present experiments for a broad variety of models (from x86-TSO to Power) and a vast range of verification tools, quantify the additional cost of the transformation and highlight the cases when we can drastically reduce it. Our benchmarks include work-queue management code from PostgreSQL.