ppc/rfe (tooling date Sun Jan 22 02:23:23 GMT 2012)

This family corresponds to litmus tests showing that Power relaxes the atomicity of writes. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.

Name

SC

CAV'11

TSO (all delay/cyc)

TSO (1 delay/cyc)

TSO (opt delay/cyc)

Expected (TSO)

PSO (all delay/cyc)

PSO (1 delay/cyc)

PSO (opt delay/cyc)

Expected (PSO)

RMO (all delay/cyc)

RMO (1 delay/cyc)

RMO (opt delay/cyc)

Expected (RMO)

Power (all delay/cyc)

Power (1 delay/cyc)

Power (opt delay/cyc)

Expected (Power)