http://www.dagstuhl.de/16471

November 20 – 25 , 2016, Dagstuhl Seminar 16471

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

Organizers

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

Coordinators

Caterina Urban (ETH Zürich, CH)


1 / 4 >

For support, please contact

Annette Beyer for administrative matters

Marc Herbstritt for scientific matters

Documents

List of Participants
Shared Documents
Dagstuhl Seminar Wiki
Dagstuhl Seminar Schedule [pdf]

(Use seminar number and access code to log in)

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

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.