Correct Translation between Weak Memory Model Architectures
D.G. Sprokholt (TU Delft - Programming Languages)
K.G. Langendoen – Promotor (TU Delft - Embedded Systems)
S.S. Chakraborty – Copromotor (TU Delft - Programming Languages)
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
This dissertation is about translating concurrent programs between computer architectures. Legacy programs—built-for and tested-on x86—behave differently on newer architectures, such as Arm and RISC-V. Particularly, weak memory behaviors emerge when two micro-architectural features interact: (i) concurrency, where multiple CPU cores simultaneously execute parts of a program, and (ii) out-of-order execution, where a CPU core reorders instructions to increase throughput. Programs can non-deterministically show one of various weak memory behaviors, meaning it could behave differently when executing again. Those behaviors differ between architectures. When migrating programs from x86 to Arm or RISC-V, the same program could non-deterministically show behaviors never observed on x86.
In part I, we look at binary translators, which are software systems that translate compiled binary programs between architectures. We study the translation process of three such real-world systems, identify errors in their translation of concurrency primitives, and fix them. We propose mathematically-rigorous weak memory models for these translators. We then define mapping schemes to translate concurrency primitives one-by-one from x86 to Arm and RISC-V. With the formal semantics, we prove those mapping schemes correct in the Agda proof assistant.
In part II, we study the common structure of our weak memory proofs written in Agda. As those proofs are often large, complex, and rigid, we identify their common structures for which we identify domain-specific abstractions. We implement those abstractions in our novel Agda proof framework Burrow to greatly simplify writing future weak memory proofs.
In part III, we use dynamic analysis to identify weak behaviors that were never seen on x86 but could appear on Arm. Our analysis simulates the program’s execution with the formal weak memory semantics of x86 and Arm. This analysis identifies only the new behaviors the program shows in practice. After finding any new behavior on Arm, we judiciously modify the program to eliminate only that behavior.
help_outline