Wed Dec 30 09:35:14 CET 2009
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr000.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr000
"Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr000 Allowed
Histogram (21 states)
130 :>3:r1=0; 3:r3=0; x=2; y=2;
37829 :>3:r1=2; 3:r3=0; x=2; y=1;
72189 :>3:r1=1; 3:r3=0; x=1; y=1;
48405 :>3:r1=2; 3:r3=0; x=1; y=2;
125362:>3:r1=1; 3:r3=1; x=2; y=1;
268 :>3:r1=1; 3:r3=1; x=2; y=2;
285 :>3:r1=2; 3:r3=1; x=2; y=2;
180414:>3:r1=1; 3:r3=0; x=1; y=2;
44279 :>3:r1=0; 3:r3=1; x=2; y=2;
1834053:>3:r1=2; 3:r3=1; x=1; y=2;
1130772:>3:r1=0; 3:r3=0; x=1; y=2;
1546965:>3:r1=1; 3:r3=1; x=1; y=2;
2841629:>3:r1=2; 3:r3=0; x=1; y=1;
1354472:>3:r1=0; 3:r3=1; x=1; y=2;
9434137:>3:r1=0; 3:r3=0; x=1; y=1;
7695974:>3:r1=2; 3:r3=1; x=1; y=1;
1719071:>3:r1=0; 3:r3=1; x=1; y=1;
3079938:>3:r1=1; 3:r3=1; x=1; y=1;
544958:>3:r1=0; 3:r3=0; x=2; y=1;
5068984:>3:r1=2; 3:r3=1; x=2; y=1;
3239886:>3:r1=0; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=7074ebf0a4e494a7c168353216394741
Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr000 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr000 101.72
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr001.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr001
"Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | sync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr001 Allowed
Histogram (21 states)
597 :>3:r1=1; 3:r3=1; x=2; y=2;
2663 :>3:r1=0; 3:r3=0; x=2; y=2;
756 :>3:r1=2; 3:r3=1; x=2; y=2;
73350 :>3:r1=1; 3:r3=0; x=1; y=1;
38378 :>3:r1=2; 3:r3=0; x=1; y=2;
152475:>3:r1=1; 3:r3=0; x=1; y=2;
99637 :>3:r1=0; 3:r3=1; x=2; y=2;
93756 :>3:r1=2; 3:r3=0; x=2; y=1;
2225644:>3:r1=2; 3:r3=0; x=1; y=1;
224705:>3:r1=1; 3:r3=1; x=2; y=1;
3586738:>3:r1=0; 3:r3=1; x=2; y=1;
1275753:>3:r1=0; 3:r3=0; x=1; y=2;
2060620:>3:r1=2; 3:r3=1; x=1; y=2;
1613774:>3:r1=0; 3:r3=0; x=2; y=1;
1630695:>3:r1=1; 3:r3=1; x=1; y=2;
1195581:>3:r1=0; 3:r3=1; x=1; y=2;
1166606:>3:r1=0; 3:r3=1; x=1; y=1;
2926367:>3:r1=1; 3:r3=1; x=1; y=1;
8242735:>3:r1=0; 3:r3=0; x=1; y=1;
6754397:>3:r1=2; 3:r3=1; x=2; y=1;
6634773:>3:r1=2; 3:r3=1; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=42a8ec6eccd807ced6dea1376fc81b0b
Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr001 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr001 105.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr002.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr002
"Fre SyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | | lwz r3,0(r4) ;
li r3,1 | | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr002 Allowed
Histogram (9 states)
58644 :>2:r1=0; 2:r3=0; x=2;
5097643:>2:r1=2; 2:r3=0; x=1;
3927997:>2:r1=1; 2:r3=1; x=1;
2735603:>2:r1=0; 2:r3=1; x=2;
663710:>2:r1=2; 2:r3=1; x=2;
3405349:>2:r1=0; 2:r3=1; x=1;
10511524:>2:r1=2; 2:r3=1; x=1;
725076:>2:r1=1; 2:r3=1; x=2;
12874454:>2:r1=0; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=e86498b53008de1e6a240afbf078cd14
Cycle=Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr002 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr002 62.92
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr003.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr003
"Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r8,0(r2)
_litmus_P1_0_: li r11,1
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr003 Allowed
Histogram (21 states)
421 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
373 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
97785 :>0:r3=1; 3:r1=1; 3:r3=0; y=1;
419 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
30632 :>0:r3=1; 3:r1=2; 3:r3=0; y=2;
133917:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
105813:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
182310:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
117260:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
1426136:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
1283361:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
1086911:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
3330785:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
1616829:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
5411703:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
4597893:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
5776220:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
1248129:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
9073871:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
3097294:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
1381938:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=9599d8c79b2e28a1f015a74966a65bac
Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr003 No ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr003 86.83
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr004.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr004
"Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr004 Allowed
Histogram (39 states)
1 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
100 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
3760 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
2927 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
414 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
10962 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
24539 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
1455 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
2525 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
24019 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
374781:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
9454 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1393 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
96950 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
413528:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
97569 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
508777:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
28835 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
363359:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
59283 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
766737:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
520534:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1670762:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
2708530:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
2742368:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
521136:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
804046:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
108028:>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
1190320:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
2546617:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
2471025:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1714338:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1880934:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1734539:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
2233948:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
4332896:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
3499461:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
6049698:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
479452:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=32cc2d7800b6941b57852b520691800f
Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr004 No ACLwSyncdRR
Safe=Fre Wse SyncsWR SyncdWW
Time aclwdrr004 122.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr005.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr005
"Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr005 Allowed
Histogram (21 states)
123 :>3:r1=0; 3:r3=0; x=2; y=2;
149980:>3:r1=1; 3:r3=0; x=1; y=1;
3428 :>3:r1=2; 3:r3=1; x=2; y=2;
13271 :>3:r1=2; 3:r3=0; x=2; y=1;
3951 :>3:r1=1; 3:r3=1; x=2; y=2;
54703 :>3:r1=0; 3:r3=1; x=2; y=2;
161567:>3:r1=1; 3:r3=1; x=2; y=1;
741506:>3:r1=1; 3:r3=0; x=1; y=2;
258025:>3:r1=2; 3:r3=0; x=1; y=2;
3435129:>3:r1=2; 3:r3=0; x=1; y=1;
1771165:>3:r1=0; 3:r3=0; x=1; y=2;
2941881:>3:r1=1; 3:r3=1; x=1; y=2;
3853123:>3:r1=2; 3:r3=1; x=1; y=2;
2858334:>3:r1=1; 3:r3=1; x=1; y=1;
1425876:>3:r1=0; 3:r3=1; x=1; y=1;
989696:>3:r1=0; 3:r3=1; x=1; y=2;
6146056:>3:r1=2; 3:r3=1; x=1; y=1;
3015091:>3:r1=0; 3:r3=1; x=2; y=1;
7975030:>3:r1=0; 3:r3=0; x=1; y=1;
379704:>3:r1=0; 3:r3=0; x=2; y=1;
3822361:>3:r1=2; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=4867d1504e0b1c594b9643e48c015b80
Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr005 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr005 102.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr006.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr006
"Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | lwsync | | lwz r3,0(r4) ;
li r3,1 | li r3,1 | | ;
stw r3,0(r4) | stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr006 Allowed
Histogram (21 states)
3138 :>3:r1=0; 3:r3=0; x=2; y=2;
13190 :>3:r1=2; 3:r3=1; x=2; y=2;
70133 :>3:r1=1; 3:r3=0; x=1; y=1;
11465 :>3:r1=1; 3:r3=1; x=2; y=2;
164918:>3:r1=2; 3:r3=0; x=1; y=2;
43766 :>3:r1=2; 3:r3=0; x=2; y=1;
2018961:>3:r1=2; 3:r3=0; x=1; y=1;
557432:>3:r1=1; 3:r3=0; x=1; y=2;
246974:>3:r1=0; 3:r3=1; x=2; y=2;
640881:>3:r1=1; 3:r3=1; x=2; y=1;
1336513:>3:r1=0; 3:r3=0; x=2; y=1;
3825313:>3:r1=2; 3:r3=1; x=1; y=2;
1248028:>3:r1=0; 3:r3=0; x=1; y=2;
3319265:>3:r1=1; 3:r3=1; x=1; y=2;
660222:>3:r1=0; 3:r3=1; x=1; y=2;
767928:>3:r1=0; 3:r3=1; x=1; y=1;
7382125:>3:r1=0; 3:r3=0; x=1; y=1;
5839177:>3:r1=2; 3:r3=1; x=1; y=1;
2479053:>3:r1=1; 3:r3=1; x=1; y=1;
6446535:>3:r1=2; 3:r3=1; x=2; y=1;
2924983:>3:r1=0; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=7e01ecd8b2bc06ff5ba0d2b4e58340c6
Cycle=Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr006 No ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr006 99.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr007
"Fre LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | | lwz r3,0(r4) ;
li r3,1 | | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,1
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr007 Allowed
Histogram (9 states)
515691:>2:r1=0; 2:r3=0; x=2;
2844593:>2:r1=2; 2:r3=0; x=1;
1126853:>2:r1=0; 2:r3=1; x=1;
4324365:>2:r1=1; 2:r3=1; x=2;
10171467:>2:r1=2; 2:r3=1; x=1;
1030026:>2:r1=0; 2:r3=1; x=2;
3432429:>2:r1=1; 2:r3=1; x=1;
4230757:>2:r1=2; 2:r3=1; x=2;
12323819:>2:r1=0; 2:r3=0; x=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=ba17863040d25a62a648bb8030bf59fd
Cycle=Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr007 No ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr007 61.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr008.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr008
"Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | | lwz r3,0(r4) ;
lwz r3,0(r4) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r8,0(r2)
_litmus_P1_0_: li r11,1
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr008 Allowed
Histogram (21 states)
1636 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
45757 :>0:r3=0; 3:r1=2; 3:r3=0; y=1;
200939:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
33234 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
219640:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
42674 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
658032:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
158365:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
405453:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
2706842:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
1189800:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
3451861:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
2534876:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
958745:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
795387:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
2925626:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
8615160:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
3860157:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
5539797:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
926600:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
4729419:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=61bd93196401321b8fb91e15727e3c64
Cycle=Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr008 No ACLwSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time aclwdrr008 86.05
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr009.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr009
"Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | lwsync | | lwz r3,0(r4) ;
lwz r3,0(r2) | li r3,1 | | ;
| stw r3,0(r4) | | ;
exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r11,2
_litmus_P1_1_: stw r11,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r10,1
_litmus_P1_4_: stw r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr009 Allowed
Histogram (38 states)
106 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
422 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
8675 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
11008 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5399 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
32236 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
41798 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
9890 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
32316 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
74952 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
148668:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
347862:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
328132:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
126150:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
359317:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
1005430:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
262699:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
165884:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
48576 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
924741:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
109798:>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
213023:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
1391650:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
271383:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
480008:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
2461655:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
3710425:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
5055630:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
2593387:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
2453600:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
679008:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1945331:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1955040:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
4095423:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
2905583:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1961941:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
1716581:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
2066273:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=ab46080bf73ab92da49cdd6b27ede9b2
Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr009 No ACLwSyncdRR
Safe=Fre Wse SyncsWR LwSyncdWW
Time aclwdrr009 118.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr010.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr010
"Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;}
P0 | P1 | P2 | P3 ;
lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ;
lwsync | stw r1,0(r2) | lwsync | stw r1,0(r2) ;
lwz r3,0(r4) | | lwz r3,0(r4) | ;
exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: lwz r7,0(r9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz r8,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
_litmus_P3_0_: li r9,1
_litmus_P3_1_: stw r9,0(r2)
Test aclwdrr010 Allowed
Histogram (15 states)
224053:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
114956:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
280405:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
147954:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
122159:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
4848215:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
1763394:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
2606857:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
3304753:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
3767513:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
13122673:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1;
922966:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
4659592:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
3393077:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
721433:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=8ce05c9f86d49b2adfd5546bd471aa44
Cycle=Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr010 No ACLwSyncdRR
Safe=Fre
Time aclwdrr010 58.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr011
"Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,1 | | | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr011 Allowed
Histogram (15 states)
14626 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
161 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
3388 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
73412 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
419216:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
413710:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
2498657:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
2481609:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
4078194:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
3408861:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
4629262:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
4034543:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
1170945:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
8064605:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
8708811:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=064d7a96bedb614c156f5bd3adf783d8
Cycle=Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr011 No ACLwSyncdRR
Safe=Fre SyncdWW
Time aclwdrr011 69.41
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr012.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr012
"Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,2 | | | ;
stw r3,0(r2) | | | ;
exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr012 Allowed
Histogram (33 states)
12 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
100 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
659 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1979 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
9765 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
62499 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
125007:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
9844 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
84330 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
23928 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
250688:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
941507:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1687028:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
298190:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
1884238:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
35445 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1081414:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
2052134:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1657816:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
371520:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
298859:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
4121241:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
3317937:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
2349661:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
2950528:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
2858699:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1578087:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
331297:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
147313:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
3514443:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
776423:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
6216747:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
960662:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=992754280de579a7f5feb516274ac846
Cycle=Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr012 No ACLwSyncdRR
Safe=Fre SyncsWW
Time aclwdrr012 96.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr013
"Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,1 | | | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr013 Allowed
Histogram (15 states)
4524 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
5769 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
28502 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
261497:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
333531:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
1366421:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
2057379:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
1774713:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
765929:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
3545644:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
3140618:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
6285985:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
7381699:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
8181006:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
4866783:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=4eddb3c8ea9ccf8a71927b2e31094cad
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr013 No ACLwSyncdRR
Safe=Fre LwSyncdWW
Time aclwdrr013 70.82
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr014.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr014
"Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,2 | | | ;
stw r3,0(r2) | | | ;
exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r11,2
_litmus_P0_4_: stw r11,0(r2)
_litmus_P1_0_: lwz r7,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr014 Allowed
Histogram (33 states)
3 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
88 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
49 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
9 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
2051 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1505 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
31012 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
12207 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
146549:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
11592 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
120077:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
86192 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
57766 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
265842:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
132370:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
414725:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
315368:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
168374:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1480218:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
314029:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
40180 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
4451047:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
3108673:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
3825326:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
3338563:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
710402:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
237115:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
10799555:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
3917824:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
3456678:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1249544:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
1226311:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
78756 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=0363e525d1d5c107b6654781a780ef6a
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr014 No ACLwSyncdRR
Safe=Fre LwSyncsWW
Time aclwdrr014 104.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr015.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr015
"Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
li r3,1 | lwz r3,0(r4) | | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr015 Allowed
Histogram (15 states)
375 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
2603 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
113929:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
169827:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
1713183:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
1158531:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
66275 :>1:r3=0; 3:r1=0; 3:r3=1; x=2;
3964495:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
3206710:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
1981095:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
8753513:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
1235412:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
2982200:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
9086656:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
5565196:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=61d664ae95ff6d97da76ebb37bc47ca3
Cycle=Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr015 No ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr015 85.53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr016.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr016
"Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | sync | | lwz r3,0(r4) ;
li r3,1 | lwz r3,0(r4) | | ;
stw r3,0(r4) | | | ;
exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r11,1
_litmus_P0_1_: stw r11,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r10,1
_litmus_P0_4_: stw r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr016 Allowed
Histogram (15 states)
4088 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
7070 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
92857 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
209312:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
146221:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
1612034:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
2270092:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
2296581:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
2157881:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
7217833:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
606990:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
2861636:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
7801261:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
9111631:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
3604513:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=4947e9ed11cb60630be5b54900bf7b6c
Cycle=Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr016 No ACLwSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time aclwdrr016 87.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr017
"Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | | ;
exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r8,1
_litmus_P0_1_: stw r8,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r7,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r8,0(r2)
Test aclwdrr017 Allowed
Histogram (7 states)
2502044:>0:r3=0; 2:r1=1; 2:r3=1;
2704135:>0:r3=1; 2:r1=0; 2:r3=1;
5639336:>0:r3=1; 2:r1=1; 2:r3=0;
12788852:>0:r3=1; 2:r1=0; 2:r3=0;
12183964:>0:r3=1; 2:r1=1; 2:r3=1;
4081994:>0:r3=0; 2:r1=0; 2:r3=1;
99675 :>0:r3=0; 2:r1=0; 2:r3=0;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated
Hash=0dd8df1959f84e11508b32d374a44775
Cycle=Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr017 No ACLwSyncdRR
Safe=Fre SyncdWR
Time aclwdrr017 47.61
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr018
"Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | lwz r3,0(r4) | | ;
exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r8,0(r2)
_litmus_P1_0_: li r10,1
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr018 Allowed
Histogram (15 states)
107935:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
570 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
6562 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
86583 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
1913301:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
181768:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
3218859:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
9148677:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1;
1222703:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
4055703:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
1056700:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
8731161:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
1198062:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
5960479:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
3110937:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=3fed6cc74892902ab28df779672578f8
Cycle=Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr018 No ACLwSyncdRR
Safe=Fre SyncdWR
Time aclwdrr018 71.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr019.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr019
"Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r2) | lwz r3,0(r4) | | ;
exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r9,1
_litmus_P0_1_: stw r9,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r10,0(r2)
_litmus_P1_0_: li r10,2
_litmus_P1_1_: stw r10,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r8,0(r2)
_litmus_P2_0_: li r9,1
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr019 Allowed
Histogram (31 states)
1 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
200 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1048 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
69235 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
2961 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
4697 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
14111 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
9531 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
682147:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
598597:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
62715 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
244582:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
1530633:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
871994:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
51830 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
4259436:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
614052:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
2021165:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
143063:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
2808868:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
2946138:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
172976:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
662562:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
4945932:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
2172239:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
343531:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
3196387:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
2479251:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
5954806:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
2091911:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1043401:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=660c5e262906b3ab9066962d8bf69882
Cycle=Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr019 No ACLwSyncdRR
Safe=Fre SyncsWR SyncdWR
Time aclwdrr019 101.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr020.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr020
"Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 3:r2=x; 3:r4=y;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | lwz r3,0(r2) | | ;
exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r10,1
_litmus_P0_1_: stw r10,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r8,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r10,0(r2)
_litmus_P2_0_: li r9,2
_litmus_P2_1_: stw r9,0(r2)
_litmus_P3_0_: lwz r7,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r8,0(r2)
Test aclwdrr020 Allowed
Histogram (44 states)
8 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
255 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
17 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
94 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
43 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
32 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
400 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
11800 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
2181 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
12202 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
12611 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
175743:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
76873 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
69229 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
1903018:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
2338051:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
810645:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
954392:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
33873 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
327098:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
320846:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
478419:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
529333:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
16499 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
1104983:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
250231:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
946329:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
2968593:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
1287459:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
895017:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
429999:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
1937568:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
2301533:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
2228938:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
378997:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
390677:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
808732:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
3511362:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
632946:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
5457200:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
3814051:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
40975 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
2088410:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
452338:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=bad92812900a1656a66221eff19f711e
Cycle=Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR
Relax aclwdrr020 No ACLwSyncdRR
Safe=Fre SyncsWR SyncdWR
Time aclwdrr020 112.20
$Revision: 3163 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=-r 40
Wed Dec 30 10:06:07 CET 2009