Thu Dec 24 23:06:11 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)
113 :>3:r1=1; 3:r3=1; x=2; y=2;
145 :>3:r1=2; 3:r3=1; x=2; y=2;
91 :>3:r1=0; 3:r3=0; x=2; y=2;
50940 :>3:r1=1; 3:r3=0; x=1; y=1;
11642 :>3:r1=2; 3:r3=0; x=2; y=1;
18870 :>3:r1=2; 3:r3=0; x=1; y=2;
13880 :>3:r1=0; 3:r3=1; x=2; y=2;
1407703:>3:r1=2; 3:r3=0; x=1; y=1;
45542 :>3:r1=1; 3:r3=0; x=1; y=2;
56824 :>3:r1=1; 3:r3=1; x=2; y=1;
327145:>3:r1=0; 3:r3=0; x=2; y=1;
839093:>3:r1=1; 3:r3=1; x=1; y=2;
1228624:>3:r1=0; 3:r3=1; x=2; y=1;
377420:>3:r1=0; 3:r3=0; x=1; y=2;
755281:>3:r1=0; 3:r3=1; x=1; y=1;
4159111:>3:r1=2; 3:r3=1; x=1; y=1;
2754029:>3:r1=2; 3:r3=1; x=2; y=1;
643560:>3:r1=0; 3:r3=1; x=1; y=2;
4720626:>3:r1=0; 3:r3=0; x=1; y=1;
1668428:>3:r1=1; 3:r3=1; x=1; y=1;
920933:>3:r1=2; 3:r3=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 44.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1089 :>3:r1=2; 3:r3=1; x=2; y=2;
836 :>3:r1=1; 3:r3=1; x=2; y=2;
1663 :>3:r1=0; 3:r3=0; x=2; y=2;
11933 :>3:r1=2; 3:r3=0; x=1; y=2;
18885 :>3:r1=1; 3:r3=0; x=1; y=1;
55573 :>3:r1=0; 3:r3=1; x=2; y=2;
66091 :>3:r1=1; 3:r3=0; x=1; y=2;
46376 :>3:r1=2; 3:r3=0; x=2; y=1;
805731:>3:r1=2; 3:r3=0; x=1; y=1;
1254733:>3:r1=0; 3:r3=0; x=2; y=1;
617148:>3:r1=0; 3:r3=1; x=1; y=2;
1101557:>3:r1=2; 3:r3=1; x=1; y=2;
1375670:>3:r1=1; 3:r3=1; x=1; y=1;
3944113:>3:r1=2; 3:r3=1; x=2; y=1;
503275:>3:r1=0; 3:r3=0; x=1; y=2;
3206777:>3:r1=2; 3:r3=1; x=1; y=1;
1619414:>3:r1=0; 3:r3=1; x=2; y=1;
476226:>3:r1=0; 3:r3=1; x=1; y=1;
3743701:>3:r1=0; 3:r3=0; x=1; y=1;
176889:>3:r1=1; 3:r3=1; x=2; y=1;
972320:>3:r1=1; 3:r3=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 40.27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
10416 :>2:r1=0; 2:r3=0; x=2;
2174854:>2:r1=2; 2:r3=0; x=1;
335804:>2:r1=2; 2:r3=1; x=2;
1425234:>2:r1=0; 2:r3=1; x=2;
391120:>2:r1=1; 2:r3=1; x=2;
5355990:>2:r1=2; 2:r3=1; x=1;
6491192:>2:r1=0; 2:r3=0; x=1;
1928110:>2:r1=1; 2:r3=1; x=1;
1887280:>2:r1=0; 2:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 26.89
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
169 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
514 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
389 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
10135 :>0:r3=1; 3:r1=2; 3:r3=0; y=2;
44410 :>0:r3=1; 3:r1=1; 3:r3=0; y=1;
66294 :>0:r3=0; 3:r1=1; 3:r3=1; y=1;
55255 :>0:r3=0; 3:r1=2; 3:r3=0; y=1;
41891 :>0:r3=0; 3:r1=0; 3:r3=1; y=2;
26901 :>0:r3=1; 3:r1=1; 3:r3=0; y=2;
453262:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
641032:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
575236:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
596983:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
1641422:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
665760:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
1972889:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
2923778:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
3277705:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
4622519:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
1710173:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
673283:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 40.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (38 states)
224 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
310 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
281 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
1738 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1068 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
271 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
773 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
38 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
43306 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
16864 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
54124 :>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
22429 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
10353 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
389481:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
66160 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
504419:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
53382 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
281025:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
2232 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
120295:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
847888:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
1715988:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
78830 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
40838 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
251015:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1306866:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
2007897:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
342213:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
791156:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
623976:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
2063772:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
1607444:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1016176:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
2791379:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
847812:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
918778:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
429060:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
750139:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 50.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
104 :>3:r1=0; 3:r3=0; x=2; y=2;
2310 :>3:r1=1; 3:r3=1; x=2; y=2;
2322 :>3:r1=2; 3:r3=1; x=2; y=2;
77667 :>3:r1=2; 3:r3=0; x=1; y=2;
3955 :>3:r1=2; 3:r3=0; x=2; y=1;
39915 :>3:r1=1; 3:r3=0; x=1; y=1;
40312 :>3:r1=0; 3:r3=1; x=2; y=2;
302488:>3:r1=1; 3:r3=0; x=1; y=2;
1008627:>3:r1=2; 3:r3=0; x=1; y=1;
258084:>3:r1=0; 3:r3=0; x=2; y=1;
773342:>3:r1=0; 3:r3=0; x=1; y=2;
1985881:>3:r1=2; 3:r3=1; x=1; y=2;
697834:>3:r1=0; 3:r3=1; x=1; y=1;
1518912:>3:r1=1; 3:r3=1; x=1; y=2;
1177344:>3:r1=0; 3:r3=1; x=2; y=1;
594194:>3:r1=0; 3:r3=1; x=1; y=2;
3716157:>3:r1=2; 3:r3=1; x=1; y=1;
1405329:>3:r1=1; 3:r3=1; x=1; y=1;
4092974:>3:r1=0; 3:r3=0; x=1; y=1;
165550:>3:r1=1; 3:r3=1; x=2; y=1;
2136699:>3:r1=2; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 40.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
34023 :>3:r1=1; 3:r3=0; x=1; y=1;
4276 :>3:r1=0; 3:r3=0; x=2; y=2;
18042 :>3:r1=2; 3:r3=0; x=2; y=1;
191112:>3:r1=1; 3:r3=0; x=1; y=2;
972315:>3:r1=2; 3:r3=0; x=1; y=1;
6677 :>3:r1=1; 3:r3=1; x=2; y=2;
7920 :>3:r1=2; 3:r3=1; x=2; y=2;
540721:>3:r1=0; 3:r3=0; x=1; y=2;
53966 :>3:r1=2; 3:r3=0; x=1; y=2;
336624:>3:r1=1; 3:r3=1; x=2; y=1;
1892080:>3:r1=2; 3:r3=1; x=1; y=2;
893342:>3:r1=0; 3:r3=0; x=2; y=1;
352544:>3:r1=0; 3:r3=1; x=1; y=1;
1571812:>3:r1=0; 3:r3=1; x=2; y=1;
383055:>3:r1=0; 3:r3=1; x=1; y=2;
2902117:>3:r1=2; 3:r3=1; x=1; y=1;
3138623:>3:r1=2; 3:r3=1; x=2; y=1;
1629478:>3:r1=1; 3:r3=1; x=1; y=2;
3621472:>3:r1=0; 3:r3=0; x=1; y=1;
1317376:>3:r1=1; 3:r3=1; x=1; y=1;
132425:>3:r1=0; 3:r3=1; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 42.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1489261:>2:r1=2; 2:r3=0; x=1;
166345:>2:r1=0; 2:r3=0; x=2;
530230:>2:r1=0; 2:r3=1; x=2;
2409795:>2:r1=1; 2:r3=1; x=2;
1947290:>2:r1=2; 2:r3=1; x=2;
4899335:>2:r1=2; 2:r3=1; x=1;
6312793:>2:r1=0; 2:r3=0; x=1;
1621073:>2:r1=1; 2:r3=1; x=1;
623878:>2:r1=0; 2:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 25.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
634 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
10469 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
8379 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
119822:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
32025 :>0:r3=0; 3:r1=2; 3:r3=0; y=1;
138701:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
368124:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
119122:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
606277:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
478332:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
1139807:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
656226:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
1356356:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
440911:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
2547016:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
1534008:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
2611805:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
2228137:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
4312292:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
1223306:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
68251 :>0:r3=0; 3:r1=0; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 41.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (39 states)
1 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
384 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
4304 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
92 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
3860 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
6359 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
5075 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
35349 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
17561 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
315075:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
228312:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
72850 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
95333 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
254509:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
90528 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
721714:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
152604:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
38373 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
1404505:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
802442:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
18485 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1897990:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
95076 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
371349:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1729611:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
71456 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
261241:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
2496963:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
820261:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
114131:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
708992:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
353705:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
791780:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1575288:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
883989:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1482321:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
1266478:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
671894:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
139760:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 49.96
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
114730:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
91188 :>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
58425 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
64859 :>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
64706 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
1005368:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
382376:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
2143201:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
2222717:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
1434457:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
1586613:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
6500655:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1;
2031868:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
1918381:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
380456:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 30.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
89 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
2558 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
250448:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
5928 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
53735 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
223398:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
2532289:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1258815:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
1075796:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
993576:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
655335:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1991915:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
4173271:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
2172214:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
4610633:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 35.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
6 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
31 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
4033 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
979 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
4569 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
10558 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
50489 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
352 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
64486 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
140178:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
642682:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
33081 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
128997:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
112711:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1192727:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1126050:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
466267:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
129759:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
8909 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
836016:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
710933:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
378944:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1519632:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
871505:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
205024:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
961065:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1383540:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1588211:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
57951 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
2244718:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1563993:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
3132528:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
429076:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 42.63
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
6691 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
210159:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
4053 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
173796:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
11822 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1457407:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
2369051:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
4116559:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1732219:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
3656436:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
1027977:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
358049:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1235811:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
549068:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
3090902:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 33.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (32 states)
2 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
9 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
21 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
876 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
6381 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2237 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
53203 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
24829 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
77198 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
103321:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
6978 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
99062 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
18201 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
68207 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
56747 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
168003:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
429159:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
778920:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
14060 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
160988:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
363006:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
70029 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1429719:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
144835:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
2338661:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1144790:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1262038:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1324856:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
46008 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
2451170:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
5516590:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1839896:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 42.16
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
99 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
888 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
79451 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
63958 :>1:r3=1; 3:r1=1; 3:r3=0; x=2;
25015 :>1:r3=0; 3:r1=0; 3:r3=1; x=2;
1649760:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
445943:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
649210:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
1024629:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
1407908:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
661037:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
5088714:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
4591765:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
2952152:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
1359471:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 37.18
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1452 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
48343 :>1:r3=1; 3:r1=1; 3:r3=0; x=2;
43469 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
1376 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
1151519:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
50345 :>1:r3=0; 3:r1=0; 3:r3=1; x=2;
1075843:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
901283:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
946963:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
1769914:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
1335355:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
3867647:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
346496:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
4163746:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
4296249:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 38.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2986830:>0:r3=1; 2:r1=1; 2:r3=0;
55209 :>0:r3=0; 2:r1=0; 2:r3=0;
1841255:>0:r3=0; 2:r1=0; 2:r3=1;
6403169:>0:r3=1; 2:r1=0; 2:r3=0;
1470610:>0:r3=1; 2:r1=0; 2:r3=1;
1278851:>0:r3=0; 2:r1=1; 2:r3=1;
5964076:>0:r3=1; 2:r1=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 23.13
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
321 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
43442 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
6471 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
56113 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
106686:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
584801:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
584164:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
973952:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
1804658:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
509587:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
4369731:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1;
1995034:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
4371009:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
2944412:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
1649619:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 36.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (30 states)
565 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
2070 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1053 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
123 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
3877 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
17869 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
298259:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
83118 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
302786:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
402977:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
25945 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
246390:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
2951 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
96518 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
157182:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
40221 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
66712 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
918762:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
435879:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
228925:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
1591166:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
1364336:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
1951761:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
1075821:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1139973:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1393074:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1611668:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
2350177:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
3294226:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
895616:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 20000000
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 45.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
36 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
49 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
17 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
1479 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
15 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
5573 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
245 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
7820 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
227 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
91243 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
3454 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
35411 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
15507 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
17448 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
992817:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
580822:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
8003 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
572961:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
1318619:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
47515 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
235775:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
157597:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
197614:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
189706:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
239899:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
525883:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
506758:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
174510:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
881337:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
1521805:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
1851938:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
413159:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
474206:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
134710:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
917887:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
2083969:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
973368:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
161620:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
2708772:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
344452:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
493842:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
181032:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
930895:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 20000000
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 48.02
$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: false */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 "
LITMUSOPTS=-r 20
Thu Dec 24 23:19:46 CET 2009