Fri Dec 25 19:08:27 GMT 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww000
"DpdR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r5=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ;
sync | lwzx r4,r3,r5 | sync | lwzx r4,r3,r5 ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r4=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: xor 10,3,3
_litmus_P3_2_: lwzx 31,10,9
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww000 Allowed
Histogram (76 states)
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
4 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
6 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
3 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
1241 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
1586 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3498 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1095 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
3707 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
3228 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
1872 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
6426 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
28396 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
2453 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3179 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
29091 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
7129 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
76221 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
145465:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
415716:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
78117 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
64999 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
62415 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
22752 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
21888 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
109815:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
680479:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
29620 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
3056910:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
671050:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
2131696:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
150793:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
409369:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
548868:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
2328755:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
3114431:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
4482111:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
1257857:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
2047165:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
672347:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
1022484:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
1160703:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
649668:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3973158:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
586800:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2194269:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
1794867:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
2445486:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
97686 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
2083477:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
4002562:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
20251088:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
3044353:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
4276941:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
1064423:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
4338078:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
4387166:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
1233051:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
1146198:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
10872081:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
2123339:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
4562141:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
1859167:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
14561526:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
3163717:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
4144461:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
20564847:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
2237813:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
4029996:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
4581263:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
41836312:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
14641870:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
10724766:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
20243552:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
20408382:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
57020555:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r4=0) is NOT validated
Hash=9fe623fb41a5ce2e4216ef423b67f696
Cycle=DpdR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww000 No BCSyncsWW
Safe=Fre DpdR
Time bcssww000 95.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww001
"SyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | sync ;
sync | lwzx r4,r3,r5 | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww001 Allowed
Histogram (75 states)
1 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
3 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
1683 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
14387 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
3744 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1162 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1656 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
26800 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
3513 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1561 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
15285 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1267192:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
41874 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
8548 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
31767 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
140562:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
587545:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
499692:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
218716:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
901449:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
68604 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
155223:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
609192:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
320954:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
403111:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
408317:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
262844:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
211180:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1335724:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
848730:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
48914 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
2344942:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2917873:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
1382728:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2146946:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
921358:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
3604222:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
4643013:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
2193171:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
3762380:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2760300:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
163501:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2169429:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1232256:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2067189:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
586028:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
86422 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
3875993:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
2335565:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
4077700:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
5059310:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
723148:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2475153:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1092644:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
3311308:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
14046036:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1551802:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
10217174:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3371687:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
16957350:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
4546892:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
17693349:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
21305073:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
1795264:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
18830770:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
2698107:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
6058277:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
2769570:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
13313327:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
18478922:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3572025:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
5338197:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
34966682:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
58116982:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=c19feeb22b3e4fe95d3ae9cd399e4667
Cycle=SyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww001 No BCSyncsWW
Safe=Fre SyncdRR DpdR
Time bcssww001 96.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww002
"LwSyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r5=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ;
sync | lwzx r4,r3,r5 | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: xor 10,3,3
_litmus_P1_2_: lwzx 31,10,9
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww002 Allowed
Histogram (75 states)
1 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1674 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2659 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1048 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
9965 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1382 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3790 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1509 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
7786 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
30108 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
207175:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
39656 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
33125 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
912090:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
183549:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
103469:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
354013:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
432919:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
130137:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
598729:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
22873 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
12212 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
2247813:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
308296:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
227540:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
573037:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2050176:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
937639:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
175105:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
3790319:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
565741:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1318503:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1368706:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
2197814:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
4401706:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
10327179:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
71372 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1928643:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3937738:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
707311:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
3258300:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
127158:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
22289666:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
1023600:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
3368435:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
45100 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
5072230:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
3099923:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
1585777:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
324737:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
4254409:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
13054538:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
3160935:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
971472:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3501106:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
2038400:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
2877636:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
5166856:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
20341031:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1127329:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
3783636:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
646194:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
17191070:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
4678245:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3315187:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
59939428:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
20115511:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1863829:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
17975450:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1872483:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2031761:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
36059334:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
13614724:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r4=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=a2812688a109c131b01004a694cfdd81
Cycle=LwSyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww002 No BCSyncsWW
Safe=Fre LwSyncdRR DpdR
Time bcssww002 94.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww003
"DpdW Wse SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | li r4,1 ;
lwz r3,0(r4) | li r3,2 | stwx r4,r3,r5 ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: xor 31,3,3
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,31,9
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww003 Allowed
Histogram (17 states)
6 :>0:r3=1; 2:r1=2; x=2; y=2;
26 :>0:r3=0; 2:r1=1; x=2; y=2;
173754:>0:r3=1; 2:r1=1; x=2; y=2;
174173:>0:r3=2; 2:r1=0; x=1; y=2;
1493780:>0:r3=1; 2:r1=1; x=1; y=2;
283925:>0:r3=1; 2:r1=0; x=1; y=2;
2862147:>0:r3=1; 2:r1=2; x=1; y=2;
1890407:>0:r3=2; 2:r1=1; x=1; y=2;
6809551:>0:r3=2; 2:r1=1; x=2; y=2;
17786665:>0:r3=0; 2:r1=1; x=1; y=2;
17303785:>0:r3=1; 2:r1=0; x=2; y=2;
87901818:>0:r3=2; 2:r1=2; x=1; y=2;
41610594:>0:r3=0; 2:r1=2; x=1; y=2;
53619445:>0:r3=0; 2:r1=0; x=2; y=2;
71568485:>0:r3=0; 2:r1=0; x=1; y=2;
36087224:>0:r3=2; 2:r1=2; x=2; y=2;
60434215:>0:r3=2; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=316a93ca86d6e131419704cdf84a4e06
Cycle=DpdW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww003 No BCSyncsWW
Safe=Fre Wse SyncdWR DpdW
Time bcssww003 76.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww004
"SyncdRW Wse SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | li r3,1 ;
lwz r3,0(r4) | li r3,2 | stw r3,0(r4) ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww004 Allowed
Histogram (15 states)
3197024:>0:r3=1; 2:r1=2; x=1; y=2;
480026:>0:r3=1; 2:r1=0; x=1; y=2;
140750:>0:r3=1; 2:r1=1; x=2; y=2;
3842853:>0:r3=2; 2:r1=1; x=1; y=2;
2203008:>0:r3=1; 2:r1=1; x=1; y=2;
6351939:>0:r3=2; 2:r1=1; x=2; y=2;
17731907:>0:r3=1; 2:r1=0; x=2; y=2;
61276156:>0:r3=2; 2:r1=0; x=2; y=2;
16830876:>0:r3=0; 2:r1=1; x=1; y=2;
41971283:>0:r3=0; 2:r1=0; x=2; y=2;
742591:>0:r3=2; 2:r1=0; x=1; y=2;
90954369:>0:r3=2; 2:r1=2; x=1; y=2;
86148208:>0:r3=0; 2:r1=0; x=1; y=2;
38078372:>0:r3=0; 2:r1=2; x=1; y=2;
30050638:>0:r3=2; 2:r1=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=4a84f5a0d5b5b42156717d2ee2b4312f
Cycle=SyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww004 No BCSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcssww004 78.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww005
"LwSyncdRW Wse SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | li r3,1 ;
lwz r3,0(r4) | li r3,2 | stw r3,0(r4) ;
| stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 4,1
_litmus_P2_3_: stw 4,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,2
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww005 Allowed
Histogram (16 states)
3 :>0:r3=0; 2:r1=1; x=2; y=2;
528378:>0:r3=1; 2:r1=0; x=1; y=2;
419577:>0:r3=2; 2:r1=0; x=1; y=2;
3692331:>0:r3=1; 2:r1=2; x=1; y=2;
7844620:>0:r3=2; 2:r1=1; x=2; y=2;
173124:>0:r3=1; 2:r1=1; x=2; y=2;
2392141:>0:r3=1; 2:r1=1; x=1; y=2;
18663016:>0:r3=1; 2:r1=0; x=2; y=2;
3936488:>0:r3=2; 2:r1=1; x=1; y=2;
17370943:>0:r3=0; 2:r1=1; x=1; y=2;
78527468:>0:r3=0; 2:r1=0; x=1; y=2;
88717622:>0:r3=2; 2:r1=2; x=1; y=2;
48706253:>0:r3=0; 2:r1=0; x=2; y=2;
35915643:>0:r3=0; 2:r1=2; x=1; y=2;
30718573:>0:r3=2; 2:r1=2; x=2; y=2;
62393820:>0:r3=2; 2:r1=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated
Hash=585ce030a2274090c0b4fa0251d7b3ad
Cycle=LwSyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww005 No BCSyncsWW
Safe=Fre Wse SyncdWR LwSyncdRW
Time bcssww005 75.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww006
"DpdR Fre SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r5=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ;
sync | sync | lwzx r4,r3,r5 ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r4=0)
Generated assembler
_litmus_P2_0_: lwz 30,0(11)
_litmus_P2_1_: xor 10,30,30
_litmus_P2_2_: lwzx 31,10,9
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww006 Allowed
Histogram (17 states)
52 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
64 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
323990:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
100882:>0:r3=2; 2:r1=0; 2:r4=1; y=2;
304207:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
3789938:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
866139:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
1358774:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
7797075:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
17126284:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
72951775:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
61309202:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
80718127:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
17324065:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
42783065:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
54320847:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
38925514:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r4=0) is NOT validated
Hash=eea77ff32793e8bed4abb1ad0c914c0d
Cycle=DpdR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww006 No BCSyncsWW
Safe=Fre SyncdWR DpdR
Time bcssww006 77.70
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww007
"SyncdRR Fre SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | sync ;
sync | sync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww007 Allowed
Histogram (15 states)
218982:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
3201349:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
244913:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
253242:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
2133700:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
2796596:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
7384954:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
83745453:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
17771625:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
60915673:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
16614066:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
38459726:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
37090248:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
52256392:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
76913081:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=66d340e023bd1d1ae19ed5903eb5d2ea
Cycle=SyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww007 No BCSyncsWW
Safe=Fre SyncdWR SyncdRR
Time bcssww007 79.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww008
"LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe"
{0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=x;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww008 Allowed
Histogram (17 states)
50 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
34 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
481399:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
278300:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
3558235:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
311626:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
9431592:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
3133332:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
2591487:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
18773033:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
16744908:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
76608717:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
82054039:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
60750097:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
52519808:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
36558985:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
36204358:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=d19882d97477fc15c9e4fbc588dc8a96
Cycle=LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww008 No BCSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bcssww008 80.01
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww009
"SyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | sync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww009 Allowed
Histogram (73 states)
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
2139 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1417 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1185 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2048 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1243 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1055 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
43561 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
8336 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
457281:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
31096 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
894901:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
334425:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
216649:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
797351:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
746228:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
917914:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
66701 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
314617:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
255490:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
269496:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
265122:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
269319:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
135248:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
715451:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1795303:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2325143:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1112006:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
636583:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
724876:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1751626:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2308403:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4309329:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
217452:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
335666:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1945946:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
606471:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1801233:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1737658:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2712527:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2711868:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2038492:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
4370494:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
5711061:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
3742138:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3641749:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
43324 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
4316351:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
127446:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
728084:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2312264:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
692699:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
4356163:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2483687:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
4412220:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1186655:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4368260:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
447237:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1345321:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
17260755:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2849207:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
5790098:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1310519:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
13641452:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
16946220:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
13751772:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2931319:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
17311256:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
20056400:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
16563202:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
33860423:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
19778561:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
57844807:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=ac99317f895df8ed08197fb9ed0e136a
Cycle=SyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww009 No BCSyncsWW
Safe=Fre SyncdRR
Time bcssww009 94.84
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww010
"LwSyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | sync | stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww010 Allowed
Histogram (75 states)
2 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1239 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2227 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
823 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
8038 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1406 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2216 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
19860 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1247 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
332961:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1094273:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
44547 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
27824 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
328782:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
72839 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
116913:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
269867:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
197317:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
127097:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
292738:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
263867:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
285095:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
216033:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
228525:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1704782:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
782246:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1290572:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1301872:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
607785:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
791622:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
334688:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2141309:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
713173:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
607990:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
741137:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2715668:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
4261925:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1732299:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1706512:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
1267150:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2834362:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2280432:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
5461056:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2169357:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
4179571:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
13208336:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2607345:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
334149:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
747840:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4141826:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
4357953:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3137236:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
1807324:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2295752:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4336051:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
6034515:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3808112:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
19346679:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
984822:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2528097:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1205310:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4525867:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
699020:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
20773714:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
13730887:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3163788:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
16249880:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
16326440:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
58563508:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
32999736:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3855929:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
16812935:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
17855701:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=fdf7665f1e0ce0f0c6d4d353ee548d9e
Cycle=LwSyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww010 No BCSyncsWW
Safe=Fre SyncdRR LwSyncdRR
Time bcssww010 95.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/bcssww011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
bcssww011
"LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe"
{0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=x;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test bcssww011 Allowed
Histogram (77 states)
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
3 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
3 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1599 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1544 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1333 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
10607 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
12132 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1203 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
3045 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2690 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
330879:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
123134:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
27929 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
26010 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
360382:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
120363:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
277878:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1797610:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
276488:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1733244:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
75928 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
835984:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1083435:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
2238109:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1012938:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
783993:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
244973:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
216958:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
329033:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
3954187:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
846811:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
708449:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1314330:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2334606:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1357894:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1681644:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
236533:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
320580:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
711961:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
617630:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
219865:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1731956:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
3398016:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
2210608:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1305902:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
5911960:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1238156:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
4033080:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2781643:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2838081:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
4315350:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4355693:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
662506:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
886086:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
4075032:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
15619642:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4367664:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5659864:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2771511:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
17127164:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2181158:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
20304418:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
17352002:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2682807:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
16198034:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
19887468:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
13022708:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3810417:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
31992987:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
59741484:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
3362241:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
323822:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4507440:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
13109176:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=7c8f7188794f6e0c8b799c86369a2299
Cycle=LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe
Relax bcssww011 No BCSyncsWW
Safe=Fre LwSyncdRR
Time bcssww011 92.96
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 2000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 20000
#endif
#ifndef N_EXE
#define N_EXE (32 < N ? 1 : 32 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Fri Dec 25 19:25:45 GMT 2009