Concurrent programming on modern multi-processor architectures is difficult because memory operations might not be executed in the order specified by the program code. In multi-threaded environments (or when interfacing with other hardware via memory buses) this out-of-order execution (or more generally these weak consistency scenarios) may lead to counter-intuitive behaviours. Fortunately the programmer can use memory barriers, or fences, to order memory accesses. But the semantics of fences is often far from being well documented. Moreover they are difficult to position correctly, since this is a hardware-dependent task. Thus the daily job of concurrent programmers can become very hard.

The lack of formal concepts to describe weakly consistent systems (such as hardware chips, programming languages, or distributed systems) has made their modeling difficult. One way forward is to develop automated methods and tools ensuring the correctness of concurrent programs. This is the objective of this seminar on the semantics, languages, compilation, verification, static analysis, and synthesis in the context of concurrency with weak consistency models.

The objective of the seminar is to set up a research program to design formal methods and produce tools to make multi-processor programming feasible, easier, and definitely safe in the next decades:

• Which semantic models of hardware are best suited for formal methods?
• Which abstraction of existing semantics?
• Which concept of parallel execution which is simple enough and compatible with modern hardware?
• Which semantics definitions of programming languages are best suited for verification methods?
• How can weak memory models be taken into account in program verification and proof methods?
• How to verify compilers for parallel programs compiled on microprocessors with weak memory models?
• Which semantics and abstractions, including parameterised by a formal description of the architecture, are more appropriate for static program analysis?
• Which synthesis methods are more appropriate for automatic barrier placement, including parameterised by a formal description of the architecture?

Correct parallel programming for modern machine architectures is a very difficult problem, which will certainly take more than one decade to be solved satisfactorily. The outcome of this seminar should essentially be a plan to achieve this goal in a decent horizon. This requires the mobilisation of communities which rarely intersect by lack of federating projects and conferences such as hardware and parallel computer architecture, semantics of parallelism, programming languages supporting concurrency, compilation of parallel programs, verification, static analysis, and synthesis of concurrency, in all cases in the context of weak memory models. We hope that this seminar will be a successful starting point for this long-term effort.

• Jade Alglave (University College London, GB) [dblp]
• Giovanni Tito Bernardi (University Paris-Diderot, FR) [dblp]
• Annette Bieniusa (TU Kaiserslautern, DE) [dblp]
• Richard Bornat (Middlesex University - London, GB) [dblp]
• Stephen Brookes (Carnegie Mellon University - Pittsburgh, US) [dblp]
• Simon Castellan (ENS - Lyon, FR) [dblp]
• Andrea Cerone (Imperial College London, GB) [dblp]
• Pierre Clairambault (ENS - Lyon, FR) [dblp]
• Patrick Cousot (New York University, US) [dblp]
• Andrei Marian Dan (ETH Zürich, CH) [dblp]
• Will Deacon (ARM Ltd. - Cambridge, GB) [dblp]
• David Delmas (Airbus S.A.S. - Toulouse, FR) [dblp]
• Delphine Demange (IRISA - Rennes, FR) [dblp]
• Stephan Diestelhorst (ARM Ltd. - Cambridge, GB) [dblp]
• Charles Anthony Richard Hoare (Microsoft Research UK - Cambridge, GB) [dblp]
• Vincent Jacques (University College London, GB)
• Bernhard Kragl (IST Austria - Klosterneuburg, AT) [dblp]
• Ori Lahav (MPI-SWS - Kaiserslautern, DE) [dblp]
• Daniel Lustig (NVIDIA Corp. - Santa Clara, US) [dblp]
• Yatin Manerkar (Princeton University, US) [dblp]
• Luc Maranget (INRIA - Paris, FR) [dblp]
• Paul McKenney (IBM - Beaverton, US) [dblp]
• Paul-Andre Mellies (University Paris-Diderot, FR) [dblp]
• Roland Meyer (TU Braunschweig, DE) [dblp]
• Maged M. Michael (Facebook - New York, US) [dblp]
• Antoine Miné (CNRS & University Pierre & Marie Curie - Paris, FR) [dblp]
• Vincent Nimal (Microsoft Research UK - Cambridge, GB) [dblp]
• Andrea Parri (INRIA - Paris, FR) [dblp]
• Gustavo Petri (University Paris-Diderot, FR) [dblp]
• Susmit Sarkar (University of St. Andrews, GB) [dblp]
• Helmut Seidl (TU München, DE) [dblp]
• Suzanne Shoaraee (ARM France SAS - Sophia-Antipolis, FR)
• Daryl Stewart (ARM Ltd. - Cambridge, GB) [dblp]
• Caroline Trippel (Princeton University, US) [dblp]
• Caterina Urban (ETH Zürich, CH) [dblp]
• Viktor Vafeiadis (MPI-SWS - Kaiserslautern, DE) [dblp]
• Derek Williams (IBM Research Lab. - Austin, US) [dblp]
• Glynn Winskel (University of Cambridge, GB) [dblp]
• Sizhuo Zhang (MIT - Cambridge, US) [dblp]