http://www.dagstuhl.de/16471

20. – 25. November 2016, Dagstuhl Seminar 16471

Concurrency with Weak Memory Models: Semantics, Languages, Compilation, Verification, Static Analysis, and Synthesis

Organisatoren

Jade Alglave (University College London, GB)
Patrick Cousot (New York University, US)

Koordinatoren

Caterina Urban (ETH Zürich, CH)


1 / 4 >

Auskunft zu diesem Dagstuhl Seminar erteilen

Annette Beyer zu administrativen Fragen

Marc Herbstritt zu wissenschaftlichen Fragen

Dokumente

Teilnehmerliste
Gemeinsame Dokumente
Dagstuhl Seminar Wiki
Programm des Dagstuhl Seminars [pdf]

(Zum Einloggen bitte Seminarnummer und Zugangscode verwenden)

Motivation

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.

Classification

  • Programming Languages / Compiler
  • Semantics / Formal Methods
  • Verification / Logic

Keywords

  • Compilation
  • Computer memory
  • Concurrency
  • Memory barrier
  • Memory ordering
  • Micro-architecture
  • Multiprocessor
  • Out-of-order execution
  • Parallelism
  • Program synthesis
  • Programming language
  • Semantics
  • Static analysis
  • Verification
  • Weak memory model

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

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).

Publikationen

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.