University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Automatically comparing memory consistency models

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 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity