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

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

van den Ham, Pieter (TU Delft Electrical Engineering, Mathematics and Computer Science)

Chakraborty, S.S. (mentor)
Sprokholt, D.G. (mentor)
Langendoen, K.G. (graduation committee)

Delft University of Technology

Computer Science

2022-12-02

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.

weak memory model
robustness analysis
concurrency
computer architectures
static analysis

http://resolver.tudelft.nl/uuid:17fbcc63-fced-4077-bb1d-efc2d10bd871

Student theses

master thesis

© 2022 Pieter van den Ham