November 20 – 25 , 2016, Dagstuhl Seminar 16471
Concurrency with Weak Memory Models: Semantics, Languages, Compilation, Verification, Static Analysis, and Synthesis
Caterina Urban (ETH Zürich, CH)
1 / 4 >
For support, please contact
(Use seminar number and access code to log in)
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.
Creative Commons BY 3.0 Unported license
Jade Alglave and Patrick Cousot
- Programming Languages / Compiler
- Semantics / Formal Methods
- Verification / Logic
- Computer memory
- Memory barrier
- Memory ordering
- Out-of-order execution
- Program synthesis
- Programming language
- Static analysis
- Weak memory model