Tue Dec 29 15:09:19 CET 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr000
"Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr000 Allowed
Histogram (21 states)
133 :>3:r1=0; 3:r3=0; x=2; y=2;
290 :>3:r1=1; 3:r3=1; x=2; y=2;
75514 :>3:r1=1; 3:r3=0; x=1; y=1;
27148 :>3:r1=2; 3:r3=0; x=1; y=2;
94200 :>3:r1=1; 3:r3=0; x=1; y=2;
30089 :>3:r1=2; 3:r3=0; x=2; y=1;
133132:>3:r1=1; 3:r3=1; x=2; y=1;
596970:>3:r1=0; 3:r3=0; x=2; y=1;
29622 :>3:r1=0; 3:r3=1; x=2; y=2;
1878350:>3:r1=2; 3:r3=1; x=1; y=2;
1371860:>3:r1=1; 3:r3=1; x=1; y=2;
2859121:>3:r1=0; 3:r3=1; x=2; y=1;
2512667:>3:r1=2; 3:r3=0; x=1; y=1;
4647248:>3:r1=2; 3:r3=1; x=2; y=1;
1125452:>3:r1=0; 3:r3=0; x=1; y=2;
8216168:>3:r1=2; 3:r3=1; x=1; y=1;
1867243:>3:r1=0; 3:r3=1; x=1; y=1;
1509297:>3:r1=0; 3:r3=1; x=1; y=2;
9673757:>3:r1=0; 3:r3=0; x=1; y=1;
3351315:>3:r1=1; 3:r3=1; x=1; y=1;
424 :>3:r1=2; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=7074ebf0a4e494a7c168353216394741
Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr000 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr000 60.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr001
"Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | sync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr001 Allowed
Histogram (21 states)
119915:>3:r1=1; 3:r3=0; x=1; y=1;
1454 :>3:r1=0; 3:r3=0; x=2; y=2;
37709 :>3:r1=2; 3:r3=0; x=1; y=2;
1129 :>3:r1=2; 3:r3=1; x=2; y=2;
76805 :>3:r1=0; 3:r3=1; x=2; y=2;
95001 :>3:r1=1; 3:r3=0; x=1; y=2;
61101 :>3:r1=2; 3:r3=0; x=2; y=1;
264482:>3:r1=1; 3:r3=1; x=2; y=1;
1211581:>3:r1=0; 3:r3=1; x=1; y=2;
1561162:>3:r1=0; 3:r3=0; x=2; y=1;
1163526:>3:r1=1; 3:r3=1; x=1; y=2;
1583634:>3:r1=2; 3:r3=1; x=1; y=2;
7140312:>3:r1=2; 3:r3=1; x=1; y=1;
915631:>3:r1=0; 3:r3=1; x=1; y=1;
7261907:>3:r1=2; 3:r3=1; x=2; y=1;
1512010:>3:r1=0; 3:r3=0; x=1; y=2;
2055376:>3:r1=2; 3:r3=0; x=1; y=1;
3061376:>3:r1=0; 3:r3=1; x=2; y=1;
8535087:>3:r1=0; 3:r3=0; x=1; y=1;
3339986:>3:r1=1; 3:r3=1; x=1; y=1;
816 :>3:r1=1; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=42a8ec6eccd807ced6dea1376fc81b0b
Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr001 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr001 60.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr002
"Fre SyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | | lwz r3,0(r4) ;
li r3,1 | | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r11,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r10,0(r2)
Test aclwdrr002 Allowed
Histogram (9 states)
48830 :>2:r1=0; 2:r3=0; x=2;
4072602:>2:r1=2; 2:r3=0; x=1;
755862:>2:r1=1; 2:r3=1; x=2;
10515832:>2:r1=2; 2:r3=1; x=1;
3866159:>2:r1=0; 2:r3=1; x=1;
13028798:>2:r1=0; 2:r3=0; x=1;
3481536:>2:r1=1; 2:r3=1; x=1;
679152:>2:r1=2; 2:r3=1; x=2;
3551229:>2:r1=0; 2:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=e86498b53008de1e6a240afbf078cd14
Cycle=Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr002 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr002 37.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr003
"Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r11,0(r2)
_litmus_P1_0_: li r11,1
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr003 Allowed
Histogram (21 states)
681 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
781 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
389 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
92152 :>0:r3=1; 3:r1=1; 3:r3=0; y=1;
27530 :>0:r3=1; 3:r1=2; 3:r3=0; y=2;
57410 :>0:r3=0; 3:r1=0; 3:r3=1; y=2;
77828 :>0:r3=0; 3:r1=1; 3:r3=1; y=1;
1119752:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
76958 :>0:r3=1; 3:r1=1; 3:r3=0; y=2;
1219113:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
855566:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
4809806:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
1449521:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
5050791:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
162900:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
5530801:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
4362917:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
1386841:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
9592029:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
2665895:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
1460339:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=9599d8c79b2e28a1f015a74966a65bac
Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr003 No ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr003 55.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr004
"Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r9,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr004 Allowed
Histogram (38 states)
1096 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1059 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
924 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2539 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
25312 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
2997 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
6241 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
97799 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
5541 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
366360:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
96089 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
514657:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
36754 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
167704:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
291 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1279 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
39621 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
675907:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
705190:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
86475 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
1501025:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
3031116:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
2006624:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
1302535:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
3386963:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
2161343:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1065711:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
2288640:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
4133832:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
5807648:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
680124:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
1891861:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
2427751:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
151382:>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
419763:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
2912182:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
977615:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
1020050:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=32cc2d7800b6941b57852b520691800f
Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr004 No ACLwSyncdRR
Safe=Fre Wse SyncsWR SyncdWW
Time aclwdrr004 55.80
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr005
"Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr005 Allowed
Histogram (21 states)
213 :>3:r1=0; 3:r3=0; x=2; y=2;
3740 :>3:r1=1; 3:r3=1; x=2; y=2;
61102 :>3:r1=0; 3:r3=1; x=2; y=2;
98401 :>3:r1=1; 3:r3=0; x=1; y=1;
15605 :>3:r1=2; 3:r3=0; x=2; y=1;
174993:>3:r1=2; 3:r3=0; x=1; y=2;
519738:>3:r1=0; 3:r3=0; x=2; y=1;
526469:>3:r1=1; 3:r3=0; x=1; y=2;
2594711:>3:r1=2; 3:r3=0; x=1; y=1;
244141:>3:r1=1; 3:r3=1; x=2; y=1;
3004078:>3:r1=1; 3:r3=1; x=1; y=2;
2035744:>3:r1=0; 3:r3=0; x=1; y=2;
3951061:>3:r1=2; 3:r3=1; x=2; y=1;
2934132:>3:r1=0; 3:r3=1; x=2; y=1;
926843:>3:r1=0; 3:r3=1; x=1; y=2;
1242302:>3:r1=0; 3:r3=1; x=1; y=1;
6977696:>3:r1=2; 3:r3=1; x=1; y=1;
3736019:>3:r1=2; 3:r3=1; x=1; y=2;
7817401:>3:r1=0; 3:r3=0; x=1; y=1;
3131983:>3:r1=1; 3:r3=1; x=1; y=1;
3628 :>3:r1=2; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=4867d1504e0b1c594b9643e48c015b80
Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr005 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr005 60.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr006
"Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | lwsync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr006 Allowed
Histogram (21 states)
60558 :>3:r1=1; 3:r3=0; x=1; y=1;
4925 :>3:r1=0; 3:r3=0; x=2; y=2;
12425 :>3:r1=2; 3:r3=1; x=2; y=2;
12303 :>3:r1=1; 3:r3=1; x=2; y=2;
30092 :>3:r1=2; 3:r3=0; x=2; y=1;
131666:>3:r1=2; 3:r3=0; x=1; y=2;
288789:>3:r1=0; 3:r3=1; x=2; y=2;
1679148:>3:r1=2; 3:r3=0; x=1; y=1;
419709:>3:r1=1; 3:r3=0; x=1; y=2;
1508563:>3:r1=0; 3:r3=0; x=1; y=2;
1538485:>3:r1=0; 3:r3=0; x=2; y=1;
2999543:>3:r1=1; 3:r3=1; x=1; y=2;
2745112:>3:r1=1; 3:r3=1; x=1; y=1;
3869630:>3:r1=2; 3:r3=1; x=1; y=2;
2405650:>3:r1=0; 3:r3=1; x=2; y=1;
697008:>3:r1=0; 3:r3=1; x=1; y=1;
605433:>3:r1=0; 3:r3=1; x=1; y=2;
6227996:>3:r1=2; 3:r3=1; x=1; y=1;
7235261:>3:r1=0; 3:r3=0; x=1; y=1;
918554:>3:r1=1; 3:r3=1; x=2; y=1;
6609150:>3:r1=2; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=7e01ecd8b2bc06ff5ba0d2b4e58340c6
Cycle=Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr006 No ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr006 60.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr007
"Fre LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | | lwz r3,0(r4) ;
li r3,1 | | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r11,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r10,0(r2)
Test aclwdrr007 Allowed
Histogram (9 states)
487076:>2:r1=0; 2:r3=0; x=2;
1053120:>2:r1=0; 2:r3=1; x=1;
3091095:>2:r1=2; 2:r3=0; x=1;
9959870:>2:r1=2; 2:r3=1; x=1;
4047535:>2:r1=1; 2:r3=1; x=2;
12614899:>2:r1=0; 2:r3=0; x=1;
3008478:>2:r1=1; 2:r3=1; x=1;
4182150:>2:r1=2; 2:r3=1; x=2;
1555777:>2:r1=0; 2:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=ba17863040d25a62a648bb8030bf59fd
Cycle=Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr007 No ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr007 36.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr008
"Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r11,0(r2)
_litmus_P1_0_: li r11,1
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr008 Allowed
Histogram (21 states)
1145 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
10620 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
17131 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
87833 :>0:r3=0; 3:r1=2; 3:r3=0; y=1;
124890:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
1101816:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
210549:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
3751705:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
636404:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
280436:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
1883129:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
861940:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
190429:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
1241079:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
4809473:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
3022136:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
4716542:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
5039470:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
8595614:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
2490285:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
927374:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=61bd93196401321b8fb91e15727e3c64
Cycle=Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr008 No ACLwSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time aclwdrr008 55.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr009
"Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r9,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr009 Allowed
Histogram (39 states)
6 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
12759 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
495 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
383 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
226248:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
12321 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
17373 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
38456 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
113335:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
46172 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
68771 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
186410:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
420886:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
263527:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
60646 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
256634:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
294762:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
15890 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
840163:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
247212:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
2516382:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
139042:>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
2487585:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
4514972:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
2042436:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
524963:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
217988:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
3364599:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
2492535:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
1093156:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1706109:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
3184265:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
3870643:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
922618:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
2040380:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
2043421:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
2080524:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1221863:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
414070:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=ab46080bf73ab92da49cdd6b27ede9b2
Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr009 No ACLwSyncdRR
Safe=Fre Wse SyncsWR LwSyncdWW
Time aclwdrr009 55.32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr010
"Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ;
lwsync | stw r1,0(r2) | lwsync | stw r1,0(r2) ;
lwz r3,0(r4) | | lwz r3,0(r4) | ;
exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: lwz r11,0(r9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r11,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r10,0(r2)
_litmus_P3_0_: li r9,1
_litmus_P3_1_: stw r9,0(r2)
Test aclwdrr010 Allowed
Histogram (15 states)
244555:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
554146:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
399505:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
680154:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
712605:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
75523 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
2629091:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
5133341:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
270253:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
1858346:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
3007918:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
2543996:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
3043383:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
5226940:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
13620244:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=8ce05c9f86d49b2adfd5546bd471aa44
Cycle=Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr010 No ACLwSyncdRR
Safe=Fre
Time aclwdrr010 39.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr011
"Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
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) | | lwz r3,0(r4) ;
li r3,1 | | | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r11,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r10,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr011 Allowed
Histogram (15 states)
103 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
24648 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
2494 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
328368:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
61495 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
368826:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
2523779:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
3228537:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
3011847:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
4760339:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1291965:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
8792111:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
3960312:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
7937014:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
3708162:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=064d7a96bedb614c156f5bd3adf783d8
Cycle=Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr011 No ACLwSyncdRR
Safe=Fre SyncdWW
Time aclwdrr011 48.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr012
"Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
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) | | lwz r3,0(r4) ;
li r3,2 | | | ;
stw r3,0(r2) | | | ;
exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r11,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r10,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr012 Allowed
Histogram (33 states)
15 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
118 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
9405 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
14397 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2653 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
730 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
19844 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
134756:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
90982 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
151126:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
215500:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
17550 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
965114:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
457601:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
638193:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
251112:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
858852:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
2585167:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1820724:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
3263886:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
305752:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
4292667:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1678774:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1968259:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
829443:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
71623 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
3192705:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1515714:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
302435:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1586440:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
3412983:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
6425859:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
2919621:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=992754280de579a7f5feb516274ac846
Cycle=Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr012 No ACLwSyncdRR
Safe=Fre SyncsWW
Time aclwdrr012 49.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr013
"Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
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 ;
lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,1 | | | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r11,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r10,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr013 Allowed
Histogram (15 states)
3471 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
34411 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
7974 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
476119:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
215988:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
2150964:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
3013004:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
2321402:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
884430:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
598846:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
8258799:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
3238389:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
7466026:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
6739430:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
4590747:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=4eddb3c8ea9ccf8a71927b2e31094cad
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr013 No ACLwSyncdRR
Safe=Fre LwSyncdWW
Time aclwdrr013 47.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr014
"Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
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 ;
lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,2 | | | ;
stw r3,0(r2) | | | ;
exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r11,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r10,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr014 Allowed
Histogram (32 states)
5 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
60 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
27 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
2358 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1707 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
155399:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
26649 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
203255:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
9828 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
111908:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
204918:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
930824:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
68190 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1729410:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
408458:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
21952 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
300022:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
4625005:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
73446 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
804104:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
21099 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
323587:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
255682:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
82547 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
181064:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
2738537:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
2633173:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
4758597:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
3246308:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
2931251:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
12156289:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
994341:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=0363e525d1d5c107b6654781a780ef6a
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr014 No ACLwSyncdRR
Safe=Fre LwSyncsWW
Time aclwdrr014 49.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr015
"Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
li r3,1 | lwz r3,0(r4) | | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r11,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr015 Allowed
Histogram (15 states)
159 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
49962 :>1:r3=0; 3:r1=0; 3:r3=1; x=2;
1435 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
4465456:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
108865:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
959549:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
188561:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
2072771:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
814207:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
2995396:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
1333965:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
1968204:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
10337943:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
9046922:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
5656605:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=61d664ae95ff6d97da76ebb37bc47ca3
Cycle=Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr015 No ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr015 54.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr016
"Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | sync | | lwz r3,0(r4) ;
li r3,1 | lwz r3,0(r4) | | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r11,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr016 Allowed
Histogram (15 states)
3314 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
3952 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
68323 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
206493:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
105945:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
1955109:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
1544944:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
2268521:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
2637392:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
8522617:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
7994028:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
2845774:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
710412:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
2008724:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
9124452:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=4947e9ed11cb60630be5b54900bf7b6c
Cycle=Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr016 No ACLwSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time aclwdrr016 53.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr017
"Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | | ;
exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r11,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r11,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r10,0(r2)
Test aclwdrr017 Allowed
Histogram (7 states)
7651301:>0:r3=1; 2:r1=1; 2:r3=0;
3254270:>0:r3=0; 2:r1=0; 2:r3=1;
12966365:>0:r3=1; 2:r1=0; 2:r3=0;
2336847:>0:r3=1; 2:r1=0; 2:r3=1;
11427313:>0:r3=1; 2:r1=1; 2:r3=1;
2234912:>0:r3=0; 2:r1=1; 2:r3=1;
128992:>0:r3=0; 2:r1=0; 2:r3=0;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=0dd8df1959f84e11508b32d374a44775
Cycle=Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr017 No ACLwSyncdRR
Safe=Fre SyncdWR
Time aclwdrr017 34.39
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr018
"Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | lwz r3,0(r4) | | ;
exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r11,0(r2)
_litmus_P1_0_: li r10,1
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r11,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr018 Allowed
Histogram (15 states)
961 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
10920 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
75412 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
292256:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
1377939:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
2095357:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
2793104:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
3420998:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
4191394:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
1186498:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
8994618:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
8552193:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1;
1134718:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
5723167:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
150465:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=3fed6cc74892902ab28df779672578f8
Cycle=Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr018 No ACLwSyncdRR
Safe=Fre SyncdWR
Time aclwdrr018 49.71
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr019
"Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r2) | lwz r3,0(r4) | | ;
exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r9,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r11,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr019 Allowed
Histogram (31 states)
1 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
14800 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
3700 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1739 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
441 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
331005:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
826223:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
704199:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
49228 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
8913 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1175002:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
2254374:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
9609 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
2897985:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
690544:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
44169 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
2035143:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
2855066:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
70038 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1484267:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
772455:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
280103:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
101958:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
2816512:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
2269758:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
2339244:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
4108885:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
4264447:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
6770691:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
480982:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
338519:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=660c5e262906b3ab9066962d8bf69882
Cycle=Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr019 No ACLwSyncdRR
Safe=Fre SyncsWR SyncdWR
Time aclwdrr019 51.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr020
"Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | lwz r3,0(r2) | | ;
exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r11,0(r2)
_litmus_P1_0_: li r11,1
_litmus_P1_1_: stw r11,0(r2)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r9,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r11,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r10,0(r2)
Test aclwdrr020 Allowed
Histogram (45 states)
2 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
131 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
426 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
137 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
2512 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
22 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
16687 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
831935:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
40199 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
13440 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
261320:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
309 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
381002:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
124 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
39251 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
111094:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
12542 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
418110:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
99062 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
836989:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
1455469:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
213734:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
3072345:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
2635554:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
664980:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
12211 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
255063:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
723704:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
370371:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
421520:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
417120:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
2432923:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
1242564:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
2004937:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
1943726:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
855541:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
271567:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
3710957:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
3740495:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
823899:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
5010885:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
2062676:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
2173875:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
418207:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
383 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=bad92812900a1656a66221eff19f711e
Cycle=Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR
Relax aclwdrr020 No ACLwSyncdRR
Safe=Fre SyncsWR SyncdWR
Time aclwdrr020 52.76
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O2 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 -O2"
LITMUSOPTS=-r 40
Tue Dec 29 15:27:06 CET 2009