Mon Dec 28 10:23:00 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 (78 states)
1 :>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
2 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
3 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
5 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
1636 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
1627 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
3119 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
7756 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
3387 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
3174 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
3780 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
6755 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
1698 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
34298 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
3419 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1481 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
25822 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
33439 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
25683 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
76250 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
721770:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
507281:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
496590:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
110292:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
176080:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
687286:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
167852:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
783676:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
36033 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
788720:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
83892 :>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
2148237:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
2146617:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
1316009:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
75608 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
4721333:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
108340:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
672343:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
658395:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3536865:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
1330590:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
2869396:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
2400356:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
86205 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
4858758:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
3273463:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
1127839:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
3537358:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
1431743:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
4958007:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
2175803:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
1413031:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
10529865:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
2282502:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2465572:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
1112542:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
2278661:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
4245759:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
19978449:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
4108204:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
19514196:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
14355639:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
3771862:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
4323386:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
10578249:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
4603226:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
3166044:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
3627938:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
14258785:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
2340798:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
4336254:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
19626221:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
2768536:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
40116871:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
19665602:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
56305734:>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 94.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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=1; 3:r1=2; 3:r3=0; 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=0; 3:r1=1; 3:r3=0; x=2; y=2;
1266 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
3064 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1189 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3060 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1227 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
6885 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1650 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
34346 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
11153 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
258527:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
13060 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
32474 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
22962 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
54868 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
121993:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
38548 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
209046:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
197794:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
594093:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
353510:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
793805:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
244146:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1005411:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
303241:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1085225:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1972673:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
68894 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
140273:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
613110:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
3304167:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
558568:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
2058043:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
471501:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
886020:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
4241906:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
709716:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
123869:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2224552:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1809693:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1064341:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2001720:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
384200:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2787566:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
4850739:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
3417559:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
1283728:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
3453397:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
1832598:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1848099:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
5174059:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
2175310:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
13483679:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
5694531:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
14180882:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
10270732:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3573519:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
4415758:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3785611:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
3743142:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
980908:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
22191923:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
3037416:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
19291906:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
17276010:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
1430385:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
3061044:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
58561902:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
3875652:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
2320809:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
36270794:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
18203135:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
19501414:>1:r1=2; 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=c19feeb22b3e4fe95d3ae9cd399e4667
Cycle=SyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww001 No BCSyncsWW
Safe=Fre SyncdRR DpdR
Time bcssww001 95.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (77 states)
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>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=2; 3:r3=1; x=2; y=2;
8 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
10 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1439 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
1566 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1510 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
4100 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
1763 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3713 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
8341 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
11483 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
38779 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
24549 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
266777:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
35134 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
49076 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
235328:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
115868:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
32193 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
67483 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
191231:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
123734:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
724027:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
353254:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
13207 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1893630:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
2339636:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
649498:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1220666:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
586864:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
575182:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
127187:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
2829306:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1027885:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
283384:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
996836:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
2166693:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1385068:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
411196:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
1917394:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
3292704:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
776215:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
3599698:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
3027479:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
2194378:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
1703594:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
1414794:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
182137:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2407754:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
2061450:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
4140451:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
1087021:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
4454504:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3621277:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
4288680:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
3735828:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
914790:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
5066009:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
506523:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
59425775:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
2027435:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
5292298:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
4785766:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
19595067:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
3680588:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
3446113:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
12913843:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
10340917:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3480734:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
21692791:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
13590243:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
17770325:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
16973779:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
20148203:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
35645836:>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=a2812688a109c131b01004a694cfdd81
Cycle=LwSyncdRR Fre SyncsWW Rfe DpdR Fre SyncsWW Rfe
Relax bcssww002 No BCSyncsWW
Safe=Fre LwSyncdRR DpdR
Time bcssww002 94.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
8 :>0:r3=1; 2:r1=2; x=2; y=2;
38 :>0:r3=0; 2:r1=1; x=2; y=2;
357614:>0:r3=1; 2:r1=0; x=1; y=2;
3204713:>0:r3=1; 2:r1=2; x=1; y=2;
193744:>0:r3=2; 2:r1=0; x=1; y=2;
1612452:>0:r3=1; 2:r1=1; x=1; y=2;
7590621:>0:r3=2; 2:r1=1; x=2; y=2;
2106804:>0:r3=2; 2:r1=1; x=1; y=2;
17584920:>0:r3=1; 2:r1=0; x=2; y=2;
166760:>0:r3=1; 2:r1=1; x=2; y=2;
71667990:>0:r3=0; 2:r1=0; x=1; y=2;
18047336:>0:r3=0; 2:r1=1; x=1; y=2;
60865075:>0:r3=2; 2:r1=0; x=2; y=2;
35705443:>0:r3=2; 2:r1=2; x=2; y=2;
52741688:>0:r3=0; 2:r1=0; x=2; y=2;
40682430:>0:r3=0; 2:r1=2; x=1; y=2;
87472364:>0:r3=2; 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 74.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (16 states)
1 :>0:r3=0; 2:r1=1; x=2; y=2;
473432:>0:r3=1; 2:r1=0; x=1; y=2;
134247:>0:r3=1; 2:r1=1; x=2; y=2;
4123813:>0:r3=2; 2:r1=1; x=1; y=2;
2193777:>0:r3=1; 2:r1=1; x=1; y=2;
786394:>0:r3=2; 2:r1=0; x=1; y=2;
3515489:>0:r3=1; 2:r1=2; x=1; y=2;
6938262:>0:r3=2; 2:r1=1; x=2; y=2;
17654337:>0:r3=0; 2:r1=1; x=1; y=2;
18299083:>0:r3=1; 2:r1=0; x=2; y=2;
86051363:>0:r3=0; 2:r1=0; x=1; y=2;
91556357:>0:r3=2; 2:r1=2; x=1; y=2;
41879307:>0:r3=0; 2:r1=0; x=2; y=2;
36406824:>0:r3=0; 2:r1=2; x=1; y=2;
28731046:>0:r3=2; 2:r1=2; x=2; y=2;
61256268:>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=4a84f5a0d5b5b42156717d2ee2b4312f
Cycle=SyncdRW Wse SyncdWR Fre SyncsWW Rfe
Relax bcssww004 No BCSyncsWW
Safe=Fre Wse SyncdWR SyncdRW
Time bcssww004 72.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (17 states)
2 :>0:r3=1; 2:r1=2; x=2; y=2;
4 :>0:r3=0; 2:r1=1; x=2; y=2;
422354:>0:r3=2; 2:r1=0; x=1; y=2;
182851:>0:r3=1; 2:r1=1; x=2; y=2;
3915154:>0:r3=2; 2:r1=1; x=1; y=2;
538982:>0:r3=1; 2:r1=0; x=1; y=2;
49235334:>0:r3=0; 2:r1=0; x=2; y=2;
16686084:>0:r3=0; 2:r1=1; x=1; y=2;
2367976:>0:r3=1; 2:r1=1; x=1; y=2;
7650025:>0:r3=2; 2:r1=1; x=2; y=2;
3624287:>0:r3=1; 2:r1=2; x=1; y=2;
78268832:>0:r3=0; 2:r1=0; x=1; y=2;
88115033:>0:r3=2; 2:r1=2; x=1; y=2;
17953462:>0:r3=1; 2:r1=0; x=2; y=2;
37118798:>0:r3=0; 2:r1=2; x=1; y=2;
31480743:>0:r3=2; 2:r1=2; x=2; y=2;
62440079:>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 77.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
76 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
45 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
298813:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
90875 :>0:r3=2; 2:r1=0; 2:r4=1; y=2;
766859:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
3739395:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
7786127:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
1318918:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
321178:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
18147926:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
18516599:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
80998724:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
61000881:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
37716122:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
42582384:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
53805314:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
72909764:>0:r3=0; 2:r1=0; 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 75.91
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (17 states)
3 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
1 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
3415354:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
234983:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
2329269:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
341541:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
2938122:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
261118:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
18404583:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
84592684:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
37262014:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
77686519:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
35662070:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
51385774:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
16776128:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
7755627:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
60954210:>0:r3=2; 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 74.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
16 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
34 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
321651:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
275595:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
3342935:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
240478:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
2261587:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
37339928:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
8668646:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
2762616:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
16309185:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
17878836:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
37834495:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
61621886:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
82184633:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
76333171:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
52624308:>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=d19882d97477fc15c9e4fbc588dc8a96
Cycle=LwSyncdRR Fre SyncdWR Fre SyncsWW Rfe
Relax bcssww008 No BCSyncsWW
Safe=Fre SyncdWR LwSyncdRR
Time bcssww008 77.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (72 states)
1041 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1968 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1107 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1342 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1373 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2540 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
8720 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
50906 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
71043 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
49923 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
145125:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
39014 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
326703:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
932884:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
133089:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
343515:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
561264:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
283996:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
223133:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
335017:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1277903:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
224508:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2147519:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1145071:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
967272:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
317627:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
4194220:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
288359:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
789413:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
324019:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
589962:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
273713:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1786446:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
356846:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
836551:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
788355:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3706619:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3799341:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
6014642:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
750012:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1663571:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
698452:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1700947:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
19750764:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
5867617:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1211592:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2243095:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
13625862:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1333628:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1830026:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
4453455:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4539428:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4263687:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2673171:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2559045:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2179359:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
4283202:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2374648:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2856943:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2059169:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2683776:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
17272630:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4216109:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
751071:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2935905:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
33262624:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
17112998:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
57617513:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
16656611:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
20205189:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
13717993:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
17307819:>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=ac99317f895df8ed08197fb9ed0e136a
Cycle=SyncdRR Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe
Relax bcssww009 No BCSyncsWW
Safe=Fre SyncdRR
Time bcssww009 92.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
5 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1542 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1046 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
993 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2392 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1570 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
9089 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
3200 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
41251 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
70106 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
25797 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
896893:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
17174 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
116478:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
283701:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
793612:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
271662:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
277347:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
793247:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
309824:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
746573:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
117915:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
754513:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
588297:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2283287:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
228386:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
330227:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
249807:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1733131:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1190748:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2165237:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
4062390:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
584773:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
205522:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1013602:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
753364:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1596208:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3196098:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
3665164:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
234170:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
3242659:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
295572:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
709756:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2065234:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2505072:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1753473:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4217281:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
5252383:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
3745808:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1316912:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1309336:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2660993:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1917206:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1774417:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
4051750:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1232484:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
4319225:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
13168306:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
16224010:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5839826:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2943972:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
19655199:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
18095404:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
315143:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4281249:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
20769005:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
16244660:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
2718257:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
58985075:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
13638287:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4469249:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
33744479:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
16921973:>1:r1=0; 1:r3=0; 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: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 93.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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=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;
3 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2425 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1986 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1528 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1519 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1856 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2949 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
11194 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
28572 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
8431 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
247709:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
106617:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
101617:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
79843 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
286999:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
228922:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
727157:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
244845:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
245836:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
304411:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
303497:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
701349:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
200471:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
26447 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
248065:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
532390:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
197756:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1237864:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
838101:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1418633:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1372495:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3502606:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
224312:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
734689:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1879916:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
753937:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1929247:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
3451111:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3670386:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
5588423:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1142770:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
504943:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
791437:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
717943:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1713954:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
16450252:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1222231:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4183821:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
786687:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
15975311:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3930002:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
3972875:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3581270:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4262048:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1701194:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2701032:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1935658:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1955784:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
3134385:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
1258525:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2855567:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
13236204:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3544545:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
13063443:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
33671947:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5291467:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
60081531:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
20836044:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3656162:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
21273365:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
18042806:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3129889:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
17948784:>1:r1=0; 1:r3=0; 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: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 97.79
$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=
Mon Dec 28 10:40:01 GMT 2009