Generating tests

We wish to generate tests which exhibit non-SC behaviours when run on x86 or Power machines.

For each architecture we first generate tests with diy. Those tests are violations of SC induced by a cycle of candidate relaxations at which at least one is relaxed by our model for the targeted architecture.

For x86, we get 58 ’X’ tests from the configuration file X.conf (i.e. diy is invoked as “diy -conf X.conf”). The condition on test outcome generated by diy detects one non-SC behaviour. We rather wish to detect any non-SC behaviour. Equivalently, we shall require SC behaviour by running our (non-released) simulator memevents in SC mode and changing test conditions so that SC behaviour is required.

As an example of the approach, running X006.litmus on some x86 machine yields 12 outcomes:

% litmus -mach chianti X006.litmus
...
Histogram (12 states)
5     :>1:EAX=1; 1:EBX=0; 2:EAX=1; 2:EBX=0; x=1;
999488:>1:EAX=2; 1:EBX=0; 2:EAX=1; 2:EBX=0; x=1;
1355  :>1:EAX=1; 1:EBX=1; 2:EAX=1; 2:EBX=0; x=1;
1062834:>1:EAX=2; 1:EBX=1; 2:EAX=1; 2:EBX=0; x=1;
1020  :>1:EAX=1; 1:EBX=0; 2:EAX=1; 2:EBX=1; x=1;
698661:>1:EAX=2; 1:EBX=0; 2:EAX=1; 2:EBX=1; x=1;
6     :>1:EAX=1; 1:EBX=1; 2:EAX=1; 2:EBX=1; x=1;
739   :>1:EAX=2; 1:EBX=1; 2:EAX=1; 2:EBX=1; x=1;
540   :>1:EAX=2; 1:EBX=0; 2:EAX=1; 2:EBX=0; x=2;
595701:>1:EAX=2; 1:EBX=1; 2:EAX=1; 2:EBX=0; x=2;
1050680:>1:EAX=2; 1:EBX=0; 2:EAX=1; 2:EBX=1; x=2;
588971:>1:EAX=2; 1:EBX=1; 2:EAX=1; 2:EBX=1; x=2;
...

However, there are only 10 SC outcomes as can be seen by running the test against SC:

% memevents -model sc X006.litmus
...
States 10
1:EAX=1; 1:EBX=0; 2:EAX=1; 2:EBX=1; x=1;
1:EAX=1; 1:EBX=1; 2:EAX=1; 2:EBX=0; x=1;
1:EAX=1; 1:EBX=1; 2:EAX=1; 2:EBX=1; x=1;
1:EAX=2; 1:EBX=0; 2:EAX=1; 2:EBX=0; x=1;
1:EAX=2; 1:EBX=0; 2:EAX=1; 2:EBX=1; x=1;
1:EAX=2; 1:EBX=0; 2:EAX=1; 2:EBX=1; x=2;
1:EAX=2; 1:EBX=1; 2:EAX=1; 2:EBX=0; x=1;
1:EAX=2; 1:EBX=1; 2:EAX=1; 2:EBX=0; x=2;
1:EAX=2; 1:EBX=1; 2:EAX=1; 2:EBX=1; x=1;
1:EAX=2; 1:EBX=1; 2:EAX=1; 2:EBX=1; x=2;
..

We see that the condition exists (x=2 /\ 1:EAX=2 /\ 1:EBX=0 /\ 2:EAX=1 /\ 2:EBX=0) of test X006 only detects one of the two non-SC outcomes, the other (1:EAX=1; 1:EBX=0; 2:EAX=1; 2:EBX=0; x=1) would remain unnoticed. We thus change the condition of test, resulting into the new test X006, so as to detect all SC outcomes. Notice that the new condition is computed automatically by memevents in SC mode.

We apply the above procedure to the complete batch of tests produced by diy. As a result, any of the 58 new ’X’ tests will yield “No” as soon as it produces a non-SC outcome and “Ok” when all outcomes are SC. Notice that the new conditions are unreadable, except for simple tests such as X054.

For Power, we proceed similarly, with a specific diy configuration file PPC.conf, resulting in 209 ’PPC’ tests.

Applying offence

For x86 we apply offence three times to all tests of the initial batch(containing for instance X006), using various synchronisation techniques:

• We insert fences with offence -technique fence, resulting in tests ’F’. See for instance test X006-F.
• We turn (some) stores into xchg instructions with offence -technique atom, resulting in tests ’A’. See for instance test X006-A.
• We lock conflicting accesses with offence -technique lock, resulting in tests ’L’. See for instance test X006-L.

For Power we apply offence four times to all tests of the initial batch (containing for instance PPC002), using various synchronisation techniques:

• We insert fences with offence -technique fence, resulting in tests ’F’. See for instance test PPC002-F.
• We turn conflicting stores and loads into store atomic (STA) and fetch and no-op (FNO) with offence -technique atom, resulting in tests ’A’. See for instance test PPC002-A.
• We use the mapping ’P’ (turn the fragile pairs loads into FNO’s, insert fences) with offence -technique atom -alt, resulting in tests ’B’¹. See for instance test PPC002-B.
• We lock conflicting accesses with offence -technique lock, resulting in tests ’L’. See for instance test PPC002-L.

One may notice that Power code uses macros for FNO, STA, LOCK and UNLOCK, while locking idioms are expanded in x86 code. Here are expanded versions of PPC002-A, PPC002-B, and PPC002-L.

Running the tests and checking soundness

For x86, we run the tests on two machines saumur (Intel Xeon with 4, 2-ways hyperthreaded, cores (8 logical procs) running Linux) and chianti (Intel Xeon with 8, 2-ways hyperthreaded, cores (16 logical procs) running Linux).

We performed several runs of the complete batch of tests, varying testing conditions (see litmus documentation). The variations are recorded in files saumur.txt and chianti.txt. This produces files S.00 to S.13 for saumur and files C.00 to C.12 for chianti. We aggregate those into S.X and C.X, respectively.

The following four tables expose the conclusion of the experiment: offence restores SC for all tests.

More precisely, remembering that “No” means that some non-SC behaviour have been observed, while “Ok” means that all observed behaviours are SC, we see that, for each test, offence experimentally restores SC with three different techniques. The leftmost table also shows the number of non-SC outcomes observed/total number of outcomes collected. Notice that the tests produced by offence have been run at least as many times as the initial tests.

For Power, we run the tests on three machines abducens (Power 6 with 4 cores 2-way SMT running Linux), vargas (Power 6 with 32 cores 2-way SMT running AIX) and power7 (Power 7 with 8 cores 4-way SMT running Linux) We performed several runs of the complete batch of tests, varying testing conditions (see litmus documentation). The variations are recorded in files abducens.txt, vargas.txt and power7.txt. We aggregate run logs into A.X, V.X, and P.X, respectively.

The tables resulting from the experiment are in a separate page. One easily checks that all outcomes collected by running offence generated programs are SC, by seeing that no cell in the last four tables ever contains ”No”. As a curiosity, notice that a few of the initial tests do not exhibit any non-SC behaviour, see PCC170 for instance.

Complete sources and logs: for x86, X86-SIMPLE (archive) and Power, PPC-SIMPLE (archive).