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)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 6, Issue 11 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents
Dagstuhl Seminar Wiki
Dagstuhl Seminar Schedule [pdf]

(Use seminar number and access code to log in)

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

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.

NSF young researcher support