Thu Dec 24 23:06:11 CET 2009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr000.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr000 "Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr000 Allowed Histogram (21 states) 113 :>3:r1=1; 3:r3=1; x=2; y=2; 145 :>3:r1=2; 3:r3=1; x=2; y=2; 91 :>3:r1=0; 3:r3=0; x=2; y=2; 50940 :>3:r1=1; 3:r3=0; x=1; y=1; 11642 :>3:r1=2; 3:r3=0; x=2; y=1; 18870 :>3:r1=2; 3:r3=0; x=1; y=2; 13880 :>3:r1=0; 3:r3=1; x=2; y=2; 1407703:>3:r1=2; 3:r3=0; x=1; y=1; 45542 :>3:r1=1; 3:r3=0; x=1; y=2; 56824 :>3:r1=1; 3:r3=1; x=2; y=1; 327145:>3:r1=0; 3:r3=0; x=2; y=1; 839093:>3:r1=1; 3:r3=1; x=1; y=2; 1228624:>3:r1=0; 3:r3=1; x=2; y=1; 377420:>3:r1=0; 3:r3=0; x=1; y=2; 755281:>3:r1=0; 3:r3=1; x=1; y=1; 4159111:>3:r1=2; 3:r3=1; x=1; y=1; 2754029:>3:r1=2; 3:r3=1; x=2; y=1; 643560:>3:r1=0; 3:r3=1; x=1; y=2; 4720626:>3:r1=0; 3:r3=0; x=1; y=1; 1668428:>3:r1=1; 3:r3=1; x=1; y=1; 920933:>3:r1=2; 3:r3=1; x=1; y=2; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=7074ebf0a4e494a7c168353216394741 Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr000 No ACLwSyncdRR Safe=Fre Wse SyncdWW Time aclwdrr000 44.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr001.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr001 "Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | sync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr001 Allowed Histogram (21 states) 1089 :>3:r1=2; 3:r3=1; x=2; y=2; 836 :>3:r1=1; 3:r3=1; x=2; y=2; 1663 :>3:r1=0; 3:r3=0; x=2; y=2; 11933 :>3:r1=2; 3:r3=0; x=1; y=2; 18885 :>3:r1=1; 3:r3=0; x=1; y=1; 55573 :>3:r1=0; 3:r3=1; x=2; y=2; 66091 :>3:r1=1; 3:r3=0; x=1; y=2; 46376 :>3:r1=2; 3:r3=0; x=2; y=1; 805731:>3:r1=2; 3:r3=0; x=1; y=1; 1254733:>3:r1=0; 3:r3=0; x=2; y=1; 617148:>3:r1=0; 3:r3=1; x=1; y=2; 1101557:>3:r1=2; 3:r3=1; x=1; y=2; 1375670:>3:r1=1; 3:r3=1; x=1; y=1; 3944113:>3:r1=2; 3:r3=1; x=2; y=1; 503275:>3:r1=0; 3:r3=0; x=1; y=2; 3206777:>3:r1=2; 3:r3=1; x=1; y=1; 1619414:>3:r1=0; 3:r3=1; x=2; y=1; 476226:>3:r1=0; 3:r3=1; x=1; y=1; 3743701:>3:r1=0; 3:r3=0; x=1; y=1; 176889:>3:r1=1; 3:r3=1; x=2; y=1; 972320:>3:r1=1; 3:r3=1; x=1; y=2; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=42a8ec6eccd807ced6dea1376fc81b0b Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr001 No ACLwSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time aclwdrr001 40.27 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr002.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr002 "Fre SyncdWW Wse Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | | lwz r3,0(r4) ; li r3,1 | | ; stw r3,0(r4) | | ; exists (x=2 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r9,2 _litmus_P1_1_: stw r9,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr002 Allowed Histogram (9 states) 10416 :>2:r1=0; 2:r3=0; x=2; 2174854:>2:r1=2; 2:r3=0; x=1; 335804:>2:r1=2; 2:r3=1; x=2; 1425234:>2:r1=0; 2:r3=1; x=2; 391120:>2:r1=1; 2:r3=1; x=2; 5355990:>2:r1=2; 2:r3=1; x=1; 6491192:>2:r1=0; 2:r3=0; x=1; 1928110:>2:r1=1; 2:r3=1; x=1; 1887280:>2:r1=0; 2:r3=1; x=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=e86498b53008de1e6a240afbf078cd14 Cycle=Fre SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr002 No ACLwSyncdRR Safe=Fre Wse SyncdWW Time aclwdrr002 26.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr003.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr003 "Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r8,0(r2) _litmus_P1_0_: li r11,1 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr003 Allowed Histogram (21 states) 169 :>0:r3=0; 3:r1=0; 3:r3=0; y=2; 514 :>0:r3=0; 3:r1=1; 3:r3=1; y=2; 389 :>0:r3=0; 3:r1=2; 3:r3=1; y=2; 10135 :>0:r3=1; 3:r1=2; 3:r3=0; y=2; 44410 :>0:r3=1; 3:r1=1; 3:r3=0; y=1; 66294 :>0:r3=0; 3:r1=1; 3:r3=1; y=1; 55255 :>0:r3=0; 3:r1=2; 3:r3=0; y=1; 41891 :>0:r3=0; 3:r1=0; 3:r3=1; y=2; 26901 :>0:r3=1; 3:r1=1; 3:r3=0; y=2; 453262:>0:r3=1; 3:r1=0; 3:r3=0; y=2; 641032:>0:r3=1; 3:r1=2; 3:r3=1; y=2; 575236:>0:r3=1; 3:r1=1; 3:r3=1; y=2; 596983:>0:r3=0; 3:r1=0; 3:r3=0; y=1; 1641422:>0:r3=0; 3:r1=0; 3:r3=1; y=1; 665760:>0:r3=1; 3:r1=0; 3:r3=1; y=2; 1972889:>0:r3=1; 3:r1=2; 3:r3=0; y=1; 2923778:>0:r3=0; 3:r1=2; 3:r3=1; y=1; 3277705:>0:r3=1; 3:r1=2; 3:r3=1; y=1; 4622519:>0:r3=1; 3:r1=0; 3:r3=0; y=1; 1710173:>0:r3=1; 3:r1=1; 3:r3=1; y=1; 673283:>0:r3=1; 3:r1=0; 3:r3=1; y=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=9599d8c79b2e28a1f015a74966a65bac Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr003 No ACLwSyncdRR Safe=Fre Wse SyncdWW SyncdWR Time aclwdrr003 40.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr004.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr004 "Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r2) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r9,1 _litmus_P0_1_: stw r9,0(r2) _litmus_P0_2_: sync _litmus_P0_3_: lwz r10,0(r2) _litmus_P1_0_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr004 Allowed Histogram (38 states) 224 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 310 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2; 281 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 1738 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 1068 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 271 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 773 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 38 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 43306 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1; 16864 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 54124 :>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2; 22429 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 10353 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2; 389481:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 66160 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1; 504419:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 53382 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1; 281025:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 2232 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 120295:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 847888:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2; 1715988:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 78830 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 40838 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 251015:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 1306866:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 2007897:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 342213:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 791156:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 623976:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 2063772:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 1607444:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 1016176:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 2791379:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 847812:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 918778:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; 429060:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 750139:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=32cc2d7800b6941b57852b520691800f Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr004 No ACLwSyncdRR Safe=Fre Wse SyncsWR SyncdWW Time aclwdrr004 50.12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr005.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr005 "Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr005 Allowed Histogram (21 states) 104 :>3:r1=0; 3:r3=0; x=2; y=2; 2310 :>3:r1=1; 3:r3=1; x=2; y=2; 2322 :>3:r1=2; 3:r3=1; x=2; y=2; 77667 :>3:r1=2; 3:r3=0; x=1; y=2; 3955 :>3:r1=2; 3:r3=0; x=2; y=1; 39915 :>3:r1=1; 3:r3=0; x=1; y=1; 40312 :>3:r1=0; 3:r3=1; x=2; y=2; 302488:>3:r1=1; 3:r3=0; x=1; y=2; 1008627:>3:r1=2; 3:r3=0; x=1; y=1; 258084:>3:r1=0; 3:r3=0; x=2; y=1; 773342:>3:r1=0; 3:r3=0; x=1; y=2; 1985881:>3:r1=2; 3:r3=1; x=1; y=2; 697834:>3:r1=0; 3:r3=1; x=1; y=1; 1518912:>3:r1=1; 3:r3=1; x=1; y=2; 1177344:>3:r1=0; 3:r3=1; x=2; y=1; 594194:>3:r1=0; 3:r3=1; x=1; y=2; 3716157:>3:r1=2; 3:r3=1; x=1; y=1; 1405329:>3:r1=1; 3:r3=1; x=1; y=1; 4092974:>3:r1=0; 3:r3=0; x=1; y=1; 165550:>3:r1=1; 3:r3=1; x=2; y=1; 2136699:>3:r1=2; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=4867d1504e0b1c594b9643e48c015b80 Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr005 No ACLwSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time aclwdrr005 40.74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr006.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr006 "Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | lwsync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr006 Allowed Histogram (21 states) 34023 :>3:r1=1; 3:r3=0; x=1; y=1; 4276 :>3:r1=0; 3:r3=0; x=2; y=2; 18042 :>3:r1=2; 3:r3=0; x=2; y=1; 191112:>3:r1=1; 3:r3=0; x=1; y=2; 972315:>3:r1=2; 3:r3=0; x=1; y=1; 6677 :>3:r1=1; 3:r3=1; x=2; y=2; 7920 :>3:r1=2; 3:r3=1; x=2; y=2; 540721:>3:r1=0; 3:r3=0; x=1; y=2; 53966 :>3:r1=2; 3:r3=0; x=1; y=2; 336624:>3:r1=1; 3:r3=1; x=2; y=1; 1892080:>3:r1=2; 3:r3=1; x=1; y=2; 893342:>3:r1=0; 3:r3=0; x=2; y=1; 352544:>3:r1=0; 3:r3=1; x=1; y=1; 1571812:>3:r1=0; 3:r3=1; x=2; y=1; 383055:>3:r1=0; 3:r3=1; x=1; y=2; 2902117:>3:r1=2; 3:r3=1; x=1; y=1; 3138623:>3:r1=2; 3:r3=1; x=2; y=1; 1629478:>3:r1=1; 3:r3=1; x=1; y=2; 3621472:>3:r1=0; 3:r3=0; x=1; y=1; 1317376:>3:r1=1; 3:r3=1; x=1; y=1; 132425:>3:r1=0; 3:r3=1; x=2; y=2; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=7e01ecd8b2bc06ff5ba0d2b4e58340c6 Cycle=Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr006 No ACLwSyncdRR Safe=Fre Wse LwSyncdWW Time aclwdrr006 42.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr007.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr007 "Fre LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | | lwz r3,0(r4) ; li r3,1 | | ; stw r3,0(r4) | | ; exists (x=2 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r9,2 _litmus_P1_1_: stw r9,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr007 Allowed Histogram (9 states) 1489261:>2:r1=2; 2:r3=0; x=1; 166345:>2:r1=0; 2:r3=0; x=2; 530230:>2:r1=0; 2:r3=1; x=2; 2409795:>2:r1=1; 2:r3=1; x=2; 1947290:>2:r1=2; 2:r3=1; x=2; 4899335:>2:r1=2; 2:r3=1; x=1; 6312793:>2:r1=0; 2:r3=0; x=1; 1621073:>2:r1=1; 2:r3=1; x=1; 623878:>2:r1=0; 2:r3=1; x=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=ba17863040d25a62a648bb8030bf59fd Cycle=Fre LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr007 No ACLwSyncdRR Safe=Fre Wse LwSyncdWW Time aclwdrr007 25.86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr008.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr008 "Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r8,0(r2) _litmus_P1_0_: li r11,1 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr008 Allowed Histogram (21 states) 634 :>0:r3=0; 3:r1=0; 3:r3=0; y=2; 10469 :>0:r3=0; 3:r1=2; 3:r3=1; y=2; 8379 :>0:r3=0; 3:r1=1; 3:r3=1; y=2; 119822:>0:r3=1; 3:r1=1; 3:r3=0; y=1; 32025 :>0:r3=0; 3:r1=2; 3:r3=0; y=1; 138701:>0:r3=1; 3:r1=2; 3:r3=0; y=2; 368124:>0:r3=1; 3:r1=1; 3:r3=0; y=2; 119122:>0:r3=0; 3:r1=1; 3:r3=1; y=1; 606277:>0:r3=0; 3:r1=0; 3:r3=0; y=1; 478332:>0:r3=1; 3:r1=0; 3:r3=1; y=1; 1139807:>0:r3=1; 3:r1=1; 3:r3=1; y=2; 656226:>0:r3=1; 3:r1=0; 3:r3=0; y=2; 1356356:>0:r3=1; 3:r1=2; 3:r3=1; y=2; 440911:>0:r3=1; 3:r1=0; 3:r3=1; y=2; 2547016:>0:r3=0; 3:r1=2; 3:r3=1; y=1; 1534008:>0:r3=0; 3:r1=0; 3:r3=1; y=1; 2611805:>0:r3=1; 3:r1=2; 3:r3=0; y=1; 2228137:>0:r3=1; 3:r1=2; 3:r3=1; y=1; 4312292:>0:r3=1; 3:r1=0; 3:r3=0; y=1; 1223306:>0:r3=1; 3:r1=1; 3:r3=1; y=1; 68251 :>0:r3=0; 3:r1=0; 3:r3=1; y=2; No Witnesses Positive: 0, Negative: 20000000 Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=61bd93196401321b8fb91e15727e3c64 Cycle=Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr008 No ACLwSyncdRR Safe=Fre Wse SyncdWR LwSyncdWW Time aclwdrr008 41.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr009.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr009 "Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | | lwz r3,0(r4) ; lwz r3,0(r2) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r9,1 _litmus_P0_1_: stw r9,0(r2) _litmus_P0_2_: sync _litmus_P0_3_: lwz r10,0(r2) _litmus_P1_0_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr009 Allowed Histogram (39 states) 1 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 384 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2; 4304 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 92 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 3860 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 6359 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 5075 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 35349 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1; 17561 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 315075:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1; 228312:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1; 72850 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 95333 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 254509:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2; 90528 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 721714:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 152604:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 38373 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2; 1404505:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 802442:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 18485 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 1897990:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 95076 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 371349:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 1729611:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; 71456 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 261241:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 2496963:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 820261:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 114131:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 708992:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2; 353705:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 791780:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 1575288:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 883989:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 1482321:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 1266478:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 671894:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 139760:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=ab46080bf73ab92da49cdd6b27ede9b2 Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr009 No ACLwSyncdRR Safe=Fre Wse SyncsWR LwSyncdWW Time aclwdrr009 49.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr010.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr010 "Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; lwsync | stw r1,0(r2) | lwsync | stw r1,0(r2) ; lwz r3,0(r4) | | lwz r3,0(r4) | ; exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: lwz r7,0(r9) _litmus_P0_1_: lwsync _litmus_P0_2_: lwz r8,0(r2) _litmus_P1_0_: li r9,1 _litmus_P1_1_: stw r9,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) _litmus_P3_0_: li r9,1 _litmus_P3_1_: stw r9,0(r2) Test aclwdrr010 Allowed Histogram (15 states) 114730:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 91188 :>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 58425 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 64859 :>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 64706 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 1005368:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 382376:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 2143201:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 2222717:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 1434457:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 1586613:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 6500655:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; 2031868:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 1918381:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 380456:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=8ce05c9f86d49b2adfd5546bd471aa44 Cycle=Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr010 No ACLwSyncdRR Safe=Fre Time aclwdrr010 30.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr011.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr011 "Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; sync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,1 | | | ; stw r3,0(r4) | | | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr011 Allowed Histogram (15 states) 89 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 2558 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 250448:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 5928 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 53735 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 223398:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 2532289:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 1258815:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 1075796:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 993576:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 655335:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 1991915:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 4173271:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 2172214:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 4610633:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=064d7a96bedb614c156f5bd3adf783d8 Cycle=Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr011 No ACLwSyncdRR Safe=Fre SyncdWW Time aclwdrr011 35.74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr012.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr012 "Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; sync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,2 | | | ; stw r3,0(r2) | | | ; exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r9,1 _litmus_P0_1_: stw r9,0(r2) _litmus_P0_2_: sync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr012 Allowed Histogram (33 states) 6 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 31 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 4033 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 979 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 4569 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 10558 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 50489 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 352 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 64486 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 140178:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 642682:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 33081 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 128997:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 112711:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 1192727:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1126050:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 466267:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 129759:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 8909 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 836016:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 710933:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 378944:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1519632:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 871505:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 205024:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 961065:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 1383540:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1588211:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 57951 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 2244718:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 1563993:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 3132528:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 429076:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; No Witnesses Positive: 0, Negative: 20000000 Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=992754280de579a7f5feb516274ac846 Cycle=Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr012 No ACLwSyncdRR Safe=Fre SyncsWW Time aclwdrr012 42.63 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr013.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr013 "Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,1 | | | ; stw r3,0(r4) | | | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr013 Allowed Histogram (15 states) 6691 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 210159:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 4053 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 173796:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 11822 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 1457407:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 2369051:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 4116559:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 1732219:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3656436:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 1027977:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 358049:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 1235811:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 549068:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3090902:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=4eddb3c8ea9ccf8a71927b2e31094cad Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr013 No ACLwSyncdRR Safe=Fre LwSyncdWW Time aclwdrr013 33.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr014.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr014 "Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,2 | | | ; stw r3,0(r2) | | | ; exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r9,1 _litmus_P0_1_: stw r9,0(r2) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr014 Allowed Histogram (32 states) 2 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 9 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 21 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 876 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 6381 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 2237 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 53203 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 24829 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 77198 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 103321:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 6978 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 99062 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 18201 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 68207 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 56747 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 168003:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 429159:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 778920:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 14060 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 160988:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 363006:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 70029 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 1429719:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 144835:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 2338661:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 1144790:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 1262038:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 1324856:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 46008 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 2451170:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 5516590:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1839896:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; No Witnesses Positive: 0, Negative: 20000000 Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=0363e525d1d5c107b6654781a780ef6a Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr014 No ACLwSyncdRR Safe=Fre LwSyncsWW Time aclwdrr014 42.16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr015.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr015 "Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; li r3,1 | lwz r3,0(r4) | | ; stw r3,0(r4) | | | ; exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr015 Allowed Histogram (15 states) 99 :>1:r3=0; 3:r1=0; 3:r3=0; x=2; 888 :>1:r3=0; 3:r1=1; 3:r3=1; x=2; 79451 :>1:r3=0; 3:r1=1; 3:r3=0; x=1; 63958 :>1:r3=1; 3:r1=1; 3:r3=0; x=2; 25015 :>1:r3=0; 3:r1=0; 3:r3=1; x=2; 1649760:>1:r3=1; 3:r1=1; 3:r3=0; x=1; 445943:>1:r3=1; 3:r1=0; 3:r3=0; x=2; 649210:>1:r3=0; 3:r1=0; 3:r3=0; x=1; 1024629:>1:r3=0; 3:r1=1; 3:r3=1; x=1; 1407908:>1:r3=0; 3:r1=0; 3:r3=1; x=1; 661037:>1:r3=1; 3:r1=0; 3:r3=1; x=1; 5088714:>1:r3=1; 3:r1=1; 3:r3=1; x=1; 4591765:>1:r3=1; 3:r1=0; 3:r3=0; x=1; 2952152:>1:r3=1; 3:r1=1; 3:r3=1; x=2; 1359471:>1:r3=1; 3:r1=0; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=61d664ae95ff6d97da76ebb37bc47ca3 Cycle=Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr015 No ACLwSyncdRR Safe=Fre Wse SyncdWW SyncdWR Time aclwdrr015 37.18 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr016.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr016 "Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | sync | | lwz r3,0(r4) ; li r3,1 | lwz r3,0(r4) | | ; stw r3,0(r4) | | | ; exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr016 Allowed Histogram (15 states) 1452 :>1:r3=0; 3:r1=0; 3:r3=0; x=2; 48343 :>1:r3=1; 3:r1=1; 3:r3=0; x=2; 43469 :>1:r3=0; 3:r1=1; 3:r3=0; x=1; 1376 :>1:r3=0; 3:r1=1; 3:r3=1; x=2; 1151519:>1:r3=1; 3:r1=1; 3:r3=0; x=1; 50345 :>1:r3=0; 3:r1=0; 3:r3=1; x=2; 1075843:>1:r3=0; 3:r1=1; 3:r3=1; x=1; 901283:>1:r3=1; 3:r1=0; 3:r3=0; x=2; 946963:>1:r3=0; 3:r1=0; 3:r3=0; x=1; 1769914:>1:r3=1; 3:r1=0; 3:r3=1; x=2; 1335355:>1:r3=0; 3:r1=0; 3:r3=1; x=1; 3867647:>1:r3=1; 3:r1=1; 3:r3=1; x=1; 346496:>1:r3=1; 3:r1=0; 3:r3=1; x=1; 4163746:>1:r3=1; 3:r1=0; 3:r3=0; x=1; 4296249:>1:r3=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=4947e9ed11cb60630be5b54900bf7b6c Cycle=Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr016 No ACLwSyncdRR Safe=Fre Wse SyncdWR LwSyncdWW Time aclwdrr016 38.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr017.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr017 "Fre SyncdWR Fre Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | | lwz r3,0(r4) ; lwz r3,0(r4) | | ; exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r8,1 _litmus_P0_1_: stw r8,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r10,0(r2) _litmus_P1_0_: li r9,1 _litmus_P1_1_: stw r9,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr017 Allowed Histogram (7 states) 2986830:>0:r3=1; 2:r1=1; 2:r3=0; 55209 :>0:r3=0; 2:r1=0; 2:r3=0; 1841255:>0:r3=0; 2:r1=0; 2:r3=1; 6403169:>0:r3=1; 2:r1=0; 2:r3=0; 1470610:>0:r3=1; 2:r1=0; 2:r3=1; 1278851:>0:r3=0; 2:r1=1; 2:r3=1; 5964076:>0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=0dd8df1959f84e11508b32d374a44775 Cycle=Fre SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr017 No ACLwSyncdRR Safe=Fre SyncdWR Time aclwdrr017 23.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr018.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr018 "Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r4) | lwz r3,0(r4) | | ; exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r8,0(r2) _litmus_P1_0_: li r10,1 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr018 Allowed Histogram (15 states) 321 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0; 43442 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0; 6471 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1; 56113 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1; 106686:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0; 584801:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; 584164:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; 973952:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; 1804658:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; 509587:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; 4369731:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; 1995034:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; 4371009:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; 2944412:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; 1649619:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=3fed6cc74892902ab28df779672578f8 Cycle=Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr018 No ACLwSyncdRR Safe=Fre SyncdWR Time aclwdrr018 36.73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr019.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr019 "Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r2) | lwz r3,0(r4) | | ; exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r9,1 _litmus_P0_1_: stw r9,0(r2) _litmus_P0_2_: sync _litmus_P0_3_: lwz r10,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr019 Allowed Histogram (30 states) 565 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 2070 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 1053 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 123 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 3877 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 17869 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1; 298259:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1; 83118 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 302786:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1; 402977:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1; 25945 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 246390:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 2951 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 96518 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1; 157182:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1; 40221 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 66712 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 918762:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 435879:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 228925:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1; 1591166:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1; 1364336:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1; 1951761:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1; 1075821:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1139973:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 1393074:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1611668:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 2350177:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1; 3294226:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 895616:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; No Witnesses Positive: 0, Negative: 20000000 Condition exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=660c5e262906b3ab9066962d8bf69882 Cycle=Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr019 No ACLwSyncdRR Safe=Fre SyncsWR SyncdWR Time aclwdrr019 45.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/aclwdrr020.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr020 "Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r4) | lwz r3,0(r2) | | ; exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r8,0(r2) _litmus_P1_0_: li r9,1 _litmus_P1_1_: stw r9,0(r2) _litmus_P1_2_: sync _litmus_P1_3_: lwz r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr020 Allowed Histogram (44 states) 5 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 36 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 49 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 17 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 1479 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 15 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 5573 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 245 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; 7820 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 227 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 91243 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 3454 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; 35411 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; 15507 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 17448 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 992817:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 580822:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 8003 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 572961:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1; 1318619:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; 47515 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 235775:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 157597:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 197614:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 189706:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 239899:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 525883:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; 506758:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 174510:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 881337:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 1521805:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 1851938:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 413159:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 474206:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 134710:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 917887:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 2083969:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 973368:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 161620:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 2708772:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 344452:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 493842:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 181032:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 930895:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; No Witnesses Positive: 0, Negative: 20000000 Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=bad92812900a1656a66221eff19f711e Cycle=Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR Relax aclwdrr020 No ACLwSyncdRR Safe=Fre SyncsWR SyncdWR Time aclwdrr020 48.02 $Revision: 3163 $ Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 1000000 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 1 #endif #ifndef N_EXE #define N_EXE (4 < N ? 1 : 4 / N) #endif /* gcc options: -Wall -std=gnu99 */ /* barrier: user */ /* tread start/join: changing */ /* memory: indirect */ /* safer: false */ /* preload: true */ /* para: self */ /* changes: false */ /* speedcheck: false */ /* proc used: 4 */ GCCOPTS="-Wall -std=gnu99 " LITMUSOPTS=-r 20 Thu Dec 24 23:19:46 CET 2009