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

Pieter van den Ham

Computer architectures with weak memory models, such as ARMv8 and ARMv7, allow memory accesses to be reordered in many situations. 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. We expand Fency with a new dependency tracking analysis, integrate it with LLVM’s alias analysis infrastructure, and improve its usability. (thesis link)

---

Previous: Liam Clark | Proving functional correctness of monadic programs using separation logic
Next: Jesper Cockx | Unfolding control for abstract blocks