Experiments


Instrumentation strategies: Delays instrumentation: Graphs: 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

This family corresponds to litmus tests involving write-read pairs, to exercise typical x86 reordering of write-read pairs 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.
^ Overview

x86/rfi

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.
^ 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.
^ Overview

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.
^ Overview

x86/thin

This family corresponds to litmus tests involving thin-air (or causal loops) cycles. Therefore they should answer No in litmus terms, or Verification Successful in verification terms, regardless of the model.
^ Overview

ppc tests

ppc/plain/podrw

This family corresponds to litmus tests involving pairs showing that Power can reorder read-write pairs. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
^ Overview

ppc/plain/podwr

This family corresponds to litmus tests involving pairs showing that Power can reorder write-read pairs. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
^ Overview

ppc/plain/podww

This family corresponds to litmus tests involving pairs showing that Power can reorder write-write pairs. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
^ Overview

ppc/plain/podrr

This family corresponds to litmus tests involving pairs showing that Power can reorder read-read pairs. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
^ Overview

ppc/plain/posrr

This family corresponds to litmus tests involving pairs showing that Power can reorder read-read pairs. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
^ Overview

ppc/nc/lwdwr

This family corresponds to litmus tests involving pairs showing that Power's lwsync barrier cannot enforce any ordering when placed between a write and a read. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
^ Overview

ppc/nc/lwswr

This family corresponds to litmus tests involving pairs showing that Power's lwsync barrier cannot enforce any ordering when placed between a write and a read. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
^ Overview

ppc/plain/rfe

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.
^ Overview

ppc/plain/rfi

This family corresponds to litmus tests showing that Power authorises store buffering. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
^ Overview

ppc/plain/podrwposwr

This family corresponds to litmus tests involving pairs showing that Power can reorder read-read pairs. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
^ Overview

ppc/ac/aclwdrr

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.
^ Overview

ppc/ac/aclwsrr

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.
^ Overview

ppc/bc/bclwdww

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.
^ Overview

ppc/bc/bclwsww

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.
^ 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.
^ Overview

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.
^ Overview

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.
^ Overview

ppc/thin

This family corresponds to litmus tests involving thin-air (or causal loops) cycles. Therefore they should answer No in litmus terms, or Verification Successful in verification terms, regardless of the model.
^ 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.
^ Overview

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.

^ Overview

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.

^ Overview