University of Cambridge > > Microsoft Research Cambridge, public talks > Fences and Stability in Weak Memory Models

Fences and Stability in Weak Memory Models

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

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

We present a class of relaxed memory models, defined in Coq, parameterised by the chosen permitted local reorderings of reads and writes, and the visibility of inter- and intra-processor communications through memory (e.g. store atomicity relaxation). Based on this class of models we develop a tool, diy, that systematically and automatically generates and runs litmus tests to determine properties of processor implementations. We detail the results of our experiments on Power and the model we base on them. This work identified a rare implementation error in Power 5 memory barriers (for which IBM is providing a workaround); our results also suggest that Power 6 does not suffer from this problem.

We prove results on the required behaviour and placement of synchronisation primitives to restore a given model, such as Sequential Consistency (SC), from a weaker one. We implemented these results in our offence tool, which places either lock-based or lock-free synchronisation in a x86 or Power program to ensure what we call its stability, i.e. it behaves as if running on SC.

This talk is part of the Microsoft Research Cambridge, public talks 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