Burrow
A Proof Framework for Weak Memory
Dennis Sprokholt (Technische Universität München)
Soham Chakraborty (TU Delft - Electrical Engineering, Mathematics and Computer Science)
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
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.
help_outline