Extending the C/C++ Memory Model with Inline Assembly
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910585809010688 |
|---|---|
| author | de Vilhena, Paulo Emílio Lahav, Ori Vafeiadis, Viktor Raad, Azalea |
| author_facet | de Vilhena, Paulo Emílio Lahav, Ori Vafeiadis, Viktor Raad, Azalea |
| contents | Programs written in C/C++ often include inline assembly: a snippet of architecture-specific assembly code used to access low-level functionalities that are impossible or expensive to simulate in the source language. Although inline assembly is widely used, its semantics has not yet been formally studied.
In this paper, we overcome this deficiency by investigating the effect of inline assembly on the consistency semantics of C/C++ programs. We propose the first memory model of the C++ Programming Language with support for inline assembly for Intel's x86 including non-temporal stores and store fences. We argue that previous provably correct compiler optimizations and correct compiler mappings should remain correct under such an extended model and we prove that this requirement is met by our proposed model. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_17208 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Extending the C/C++ Memory Model with Inline Assembly de Vilhena, Paulo Emílio Lahav, Ori Vafeiadis, Viktor Raad, Azalea Programming Languages F.3.2 Programs written in C/C++ often include inline assembly: a snippet of architecture-specific assembly code used to access low-level functionalities that are impossible or expensive to simulate in the source language. Although inline assembly is widely used, its semantics has not yet been formally studied. In this paper, we overcome this deficiency by investigating the effect of inline assembly on the consistency semantics of C/C++ programs. We propose the first memory model of the C++ Programming Language with support for inline assembly for Intel's x86 including non-temporal stores and store fences. We argue that previous provably correct compiler optimizations and correct compiler mappings should remain correct under such an extended model and we prove that this requirement is met by our proposed model. |
| title | Extending the C/C++ Memory Model with Inline Assembly |
| topic | Programming Languages F.3.2 |
| url | https://arxiv.org/abs/2408.17208 |