Concurrency with Weak Memory Models: Semantics, Languages, Compilation, Verification, Static Analysis, and Synthesis
( 20. Nov – 25. Nov, 2016 )
- Jade Alglave (University College London, GB)
- Patrick Cousot (New York University, US)
- Caterina Urban (ETH Zürich, CH)
- Annette Beyer (für administrative Fragen)
Dagstuhl Seminar Wiki
- Dagstuhl Seminar Wiki (Use personal credentials as created in DOOR to log in)
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.
In the last decade, research on weak memory has focussed on modeling accurately and precisely existing systems such as hardware chips. These laudable efforts have led to definitions of models such as IBM Power, Intel x86, Nvidia GPUs and others.
Now that we have faithful models, and know how to write others if need be, we can focus on how to use these models for verification, for example to assess the correctness of concurrent programs.
The goal of our seminar was to discuss how to get there. To do so, we gathered people from various horizons: hardware vendors, theoreticians, verification practitioners and hackers. We asked them what issues they are facing, and what tools they would need to help them tackle said issues.
The first day was dedicated to theory. We had overviews of classic semanticists tools such as event structures, message sequence charts, and pomsets. The remaining days were mostly dedicated to models and verification practices, whether from a user point of view, or a designer point of view. We chose to close the days early, so that our guests would have ample time to come back to an interesting point they had heard during one of the talks, or engage in deep discussions. The feedback we got was quite positive, in that the seminar help spark discussions with, for example, a PhD student in concurrency theory, and a verification practitioner from ARM.
- 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]
- programming languages / compiler
- semantics / formal methods
- verification / logic
- computer memory
- memory barrier
- memory ordering
- out-of-order execution
- program synthesis
- programming language
- static analysis
- weak memory model