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)

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team

Dokumente

Dagstuhl Report, Volume 6, Issue 11 Dagstuhl Report
Motivationstext
Teilnehmerliste
Gemeinsame Dokumente
Dagstuhl Seminar Wiki
Programm des Dagstuhl Seminars [pdf]

(Zum Einloggen bitte Seminarnummer und Zugangscode verwenden)

Summary

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.

License
  Creative Commons BY 3.0 Unported license
  Jade Alglave and Patrick Cousot

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.