Thu Dec 31 09:02:24 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)
232 :>3:r1=1; 3:r3=1; x=2; y=2;
277 :>3:r1=2; 3:r3=1; x=2; y=2;
40839 :>3:r1=0; 3:r3=1; x=2; y=2;
37262 :>3:r1=2; 3:r3=0; x=2; y=1;
47530 :>3:r1=2; 3:r3=0; x=1; y=2;
112 :>3:r1=0; 3:r3=0; x=2; y=2;
172337:>3:r1=1; 3:r3=0; x=1; y=2;
103454:>3:r1=1; 3:r3=1; x=2; y=1;
2947547:>3:r1=2; 3:r3=0; x=1; y=1;
482695:>3:r1=0; 3:r3=0; x=2; y=1;
83525 :>3:r1=1; 3:r3=0; x=1; y=1;
1211161:>3:r1=0; 3:r3=0; x=1; y=2;
1409600:>3:r1=1; 3:r3=1; x=1; y=2;
1879091:>3:r1=2; 3:r3=1; x=1; y=2;
3422599:>3:r1=0; 3:r3=1; x=2; y=1;
3239319:>3:r1=1; 3:r3=1; x=1; y=1;
9470766:>3:r1=0; 3:r3=0; x=1; y=1;
4717994:>3:r1=2; 3:r3=1; x=2; y=1;
1381632:>3:r1=0; 3:r3=1; x=1; y=2;
7548418:>3:r1=2; 3:r3=1; x=1; y=1;
1803610:>3:r1=0; 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=7074ebf0a4e494a7c168353216394741
Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr000 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr000 101.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
754 :>3:r1=2; 3:r3=1; x=2; y=2;
4792 :>3:r1=0; 3:r3=0; x=2; y=2;
39306 :>3:r1=2; 3:r3=0; x=1; y=2;
46948 :>3:r1=1; 3:r3=0; x=1; y=1;
675 :>3:r1=1; 3:r3=1; x=2; y=2;
102120:>3:r1=2; 3:r3=0; x=2; y=1;
233861:>3:r1=1; 3:r3=1; x=2; y=1;
166485:>3:r1=1; 3:r3=0; x=1; y=2;
2125687:>3:r1=2; 3:r3=0; x=1; y=1;
96348 :>3:r1=0; 3:r3=1; x=2; y=2;
1595065:>3:r1=0; 3:r3=0; x=2; y=1;
1426171:>3:r1=0; 3:r3=0; x=1; y=2;
1042338:>3:r1=0; 3:r3=1; x=1; y=2;
1748217:>3:r1=1; 3:r3=1; x=1; y=2;
2072401:>3:r1=2; 3:r3=1; x=1; y=2;
916329:>3:r1=0; 3:r3=1; x=1; y=1;
8148189:>3:r1=0; 3:r3=0; x=1; y=1;
6462240:>3:r1=2; 3:r3=1; x=1; y=1;
2777167:>3:r1=1; 3:r3=1; x=1; y=1;
7156588:>3:r1=2; 3:r3=1; x=2; y=1;
3838319:>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=42a8ec6eccd807ced6dea1376fc81b0b
Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr001 No ACLwSyncdRR
Safe=Fre Wse SyncdWW LwSyncdWW
Time aclwdrr001 104.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5094170:>2:r1=2; 2:r3=0; x=1;
704875:>2:r1=2; 2:r3=1; x=2;
4000080:>2:r1=1; 2:r3=1; x=1;
3314388:>2:r1=0; 2:r3=1; x=1;
2663266:>2:r1=0; 2:r3=1; x=2;
12845807:>2:r1=0; 2:r3=0; x=1;
10574256:>2:r1=2; 2:r3=1; x=1;
724386:>2:r1=1; 2:r3=1; x=2;
78772 :>2:r1=0; 2:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated
Hash=e86498b53008de1e6a240afbf078cd14
Cycle=Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr002 No ACLwSyncdRR
Safe=Fre Wse SyncdWW
Time aclwdrr002 59.30
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
404 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
386 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
479 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
115242:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
33082 :>0:r3=1; 3:r1=2; 3:r3=0; y=2;
187036:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
105090:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
130785:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
1211231:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
85076 :>0:r3=1; 3:r1=1; 3:r3=0; y=2;
1246343:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
4532736:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
869728:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
3382580:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
1340473:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
1710930:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
9005205:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
6067368:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
1276433:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
5324321:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
3375072:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=9599d8c79b2e28a1f015a74966a65bac
Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr003 No ACLwSyncdRR
Safe=Fre Wse SyncdWW SyncdWR
Time aclwdrr003 85.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2315 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2746 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
145 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
7967 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
7397 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1676 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
282 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
24376 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
18167 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
419256:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
113442:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
103990:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
2109 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
2407 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
442041:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
30696 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
603774:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
836219:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
424955:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
47530 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
665285:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
530777:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
491204:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
2527968:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
604242:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
116492:>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
1598287:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
2955951:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
2479422:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1451284:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
3665878:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
1948025:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
5302756:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
4141379:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
1401558:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
2495556:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
1937856:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
2594589:>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=32cc2d7800b6941b57852b520691800f
Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr004 No ACLwSyncdRR
Safe=Fre Wse SyncsWR SyncdWW
Time aclwdrr004 121.54
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
476 :>3:r1=0; 3:r3=0; x=2; y=2;
11761 :>3:r1=2; 3:r3=0; x=2; y=1;
109817:>3:r1=1; 3:r3=0; x=1; y=1;
6988 :>3:r1=2; 3:r3=1; x=2; y=2;
7268 :>3:r1=1; 3:r3=1; x=2; y=2;
92792 :>3:r1=0; 3:r3=1; x=2; y=2;
431654:>3:r1=0; 3:r3=0; x=2; y=1;
192597:>3:r1=2; 3:r3=0; x=1; y=2;
756981:>3:r1=1; 3:r3=0; x=1; y=2;
2949461:>3:r1=2; 3:r3=0; x=1; y=1;
3508596:>3:r1=0; 3:r3=1; x=2; y=1;
3780810:>3:r1=2; 3:r3=1; x=1; y=2;
1607338:>3:r1=0; 3:r3=0; x=1; y=2;
2852827:>3:r1=1; 3:r3=1; x=1; y=2;
2598572:>3:r1=1; 3:r3=1; x=1; y=1;
3924921:>3:r1=2; 3:r3=1; x=2; y=1;
980853:>3:r1=0; 3:r3=1; x=1; y=2;
1363430:>3:r1=0; 3:r3=1; x=1; y=1;
6352003:>3:r1=2; 3:r3=1; x=1; y=1;
8209289:>3:r1=0; 3:r3=0; x=1; y=1;
261566:>3:r1=1; 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 103.99
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
12757 :>3:r1=0; 3:r3=0; x=2; y=2;
71060 :>3:r1=1; 3:r3=0; x=1; y=1;
18321 :>3:r1=2; 3:r3=1; x=2; y=2;
156674:>3:r1=2; 3:r3=0; x=1; y=2;
16340 :>3:r1=1; 3:r3=1; x=2; y=2;
39658 :>3:r1=2; 3:r3=0; x=2; y=1;
1705111:>3:r1=2; 3:r3=0; x=1; y=1;
494445:>3:r1=1; 3:r3=0; x=1; y=2;
316795:>3:r1=0; 3:r3=1; x=2; y=2;
692951:>3:r1=1; 3:r3=1; x=2; y=1;
1350744:>3:r1=0; 3:r3=0; x=1; y=2;
2497013:>3:r1=1; 3:r3=1; x=1; y=1;
676893:>3:r1=0; 3:r3=1; x=1; y=2;
3338480:>3:r1=0; 3:r3=1; x=2; y=1;
3032768:>3:r1=1; 3:r3=1; x=1; y=2;
7058042:>3:r1=0; 3:r3=0; x=1; y=1;
5594693:>3:r1=2; 3:r3=1; x=1; y=1;
635896:>3:r1=0; 3:r3=1; x=1; y=1;
3877101:>3:r1=2; 3:r3=1; x=1; y=2;
1552308:>3:r1=0; 3:r3=0; x=2; y=1;
6861950:>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=7e01ecd8b2bc06ff5ba0d2b4e58340c6
Cycle=Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr006 No ACLwSyncdRR
Safe=Fre Wse LwSyncdWW
Time aclwdrr006 99.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Results for ./src/aclwdrr007.litmus %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
PPC
aclwdrr007
"Fre LwSyncdWW Wse Rfe LwSyncdRR"
{0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;}
P0 | P1 | P2 ;
li r1,1 | li r1,2 | lwz r1,0(r2) ;
stw r1,0(r2) | stw r1,0(r2) | lwsync ;
lwsync | | lwz r3,0(r4) ;
li r3,1 | | ;
stw r3,0(r4) | | ;
exists (x=2 /\ 2:r1=2 /\ 2:r3=0)
Generated assembler
_litmus_P0_0_: li 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)
2517995:>2:r1=2; 2:r3=0; x=1;
447474:>2:r1=0; 2:r3=0; x=2;
1189693:>2:r1=0; 2:r3=1; x=2;
3389454:>2:r1=1; 2:r3=1; x=1;
4230854:>2:r1=2; 2:r3=1; x=2;
1135689:>2:r1=0; 2:r3=1; x=1;
10275897:>2:r1=2; 2:r3=1; x=1;
4376568:>2:r1=1; 2:r3=1; x=2;
12436376:>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.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
207476:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
3469 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
38211 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
33875 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
76469 :>0:r3=0; 3:r1=2; 3:r3=0; y=1;
245223:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
281379:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
215529:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
663740:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
939708:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
2254413:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
2762587:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
2838436:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
3500416:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
1223610:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
8365816:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
4559765:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
924737:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
4829940:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
1312406:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
4722795:>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 84.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
117 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
438 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
9937 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
8686 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
11713 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
11483 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
48037 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
89663 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
38251 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
129071:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
424695:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
388151:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
40352 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
147601:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
221264:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
585074:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
39714 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
1297661:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
2671658:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1007011:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
821003:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1023125:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
394060:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
100905:>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
310825:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
117969:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
1660412:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
2575154:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
3791476:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1889237:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
3053016:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
1547409:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
2429810:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
3552221:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
2166121:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
5023559:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
2111058:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
262062:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=ab46080bf73ab92da49cdd6b27ede9b2
Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR
Relax aclwdrr009 No ACLwSyncdRR
Safe=Fre Wse SyncsWR LwSyncdWW
Time aclwdrr009 118.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
121317:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
193791:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
637331:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
125130:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
3431885:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
119022:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
843507:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
4565962:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
289077:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
2267579:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
12953957:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1;
3493700:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
3594672:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
4684717:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
2678353:>0:r1=1; 0:r3=1; 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 59.06
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
129 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
16269 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
2890 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
57922 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
3183657:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
476798:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
357676:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
2171665:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
4360039:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
2043532:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
4304810:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
1090831:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
8294005:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
9212539:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
4427238:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=064d7a96bedb614c156f5bd3adf783d8
Cycle=Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr011 No ACLwSyncdRR
Safe=Fre SyncdWW
Time aclwdrr011 68.94
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
8 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
85 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
6109 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
6082 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2161 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
558 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
104860:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
64976 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
32974 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
21516 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
60370 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
247843:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
300358:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
339398:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
751516:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
273041:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1060191:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
1726097:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
132426:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
777563:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
296797:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
863885:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
2983093:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
4495912:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
3160596:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
3369707:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
2218877:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
6244932:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
3033271:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1617749:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1838543:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
1991256:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1977250:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=992754280de579a7f5feb516274ac846
Cycle=Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr012 No ACLwSyncdRR
Safe=Fre SyncsWW
Time aclwdrr012 100.79
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5686 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
12430 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
42040 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
296047:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
331127:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
2189282:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
2427047:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
3616889:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
2976985:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
7110694:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
7883410:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
702768:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
4772941:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
1439169:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
6193485:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=4eddb3c8ea9ccf8a71927b2e31094cad
Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr013 No ACLwSyncdRR
Safe=Fre LwSyncdWW
Time aclwdrr013 66.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)
1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
4 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
27 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
55 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
2482 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
2168 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
12397 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
63586 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
10997 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
129355:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
126258:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
99395 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
30446 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
96030 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
182281:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
170766:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
1154769:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
172160:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1323377:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
318174:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
615190:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
166827:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
385812:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
39985 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
3786263:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1844779:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
363414:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
3268332:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
3293030:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
3573978:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
4140658:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
10698818:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
3928186:>1:r1=0; 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=0363e525d1d5c107b6654781a780ef6a
Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR
Relax aclwdrr014 No ACLwSyncdRR
Safe=Fre LwSyncsWW
Time aclwdrr014 102.12
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
213 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
175620:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
1897 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
53866 :>1:r3=0; 3:r1=0; 3:r3=1; x=2;
169257:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
2119490:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
1048881:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
3139973:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
6068222:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
1315372:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
3808954:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
974965:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
9117038:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
9360359:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
2645893:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
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 80.62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3278 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
85420 :>1:r3=0; 3:r1=1; 3:r3=0; x=1;
320121:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
135261:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
2689509:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
2292767:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
3411263:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
1539794:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
7016716:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
2579921:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
504731:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
2426120:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
7524063:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
9464506:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
6530 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=4947e9ed11cb60630be5b54900bf7b6c
Cycle=Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr016 No ACLwSyncdRR
Safe=Fre Wse SyncdWR LwSyncdWW
Time aclwdrr016 79.88
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
105183:>0:r3=0; 2:r1=0; 2:r3=0;
2451623:>0:r3=0; 2:r1=1; 2:r3=1;
3903459:>0:r3=0; 2:r1=0; 2:r3=1;
12827629:>0:r3=1; 2:r1=0; 2:r3=0;
5398917:>0:r3=1; 2:r1=1; 2:r3=0;
12235386:>0:r3=1; 2:r1=1; 2:r3=1;
3077803:>0:r3=1; 2:r1=0; 2:r3=1;
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 46.95
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
409 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
272079:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
82518 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
4802107:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
1151219:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
3321990:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
1105432:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
3057345:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
2056233:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
5861084:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
5948 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
1091124:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
8761828:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
8348795:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1;
81889 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated
Hash=3fed6cc74892902ab28df779672578f8
Cycle=Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR
Relax aclwdrr018 No ACLwSyncdRR
Safe=Fre SyncdWR
Time aclwdrr018 70.22
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
186 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
2341 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
5237 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
12084 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1260 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
69697 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
160174:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
6654 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
412337:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
455532:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
1535168:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
810367:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
241585:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
3150157:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
69075 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
46237 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
131958:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
3359125:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
604576:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
3308689:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
2039266:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
1757733:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
355102:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
6607655:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
2157806:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
4360548:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
1905874:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
4810354:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
619095:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1004125:>0:r3=1; 1:r3=0; 3:r1=0; 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.07
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (45 states)
1 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
21 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
47 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
25 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
516 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
487 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
44 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
2364 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
76 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
17987 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
10519 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
47295 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
613113:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
57000 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
30186 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
171017:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
106990:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
10629 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
432192:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
14119 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
477577:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
432403:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
404632:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
2202360:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
484335:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
591304:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
474464:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
1831766:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
343086:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
753016:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
3988943:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
1210864:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
4484511:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
370755:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
663124:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
374532:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
2145175:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
2115935:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
2380395:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
1110126:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
4810735:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
732807:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
2271663:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
1185233:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
2645631:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
No
Witnesses
Positive: 0, Negative: 40000000
Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated
Hash=bad92812900a1656a66221eff19f711e
Cycle=Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR
Relax aclwdrr020 No ACLwSyncdRR
Safe=Fre SyncsWR SyncdWR
Time aclwdrr020 115.00
$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
Thu Dec 31 09:32:57 CET 2009