October 21, 2016
Francesco Zappa Nardelli
We will review the possible approaches to defining memory models for programming languages, and will describe the C11 memory model. But we will go further: by leveraging the semantics of C11 low-level relaxed atomic accesses (which allows programmers to take full advantage of weakly-ordered memory operations) we will show that, among other dreadful consequences, the C11 standard does not permit many common source-to-source program transformations (such as expression linearisation and “roach motel” reorderings) that modern compilers perform and that are deemed to be correct. We will consider and evaluate a number of possible local fixes, some strengthening and some weakening the model. We will conclude with the remarkable and disturbing observation that, currently, there is no really satisfactory proposal for the semantics of a general-purpose shared-memory concurrent programming language.