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.