Extending the C/C++ memory model with inline assembly
File(s)
Published version
Author(s)
DE Vilhena, Paulo Emilio
Lahav, Ori
Vafeiadis, Viktor
Raad, Azalea
Type
Journal Article
Abstract
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.
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.
Date Issued
2024-10-08
Date Acceptance
2024-08-18
Citation
Proceedings of the ACM on Programming Languages, 2024, 8 (OOPSLA), pp.1081-1107
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
1081
End Page
1107
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
8
Issue
OOPSLA
Copyright Statement
© 2024 Owner/Author. This work is licensed under a Creative Commons Attribution International 4.0 License.
License URL
Subjects
Computer Science
Computer Science, Software Engineering
Concurrency
Science & Technology
Semantics of Programming Languages
Technology
Weak Memory Models
Publication Status
Published
Article Number
309
Date Publish Online
2024-10-08