Sat Dec 26 13:39:08 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_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 10,2
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: lwz 5,0(11)
_litmus_P1_1_: xor 10,5,5
_litmus_P1_2_: lwzx 6,10,9
_litmus_P2_0_: li 11,1
_litmus_P2_1_: stw 11,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 10,2
_litmus_P2_4_: stw 10,0(9)
_litmus_P3_0_: lwz 5,0(11)
_litmus_P3_1_: xor 10,5,5
_litmus_P3_2_: lwzx 6,10,9
Test bcssww000 Allowed
Histogram (77 states)
1 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
1 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
6 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
2 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
2 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
2035 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
2216 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
6640 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
5520 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
2895 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
3631 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3332 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
4198 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
6913 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
7658 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
8162 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
32761 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
53748 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
53390 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
24546 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
128071:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
396235:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
63285 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
79396 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
34367 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
28467 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
464156:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
819868:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
2350772:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
48072 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
99502 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
24327 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
830149:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
468379:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
1294897:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
3458295:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
1303688:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
116294:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
626166:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
1850175:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
2230712:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
13661473:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
1232832:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
689887:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
1199863:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
4283265:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
3588117:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
2588240:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
994365:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
4077301:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
19680739:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
3196631:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
1916507:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
4647441:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
2548210:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2339717:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
10392268:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
2228003:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
4728746:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
4151231:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
2307178:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
4870398:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2590487:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
1281673:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
4866942:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
529985:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
4070717:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
10731412:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
3852854:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
56609284:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
20706588:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
21121025:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
4107190:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
18823984:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
3529949:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
40058587:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
14863981:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=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: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 238.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 10,2
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: lwz 5,0(11)
_litmus_P1_1_: xor 10,5,5
_litmus_P1_2_: lwzx 6,10,9
_litmus_P2_0_: li 11,1
_litmus_P2_1_: stw 11,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 10,2
_litmus_P2_4_: stw 10,0(9)
_litmus_P3_0_: lwz 6,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 7,0(9)
Test bcssww001 Allowed
Histogram (76 states)
1 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1 :>1:r1=1; 1:r4=0; 3:r1=2; 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=0; x=2; y=2;
1154 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
2059 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1315 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1021 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
22155 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
39842 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
226568:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
214692:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
4999 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1000 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
35593 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
1539 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
758161:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
44362 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
54702 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
58859 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
54004 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
142968:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
634934:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
464575:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
18738 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
286313:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
82047 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1210265:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
560172:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
354747:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1778768:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1177807:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1105984:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
2237822:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
4146405:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
3233184:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3006559:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
3215156:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
3825965:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
137770:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
3565214:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1141216:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1134328:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
5632032:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
208117:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
251535:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
550973:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
2144656:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1114547:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
5337532:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
10727090:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
2163938:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
887850:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
3277117:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
4687398:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
2013055:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
862926:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
19037673:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3134028:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
22788776:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
304688:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
595219:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
3608385:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
3067155:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
4764519:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
2009248:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
14721222:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
2040303:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
4945817:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
4122717:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
54457941:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
15024087:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
17630665:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
16561245:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
18601829:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
37742750:>1:r1=2; 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=c19feeb22b3e4fe95d3ae9cd399e4667
Cycle=SyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww001 No BCSyncsWW
Safe=Fre SyncdRR DpdR
Time bcssww001 235.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 10,2
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: lwz 5,0(11)
_litmus_P1_1_: xor 10,5,5
_litmus_P1_2_: lwzx 6,10,9
_litmus_P2_0_: li 11,1
_litmus_P2_1_: stw 11,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 10,2
_litmus_P2_4_: stw 10,0(9)
_litmus_P3_0_: lwz 6,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 7,0(9)
Test bcssww002 Allowed
Histogram (75 states)
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
2 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
7 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1469 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1627 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
3086 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3172 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
9363 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2895 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
11973 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
42485 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
56536 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
113558:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
212427:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
36812 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
28741 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
13167 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
107478:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
3587 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
285968:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
543406:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
747581:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
196108:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
766410:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
177724:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
750593:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
2174491:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1221666:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
166890:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
575792:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
77293 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1691877:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
421458:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
40136 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
3721656:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
3166913:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
2033153:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1854107:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
3345336:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
256699:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
35647 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
4211817:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
4409118:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
1102311:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
562315:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1100354:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1880056:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
3714749:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1998753:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
2182920:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
3706931:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
4969352:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
4661817:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2715530:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
1087253:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
3064032:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
381834:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
4302985:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
14286657:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
1103246:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
14468321:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
593518:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3757676:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
4950443:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
19483225:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
16412821:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
3091031:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
3744270:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
17595844:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
38387131:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
19942079:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1078177:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
56316289:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
22827501:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
11010354:>1:r1=0; 1:r4=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: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 238.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 8,2
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 11,1
_litmus_P1_1_: stw 11,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,2
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: lwz 6,0(11)
_litmus_P2_1_: xor 10,6,6
_litmus_P2_2_: li 7,1
_litmus_P2_3_: stwx 7,10,9
Test bcssww003 Allowed
Histogram (17 states)
4 :>0:r3=1; 2:r1=2; x=2; y=2;
10 :>0:r3=0; 2:r1=1; x=2; y=2;
66991 :>0:r3=1; 2:r1=1; x=2; y=2;
206243:>0:r3=1; 2:r1=0; x=1; y=2;
598245:>0:r3=1; 2:r1=1; x=1; y=2;
1422423:>0:r3=2; 2:r1=1; x=1; y=2;
5914495:>0:r3=2; 2:r1=1; x=2; y=2;
4287032:>0:r3=1; 2:r1=2; x=1; y=2;
18322570:>0:r3=1; 2:r1=0; x=2; y=2;
211547:>0:r3=2; 2:r1=0; x=1; y=2;
17326536:>0:r3=0; 2:r1=1; x=1; y=2;
59696217:>0:r3=2; 2:r1=0; x=2; y=2;
74405495:>0:r3=0; 2:r1=0; x=1; y=2;
37468721:>0:r3=2; 2:r1=2; x=2; y=2;
88410245:>0:r3=2; 2:r1=2; x=1; y=2;
52095469:>0:r3=0; 2:r1=0; x=2; y=2;
39567757:>0:r3=0; 2:r1=2; x=1; 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 109.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 8,2
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 11,1
_litmus_P1_1_: stw 11,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,2
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: lwz 7,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: li 8,1
_litmus_P2_3_: stw 8,0(9)
Test bcssww004 Allowed
Histogram (16 states)
1 :>0:r3=0; 2:r1=1; x=2; y=2;
52999 :>0:r3=1; 2:r1=1; x=2; y=2;
423235:>0:r3=1; 2:r1=0; x=1; y=2;
4587499:>0:r3=2; 2:r1=1; x=2; y=2;
37007899:>0:r3=0; 2:r1=2; x=1; y=2;
3639186:>0:r3=1; 2:r1=2; x=1; y=2;
2705997:>0:r3=2; 2:r1=1; x=1; y=2;
18830185:>0:r3=1; 2:r1=0; x=2; y=2;
16842663:>0:r3=0; 2:r1=1; x=1; y=2;
611763:>0:r3=2; 2:r1=0; x=1; y=2;
959498:>0:r3=1; 2:r1=1; x=1; y=2;
62201391:>0:r3=2; 2:r1=0; x=2; y=2;
93386873:>0:r3=2; 2:r1=2; x=1; y=2;
46296210:>0:r3=0; 2:r1=0; x=2; y=2;
81162908:>0:r3=0; 2:r1=0; x=1; y=2;
31291693:>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 108.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 8,2
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 11,1
_litmus_P1_1_: stw 11,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,2
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: lwz 7,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: li 8,1
_litmus_P2_3_: stw 8,0(9)
Test bcssww005 Allowed
Histogram (15 states)
58934 :>0:r3=1; 2:r1=1; x=2; y=2;
360037:>0:r3=1; 2:r1=0; x=1; y=2;
440761:>0:r3=2; 2:r1=0; x=1; y=2;
4702705:>0:r3=2; 2:r1=1; x=2; y=2;
3886451:>0:r3=1; 2:r1=2; x=1; y=2;
846597:>0:r3=1; 2:r1=1; x=1; y=2;
18887972:>0:r3=1; 2:r1=0; x=2; y=2;
2290236:>0:r3=2; 2:r1=1; x=1; y=2;
79370695:>0:r3=0; 2:r1=0; x=1; y=2;
16698080:>0:r3=0; 2:r1=1; x=1; y=2;
49636730:>0:r3=0; 2:r1=0; x=2; y=2;
91025836:>0:r3=2; 2:r1=2; x=1; y=2;
36316374:>0:r3=0; 2:r1=2; x=1; y=2;
33897215:>0:r3=2; 2:r1=2; x=2; y=2;
61581377:>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 108.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 11,1
_litmus_P1_1_: stw 11,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,2
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: lwz 5,0(11)
_litmus_P2_1_: xor 10,5,5
_litmus_P2_2_: lwzx 6,10,9
Test bcssww006 Allowed
Histogram (17 states)
97 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
39 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
142857:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
715883:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
265836:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
3343725:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
146762:>0:r3=2; 2:r1=0; 2:r4=1; y=2;
473791:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
9040765:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
19218702:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
60485400:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
19303489:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
74287202:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
78768323:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
51210359:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
37198276:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
45398494:>0:r3=2; 2:r1=2; 2:r4=0; 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 105.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 11,1
_litmus_P1_1_: stw 11,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,2
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: lwz 6,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 7,0(9)
Test bcssww007 Allowed
Histogram (16 states)
2 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
402268:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
89693 :>0:r3=1; 2:r1=1; 2:r3=0; y=2;
360420:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
1482385:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
4439708:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
8685785:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
19751125:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
84111515:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
77151378:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
19258119:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
59951356:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
35762163:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
683855:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
39823505:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
48046723:>0:r3=0; 2:r1=0; 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=66d340e023bd1d1ae19ed5903eb5d2ea
Cycle=SyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww007 No BCSyncsWW
Safe=Fre SyncdWR SyncdRR
Time bcssww007 104.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 8,1
_litmus_P0_1_: stw 8,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 7,0(9)
_litmus_P1_0_: li 11,1
_litmus_P1_1_: stw 11,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 10,2
_litmus_P1_4_: stw 10,0(9)
_litmus_P2_0_: lwz 6,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 7,0(9)
Test bcssww008 Allowed
Histogram (17 states)
51 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
9 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
182521:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
250591:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
75162 :>0:r3=1; 2:r1=1; 2:r3=0; y=2;
3326359:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
6564996:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
463483:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
1059555:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
19245140:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
60685364:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
38079382:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
74974005:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
83841977:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
50713881:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
18224274:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
42313250:>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 107.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 10,2
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: lwz 6,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 7,0(9)
_litmus_P2_0_: li 11,1
_litmus_P2_1_: stw 11,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 10,2
_litmus_P2_4_: stw 10,0(9)
_litmus_P3_0_: lwz 6,0(11)
_litmus_P3_1_: sync
_litmus_P3_2_: lwz 7,0(9)
Test bcssww009 Allowed
Histogram (72 states)
1549 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1358 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2220 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
28518 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1864 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2222 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1980 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
48025 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
224446:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
95664 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
6846 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
161730:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
475709:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
218984:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
209688:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
49242 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
629370:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1133790:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
344679:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
3459885:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
481562:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
490455:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1072958:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
217371:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
142039:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2762826:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
982397:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2157071:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2784740:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3286433:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
141710:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
65439 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
4835650:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3435020:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
4668057:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
242589:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2180025:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1788453:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
796648:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
958052:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
209515:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
19008471:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4643311:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
5060632:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
336964:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2050666:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
13053574:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
62512 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
797662:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
486772:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4801472:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
20664182:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
155923:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3838041:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
39528938:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3315077:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
17001833:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
17085975:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5141408:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
216204:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2752437:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
13048131:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3892891:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
637135:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1067097:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2063076:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2740009:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1795288:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
19138328:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1158752:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
20560140:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
53100320:>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 237.85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 10,2
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: lwz 6,0(11)
_litmus_P1_1_: sync
_litmus_P1_2_: lwz 7,0(9)
_litmus_P2_0_: li 11,1
_litmus_P2_1_: stw 11,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 10,2
_litmus_P2_4_: stw 10,0(9)
_litmus_P3_0_: lwz 6,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 7,0(9)
Test bcssww010 Allowed
Histogram (75 states)
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
5 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
5 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1834 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2694 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2809 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1451 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
48018 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
32544 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1809 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
7057 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2055 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
52037 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
382491:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
65715 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
609930:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
860277:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
981112:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
736134:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
291931:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
138471:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
156148:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
151330:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1532983:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
225987:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
62479 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
246354:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
852217:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
820402:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
231919:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
354963:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
220420:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
542583:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
189599:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
149413:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
452875:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
75893 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1253583:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1054407:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1141367:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1813066:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1739556:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2063568:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2303072:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2213766:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2107451:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4833851:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2731091:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4995902:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3299378:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3612835:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
5070510:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
18956221:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
12347839:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2812965:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3863121:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
5179945:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4640624:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
469348:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
4634268:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3349484:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4005412:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2843585:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1091749:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
375988:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
18317590:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3075126:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
13019355:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
20054921:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
16314171:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3457717:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
38918388:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
20933745:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
53817348:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
16803742:>1:r1=2; 1:r3=2; 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=fdf7665f1e0ce0f0c6d4d353ee548d9e
Cycle=LwSyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww010 No BCSyncsWW
Safe=Fre SyncdRR LwSyncdRR
Time bcssww010 237.17
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 10,2
_litmus_P0_4_: stw 10,0(9)
_litmus_P1_0_: lwz 6,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 7,0(9)
_litmus_P2_0_: li 11,1
_litmus_P2_1_: stw 11,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 10,2
_litmus_P2_4_: stw 10,0(9)
_litmus_P3_0_: lwz 6,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 7,0(9)