Extending the C/C++ Memory Model with Inline Assembly

TL;DR

This paper introduces a formal memory model for C++ that incorporates inline assembly, enabling better understanding and verification of low-level code interactions in concurrent programs.

Contribution

It presents the first formal memory model for C++ with inline assembly support, including non-temporal stores and fences, and proves its correctness for compiler optimizations.

Findings

Proposed a memory model for C++ with inline assembly support

Validated that existing compiler optimizations remain correct under the new model

Extended the model to include x86-specific features like non-temporal stores

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.