Tue Dec 22 17:39:11 GMT 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr000 Allowed
Histogram (22 states)
2 :>3:r1=2; 3:r3=0; x=2; y=2;
1083877:>3:r1=0; 3:r3=1; x=1; y=1;
1159411:>3:r1=0; 3:r3=0; x=2; y=2;
1279765:>3:r1=1; 3:r3=1; x=2; y=2;
2253880:>3:r1=2; 3:r3=1; x=2; y=2;
4091116:>3:r1=2; 3:r3=0; x=2; y=1;
7608628:>3:r1=0; 3:r3=1; x=1; y=2;
6906699:>3:r1=1; 3:r3=0; x=1; y=2;
12177710:>3:r1=2; 3:r3=1; x=1; y=1;
3991249:>3:r1=2; 3:r3=0; x=1; y=2;
11218119:>3:r1=0; 3:r3=1; x=2; y=2;
3913781:>3:r1=1; 3:r3=0; x=1; y=1;
14084053:>3:r1=1; 3:r3=1; x=1; y=2;
10301617:>3:r1=1; 3:r3=1; x=2; y=1;
23873904:>3:r1=1; 3:r3=1; x=1; y=1;
36301745:>3:r1=0; 3:r3=0; x=1; y=1;
39616858:>3:r1=0; 3:r3=0; x=1; y=2;
38456787:>3:r1=2; 3:r3=1; x=2; y=1;
24743064:>3:r1=2; 3:r3=0; x=1; y=1;
20593683:>3:r1=0; 3:r3=0; x=2; y=1;
26593762:>3:r1=2; 3:r3=1; x=1; y=2;
29750290:>3:r1=0; 3:r3=1; x=2; y=1;
Ok
Witnesses
Positive: 2, Negative: 319999998
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=7074ebf0a4e494a7c168353216394741
Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr000 Ok ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr000 87.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr001 Allowed
Histogram (22 states)
3 :>3:r1=2; 3:r3=0; x=2; y=2;
4686110:>3:r1=2; 3:r3=0; x=2; y=1;
715520:>3:r1=0; 3:r3=1; x=1; y=1;
1775413:>3:r1=1; 3:r3=1; x=2; y=2;
1761847:>3:r1=0; 3:r3=0; x=2; y=2;
4030259:>3:r1=2; 3:r3=0; x=1; y=2;
3690971:>3:r1=1; 3:r3=0; x=1; y=1;
6073931:>3:r1=0; 3:r3=1; x=1; y=2;
13432493:>3:r1=0; 3:r3=1; x=2; y=2;
6830146:>3:r1=1; 3:r3=0; x=1; y=2;
12589349:>3:r1=1; 3:r3=1; x=2; y=1;
38884646:>3:r1=0; 3:r3=0; x=1; y=2;
3031791:>3:r1=2; 3:r3=1; x=2; y=2;
13766363:>3:r1=1; 3:r3=1; x=1; y=2;
22457802:>3:r1=2; 3:r3=0; x=1; y=1;
32060616:>3:r1=0; 3:r3=0; x=1; y=1;
43291420:>3:r1=2; 3:r3=1; x=2; y=1;
9791571:>3:r1=2; 3:r3=1; x=1; y=1;
29894466:>3:r1=0; 3:r3=1; x=2; y=1;
24032109:>3:r1=0; 3:r3=0; x=2; y=1;
21674307:>3:r1=1; 3:r3=1; x=1; y=1;
25528867:>3:r1=2; 3:r3=1; x=1; y=2;
Ok
Witnesses
Positive: 3, Negative: 319999997
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=42a8ec6eccd807ced6dea1376fc81b0b
Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr001 Ok ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr001 86.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 6,2
_litmus_P1_1_: stw 6,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test aclwdrr002 Allowed
Histogram (10 states)
33 :>2:r1=2; 2:r3=0; x=2;
2585350:>2:r1=0; 2:r3=1; x=1;
53214959:>2:r1=0; 2:r3=1; x=2;
101510626:>2:r1=0; 2:r3=0; x=1;
47190552:>2:r1=1; 2:r3=1; x=1;
40961900:>2:r1=2; 2:r3=1; x=2;
54232296:>2:r1=2; 2:r3=1; x=1;
47351768:>2:r1=2; 2:r3=0; x=1;
30691694:>2:r1=0; 2:r3=0; x=2;
22260822:>2:r1=1; 2:r3=1; x=2;
Ok
Witnesses
Positive: 33, Negative: 399999967
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is validated
Hash=e86498b53008de1e6a240afbf078cd14
Cycle=Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr002 Ok ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr002 69.67
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test aclwdrr003 Allowed
Histogram (22 states)
2 :>0:r3=0; 3:r1=2; 3:r3=0; y=2;
641677:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
5383968:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
13304795:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
2818439:>0:r3=0; 3:r1=2; 3:r3=1; y=2;
29497501:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
6411937:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
7247302:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
4072070:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
19545238:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
13235976:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
36833176:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
8086410:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
2933139:>0:r3=0; 3:r1=0; 3:r3=0; y=2;
30144714:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
43635466:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
1772390:>0:r3=0; 3:r1=1; 3:r3=1; y=2;
24491497:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
28750848:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
14012599:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
4297190:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
22883666:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
Ok
Witnesses
Positive: 2, Negative: 319999998
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=9599d8c79b2e28a1f015a74966a65bac
Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr003 Ok ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr003 85.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 6,2
_litmus_P1_1_: stw 6,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 5,1
_litmus_P1_4_: stw 5,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 6,0(9)
Test aclwdrr004 Allowed
Histogram (42 states)
5 :>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
2 :>0:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
5 :>0:r3=1; 3:r1=2; 3:r3=0; x=2; y=1;
917340:>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
643401:>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
17164 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
54275 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
755330:>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
98437 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
104884:>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
2842530:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1606468:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
635144:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
6648621:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
12198686:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1797825:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2625450:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
1698682:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
2936675:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
9241705:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
6373026:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1223521:>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3893086:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1138118:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
2989707:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
9270451:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
18872476:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
4204817:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
7509802:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
18052972:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
3170314:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
22733888:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
11522055:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
7075239:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
5640049:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
23869003:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
25314673:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
14826225:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
12582357:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
17728710:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
25594753:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
31592129:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
Ok
Witnesses
Positive: 2, Negative: 319999998
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=32cc2d7800b6941b57852b520691800f
Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr004 Ok ACLwSyncdRR
Safe=Fre Wse SyncsWR SyncdWW
Time aclwdrr004 81.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr005 Allowed
Histogram (23 states)
3 :>3:r1=2; 3:r3=0; x=2; y=2;
19 :>3:r1=1; 3:r3=0; x=2; y=1;
1920923:>3:r1=1; 3:r3=1; x=2; y=2;
2945103:>3:r1=2; 3:r3=1; x=2; y=2;
664244:>3:r1=0; 3:r3=1; x=1; y=1;
1400416:>3:r1=0; 3:r3=0; x=2; y=2;
12439437:>3:r1=0; 3:r3=1; x=2; y=2;
5971225:>3:r1=0; 3:r3=1; x=1; y=2;
17062343:>3:r1=1; 3:r3=1; x=1; y=2;
9936513:>3:r1=2; 3:r3=1; x=1; y=1;
12485577:>3:r1=1; 3:r3=0; x=1; y=2;
22344866:>3:r1=1; 3:r3=1; x=1; y=1;
4347263:>3:r1=1; 3:r3=0; x=1; y=1;
6297001:>3:r1=2; 3:r3=0; x=1; y=2;
19678291:>3:r1=0; 3:r3=0; x=2; y=1;
27490907:>3:r1=0; 3:r3=1; x=2; y=1;
23099248:>3:r1=2; 3:r3=0; x=1; y=1;
36713622:>3:r1=0; 3:r3=0; x=1; y=2;
34781456:>3:r1=2; 3:r3=1; x=2; y=1;
3765346:>3:r1=2; 3:r3=0; x=2; y=1;
32703460:>3:r1=0; 3:r3=0; x=1; y=1;
31407636:>3:r1=2; 3:r3=1; x=1; y=2;
12545101:>3:r1=1; 3:r3=1; x=2; y=1;
Ok
Witnesses
Positive: 3, Negative: 319999997
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=4867d1504e0b1c594b9643e48c015b80
Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr005 Ok ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr005 84.21
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr006 Allowed
Histogram (24 states)
5 :>3:r1=1; 3:r3=0; x=2; y=2;
36 :>3:r1=1; 3:r3=0; x=2; y=1;
3 :>3:r1=2; 3:r3=0; x=2; y=2;
4082175:>3:r1=1; 3:r3=0; x=1; y=1;
5733549:>3:r1=2; 3:r3=0; x=1; y=2;
2740180:>3:r1=1; 3:r3=1; x=2; y=2;
2025783:>3:r1=0; 3:r3=0; x=2; y=2;
14398902:>3:r1=0; 3:r3=1; x=2; y=2;
4227520:>3:r1=2; 3:r3=0; x=2; y=1;
5105433:>3:r1=0; 3:r3=1; x=1; y=2;
28071050:>3:r1=0; 3:r3=1; x=2; y=1;
465607:>3:r1=0; 3:r3=1; x=1; y=1;
20845368:>3:r1=2; 3:r3=0; x=1; y=1;
20994340:>3:r1=1; 3:r3=1; x=1; y=1;
16438061:>3:r1=1; 3:r3=1; x=1; y=2;
14282731:>3:r1=1; 3:r3=1; x=2; y=1;
8787621:>3:r1=2; 3:r3=1; x=1; y=1;
4167415:>3:r1=2; 3:r3=1; x=2; y=2;
35778469:>3:r1=0; 3:r3=0; x=1; y=2;
30082466:>3:r1=0; 3:r3=0; x=1; y=1;
29945226:>3:r1=2; 3:r3=1; x=1; y=2;
22164315:>3:r1=0; 3:r3=0; x=2; y=1;
11657605:>3:r1=1; 3:r3=0; x=1; y=2;
38006140:>3:r1=2; 3:r3=1; x=2; y=1;
Ok
Witnesses
Positive: 3, Negative: 319999997
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=7e01ecd8b2bc06ff5ba0d2b4e58340c6
Cycle=Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr006 Ok ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr006 86.47
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 6,2
_litmus_P1_1_: stw 6,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test aclwdrr007 Allowed
Histogram (10 states)
42 :>2:r1=2; 2:r3=0; x=2;
1262992:>2:r1=0; 2:r3=1; x=1;
56257420:>2:r1=2; 2:r3=1; x=2;
46783342:>2:r1=2; 2:r3=0; x=1;
40260394:>2:r1=0; 2:r3=1; x=2;
45961394:>2:r1=2; 2:r3=1; x=1;
94671035:>2:r1=0; 2:r3=0; x=1;
44002931:>2:r1=1; 2:r3=1; x=1;
33587964:>2:r1=1; 2:r3=1; x=2;
37212486:>2:r1=0; 2:r3=0; x=2;
Ok
Witnesses
Positive: 42, Negative: 399999958
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is validated
Hash=ba17863040d25a62a648bb8030bf59fd
Cycle=Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr007 Ok ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr007 74.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test aclwdrr008 Allowed
Histogram (24 states)
2 :>0:r3=0; 3:r1=1; 3:r3=0; y=2;
2 :>0:r3=0; 3:r1=2; 3:r3=0; y=2;
88 :>0:r3=0; 3:r1=1; 3:r3=0; y=1;
4156041:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
380916:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
15735510:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
14982804:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
21363329:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
2567574:>0:r3=0; 3:r1=1; 3:r3=1; y=2;
3699375:>0:r3=0; 3:r1=2; 3:r3=1; y=2;
7062125:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
38198734:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
3407657:>0:r3=0; 3:r1=0; 3:r3=0; y=2;
18797348:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
6416403:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
4533697:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
33780655:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
28033967:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
26448483:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
29235460:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
5823960:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
15340195:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
27417058:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
12618617:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
Ok
Witnesses
Positive: 2, Negative: 319999998
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=61bd93196401321b8fb91e15727e3c64
Cycle=Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr008 Ok ACLwSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time aclwdrr008 88.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 6,2
_litmus_P1_1_: stw 6,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 5,1
_litmus_P1_4_: stw 5,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 6,0(9)
Test aclwdrr009 Allowed
Histogram (44 states)
1 :>0:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>0:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
7 :>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
6 :>0:r3=1; 3:r1=2; 3:r3=0; x=2; y=1;
1 :>0:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
59318 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
24128 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
766180:>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
65120 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
940101:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
1001862:>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
543730:>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1166103:>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1414770:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
2697714:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1261628:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
317149:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
4940314:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
3293736:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
115578:>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
3850414:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
6090158:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
3653435:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
5554567:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1163912:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
12265894:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
23560960:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
15291809:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
5056772:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
6975483:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
15102963:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
11476116:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
10146233:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
3798252:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
10607855:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
5004651:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
9123316:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
17065370:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
17347000:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
21631824:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
28142535:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
15984500:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
23273048:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
29225485:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
Ok
Witnesses
Positive: 1, Negative: 319999999
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=ab46080bf73ab92da49cdd6b27ede9b2
Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr009 Ok ACLwSyncdRR
Safe=Fre Wse SyncsWR LwSyncdWW
Time aclwdrr009 86.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: li 8,1
_litmus_P3_1_: stw 8,0(9)
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 4,0(9)
_litmus_P1_0_: li 7,1
_litmus_P1_1_: stw 7,0(9)
_litmus_P0_0_: lwz 3,0(11)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz 4,0(9)
Test aclwdrr010 Allowed
Histogram (16 states)
16 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=0;
255875:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
57015841:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
6036588:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
24039092:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
24886214:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
6623156:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
22916416:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
19242913:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
6536360:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
22556867:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
19252025:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
5929719:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
25661155:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
25262916:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
53784847:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1;
Ok
Witnesses
Positive: 16, Negative: 319999984
Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated
Hash=8ce05c9f86d49b2adfd5546bd471aa44
Cycle=Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr010 Ok ACLwSyncdRR
Safe=Fre
Time aclwdrr010 77.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr011 Allowed
Histogram (15 states)
974421:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
6586700:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
2270439:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
12554772:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
2409125:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
13024093:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
1341241:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
20791040:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
30490013:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
28614097:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
30556930:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
37803748:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
63128089:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
32489164:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
36966128:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 320000000
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 83.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test aclwdrr012 Allowed
Histogram (35 states)
2 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
9 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
4157 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
155683:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
107030:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
2906757:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
467354:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
928459:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
3534859:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1958664:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
2340245:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
4489760:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1148197:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
5630265:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
2219855:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
1309409:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
2307933:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
5105752:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
12267412:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
897236:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
4940450:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
6869241:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
2626556:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2848899:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
19601778:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
18772232:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
26917430:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
20264430:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
21572821:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
4488519:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
39619188:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
19320775:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
20815940:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
4561730:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
59000973:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
Ok
Witnesses
Positive: 2, Negative: 319999998
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=992754280de579a7f5feb516274ac846
Cycle=Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr012 Ok ACLwSyncdRR
Safe=Fre SyncsWW
Time aclwdrr012 84.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr013 Allowed
Histogram (16 states)
40 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0;
1180191:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1556288:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
2664438:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
15090759:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
17075899:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
35463082:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
6112266:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
28427314:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
3995799:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
26556936:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
21685931:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
26358223:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
61522102:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
30250544:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
42060188:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
Ok
Witnesses
Positive: 40, Negative: 319999960
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=4eddb3c8ea9ccf8a71927b2e31094cad
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr013 Ok ACLwSyncdRR
Safe=Fre LwSyncdWW
Time aclwdrr013 84.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test aclwdrr014 Allowed
Histogram (36 states)
1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
9 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
3 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
1129 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
61097 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
245243:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1181965:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
490443:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
131601:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
144262:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1157445:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2534854:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
884861:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
145162:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1927758:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1257521:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
1078884:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
2708349:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
783052:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1985053:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1852289:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
16455460:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
4405946:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
23811073:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
5673745:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
423750:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
19364716:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
5810088:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
23737182:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
6248905:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
22419977:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
24553624:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
23100699:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
21697308:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
46299160:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
57427386:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
Ok
Witnesses
Positive: 3, Negative: 319999997
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=0363e525d1d5c107b6654781a780ef6a
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr014 Ok ACLwSyncdRR
Safe=Fre LwSyncsWW
Time aclwdrr014 81.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr015 Allowed
Histogram (16 states)
5 :>1:r3=0; 3:r1=1; 3:r3=0; x=2;
415210:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
2635982:>1:r3=0; 3:r1=0; 3:r3=0; x=2;
5089925:>1:r3=0; 3:r1=1; 3:r3=1; x=2;
27585589:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
5978117:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
23212474:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
27624325:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
19789194:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
4158546:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
27858411:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
29831115:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
22016435:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
46961903:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
19256537:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
57586232:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
Ok
Witnesses
Positive: 5, Negative: 319999995
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=61d664ae95ff6d97da76ebb37bc47ca3
Cycle=Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr015 Ok ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr015 84.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr016 Allowed
Histogram (16 states)
4 :>1:r3=0; 3:r1=1; 3:r3=0; x=2;
263624:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
3699260:>1:r3=0; 3:r1=0; 3:r3=0; x=2;
23593788:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
20287812:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
52403615:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
5804840:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
22324162:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
4785876:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
22062444:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
26402508:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
24931007:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
55610386:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
25054920:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
26589015:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
6186739:>1:r3=0; 3:r1=1; 3:r3=1; x=2;
Ok
Witnesses
Positive: 4, Negative: 319999996
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=4947e9ed11cb60630be5b54900bf7b6c
Cycle=Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr016 Ok ACLwSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time aclwdrr016 82.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 6,1
_litmus_P1_1_: stw 6,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test aclwdrr017 Allowed
Histogram (8 states)
85 :>0:r3=0; 2:r1=1; 2:r3=0;
772688:>0:r3=1; 2:r1=0; 2:r3=1;
52863656:>0:r3=0; 2:r1=1; 2:r3=1;
86813163:>0:r3=1; 2:r1=1; 2:r3=1;
81633632:>0:r3=1; 2:r1=0; 2:r3=0;
49919104:>0:r3=1; 2:r1=1; 2:r3=0;
76996242:>0:r3=0; 2:r1=0; 2:r3=1;
51001430:>0:r3=0; 2:r1=0; 2:r3=0;
Ok
Witnesses
Positive: 85, Negative: 399999915
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated
Hash=0dd8df1959f84e11508b32d374a44775
Cycle=Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr017 Ok ACLwSyncdRR
Safe=Fre SyncdWR
Time aclwdrr017 70.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test aclwdrr018 Allowed
Histogram (16 states)
7 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=0;
207199:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
22115661:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
6315112:>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
52356026:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
6082073:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
21922282:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1;
24791114:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
26619001:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
24334694:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
18450541:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
6853884:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
55300060:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
23000557:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
5893322:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
25758467:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
Ok
Witnesses
Positive: 7, Negative: 319999993
Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=3fed6cc74892902ab28df779672578f8
Cycle=Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr018 Ok ACLwSyncdRR
Safe=Fre SyncdWR
Time aclwdrr018 84.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,1
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 4,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 6,0(9)
Test aclwdrr019 Allowed
Histogram (35 states)
1 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
1 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
9 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0; y=1;
21 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
873007:>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
29080 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
37221 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
47371 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
530341:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
172161:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
105742:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1231081:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
1714583:>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2149657:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1895145:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
6214666:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1339337:>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
6276110:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
18586648:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
9525693:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
19431721:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
19245856:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
24707089:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
13284027:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
5199571:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
28720296:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
8021696:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
3146641:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
14138109:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
19557802:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
8099646:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
19866311:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
34197786:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
22231934:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
29423640:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
Ok
Witnesses
Positive: 1, Negative: 319999999
Condition exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=660c5e262906b3ab9066962d8bf69882
Cycle=Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr019 Ok ACLwSyncdRR
Safe=Fre SyncsWR SyncdWR
Time aclwdrr019 84.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 7,2
_litmus_P2_1_: stw 7,0(9)
_litmus_P1_0_: li 11,1
_litmus_P1_1_: stw 11,0(9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz 5,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 4,0(9)
Test aclwdrr020 Allowed
Histogram (54 states)
1 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
12 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
18 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
4 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
3 :>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
17 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
4 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
106 :>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
239 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
24321 :>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
66039 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
7016 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
129385:>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
597784:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
127192:>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
78744 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
429248:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
2682042:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
87321 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
169807:>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
217171:>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
2541431:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
2987887:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
1585911:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
6558 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
6298447:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
108023:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
17589180:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
10663995:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
6367838:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
9184584:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
13792308:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
16529916:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
9287204:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
2515718:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
1844429:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
20612740:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
18668333:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
3168846:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
1321607:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
10041007:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
17024764:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
15366735:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
17206063:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
18715961:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
20420854:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
7529593:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
6685548:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
15256472:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
7090764:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
11989245:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
10237692:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
7077377:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
5666496:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
Ok
Witnesses
Positive: 4, Negative: 319999996
Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=bad92812900a1656a66221eff19f711e
Cycle=Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR
Relax aclwdrr020 Ok ACLwSyncdRR
Safe=Fre SyncsWR SyncdWR
Time aclwdrr020 84.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr021.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr021
"Fre SyncdWW Wse SyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz 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 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test aclwdrr021 Allowed
Histogram (7 states)
13203864:>2:r1=0; 2:r3=1; x=1;
9399127:>2:r1=1; 2:r3=1; x=2;
35045359:>2:r1=0; 2:r3=0; x=2;
16152874:>2:r1=1; 2:r3=0; x=1;
134985705:>2:r1=0; 2:r3=0; x=1;
108507764:>2:r1=0; 2:r3=1; x=2;
82705307:>2:r1=1; 2:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=aeec733dac4af8be94573c9aff9d0c10
Cycle=Fre SyncdWW Wse SyncdWW Rfe LwSyncdRR
Relax aclwdrr021 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr021 75.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr022.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr022
"Fre LwSyncdWW Wse SyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz 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 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test aclwdrr022 Allowed
Histogram (7 states)
10020320:>2:r1=0; 2:r3=1; x=1;
12190912:>2:r1=1; 2:r3=1; x=2;
38733758:>2:r1=0; 2:r3=0; x=2;
76512959:>2:r1=1; 2:r3=1; x=1;
116080818:>2:r1=0; 2:r3=1; x=2;
130932903:>2:r1=0; 2:r3=0; x=1;
15528330:>2:r1=1; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=fb989d16658311d76866354f8a671029
Cycle=Fre LwSyncdWW Wse SyncdWW Rfe LwSyncdRR
Relax aclwdrr022 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr022 75.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr023.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr023
"Fre SyncdWW Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr023 Allowed
Histogram (3 states)
222420686:>1:r1=1; 1:r3=1;
319325764:>1:r1=0; 1:r3=0;
98253550:>1:r1=0; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=501f8f5a33589295352fe1de9678142b
Cycle=Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr023 No ACLwSyncdRR
Safe=Fre SyncdWW
Time aclwdrr023 72.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr024.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr024
"Fre SyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
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,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test aclwdrr024 Allowed
Histogram (15 states)
733603:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
5296411:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
480182:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
515810:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
844297:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
12651120:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
32946526:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
48180518:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
11976966:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
49611664:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
13083465:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
19992240:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
13345706:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
34054883:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
76286609:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=d941e505b27c9a2748aeb4651a9cb643
Cycle=Fre SyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr024 No ACLwSyncdRR
Safe=Fre SyncdWW
Time aclwdrr024 91.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr025.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr025
"Fre SyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=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) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test aclwdrr025 Allowed
Histogram (34 states)
1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
573 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
931502:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
540922:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
653305:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
1008429:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
937265:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1834839:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
904232:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
822778:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
3525328:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
3810768:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
756655:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1213954:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
4428289:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1342843:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
7270801:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
2404962:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
874624:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
3059482:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
33317151:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
21740773:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
5010136:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
745974:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
8141076:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
24051728:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
66290856:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
21370664:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
1085292:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
13565069:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
32203330:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
28155181:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
10503462:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
17497756:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=32b005fb973345d626b38029866e06f9
Cycle=Fre SyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr025 No ACLwSyncdRR
Safe=Fre SyncsWW SyncdWW
Time aclwdrr025 89.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr026.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr026
"Fre LwSyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
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) | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test aclwdrr026 Allowed
Histogram (16 states)
5 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0;
681020:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1020755:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
501522:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1405752:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
10728339:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
11705715:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
4342105:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
31041309:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
47080804:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
15866854:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
20078807:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
41708447:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
23172672:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
36980689:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
73685205:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
Ok
Witnesses
Positive: 5, Negative: 319999995
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=7a7cbc5359389bdb4170629397f77be6
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr026 Ok ACLwSyncdRR
Safe=Fre SyncdWW LwSyncdWW
Time aclwdrr026 90.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr027.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr027
"Fre LwSyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=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) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: sync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test aclwdrr027 Allowed
Histogram (33 states)
166 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
234381:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
456512:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
200824:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
302352:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
118588:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
386670:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1121208:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1959726:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
3487854:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
275831:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
560501:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1328939:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
1354998:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
4264038:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
2423892:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1772310:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
2615533:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
10660468:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
31009284:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
1581000:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
319801:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
4523840:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
25964165:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
19453371:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
934918:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
11776436:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
63493113:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
31451850:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1688748:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
27668990:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
29348354:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
37261339:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=c2a2e1328465d78b88dcae553e33604e
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr027 No ACLwSyncdRR
Safe=Fre SyncdWW LwSyncsWW
Time aclwdrr027 89.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr028.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr028
"Fre SyncdWR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
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,1 | ;
| stw r3,0(r4) | ;
exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test aclwdrr028 Allowed
Histogram (7 states)
6887826:>0:r3=1; 2:r1=0; 2:r3=1;
16669072:>0:r3=0; 2:r1=1; 2:r3=1;
16374037:>0:r3=1; 2:r1=1; 2:r3=0;
117780227:>0:r3=1; 2:r1=0; 2:r3=0;
114868565:>0:r3=0; 2:r1=0; 2:r3=1;
53435546:>0:r3=0; 2:r1=0; 2:r3=0;
73984727:>0:r3=1; 2:r1=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=eebdc6b096cdd9c24f38c118593f06bb
Cycle=Fre SyncdWR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr028 No ACLwSyncdRR
Safe=Fre SyncdWW SyncdWR
Time aclwdrr028 75.68
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr029.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr029
"Fre SyncsWR Fre SyncdWW Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=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 | sync | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: sync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test aclwdrr029 Allowed
Histogram (13 states)
2099587:>0:r3=2; 2:r1=1; 2:r3=2; y=2;
118948:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
1119097:>0:r3=2; 2:r1=0; 2:r3=2; y=2;
8792527:>0:r3=1; 2:r1=0; 2:r3=1; y=1;
8231970:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
69748406:>0:r3=1; 2:r1=1; 2:r3=1; y=1;
13995264:>0:r3=1; 2:r1=1; 2:r3=2; y=2;
41146625:>0:r3=1; 2:r1=0; 2:r3=2; y=1;
54001175:>0:r3=1; 2:r1=0; 2:r3=2; y=2;
58306300:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
63437081:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
13862829:>0:r3=1; 2:r1=1; 2:r3=2; y=1;
65140191:>0:r3=1; 2:r1=0; 2:r3=0; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=4ab12861c7fd48307d5dbbb06073fa65
Cycle=Fre SyncsWR Fre SyncdWW Rfe LwSyncdRR
Relax aclwdrr029 No ACLwSyncdRR
Safe=Fre SyncsWR SyncdWW
Time aclwdrr029 75.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr030.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr030
"Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW 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) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 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 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test aclwdrr030 Allowed
Histogram (76 states)
1 :>1:r1=1; 1:r3=0; 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;
3 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1458 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
1429 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1431 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
8736 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1632 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2505 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2282 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
10831 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
271595:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
106830:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
24520 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
289232:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
311932:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
229785:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
953712:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
74580 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
26675 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
714055:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
106444:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1024705:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
255274:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
710123:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
807352:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1309289:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
199235:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
586500:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
2631980:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1717815:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
308254:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
756868:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2084242:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1614454:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
3794670:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
4105346:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
268876:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
301928:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
197268:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1275589:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1756162:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
774220:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
542482:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1246749:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
5670518:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2938841:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
13208169:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
218711:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1222345:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
1690749:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
4215130:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
3842208:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
2777955:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
2158778:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
17795662:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
2168860:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
5389518:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
15680848:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
3865486:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2167437:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
4333053:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
3627535:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
3529931:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
710610:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
20748282:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
59903322:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
17564901:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
33012614:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2959969:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
13072793:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4082606:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
16172733:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
20345618:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
3515766:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=ee8538d5ca48a381e732df1d7c7a6726
Cycle=Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR
Relax aclwdrr030 No ACLwSyncdRR
Safe=Fre SyncsWW
Time aclwdrr030 96.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr031.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr031
"Fre LwSyncdWW Rfe LwSyncdRR Fre SyncsWW 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) | sync | lwz r3,0(r4) ;
li r3,1 | | li r3,2 | ;
stw r3,0(r4) | | stw r3,0(r2) | ;
exists (y=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 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 31,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr031 Allowed
Histogram (36 states)
14 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; y=2;
2 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; y=2;
14 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
725 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
420169:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
981920:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; y=2;
893295:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
993411:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; y=2;
1331656:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
774736:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
1579501:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2157735:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
3504987:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; y=2;
1199450:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; y=2;
783642:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; y=2;
989895:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
4940489:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; y=2;
1703918:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; y=2;
1259789:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; y=2;
1466870:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
2450750:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; y=2;
7089636:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
17882666:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; y=2;
7762057:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
19202280:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; y=2;
4926911:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
19217772:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
4347063:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; y=2;
19587083:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; y=2;
30209934:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; y=2;
11647907:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; y=2;
29149494:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
21922136:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; y=2;
65158899:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
32075672:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; y=2;
2387522:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; y=2;
Ok
Witnesses
Positive: 14, Negative: 319999986
Condition exists (y=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=7e70701bff0ff65c82954a7448132407
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR
Relax aclwdrr031 Ok ACLwSyncdRR
Safe=Fre SyncsWW LwSyncdWW
Time aclwdrr031 90.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr032.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr032
"Fre LwSyncsWW Rfe LwSyncdRR Fre SyncsWW 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) | sync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 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 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test aclwdrr032 Allowed
Histogram (75 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;
6 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
328 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
279 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
3971 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1273 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
1686 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
3278 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
2643 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
26884 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
520 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
8577 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
59997 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
112054:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
55960 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
178225:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
240305:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
320500:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
248589:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
47604 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
32358 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
271801:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
67181 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
332981:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
271126:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
834283:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
241692:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
559656:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
162455:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
2131642:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
68263 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
101057:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
402349:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
371999:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
2125264:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
129262:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
1027030:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
1061502:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
1880892:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2207469:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1163388:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
1224391:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
775676:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
146158:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
2592533:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
3255950:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
817179:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
5282839:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
3002953:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
1310550:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1727909:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
363114:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
2254265:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1741327:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
3835900:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
5358710:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
5476403:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
5159903:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
18084567:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
17343107:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
2617087:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
3561141:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
16788876:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
18539040:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
2348430:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
20886263:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
797329:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
4580793:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
12030586:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
37813468:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
57842124:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
3551510:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
23597220:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
18536368:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 320000000
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=74930e6bce52d51f9df9817f8385847f
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR
Relax aclwdrr032 No ACLwSyncdRR
Safe=Fre SyncsWW LwSyncsWW
Time aclwdrr032 96.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr033.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr033
"Fre SyncdWR Fre SyncsWW 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 | sync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 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 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test aclwdrr033 Allowed
Histogram (17 states)
25 :>0:r3=1; 2:r1=2; 2:r3=0; x=2;
69 :>0:r3=0; 2:r1=1; 2:r3=0; x=2;
289349:>0:r3=1; 2:r1=1; 2:r3=0; x=2;
2238842:>0:r3=1; 2:r1=1; 2:r3=1; x=2;
297062:>0:r3=1; 2:r1=0; 2:r3=1; x=2;
247507:>0:r3=2; 2:r1=0; 2:r3=1; x=2;
3302138:>0:r3=1; 2:r1=2; 2:r3=1; x=2;
2744269:>0:r3=2; 2:r1=1; 2:r3=1; x=2;
37593079:>0:r3=2; 2:r1=2; 2:r3=0; x=2;
53183117:>0:r3=0; 2:r1=0; 2:r3=0; x=2;
16195081:>0:r3=0; 2:r1=1; 2:r3=1; x=2;
8385830:>0:r3=2; 2:r1=1; 2:r3=0; x=2;
17775671:>0:r3=1; 2:r1=0; 2:r3=0; x=2;
38077045:>0:r3=0; 2:r1=2; 2:r3=1; x=2;
82229842:>0:r3=2; 2:r1=2; 2:r3=1; x=2;
76228695:>0:r3=0; 2:r1=0; 2:r3=1; x=2;
61212379:>0:r3=2; 2:r1=0; 2:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=9aeeb761b71ddabb3db56388750f2a1a
Cycle=Fre SyncdWR Fre SyncsWW Rfe LwSyncdRR
Relax aclwdrr033 No ACLwSyncdRR
Safe=Fre SyncsWW SyncdWR
Time aclwdrr033 76.98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr034.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr034
"Fre SyncdWW Wse LwSyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz 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 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test aclwdrr034 Allowed
Histogram (8 states)
124 :>2:r1=1; 2:r3=0; x=2;
7548577:>2:r1=0; 2:r3=1; x=1;
35168671:>2:r1=0; 2:r3=0; x=2;
12687420:>2:r1=1; 2:r3=1; x=2;
28364147:>2:r1=1; 2:r3=0; x=1;
104551695:>2:r1=0; 2:r3=1; x=2;
121179237:>2:r1=0; 2:r3=0; x=1;
90500129:>2:r1=1; 2:r3=1; x=1;
Ok
Witnesses
Positive: 124, Negative: 399999876
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is validated
Hash=10939fdb629e01d3ec7a75f951037026
Cycle=Fre SyncdWW Wse LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr034 Ok ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr034 77.33
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr035.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr035
"Fre LwSyncdWW Wse LwSyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz 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 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 4,2
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test aclwdrr035 Allowed
Histogram (8 states)
94 :>2:r1=1; 2:r3=0; x=2;
38555216:>2:r1=0; 2:r3=0; x=2;
4846481:>2:r1=0; 2:r3=1; x=1;
27654304:>2:r1=1; 2:r3=0; x=1;
111320893:>2:r1=0; 2:r3=1; x=2;
116544681:>2:r1=0; 2:r3=0; x=1;
84467291:>2:r1=1; 2:r3=1; x=1;
16611040:>2:r1=1; 2:r3=1; x=2;
Ok
Witnesses
Positive: 94, Negative: 399999906
Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is validated
Hash=b62ccd86d3f88c50d13b5221a86b68a5
Cycle=Fre LwSyncdWW Wse LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr035 Ok ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr035 75.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr036.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr036
"Fre LwSyncdWW Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;}
P0 | P1 ;
li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) ;
li r3,1 | ;
stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0)
Generated assembler
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 6,1
_litmus_P0_1_: stw 6,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 5,1
_litmus_P0_4_: stw 5,0(9)
Test aclwdrr036 Allowed
Histogram (3 states)
41207261:>1:r1=0; 1:r3=1;
319426918:>1:r1=0; 1:r3=0;
279365821:>1:r1=1; 1:r3=1;
No
Witnesses
Positive: 0, Negative: 640000000
Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated
Hash=25520ac6610aa6339bae2caee0005d5b
Cycle=Fre LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr036 No ACLwSyncdRR
Safe=Fre LwSyncdWW
Time aclwdrr036 72.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr037.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr037
"Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR"
{0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;}
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) | lwsync | lwz r3,0(r4) ;
li r3,1 | | li r3,1 | ;
stw r3,0(r4) | | stw r3,0(r4) | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 5,1
_litmus_P2_4_: stw 5,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 31,0(9)
_litmus_P0_0_: li 5,1
_litmus_P0_1_: stw 5,0(11)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 4,1
_litmus_P0_4_: stw 4,0(9)
Test aclwdrr037 Allowed
Histogram (16 states)
17 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0;
1216652:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
1290201:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1224664:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
14736499:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
39093055:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
32366301:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
3361138:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
40006086:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
28782529:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
71743708:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
18399360:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
17699863:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
15446143:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
33485314:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
1148470:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
Ok
Witnesses
Positive: 17, Negative: 319999983
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=e45e2fb06db799317c9d3aeed10f6d45
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr037 Ok ACLwSyncdRR
Safe=Fre LwSyncdWW
Time aclwdrr037 94.36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr038.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr038
"Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR"
{0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=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) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,1 | ;
stw r3,0(r2) | | stw r3,0(r4) | ;
exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 5,1
_litmus_P2_1_: stw 5,0(11)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 4,1
_litmus_P2_4_: stw 4,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test aclwdrr038 Allowed
Histogram (36 states)
4 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
5 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
43 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
552 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
196049:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
122989:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
699147:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
1663640:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
611792:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
2568354:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
363968:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
142463:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2;
2427449:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
2118111:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
186870:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
601536:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2;
2962590:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
370961:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2;
1030052:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
1978649:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
3606459:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2;
641517:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
1168906:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
3345164:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
19525624:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
1637302:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2;
33566271:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2;
26214430:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
37310892:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2;
61730019:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
4546770:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2;
13050811:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2;
27994624:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2;
24547910:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
25724728:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2;
17343349:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2;
Ok
Witnesses
Positive: 43, Negative: 319999957
Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated
Hash=459d76f119641ec12aab94d071c86542
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr038 Ok ACLwSyncdRR
Safe=Fre LwSyncsWW LwSyncdWW
Time aclwdrr038 90.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr039.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr039
"Fre SyncdWR Fre LwSyncdWW Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz 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 (0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 4,1
_litmus_P1_1_: stw 4,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 3,1
_litmus_P1_4_: stw 3,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test aclwdrr039 Allowed
Histogram (8 states)
82 :>0:r3=0; 2:r1=1; 2:r3=0;
105238437:>0:r3=1; 2:r1=0; 2:r3=0;
3414681:>0:r3=1; 2:r1=0; 2:r3=1;
80145622:>0:r3=1; 2:r1=1; 2:r3=1;
110666645:>0:r3=0; 2:r1=0; 2:r3=1;
20453432:>0:r3=0; 2:r1=1; 2:r3=1;
27793672:>0:r3=1; 2:r1=1; 2:r3=0;
52287429:>0:r3=0; 2:r1=0; 2:r3=0;
Ok
Witnesses
Positive: 82, Negative: 399999918
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated
Hash=9adf86efa9ed99398ed262e7a29cb549
Cycle=Fre SyncdWR Fre LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr039 Ok ACLwSyncdRR
Safe=Fre SyncdWR LwSyncdWW
Time aclwdrr039 75.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr040.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr040
"Fre SyncsWR Fre LwSyncdWW Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=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 | lwsync | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | ;
| stw r3,0(r4) | ;
exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 5,2
_litmus_P1_1_: stw 5,0(11)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 4,1
_litmus_P1_4_: stw 4,0(9)
_litmus_P0_0_: li 11,1
_litmus_P0_1_: stw 11,0(9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 5,0(9)
Test aclwdrr040 Allowed
Histogram (13 states)
2530591:>0:r3=2; 2:r1=1; 2:r3=2; y=2;
121092:>0:r3=2; 2:r1=0; 2:r3=1; y=2;
3083892:>0:r3=1; 2:r1=0; 2:r3=1; y=1;
8367925:>0:r3=2; 2:r1=0; 2:r3=0; y=2;
65988194:>0:r3=1; 2:r1=0; 2:r3=0; y=1;
1118913:>0:r3=2; 2:r1=0; 2:r3=2; y=2;
62604275:>0:r3=1; 2:r1=0; 2:r3=1; y=2;
26181012:>0:r3=1; 2:r1=1; 2:r3=2; y=1;
49045481:>0:r3=1; 2:r1=0; 2:r3=2; y=2;
27005895:>0:r3=1; 2:r1=0; 2:r3=2; y=1;
57175058:>0:r3=1; 2:r1=0; 2:r3=0; y=2;
19507743:>0:r3=1; 2:r1=1; 2:r3=2; y=2;
77269929:>0:r3=1; 2:r1=1; 2:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 400000000
Condition exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=1a7c6d1dc4425965c5dae6a980780759
Cycle=Fre SyncsWR Fre LwSyncdWW Rfe LwSyncdRR
Relax aclwdrr040 No ACLwSyncdRR
Safe=Fre SyncsWR LwSyncdWW
Time aclwdrr040 76.10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr041.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr041
"Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW 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) | lwsync | lwz r3,0(r4) ;
li r3,2 | | li r3,2 | ;
stw r3,0(r2) | | stw r3,0(r2) | ;
exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P3_0_: lwz 3,0(11)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz 4,0(9)
_litmus_P2_0_: li 6,1
_litmus_P2_1_: stw 6,0(9)
_litmus_P2_2_: lwsync
_litmus_P2_3_: li 11,2
_litmus_P2_4_: stw 11,0(9)
_litmus_P1_0_: lwz 3,0(11)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz 4,0(9)
_litmus_P0_0_: li 7,1
_litmus_P0_1_: stw 7,0(9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li 11,2
_litmus_P0_4_: stw 11,0(9)
Test aclwdrr041 Allowed
Histogram (78 states)
1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
2 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
4 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
2 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
295 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
282 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
316 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
4343 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
669 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
1070 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
8467 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
12975 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
251 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
707 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
13959 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2;
11633 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
11626 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2;
89414 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
8335 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
356211:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
211521:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
220442:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2;
85813 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
117153:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
372145:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
130073:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
115546:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2;
155543:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2;
98775 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
362292:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
71479 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
219483:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1221128:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
39462 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1160298:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2;
80513 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
989872:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
716828:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
99997 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1211920:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
5034487:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2;
1921332:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2;
23063794:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
2685981:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1891782:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
106974:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
82896 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
1185775:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
993537:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1167489:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
39775 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2;
100051:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
380689:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
2584538:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2;
2561552:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
19873838:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4998094:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1972741:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
43293755:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1996288:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
4989907:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2;
19317449:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
16132155:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
755131:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2;
2862945:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
1935496:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
22346671:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
16261994:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
23329869:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
4899836:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
968520:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2;
55684228:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2;
1885785:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
886184:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2;
22211442:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2;
1396171:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2;
Ok
Witnesses
Positive: 2, Negative: 319999998
Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is validated
Hash=f658f820f1d5e1aea992b078ad3de29c
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW Rfe LwSyncdRR
Relax aclwdrr041 Ok ACLwSyncdRR
Safe=Fre LwSyncsWW
Time aclwdrr041 93.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for src/aclwdrr042.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr042
"Fre SyncdWR Fre LwSyncsWW 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 | lwsync | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,2 | ;
| stw r3,0(r2) | ;
exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P2_0_: lwz 3,0(11)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz 31,0(9)
_litmus_P1_0_: li 5,1
_litmus_P1_1_: stw 5,0(9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li 11,2
_litmus_P1_4_: stw 11,0(9)
_litmus_P0_0_: li 4,1
_litmus_P0_1_: stw 4,0(11)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz 3,0(9)
Test aclwdrr042 Allowed
Histogram (18 states)
6 :>0:r3=0; 2:r1=1; 2:r3=0; x=2;
13 :>0:r3=0; 2:r1=2; 2:r3=0; x=2;
1734 :>0:r3=1; 2:r1=2; 2:r3=0; x=2;
386043:>0:r3=2; 2:r1=0; 2:r3=1; x=2;
83823 :>0:r3=1; 2:r1=0; 2:r3=1; x=2;
932784:>0:r3=1; 2:r1=2; 2:r3=1; x=2;
28345 :>0:r3=1; 2:r1=1; 2:r3=0; x=2;
2182860:>0:r3=2; 2:r1=1; 2:r3=0; x=2;
440626:>0:r3=1; 2:r1=1; 2:r3=1; x=2;
1642877:>0:r3=2; 2:r1=1; 2:r3=1; x=2;
6619671:>0:r3=0; 2:r1=1; 2:r3=1; x=2;
47099765:>0:r3=2; 2:r1=2; 2:r3=0; x=2;
48207572:>0:r3=0; 2:r1=2; 2:r3=1; x=2;
6460701:>0:r3=1; 2:r1=0; 2:r3=0; x=2;
52065151:>0:r3=0; 2:r1=0; 2:r3=0; x=2;
73483985:>0:r3=2; 2:r1=0; 2:r3=0; x=2;
84450831:>0:r3=2; 2:r1=2; 2:r3=1; x=2;
75913213:>0:r3=0; 2:r1=0; 2:r3=1; x=2;
Ok
Witnesses
Positive: 13, Negative: 399999987
Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is validated
Hash=9862f681ad48c0682ff709f0b167939f
Cycle=Fre SyncdWR Fre LwSyncsWW Rfe LwSyncdRR
Relax aclwdrr042 Ok ACLwSyncdRR
Safe=Fre SyncdWR LwSyncsWW
Time aclwdrr042 80.13
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 2000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 20000
#endif
#ifndef N_EXE
#define N_EXE (32 < N ? 1 : 32 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O -pthread */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 32 */
GCCOPTS="-Wall -std=gnu99 -O -pthread"
LITMUSOPTS=
Tue Dec 22 18:38:40 GMT 2009