论文标题
C11内存模型下的围栏合成
Fence Synthesis under the C11 Memory Model
论文作者
论文摘要
C/C ++ 11（C11）标准提供了在内存访问操作上保证订购的范围。此类订购的组合在制定正确有效的弱记忆程序方面构成了挑战。一种常见的解决方案，以排除违反正确性规范的程序结果是使用C11同步遗迹，该文件在程序事件上建立订单。挑战在于选择（i）恢复输入程序的正确性的围栏的组合，（ii）对效率的影响尽可能少（即最小的最弱围栏）。这个问题是最佳的围栏合成问题，是直线程序的NP-HARD。在这项工作中，我们为C11程序提出了第一个名为Fensinging的栅栏合成技术，并显示了其最佳性。我们还提出了一种称为ffensying的近乎最佳有效的替代方案。我们证明了弹性的最佳性和ffensing的健全性，并提出了两种技术的实现。最后，我们对比两种技术的性能，并在经验上证明了效率的有效性。
The C/C++11 (C11) standard offers a spectrum of ordering guarantees on memory access operations. The combinations of such orderings pose a challenge in developing correct and efficient weak memory programs. A common solution to preclude those program outcomes that violate the correctness specification is using C11 synchronization-fences, which establish ordering on program events. The challenge is in choosing a combination of fences that (i) restores the correctness of the input program, with (ii) as little impact on efficiency as possible (i.e., the smallest set of weakest fences). This problem is the optimal fence synthesis problem and is NP-hard for straight-line programs. In this work, we propose the first fence synthesis technique for C11 programs called FenSying and show its optimality. We additionally propose a near-optimal efficient alternative called fFenSying. We prove the optimality of FenSying and the soundness of fFenSying and present an implementation of both techniques. Finally, we contrast the performance of the two techniques and empirically demonstrate fFenSyings effectiveness.
