Relaxed memory concurrency

Timing: Monday, Thursday 14:00 - 15:30 hrs

Venue: Bharti 425

Instructor: Soham Chakraborty


In the multicore era, all performance-critical software employs some form of concurrent programming; typically shared memory concurrency. In this setting, traditionally programmers have assumed that a multithreaded program executed simply by interleaving the executions of its threads—a model known as sequential consistency (SC). This assumption is, however, invalidated both by mainstream multicore architectures, which often execute instructions out of order, and by compilers, whose optimizations affect the outcomes of concurrent programs. As a result, concurrent programs have more outcomes than SC allows. Relaxed memory consistency or relaxed memory concurrency concern the mathematical study of these additional outcomes.

Course structure:

In this course we will go through various relaxed memory concurrency models. We will start with some traditional models (e.g. TSO, PSO, RMO) and then move to more state-of-the art models. We will study the relaxed memory models in multicore architectures (x86, ARM, Power) as well as in programming languages (C++11). Next we will focus on correct compilation of concurrency from programming languages to the architectures. Finally we go through some topics to demonstrate the tradeoff in defining semantic definitions and efficient compilation. In addition, we will learn some automated tools (e.g herd, memalloy) which are used significantly to study relaxed memory concurrency.

Course objective:

On successful completion of the course, a student will be able to appreciate literatures in this area and pursue further. we hope a student will appreciate the role of formal methods in designing architectures, programming languages, and compilers.


Grading will be relative. Tentative scheme: paper reading and presentation 20%, each minor 20%, Major 40%. Lower cutoff for audit is grade B.


Date Topic Notes/Readings
30.12.2019 Introduction PDF
02.01.2020 Traditional models and transformational semantics PDF
06.01.2020 Introduction to Operational Semantics PDF, FSPL Chapter-2
09.01.2020, 13.01.2020 Operational Semantics for Concurrency (SC) PDF
16.01.2020 Operational Semantics for TSO PDF, [TPHOLs'09]
20.01.2020 Axiomatic Semantics PDF
23.01.2020 Axiomatic Semantics: Coherence, Atomicity, RA, SC PDF
27.01.2020 TSO model, equivalence between coherence axioms PDF
30.01.2020 equivalence between coherence axioms: alternative proof PDF
Minor 1 PDF
10.02.2020 PowerPC Architecture PDF
13.02.2020 PowerPC Architecture PDF
17.02.2020 PowerPC and ARMv7 Architectures PDF, [PLDI 2011-supplimentary], [HERD]: Section 1-6
20.02.2020, 22.02.2020 ARMv8 Architectures PDF, More details: [POPL'18]
22.02.2020, 24.02.2020 Relaxed memory concurrency in progrmming languages: DRF0 PDF, Details: [ISCA'90]

27.02.2020 C++ Concurrency Primitives and Relations PDF
02.03.2020 C++ Concurrency Axioms PDF
02.03.2020 C++ Concurrency Challenges PDF
30.03.2020 C++ Concurrency and Correctness of Program Transformations PDF
06.04.2020 C++ Concurrency and Correctness of Program Transformations PDF
09.04.2020 C++ Concurrency and Correctness of Program Transformations PDF
24.04.2020 C++ Concurrency and Correctness of Program Transformations PDF
24.04.2020 C++ Concurrency and Correctness of Program Transformations PDF
C++ Concurrency and Correctness of Program Transformations PDF
C++ Mappings to Processors PDF
C++ Mappings to Processors PDF
Data-Race-Freedom (DRF) Guarantee PDF
Mixed-Size Access Paper

Some readings/References:

* Weak memory consistency (2017) by Ori Lahav and Viktor Vafeiadis

* [FSPL] The Formal Semantics of Programming Languages: An Introduction. Glynn Winskel.

* [TPHOLs'09] A Better x86 Memory Model: x86-TSO. Scott Owens Susmit Sarkar Peter Sewell.

* [PLDI 2011-supplimentary] A Tutorial Introduction to the ARM and POWER Relaxed Memory Models. Luc Maranget, Susmit Sarkar, Peter Sewell.

* [HERD] Herding cats: Modelling, Simulation, Testing, and Data-mining for Weak Memory. Jade Alglave, Luc Maranget, and Michael Tautschnig.

* [RACES '12] Position Paper: Nondeterminims is Unavoidable, but Data Races are Pure Evil. Hans-J. Boehm.

* [HotPar'11] How to miscompile programs with "benign" data races. Hans-J. Boehm.

* [ISCA '90] Weak Ordering - A New Definition. Sarita V. Adve, Mark D. Hill

* [POPL'11] Mathematizing C++ concurrency. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber

* [POPL'15] Common compiler optimisations are invalid in the C11 memory model and what we can do about it. Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli

* [POPL'16] Overhauling SC atomics in C11 and OpenCL. Mark Batty, Alastair F. Donaldson, John Wickerson

* [PLDI'17] Repairing Sequential Consistency in C/C++11. Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer

* [FM'16] Explaining Relaxed Memory Models with Program Transformations. Ori Lahav, Viktor Vafeiadis.

* [POPL'18] Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell