These web pages are companion material to our article
Description of experiments
Comparison of our model with hardware:
with classification of invalid behaviours for ARM.
- As experiments on ARM invalidate our model, we
analyse the situation further
by relaxing our model,
of the few observed behaviours that still invalidate the relaxed model.
- We performed specific experiments to get insight on various issues:
- Comparison of the PLDI’11  operational model
with our Power
and ARM models.
We also compare the PLDI’11 model with
Power and ARM hardware.
- Comparison of the CAV’12  (axiomatic multi-event) model
with our model on Power only.
We also compare the CAV’12 model with Power hardware
on those few tests that invalidate the PLDI’11 model.
- Comparisons of ARM
models derived from PLDI’11  operational
model: non-flowing and
both with herd models and ARM hardware.
We also compare
the flowing and non-flowing models.
ARM Barrier Litmus Tests and Cookbook, November 2009.
Document number: PRD03-GENC-007826 1.0, http://infocenter.arm.com/help/topic/com.arm.doc.genc007826/Barrier_Litmus_Tests_and_Cookbook_A08.pdf.
Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave,
Scott Owens, Rajeev Alur, Milo Martin, Peter Sewell, and Derek Williams.
An axiomatic memory model for Power multiprocessors.
In CAV 2012.
Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams.
Understanding Power multiprocessors.
In PLDI 2011.
This document was translated from LATEX by