Fencing off unwanted behavior: Improving and evaluating the Fency static analysis tool
P.E. van den Ham (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Soham Chakraborty – Mentor (TU Delft - Programming Languages)
D.G. Sprokholt – Mentor (TU Delft - Programming Languages)
Koen Langendoen – Graduation committee member (TU Delft - Embedded Systems)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
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.