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.
翻译:C/C+/11 (C11) 标准为内存存存取操作提供了一系列的定序保证。 这种定购组合对开发正确而高效的内存程序构成挑战。 防止那些违反正确性规格的方案结果的一个共同解决办法是使用C11同步栅栏,对程序事件进行定序。 挑战在于选择各种围栏组合,以便(一) 恢复输入程序的正确性,(二) 对效率的影响尽可能小(即最小的最弱的栅栏) 。 这个问题是最佳的围栏合成问题,对直线程序来说是硬的。 在这项工作中,我们为C11 程序提出了第一个称为“ enSying” 的围栏合成技术,并展示了它的最佳性。 我们还提出了一种近于最佳的、有效的替代方法,即“fenSying”。 我们证明了FenSying的优化性,FenSying的健全性,并展示了这两种技术的实施。 最后,我们比较了两种技术的性能,并用经验展示了FenSyings 的效能。