An Axiomatic Memory Model for Power's Multiprocessors

The following page provides supplementary material for the axiomatic specifications of Power's memory consistency model (submtted to CAV2012)

• Semi-formal definition of the aximatic model
  
• Proof of equivalence of the axiomatic model to the operational model
• Formal specifications of the axiomatic model, in Lem
• Test information