19th of July

Colocated with CAV

Memory consistency models define the behaviour of concurrent systems communicating through shared memory. Programmers typically assume sequential consistency (SC). To support commonly used hardware and software optimisations, such as store buffers, out-of-order execution and compiler transformations, most systems, however, implement more relaxed memory models. Most formal methods and verification tools assume SC, and hence may be unsound under weaker models. With the increase in commercial prominence of multi-core systems, the verification community cannot ignore these issues: bugs solely attributed to weak memory models have already surfaced in both open source and commercial software.

Weak memory models are at the boundaries of hardware and software. Hence, research on weak memory models is a multi-disciplinary effort involving different areas of expertise, including formal methods, verification, computer architecture, concurrency, and programming languages. For example, active research in this area include the design of formal models for hardware systems, tools and techniques for testing formal models by contrasting them with both other models and actual hardware, and verification of software running on weak memory hardware.

Here is the program:

08:30-09:00: Olivier Giroux (Nvidia)
TBD, Abstract
09:00-09:30: Daniel Lustig (Princeton)
Verifying Memory Consistency Models at the Microarchitecture Level, Abstract
09:30-10:00: Muralidaran Vijayaraghavan (MIT)
WMM: A Resilient Weak Memory Model, Abstract
10:00-10:30: Coffee break
10:30-11:00: Alex Horn (Oxford)
A Concurrency Problem with Exponential DPLL(T) Proofs, Abstract
11:00-11:30: Gustavo Petri (Purdue)
Formalizing JMM Implementation Recipes, Abstract
11:30-12:00: TBD
TBD, Abstract
12:00-13:30: Lunch break
Afternoon: Discussion

See also the webpage of last year's edition.