03. – 07. Januar 2011, Dagstuhl Seminar 11011

Multi-Core Memory Models and Concurrency Theory


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)

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 1, Issue 1 Dagstuhl Report
Gemeinsame Dokumente


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:

  1. Survey of problem domain: state of the practice in multi-core-programming and state of the art in memory consistency models.
  2. Application of concurrency theory approaches to reveal underlying concepts of parallelism, reordering, causality, and consistency.
  3. Cross-fertilization across formal approaches to memory consistency models and semantics of multithreaded programming.
  4. 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


  • Concurrency
  • Formal Methods
  • Memory Models
  • Multi-Core
  • Multithreading
  • Program Semantics
  • Shared Memory


Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.