Proceedings of ISP RAS


Promising Compilation to ARMv8.3

Podkopaev A.V. (SPBU, St. Petersburg, Russia; JetBrains Research, St. Petersburg, Russia)
Lahav O. (TAU, Tel Aviv, Israel)
Vafeiadis V. (MPG, Kaiserslautern, Germany)

Abstract

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.

Keywords

concurrency; compilation correctness; weak memory models

Edition

Proceedings of the Institute for System Programming, vol. 29, issue 5, 2017, pp. 149-164.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(5)-9

Full text of the paper in pdf (in Russian) Back to the contents of the volume