Fencing off unwanted behavior: Improving and evaluating the Fency static analysis tool

More Info


Computer architectures with weak memory models, such as ARMv8 and ARMv7, allow memory accesses to be reordered in many situations.
Therefore, weak memory models may cause a program to exhibit more behavior than a strong memory model, such as x86.
Fency is a static analysis tool that inserts memory fences to ensure that a program exhibits the same behavior when run on a weaker memory model.
However, Fency lacks important features such as function call support, does not use LLVM's alias analysis algorithms, and inserts too many fences when targeting ARMv8.

We expand Fency with a new dependency tracking analysis, integrate it with LLVM's alias analysis infrastructure, and improve its usability.
We show that while the new alias analysis fixes a vital soundness issue, it does not reduce the number of fences Fency inserts.
Additionally, our evaluation of the dependency tracking analysis shows that it can eliminate some redundant fences.
Finally, we run Fency on larger C/C++ programs, which we made possible by reimplementing Fency as a module pass.