January 14-18, 2013, ENS Lyon.


Francesco Zappa Nardelli (INRIA), Mark Batty (University of Cambridge), Alastair Donaldson(Imperial College London), and Martin Vechev (ETH Zurich)


Available from here


Optimisations performed by the hardware or by high-level language compilers can reorder memory accesses in various subtle ways. These reorderings can sometimes be observed by concurrent programs, exacerbating the usual problems of concurrent programming. The situation is even worse when we abandon traditional shared memory concurrency in favor of graphics processing units (GPUs) or exotic hardware. In these lectures we will cover recent progress in understanding and specifying the behaviour of some major processor architectures and the impact of optimisations performed by high-level programming language compilers, stablishing a solid basis for shared memory programming. We will then explore techniques which can help programmers develop reliable concurrent software by automatically discovering the necessary synchronization. We will also discuss techniques for verification of multicore software, including GPU kernels.


  • Monday:
    • 10h30-12h30: Welcome + introduction
    • 14h: Batty: x86TSO
    • 15h30-16h30: TD: x86TSO
  • Tuesday
    • 9h-10h30: Batty + Zappa: ARM & Power
    • 11h-12h30: Zappa : Compiler Optimisations + DRF
    • 14h-15h: TD: ARM & Power
    • 15h30-16h30: TD: Compiler Optimisations + DRF
  • Wednesday
    • 9h-10h30: Batty : C11
    • 11h-12h30: Vechev (1)
    • 14h-15h: TD : C11
    • 15h30-16h30: TD : Vechev
  • Thursday
    • 9h-10h30: Vechev (2)
    • 11h-12h30: Alastair (1)
  • Friday
    • 9h-10h30: Alastair (2)
    • 11h-12h30: TD: Alastair
    • 14h-15h30: Mini-exam

For the practical sessions

Please bring your laptop with you. In case you do not have one, please get in contact with Filippo Bonchi (ens-lyon.fr).

Contact: Filippo Bonchi.


Registration is free, but there is a limit on the number of participants and it does include neither housing nor meals (though for lunch the attendees will be granted access to the student cafeteria). Registration should be made before Monday, January 8, by clicking on this link and filling in and sending the e-mail form. You shall receive a confirmation as soon as possible.

Alternatively, you can copy/paste and fill the following form and send it by e-mail to research.school.1@gmail.com, with subject “Registration form — research school 2”

First Name:

Last Name:


Position (MSc student, PhD student, researcher, etc.):

E-mail address:

wishes to attend the research school ‘Semantics and tools for low-level concurrent programming’, taking place at ENS Lyon, from Jan. 14 to Jan. 18.