C11内存模型下的栅栏综合
分布式、并行与集群计算
2022-08-03 v2 编程语言
摘要
C/C++11（C11）标准对内存访问操作提供了一系列排序保证。此类排序的组合给开发正确且高效的弱内存程序带来挑战。排除那些违反正确性规约的程序结果的一种常见方案是使用C11同步栅栏，其在程序事件上建立排序。挑战在于选择一组栅栏，使得（i）恢复输入程序的正确性，且（ii）对效率影响尽可能小（即最弱栅栏的最小集合）。该问题即最优栅栏综合问题，对直线程序是NP难的。在本文中，我们提出首个针对C11程序的栅栏综合技术FenSying并证明其最优性。我们还提出一种近最优的高效替代方案fFenSying。我们证明了FenSying的最优性与fFenSying的可靠性，并给出了两种技术的实现。最后，我们对比了两种技术的性能并实证展示了fFenSying的有效性。
引用
@article{arxiv.2208.00285,
title = {Fence Synthesis under the C11 Memory Model},
author = {Sanjana Singh and Divyanjali Sharma and Ishita Jaju and Subodh Sharma},
journal= {arXiv preprint arXiv:2208.00285},
year = {2022}
}