Promising Compilation to ARMv8.3
Concurrent programs have behaviors, which cannot be explained by interleaving execution of their threads on a single processing unit due to optimizations, which are performed by modern compilers and CPUs. How to correctly and completely define a semantics of a programming language, which accounts for the behaviors, is an open research problem. There is an auspicious attempt to solve the problem – promising memory model. To show that the model might be used as a part of an industrial language standard, it is necessary to prove correctness of compilation from the model to memory models of target processor architectures. In this paper, we present a proof of compilation correctness from a subset of promising memory model to an axiomatic ARMv8.3 memory model. The subset contains relaxed memory accesses and release and acquire fences. The proof is based on a novel approach of an execution graph traversal.
Proceedings of the Institute for System Programming, vol. 29, issue 5, 2017, pp. 149-164.
ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).