使用重新排序有界模型检验的属性驱动的栅栏插入
Property-Driven Fence Insertion using Reorder Bounded Model Checking
摘要：
现代体系结构提供的内存一致性保证比顺序一致性要弱。这些较弱的保证允许程序表现出程序语句似乎已经按照程序顺序执行的行为。幸运的是，如果需要，现代体系结构提供了内存屏障（栅栏）来强制执行一对语句之间的程序顺序。由于弱内存模型的复杂语义，即使对于有经验的程序员来说，栅栏的放置也是一个挑战。栅栏太少会导致bug，而过度使用栅栏会导致性能下降。这促使了围栏的自动放置。恢复程序中顺序一致性的工具可能会插入比程序正确所需的更多的栅栏。因此，我们提出了一个属性驱动的技术，引入“重新排序有界的探索”，以确定最小数量的程序位置围栏放置。我们在CBMC之上实现了我们的技术;然而，原则上，我们的技术足够通用，可以用于任何模型检查器。我们的实验结果表明，我们的技术是更快，解决更多的相关基准的实例相比，早期的方法。
英文摘要：
Modern architectures provide weaker memory consistency guarantees than sequential consistency. These weaker guarantees allow programs to exhibit behaviours where the program statements appear to have executed out of program order. Fortunately, modern architectures provide memory barriers (fences) to enforce the program order between a pair of statements if needed. Due to the intricate semantics of weak memory models, the placement of fences is challenging even for experienced programmers. Too few fences lead to bugs whereas overuse of fences results in performance degradation. This motivates automated placement of fences. Tools that restore sequential consistency in the program may insert more fences than necessary for the program to be correct. Therefore, we propose a property-driven technique that introduces "reorder-bounded exploration" to identify the smallest number of program locations for fence placement. We implemented our technique on top of CBMC; however, in principle, our technique is generic enough to be used with any model checker. Our experimental results show that our technique is faster and solves more instances of relevant benchmarks as compared to earlier approaches.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
