Compositional Verification of Relaxed-Memory Program Transformations
Compositional Verification of Relaxed-Memory Program Transformations
复制标题
宽松内存程序转换的组合验证
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Mark
中科院分区：
文献类型：
--
作者：
Mike Dodds;Mark Batty;Alexey Gotsman;Mark
本文是关于在C/C++和Java中使用的公理化松弛内存模型上验证程序转换的。松弛模型对验证程序转换提出了特殊的挑战，因为它们在代码和上下文之间生成了许多额外的交互模式。对于一个被转换的代码块，我们从它在一组有代表性的上下文中的行为定义了一个表示。我们的表示总结了代码块与程序的其余部分通过局部和全局变量的相互作用，并通过微妙的同步效果，由于放松的内存。然后，我们可以通过比较前后代码块的表示来证明转换不会引入新的程序行为。我们的方法是组合的：通过只检查有代表性的上下文，转换被验证为任何上下文。它也是完全抽象的，这意味着任何有效的转换都可以被验证。我们涵盖了C/C++风格内存模型的几个棘手的方面，包括释放-获取操作，顺序一致的围栏和非原子。我们还定义了一个变体，我们的外延是有限的代价是失去充分的抽象。基于这个变体，我们已经实现了一个原型验证工具，并应用它来自动证明和反驳一系列的编译器优化。
This paper is about verifying program transformations on an axiomatic relaxed memory model of the kind used in C/C++ and Java. Relaxed models present particular challenges for verifying program transformations, because they generate many additional modes of interaction between code and context. For a block of code being transformed, we define a denotation from its behaviour in a set of representative contexts. Our denotation summarises interactions of the code block with the rest of the program both through local and global variables, and through subtle synchronisation effects due to relaxed memory. We can then prove that a transformation does not introduce new program behaviours by comparing the denotations of the code block before and after. Our approach is compositional: by examining only representative contexts, transformations are verified for any context. It is also fully abstract, meaning any valid transformation can be verified. We cover several tricky aspects of C/C++-style memory models, including release-acquire operations, sequentially consistent fences, and non-atomics. We also define a variant of our denotation that is finite at the cost of losing full abstraction. Based on this variant, we have implemented a prototype verification tool and applied it to automatically prove and disprove a range of compiler optimisations.
DOI：
10.1145/3009837.3009838
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Wickerson J
通讯作者：
Wickerson J
C/C 并发的库抽象
DOI：
10.1145/2429069.2429099
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M