Burrow: A Proof Framework for Weak Memory

Abstract

Abstract Burrow is a proof framework for weak memory mapping proofs. Those mappings appear as optimizations and translations between languages inside compilers and binary translators. However, their mechanized proofs, when defined over formal axiomatic weak memory semantics, are often large and complex. In this paper, we discuss the proof primitives provided by Burrow which simplify mechanizing those mapping proofs and help to prove many lemmas generally . To demonstrate the benefits of these primitives, we use Burrow to prove a mapping from x86 to Arm correct.