Imperial College London > Talks@ee.imperial > CAS Talks > HiPEDS Seminar - Automatically Comparing Memory Consistency Models

HiPEDS Seminar - Automatically Comparing Memory Consistency Models

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Wiesia R Hsissen.

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 when a thread in a concurrent program reads from a shared memory location. Because MCMs have to take into account various optimisations employed by modern architectures (such as store buffering and instruction reordering) and compilers (such as constant propagation), they often end up being complex and counterintuitive, which makes them challenging to design and to understand.

In this work, we identify four important 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 can be cast as instances of a general constraint-satisfaction problem to which the solution is either a program or a pair of programs. We further show that although these constraints aren’t tractable for automatic solvers when phrased over programs directly, we can solve analogous constraints over programexecutions, and then reconstruct programs that satisfy the original constraints.

We illustrate our technique, which is implemented in the Alloy modelling framework, on a range of software- and architecture-level MCMs, both axiomatically and operationally defined. First, we automatically recreate – often in a simpler form – several known results, including: distinctions between several variants of the C/C+ MCM ; a failure of the ‘SC-DRF guarantee’ in an early C+ draft; that x86 is ‘multi-copy atomic’ and Power is not; bugs in common C/C++ compiler optimisations; and bugs in compiler mappings from OpenCL to AMD -style and NVIDIA GP Us. Second, we use our technique to develop and validate a stronger MCM for NVIDIA GP Us that supports a natural mapping from OpenCL.

This talk is part of the CAS Talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Changes to Talks@imperial | Privacy and Publicity