![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Fences and Stability in Weak Memory Models
![]() Fences and Stability in Weak Memory ModelsAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsType the title of a new list here Cambridge Carbon Footprint Eurostrings 2015Other talksHunting for cacti in the caribbean Richard Horton (The Lancet Cheif Editor): Scientific Publishing Interrogating T cell signalling and effector function in hypoxic environments Modularity, criticality and evolvability of a developmental GRN Overview of Research Process |