Experiments

Abstract: These web pages are companion material to our article “Herding Cats”.

Description of experiments

• Simulators and machines
• Tests
  • Test base
  • What is a test?
  • Ambiguous test executions
• Reading tables of results
  • A table that lists test results
  • Comparison tables
• Classification of forbidden behaviours
• Some model and hardware logs

Experiments

• Comparison of our model with hardware: Power and ARM, with classification of invalid behaviours for ARM.
• As experiments on ARM invalidate our model, we analyse the situation further by relaxing our model, with classification of the few observed behaviours that still invalidate the relaxed model.
• We performed specific experiments to get insight on various issues:
  • A focus on recent ARM processors.
  • A focus on Qualcomm processors.
  • Comparing the sequentially consistent model (SC) with NVIDIA Denver in 32bit mode.
  • Comparing our proposed ARM model with hardware.
  • Comparing a model without dynamic components in ppo, with the base Power-ARM model.
  • Data and address dependencies are different.
  • Additional fences: Power eieio barrier and ARM dmb.st and dsb.st fences.
• Comparison of the PLDI’11 [3] 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 [2] (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 [3] operational model: non-flowing and flowing, both with herd models and ARM hardware. We also compare the flowing and non-flowing models and study the new “Pop” and “Lazy Pop” models.
• Comparisons of updated Power operational models derived from PLDI’11 [3] and of Power “Pop” model.
• Experimental models for load-reserve and store conditional: comparing the flowing model and herd. See also herd-based experiments, for ARM and Power.

References

[1]

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

[2]

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. http://www.cl.cam.ac.uk/~pes20/weakmemory/CAV2012paper-final.pdf.

[3]

Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. Understanding Power multiprocessors. In PLDI 2011. http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/index.html.

This document was translated from L^AT_EX by H^EV^EA.