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
Contents
Litmus tests for X86/TSO:
|
Litmus tests for Power/ARM:
|
|
C code:
|
|
|
|
|
x86 tests
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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.
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
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
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