Campus Event Calendar
Event Entry
What and Who
Fences in Weak Memory Models
Jade Alglave
Inria
SWS Colloquium
SWS, RG1
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 8 February 2010
14:00
60 Minutes
E1 5
5th floor
Saarbrücken
Abstract
We present an axiomatic framework, implemented in Coq, to define weak memory
models w.r.t. several parameters: local reorderings of reads and writes, and
visibility of inter and intra processor communications through memory,
including full store atomicity relaxation. Thereby, we give a formal hierarchy
of weak memory models, in which we provide a formal study of what should be the
action and placement of fences to restore a given model such as Sequential
Consistency from a weaker one. Finally, we provide a tool, diy, that tests a
given machine to determine the architecture it exhibits. We detail the results
of our experiments on Power and the model we extract from it. This identified
an implementation error in Power 5 memory barriers (for which IBM is providing
a software workaround); our results also suggest that Power 6 does not suffer
from this problem.
models w.r.t. several parameters: local reorderings of reads and writes, and
visibility of inter and intra processor communications through memory,
including full store atomicity relaxation. Thereby, we give a formal hierarchy
of weak memory models, in which we provide a formal study of what should be the
action and placement of fences to restore a given model such as Sequential
Consistency from a weaker one. Finally, we provide a tool, diy, that tests a
given machine to determine the architecture it exhibits. We detail the results
of our experiments on Power and the model we extract from it. This identified
an implementation error in Power 5 memory barriers (for which IBM is providing
a software workaround); our results also suggest that Power 6 does not suffer
from this problem.
Contact
Bettina Peden-Bennett
0631-9303 9602
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
206
passcode not visible
logged in users only
Uwe Brahm, 02/18/2010 16:18
Bettina Peden-Bennett, 02/09/2010 11:45 -- Created document.
Bettina Peden-Bennett, 02/09/2010 11:45 -- Created document.