This program is tentative and subject to change.
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 to 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.
This program is tentative and subject to change.
Fri 25 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:20 | |||
11:00 20mTalk | A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code OOPSLA 2024 Julien Simonnet CEA LIST, Matthieu Lemerre Université Paris-Saclay - CEA LIST, Mihaela Sighireanu University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF | ||
11:20 20mTalk | Modeling Dynamic (De)Allocations of Local Memory for Translation Validation OOPSLA 2024 | ||
11:40 20mTalk | Extending the C/C++ Memory Model with Inline Assembly OOPSLA 2024 Paulo Emílio de Vilhena Imperial College London, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Azalea Raad Imperial College London | ||
12:00 20mTalk | Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe WebAssembly OOPSLA 2024 Maxime Legoupil Aarhus University, June Rousseau Aarhus University, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Jean Pichon-Pharabod Aarhus University, Lars Birkedal Aarhus University |