Dagstuhl Seminar 11011
Multi-Core Memory Models and Concurrency Theory
( Jan 03 – Jan 07, 2011 )
- Hans-J. Boehm (HP Labs - Palo Alto, US)
- Ursula Goltz (TU Braunschweig, DE)
- Holger Hermanns (Universität des Saarlandes, DE)
- Peter Sewell (University of Cambridge, GB)
- Annette Beyer (for administrative matters)
The current and future trend to multi-core and many-core computing systems suggests that within the next decade, concurrent multi-threaded programming will replace sequential programming as the standard programming paradigm. However, concurrency and modern computer architecture do not go together easily:
- Current programming language memory models are still incomplete. Mainstream languages such as Java increasingly promise sequential consistency for data-race-free programs. However,how data races can be handled in a way that supports reasonable performance, security, and debugability, is currently completely unknown.
- Hardware specifications are so informal that it is very hard to know whether we have a correct implementation of the language specs (if we knew how to specify those fully). It is not clear that existing ISAs, which have a long history, are a good match for the language semantics we are developing. There is an argument that this misalignment continues to encourage languages to support complex low-level constructs.
- The concurrent algorithms that are now being developed, and which are key to exploiting multiprocessors (via high-performance operating systems, hypervisor kernels, and concurrency libraries), are very subtle, so informal reasoning cannot give high confidence in their correctness.
- While there is a rich literature on concurrency theory, and extensive prior work on software verification for concurrency software (including process calculi, model-checking, temporal logics, rely-guarantee reasoning, and separation logic), almost all of it assumes a global notion of time, unrealistic though that is for these systems and algorithms.
Concurrency theory has a long tradition in investigating the foundational principles of concurrent computation, devoted to parallelism and causality of operations. It has created a wealth of models and notions readily applicable in this semantic challenge. Recent developments in the research communities of programming languages and concurrency theory, respectively, indeed show a growing trend towards cross-fertilization.
This seminar has fostered cross-fertilization of different expertises that will help to develop novel practical and, at the same time, theoretically sound paradigms for multi-core programming. It brought together concurrency theorists, memory model experts, computer systems architects, compiler experts, and formal verification researchers. The aim of the seminar was to adress in particular:
- Survey of problem domain: state of the practice in multi-core-programming and state of the art in memory consistency models.
- Application of concurrency theory approaches to reveal underlying concepts of parallelism, reordering, causality, and consistency.
- Cross-fertilization across formal approaches to memory consistency models and semantics of multithreaded programming.
- Attack points for formal analysis and computer aided programmer support.
Many of the questions that stood at the outset of this seminar have not been conclusively answered, thus yielding many potentials for further investigation. However, what makes this seminar uniquely successful is that it initiated a vivid exchange between a multitude of different scientific and industrial communities. During the seminar, it became clear that the current and future challenges of multi-core programming and memory models design in software and hardware can only be solved if the communities continue to exchange ideas and will learn from each other.
- Sarita Adve (University of Illinois - Urbana-Champaign, US) [dblp]
- Jade Alglave (University of Oxford, GB) [dblp]
- Arvind (MIT - Cambridge, US)
- Mark Batty (University of Cambridge, GB) [dblp]
- Hans-J. Boehm (HP Labs - Palo Alto, US) [dblp]
- Peter Boehm (University of Oxford, GB)
- Richard Bornat (Middlesex University, GB) [dblp]
- Ahmed Bouajjani (University of Paris VII, FR) [dblp]
- Gérard Boudol (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
- Sebastian Burckhardt (Microsoft Corporation - Redmond, US) [dblp]
- Luis Ceze (University of Washington - Seattle, US) [dblp]
- Stephan Diestelhorst (AMD - Dornbach, DE) [dblp]
- Mike Dodds (University of Cambridge, GB) [dblp]
- Laura Effinger-Dean (University of Washington - Seattle, US)
- Christian Eisentraut (Universität des Saarlandes, DE)
- Sibylle Fröschle (Universität Oldenburg, DE) [dblp]
- Ursula Goltz (TU Braunschweig, DE)
- Alexey Gotsman (IMDEA Software - Madrid, ES) [dblp]
- Richard Grisenthwaite (ARM Ltd. - Cambridge, GB)
- Erik Hagersten (Uppsala University, SE)
- Holger Hermanns (Universität des Saarlandes, DE) [dblp]
- Lisa Higham (University of Calgary, CA) [dblp]
- Mark D. Hill (University of Wisconsin - Madison, US) [dblp]
- Marieke Huisman (University of Twente, NL) [dblp]
- Bengt Jonsson (Uppsala University, SE) [dblp]
- Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
- Michael Kuperstein (Technion - Haifa, IL)
- Doug Lea (SUNY - Oswego, US) [dblp]
- Malte Lochau (TU Braunschweig, DE) [dblp]
- Andreas Lochbihler (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Michele Loreti (University of Florence, IT) [dblp]
- Brandon M. Lucia (University of Washington - Seattle, US) [dblp]
- Gerald Lüttgen (Universität Bamberg, DE) [dblp]
- Sela Mador-Haim (University of Pennsylvania - Philadelphia, US)
- Luc Maranget (INRIA - Le Chesnay, FR) [dblp]
- Milo M. K. Martin (University of Pennsylvania - Philadelphia, US)
- Paul McKenney (IBM - Beaverton, US) [dblp]
- Michael Mendler (Universität Bamberg, DE) [dblp]
- Maged M. Michael (IBM TJ Watson Research Center - Yorktown Heights, US) [dblp]
- Samuel P. Midkiff (Purdue University - West Lafayette, US)
- Madan Musuvathi (Microsoft Research - Redmond, US) [dblp]
- Uwe Nestmann (TU Berlin, DE) [dblp]
- Scott Owens (University of Cambridge, GB) [dblp]
- Gustavo Petri (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
- James Riely (DePaul University - Chicago, US) [dblp]
- Vijay A. Saraswat (IBM TJ Watson Research Center - Yorktown Heights, US) [dblp]
- Susmit Sarkar (University of Cambridge, GB) [dblp]
- Jens-Wolfhard Schicke (TU Braunschweig, DE)
- Jaroslav Sevcik (University of Cambridge, GB)
- Peter Sewell (University of Cambridge, GB) [dblp]
- Rob van Glabbeek (Data61 / NICTA - Sydney, AU)
- Heike Wehrheim (Universität Paderborn, DE) [dblp]
- Derek Williams (IBM Research Lab. - Austin, US) [dblp]
- Sascha Zickenrott (Universität des Saarlandes, DE)
- concurrent computation
- programming languages / compiler
- formal methods / semantics
- Formal Methods
- Memory Models
- Program Semantics
- Shared Memory