Automatically comparing memory consistency models

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

• John Wickerson, Imperial College
• Friday 24 June 2016, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Dominic Mulligan.

We identify five tasks involved in designing and reasoning about memory consistency models (MCMs): generating conformance tests, distinguishing two MCMs, searching for monotonicity violations, debugging compilation schemes, and checking the “SC-DRF guarantee”. We show that each of these tasks corresponds to solving an instance of a general constraint-satisfaction problem. We further show that although these constraints are not tractable for automatic solvers when phrased over programs directly, we can solve analogous constraints over program executions 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. In particular, we generate: programs that distinguish several recently-published variants of the C11 MCM , monotonicity violations in both C11 and x86, compilation quirks from OpenCL to NVIDIA and AMD -style GPUs, and SC-DRF violations in an early draft of C11 . In several cases, our automatically-generated solutions are either new or substantially simpler than those found manually in previous work.

This is joint work with Mark Batty (U Kent), Tyler Sorensen (Imperial) and George A. Constantinides (Imperial).

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.