[REORDER] – [Workshop on Memory Consistency]
[17th of July 2014] · Vienna, Austria
http://www0.cs.ucl.ac.uk/staff/j.alglave/reorder.html
Aims and Scope
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.
Organiser
Jade Alglave