Tue Jan 5 17:58:00 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)
2141279:>3:r1=0; 3:r3=0; x=1; y=1;
102498:>3:r1=1; 3:r3=0; x=1; y=1;
1262998:>3:r1=2; 3:r3=0; x=1; y=1;
37959 :>3:r1=0; 3:r3=1; x=1; y=1;
1238096:>3:r1=1; 3:r3=1; x=1; y=1;
1094809:>3:r1=2; 3:r3=1; x=1; y=1;
1981367:>3:r1=0; 3:r3=0; x=2; y=1;
234993:>3:r1=2; 3:r3=0; x=2; y=1;
1991971:>3:r1=0; 3:r3=1; x=2; y=1;
350027:>3:r1=1; 3:r3=1; x=2; y=1;
3794136:>3:r1=2; 3:r3=1; x=2; y=1;
2186234:>3:r1=0; 3:r3=0; x=1; y=2;
245050:>3:r1=1; 3:r3=0; x=1; y=2;
189036:>3:r1=2; 3:r3=0; x=1; y=2;
400444:>3:r1=0; 3:r3=1; x=1; y=2;
901402:>3:r1=1; 3:r3=1; x=1; y=2;
1557862:>3:r1=2; 3:r3=1; x=1; y=2;
5827 :>3:r1=0; 3:r3=0; x=2; y=2;
277298:>3:r1=0; 3:r3=1; x=2; y=2;
2197 :>3:r1=1; 3:r3=1; x=2; y=2;
4517 :>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 27.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1742719:>3:r1=0; 3:r3=0; x=1; y=1;
105564:>3:r1=1; 3:r3=0; x=1; y=1;
1027976:>3:r1=2; 3:r3=0; x=1; y=1;
27335 :>3:r1=0; 3:r3=1; x=1; y=1;
1113016:>3:r1=1; 3:r3=1; x=1; y=1;
657215:>3:r1=2; 3:r3=1; x=1; y=1;
2404276:>3:r1=0; 3:r3=0; x=2; y=1;
461694:>3:r1=2; 3:r3=0; x=2; y=1;
2404703:>3:r1=0; 3:r3=1; x=2; y=1;
380872:>3:r1=1; 3:r3=1; x=2; y=1;
4284310:>3:r1=2; 3:r3=1; x=2; y=1;
2286527:>3:r1=0; 3:r3=0; x=1; y=2;
314826:>3:r1=1; 3:r3=0; x=1; y=2;
244643:>3:r1=2; 3:r3=0; x=1; y=2;
188092:>3:r1=0; 3:r3=1; x=1; y=2;
730229:>3:r1=1; 3:r3=1; x=1; y=2;
1352195:>3:r1=2; 3:r3=1; x=1; y=2;
7383 :>3:r1=0; 3:r3=0; x=2; y=2;
254204:>3:r1=0; 3:r3=1; x=2; y=2;
3052 :>3:r1=1; 3:r3=1; x=2; y=2;
9169 :>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 26.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
5451758:>2:r1=0; 2:r3=0; x=1;
1968821:>2:r1=2; 2:r3=0; x=1;
325724:>2:r1=0; 2:r3=1; x=1;
3205322:>2:r1=1; 2:r3=1; x=1;
3474303:>2:r1=2; 2:r3=1; x=1;
1213303:>2:r1=0; 2:r3=0; x=2;
1316277:>2:r1=0; 2:r3=1; x=2;
1084336:>2:r1=1; 2:r3=1; x=2;
1960156:>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 18.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2281142:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
2051750:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
263207:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
384731:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
1528143:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
1693370:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
38204 :>0:r3=1; 3:r1=0; 3:r3=1; y=1;
632784:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
1366962:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
3682369:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
763029:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
10764 :>0:r3=0; 3:r1=0; 3:r3=0; y=2;
2115407:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
223695:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
296866:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
661412:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
236347:>0:r3=1; 3:r1=0; 3:r3=1; y=2;
4164 :>0:r3=0; 3:r1=1; 3:r3=1; y=2;
504566:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
3516 :>0:r3=0; 3:r1=2; 3:r3=1; y=2;
1257572:>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 26.38
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (39 states)
1685811:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
434634:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
26766 :>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
1040410:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
770955:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
31435 :>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
51484 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
483526:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
511487:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
227033:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
827251:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1723108:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
1210547:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
144722:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
92333 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
2290797:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
481338:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
393358:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
237709:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
1556044:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
88 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1427696:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
1703 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
479741:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
1977 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
510134:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
10680 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
2654983:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
289005:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
7129 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
1706 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
12643 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
1 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
374596:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
1580 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
1850 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
242 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
3319 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
179 :>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 25.60
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1735058:>3:r1=0; 3:r3=0; x=1; y=1;
115075:>3:r1=1; 3:r3=0; x=1; y=1;
1350249:>3:r1=2; 3:r3=0; x=1; y=1;
17119 :>3:r1=0; 3:r3=1; x=1; y=1;
1087342:>3:r1=1; 3:r3=1; x=1; y=1;
812478:>3:r1=2; 3:r3=1; x=1; y=1;
1841015:>3:r1=0; 3:r3=0; x=2; y=1;
148991:>3:r1=2; 3:r3=0; x=2; y=1;
1753157:>3:r1=0; 3:r3=1; x=2; y=1;
621836:>3:r1=1; 3:r3=1; x=2; y=1;
3402451:>3:r1=2; 3:r3=1; x=2; y=1;
2027268:>3:r1=0; 3:r3=0; x=1; y=2;
716955:>3:r1=1; 3:r3=0; x=1; y=2;
408247:>3:r1=2; 3:r3=0; x=1; y=2;
180246:>3:r1=0; 3:r3=1; x=1; y=2;
1271430:>3:r1=1; 3:r3=1; x=1; y=2;
1950123:>3:r1=2; 3:r3=1; x=1; y=2;
33179 :>3:r1=0; 3:r3=0; x=2; y=2;
476033:>3:r1=0; 3:r3=1; x=2; y=2;
22346 :>3:r1=1; 3:r3=1; x=2; y=2;
29402 :>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 26.69
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1455062:>3:r1=0; 3:r3=0; x=1; y=1;
121731:>3:r1=1; 3:r3=0; x=1; y=1;
1150209:>3:r1=2; 3:r3=0; x=1; y=1;
12578 :>3:r1=0; 3:r3=1; x=1; y=1;
936096:>3:r1=1; 3:r3=1; x=1; y=1;
536515:>3:r1=2; 3:r3=1; x=1; y=1;
2150005:>3:r1=0; 3:r3=0; x=2; y=1;
318689:>3:r1=2; 3:r3=0; x=2; y=1;
2078593:>3:r1=0; 3:r3=1; x=2; y=1;
752044:>3:r1=1; 3:r3=1; x=2; y=1;
3701923:>3:r1=2; 3:r3=1; x=2; y=1;
1906488:>3:r1=0; 3:r3=0; x=1; y=2;
800086:>3:r1=1; 3:r3=0; x=1; y=2;
436658:>3:r1=2; 3:r3=0; x=1; y=2;
105576:>3:r1=0; 3:r3=1; x=1; y=2;
1096822:>3:r1=1; 3:r3=1; x=1; y=2;
1771707:>3:r1=2; 3:r3=1; x=1; y=2;
114327:>3:r1=0; 3:r3=0; x=2; y=2;
479551:>3:r1=0; 3:r3=1; x=2; y=2;
26695 :>3:r1=1; 3:r3=1; x=2; y=2;
48645 :>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 26.35
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4465783:>2:r1=0; 2:r3=0; x=1;
1742807:>2:r1=2; 2:r3=0; x=1;
24772 :>2:r1=0; 2:r3=1; x=1;
2446150:>2:r1=1; 2:r3=1; x=1;
2477451:>2:r1=2; 2:r3=1; x=1;
2206622:>2:r1=0; 2:r3=0; x=2;
321306:>2:r1=0; 2:r3=1; x=2;
2365745:>2:r1=1; 2:r3=1; x=2;
3949364:>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 17.75
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1748419:>0:r3=0; 3:r1=0; 3:r3=0; y=1;
1413241:>0:r3=1; 3:r1=0; 3:r3=0; y=1;
274118:>0:r3=1; 3:r1=1; 3:r3=0; y=1;
367602:>0:r3=0; 3:r1=2; 3:r3=0; y=1;
1312246:>0:r3=1; 3:r1=2; 3:r3=0; y=1;
1071307:>0:r3=0; 3:r1=0; 3:r3=1; y=1;
9864 :>0:r3=1; 3:r1=0; 3:r3=1; y=1;
1198480:>0:r3=0; 3:r1=1; 3:r3=1; y=1;
1175812:>0:r3=1; 3:r1=1; 3:r3=1; y=1;
2460947:>0:r3=0; 3:r1=2; 3:r3=1; y=1;
499419:>0:r3=1; 3:r1=2; 3:r3=1; y=1;
362700:>0:r3=0; 3:r1=0; 3:r3=0; y=2;
1742759:>0:r3=1; 3:r1=0; 3:r3=0; y=2;
1234791:>0:r3=1; 3:r1=1; 3:r3=0; y=2;
627342:>0:r3=1; 3:r1=2; 3:r3=0; y=2;
1257524:>0:r3=0; 3:r1=0; 3:r3=1; y=2;
68093 :>0:r3=1; 3:r1=0; 3:r3=1; y=2;
113254:>0:r3=0; 3:r1=1; 3:r3=1; y=2;
970699:>0:r3=1; 3:r1=1; 3:r3=1; y=2;
354083:>0:r3=0; 3:r1=2; 3:r3=1; y=2;
1737300:>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 26.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (39 states)
1292671:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1;
555455:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1;
19393 :>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1;
859309:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1;
615595:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1;
25785 :>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1;
59618 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1;
557971:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1;
1051532:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1;
158767:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1;
1194302:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1;
1996556:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1;
611413:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1;
588426:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1;
234189:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1;
2132184:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2;
438296:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2;
254758:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2;
154826:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2;
1438042:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2;
73 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2;
1158252:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2;
1875 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2;
284832:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2;
2568 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2;
902602:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2;
43723 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2;
2193386:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2;
312854:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2;
49905 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2;
21638 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2;
76903 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2;
59 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2;
590100:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2;
3189 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2;
44262 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2;
1332 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2;
72004 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2;
1355 :>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 25.50
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2695206:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0;
672055:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0;
971174:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0;
2026249:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0;
485350:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0;
1104440:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0;
320261:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0;
1246986:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1;
1102126:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1;
3072 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1;
1493259:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1;
1901601:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1;
305235:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1;
1526478:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1;
4146508:>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 18.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 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)
4254237:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
30863 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
2194816:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
333968:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
625119:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1934948:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
44922 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1855470:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
908422:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
25935 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1080781:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
1966275:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
158848:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
2618442:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
1966954:>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 21.44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2795708:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
206496:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
172082:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1443276:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
582565:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1246587:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
639716:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
1332474:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
206506:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
122030:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
351855:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
82 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
2118 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
706 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
49 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
7115 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
309970:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
9 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
615124:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
3156 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
263326:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
576705:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
16799 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1021381:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
723 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
7319 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1246772:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1670388:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
6882 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
361542:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1246153:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
423914:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
3120472:>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 24.24
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
4209984:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0;
50504 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0;
1724312:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0;
829176:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0;
634492:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0;
1649981:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0;
120398:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0;
1028734:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1;
1295907:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1;
17889 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1;
1232342:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1;
1569755:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1;
405529:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1;
2168086:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1;
3062911:>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 21.08
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
2574665:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
3159 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
537550:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
1219497:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
3826 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
1939353:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
584824:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2;
1253408:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
3613 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
327974:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
8867 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
2 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
77 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
34 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
403 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
40388 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2;
42455 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
6 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
21011 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1200103:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
5397 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
1039687:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
4402 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
3648 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1477294:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
1893765:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1773 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
353634:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
1679898:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
25760 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
3753525:>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 23.70
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3189376:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
2235693:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
790623:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
1836345:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
761518:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
3985 :>1:r3=1; 3:r1=0; 3:r3=1; x=1;
1740903:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
1546180:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
8269 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
1643721:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
346009:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
483182:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
1744754:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
12781 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
3656661:>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 26.49
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
3138011:>1:r3=0; 3:r1=0; 3:r3=0; x=1;
1742457:>1:r3=1; 3:r1=0; 3:r3=0; x=1;
753698:>1:r3=0; 3:r1=1; 3:r3=0; x=1;
1574400:>1:r3=1; 3:r1=1; 3:r3=0; x=1;
533347:>1:r3=0; 3:r1=0; 3:r3=1; x=1;
1665 :>1:r3=1; 3:r1=0; 3:r3=1; x=1;
1574598:>1:r3=0; 3:r1=1; 3:r3=1; x=1;
962394:>1:r3=1; 3:r1=1; 3:r3=1; x=1;
50330 :>1:r3=0; 3:r1=0; 3:r3=0; x=2;
2192677:>1:r3=1; 3:r1=0; 3:r3=0; x=2;
475898:>1:r3=1; 3:r1=1; 3:r3=0; x=2;
462130:>1:r3=0; 3:r1=0; 3:r3=1; x=2;
2226628:>1:r3=1; 3:r1=0; 3:r3=1; x=2;
24539 :>1:r3=0; 3:r1=1; 3:r3=1; x=2;
4287228:>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 26.23
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
1339808:>0:r3=0; 2:r1=0; 2:r3=0;
5324926:>0:r3=1; 2:r1=0; 2:r3=0;
2926970:>0:r3=1; 2:r1=1; 2:r3=0;
2545115:>0:r3=0; 2:r1=0; 2:r3=1;
2960 :>0:r3=1; 2:r1=0; 2:r3=1;
4118572:>0:r3=0; 2:r1=1; 2:r3=1;
3741649:>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 15.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
482909:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0;
2651793:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0;
1888726:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0;
1795298:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0;
628324:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0;
483179:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0;
1721903:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0;
1165451:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1;
908917:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1;
1260807:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1;
1174 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1;
302986:>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1;
1639251:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1;
3973807:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1;
1095475:>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 21.77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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)
814537:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1;
1557657:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1;
592697:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1;
757433:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1;
1167 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1;
2409328:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1;
1120561:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1;
1443763:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1;
3152 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1;
366661:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1;
624490:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1;
33308 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
14488 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2;
2105445:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
471879:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2;
432980:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
298864:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2;
63231 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
139 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2;
1459236:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
69 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2;
1835695:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
1784 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2;
613741:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
3243 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2;
187118:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
610 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2;
20464 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
201 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2;
2504652:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2;
261407:>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 25.56
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 (45 states)
474901:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
1939319:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
822397:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1;
358445:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1;
1374723:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
407305:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1;
1019526:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
2992 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
4401 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1;
884809:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
1090929:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
190662:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1;
1076505:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
422865:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
1142351:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1;
226331:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
361664:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
767126:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2;
110165:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
18 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
311061:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2;
221500:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
1153748:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2;
20 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
187 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2;
690705:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2;
5083 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2;
464741:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
2499 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
2962 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2;
205707:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
3 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
689 :>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2;
695549:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
718159:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
235007:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2;
36 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
72 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
124 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2;
395350:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
208483:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
1742940:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2;
249453:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
90 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2;
18398 :>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 24.88
$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=-s 1000 -r 20000
Tue Jan 5 18:06:16 CET 2010