RUS  ENG
Full version
JOURNALS // Computing, Telecommunication and Control // Archive

St. Petersburg Polytechnical University Journal. Computer Science. Telecommunication and Control Sys, 2017 Volume 10, Issue 4, Pages 51–69 (Mi ntitu192)

Software of Computer, Telecommunications and Control Systems

On compilation correctness for a subset of a promising memory model to the ARMv8.3 memory model

A. V. Podkopaeva, O. Lahavb, V. Vafeiadisc

a Saint Petersburg State University
b Tel Aviv University
c Max Planck Society

Abstract: A 'promising' memory model is an auspicious solution to the problem of defining semantics for an imperative language with concurrency, such as C/C++ or Java. An essential requirement for such a memory model is the existence of an effective and correct compilation scheme from the language to its target platforms. There are compilation correctness proofs from the promising model to x86 and Power as well as to an operational model ARMv8 POP. This paper presents such proof for an axiomatic memory model for ARMv8.3. In the proof, we use a new method of execution traversal, which might be used in other compilation correctness proofs for the promising memory model.

Keywords: concurrency, compilation correctness, weak memory models, ARM, semantics.

UDC: 004.4'422

Language: English

DOI: 10.18721/JCSTCS.10405



© Steklov Math. Inst. of RAS, 2024