# Experiments

**Instrumentation strategies:**

- all delays/cyc: instruments all the unsafe delay pairs per cycle
- 1 delay/cyc: instruments one unsafe delay pair per cycle

**Delays instrumentation:**

- for e1 -po-> e2: instrument e1
- for e1 -rfe-> e2: instrument e1 and e2

**Graphs:**

- instrumented events in red boxes
- only non-uniproc non-thin-air cycles with instrumented events drawn
- an empty graph means that there is nothing to instrument

**Experiments setting:**Intel(R) Xeon(R) CPU X5667 @ 3.07GHz x 4

49551096 kB

Linux 2.6.32-37-server x86_64

### x86 tests

#### x86/podwr

^ Overview#### x86/rfi

^ Overview#### x86/mix

This family corresponds to litmus tests involving either write-read pairs or internal read-from, to exercise typical x86/TSO 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. It differs from x86/podwr and x86/rfi in that it involves several diy cycles instead of one. |

#### x86/safe

This family corresponds to litmus tests involving only safe x86 relations. Therefore they should answer No in litmus terms, or Verification Successful in verification terms, if the model is x86/TSO. |

#### x86/thin

^ Overview### ppc tests

#### ppc/plain/podrw

^ Overview#### ppc/plain/podwr

^ Overview#### ppc/plain/podww

^ Overview#### ppc/plain/podrr

^ Overview#### ppc/plain/posrr

^ Overview#### ppc/nc/lwdwr

^ Overview#### ppc/nc/lwswr

^ Overview#### ppc/plain/rfe

^ Overview#### ppc/plain/rfi

^ Overview#### ppc/plain/podrwposwr

^ Overview#### ppc/ac/aclwdrr

^ Overview#### ppc/ac/aclwsrr

^ Overview#### ppc/bc/bclwdww

^ Overview#### ppc/bc/bclwsww

^ Overview#### ppc/safe

This family corresponds to litmus tests involving only safe Power relations. Therefore they should answer No in litmus terms, or Verification Successful in verification terms, if the model is Power. |

#### ppc/cross

This family corresponds to litmus tests involving pairs exercising typical Power scenarios. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms, as soon as the model is Power. It involves several diy cycles instead of one. |

#### ppc/mix

This family corresponds to litmus tests involving pairs exercising typical Power scenarios. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power. It involves several diy cycles instead of one. |

#### ppc/thin

^ Overview### C source

For the following set of experiments, which use non-generated code the origin of which is explained for each group below, the verification results even for the SC case must be taken with a grain of salt: the truth values of properties embedded in the code may be affected by the way integer variables are handled, i.e., whether boundedness and overflow are taken into account or not. We tried to work around these inconsistencies by adding additional assumptions, but no such change will eliminate the potential efficiency gains of (unsoundly) treating C integers and mathematical (unbounded) integers. Therefore, again, we solely focus on the soundness of tools, but not their relative efficiency.#### Standard C algorithms

This family consists of Dekker, Szymanski, Lamport, Peterson's mutual exclusion algorithms, and Lamport's bakery algorithm. They should answer Yes in litmus terms, or Verification Failed in verification terms, starting from x86/TSO. |

#### Borrowed C examples

This family contains the bug found by Sebastian Burckhart and Madan Musuvathi with their Sober tool, presented in their CAV 2008 paper, and our own fix for it. It should answer Yes in litmus terms, or Verification Failed in verification terms, starting from x86/TSO. Its fixed version should answer No in litmus terms, or Verification Successful in verification terms, regardless of the model. |

#### Other C programs

On the one hand, this family contains the PostgreSQL bug, the fix proposed by PostgreSQL developers and our own fix for it. It should answer Yes in litmus terms, or Verification Failed in verification terms, starting from RMO. The fix proposed by the developers is not enough, hence should answer Yes in litmus terms, or Verification Failed in verification terms, starting from RMO. Our fix should answer No in litmus terms and Verification Successful in verification terms, regardless of the model. On the other hand, this family contains our experiments with RCU and Apache. It shows all the cycles (i.e. potential bugs) exhibited by RCU, and verifies Apache. |