Fri Jan 1 16:48:54 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 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)
209 :>3:r1=0; 3:r3=0; x=2; y=2;
470 :>3:r1=2; 3:r3=1; x=2; y=2;
375 :>3:r1=1; 3:r3=1; x=2; y=2;
62607 :>3:r1=0; 3:r3=1; x=2; y=2;
80508 :>3:r1=2; 3:r3=0; x=1; y=2;
93964 :>3:r1=2; 3:r3=0; x=2; y=1;
1176622:>3:r1=0; 3:r3=0; x=2; y=1;
141752:>3:r1=1; 3:r3=0; x=1; y=1;
234323:>3:r1=1; 3:r3=1; x=2; y=1;
6049234:>3:r1=2; 3:r3=0; x=1; y=1;
300634:>3:r1=1; 3:r3=0; x=1; y=2;
5908104:>3:r1=0; 3:r3=1; x=2; y=1;
3514486:>3:r1=2; 3:r3=1; x=1; y=2;
2225218:>3:r1=0; 3:r3=0; x=1; y=2;
3617620:>3:r1=0; 3:r3=1; x=1; y=1;
9711019:>3:r1=2; 3:r3=1; x=2; y=1;
2938601:>3:r1=0; 3:r3=1; x=1; y=2;
6404729:>3:r1=1; 3:r3=1; x=1; y=1;
18701068:>3:r1=0; 3:r3=0; x=1; y=1;
15704453:>3:r1=2; 3:r3=1; x=1; y=1;
3134004:>3:r1=1; 3:r3=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 205.43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3788 :>3:r1=0; 3:r3=0; x=2; y=2;
1764 :>3:r1=2; 3:r3=1; x=2; y=2;
1462 :>3:r1=1; 3:r3=1; x=2; y=2;
92734 :>3:r1=2; 3:r3=0; x=1; y=2;
127240:>3:r1=1; 3:r3=0; x=1; y=1;
328435:>3:r1=1; 3:r3=0; x=1; y=2;
171141:>3:r1=2; 3:r3=0; x=2; y=1;
589506:>3:r1=1; 3:r3=1; x=2; y=1;
3755859:>3:r1=2; 3:r3=1; x=1; y=2;
3909840:>3:r1=2; 3:r3=0; x=1; y=1;
187606:>3:r1=0; 3:r3=1; x=2; y=2;
3752313:>3:r1=1; 3:r3=1; x=1; y=2;
5463476:>3:r1=1; 3:r3=1; x=1; y=1;
2596786:>3:r1=0; 3:r3=1; x=1; y=2;
2409529:>3:r1=0; 3:r3=0; x=1; y=2;
16690665:>3:r1=0; 3:r3=0; x=1; y=1;
13342519:>3:r1=2; 3:r3=1; x=1; y=1;
1983320:>3:r1=0; 3:r3=1; x=1; y=1;
3037081:>3:r1=0; 3:r3=0; x=2; y=1;
14760832:>3:r1=2; 3:r3=1; x=2; y=1;
6794104:>3:r1=0; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 206.59
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
9133925:>2:r1=2; 2:r3=0; x=1;
146946:>2:r1=0; 2:r3=0; x=2;
8723686:>2:r1=1; 2:r3=1; x=1;
1440738:>2:r1=2; 2:r3=1; x=2;
5419785:>2:r1=0; 2:r3=1; x=2;
25710788:>2:r1=0; 2:r3=0; x=1;
21306836:>2:r1=2; 2:r3=1; x=1;
1460442:>2:r1=1; 2:r3=1; x=2;
6656854:>2:r1=0; 2:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 121.65
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
773 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
876 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
651 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
206977:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
206743:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
349759:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
70636 :>0:r3=1; 3:r1=2; 3:r3=0; y=2;
272853:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
194060:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
2135598:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
2801186:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
7278401:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
2502667:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
3259894:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
11113106:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
8463658:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
2359372:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
11714264:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
18125952:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
6358724:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
2583850:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 173.27
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
226 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
576 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
5369 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
4686 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
2950 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
13800 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
3120 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
200285:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
52465 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
194152:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
62176 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
799957:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
4788 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
773891:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
14896 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1057266:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
1747138:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
653047:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
5011276:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
3362060:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
1084972:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
997322:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
5220408:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
98449 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
3264794:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
220063:>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
2667139:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
11706259:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
1408943:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
4838293:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
3188411:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
4355185:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
4441232:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
8661479:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
5851634:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
7091885:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
887217:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
52191 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 232.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
592 :>3:r1=0; 3:r3=0; x=2; y=2;
33276 :>3:r1=2; 3:r3=0; x=2; y=1;
12425 :>3:r1=1; 3:r3=1; x=2; y=2;
237971:>3:r1=1; 3:r3=0; x=1; y=1;
12145 :>3:r1=2; 3:r3=1; x=2; y=2;
414363:>3:r1=2; 3:r3=0; x=1; y=2;
153670:>3:r1=0; 3:r3=1; x=2; y=2;
6129577:>3:r1=2; 3:r3=0; x=1; y=1;
1413910:>3:r1=1; 3:r3=0; x=1; y=2;
2851477:>3:r1=0; 3:r3=0; x=1; y=2;
980849:>3:r1=0; 3:r3=0; x=2; y=1;
5992443:>3:r1=1; 3:r3=1; x=1; y=2;
6097267:>3:r1=0; 3:r3=1; x=2; y=1;
7423426:>3:r1=2; 3:r3=1; x=1; y=2;
2572686:>3:r1=0; 3:r3=1; x=1; y=1;
8493494:>3:r1=2; 3:r3=1; x=2; y=1;
12822386:>3:r1=2; 3:r3=1; x=1; y=1;
1898589:>3:r1=0; 3:r3=1; x=1; y=2;
5404222:>3:r1=1; 3:r3=1; x=1; y=1;
16467072:>3:r1=0; 3:r3=0; x=1; y=1;
588160:>3:r1=1; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 206.29
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
12818 :>3:r1=0; 3:r3=0; x=2; y=2;
145548:>3:r1=1; 3:r3=0; x=1; y=1;
17827 :>3:r1=1; 3:r3=1; x=2; y=2;
95027 :>3:r1=2; 3:r3=0; x=2; y=1;
283704:>3:r1=2; 3:r3=0; x=1; y=2;
3952632:>3:r1=2; 3:r3=0; x=1; y=1;
984371:>3:r1=1; 3:r3=0; x=1; y=2;
522448:>3:r1=0; 3:r3=1; x=2; y=2;
20654 :>3:r1=2; 3:r3=1; x=2; y=2;
1196869:>3:r1=1; 3:r3=1; x=2; y=1;
8061430:>3:r1=2; 3:r3=1; x=1; y=2;
6419666:>3:r1=0; 3:r3=1; x=2; y=1;
1594884:>3:r1=0; 3:r3=1; x=1; y=1;
6330827:>3:r1=1; 3:r3=1; x=1; y=2;
1400200:>3:r1=0; 3:r3=1; x=1; y=2;
2737640:>3:r1=0; 3:r3=0; x=1; y=2;
14283639:>3:r1=0; 3:r3=0; x=1; y=1;
11726098:>3:r1=2; 3:r3=1; x=1; y=1;
4735563:>3:r1=1; 3:r3=1; x=1; y=1;
2943151:>3:r1=0; 3:r3=0; x=2; y=1;
12535004:>3:r1=2; 3:r3=1; x=2; y=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 196.51
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5529900:>2:r1=2; 2:r3=0; x=1;
7083269:>2:r1=1; 2:r3=1; x=1;
934749:>2:r1=0; 2:r3=0; x=2;
1984297:>2:r1=0; 2:r3=1; x=2;
8438911:>2:r1=1; 2:r3=1; x=2;
24807479:>2:r1=0; 2:r3=0; x=1;
20351442:>2:r1=2; 2:r3=1; x=1;
8771063:>2:r1=2; 2:r3=1; x=2;
2098890:>2:r1=0; 2:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 119.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
83283 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
377739:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
376584:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
133904:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
4782 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
77906 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
1297081:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
5782805:>0:r3=1; 3:r1=2; 3:r3=1; y=2;
477413:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
2444507:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
645917:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
2091624:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
6843767:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
1718669:>0:r3=1; 3:r1=0; 3:r3=1; y=1;
4725793:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
8729903:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
10321258:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
5615269:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
16953681:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
9465495:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
1832620:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 168.11
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
200 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
909 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
18437 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2;
100833:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
217751:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
15934 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
79719 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
16471 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
247608:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
825831:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
918959:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
283676:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
242954:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
2612260:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
823106:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
2282011:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
97602 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
473880:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
9691 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
3785918:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
5605078:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
55904 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
7453425:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
394932:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
601298:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
230486:>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
5590989:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
5869131:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
4260323:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
3879471:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
7910558:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
10044206:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
4093257:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
1558875:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1889965:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
1071608:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
3369717:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
3067024:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 233.55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
251284:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
693324:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
260068:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
238478:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
1479152:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
7864419:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
8676313:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
469805:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
5764258:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
8242554:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
25992466:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1;
6539948:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
4479649:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
7653966:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
1394316:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 117.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
452 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
8037 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
26800 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
177462:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
887627:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
725730:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
5083142:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
9867026:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
5769515:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
2412637:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
4497774:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
8395762:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
7785007:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
16395856:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
17967173:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 137.28
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
22 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
1147 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
12661 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
3494 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
168 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
139701:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
12896 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
126683:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
238444:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
427087:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
590908:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1502214:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1806079:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
458662:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
3372070:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
3425779:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1911440:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
3865616:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
718382:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
610467:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
65527 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
5581787:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
4875708:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
6211314:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1873653:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
9050015:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
6873165:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
3414962:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
294436:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
3970074:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
13011346:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
5511373:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
42720 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 195.52
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
14391 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
9804 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
365312:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
59463 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
539812:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
3953687:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
1621361:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
9099634:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
6186357:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
7610894:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
14805161:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
3811007:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
17402474:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
2340142:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
12180501:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 136.04
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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;
105 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
14 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
54 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
3913 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
25261 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
200658:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
123598:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
4173 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
269481:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
280651:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
758644:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
616023:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
280981:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
874639:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
637874:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
419071:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
22286 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
7279095:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
310033:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
76226 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1946737:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
172069:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
8287673:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1435761:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
6778968:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
2704965:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
6353259:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
8031322:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
3624689:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
61114 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
21399063:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
7021599:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 201.46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
404 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
4858 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
293271:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
272345:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
2235690:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
3167742:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
6307769:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
4084259:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
7344765:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
6179541:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
2195894:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
11558177:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
18255787:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
17984505:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
114993:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 162.37
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
7329 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
12115 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
399336:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
254147:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
4690635:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
278457:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
3059297:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
6369356:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
4056620:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
15363135:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
5837049:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
1172204:>1:r3=1; 3:r1=0; 3:r3=1; x=1;
15732521:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
4990171:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
17777628:>1:r3=1; 3:r1=1; 3:r3=1; x=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 160.64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
195341:>0:r3=0; 2:r1=0; 2:r3=0;
5135841:>0:r3=0; 2:r1=1; 2:r3=1;
12315558:>0:r3=1; 2:r1=1; 2:r3=0;
7565810:>0:r3=0; 2:r1=0; 2:r3=1;
25714965:>0:r3=1; 2:r1=0; 2:r3=0;
5294489:>0:r3=1; 2:r1=0; 2:r3=1;
23777996:>0:r3=1; 2:r1=1; 2:r3=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 97.34
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
885 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
14301 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
200618:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
221780:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
2242252:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
6710147:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
7005043:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
4019082:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
18488666:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1;
17828463:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
310654:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
2076296:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
2105309:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
12702452:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
6074052:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 134.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
412 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
11542 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
20689 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
7729 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1131465:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
324559:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
162462:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
2329 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1067495:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
413296:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
139033:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
116664:>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1549150:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
2068443:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
3343257:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
32682 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
316789:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
5000325:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
1310842:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
612914:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
2068944:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
3822276:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
4365656:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
7654658:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
9705607:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
12355678:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
7044763:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
5713122:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
5491510:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
4145705:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
No
Witnesses
Positive: 0, Negative: 80000000
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 204.90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
47 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
62 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
104 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
829 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
194 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
711 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
4867 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
120 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
20305 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
24701 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
349925:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
68250 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
76751 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
34076 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
24665 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
161481:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
1265346:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
2335089:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
2442082:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
615416:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
816263:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
3388643:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
561270:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
770389:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
728943:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
1988995:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
4211306:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
7357848:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
575454:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
166223:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
2516499:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
843107:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
3713172:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
1832629:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
1467951:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
1120100:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
11060050:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
7791787:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
6990141:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
3948740:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
4446763:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
3499490:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
1043093:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
1736121:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
No
Witnesses
Positive: 0, Negative: 80000000
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 230.16
$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 80
Fri Jan 1 17:49:35 CET 2010