Property-Driven Fence Insertion using Reorder Bounded Model Checking
This work addresses the problem of optimizing fence insertion for correctness and efficiency in concurrent programming, which is incremental as it builds on existing model-checking methods.
The paper tackles the challenge of automated fence placement in weak memory models to prevent bugs without performance degradation, proposing a property-driven technique that identifies the minimal number of fence locations, resulting in faster performance and solving more benchmark instances than earlier approaches.
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.