Sun Dec 27 15:23:05 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 r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr000 Allowed
Histogram (21 states)
148 :>3:r1=0; 3:r3=0; x=2; y=2;
578 :>3:r1=2; 3:r3=1; x=2; y=2;
35868 :>3:r1=0; 3:r3=1; x=2; y=2;
364 :>3:r1=1; 3:r3=1; x=2; y=2;
66193 :>3:r1=1; 3:r3=0; x=1; y=1;
27261 :>3:r1=2; 3:r3=0; x=1; y=2;
29634 :>3:r1=2; 3:r3=0; x=2; y=1;
167122:>3:r1=1; 3:r3=0; x=1; y=2;
550575:>3:r1=0; 3:r3=0; x=2; y=1;
1739428:>3:r1=0; 3:r3=0; x=1; y=2;
1481748:>3:r1=2; 3:r3=1; x=1; y=2;
2570494:>3:r1=2; 3:r3=0; x=1; y=1;
2942967:>3:r1=1; 3:r3=1; x=1; y=1;
1158326:>3:r1=1; 3:r3=1; x=1; y=2;
1563141:>3:r1=0; 3:r3=1; x=1; y=2;
1926447:>3:r1=0; 3:r3=1; x=1; y=1;
4039282:>3:r1=0; 3:r3=1; x=2; y=1;
7331971:>3:r1=2; 3:r3=1; x=1; y=1;
10009888:>3:r1=0; 3:r3=0; x=1; y=1;
153458:>3:r1=1; 3:r3=1; x=2; y=1;
4205107:>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=7074ebf0a4e494a7c168353216394741
Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr000 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr000 59.87
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr001 Allowed
Histogram (21 states)
4191 :>3:r1=0; 3:r3=0; x=2; y=2;
24815 :>3:r1=2; 3:r3=0; x=1; y=2;
963 :>3:r1=1; 3:r3=1; x=2; y=2;
78281 :>3:r1=1; 3:r3=0; x=1; y=2;
144944:>3:r1=2; 3:r3=0; x=2; y=1;
65148 :>3:r1=1; 3:r3=0; x=1; y=1;
90582 :>3:r1=0; 3:r3=1; x=2; y=2;
2345787:>3:r1=2; 3:r3=0; x=1; y=1;
220908:>3:r1=1; 3:r3=1; x=2; y=1;
1324290:>3:r1=1; 3:r3=1; x=1; y=2;
1866586:>3:r1=0; 3:r3=0; x=2; y=1;
1034157:>3:r1=0; 3:r3=0; x=1; y=2;
1902655:>3:r1=2; 3:r3=1; x=1; y=2;
1330543:>3:r1=0; 3:r3=1; x=1; y=2;
3413640:>3:r1=0; 3:r3=1; x=2; y=1;
1076081:>3:r1=0; 3:r3=1; x=1; y=1;
6851329:>3:r1=2; 3:r3=1; x=2; y=1;
6837772:>3:r1=2; 3:r3=1; x=1; y=1;
8107969:>3:r1=0; 3:r3=0; x=1; y=1;
3277772:>3:r1=1; 3:r3=1; x=1; y=1;
1587 :>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=42a8ec6eccd807ced6dea1376fc81b0b
Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr001 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr001 60.80
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r30,0(r2)
Test aclwdrr002 Allowed
Histogram (9 states)
794827:>2:r1=2; 2:r3=1; x=2;
5256344:>2:r1=2; 2:r3=0; x=1;
17345 :>2:r1=0; 2:r3=0; x=2;
682529:>2:r1=1; 2:r3=1; x=2;
3122305:>2:r1=0; 2:r3=1; x=2;
10263258:>2:r1=2; 2:r3=1; x=1;
3060781:>2:r1=0; 2:r3=1; x=1;
3696752:>2:r1=1; 2:r3=1; x=1;
13105859:>2:r1=0; 2:r3=0; x=1;
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 38.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r3,0(r2)
_litmus_P1_0_: li r30,1
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr003 Allowed
Histogram (21 states)
540 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
559 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
103367:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
21641 :>0:r3=1; 3:r1=2; 3:r3=0; y=2;
158042:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
67985 :>0:r3=1; 3:r1=1; 3:r3=0; y=2;
82801 :>0:r3=0; 3:r1=0; 3:r3=1; y=2;
392 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
115325:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
949966:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
1138699:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
1362572:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
5928068:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
1499973:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
1512480:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
5321360:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
4182302:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
1462481:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
9427893:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
2759742:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
3903812:>0:r3=0; 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=9599d8c79b2e28a1f015a74966a65bac
Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr003 No ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr003 56.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r4,0(r2)
_litmus_P1_0_: li r4,2
_litmus_P1_1_: stw r4,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr004 Allowed
Histogram (39 states)
1 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
923 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
1141 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1899 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
892 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4609 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1220 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3158 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
196 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
6864 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
89622 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
18211 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
38891 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
502034:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
110909:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
405244:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
937024:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
758837:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
38774 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1988790:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
3271330:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
561585:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
671199:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
1860841:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
2995798:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1765514:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1529404:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
131741:>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
505398:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1801258:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1485680:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
5954637:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
2604746:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
2397712:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
4494607:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
1724773:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
88152 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
983446:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
262940:>0:r3=1; 3:r1=0; 3:r3=0; 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=32cc2d7800b6941b57852b520691800f
Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr004 No ACLwSyncdRR
Safe=Fre Wse SyncsWR SyncdWW
Time aclwdrr004 59.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr005 Allowed
Histogram (21 states)
292 :>3:r1=0; 3:r3=0; x=2; y=2;
6564 :>3:r1=2; 3:r3=1; x=2; y=2;
6883 :>3:r1=1; 3:r3=1; x=2; y=2;
128455:>3:r1=1; 3:r3=0; x=1; y=1;
19208 :>3:r1=2; 3:r3=0; x=2; y=1;
219580:>3:r1=2; 3:r3=0; x=1; y=2;
637377:>3:r1=1; 3:r3=0; x=1; y=2;
90966 :>3:r1=0; 3:r3=1; x=2; y=2;
2537752:>3:r1=2; 3:r3=0; x=1; y=1;
484871:>3:r1=0; 3:r3=0; x=2; y=1;
2655027:>3:r1=1; 3:r3=1; x=1; y=2;
1510558:>3:r1=0; 3:r3=0; x=1; y=2;
2747664:>3:r1=1; 3:r3=1; x=1; y=1;
984054:>3:r1=0; 3:r3=1; x=1; y=2;
1101921:>3:r1=0; 3:r3=1; x=1; y=1;
5016496:>3:r1=2; 3:r3=1; x=2; y=1;
3764222:>3:r1=2; 3:r3=1; x=1; y=2;
6414676:>3:r1=2; 3:r3=1; x=1; y=1;
8601619:>3:r1=0; 3:r3=0; x=1; y=1;
418792:>3:r1=1; 3:r3=1; x=2; y=1;
2653023:>3:r1=0; 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=4867d1504e0b1c594b9643e48c015b80
Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr005 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr005 60.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr006 Allowed
Histogram (21 states)
3596 :>3:r1=0; 3:r3=0; x=2; y=2;
12635 :>3:r1=2; 3:r3=1; x=2; y=2;
33124 :>3:r1=2; 3:r3=0; x=2; y=1;
75961 :>3:r1=1; 3:r3=0; x=1; y=1;
157469:>3:r1=2; 3:r3=0; x=1; y=2;
273129:>3:r1=0; 3:r3=1; x=2; y=2;
11653 :>3:r1=1; 3:r3=1; x=2; y=2;
2033408:>3:r1=2; 3:r3=0; x=1; y=1;
1127952:>3:r1=0; 3:r3=0; x=2; y=1;
478666:>3:r1=1; 3:r3=0; x=1; y=2;
1627468:>3:r1=0; 3:r3=0; x=1; y=2;
715618:>3:r1=0; 3:r3=1; x=1; y=2;
804912:>3:r1=0; 3:r3=1; x=1; y=1;
3517556:>3:r1=2; 3:r3=1; x=1; y=2;
6105551:>3:r1=2; 3:r3=1; x=2; y=1;
2609870:>3:r1=1; 3:r3=1; x=1; y=1;
5797493:>3:r1=2; 3:r3=1; x=1; y=1;
3055668:>3:r1=1; 3:r3=1; x=1; y=2;
7860009:>3:r1=0; 3:r3=0; x=1; y=1;
778930:>3:r1=1; 3:r3=1; x=2; y=1;
2919332:>3:r1=0; 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.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r30,0(r2)
Test aclwdrr007 Allowed
Histogram (9 states)
3032732:>2:r1=2; 2:r3=0; x=1;
2222073:>2:r1=0; 2:r3=1; x=2;
4669470:>2:r1=1; 2:r3=1; x=2;
10005720:>2:r1=2; 2:r3=1; x=1;
1419310:>2:r1=0; 2:r3=1; x=1;
13004547:>2:r1=0; 2:r3=0; x=1;
2171448:>2:r1=1; 2:r3=1; x=1;
3253749:>2:r1=2; 2:r3=1; x=2;
220951:>2:r1=0; 2:r3=0; 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 35.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r3,0(r2)
_litmus_P1_0_: li r30,1
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr008 Allowed
Histogram (21 states)
1187 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
107964:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
158510:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
13235 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
17370 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
209513:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
144806:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
1306117:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
207894:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
576123:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
4731677:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
4206083:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
1022638:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
4379306:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
1555973:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
2006963:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
4764689:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
1052557:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
8380597:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
2315636:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
2841162:>0:r3=1; 3:r1=2; 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=61bd93196401321b8fb91e15727e3c64
Cycle=Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr008 No ACLwSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time aclwdrr008 55.81
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r4,0(r2)
_litmus_P1_0_: li r4,2
_litmus_P1_1_: stw r4,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr009 Allowed
Histogram (39 states)
8 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
203 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
15423 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
39050 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
11099 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
16588 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
150871:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
71779 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
851 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
501986:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
166661:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
35030 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
362505:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
615341:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
411050:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
46812 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
625187:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
64671 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
845624:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
284411:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1167506:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
2218837:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
3623793:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
599228:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
2229452:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
126516:>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
3292596:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
2592501:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
4716114:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1926869:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1799877:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
1933556:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
2149926:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
196610:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
1323879:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
393387:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
69664 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
1725512:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
3649027:>0:r3=1; 3:r1=0; 3:r3=0; 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=ab46080bf73ab92da49cdd6b27ede9b2
Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr009 No ACLwSyncdRR
Safe=Fre Wse SyncsWR LwSyncdWW
Time aclwdrr009 59.00
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r27,0(r9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz r30,0(r2)
_litmus_P1_0_: li r5,1
_litmus_P1_1_: stw r5,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r30,0(r2)
_litmus_P3_0_: li r6,1
_litmus_P3_1_: stw r6,0(r2)
Test aclwdrr010 Allowed
Histogram (15 states)
108679:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
393042:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
127101:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
169522:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
586449:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
124428:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
5172806:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
2380076:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
3420974:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
727299:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
2847520:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
2182251:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
3206872:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
5047873:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
13505108:>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 40.02
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr011 Allowed
Histogram (15 states)
115 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
2069 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
15531 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
601983:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
63332 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
3593443:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
4799654:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
8261113:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
3575101:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
1145941:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
8234058:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
3106124:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
248976:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
3985460:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
2367100:>1:r1=1; 1:r3=1; 3:r1=0; 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.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r5,1
_litmus_P0_1_: stw r5,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r9,2
_litmus_P0_4_: stw r9,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr012 Allowed
Histogram (33 states)
10 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
97 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
580 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
4232 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
7843 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2087 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
89060 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
96595 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
286544:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
35945 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
92727 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
187268:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
1192470:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
41287 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
239194:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
101374:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
494691:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1961239:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
341793:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
3330301:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1895769:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
3129924:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
610456:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
832155:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1536075:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
923823:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
3796683:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1761283:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
3584697:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
4015246:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1891845:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
5113317:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
2403390:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 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 51.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr013 Allowed
Histogram (15 states)
3923 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
34460 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
8299 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
266357:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
967034:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
3277644:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
509893:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
820542:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
4860273:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
8042204:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
7173901:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
2483937:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
3186240:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
2822022:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
5543271:>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=4eddb3c8ea9ccf8a71927b2e31094cad
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr013 No ACLwSyncdRR
Safe=Fre LwSyncdWW
Time aclwdrr013 47.42
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r5,1
_litmus_P0_1_: stw r5,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r9,2
_litmus_P0_4_: stw r9,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr014 Allowed
Histogram (32 states)
3 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
56 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
14 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
441 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
148339:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
32882 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1570 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
10752 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
120125:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
192443:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
140736:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
243267:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
1023394:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
134685:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
43548 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
19920 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
342540:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
85549 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
19731 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
2108422:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
285328:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
293337:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
116763:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
3645153:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
3999975:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
966500:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
3854571:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
3294378:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
3686366:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
2783636:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
11366676:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1038900:>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.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r29,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr015 Allowed
Histogram (15 states)
244 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
1222 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
71427 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
59357 :>1:r3=0; 3:r1=0; 3:r3=1; x=2;
141130:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
1952443:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
8671839:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
889066:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
4216976:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
3492383:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
1345263:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
1716513:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
2972982:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
9223749:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
5245406:>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 r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r29,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr016 Allowed
Histogram (15 states)
3188 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
80748 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
268233:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
127953:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
3528 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
1799779:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
2964054:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
2209321:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
2042205:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
3741021:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
2900590:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
678761:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
6778019:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
8107070:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
8295530:>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.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r27,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r30,0(r2)
Test aclwdrr017 Allowed
Histogram (7 states)
4799450:>0:r3=1; 2:r1=1; 2:r3=0;
115992:>0:r3=0; 2:r1=0; 2:r3=0;
1116270:>0:r3=1; 2:r1=0; 2:r3=1;
2090829:>0:r3=0; 2:r1=0; 2:r3=1;
15710044:>0:r3=1; 2:r1=1; 2:r3=1;
3166574:>0:r3=0; 2:r1=1; 2:r3=1;
13000841:>0:r3=1; 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 33.57
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r3,0(r2)
_litmus_P1_0_: li r30,1
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r29,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr018 Allowed
Histogram (15 states)
1183 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
8300 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
83610 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
150230:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
2197365:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
1137274:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
6607361:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
3245273:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
126023:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
1077140:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
3118672:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
9152567:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
1351530:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
8886528:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1;
2856944:>0:r3=1; 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 50.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r4,0(r2)
_litmus_P1_0_: li r30,2
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r3,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr019 Allowed
Histogram (30 states)
3974 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1343 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
4002 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
289 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
38129 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
481144:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
171674:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
14670 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
583849:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
228093:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
8474 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
133695:>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1000792:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1911444:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
604129:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
24681 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
2210986:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
570247:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
2915544:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
1094598:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
3835009:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
3112901:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
2409003:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1950997:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
379401:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
3596168:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
4148760:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
2550767:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
5834549:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
180688:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
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 52.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r3,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr020 Allowed
Histogram (45 states)
1 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
27 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
48 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
478 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
81 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
2663 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
48 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
67 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
289 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
14012 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
15773 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
23864 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
220717:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
100911:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
1496372:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
36396 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
19986 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
624105:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
1188703:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
293025:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
458060:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
14374 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
2877083:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
226179:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
328176:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
478636:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
1051583:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
390447:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
163086:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
940360:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
1913525:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
3294549:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
1907795:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
2977452:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
1122265:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
2226929:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
2200229:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
997864:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
1533616:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
472996:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
5032438:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
1005895:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
3727214:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
365879:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
255804:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; 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 53.53
$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 -O */
/* 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 -O"
LITMUSOPTS=-r 40 -v
Sun Dec 27 15:41:08 CET 2009