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
Annette Beyer for administrative matters
Marc Herbstritt for scientific matters
(Use seminar number and access code to log in)
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.
- 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