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

This family corresponds to litmus tests involving pairs showing that Power's lwsync barrier cannot enforce an A-cumulative ordering when placed between two reads. 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)