************************************************************************
Research School on "Semantics and tools for low-level programming"
January 14-18, 2013, ENS Lyon
************************************************************************

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

Webpage: http://www.ens-lyon.fr/DI/?p=2803&lang=en
Local Contact: Filippo Bonchi
The registration is free and closes Monday 8th of January.

Abstract:
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.