https://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
Dokumente
Dagstuhl Report, Volume 6, Issue 11
Motivationstext
Teilnehmerliste
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.


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