x86/rfi (tooling date Sun Jan 22 02:23:23 GMT 2012)
This family corresponds to litmus tests involving internal read-from pairs, to exercise typical x86 store buffering scenarios. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms, as soon as the model is x86/TSO or a weaker one.
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) |