ppc/bclwsww (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 a B-cumulative ordering when placed between two 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)