REORDER 2012

First International Workshop on Memory Consistency Models

Sunday, July 8th, 2012. At CAV, Berkeley, California

CAV home

Overview


Goals

Scope

Organizers

Call for abstracts

Workshop program

Update: 9:00-12:00 sessions will be in room 310 Soda hall
News: the program is updated (last updated 7.5.2012)

Overview


Memory consistency models define the behaviour of concurrent systems
communicating through shared memory. Even though programmers typically
assume sequential consistency (SC), due to the effect of commonly used
hardware and software optimisations such as store buffers, out-of-order
execution and compiler transformations, most systems implement more
relaxed memory models. Most formal method and verification tools assume
SC, and hence may be unsound under weaker models. With the increase in
commercial prominence of multi-core systems, we need more involvement of
the verification community.

Goals


The aim of REORDER is to bring together the verification community and
experts from other relevant communities such as processor industry,
computer architecture, programming languages, semantics and concurrency
theory. To achieve this goal, we invite experts in these areas as
speakers to this workshop, and consequently create an opportunity for
experts from other communities to meet with people from the verification
community and discuss the major issues in this area.

Scope


This workshop welcomes participants interested in both hardware-level
and software-level memory models, in formal methods context, including,
but not limited to, the following topics:

- Design and specification of memory consistency models
- Verification of concurrent software wrt relaxed memory orderings
- Testing and verification of memory models wrt hardware
- Compiler transformations and relaxed memory models
- Fence insertion

Organizers


Sela Mador-Haim (University of Pennsylvania)
Jade Alglave (Oxford)

Call for abstracts

We welcome submission of abstracts for presentations in the workshop, including work in progress and published work.  Short abstracts (two to four paragraphs) in text format should be sent to Jade Alglave
(jade.alglave@cs.ox.ac.uk) and Sela Mador-Haim (selama@seas.upenn.edu)  by May 20th, 2012.

There will be no formal proceedings,and therefore the work will be considered unpublished.

Notifications of acceptance will be sent by May 27.

Workshop Program

Workshop location: Room 373, Soda hall, EECS department.

9:00-10:00
Akash Lal. Bounding and sequencing concurrent programs (EC^2 invited talk)

Shared with EC^2
(room 310 Soda)
10:00-10:30
Coffee break


10:30-12:00
Hans Boehm. The C11 and C++11 memory model (REORDER keynote)
Richard Bornat. Abducing Barriers for Power (presented by Peter Sewell)
Shared with EC^2
(room 310 Soda)
12:00-1:30
Lunch break


1:30-3:00
Madan Muthuvathi. The interoperability of TSO and data-race free memory models
Susmit Sarkar. An academic perspective on industrial memory models
Derek Williams. An industrial perspective on academic memory models

room 373 Soda
3:00-3:30
Coffee break


3:30-5:00
Ahmed Bouajjani. Checking state reachability for weak memory models
Roland Meyer. Robustness against TSO - towards algorithms.
Alexander Linden. Verifying programs on the TSO/PSO relaxed memory models

room 373 Soda
5:00
Discussion