Automatically Comparing Memory Consistency Models [CEST evenings]

[zx9w]

Introduction

Automatically comparing memory consistency models is a paper about formal verification (using Alloy) and the semantic relationships between memory models (~ISA). It would be good to have heard of causality primitives like Acq/Rel, Barriers.. or have a good understanding of order theory.

This paper is (so far) a bit over my head, but Alloy is relatively simple and I don't think it'd be impossible to build some simple models for sanity-checking understanding of their arguments.

Availability shouldn't matter, we can use the #readtogether channel on freenode and a persistent codiMD to try to decipher the paper. I am also open to more synchronous and in depth sessions.

Abstract

A memory consistency model (MCM) is the part of a programming language or computer architecture specification that defines which values can legally be read from shared memory locations. Because MCMs take into account various optimisations employed by architectures and compilers, they are often complex and counterintuitive, which makes them challenging to design and to understand.

We identify four tasks involved in designing and understanding MCMs: generating conformance tests, distinguishing two MCMs, checking compiler optimisations, and checking compiler mappings. We show that all four tasks are instances of a general constraint-satisfaction problem to which the solution is either a program or a pair of programs. Although this problem is intractable for automatic solvers when phrased over programs directly, we show how to solve analogous constraints over program executions, and then construct programs that satisfy the original constraints.

Our technique, which is implemented in the Alloy modelling framework, is illustrated on several software- and architecture-level MCMs, both axiomatically and operationally defined. We automatically recreate several known results, often in a simpler form, including: distinctions between variants of the C11 MCM; a failure of the "SC-DRF guarantee" in an early C11 draft; that x86 is "multi-copy atomic" and Power is not; bugs in common C11 compiler optimisations; and bugs in a compiler mapping from OpenCL to AMD-style GPUs. We also use our technique to develop and validate a new MCM for NVIDIA GPUs that supports a natural mapping from OpenCL.

Idea

There are two parallel skill I would like to develop with this exercise:

• Learn how to use Alloy, which seems like a very lenient introduction to modelling computational structures.
• Get familiar with the points of disagreement between different memory models and the relative tradeoffs in that space.

Ideally we digest the arguments in the paper into executable models but since I don't know too much about this area of CS I can't tell if there is something better to read. Therefore I don't expect to go to deep on this particular paper, rather focus on developing those two skills; modelling and understanding the machine memory model.

Politics

Not needed, this is just something I will be poking for a few minutes a week (unless someone engages me, in which case I'm willing to do it your way).

• Asynchronous persistent channel :: #readtogether on freenode
• Synchronous ephemeral channels :: No meeting planned.
• Prerequisites for participation :: None
• Postcondition (for merging) :: Having a model that at least resembles a memory consistency model for some ISA. Stretch goal would be to have two of them and being able to order them by power. A table with ISA features and implications for said ordering would also be nice to have.