Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Programming shared memory multicore machines (24h, 3ECTS)

Person in charge: Luc Maranget (INRIA)

Follow the course in this virtual room.

Teachers

  1. Relexed Memory Concurrency (12h): Luc Maranget, notes de cours.
  2. Runtime systems and task-parallel languages (12h): Adrien Guatto

Warm-up

Answers at the bottom of this page.

Quiz 1. Consider the system below, where two threads and run in parallel on an x86 or Power multicore/multiprocessor, and share two memory locations x and y, which initially hold 0. Each thread executes sequentially its code; for reference, x ← 1 stores the value 1 into the shared memory location x, r2 ← x reads the content of x and stores it in a local register r1.

Thread 0 Thread 1
x ← 1
r1 ← y
y ← 1
r2 ← x

Can you guess all the possible values stored in r1 and r2 at the end of an execution of the system? How many different final states are there?

Quiz 2. Consider the following Java program (again the two threads share memory locations x and y, which initially hold 0, while r1 and r2 are local variables).

Thread 0 Thread 1
r1 = x
y = r1
r2 = y
x = (r2==1)?y:1
print r2

Can this concurrent Java program print 1?

Course objectives

In the recent years multicore and multiprocessors systems have become ubiquitous. However, despite 40 years of research on concurrency and programming languages, programming and reasoning about concurrent systems remains very challenging. Both hardware and high-level programming languages incorporate many performance optimisations: these are typically unobservable by single-threaded programs, but, as illustrated by the examples above, some have observable consequences for the behaviour of concurrent code.

The aim of this module is to introduce some of the theory and the practice of concurrent programming, from hardware memory models and the design of high-level programming languages to the correctness of concurrent algorithms. In particular, we will:

  • give a formal and precise overview of the semantics of modern multiprocessor architectures, including x86 and Power/ARM;
  • illustrate how common compiler optimisations are source of unexpected behaviours, and will discuss the design of the memory model of high-level programming languages;
  • study the design and correctness of modern concurrent algorithms.

Some familiarity with discrete mathematics (sets, partial orders, etc.) and with sequential programming will be assumed, and experience with operational semantics and with some concurrent programming would be helpful. However the course will be self-contained.

Lectures

On Wednesday, 16h15–19h15, room 1014

Answers

  1. The correct answer is 4: an execution on x86 or Power can also terminate with r1 = r2 = 0 and x = y = 1. Why?
  2. Intuitively it should not. However if compiled with the HotSpot compiler or GCJ, it does print 1. Why?
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA