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 [Kang et al. POPL’17]. To show that the model might be used as a part of an industrial language standart, it is necessary to prove correctness of compilation from the model to memory models of target processor architectures. In the talk, we present a proof of compilation correctness from a subset of promising memory model to an axiomatic ARMv8.3 memory model [Pulte et al. POPL’18]. The subset contains relaxed memory accesses and release and acquire fences. The proof is based on a novel approach of an execution graph traversal.
The talk is based on the paper (in Russian).
The full version of the proof is available here(in Russian).
Presenter --- Anton Podkopaev
Date: November 20, 2017
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28