RUS  ENG
Full version
JOURNALS // Proceedings of the Institute for System Programming of the RAS // Archive

Proceedings of ISP RAS, 2017 Volume 29, Issue 5, Pages 149–164 (Mi tisp263)

This article is cited in 1 paper

Promising compilation to ARMv8.3

A. V. Podkopaevab, O. Lahavc, V. Vafeiadisd

a JetBrains Research
b St. Petersburg University
c Tel-Aviv University
d Max Planck Institute for Software Systems

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.

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



Bibliographic databases:


© Steklov Math. Inst. of RAS, 2024