Fri Jan 1 15:58:00 GMT 2010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P3_1_: xor 10,28,28
_litmus_P3_2_: lwzx 30,10,9
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,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 (75 states)
3 :>1:r1=1; 1:r4=0; 3:r1=1; 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;
4193 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
6720 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
5518 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
3660 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
10001 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
16184 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
12399 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
3889 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
11813 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
82561 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
3924 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
28463 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
96065 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
162514:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
212976:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=2;
830796:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
425201:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
284652:>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
3203897:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
804733:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; x=2; y=2;
288245:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=1; x=2; y=2;
1436667:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; x=2; y=2;
1108146:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
149033:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=2; y=2;
445021:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
1696511:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
382578:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
87173 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
99210 :>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
1236502:>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2634265:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
3779143:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
5000928:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
4529679:>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
242493:>1:r1=1; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=2;
1705975:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=2;
5666866:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
5125716:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; x=2; y=2;
7123842:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=1; x=2; y=2;
3001863:>1:r1=2; 1:r4=1; 3:r1=1; 3:r4=2; x=2; y=2;
6886492:>1:r1=2; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=2;
3858103:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
10433285:>1:r1=1; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
28067188:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=2;
1643458:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
1548480:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
39553445:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
4255366:>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=2;
1912508:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=0; x=2; y=2;
6092048:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; x=2; y=2;
9109614:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=2;
9062597:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=2; y=2;
28142414:>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
6292927:>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
24276529:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
1811651:>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=0; x=2; y=2;
4003571:>1:r1=2; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
2186180:>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
7759450:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=0; x=2; y=2;
9284177:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
9293207:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=2; y=2;
23987098:>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
6538217:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
40129237:>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
9924499:>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=2; x=2; y=2;
6077491:>1:r1=2; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=2;
8054348:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
4380587:>1:r1=1; 1:r4=2; 3:r1=2; 3:r4=0; x=2; y=2;
40719420:>1:r1=2; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=2;
107417248:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=2;
39959484:>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=2;
85389659:>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 176.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,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=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;
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
5340 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
3872 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
3545 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
52765 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
18933 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
5709 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
4383 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
4526 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
54027 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
24476 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
571704:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
76358 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
1270938:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1622424:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
200987:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
733420:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
323538:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
424371:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
167912:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
159399:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
489093:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
1807403:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
6315584:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
635889:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
348127:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
561831:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
918951:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
618403:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
4790571:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
7423948:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
4845497:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1695778:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
10349084:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
2039354:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
8891577:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
3770159:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
618133:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
2739915:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
25865079:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
3427745:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
5000103:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
3649692:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
8489073:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
5823194:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
1420016:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
5718856:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
1045356:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
5285796:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
2750488:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
2436656:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1241186:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
10939880:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
1875532:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
3806207:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
9508262:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
7271089:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
8583304:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
3774485:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
5969811:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
24284866:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
39314878:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
42387368:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
10923793:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
75522313:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
34171186:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
1730934:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
3935335:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
36649768:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
28478739:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
35500864:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
7596794:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
111033425:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 177.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: sync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 28,0(11)
_litmus_P1_1_: xor 10,28,28
_litmus_P1_2_: lwzx 30,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 (76 states)
1 :>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
2788 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
3706 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
4615 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
4067 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
5645 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
35160 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
46712 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
56309 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
41174 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
627535:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
22100 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
129877:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
4374 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1262441:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
137757:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
946842:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
556090:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
1078284:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
299795:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
757036:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
1746615:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=2;
1875397:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
487612:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
400613:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=2;
618817:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=2;
416674:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
4109087:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
3916783:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
2220965:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1073721:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=2;
8396687:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
1725385:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
1557973:>1:r1=1; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
7764700:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
6285278:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
4785674:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=2;
5885084:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
224207:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=2; y=2;
5258542:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; x=2; y=2;
2643082:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
1904105:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=0; x=2; y=2;
1307521:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
4017209:>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=2;
9281888:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
9733162:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
1948506:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; x=2; y=2;
5352189:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=2;
8069194:>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=0; x=2; y=2;
11250165:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=2;
4659943:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=2;
2813704:>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=2; x=2; y=2;
6280760:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=0; x=2; y=2;
1996658:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
5694007:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
27812079:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
3262921:>1:r1=2; 1:r4=0; 3:r1=1; 3:r3=2; x=2; y=2;
4692620:>1:r1=2; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
7186424:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
34921868:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=2;
2822671:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=2;
10771840:>1:r1=1; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
3861726:>1:r1=1; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
39011408:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
11471490:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=2; y=2;
24318192:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
24311692:>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=2;
9211454:>1:r1=2; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=2;
74703515:>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=2;
33827628:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=2;
40787361:>1:r1=2; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=2;
36026594:>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=0; x=2; y=2;
109274298:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 178.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: xor 30,28,28
_litmus_P2_2_: li 10,1
_litmus_P2_3_: stwx 10,30,9
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,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;
32 :>0:r3=0; 2:r1=1; x=2; y=2;
446661:>0:r3=2; 2:r1=0; x=1; y=2;
838348:>0:r3=1; 2:r1=0; x=1; y=2;
751671:>0:r3=1; 2:r1=1; x=2; y=2;
18909981:>0:r3=2; 2:r1=1; x=2; y=2;
34068817:>0:r3=1; 2:r1=0; x=2; y=2;
11721949:>0:r3=1; 2:r1=2; x=1; y=2;
8263019:>0:r3=1; 2:r1=1; x=1; y=2;
6847963:>0:r3=2; 2:r1=1; x=1; y=2;
36047227:>0:r3=0; 2:r1=1; x=1; y=2;
65296017:>0:r3=2; 2:r1=2; x=2; y=2;
108750877:>0:r3=0; 2:r1=0; x=2; y=2;
153744447:>0:r3=0; 2:r1=0; x=1; y=2;
165337287:>0:r3=2; 2:r1=2; x=1; y=2;
117617258:>0:r3=2; 2:r1=0; x=2; y=2;
71358440:>0:r3=0; 2:r1=2; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 104.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww004 Allowed
Histogram (15 states)
345986:>0:r3=1; 2:r1=1; x=2; y=2;
15459570:>0:r3=2; 2:r1=1; x=2; y=2;
11358596:>0:r3=2; 2:r1=1; x=1; y=2;
35847023:>0:r3=0; 2:r1=1; x=1; y=2;
2239679:>0:r3=2; 2:r1=0; x=1; y=2;
34547946:>0:r3=1; 2:r1=0; x=2; y=2;
69854378:>0:r3=0; 2:r1=2; x=1; y=2;
8757888:>0:r3=1; 2:r1=1; x=1; y=2;
77486964:>0:r3=0; 2:r1=0; x=2; y=2;
10910585:>0:r3=1; 2:r1=2; x=1; y=2;
1784782:>0:r3=1; 2:r1=0; x=1; y=2;
176774293:>0:r3=2; 2:r1=2; x=1; y=2;
124338659:>0:r3=2; 2:r1=0; x=2; y=2;
54261508:>0:r3=2; 2:r1=2; x=2; y=2;
176032143:>0:r3=0; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 102.58
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,1
_litmus_P2_3_: stw 30,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,2
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww005 Allowed
Histogram (15 states)
537233:>0:r3=1; 2:r1=1; x=2; y=2;
1589024:>0:r3=1; 2:r1=0; x=1; y=2;
10851184:>0:r3=1; 2:r1=2; x=1; y=2;
8668096:>0:r3=1; 2:r1=1; x=1; y=2;
10299070:>0:r3=2; 2:r1=1; x=1; y=2;
35784864:>0:r3=0; 2:r1=1; x=1; y=2;
68562370:>0:r3=0; 2:r1=2; x=1; y=2;
1184837:>0:r3=2; 2:r1=0; x=1; y=2;
34478020:>0:r3=1; 2:r1=0; x=2; y=2;
57940245:>0:r3=2; 2:r1=2; x=2; y=2;
171519598:>0:r3=2; 2:r1=2; x=1; y=2;
126245704:>0:r3=2; 2:r1=0; x=2; y=2;
17323807:>0:r3=2; 2:r1=1; x=2; y=2;
88090045:>0:r3=0; 2:r1=0; x=2; y=2;
166925903:>0:r3=0; 2:r1=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 103.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: xor 10,28,28
_litmus_P2_2_: lwzx 30,10,9
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww006 Allowed
Histogram (17 states)
27 :>0:r3=0; 2:r1=1; 2:r4=0; y=2;
8 :>0:r3=1; 2:r1=2; 2:r4=0; y=2;
724864:>0:r3=1; 2:r1=0; 2:r4=1; y=2;
313598:>0:r3=2; 2:r1=0; 2:r4=1; y=2;
8401455:>0:r3=1; 2:r1=2; 2:r4=1; y=2;
811558:>0:r3=1; 2:r1=1; 2:r4=0; y=2;
6266302:>0:r3=1; 2:r1=1; 2:r4=1; y=2;
29757008:>0:r3=1; 2:r1=0; 2:r4=0; y=2;
68120806:>0:r3=2; 2:r1=2; 2:r4=0; y=2;
4431939:>0:r3=2; 2:r1=1; 2:r4=1; y=2;
36922684:>0:r3=0; 2:r1=1; 2:r4=1; y=2;
169477911:>0:r3=2; 2:r1=2; 2:r4=1; y=2;
100091022:>0:r3=0; 2:r1=0; 2:r4=0; y=2;
140987078:>0:r3=0; 2:r1=0; 2:r4=1; y=2;
19093100:>0:r3=2; 2:r1=1; 2:r4=0; y=2;
132250532:>0:r3=2; 2:r1=0; 2:r4=0; y=2;
82350108:>0:r3=0; 2:r1=2; 2:r4=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 100.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: sync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww007 Allowed
Histogram (15 states)
907406:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
9025702:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
622181:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
8290009:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
8054729:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
840528:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
36437679:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
74462901:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
32738446:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
131780331:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
17957711:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
64167251:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
93796850:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
153364676:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
167553600:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 101.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 28,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 30,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 30,1
_litmus_P0_1_: stw 30,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test bcssww008 Allowed
Histogram (17 states)
9 :>0:r3=1; 2:r1=2; 2:r3=0; y=2;
7 :>0:r3=0; 2:r1=1; 2:r3=0; y=2;
857297:>0:r3=1; 2:r1=1; 2:r3=0; y=2;
598971:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
776429:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
9093834:>0:r3=1; 2:r1=2; 2:r3=1; y=2;
8028452:>0:r3=1; 2:r1=1; 2:r3=1; y=2;
17589127:>0:r3=2; 2:r1=1; 2:r3=0; y=2;
31285751:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
7930286:>0:r3=2; 2:r1=1; 2:r3=1; y=2;
77401229:>0:r3=0; 2:r1=2; 2:r3=1; y=2;
66998897:>0:r3=2; 2:r1=2; 2:r3=0; y=2;
150760512:>0:r3=0; 2:r1=0; 2:r3=1; y=2;
133317101:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
95939402:>0:r3=0; 2:r1=0; 2:r3=0; y=2;
164850834:>0:r3=2; 2:r1=2; 2:r3=1; y=2;
34571862:>0:r3=0; 2:r1=1; 2:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 800000000
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 101.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,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 30,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)
3694 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
4459 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
3911 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2655 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
2914 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
118757:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
142303:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
353299:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
776316:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
4886 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
696227:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
17489 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
362030:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
903241:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1509140:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1726235:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1550386:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
801461:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3995877:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
896311:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1698197:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
587729:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1307516:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
728804:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
560790:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
81087 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
4824689:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
5627846:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
8450518:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1548125:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3702755:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2260501:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
816807:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
8533222:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
4356356:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
3196095:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4804225:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
39993049:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3885738:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
767958:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2013244:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
7724172:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
522234:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
11402263:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2594476:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
9042992:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2152418:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
3077525:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2624312:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
30764339:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
9001977:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
10091292:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
33407771:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
32885903:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2050769:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
8916542:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3114280:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
9313241:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4499230:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
1631796:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
165064:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1236557:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
34267391:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
28587812:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3838597:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
30600230:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
11289295:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
4741708:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
112431962:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
68237599:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
40311375:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
5858036:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 176.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,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 30,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 (74 states)
1 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3417 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
3838 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
3185 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
4334 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2942 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
20822 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
106028:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1677892:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
5046 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
330872:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
69655 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
666822:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
669829:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
100695:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1749398:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
4873442:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
748349:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
342965:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
792425:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
3710774:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
681124:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
822821:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
904352:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1784606:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1661003:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1585256:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
9119551:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
139107:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1204916:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2700555:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
577007:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
8435461:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
4440852:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
2010900:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2726982:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1950104:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
721044:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
549383:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
4378505:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
4171164:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
4938834:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
5567721:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
7825279:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
588165:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
30616746:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3773632:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
5792143:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
2140911:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
3790001:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
11193263:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2354703:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
30870064:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4461770:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
8829176:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
3315223:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4800979:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
11866596:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3282888:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
8582745:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1454648:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
10216062:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
8603155:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
32095454:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
38422861:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
9649645:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
28517410:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1271848:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
69361591:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
33973258:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
32820455:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
39333474:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
113241874:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 176.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 30,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,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 30,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 (76 states)
1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>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=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
3676 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
30692 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2999 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
4611 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
4773 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
5112 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
64232 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
70789 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1433368:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
408410:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1126679:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
3005 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
401862:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
780541:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
739064:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3733463:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
579008:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1645917:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
634271:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
828030:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1388590:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2237954:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
717955:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
109945:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
924894:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
849793:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
90635 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1934028:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
621146:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1415889:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4070657:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
1782518:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
1186043:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
4869766:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1947457:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1823440:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
8431119:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
7969425:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
8657389:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2224155:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
5922708:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
4792166:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3244175:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2038959:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
8851274:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
9026447:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3895297:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2805348:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
9566134:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4768817:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2211067:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2843275:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
9034619:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
4076437:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
4365901:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
11812910:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
29895148:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
9786568:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
6010450:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
3114338:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
29066226:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
68136873:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4905340:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
32770676:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
32520031:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
31650259:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
11178672:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
38751158:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
28436227:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4449257:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
38688456:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
115631481:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 640000000
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 178.04
$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: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=-s 80000 -r 1000
Fri Jan 1 16:26:00 GMT 2010