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

on YouTube ↗20m

" summary

A formal memory model is built that extends RC11 to handle inline x86 assembly, specifically first C++ model with inline assembly for x86 covering non-temporal stores and store fences. The paper formalizes three new access modes, proves that programs fully in C++ keep RC11 semantics and programs fully in assembly get x86 semantics, establishes a data-race-freedom theorem, and verifies most compiler mappings and optimizations correct except sequentialization; current scope is x86 and integer-only operations.

AI-written summary · about

" chapters (16)

1. 0:00Introduction
2. 0:21Problem and motivation
3. 1:03Inline assembly applications
4. 2:25Challenges combining C++ and x86
5. 3:07RC11 and x86 concurrency models
6. 5:55Non-temporal stores issue
7. 6:39Compiler optimizations issue
8. 7:47Access mode limitations issue
9. 8:30Solution overview
10. 9:10Non-temporal stores with fences
11. 9:56Enforcing x86 consistency
12. 10:40New access modes
13. 12:03Design choices rationale
14. 13:30Model properties and correctness
15. 14:36Summary
16. 16:02Q&A