COL 869: SPECIAL TOPICS IN CONCURRENCY
Relaxed memory concurrency
Timing: Monday, Thursday 14:00 - 15:30 hrs
Venue: Bharti 425
Overview
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:
Grading will be relative. Tentative scheme: paper reading and presentation 20%, each minor 20%, Major 40%. Lower cutoff for audit is grade B.
Schedule
| 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] C/C++ PDF |
| 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