Promising Compilation to ARMv8.3
| Autor: | A. V. Podkopaev, O. Lahav, V. Vafeiadis |
|---|---|
| Jazyk: | English<br />Russian |
| Rok vydání: | 2018 |
| Předmět: | |
| Zdroj: | Труды Института системного программирования РАН, Vol 29, Iss 5, Pp 149-164 (2018) |
| Druh dokumentu: | article |
| ISSN: | 2079-8156 2220-6426 |
| DOI: | 10.15514/ISPRAS-2017-29(5)-9 |
| Popis: | 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. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|