Mon Jan 4 13:37:14 CET 2010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr000 Allowed
Histogram (21 states)
4778519:>3:r1=0; 3:r3=0; x=1; y=1;
51968 :>3:r1=1; 3:r3=0; x=1; y=1;
1651477:>3:r1=2; 3:r3=0; x=1; y=1;
945117:>3:r1=0; 3:r3=1; x=1; y=1;
1460953:>3:r1=1; 3:r3=1; x=1; y=1;
3470779:>3:r1=2; 3:r3=1; x=1; y=1;
360578:>3:r1=0; 3:r3=0; x=2; y=1;
23554 :>3:r1=2; 3:r3=0; x=2; y=1;
1693722:>3:r1=0; 3:r3=1; x=2; y=1;
56876 :>3:r1=1; 3:r3=1; x=2; y=1;
2224085:>3:r1=2; 3:r3=1; x=2; y=1;
642610:>3:r1=0; 3:r3=0; x=1; y=2;
69382 :>3:r1=1; 3:r3=0; x=1; y=2;
19655 :>3:r1=2; 3:r3=0; x=1; y=2;
759633:>3:r1=0; 3:r3=1; x=1; y=2;
812114:>3:r1=1; 3:r3=1; x=1; y=2;
963586:>3:r1=2; 3:r3=1; x=1; y=2;
78 :>3:r1=0; 3:r3=0; x=2; y=2;
15154 :>3:r1=0; 3:r3=1; x=2; y=2;
77 :>3:r1=1; 3:r3=1; x=2; y=2;
83 :>3:r1=2; 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=7074ebf0a4e494a7c168353216394741
Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr000 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr000 34.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr001 Allowed
Histogram (21 states)
4121898:>3:r1=0; 3:r3=0; x=1; y=1;
22306 :>3:r1=1; 3:r3=0; x=1; y=1;
1130965:>3:r1=2; 3:r3=0; x=1; y=1;
539413:>3:r1=0; 3:r3=1; x=1; y=1;
1269271:>3:r1=1; 3:r3=1; x=1; y=1;
3165386:>3:r1=2; 3:r3=1; x=1; y=1;
951119:>3:r1=0; 3:r3=0; x=2; y=1;
38592 :>3:r1=2; 3:r3=0; x=2; y=1;
2254827:>3:r1=0; 3:r3=1; x=2; y=1;
89543 :>3:r1=1; 3:r3=1; x=2; y=1;
3016651:>3:r1=2; 3:r3=1; x=2; y=1;
994698:>3:r1=0; 3:r3=0; x=1; y=2;
85863 :>3:r1=1; 3:r3=0; x=1; y=2;
13271 :>3:r1=2; 3:r3=0; x=1; y=2;
571696:>3:r1=0; 3:r3=1; x=1; y=2;
626625:>3:r1=1; 3:r3=1; x=1; y=2;
1053625:>3:r1=2; 3:r3=1; x=1; y=2;
3102 :>3:r1=0; 3:r3=0; x=2; y=2;
50248 :>3:r1=0; 3:r3=1; x=2; y=2;
358 :>3:r1=1; 3:r3=1; x=2; y=2;
543 :>3:r1=2; 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=42a8ec6eccd807ced6dea1376fc81b0b
Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr001 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr001 33.86
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r27,1
_litmus_P0_4_: stw r27,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r26,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r27,0(r2)
Test aclwdrr002 Allowed
Histogram (9 states)
6505620:>2:r1=0; 2:r3=0; x=1;
2878213:>2:r1=2; 2:r3=0; x=1;
1440444:>2:r1=0; 2:r3=1; x=1;
1967587:>2:r1=1; 2:r3=1; x=1;
5010070:>2:r1=2; 2:r3=1; x=1;
54466 :>2:r1=0; 2:r3=0; x=2;
1405172:>2:r1=0; 2:r3=1; x=2;
345539:>2:r1=1; 2:r3=1; x=2;
392889:>2:r1=2; 2:r3=1; x=2;
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 21.19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r27,0(r2)
_litmus_P1_0_: li r28,1
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr003 Allowed
Histogram (21 states)
511543:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
4917210:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
35874 :>0:r3=1; 3:r1=1; 3:r3=0; y=1;
89769 :>0:r3=0; 3:r1=2; 3:r3=0; y=1;
1996052:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
2522057:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
687018:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
70457 :>0:r3=0; 3:r1=1; 3:r3=1; y=1;
1222050:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
2216302:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
2837383:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
143 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
989928:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
67472 :>0:r3=1; 3:r1=1; 3:r3=0; y=2;
9939 :>0:r3=1; 3:r1=2; 3:r3=0; y=2;
41789 :>0:r3=0; 3:r1=0; 3:r3=1; y=2;
800033:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
232 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
493655:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
291 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
490803:>0:r3=1; 3:r1=2; 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=9599d8c79b2e28a1f015a74966a65bac
Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr003 No ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr003 29.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr004 Allowed
Histogram (38 states)
2421595:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
251906:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
360422:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1327883:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1594851:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
221497:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
14282 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
469851:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
100442:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
941238:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
791641:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
851072:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
234683:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
24798 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
10164 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
799195:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1386203:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
54002 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
232755:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
772083:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
52 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1059144:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
335 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
1309165:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
81309 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
404453:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
45782 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
2815331:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1105934:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
276 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1343 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1222 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
287254:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
22047 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1873 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
566 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2729 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
622 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; 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 31.31
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr005 Allowed
Histogram (21 states)
3979791:>3:r1=0; 3:r3=0; x=1; y=1;
56501 :>3:r1=1; 3:r3=0; x=1; y=1;
1404819:>3:r1=2; 3:r3=0; x=1; y=1;
735896:>3:r1=0; 3:r3=1; x=1; y=1;
1153866:>3:r1=1; 3:r3=1; x=1; y=1;
3177478:>3:r1=2; 3:r3=1; x=1; y=1;
344464:>3:r1=0; 3:r3=0; x=2; y=1;
9314 :>3:r1=2; 3:r3=0; x=2; y=1;
2009242:>3:r1=0; 3:r3=1; x=2; y=1;
74521 :>3:r1=1; 3:r3=1; x=2; y=1;
1679057:>3:r1=2; 3:r3=1; x=2; y=1;
1107841:>3:r1=0; 3:r3=0; x=1; y=2;
374384:>3:r1=1; 3:r3=0; x=1; y=2;
100212:>3:r1=2; 3:r3=0; x=1; y=2;
518804:>3:r1=0; 3:r3=1; x=1; y=2;
1317231:>3:r1=1; 3:r3=1; x=1; y=2;
1913771:>3:r1=2; 3:r3=1; x=1; y=2;
186 :>3:r1=0; 3:r3=0; x=2; y=2;
39190 :>3:r1=0; 3:r3=1; x=2; y=2;
1635 :>3:r1=1; 3:r3=1; x=2; y=2;
1797 :>3:r1=2; 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=4867d1504e0b1c594b9643e48c015b80
Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr005 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr005 34.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_P0_0_: li r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr006 Allowed
Histogram (21 states)
3584989:>3:r1=0; 3:r3=0; x=1; y=1;
49829 :>3:r1=1; 3:r3=0; x=1; y=1;
883688:>3:r1=2; 3:r3=0; x=1; y=1;
357170:>3:r1=0; 3:r3=1; x=1; y=1;
1394749:>3:r1=1; 3:r3=1; x=1; y=1;
2817354:>3:r1=2; 3:r3=1; x=1; y=1;
617822:>3:r1=0; 3:r3=0; x=2; y=1;
18916 :>3:r1=2; 3:r3=0; x=2; y=1;
1684341:>3:r1=0; 3:r3=1; x=2; y=1;
353420:>3:r1=1; 3:r3=1; x=2; y=1;
2944149:>3:r1=2; 3:r3=1; x=2; y=1;
1179746:>3:r1=0; 3:r3=0; x=1; y=2;
290527:>3:r1=1; 3:r3=0; x=1; y=2;
100293:>3:r1=2; 3:r3=0; x=1; y=2;
387260:>3:r1=0; 3:r3=1; x=1; y=2;
1690234:>3:r1=1; 3:r3=1; x=1; y=2;
1528538:>3:r1=2; 3:r3=1; x=1; y=2;
2569 :>3:r1=0; 3:r3=0; x=2; y=2;
105590:>3:r1=0; 3:r3=1; x=2; y=2;
3938 :>3:r1=1; 3:r3=1; x=2; y=2;
4878 :>3:r1=2; 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 33.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r27,1
_litmus_P0_4_: stw r27,0(r2)
_litmus_P1_0_: li r9,2
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r26,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r27,0(r2)
Test aclwdrr007 Allowed
Histogram (9 states)
5794040:>2:r1=0; 2:r3=0; x=1;
1666417:>2:r1=2; 2:r3=0; x=1;
813641:>2:r1=0; 2:r3=1; x=1;
1547228:>2:r1=1; 2:r3=1; x=1;
4789605:>2:r1=2; 2:r3=1; x=1;
720531:>2:r1=0; 2:r3=0; x=2;
977497:>2:r1=0; 2:r3=1; x=2;
1742163:>2:r1=1; 2:r3=1; x=2;
1948878:>2:r1=2; 2:r3=1; x=2;
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 20.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r27,0(r2)
_litmus_P1_0_: li r28,1
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr008 Allowed
Histogram (21 states)
369103:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
4327503:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
173123:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
30173 :>0:r3=0; 3:r1=2; 3:r3=0; y=1;
2302518:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
2356503:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
480068:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
74663 :>0:r3=0; 3:r1=1; 3:r3=1; y=1;
1446688:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
1963013:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
1993314:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
811 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
1027878:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
433664:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
145556:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
86628 :>0:r3=0; 3:r1=0; 3:r3=1; y=2;
532328:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
10959 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
1113205:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
10332 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
1121970:>0:r3=1; 3:r1=2; 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 29.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: lwsync
_litmus_P1_3_: li r3,1
_litmus_P1_4_: stw r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr009 Allowed
Histogram (38 states)
1850907:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
160771:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
153106:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1395751:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1597584:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
193895:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
38112 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
677450:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
399736:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
340388:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
1251326:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1664948:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
315855:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
231338:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
111325:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
657884:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
1798174:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
19434 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
130661:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
772790:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
50 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
678735:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
244 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
1158042:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
82777 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
463177:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
76339 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
2307259:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
861582:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
2425 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
12891 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
7084 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
403592:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
35810 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
72354 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
7115 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
62963 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
6126 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; 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=ab46080bf73ab92da49cdd6b27ede9b2
Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr009 No ACLwSyncdRR
Safe=Fre Wse SyncsWR LwSyncdWW
Time aclwdrr009 30.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 r27,0(r9)
_litmus_P0_1_: lwsync
_litmus_P0_2_: lwz r30,0(r2)
_litmus_P1_0_: li r5,1
_litmus_P1_1_: stw r5,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r30,0(r2)
_litmus_P3_0_: li r6,1
_litmus_P3_1_: stw r6,0(r2)
Test aclwdrr010 Allowed
Histogram (15 states)
1036524:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
162698:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
1762333:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
2251641:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
57314 :>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
324171:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
62789 :>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
1856162:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
362218:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
68177 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
1680774:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
2364933:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
91393 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
1247166:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
6671707:>0:r1=1; 0:r3=1; 2:r1=1; 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 19.48
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr011.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr011
"Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
sync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,1 | | | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr011 Allowed
Histogram (15 states)
1392064:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
43 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
3979583:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
144249:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
187765:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1464213:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
7217 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
2406583:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
19523 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
788745:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1362413:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
2123949:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
249 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
4529121:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1594283:>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=064d7a96bedb614c156f5bd3adf783d8
Cycle=Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr011 No ACLwSyncdRR
Safe=Fre SyncdWW
Time aclwdrr011 23.80
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,1
_litmus_P0_1_: stw r4,0(r2)
_litmus_P0_2_: sync
_litmus_P0_3_: li r9,2
_litmus_P0_4_: stw r9,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r28,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr012 Allowed
Histogram (33 states)
1219619:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
37207 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
4405 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1832916:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1981310:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
510622:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
197624:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
697246:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
98020 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
7621 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
928184:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
56 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
4907 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
36407 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
377 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
159799:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
591176:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
5 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
1029128:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1191 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
380401:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
649237:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
191962:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
355009:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
6662 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
170889:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1619179:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1725391:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
31320 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
35950 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
951156:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1539706:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
3005318:>1:r1=2; 1:r3=1; 3:r1=1; 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 26.20
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr013.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr013
"Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ;
lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ;
li r3,1 | | | ;
stw r3,0(r4) | | | ;
exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r4,1
_litmus_P0_1_: stw r4,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r30,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr013 Allowed
Histogram (15 states)
1341744:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
1123 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
3583500:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
510601:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
115520:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1349836:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
17527 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
2019865:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
131555:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
493333:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1437870:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
2292367:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1441 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
4081956:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
2621762:>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 23.73
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r4,1
_litmus_P0_1_: stw r4,0(r2)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r9,2
_litmus_P0_4_: stw r9,0(r2)
_litmus_P1_0_: lwz r27,0(r9)
_litmus_P1_1_: lwsync
_litmus_P1_2_: lwz r28,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr014 Allowed
Histogram (32 states)
932236:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
8602 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
37537 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1905640:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
313124:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1955748:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
47403 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
537715:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
39213 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
63966 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
192622:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
5 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
301 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
11099 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
10 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
35863 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
89216 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
174153:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
31 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
78956 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1717338:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
6092 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
546569:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
47174 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
11415 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1550411:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
2347789:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1636 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
114548:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1271465:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
152952:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
5809171:>1:r1=2; 1:r3=1; 3:r1=1; 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 25.74
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r27,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr015 Allowed
Histogram (15 states)
702299:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
4601079:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
59006 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
1781896:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
1603574:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
734310:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
1101876:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
4402502:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
100 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
428743:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
92348 :>1:r3=1; 3:r1=1; 3:r3=0; x=2;
35105 :>1:r3=0; 3:r1=0; 3:r3=1; x=2;
1789862:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
1062 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
2666238:>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=61d664ae95ff6d97da76ebb37bc47ca3
Cycle=Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr015 No ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr015 29.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: lwsync
_litmus_P0_3_: li r3,1
_litmus_P0_4_: stw r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r27,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr016 Allowed
Histogram (15 states)
900121:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
4018728:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
53368 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
1453828:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
1208743:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
382142:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
1066229:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
3676411:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
1787 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
1059943:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
148080:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
96301 :>1:r3=0; 3:r1=0; 3:r3=1; x=2;
2169542:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
2933 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
3761844:>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 29.15
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr017.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr017
"Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | | ;
exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r27,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P2_0_: lwz r27,0(r9)
_litmus_P2_1_: lwsync
_litmus_P2_2_: lwz r30,0(r2)
Test aclwdrr017 Allowed
Histogram (7 states)
66871 :>0:r3=0; 2:r1=0; 2:r3=0;
6458761:>0:r3=1; 2:r1=0; 2:r3=0;
2042815:>0:r3=1; 2:r1=1; 2:r3=0;
2150476:>0:r3=0; 2:r1=0; 2:r3=1;
1188634:>0:r3=1; 2:r1=0; 2:r3=1;
1163163:>0:r3=0; 2:r1=1; 2:r3=1;
6929280:>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 17.45
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr018.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr018
"Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR"
{0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;}
P0 | P1 | P2 | P3 ;
li r1,1 | li r1,1 | li r1,1 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ;
sync | sync | | lwz r3,0(r4) ;
lwz r3,0(r4) | lwz r3,0(r4) | | ;
exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0)
Generated assembler
_litmus_P0_0_: li r30,1
_litmus_P0_1_: stw r30,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r3,0(r2)
_litmus_P1_0_: li r30,1
_litmus_P1_1_: stw r30,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r29,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r30,0(r2)
Test aclwdrr018 Allowed
Histogram (15 states)
402 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
640166:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
529776:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
4484500:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
22484 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
90680 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
1585458:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
43464 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
1870632:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
1872059:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
620506:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
2274 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
1022177:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
2922800:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
4292622:>0:r3=1; 1:r3=1; 3:r1=1; 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 24.66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r3,0(r2)
_litmus_P1_0_: li r28,2
_litmus_P1_1_: stw r28,0(r9)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r27,0(r2)
_litmus_P2_0_: li r5,1
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr019 Allowed
Histogram (31 states)
189142:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
2304163:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
239807:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
1714547:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
184016:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
882399:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
2258668:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
528014:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
279993:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
35267 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
413264:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
2112 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
7778 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
661049:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1554208:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
50348 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
196371:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
8734 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1255334:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
132 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1758629:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
482 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
202866:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
25386 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
863675:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
67707 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
16070 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
3536 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
3173963:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1122339:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; 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 27.26
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 r28,1
_litmus_P0_1_: stw r28,0(r9)
_litmus_P0_2_: sync
_litmus_P0_3_: lwz r27,0(r2)
_litmus_P1_0_: li r9,1
_litmus_P1_1_: stw r9,0(r2)
_litmus_P1_2_: sync
_litmus_P1_3_: lwz r3,0(r2)
_litmus_P2_0_: li r5,2
_litmus_P2_1_: stw r5,0(r2)
_litmus_P3_0_: lwz r27,0(r9)
_litmus_P3_1_: lwsync
_litmus_P3_2_: lwz r28,0(r2)
Test aclwdrr020 Allowed
Histogram (44 states)
5199 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
2891792:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
187085:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
470732:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
1702618:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
21715 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
528262:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
215959:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
267917:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
250435:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
1958597:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
540095:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
240475:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
926878:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
1128055:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
972 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
88238 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
990027:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
4218 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
6 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
783984:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
5065 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
1381050:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
374 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
373190:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
50392 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
50594 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
216661:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
7315 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
495286:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
32 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
123386:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
125017:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
388860:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
862521:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
10 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
36 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
161 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
10615 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
199578:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
1936752:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
115359:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
27 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
454460:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
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 26.98
$Revision: 3228 $
Parameters
#ifndef SIZE_OF_TEST
#define SIZE_OF_TEST 1000000
#endif
#ifndef NUMBER_OF_RUN
#define NUMBER_OF_RUN 1
#endif
#ifndef N_EXE
#define N_EXE (4 < N ? 1 : 4 / N)
#endif
/* gcc options: -Wall -std=gnu99 -O */
/* barrier: user */
/* tread start/join: changing */
/* memory: indirect */
/* safer: true */
/* preload: true */
/* para: self */
/* changes: false */
/* speedcheck: false */
/* proc used: 4 */
GCCOPTS="-Wall -std=gnu99 -O"
LITMUSOPTS=-r 20 -v
Mon Jan 4 13:46:47 CET 2010