Tue Dec 22 18:38:53 GMT 2009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw000.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw000 "Rfe SyncdRW Rfe SyncdRW" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;} P0 | P1 ; lwz r1,0(r2) | lwz r1,0(r2) ; sync | sync ; li r3,1 | li r3,1 ; stw r3,0(r4) | stw r3,0(r4) ; exists (0:r1=1 /\ 1:r1=1) Generated assembler _litmus_P1_0_: lwz 4,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 5,1 _litmus_P1_3_: stw 5,0(9) _litmus_P0_0_: lwz 4,0(11) _litmus_P0_1_: sync _litmus_P0_2_: li 5,1 _litmus_P0_3_: stw 5,0(9) Test acsdrw000 Allowed Histogram (3 states) 212963230:>0:r1=0; 1:r1=0; 207924270:>0:r1=1; 1:r1=0; 219112500:>0:r1=0; 1:r1=1; No Witnesses Positive: 0, Negative: 640000000 Condition exists (0:r1=1 /\ 1:r1=1) is NOT validated Hash=594183612285ea19f22ca74320b9670d Cycle=Rfe SyncdRW Rfe SyncdRW Relax acsdrw000 No ACSyncdRW Safe= Time acsdrw000 78.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw001.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw001 "Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; sync | sync | sync ; li r3,1 | li r3,1 | li r3,1 ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: lwz 3,0(11) _litmus_P0_1_: sync _litmus_P0_2_: li 4,1 _litmus_P0_3_: stw 4,0(9) Test acsdrw001 Allowed Histogram (7 states) 5474099:>0:r1=1; 1:r1=0; 2:r1=1; 4512346:>0:r1=1; 1:r1=1; 2:r1=0; 109138863:>0:r1=0; 1:r1=0; 2:r1=1; 59149168:>0:r1=0; 1:r1=0; 2:r1=0; 7124806:>0:r1=0; 1:r1=1; 2:r1=1; 101106836:>0:r1=1; 1:r1=0; 2:r1=0; 113493882:>0:r1=0; 1:r1=1; 2:r1=0; No Witnesses Positive: 0, Negative: 400000000 Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1) is NOT validated Hash=e9f79bffdc4009277d2d5ec18c343e3a Cycle=Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW Relax acsdrw001 No ACSyncdRW Safe= Time acsdrw001 78.40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw002.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw002 "Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; sync | sync | sync | sync ; li r3,1 | li r3,1 | li r3,1 | li r3,1 ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 4,1 _litmus_P1_3_: stw 4,0(9) _litmus_P0_0_: lwz 3,0(11) _litmus_P0_1_: sync _litmus_P0_2_: li 4,1 _litmus_P0_3_: stw 4,0(9) Test acsdrw002 Allowed Histogram (15 states) 166004:>0:r1=1; 1:r1=1; 2:r1=1; 3:r1=0; 161460:>0:r1=0; 1:r1=1; 2:r1=1; 3:r1=1; 158760:>0:r1=1; 1:r1=1; 2:r1=0; 3:r1=1; 159725:>0:r1=1; 1:r1=0; 2:r1=1; 3:r1=1; 23779119:>0:r1=0; 1:r1=0; 2:r1=0; 3:r1=0; 7095360:>0:r1=1; 1:r1=1; 2:r1=0; 3:r1=0; 7149076:>0:r1=0; 1:r1=1; 2:r1=1; 3:r1=0; 7468753:>0:r1=1; 1:r1=0; 2:r1=0; 3:r1=1; 51295566:>0:r1=0; 1:r1=0; 2:r1=1; 3:r1=0; 51943937:>0:r1=0; 1:r1=0; 2:r1=0; 3:r1=1; 7260485:>0:r1=0; 1:r1=0; 2:r1=1; 3:r1=1; 30838753:>0:r1=1; 1:r1=0; 2:r1=1; 3:r1=0; 30898184:>0:r1=0; 1:r1=1; 2:r1=0; 3:r1=1; 50705730:>0:r1=0; 1:r1=1; 2:r1=0; 3:r1=0; 50919088:>0:r1=1; 1:r1=0; 2:r1=0; 3:r1=0; No Witnesses Positive: 0, Negative: 320000000 Condition exists (0:r1=1 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=43fcee2c783ce4df2d729acef9bebaf0 Cycle=Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW Relax acsdrw002 No ACSyncdRW Safe= Time acsdrw002 92.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw003.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw003 "Wse Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) | li r1,2 ; sync | sync | sync | stw r1,0(r2) ; li r3,1 | li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) | ; exists (z=2 /\ 0:r1=2 /\ 1:r1=1 /\ 2:r1=1) Generated assembler _litmus_P3_0_: li 8,2 _litmus_P3_1_: stw 8,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 4,1 _litmus_P1_3_: stw 4,0(9) _litmus_P0_0_: lwz 4,0(11) _litmus_P0_1_: sync _litmus_P0_2_: li 5,1 _litmus_P0_3_: stw 5,0(9) Test acsdrw003 Allowed Histogram (21 states) 1352335:>0:r1=2; 1:r1=0; 2:r1=1; z=2; 820151:>0:r1=1; 1:r1=0; 2:r1=1; z=2; 757923:>0:r1=2; 1:r1=1; 2:r1=1; z=1; 149516:>0:r1=0; 1:r1=1; 2:r1=1; z=2; 3772809:>0:r1=1; 1:r1=1; 2:r1=0; z=2; 6475498:>0:r1=0; 1:r1=0; 2:r1=0; z=1; 21449435:>0:r1=1; 1:r1=0; 2:r1=0; z=2; 24309762:>0:r1=0; 1:r1=0; 2:r1=0; z=2; 13262717:>0:r1=2; 1:r1=1; 2:r1=0; z=1; 8567852:>0:r1=1; 1:r1=0; 2:r1=1; z=1; 35512607:>0:r1=2; 1:r1=0; 2:r1=1; z=1; 28657466:>0:r1=0; 1:r1=1; 2:r1=0; z=1; 35629076:>0:r1=0; 1:r1=0; 2:r1=1; z=1; 20490298:>0:r1=2; 1:r1=0; 2:r1=0; z=1; 6604750:>0:r1=0; 1:r1=1; 2:r1=1; z=1; 10090486:>0:r1=0; 1:r1=0; 2:r1=1; z=2; 2071791:>0:r1=2; 1:r1=1; 2:r1=0; z=2; 2667058:>0:r1=1; 1:r1=1; 2:r1=0; z=1; 32184185:>0:r1=0; 1:r1=1; 2:r1=0; z=2; 31859311:>0:r1=1; 1:r1=0; 2:r1=0; z=1; 33314974:>0:r1=2; 1:r1=0; 2:r1=0; z=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (z=2 /\ 0:r1=2 /\ 1:r1=1 /\ 2:r1=1) is NOT validated Hash=aea399e22ba161d291e7b869ebf94dca Cycle=Wse Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW Relax acsdrw003 No ACSyncdRW Safe=Wse Time acsdrw003 86.04 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw004.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw004 "Wse SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | sync ; sync | li r3,1 | li r3,1 | li r3,1 ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; stw r3,0(r4) | | | ; exists (a=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 4,1 _litmus_P1_3_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw004 Allowed Histogram (15 states) 305639:>1:r1=1; 2:r1=1; 3:r1=0; a=2; 373993:>1:r1=1; 2:r1=0; 3:r1=1; a=2; 14738442:>1:r1=0; 2:r1=0; 3:r1=0; a=1; 118019:>1:r1=1; 2:r1=1; 3:r1=1; a=1; 7243774:>1:r1=0; 2:r1=1; 3:r1=1; a=1; 45296439:>1:r1=0; 2:r1=1; 3:r1=0; a=2; 25793962:>1:r1=1; 2:r1=0; 3:r1=1; a=1; 41310011:>1:r1=0; 2:r1=1; 3:r1=0; a=1; 12253885:>1:r1=0; 2:r1=0; 3:r1=1; a=2; 11837982:>1:r1=1; 2:r1=0; 3:r1=0; a=2; 6153511:>1:r1=1; 2:r1=1; 3:r1=0; a=1; 48265601:>1:r1=0; 2:r1=0; 3:r1=1; a=1; 64737117:>1:r1=0; 2:r1=0; 3:r1=0; a=2; 41322323:>1:r1=1; 2:r1=0; 3:r1=0; a=1; 249302:>1:r1=0; 2:r1=1; 3:r1=1; a=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=7a59c834bf44e53a4afef86a80f647c7 Cycle=Wse SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW Relax acsdrw004 No ACSyncdRW Safe=Wse SyncdWW Time acsdrw004 91.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw005.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw005 "Wse LwSyncdWW Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | sync ; lwsync | li r3,1 | li r3,1 | li r3,1 ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; stw r3,0(r4) | | | ; exists (a=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 4,1 _litmus_P1_3_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw005 Allowed Histogram (15 states) 212683:>1:r1=0; 2:r1=1; 3:r1=1; a=2; 242091:>1:r1=1; 2:r1=1; 3:r1=1; a=1; 467419:>1:r1=1; 2:r1=1; 3:r1=0; a=2; 407205:>1:r1=1; 2:r1=0; 3:r1=1; a=2; 11581274:>1:r1=0; 2:r1=0; 3:r1=0; a=1; 37717449:>1:r1=0; 2:r1=1; 3:r1=0; a=1; 46968166:>1:r1=1; 2:r1=0; 3:r1=0; a=1; 44659458:>1:r1=0; 2:r1=0; 3:r1=1; a=1; 30647582:>1:r1=1; 2:r1=0; 3:r1=1; a=1; 14559129:>1:r1=1; 2:r1=0; 3:r1=0; a=2; 6939012:>1:r1=0; 2:r1=1; 3:r1=1; a=1; 11110868:>1:r1=0; 2:r1=0; 3:r1=1; a=2; 61268703:>1:r1=0; 2:r1=0; 3:r1=0; a=2; 9571030:>1:r1=1; 2:r1=1; 3:r1=0; a=1; 43647931:>1:r1=0; 2:r1=1; 3:r1=0; a=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=ae4a7029db4e5441e31be405bd78f18a Cycle=Wse LwSyncdWW Rfe SyncdRW Rfe SyncdRW Rfe SyncdRW Relax acsdrw005 No ACSyncdRW Safe=Wse LwSyncdWW Time acsdrw005 90.23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw006.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw006 "Wse Rfe SyncdRW Rfe SyncdRW" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;} P0 | P1 | P2 ; lwz r1,0(r2) | lwz r1,0(r2) | li r1,2 ; sync | sync | stw r1,0(r2) ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (y=2 /\ 0:r1=2 /\ 1:r1=1) Generated assembler _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 4,1 _litmus_P1_3_: stw 4,0(9) _litmus_P0_0_: lwz 3,0(11) _litmus_P0_1_: sync _litmus_P0_2_: li 4,1 _litmus_P0_3_: stw 4,0(9) Test acsdrw006 Allowed Histogram (9 states) 10190895:>0:r1=0; 1:r1=0; y=1; 21736160:>0:r1=2; 1:r1=1; y=1; 46608174:>0:r1=2; 1:r1=0; y=2; 12645658:>0:r1=0; 1:r1=1; y=2; 62957892:>0:r1=2; 1:r1=0; y=1; 25189649:>0:r1=1; 1:r1=0; y=2; 82245786:>0:r1=0; 1:r1=0; y=2; 78875347:>0:r1=0; 1:r1=1; y=1; 59550439:>0:r1=1; 1:r1=0; y=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (y=2 /\ 0:r1=2 /\ 1:r1=1) is NOT validated Hash=e3edf89052cc50f1c44e40a365bc727f Cycle=Wse Rfe SyncdRW Rfe SyncdRW Relax acsdrw006 No ACSyncdRW Safe=Wse Time acsdrw006 73.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw007.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw007 "Wse SyncdWW Wse Rfe SyncdRW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; sync | | li r3,1 | li r3,1 ; li r3,1 | | stw r3,0(r4) | stw r3,0(r4) ; stw r3,0(r4) | | | ; exists (x=2 /\ z=2 /\ 2:r1=2 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 7,2 _litmus_P1_1_: stw 7,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw007 Allowed Histogram (21 states) 1648874:>2:r1=1; 3:r1=1; x=1; z=1; 1397910:>2:r1=2; 3:r1=1; x=1; z=2; 3381075:>2:r1=1; 3:r1=1; x=2; z=1; 2393723:>2:r1=2; 3:r1=0; x=2; z=2; 1475342:>2:r1=1; 3:r1=0; x=2; z=2; 1708012:>2:r1=2; 3:r1=1; x=2; z=1; 14374482:>2:r1=2; 3:r1=1; x=1; z=1; 12850444:>2:r1=1; 3:r1=0; x=1; z=2; 548048:>2:r1=0; 3:r1=1; x=2; z=2; 29491779:>2:r1=0; 3:r1=1; x=2; z=1; 3184501:>2:r1=0; 3:r1=0; x=1; z=1; 17021501:>2:r1=0; 3:r1=0; x=2; z=1; 18214485:>2:r1=1; 3:r1=0; x=2; z=1; 29208072:>2:r1=0; 3:r1=1; x=1; z=1; 12739699:>2:r1=0; 3:r1=1; x=1; z=2; 22630409:>2:r1=1; 3:r1=0; x=1; z=1; 45966893:>2:r1=2; 3:r1=0; x=1; z=2; 42438003:>2:r1=0; 3:r1=0; x=1; z=2; 27516063:>2:r1=2; 3:r1=0; x=2; z=1; 16220433:>2:r1=2; 3:r1=0; x=1; z=1; 15590252:>2:r1=0; 3:r1=0; x=2; z=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ z=2 /\ 2:r1=2 /\ 3:r1=1) is NOT validated Hash=607d50c12790231d610fd3d79d562962 Cycle=Wse SyncdWW Wse Rfe SyncdRW Rfe SyncdRW Relax acsdrw007 No ACSyncdRW Safe=Wse SyncdWW Time acsdrw007 84.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw008.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw008 "Wse LwSyncdWW Wse Rfe SyncdRW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; lwsync | | li r3,1 | li r3,1 ; li r3,1 | | stw r3,0(r4) | stw r3,0(r4) ; stw r3,0(r4) | | | ; exists (x=2 /\ z=2 /\ 2:r1=2 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 7,2 _litmus_P1_1_: stw 7,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw008 Allowed Histogram (21 states) 615108:>2:r1=0; 3:r1=1; x=2; z=2; 1790077:>2:r1=1; 3:r1=1; x=1; z=1; 2328412:>2:r1=2; 3:r1=1; x=2; z=1; 3011683:>2:r1=0; 3:r1=0; x=1; z=1; 1199275:>2:r1=2; 3:r1=1; x=1; z=2; 22300749:>2:r1=1; 3:r1=0; x=1; z=1; 2084216:>2:r1=1; 3:r1=0; x=2; z=2; 15046699:>2:r1=0; 3:r1=0; x=2; z=1; 16882810:>2:r1=0; 3:r1=0; x=2; z=2; 15700446:>2:r1=2; 3:r1=0; x=1; z=1; 5568102:>2:r1=1; 3:r1=1; x=2; z=1; 10897562:>2:r1=0; 3:r1=1; x=1; z=2; 3101635:>2:r1=2; 3:r1=0; x=2; z=2; 27133896:>2:r1=0; 3:r1=1; x=1; z=1; 40555823:>2:r1=2; 3:r1=0; x=1; z=2; 23816460:>2:r1=1; 3:r1=0; x=2; z=1; 40374401:>2:r1=0; 3:r1=0; x=1; z=2; 13198917:>2:r1=2; 3:r1=1; x=1; z=1; 27423875:>2:r1=0; 3:r1=1; x=2; z=1; 32905439:>2:r1=2; 3:r1=0; x=2; z=1; 14064415:>2:r1=1; 3:r1=0; x=1; z=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ z=2 /\ 2:r1=2 /\ 3:r1=1) is NOT validated Hash=a2cf778e758c7ad9ed656ae2435bb232 Cycle=Wse LwSyncdWW Wse Rfe SyncdRW Rfe SyncdRW Relax acsdrw008 No ACSyncdRW Safe=Wse LwSyncdWW Time acsdrw008 86.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw009.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw009 "Wse SyncdWR Fre Rfe SyncdRW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; sync | | li r3,1 | li r3,1 ; lwz r3,0(r4) | | stw r3,0(r4) | stw r3,0(r4) ; exists (z=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 7,1 _litmus_P1_1_: stw 7,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrw009 Allowed Histogram (15 states) 931973:>0:r3=0; 2:r1=0; 3:r1=1; z=2; 2332505:>0:r3=1; 2:r1=0; 3:r1=0; z=1; 1293605:>0:r3=1; 2:r1=1; 3:r1=1; z=2; 4876653:>0:r3=0; 2:r1=1; 3:r1=0; z=2; 24617508:>0:r3=0; 2:r1=0; 3:r1=0; z=2; 35575178:>0:r3=1; 2:r1=1; 3:r1=0; z=1; 29204153:>0:r3=0; 2:r1=1; 3:r1=0; z=1; 23230374:>0:r3=1; 2:r1=0; 3:r1=1; z=1; 1895168:>0:r3=0; 2:r1=1; 3:r1=1; z=1; 11028503:>0:r3=1; 2:r1=0; 3:r1=1; z=2; 37257682:>0:r3=1; 2:r1=0; 3:r1=0; z=2; 14427222:>0:r3=1; 2:r1=1; 3:r1=1; z=1; 38662874:>0:r3=0; 2:r1=0; 3:r1=1; z=1; 56069269:>0:r3=1; 2:r1=1; 3:r1=0; z=2; 38597333:>0:r3=0; 2:r1=0; 3:r1=0; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (z=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=9fc08bd228c3c568859dbc72215d222b Cycle=Wse SyncdWR Fre Rfe SyncdRW Rfe SyncdRW Relax acsdrw009 No ACSyncdRW Safe=Fre Wse SyncdWR Time acsdrw009 82.80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw010.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw010 "Wse SyncdWW Rfe SyncdRW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync ; sync | li r3,1 | li r3,1 ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) ; stw r3,0(r4) | | ; exists (z=2 /\ 1:r1=1 /\ 2:r1=1) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw010 Allowed Histogram (7 states) 36900296:>1:r1=0; 2:r1=0; z=1; 5237565:>1:r1=1; 2:r1=1; z=1; 10169049:>1:r1=1; 2:r1=0; z=2; 104196892:>1:r1=0; 2:r1=1; z=1; 139020637:>1:r1=0; 2:r1=0; z=2; 14004130:>1:r1=0; 2:r1=1; z=2; 90471431:>1:r1=1; 2:r1=0; z=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (z=2 /\ 1:r1=1 /\ 2:r1=1) is NOT validated Hash=b7caef3c5ae45279350129eabce6d3e4 Cycle=Wse SyncdWW Rfe SyncdRW Rfe SyncdRW Relax acsdrw010 No ACSyncdRW Safe=Wse SyncdWW Time acsdrw010 75.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw011.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw011 "Wse SyncdWW Wse SyncdWW Rfe SyncdRW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; sync | sync | li r3,1 | li r3,1 ; li r3,1 | li r3,1 | stw r3,0(r4) | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (a=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: li 5,2 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw011 Allowed Histogram (15 states) 200048:>2:r1=1; 3:r1=1; a=1; x=2; 854967:>2:r1=1; 3:r1=0; a=2; x=2; 563222:>2:r1=0; 3:r1=1; a=2; x=2; 131343:>2:r1=1; 3:r1=1; a=2; x=1; 5013887:>2:r1=1; 3:r1=1; a=1; x=1; 9446674:>2:r1=1; 3:r1=0; a=1; x=2; 21850058:>2:r1=0; 3:r1=0; a=2; x=2; 38901995:>2:r1=0; 3:r1=1; a=1; x=1; 53536765:>2:r1=0; 3:r1=0; a=1; x=2; 63753350:>2:r1=0; 3:r1=0; a=2; x=1; 11015262:>2:r1=0; 3:r1=1; a=2; x=1; 37157883:>2:r1=0; 3:r1=1; a=1; x=2; 8939181:>2:r1=0; 3:r1=0; a=1; x=1; 37089041:>2:r1=1; 3:r1=0; a=2; x=1; 31546324:>2:r1=1; 3:r1=0; a=1; x=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=b9ade8d0220b83a03881ae45af94a30f Cycle=Wse SyncdWW Wse SyncdWW Rfe SyncdRW Rfe SyncdRW Relax acsdrw011 No ACSyncdRW Safe=Wse SyncdWW Time acsdrw011 91.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw012.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw012 "Wse LwSyncdWW Wse SyncdWW Rfe SyncdRW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; lwsync | sync | li r3,1 | li r3,1 ; li r3,1 | li r3,1 | stw r3,0(r4) | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (a=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: li 5,2 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw012 Allowed Histogram (15 states) 111020:>2:r1=1; 3:r1=1; a=2; x=1; 265817:>2:r1=1; 3:r1=1; a=1; x=2; 8650936:>2:r1=0; 3:r1=0; a=1; x=1; 621269:>2:r1=0; 3:r1=1; a=2; x=2; 1084763:>2:r1=1; 3:r1=0; a=2; x=2; 36294802:>2:r1=0; 3:r1=1; a=1; x=1; 60054002:>2:r1=0; 3:r1=0; a=2; x=1; 9749004:>2:r1=0; 3:r1=1; a=2; x=1; 30042485:>2:r1=1; 3:r1=0; a=1; x=1; 39887345:>2:r1=0; 3:r1=1; a=1; x=2; 58144201:>2:r1=0; 3:r1=0; a=1; x=2; 24554024:>2:r1=0; 3:r1=0; a=2; x=2; 34585945:>2:r1=1; 3:r1=0; a=2; x=1; 11358332:>2:r1=1; 3:r1=0; a=1; x=2; 4596055:>2:r1=1; 3:r1=1; a=1; x=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=fab526cda64c209da4ced7f908a22782 Cycle=Wse LwSyncdWW Wse SyncdWW Rfe SyncdRW Rfe SyncdRW Relax acsdrw012 No ACSyncdRW Safe=Wse SyncdWW LwSyncdWW Time acsdrw012 90.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw013.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw013 "Wse SyncdWR Fre SyncdWW Rfe SyncdRW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; sync | sync | li r3,1 | li r3,1 ; lwz r3,0(r4) | li r3,1 | stw r3,0(r4) | stw r3,0(r4) ; | stw r3,0(r4) | | ; exists (a=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: li 5,1 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrw013 Allowed Histogram (15 states) 6224098:>0:r3=1; 2:r1=0; 3:r1=0; a=1; 206205:>0:r3=1; 2:r1=1; 3:r1=1; a=2; 1695435:>0:r3=0; 2:r1=1; 3:r1=0; a=2; 43992089:>0:r3=0; 2:r1=0; 3:r1=1; a=1; 36424669:>0:r3=1; 2:r1=1; 3:r1=0; a=2; 1128599:>0:r3=0; 2:r1=0; 3:r1=1; a=2; 11994461:>0:r3=0; 2:r1=1; 3:r1=0; a=1; 11898683:>0:r3=1; 2:r1=0; 3:r1=1; a=2; 30190058:>0:r3=0; 2:r1=0; 3:r1=0; a=2; 55101962:>0:r3=0; 2:r1=0; 3:r1=0; a=1; 29233349:>0:r3=1; 2:r1=1; 3:r1=0; a=1; 32459628:>0:r3=1; 2:r1=0; 3:r1=1; a=1; 53810334:>0:r3=1; 2:r1=0; 3:r1=0; a=2; 273499:>0:r3=0; 2:r1=1; 3:r1=1; a=1; 5366931:>0:r3=1; 2:r1=1; 3:r1=1; a=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=2054e24c0e49fb7d37b5054aea43835a Cycle=Wse SyncdWR Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Relax acsdrw013 No ACSyncdRW Safe=Fre Wse SyncdWW SyncdWR Time acsdrw013 89.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw014.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw014 "Wse SyncdWR Fre SyncsWW Rfe SyncdRW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; sync | sync | li r3,1 | li r3,1 ; lwz r3,0(r4) | li r3,2 | stw r3,0(r4) | stw r3,0(r4) ; | stw r3,0(r2) | | ; exists (x=2 /\ z=2 /\ 0:r3=0 /\ 2:r1=2 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 6,1 _litmus_P1_1_: stw 6,0(9) _litmus_P1_2_: sync _litmus_P1_3_: li 11,2 _litmus_P1_4_: stw 11,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrw014 Allowed Histogram (33 states) 375 :>0:r3=1; 2:r1=1; 3:r1=1; x=2; z=2; 260017:>0:r3=1; 2:r1=2; 3:r1=1; x=2; z=1; 635676:>0:r3=1; 2:r1=0; 3:r1=0; x=2; z=1; 2647010:>0:r3=1; 2:r1=2; 3:r1=0; x=2; z=1; 530479:>0:r3=2; 2:r1=2; 3:r1=1; x=2; z=2; 1448393:>0:r3=0; 2:r1=0; 3:r1=1; x=2; z=2; 444640:>0:r3=1; 2:r1=1; 3:r1=1; x=2; z=1; 1132369:>0:r3=1; 2:r1=0; 3:r1=1; x=2; z=2; 628096:>0:r3=2; 2:r1=1; 3:r1=1; x=2; z=2; 3479436:>0:r3=0; 2:r1=2; 3:r1=0; x=2; z=2; 7199114:>0:r3=1; 2:r1=0; 3:r1=0; x=2; z=2; 867690:>0:r3=1; 2:r1=1; 3:r1=0; x=2; z=1; 1936057:>0:r3=1; 2:r1=1; 3:r1=0; x=2; z=2; 2367040:>0:r3=1; 2:r1=2; 3:r1=0; x=2; z=2; 1174184:>0:r3=2; 2:r1=0; 3:r1=0; x=2; z=1; 3326812:>0:r3=2; 2:r1=1; 3:r1=1; x=2; z=1; 1889684:>0:r3=2; 2:r1=1; 3:r1=0; x=2; z=1; 7229785:>0:r3=0; 2:r1=1; 3:r1=0; x=2; z=1; 38548030:>0:r3=0; 2:r1=0; 3:r1=0; x=2; z=1; 9705014:>0:r3=2; 2:r1=2; 3:r1=1; x=2; z=1; 1898844:>0:r3=0; 2:r1=1; 3:r1=0; x=2; z=2; 6547513:>0:r3=2; 2:r1=1; 3:r1=0; x=2; z=2; 779370:>0:r3=0; 2:r1=1; 3:r1=1; x=2; z=1; 5823879:>0:r3=1; 2:r1=0; 3:r1=1; x=2; z=1; 27583005:>0:r3=0; 2:r1=0; 3:r1=0; x=2; z=2; 9712609:>0:r3=2; 2:r1=0; 3:r1=1; x=2; z=2; 16028123:>0:r3=2; 2:r1=0; 3:r1=1; x=2; z=1; 31090889:>0:r3=2; 2:r1=2; 3:r1=0; x=2; z=1; 839517:>0:r3=0; 2:r1=2; 3:r1=1; x=2; z=1; 43993560:>0:r3=2; 2:r1=2; 3:r1=0; x=2; z=2; 27222869:>0:r3=2; 2:r1=0; 3:r1=0; x=2; z=2; 41312383:>0:r3=0; 2:r1=0; 3:r1=1; x=2; z=1; 21717538:>0:r3=0; 2:r1=2; 3:r1=0; x=2; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ z=2 /\ 0:r3=0 /\ 2:r1=2 /\ 3:r1=1) is NOT validated Hash=d5ba76f85bcf996414074a6c632a2f47 Cycle=Wse SyncdWR Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Relax acsdrw014 No ACSyncdRW Safe=Fre Wse SyncsWW SyncdWR Time acsdrw014 91.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw015.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw015 "Wse SyncdWR Fre LwSyncsWW Rfe SyncdRW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; sync | lwsync | li r3,1 | li r3,1 ; lwz r3,0(r4) | li r3,2 | stw r3,0(r4) | stw r3,0(r4) ; | stw r3,0(r2) | | ; exists (x=2 /\ z=2 /\ 0:r3=0 /\ 2:r1=2 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 6,1 _litmus_P1_1_: stw 6,0(9) _litmus_P1_2_: lwsync _litmus_P1_3_: li 11,2 _litmus_P1_4_: stw 11,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrw015 Allowed Histogram (33 states) 171 :>0:r3=1; 2:r1=1; 3:r1=1; x=2; z=2; 56686 :>0:r3=1; 2:r1=2; 3:r1=1; x=2; z=1; 717987:>0:r3=1; 2:r1=2; 3:r1=0; x=2; z=1; 74482 :>0:r3=1; 2:r1=1; 3:r1=1; x=2; z=1; 279226:>0:r3=1; 2:r1=0; 3:r1=0; x=2; z=1; 182425:>0:r3=1; 2:r1=1; 3:r1=0; x=2; z=1; 901331:>0:r3=1; 2:r1=2; 3:r1=0; x=2; z=2; 2432697:>0:r3=1; 2:r1=0; 3:r1=1; x=2; z=1; 3651526:>0:r3=2; 2:r1=1; 3:r1=0; x=2; z=2; 1601304:>0:r3=2; 2:r1=1; 3:r1=1; x=2; z=1; 1568741:>0:r3=2; 2:r1=1; 3:r1=0; x=2; z=1; 203432:>0:r3=2; 2:r1=1; 3:r1=1; x=2; z=2; 670470:>0:r3=1; 2:r1=1; 3:r1=0; x=2; z=2; 840042:>0:r3=0; 2:r1=1; 3:r1=0; x=2; z=2; 408857:>0:r3=0; 2:r1=1; 3:r1=1; x=2; z=1; 2605037:>0:r3=1; 2:r1=0; 3:r1=0; x=2; z=2; 411362:>0:r3=1; 2:r1=0; 3:r1=1; x=2; z=2; 3321321:>0:r3=0; 2:r1=1; 3:r1=0; x=2; z=1; 763436:>0:r3=2; 2:r1=2; 3:r1=1; x=2; z=2; 1915973:>0:r3=2; 2:r1=0; 3:r1=0; x=2; z=1; 1468574:>0:r3=0; 2:r1=2; 3:r1=1; x=2; z=1; 20890161:>0:r3=2; 2:r1=0; 3:r1=1; x=2; z=1; 1248844:>0:r3=0; 2:r1=0; 3:r1=1; x=2; z=2; 34383838:>0:r3=2; 2:r1=2; 3:r1=0; x=2; z=1; 12279126:>0:r3=2; 2:r1=2; 3:r1=1; x=2; z=1; 4526781:>0:r3=0; 2:r1=2; 3:r1=0; x=2; z=2; 36623244:>0:r3=0; 2:r1=0; 3:r1=0; x=2; z=1; 39257242:>0:r3=0; 2:r1=0; 3:r1=1; x=2; z=1; 10572631:>0:r3=2; 2:r1=0; 3:r1=1; x=2; z=2; 25457587:>0:r3=0; 2:r1=0; 3:r1=0; x=2; z=2; 27592629:>0:r3=0; 2:r1=2; 3:r1=0; x=2; z=1; 51720031:>0:r3=2; 2:r1=2; 3:r1=0; x=2; z=2; 31372806:>0:r3=2; 2:r1=0; 3:r1=0; x=2; z=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ z=2 /\ 0:r3=0 /\ 2:r1=2 /\ 3:r1=1) is NOT validated Hash=702ee4808d5fb73748d69f56dfd107f8 Cycle=Wse SyncdWR Fre LwSyncsWW Rfe SyncdRW Rfe SyncdRW Relax acsdrw015 No ACSyncdRW Safe=Fre Wse SyncdWR LwSyncsWW Time acsdrw015 91.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw016.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw016 "Wse LwSyncdWW Rfe SyncdRW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync ; lwsync | li r3,1 | li r3,1 ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) ; stw r3,0(r4) | | ; exists (z=2 /\ 1:r1=1 /\ 2:r1=1) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw016 Allowed Histogram (7 states) 13443645:>1:r1=0; 2:r1=1; z=2; 9749905:>1:r1=1; 2:r1=1; z=1; 95748266:>1:r1=0; 2:r1=1; z=1; 133513306:>1:r1=0; 2:r1=0; z=2; 27483215:>1:r1=0; 2:r1=0; z=1; 106946526:>1:r1=1; 2:r1=0; z=1; 13115137:>1:r1=1; 2:r1=0; z=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (z=2 /\ 1:r1=1 /\ 2:r1=1) is NOT validated Hash=2c5a2b2bed3928162ccda350943de6c1 Cycle=Wse LwSyncdWW Rfe SyncdRW Rfe SyncdRW Relax acsdrw016 No ACSyncdRW Safe=Wse LwSyncdWW Time acsdrw016 73.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw017.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw017 "Wse SyncdWW Wse LwSyncdWW Rfe SyncdRW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; sync | lwsync | li r3,1 | li r3,1 ; li r3,1 | li r3,1 | stw r3,0(r4) | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (a=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: li 5,2 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw017 Allowed Histogram (15 states) 301984:>2:r1=1; 3:r1=1; a=1; x=2; 494122:>2:r1=0; 3:r1=1; a=2; x=2; 36303345:>2:r1=1; 3:r1=0; a=1; x=1; 316514:>2:r1=1; 3:r1=1; a=2; x=1; 19950939:>2:r1=0; 3:r1=0; a=2; x=2; 958007:>2:r1=1; 3:r1=0; a=2; x=2; 11387537:>2:r1=1; 3:r1=0; a=1; x=2; 58547300:>2:r1=0; 3:r1=0; a=2; x=1; 35879523:>2:r1=0; 3:r1=1; a=1; x=1; 43332577:>2:r1=1; 3:r1=0; a=2; x=1; 35213524:>2:r1=0; 3:r1=1; a=1; x=2; 8154072:>2:r1=1; 3:r1=1; a=1; x=1; 7457586:>2:r1=0; 3:r1=0; a=1; x=1; 51437748:>2:r1=0; 3:r1=0; a=1; x=2; 10265222:>2:r1=0; 3:r1=1; a=2; x=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=0e9894d55bfcf40a6da717befcde113c Cycle=Wse SyncdWW Wse LwSyncdWW Rfe SyncdRW Rfe SyncdRW Relax acsdrw017 No ACSyncdRW Safe=Wse SyncdWW LwSyncdWW Time acsdrw017 91.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw018.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw018 "Wse LwSyncdWW Wse LwSyncdWW Rfe SyncdRW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; lwsync | lwsync | li r3,1 | li r3,1 ; li r3,1 | li r3,1 | stw r3,0(r4) | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (a=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: li 5,2 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw018 Allowed Histogram (15 states) 1218417:>2:r1=1; 3:r1=0; a=2; x=2; 418663:>2:r1=1; 3:r1=1; a=1; x=2; 526688:>2:r1=0; 3:r1=1; a=2; x=2; 8925922:>2:r1=0; 3:r1=1; a=2; x=1; 6944207:>2:r1=0; 3:r1=0; a=1; x=1; 22652242:>2:r1=0; 3:r1=0; a=2; x=2; 55724621:>2:r1=0; 3:r1=0; a=1; x=2; 34905395:>2:r1=1; 3:r1=0; a=1; x=1; 55332430:>2:r1=0; 3:r1=0; a=2; x=1; 37805003:>2:r1=0; 3:r1=1; a=1; x=2; 7715432:>2:r1=1; 3:r1=1; a=1; x=1; 33062505:>2:r1=0; 3:r1=1; a=1; x=1; 40579492:>2:r1=1; 3:r1=0; a=2; x=1; 13922782:>2:r1=1; 3:r1=0; a=1; x=2; 266201:>2:r1=1; 3:r1=1; a=2; x=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=12c4f2af8e04285fe806dd0e796495ae Cycle=Wse LwSyncdWW Wse LwSyncdWW Rfe SyncdRW Rfe SyncdRW Relax acsdrw018 No ACSyncdRW Safe=Wse LwSyncdWW Time acsdrw018 91.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw019.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw019 "Wse SyncdWR Fre LwSyncdWW Rfe SyncdRW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | sync ; sync | lwsync | li r3,1 | li r3,1 ; lwz r3,0(r4) | li r3,1 | stw r3,0(r4) | stw r3,0(r4) ; | stw r3,0(r4) | | ; exists (a=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: li 5,1 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrw019 Allowed Histogram (15 states) 446452:>0:r3=1; 2:r1=1; 3:r1=1; a=2; 437307:>0:r3=0; 2:r1=1; 3:r1=1; a=1; 1922566:>0:r3=0; 2:r1=1; 3:r1=0; a=2; 8164096:>0:r3=1; 2:r1=1; 3:r1=1; a=1; 927510:>0:r3=0; 2:r1=0; 3:r1=1; a=2; 53181805:>0:r3=0; 2:r1=0; 3:r1=0; a=1; 5277655:>0:r3=1; 2:r1=0; 3:r1=0; a=1; 29952104:>0:r3=1; 2:r1=0; 3:r1=1; a=1; 41600925:>0:r3=0; 2:r1=0; 3:r1=1; a=1; 42086104:>0:r3=1; 2:r1=1; 3:r1=0; a=2; 50115898:>0:r3=1; 2:r1=0; 3:r1=0; a=2; 10688379:>0:r3=1; 2:r1=0; 3:r1=1; a=2; 14628815:>0:r3=0; 2:r1=1; 3:r1=0; a=1; 33240642:>0:r3=1; 2:r1=1; 3:r1=0; a=1; 27329742:>0:r3=0; 2:r1=0; 3:r1=0; a=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=5bbd5723e3c95c4928dd3326b6d1cb2c Cycle=Wse SyncdWR Fre LwSyncdWW Rfe SyncdRW Rfe SyncdRW Relax acsdrw019 No ACSyncdRW Safe=Fre Wse SyncdWR LwSyncdWW Time acsdrw019 91.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw020.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw020 "Wse Rfe SyncdRW Wse Rfe SyncdRW" {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,2 | lwz r1,0(r2) | li r1,2 ; sync | stw r1,0(r2) | sync | stw r1,0(r2) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (x=2 /\ y=2 /\ 0:r1=2 /\ 2:r1=2) Generated assembler _litmus_P3_0_: li 8,2 _litmus_P3_1_: stw 8,0(9) _litmus_P2_0_: lwz 4,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 5,1 _litmus_P2_3_: stw 5,0(9) _litmus_P1_0_: li 7,2 _litmus_P1_1_: stw 7,0(9) _litmus_P0_0_: lwz 4,0(11) _litmus_P0_1_: sync _litmus_P0_2_: li 5,1 _litmus_P0_3_: stw 5,0(9) Test acsdrw020 Allowed Histogram (28 states) 1 :>0:r1=2; 2:r1=1; x=2; y=2; 4275817:>0:r1=2; 2:r1=2; x=1; y=2; 2792235:>0:r1=2; 2:r1=1; x=2; y=1; 4171346:>0:r1=2; 2:r1=2; x=2; y=1; 5282315:>0:r1=1; 2:r1=0; x=2; y=2; 5951732:>0:r1=0; 2:r1=1; x=2; y=2; 1046790:>0:r1=0; 2:r1=0; x=1; y=1; 2766489:>0:r1=1; 2:r1=2; x=1; y=2; 16969498:>0:r1=0; 2:r1=1; x=2; y=1; 2602716:>0:r1=0; 2:r1=2; x=2; y=2; 28279540:>0:r1=2; 2:r1=2; x=1; y=1; 28149762:>0:r1=0; 2:r1=2; x=2; y=1; 7498486:>0:r1=0; 2:r1=0; x=2; y=1; 10380429:>0:r1=2; 2:r1=0; x=1; y=1; 7235757:>0:r1=0; 2:r1=0; x=1; y=2; 9908718:>0:r1=0; 2:r1=2; x=1; y=1; 16300153:>0:r1=2; 2:r1=1; x=1; y=1; 28168425:>0:r1=2; 2:r1=0; x=1; y=2; 11781479:>0:r1=0; 2:r1=2; x=1; y=2; 21498953:>0:r1=0; 2:r1=1; x=1; y=1; 23213192:>0:r1=1; 2:r1=0; x=1; y=1; 15879831:>0:r1=1; 2:r1=0; x=1; y=2; 2815579:>0:r1=0; 2:r1=1; x=1; y=2; 3142476:>0:r1=1; 2:r1=0; x=2; y=1; 12092737:>0:r1=2; 2:r1=0; x=2; y=1; 2678241:>0:r1=2; 2:r1=0; x=2; y=2; 28927619:>0:r1=0; 2:r1=0; x=2; y=2; 16189684:>0:r1=1; 2:r1=2; x=1; y=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 0:r1=2 /\ 2:r1=2) is NOT validated Hash=c0bbd742ae8d7b1814d567c2ea1f747c Cycle=Wse Rfe SyncdRW Wse Rfe SyncdRW Relax acsdrw020 No ACSyncdRW Safe=Wse Time acsdrw020 78.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw021.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw021 "Wse SyncdWW Rfe SyncdRW Wse Rfe SyncdRW" {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,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | sync ; sync | li r3,1 | | li r3,1 ; li r3,1 | stw r3,0(r4) | | stw r3,0(r4) ; stw r3,0(r4) | | | ; exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=2) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 4,1 _litmus_P1_3_: stw 4,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw021 Allowed Histogram (21 states) 689011:>1:r1=1; 3:r1=1; y=2; z=1; 3702950:>1:r1=0; 3:r1=2; y=2; z=2; 335475:>1:r1=1; 3:r1=0; y=2; z=2; 1615707:>1:r1=1; 3:r1=2; y=1; z=2; 4406605:>1:r1=0; 3:r1=1; y=1; z=2; 6782507:>1:r1=0; 3:r1=1; y=2; z=2; 3191520:>1:r1=0; 3:r1=0; y=1; z=1; 27713263:>1:r1=1; 3:r1=0; y=1; z=1; 1086040:>1:r1=1; 3:r1=2; y=2; z=1; 8303472:>1:r1=1; 3:r1=0; y=2; z=1; 16032874:>1:r1=0; 3:r1=0; y=2; z=1; 19891105:>1:r1=0; 3:r1=1; y=2; z=1; 10639668:>1:r1=1; 3:r1=0; y=1; z=2; 17642631:>1:r1=0; 3:r1=2; y=1; z=1; 35328065:>1:r1=0; 3:r1=0; y=1; z=2; 6939530:>1:r1=1; 3:r1=1; y=1; z=1; 31026786:>1:r1=0; 3:r1=1; y=1; z=1; 20283657:>1:r1=0; 3:r1=2; y=1; z=2; 42203666:>1:r1=0; 3:r1=0; y=2; z=2; 32118509:>1:r1=0; 3:r1=2; y=2; z=1; 30066959:>1:r1=1; 3:r1=2; y=1; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=2) is NOT validated Hash=fb7ddaee4aad6bfd6e76ab9096991c97 Cycle=Wse SyncdWW Rfe SyncdRW Wse Rfe SyncdRW Relax acsdrw021 No ACSyncdRW Safe=Wse SyncdWW Time acsdrw021 90.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw022.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw022 "Wse LwSyncdWW Rfe SyncdRW Wse Rfe SyncdRW" {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,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | sync ; lwsync | li r3,1 | | li r3,1 ; li r3,1 | stw r3,0(r4) | | stw r3,0(r4) ; stw r3,0(r4) | | | ; exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=2) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 4,1 _litmus_P1_3_: stw 4,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw022 Allowed Histogram (21 states) 2341014:>1:r1=1; 3:r1=2; y=2; z=1; 2733010:>1:r1=0; 3:r1=0; y=1; z=1; 537186:>1:r1=1; 3:r1=0; y=2; z=2; 1820704:>1:r1=1; 3:r1=2; y=1; z=2; 1431449:>1:r1=1; 3:r1=1; y=2; z=1; 3952641:>1:r1=0; 3:r1=1; y=1; z=2; 13500068:>1:r1=0; 3:r1=0; y=2; z=1; 17156528:>1:r1=0; 3:r1=2; y=1; z=1; 9058152:>1:r1=1; 3:r1=1; y=1; z=1; 12313705:>1:r1=1; 3:r1=0; y=1; z=2; 3211360:>1:r1=0; 3:r1=2; y=2; z=2; 11575607:>1:r1=1; 3:r1=0; y=2; z=1; 29717589:>1:r1=0; 3:r1=2; y=2; z=1; 30135411:>1:r1=1; 3:r1=0; y=1; z=1; 33932570:>1:r1=0; 3:r1=0; y=1; z=2; 28891759:>1:r1=0; 3:r1=1; y=1; z=1; 5984962:>1:r1=0; 3:r1=1; y=2; z=2; 33953641:>1:r1=1; 3:r1=2; y=1; z=1; 40502636:>1:r1=0; 3:r1=0; y=2; z=2; 18594331:>1:r1=0; 3:r1=2; y=1; z=2; 18655677:>1:r1=0; 3:r1=1; y=2; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=2) is NOT validated Hash=61c10b851057fd25b8ca046191cf271c Cycle=Wse LwSyncdWW Rfe SyncdRW Wse Rfe SyncdRW Relax acsdrw022 No ACSyncdRW Safe=Wse LwSyncdWW Time acsdrw022 85.73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw023.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw023 "Wse SyncdWW Wse Rfe SyncdRW" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | | li r3,1 ; li r3,1 | | stw r3,0(r4) ; stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 2:r1=2) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 6,2 _litmus_P1_1_: stw 6,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw023 Allowed Histogram (9 states) 27691772:>2:r1=1; x=2; y=1; 4850716:>2:r1=0; x=1; y=1; 38557725:>2:r1=2; x=1; y=2; 23052328:>2:r1=0; x=2; y=2; 58553554:>2:r1=0; x=2; y=1; 62365712:>2:r1=2; x=1; y=1; 94703598:>2:r1=0; x=1; y=2; 41476206:>2:r1=2; x=2; y=1; 48748389:>2:r1=1; x=1; y=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ y=2 /\ 2:r1=2) is NOT validated Hash=ec683f3e13cc6c2345f0d3fe16dafa14 Cycle=Wse SyncdWW Wse Rfe SyncdRW Relax acsdrw023 No ACSyncdRW Safe=Wse SyncdWW Time acsdrw023 72.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw024.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw024 "Wse SyncdWW Wse SyncdWW Wse Rfe SyncdRW" {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,2 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ; sync | sync | | li r3,1 ; li r3,1 | li r3,1 | | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ z=2 /\ 3:r1=2) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 5,2 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw024 Allowed Histogram (21 states) 5962196:>3:r1=1; x=1; y=2; z=2; 2786936:>3:r1=2; x=2; y=1; z=2; 2815714:>3:r1=1; x=1; y=1; z=2; 1374817:>3:r1=1; x=2; y=2; z=1; 3069685:>3:r1=2; x=1; y=2; z=2; 12817920:>3:r1=0; x=2; y=2; z=1; 927779:>3:r1=0; x=2; y=2; z=2; 23598636:>3:r1=1; x=1; y=1; z=1; 10793413:>3:r1=1; x=2; y=1; z=1; 35624056:>3:r1=0; x=1; y=2; z=2; 1310633:>3:r1=0; x=1; y=1; z=1; 10247805:>3:r1=0; x=1; y=2; z=1; 14248277:>3:r1=2; x=1; y=1; z=1; 40939731:>3:r1=2; x=2; y=1; z=1; 18448148:>3:r1=0; x=2; y=1; z=2; 16544094:>3:r1=1; x=1; y=2; z=1; 33138900:>3:r1=0; x=2; y=1; z=1; 21267156:>3:r1=2; x=1; y=1; z=2; 34163332:>3:r1=0; x=1; y=1; z=2; 27689079:>3:r1=2; x=1; y=2; z=1; 2231693:>3:r1=2; x=2; y=2; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ z=2 /\ 3:r1=2) is NOT validated Hash=130b35e3af196b5cb1d4fcbd6d6d026b Cycle=Wse SyncdWW Wse SyncdWW Wse Rfe SyncdRW Relax acsdrw024 No ACSyncdRW Safe=Wse SyncdWW Time acsdrw024 86.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw025.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw025 "Wse LwSyncdWW Wse SyncdWW Wse Rfe SyncdRW" {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,2 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ; lwsync | sync | | li r3,1 ; li r3,1 | li r3,1 | | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ z=2 /\ 3:r1=2) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 5,2 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw025 Allowed Histogram (21 states) 1324214:>3:r1=0; x=2; y=2; z=2; 9588539:>3:r1=0; x=1; y=2; z=1; 2569123:>3:r1=1; x=1; y=1; z=2; 5337203:>3:r1=1; x=1; y=2; z=2; 20617130:>3:r1=0; x=2; y=1; z=2; 1835925:>3:r1=1; x=2; y=2; z=1; 3124958:>3:r1=2; x=2; y=1; z=2; 15706730:>3:r1=1; x=1; y=2; z=1; 22157006:>3:r1=1; x=1; y=1; z=1; 14548285:>3:r1=0; x=2; y=2; z=1; 31753335:>3:r1=0; x=1; y=1; z=2; 12941334:>3:r1=2; x=1; y=1; z=1; 1175415:>3:r1=0; x=1; y=1; z=1; 45064334:>3:r1=2; x=2; y=1; z=1; 34344207:>3:r1=0; x=2; y=1; z=1; 2651261:>3:r1=2; x=1; y=2; z=2; 19290578:>3:r1=2; x=1; y=1; z=2; 34408659:>3:r1=0; x=1; y=2; z=2; 3034022:>3:r1=2; x=2; y=2; z=1; 26252726:>3:r1=2; x=1; y=2; z=1; 12275016:>3:r1=1; x=2; y=1; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ z=2 /\ 3:r1=2) is NOT validated Hash=330c697b909eda6c721560d939567f1e Cycle=Wse LwSyncdWW Wse SyncdWW Wse Rfe SyncdRW Relax acsdrw025 No ACSyncdRW Safe=Wse SyncdWW LwSyncdWW Time acsdrw025 84.24 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw026.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw026 "Wse SyncdWR Fre SyncdWW Wse Rfe SyncdRW" {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,2 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ; sync | sync | | li r3,1 ; lwz r3,0(r4) | li r3,1 | | stw r3,0(r4) ; | stw r3,0(r4) | | ; exists (y=2 /\ z=2 /\ 0:r3=0 /\ 3:r1=2) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 5,1 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrw026 Allowed Histogram (21 states) 952873:>0:r3=1; 3:r1=0; y=1; z=1; 2966655:>0:r3=1; 3:r1=1; y=1; z=2; 2813797:>0:r3=0; 3:r1=2; y=2; z=1; 8339476:>0:r3=1; 3:r1=0; y=2; z=1; 1874972:>0:r3=0; 3:r1=1; y=2; z=1; 3003656:>0:r3=1; 3:r1=2; y=2; z=2; 2222566:>0:r3=0; 3:r1=0; y=2; z=2; 12924846:>0:r3=0; 3:r1=1; y=1; z=1; 20323319:>0:r3=1; 3:r1=1; y=1; z=1; 10810990:>0:r3=1; 3:r1=2; y=1; z=1; 24993594:>0:r3=1; 3:r1=2; y=2; z=1; 34045989:>0:r3=0; 3:r1=0; y=1; z=1; 5904757:>0:r3=1; 3:r1=1; y=2; z=2; 20018896:>0:r3=1; 3:r1=2; y=1; z=2; 29358561:>0:r3=1; 3:r1=0; y=1; z=2; 15704470:>0:r3=1; 3:r1=1; y=2; z=1; 4371579:>0:r3=0; 3:r1=2; y=1; z=2; 24997818:>0:r3=0; 3:r1=0; y=1; z=2; 15214030:>0:r3=0; 3:r1=0; y=2; z=1; 33641734:>0:r3=1; 3:r1=0; y=2; z=2; 45515422:>0:r3=0; 3:r1=2; y=1; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (y=2 /\ z=2 /\ 0:r3=0 /\ 3:r1=2) is NOT validated Hash=ccbc67f966a73eda84203a203293a8e5 Cycle=Wse SyncdWR Fre SyncdWW Wse Rfe SyncdRW Relax acsdrw026 No ACSyncdRW Safe=Fre Wse SyncdWW SyncdWR Time acsdrw026 87.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw027.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw027 "Wse LwSyncdWW Wse Rfe SyncdRW" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; lwsync | | li r3,1 ; li r3,1 | | stw r3,0(r4) ; stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 2:r1=2) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 6,2 _litmus_P1_1_: stw 6,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw027 Allowed Histogram (9 states) 3537538:>2:r1=0; x=1; y=1; 44644186:>2:r1=1; x=1; y=1; 39217313:>2:r1=1; x=2; y=1; 46035718:>2:r1=0; x=2; y=1; 27538370:>2:r1=0; x=2; y=2; 56040264:>2:r1=2; x=1; y=1; 89193065:>2:r1=0; x=1; y=2; 57135778:>2:r1=2; x=2; y=1; 36657768:>2:r1=2; x=1; y=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ y=2 /\ 2:r1=2) is NOT validated Hash=9cbab788f1665946b25781874fe1049e Cycle=Wse LwSyncdWW Wse Rfe SyncdRW Relax acsdrw027 No ACSyncdRW Safe=Wse LwSyncdWW Time acsdrw027 71.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw028.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw028 "Wse SyncdWW Wse LwSyncdWW Wse Rfe SyncdRW" {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,2 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ; sync | lwsync | | li r3,1 ; li r3,1 | li r3,1 | | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ z=2 /\ 3:r1=2) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 5,2 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw028 Allowed Histogram (21 states) 2991373:>3:r1=1; x=1; y=1; z=2; 962426:>3:r1=0; x=1; y=1; z=1; 2022803:>3:r1=1; x=2; y=2; z=1; 2960329:>3:r1=2; x=2; y=2; z=1; 12510012:>3:r1=1; x=2; y=1; z=1; 30430387:>3:r1=0; x=2; y=1; z=1; 33841499:>3:r1=0; x=1; y=2; z=2; 1195791:>3:r1=0; x=2; y=2; z=2; 23046079:>3:r1=1; x=1; y=1; z=1; 8147320:>3:r1=0; x=1; y=2; z=1; 31209742:>3:r1=0; x=1; y=1; z=2; 20082271:>3:r1=2; x=1; y=1; z=2; 14517889:>3:r1=0; x=2; y=2; z=1; 4488707:>3:r1=2; x=1; y=2; z=2; 20515049:>3:r1=1; x=1; y=2; z=1; 9796090:>3:r1=1; x=1; y=2; z=2; 12408756:>3:r1=2; x=1; y=1; z=1; 17029349:>3:r1=0; x=2; y=1; z=2; 36817707:>3:r1=2; x=2; y=1; z=1; 32475747:>3:r1=2; x=1; y=2; z=1; 2550674:>3:r1=2; x=2; y=1; z=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ z=2 /\ 3:r1=2) is NOT validated Hash=ce2fc055a61edaee8aa3bbd23e3be87c Cycle=Wse SyncdWW Wse LwSyncdWW Wse Rfe SyncdRW Relax acsdrw028 No ACSyncdRW Safe=Wse SyncdWW LwSyncdWW Time acsdrw028 87.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw029.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw029 "Wse LwSyncdWW Wse LwSyncdWW Wse Rfe SyncdRW" {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,2 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ; lwsync | lwsync | | li r3,1 ; li r3,1 | li r3,1 | | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ z=2 /\ 3:r1=2) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 5,2 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw029 Allowed Histogram (21 states) 861751:>3:r1=0; x=1; y=1; z=1; 2847292:>3:r1=1; x=2; y=2; z=1; 4184906:>3:r1=2; x=2; y=2; z=1; 1677161:>3:r1=0; x=2; y=2; z=2; 2788421:>3:r1=2; x=2; y=1; z=2; 11471311:>3:r1=2; x=1; y=1; z=1; 19719517:>3:r1=1; x=1; y=2; z=1; 3950456:>3:r1=2; x=1; y=2; z=2; 2747224:>3:r1=1; x=1; y=1; z=2; 14208938:>3:r1=1; x=2; y=1; z=1; 17968898:>3:r1=2; x=1; y=1; z=2; 9004000:>3:r1=1; x=1; y=2; z=2; 7575979:>3:r1=0; x=1; y=2; z=1; 39786704:>3:r1=2; x=2; y=1; z=1; 31634116:>3:r1=2; x=1; y=2; z=1; 18834318:>3:r1=0; x=2; y=1; z=2; 31548086:>3:r1=0; x=2; y=1; z=1; 21809562:>3:r1=1; x=1; y=1; z=1; 32162657:>3:r1=0; x=1; y=2; z=2; 28919882:>3:r1=0; x=1; y=1; z=2; 16298821:>3:r1=0; x=2; y=2; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ z=2 /\ 3:r1=2) is NOT validated Hash=5c77813fcdc57dd97091ff7dc2189013 Cycle=Wse LwSyncdWW Wse LwSyncdWW Wse Rfe SyncdRW Relax acsdrw029 No ACSyncdRW Safe=Wse LwSyncdWW Time acsdrw029 86.62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw030.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw030 "Wse SyncdWR Fre LwSyncdWW Wse Rfe SyncdRW" {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,2 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ; sync | lwsync | | li r3,1 ; lwz r3,0(r4) | li r3,1 | | stw r3,0(r4) ; | stw r3,0(r4) | | ; exists (y=2 /\ z=2 /\ 0:r3=0 /\ 3:r1=2) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 5,1 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 4,1 _litmus_P1_4_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrw030 Allowed Histogram (21 states) 687123:>0:r3=1; 3:r1=0; y=1; z=1; 2645855:>0:r3=0; 3:r1=0; y=2; z=2; 16706287:>0:r3=0; 3:r1=0; y=2; z=1; 19529066:>0:r3=1; 3:r1=1; y=1; z=1; 2767934:>0:r3=0; 3:r1=1; y=2; z=1; 9984645:>0:r3=1; 3:r1=1; y=2; z=2; 3910036:>0:r3=0; 3:r1=2; y=1; z=2; 22776739:>0:r3=0; 3:r1=0; y=1; z=2; 14237238:>0:r3=0; 3:r1=1; y=1; z=1; 31329442:>0:r3=0; 3:r1=0; y=1; z=1; 9910184:>0:r3=1; 3:r1=2; y=1; z=1; 19683967:>0:r3=1; 3:r1=1; y=2; z=1; 3738463:>0:r3=0; 3:r1=2; y=2; z=1; 3020998:>0:r3=1; 3:r1=1; y=1; z=2; 29887877:>0:r3=1; 3:r1=2; y=2; z=1; 27013341:>0:r3=1; 3:r1=0; y=1; z=2; 6573392:>0:r3=1; 3:r1=0; y=2; z=1; 18912605:>0:r3=1; 3:r1=2; y=1; z=2; 31355828:>0:r3=1; 3:r1=0; y=2; z=2; 4477513:>0:r3=1; 3:r1=2; y=2; z=2; 40851467:>0:r3=0; 3:r1=2; y=1; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (y=2 /\ z=2 /\ 0:r3=0 /\ 3:r1=2) is NOT validated Hash=51d5a6afa9753758299771086decdacf Cycle=Wse SyncdWR Fre LwSyncdWW Wse Rfe SyncdRW Relax acsdrw030 No ACSyncdRW Safe=Fre Wse SyncdWR LwSyncdWW Time acsdrw030 85.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw031.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw031 "Wse SyncdWR Fre Rfe SyncdRW" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | | li r3,1 ; lwz r3,0(r4) | | stw r3,0(r4) ; exists (y=2 /\ 0:r3=0 /\ 2:r1=1) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 6,1 _litmus_P1_1_: stw 6,0(9) _litmus_P0_0_: li 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrw031 Allowed Histogram (7 states) 2331222:>0:r3=1; 2:r1=0; y=1; 81220596:>0:r3=1; 2:r1=0; y=2; 38901629:>0:r3=1; 2:r1=1; y=2; 38531830:>0:r3=0; 2:r1=0; y=2; 98053581:>0:r3=1; 2:r1=1; y=1; 87094501:>0:r3=0; 2:r1=0; y=1; 53866641:>0:r3=0; 2:r1=1; y=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (y=2 /\ 0:r3=0 /\ 2:r1=1) is NOT validated Hash=2a0d02101c6e625540b9687c7722733e Cycle=Wse SyncdWR Fre Rfe SyncdRW Relax acsdrw031 No ACSyncdRW Safe=Fre Wse SyncdWR Time acsdrw031 72.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw032.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw032 "Wse SyncdWW Wse SyncdWR Fre Rfe SyncdRW" {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,2 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ; sync | sync | | li r3,1 ; li r3,1 | lwz r3,0(r4) | | stw r3,0(r4) ; stw r3,0(r4) | | | ; exists (x=2 /\ z=2 /\ 1:r3=0 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,1 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw032 Allowed Histogram (15 states) 653276:>1:r3=1; 3:r1=0; x=1; z=1; 2832733:>1:r3=1; 3:r1=1; x=2; z=2; 26645753:>1:r3=1; 3:r1=0; x=2; z=1; 4833616:>1:r3=0; 3:r1=1; x=2; z=1; 4341637:>1:r3=0; 3:r1=1; x=1; z=2; 27128309:>1:r3=1; 3:r1=0; x=1; z=2; 27365498:>1:r3=0; 3:r1=0; x=1; z=1; 21053595:>1:r3=0; 3:r1=0; x=2; z=1; 28494863:>1:r3=0; 3:r1=1; x=1; z=1; 32953964:>1:r3=1; 3:r1=1; x=1; z=1; 2099775:>1:r3=0; 3:r1=0; x=2; z=2; 17606389:>1:r3=1; 3:r1=0; x=2; z=2; 49056773:>1:r3=1; 3:r1=1; x=2; z=1; 51855406:>1:r3=0; 3:r1=0; x=1; z=2; 23078413:>1:r3=1; 3:r1=1; x=1; z=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ z=2 /\ 1:r3=0 /\ 3:r1=1) is NOT validated Hash=4c866a10348f9f38c9757434df1c5cb0 Cycle=Wse SyncdWW Wse SyncdWR Fre Rfe SyncdRW Relax acsdrw032 No ACSyncdRW Safe=Fre Wse SyncdWW SyncdWR Time acsdrw032 85.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw033.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw033 "Wse LwSyncdWW Wse SyncdWR Fre Rfe SyncdRW" {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,2 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ; lwsync | sync | | li r3,1 ; li r3,1 | lwz r3,0(r4) | | stw r3,0(r4) ; stw r3,0(r4) | | | ; exists (x=2 /\ z=2 /\ 1:r3=0 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,1 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw033 Allowed Histogram (15 states) 4077428:>1:r3=0; 3:r1=1; x=1; z=2; 517775:>1:r3=1; 3:r1=0; x=1; z=1; 2860404:>1:r3=0; 3:r1=0; x=2; z=2; 27141745:>1:r3=1; 3:r1=0; x=2; z=1; 3260355:>1:r3=1; 3:r1=1; x=2; z=2; 29999571:>1:r3=1; 3:r1=1; x=1; z=1; 23717367:>1:r3=0; 3:r1=0; x=2; z=1; 27357159:>1:r3=0; 3:r1=1; x=1; z=1; 19730617:>1:r3=1; 3:r1=0; x=2; z=2; 49837870:>1:r3=0; 3:r1=0; x=1; z=2; 5961245:>1:r3=0; 3:r1=1; x=2; z=1; 20892177:>1:r3=1; 3:r1=1; x=1; z=2; 24871050:>1:r3=1; 3:r1=0; x=1; z=2; 25491715:>1:r3=0; 3:r1=0; x=1; z=1; 54283522:>1:r3=1; 3:r1=1; x=2; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ z=2 /\ 1:r3=0 /\ 3:r1=1) is NOT validated Hash=bb2441029675e3632bdb718971387ab7 Cycle=Wse LwSyncdWW Wse SyncdWR Fre Rfe SyncdRW Relax acsdrw033 No ACSyncdRW Safe=Fre Wse SyncdWR LwSyncdWW Time acsdrw033 84.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw034.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw034 "Wse SyncdWR Fre SyncdWR Fre Rfe SyncdRW" {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,2 | li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ; sync | sync | | li r3,1 ; lwz r3,0(r4) | lwz r3,0(r4) | | stw r3,0(r4) ; exists (z=2 /\ 0:r3=0 /\ 1:r3=0 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,1 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrw034 Allowed Histogram (15 states) 4333252:>0:r3=1; 1:r3=0; 3:r1=1; z=2; 4548846:>0:r3=0; 1:r3=0; 3:r1=0; z=2; 346292:>0:r3=1; 1:r3=1; 3:r1=0; z=1; 23285398:>0:r3=0; 1:r3=1; 3:r1=0; z=2; 4573024:>0:r3=0; 1:r3=1; 3:r1=1; z=2; 6064900:>0:r3=0; 1:r3=0; 3:r1=1; z=1; 22315419:>0:r3=1; 1:r3=1; 3:r1=0; z=2; 27392439:>0:r3=0; 1:r3=1; 3:r1=0; z=1; 25473770:>0:r3=1; 1:r3=1; 3:r1=1; z=1; 26288148:>0:r3=1; 1:r3=0; 3:r1=1; z=1; 54525405:>0:r3=0; 1:r3=1; 3:r1=1; z=1; 22177220:>0:r3=1; 1:r3=1; 3:r1=1; z=2; 50215445:>0:r3=1; 1:r3=0; 3:r1=0; z=2; 23363955:>0:r3=1; 1:r3=0; 3:r1=0; z=1; 25096487:>0:r3=0; 1:r3=0; 3:r1=0; z=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (z=2 /\ 0:r3=0 /\ 1:r3=0 /\ 3:r1=1) is NOT validated Hash=d166d511b295e706795c3a2985e0afcf Cycle=Wse SyncdWR Fre SyncdWR Fre Rfe SyncdRW Relax acsdrw034 No ACSyncdRW Safe=Fre Wse SyncdWR Time acsdrw034 80.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw035.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw035 "Wse SyncdWR Fre SyncsWR Fre Rfe SyncdRW" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | sync ; sync | sync | | li r3,1 ; lwz r3,0(r4) | lwz r3,0(r2) | | stw r3,0(r4) ; exists (x=2 /\ y=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 11,1 _litmus_P1_1_: stw 11,0(9) _litmus_P1_2_: sync _litmus_P1_3_: lwz 5,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrw035 Allowed Histogram (51 states) 1 :>0:r3=0; 1:r3=2; 3:r1=1; x=2; y=2; 1 :>0:r3=0; 1:r3=1; 3:r1=2; x=1; y=2; 2 :>0:r3=0; 1:r3=1; 3:r1=1; x=1; y=2; 6 :>0:r3=1; 1:r3=2; 3:r1=2; x=2; y=2; 44 :>0:r3=2; 1:r3=1; 3:r1=1; x=1; y=2; 30 :>0:r3=1; 1:r3=1; 3:r1=2; x=2; y=2; 11889 :>0:r3=1; 1:r3=2; 3:r1=0; x=2; y=1; 51817 :>0:r3=2; 1:r3=2; 3:r1=0; x=2; y=1; 2829 :>0:r3=1; 1:r3=2; 3:r1=1; x=2; y=2; 249126:>0:r3=1; 1:r3=1; 3:r1=0; x=1; y=1; 1027913:>0:r3=1; 1:r3=1; 3:r1=0; x=2; y=1; 1104987:>0:r3=2; 1:r3=2; 3:r1=2; x=2; y=2; 152711:>0:r3=1; 1:r3=2; 3:r1=0; x=2; y=2; 130803:>0:r3=2; 1:r3=2; 3:r1=1; x=2; y=1; 134124:>0:r3=0; 1:r3=2; 3:r1=1; x=2; y=1; 186986:>0:r3=2; 1:r3=2; 3:r1=1; x=2; y=2; 64441 :>0:r3=1; 1:r3=2; 3:r1=1; x=2; y=1; 2919147:>0:r3=2; 1:r3=2; 3:r1=0; x=2; y=2; 7394171:>0:r3=0; 1:r3=1; 3:r1=1; x=2; y=1; 2097639:>0:r3=0; 1:r3=2; 3:r1=2; x=2; y=1; 4570565:>0:r3=1; 1:r3=1; 3:r1=1; x=1; y=2; 7583305:>0:r3=0; 1:r3=1; 3:r1=2; x=2; y=1; 15683444:>0:r3=1; 1:r3=1; 3:r1=2; x=1; y=2; 18764484:>0:r3=1; 1:r3=1; 3:r1=0; x=1; y=2; 88355 :>0:r3=1; 1:r3=2; 3:r1=2; x=2; y=1; 1345904:>0:r3=2; 1:r3=1; 3:r1=0; x=1; y=1; 9959603:>0:r3=1; 1:r3=1; 3:r1=2; x=2; y=1; 4714903:>0:r3=1; 1:r3=1; 3:r1=2; x=1; y=1; 3006965:>0:r3=0; 1:r3=2; 3:r1=0; x=2; y=1; 10048235:>0:r3=2; 1:r3=1; 3:r1=1; x=1; y=1; 1239739:>0:r3=0; 1:r3=2; 3:r1=0; x=2; y=2; 2922363:>0:r3=2; 1:r3=2; 3:r1=2; x=2; y=1; 3662747:>0:r3=1; 1:r3=1; 3:r1=1; x=2; y=2; 9333412:>0:r3=0; 1:r3=1; 3:r1=2; x=1; y=1; 128393:>0:r3=2; 1:r3=1; 3:r1=0; x=2; y=1; 4813663:>0:r3=2; 1:r3=1; 3:r1=2; x=1; y=2; 4914777:>0:r3=2; 1:r3=1; 3:r1=2; x=2; y=2; 14564644:>0:r3=2; 1:r3=1; 3:r1=0; x=1; y=2; 10611189:>0:r3=0; 1:r3=1; 3:r1=1; x=1; y=1; 4119339:>0:r3=2; 1:r3=1; 3:r1=1; x=2; y=1; 22725011:>0:r3=2; 1:r3=1; 3:r1=2; x=1; y=1; 7182172:>0:r3=0; 1:r3=1; 3:r1=0; x=1; y=2; 21715946:>0:r3=0; 1:r3=1; 3:r1=0; x=1; y=1; 4845287:>0:r3=0; 1:r3=1; 3:r1=0; x=2; y=2; 19098415:>0:r3=2; 1:r3=1; 3:r1=2; x=2; y=1; 15275867:>0:r3=2; 1:r3=1; 3:r1=1; x=2; y=2; 10879669:>0:r3=1; 1:r3=1; 3:r1=0; x=2; y=2; 20826430:>0:r3=1; 1:r3=1; 3:r1=1; x=2; y=1; 19671567:>0:r3=1; 1:r3=1; 3:r1=1; x=1; y=1; 16553180:>0:r3=0; 1:r3=1; 3:r1=0; x=2; y=1; 13621760:>0:r3=2; 1:r3=1; 3:r1=0; x=2; y=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2) is NOT validated Hash=279ba973f0f471bb80bd3fc72999b1a5 Cycle=Wse SyncdWR Fre SyncsWR Fre Rfe SyncdRW Relax acsdrw035 No ACSyncdRW Safe=Fre Wse SyncsWR SyncdWR Time acsdrw035 87.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw036.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw036 "Wse SyncdWW Rfe SyncdRW" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;} P0 | P1 ; li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync ; sync | li r3,1 ; li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | ; exists (y=2 /\ 1:r1=1) Generated assembler _litmus_P1_0_: lwz 4,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 5,1 _litmus_P1_3_: stw 5,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw036 Allowed Histogram (3 states) 125802679:>1:r1=0; y=1; 220013862:>1:r1=1; y=1; 294183459:>1:r1=0; y=2; No Witnesses Positive: 0, Negative: 640000000 Condition exists (y=2 /\ 1:r1=1) is NOT validated Hash=a75535e637fc82ddef1b5a25aef99060 Cycle=Wse SyncdWW Rfe SyncdRW Relax acsdrw036 No ACSyncdRW Safe=Wse SyncdWW Time acsdrw036 76.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw037.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw037 "Wse SyncdWW Rfe SyncdRW Wse SyncdWW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | sync ; sync | li r3,1 | sync | li r3,1 ; li r3,1 | stw r3,0(r4) | li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (a=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 6,2 _litmus_P2_1_: stw 6,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 5,1 _litmus_P2_4_: stw 5,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 4,1 _litmus_P1_3_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw037 Allowed Histogram (15 states) 366849:>1:r1=0; 3:r1=1; a=2; y=2; 263315:>1:r1=1; 3:r1=1; a=2; y=1; 353830:>1:r1=1; 3:r1=1; a=1; y=2; 12389322:>1:r1=1; 3:r1=0; a=2; y=1; 592007:>1:r1=1; 3:r1=0; a=2; y=2; 11529359:>1:r1=1; 3:r1=0; a=1; y=2; 21061123:>1:r1=1; 3:r1=1; a=1; y=1; 9307446:>1:r1=0; 3:r1=0; a=1; y=1; 9110601:>1:r1=0; 3:r1=1; a=2; y=1; 50688698:>1:r1=0; 3:r1=0; a=1; y=2; 10416185:>1:r1=0; 3:r1=1; a=1; y=2; 38507150:>1:r1=0; 3:r1=1; a=1; y=1; 53328929:>1:r1=0; 3:r1=0; a=2; y=1; 41925643:>1:r1=1; 3:r1=0; a=1; y=1; 60159543:>1:r1=0; 3:r1=0; a=2; y=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated Hash=5a0d89fb848d7bf4d7b55d9a11d29022 Cycle=Wse SyncdWW Rfe SyncdRW Wse SyncdWW Rfe SyncdRW Relax acsdrw037 No ACSyncdRW Safe=Wse SyncdWW Time acsdrw037 91.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw038.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw038 "Wse LwSyncdWW Rfe SyncdRW Wse SyncdWW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | sync ; lwsync | li r3,1 | sync | li r3,1 ; li r3,1 | stw r3,0(r4) | li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (a=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 6,2 _litmus_P2_1_: stw 6,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 5,1 _litmus_P2_4_: stw 5,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 4,1 _litmus_P1_3_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw038 Allowed Histogram (15 states) 279181:>1:r1=1; 3:r1=1; a=2; y=1; 652671:>1:r1=1; 3:r1=1; a=1; y=2; 853899:>1:r1=1; 3:r1=0; a=2; y=2; 17010376:>1:r1=1; 3:r1=0; a=1; y=2; 312571:>1:r1=0; 3:r1=1; a=2; y=2; 8457646:>1:r1=0; 3:r1=0; a=1; y=1; 45747125:>1:r1=0; 3:r1=0; a=1; y=2; 24498256:>1:r1=1; 3:r1=1; a=1; y=1; 56601851:>1:r1=0; 3:r1=0; a=2; y=2; 14522975:>1:r1=1; 3:r1=0; a=2; y=1; 8096684:>1:r1=0; 3:r1=1; a=2; y=1; 9666083:>1:r1=0; 3:r1=1; a=1; y=2; 51023810:>1:r1=0; 3:r1=0; a=2; y=1; 46243786:>1:r1=1; 3:r1=0; a=1; y=1; 36033086:>1:r1=0; 3:r1=1; a=1; y=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated Hash=72549319ac048ba7c2ca3bfa946abf41 Cycle=Wse LwSyncdWW Rfe SyncdRW Wse SyncdWW Rfe SyncdRW Relax acsdrw038 No ACSyncdRW Safe=Wse SyncdWW LwSyncdWW Time acsdrw038 90.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw039.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw039 "Wse SyncdWW Wse SyncdWW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | sync | li r3,1 ; li r3,1 | li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ z=2 /\ 2:r1=1) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw039 Allowed Histogram (7 states) 12598192:>2:r1=1; x=1; z=2; 18585568:>2:r1=0; x=1; z=1; 26885871:>2:r1=0; x=2; z=2; 10471924:>2:r1=1; x=2; z=1; 127896545:>2:r1=0; x=1; z=2; 87806942:>2:r1=1; x=1; z=1; 115754958:>2:r1=0; x=2; z=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ z=2 /\ 2:r1=1) is NOT validated Hash=a39ae056f0cf08da6c05c2d650e01d9f Cycle=Wse SyncdWW Wse SyncdWW Rfe SyncdRW Relax acsdrw039 No ACSyncdRW Safe=Wse SyncdWW Time acsdrw039 77.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw040.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw040 "Wse LwSyncdWW Wse SyncdWW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; lwsync | sync | li r3,1 ; li r3,1 | li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ z=2 /\ 2:r1=1) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw040 Allowed Histogram (7 states) 15439059:>2:r1=0; x=1; z=1; 14219301:>2:r1=1; x=2; z=1; 12594539:>2:r1=1; x=1; z=2; 30603119:>2:r1=0; x=2; z=2; 121952288:>2:r1=0; x=1; z=2; 81988804:>2:r1=1; x=1; z=1; 123202890:>2:r1=0; x=2; z=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ z=2 /\ 2:r1=1) is NOT validated Hash=de5c4b1fb13eb35e1bba660019ee2456 Cycle=Wse LwSyncdWW Wse SyncdWW Rfe SyncdRW Relax acsdrw040 No ACSyncdRW Safe=Wse SyncdWW LwSyncdWW Time acsdrw040 74.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw041.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw041 "Wse SyncdWR Fre SyncdWW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | sync | li r3,1 ; lwz r3,0(r4) | li r3,1 | stw r3,0(r4) ; | stw r3,0(r4) | ; exists (z=2 /\ 0:r3=0 /\ 2:r1=1) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: li 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrw041 Allowed Histogram (7 states) 11350825:>0:r3=1; 2:r1=0; z=1; 78066780:>0:r3=1; 2:r1=1; z=1; 15899813:>0:r3=0; 2:r1=1; z=1; 113511956:>0:r3=1; 2:r1=0; z=2; 41156444:>0:r3=0; 2:r1=0; z=2; 127322111:>0:r3=0; 2:r1=0; z=1; 12692071:>0:r3=1; 2:r1=1; z=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (z=2 /\ 0:r3=0 /\ 2:r1=1) is NOT validated Hash=51bb1c1d348678192da6af4217c54c56 Cycle=Wse SyncdWR Fre SyncdWW Rfe SyncdRW Relax acsdrw041 No ACSyncdRW Safe=Fre Wse SyncdWW SyncdWR Time acsdrw041 75.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw042.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw042 "Wse SyncdWR Fre SyncsWW Rfe SyncdRW" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | sync | li r3,1 ; lwz r3,0(r4) | li r3,2 | stw r3,0(r4) ; | stw r3,0(r2) | ; exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 5,1 _litmus_P1_1_: stw 5,0(9) _litmus_P1_2_: sync _litmus_P1_3_: li 11,2 _litmus_P1_4_: stw 11,0(9) _litmus_P0_0_: li 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrw042 Allowed Histogram (15 states) 481693:>0:r3=1; 2:r1=0; x=2; y=1; 3406832:>0:r3=1; 2:r1=2; x=2; y=1; 2068904:>0:r3=1; 2:r1=1; x=2; y=1; 125447:>0:r3=1; 2:r1=1; x=2; y=2; 3918663:>0:r3=2; 2:r1=1; x=2; y=1; 17904048:>0:r3=1; 2:r1=0; x=2; y=2; 6491194:>0:r3=2; 2:r1=1; x=2; y=2; 763440:>0:r3=2; 2:r1=0; x=2; y=1; 17197536:>0:r3=0; 2:r1=1; x=2; y=1; 86182943:>0:r3=0; 2:r1=0; x=2; y=1; 29744631:>0:r3=2; 2:r1=2; x=2; y=2; 42113738:>0:r3=0; 2:r1=0; x=2; y=2; 91298051:>0:r3=2; 2:r1=2; x=2; y=1; 61007674:>0:r3=2; 2:r1=0; x=2; y=2; 37295206:>0:r3=0; 2:r1=2; x=2; y=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated Hash=db85f1985049d6628b5050d1b91d5bfe Cycle=Wse SyncdWR Fre SyncsWW Rfe SyncdRW Relax acsdrw042 No ACSyncdRW Safe=Fre Wse SyncsWW SyncdWR Time acsdrw042 77.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw043.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw043 "Wse SyncdWR Fre LwSyncsWW Rfe SyncdRW" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | lwsync | li r3,1 ; lwz r3,0(r4) | li r3,2 | stw r3,0(r4) ; | stw r3,0(r2) | ; exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 5,1 _litmus_P1_1_: stw 5,0(9) _litmus_P1_2_: lwsync _litmus_P1_3_: li 11,2 _litmus_P1_4_: stw 11,0(9) _litmus_P0_0_: li 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrw043 Allowed Histogram (15 states) 11597 :>0:r3=1; 2:r1=1; x=2; y=2; 174954:>0:r3=1; 2:r1=0; x=2; y=1; 1487661:>0:r3=2; 2:r1=0; x=2; y=1; 714802:>0:r3=1; 2:r1=2; x=2; y=1; 392044:>0:r3=1; 2:r1=1; x=2; y=1; 1598554:>0:r3=2; 2:r1=1; x=2; y=2; 2185048:>0:r3=2; 2:r1=1; x=2; y=1; 6097310:>0:r3=1; 2:r1=0; x=2; y=2; 6275646:>0:r3=0; 2:r1=1; x=2; y=1; 37636009:>0:r3=2; 2:r1=2; x=2; y=2; 86475257:>0:r3=0; 2:r1=0; x=2; y=1; 72675370:>0:r3=2; 2:r1=0; x=2; y=2; 40982001:>0:r3=0; 2:r1=0; x=2; y=2; 49603058:>0:r3=0; 2:r1=2; x=2; y=1; 93690689:>0:r3=2; 2:r1=2; x=2; y=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ y=2 /\ 0:r3=0 /\ 2:r1=2) is NOT validated Hash=7eb6081d4bd3f4ea6e2785c5b803c662 Cycle=Wse SyncdWR Fre LwSyncsWW Rfe SyncdRW Relax acsdrw043 No ACSyncdRW Safe=Fre Wse SyncdWR LwSyncsWW Time acsdrw043 78.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw044.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw044 "Wse LwSyncdWW Rfe SyncdRW" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;} P0 | P1 ; li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync ; lwsync | li r3,1 ; li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | ; exists (y=2 /\ 1:r1=1) Generated assembler _litmus_P1_0_: lwz 4,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 5,1 _litmus_P1_3_: stw 5,0(9) _litmus_P0_0_: li 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test acsdrw044 Allowed Histogram (3 states) 294372918:>1:r1=0; y=2; 67710337:>1:r1=0; y=1; 277916745:>1:r1=1; y=1; No Witnesses Positive: 0, Negative: 640000000 Condition exists (y=2 /\ 1:r1=1) is NOT validated Hash=5ec80fde9a34ba15dc4e9d03c1de028f Cycle=Wse LwSyncdWW Rfe SyncdRW Relax acsdrw044 No ACSyncdRW Safe=Wse LwSyncdWW Time acsdrw044 83.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw045.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw045 "Wse LwSyncdWW Rfe SyncdRW Wse LwSyncdWW Rfe SyncdRW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | sync ; lwsync | li r3,1 | lwsync | li r3,1 ; li r3,1 | stw r3,0(r4) | li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (a=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1) Generated assembler _litmus_P3_0_: lwz 4,0(11) _litmus_P3_1_: sync _litmus_P3_2_: li 5,1 _litmus_P3_3_: stw 5,0(9) _litmus_P2_0_: li 6,2 _litmus_P2_1_: stw 6,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 5,1 _litmus_P2_4_: stw 5,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 4,1 _litmus_P1_3_: stw 4,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw045 Allowed Histogram (15 states) 515206:>1:r1=0; 3:r1=1; a=2; y=2; 773785:>1:r1=1; 3:r1=1; a=1; y=2; 761144:>1:r1=1; 3:r1=0; a=2; y=2; 6648829:>1:r1=0; 3:r1=0; a=1; y=1; 43769733:>1:r1=0; 3:r1=0; a=1; y=2; 39707648:>1:r1=0; 3:r1=1; a=1; y=1; 42629184:>1:r1=1; 3:r1=0; a=1; y=1; 44991945:>1:r1=0; 3:r1=0; a=2; y=1; 13886556:>1:r1=0; 3:r1=1; a=2; y=1; 15446676:>1:r1=1; 3:r1=0; a=1; y=2; 54507064:>1:r1=0; 3:r1=0; a=2; y=2; 788655:>1:r1=1; 3:r1=1; a=2; y=1; 13621577:>1:r1=1; 3:r1=0; a=2; y=1; 30227040:>1:r1=1; 3:r1=1; a=1; y=1; 11724958:>1:r1=0; 3:r1=1; a=1; y=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (a=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated Hash=fcfd9676e9266b92575e14bee8d5ca93 Cycle=Wse LwSyncdWW Rfe SyncdRW Wse LwSyncdWW Rfe SyncdRW Relax acsdrw045 No ACSyncdRW Safe=Wse LwSyncdWW Time acsdrw045 92.08 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw046.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw046 "Wse SyncdWW Wse LwSyncdWW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | lwsync | li r3,1 ; li r3,1 | li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ z=2 /\ 2:r1=1) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw046 Allowed Histogram (7 states) 11263886:>2:r1=0; x=1; z=1; 14085010:>2:r1=1; x=2; z=1; 26270452:>2:r1=0; x=2; z=2; 98540626:>2:r1=1; x=1; z=1; 111851394:>2:r1=0; x=2; z=1; 117079387:>2:r1=0; x=1; z=2; 20909245:>2:r1=1; x=1; z=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ z=2 /\ 2:r1=1) is NOT validated Hash=f58749595e042cfacc57f69fb87c8ef5 Cycle=Wse SyncdWW Wse LwSyncdWW Rfe SyncdRW Relax acsdrw046 No ACSyncdRW Safe=Wse SyncdWW LwSyncdWW Time acsdrw046 78.61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw047.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw047 "Wse LwSyncdWW Wse LwSyncdWW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; lwsync | lwsync | li r3,1 ; li r3,1 | li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ z=2 /\ 2:r1=1) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test acsdrw047 Allowed Histogram (7 states) 21031927:>2:r1=1; x=1; z=2; 29474068:>2:r1=0; x=2; z=2; 9183894:>2:r1=0; x=1; z=1; 18666897:>2:r1=1; x=2; z=1; 118875817:>2:r1=0; x=2; z=1; 110076070:>2:r1=0; x=1; z=2; 92691327:>2:r1=1; x=1; z=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ z=2 /\ 2:r1=1) is NOT validated Hash=4c32079a1bc4ea1385655374f6bf7076 Cycle=Wse LwSyncdWW Wse LwSyncdWW Rfe SyncdRW Relax acsdrw047 No ACSyncdRW Safe=Wse LwSyncdWW Time acsdrw047 74.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrw048.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrw048 "Wse SyncdWR Fre LwSyncdWW Rfe SyncdRW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | lwsync | li r3,1 ; lwz r3,0(r4) | li r3,1 | stw r3,0(r4) ; | stw r3,0(r4) | ; exists (z=2 /\ 0:r3=0 /\ 2:r1=1) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 4,1 _litmus_P2_3_: stw 4,0(9) _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: li 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrw048 Allowed Histogram (7 states) 6924177:>0:r3=1; 2:r1=0; z=1; 21080729:>0:r3=1; 2:r1=1; z=2; 39703193:>0:r3=0; 2:r1=0; z=2; 102669244:>0:r3=1; 2:r1=0; z=2; 121929185:>0:r3=0; 2:r1=0; z=1; 20426707:>0:r3=0; 2:r1=1; z=1; 87266765:>0:r3=1; 2:r1=1; z=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (z=2 /\ 0:r3=0 /\ 2:r1=1) is NOT validated Hash=1f48972b248be819c378fce351dab380 Cycle=Wse SyncdWR Fre LwSyncdWW Rfe SyncdRW Relax acsdrw048 No ACSyncdRW Safe=Fre Wse SyncdWR LwSyncdWW Time acsdrw048 77.05 $Revision: 3163 $ Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 2000 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 20000 #endif #ifndef N_EXE #define N_EXE (32 < N ? 1 : 32 / N) #endif /* gcc options: -Wall -std=gnu99 -O -pthread */ /* barrier: user */ /* tread start/join: changing */ /* memory: indirect */ /* safer: false */ /* preload: true */ /* para: self */ /* changes: false */ /* speedcheck: false */ /* proc used: 32 */ GCCOPTS="-Wall -std=gnu99 -O -pthread" LITMUSOPTS= Tue Dec 22 19:47:11 GMT 2009