January 3 – 7 , 2011, Dagstuhl Seminar 11011
Multi-Core Memory Models and Concurrency Theory
1 / 2 >
For support, please contact
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.
- Concurrent Computation
- Programming Languages / Compiler
- Formal Methods / Semantics
- Formal Methods
- Memory Models
- Program Semantics
- Shared Memory