Property-Driven Fence Insertion using Reorder Bounded Model Checking

TL;DR

This paper presents a property-driven, reorder-bounded model checking technique for automated fence insertion in weak memory models, optimizing for minimal fence placement to ensure correctness without performance loss.

Contribution

It introduces a novel reorder-bounded exploration method for minimal fence placement, implemented on CBMC, improving efficiency and effectiveness over previous approaches.

Findings

Faster fence placement verification compared to earlier methods.

Solves more benchmark instances successfully.

Reduces unnecessary fence insertions while maintaining correctness.

Abstract

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.