Tue Dec 22 17:59:42 GMT 2009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr000.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr000 "Fre SyncdWW Wse SyncdWW Wse Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,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,1 _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 acsdrr000 Allowed Histogram (21 states) 1003116:>3:r1=0; 3:r3=1; x=1; y=1; 3711741:>3:r1=1; 3:r3=0; x=1; y=1; 1310500:>3:r1=1; 3:r3=1; x=2; y=2; 11714362:>3:r1=0; 3:r3=1; x=2; y=2; 12026904:>3:r1=2; 3:r3=1; x=1; y=1; 4065801:>3:r1=2; 3:r3=0; x=1; y=2; 23799040:>3:r1=1; 3:r3=1; x=1; y=1; 7924368:>3:r1=0; 3:r3=1; x=1; y=2; 6885259:>3:r1=1; 3:r3=0; x=1; y=2; 1133527:>3:r1=0; 3:r3=0; x=2; y=2; 2277231:>3:r1=2; 3:r3=1; x=2; y=2; 11014640:>3:r1=1; 3:r3=1; x=2; y=1; 3718404:>3:r1=2; 3:r3=0; x=2; y=1; 20595170:>3:r1=0; 3:r3=0; x=2; y=1; 14661443:>3:r1=1; 3:r3=1; x=1; y=2; 39698962:>3:r1=2; 3:r3=1; x=2; y=1; 34913859:>3:r1=0; 3:r3=0; x=1; y=1; 23783106:>3:r1=2; 3:r3=0; x=1; y=1; 39022292:>3:r1=0; 3:r3=0; x=1; y=2; 27235855:>3:r1=2; 3:r3=1; x=1; y=2; 29504420:>3:r1=0; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=f4668bbb62f5902e918e1363d7dcdd40 Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe SyncdRR Relax acsdrr000 No ACSyncdRR Safe=Fre Wse SyncdWW Time acsdrr000 85.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr001.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr001 "Fre LwSyncdWW Wse SyncdWW Wse Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,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,1 _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 acsdrr001 Allowed Histogram (21 states) 827487:>3:r1=0; 3:r3=1; x=1; y=1; 3421471:>3:r1=1; 3:r3=0; x=1; y=1; 6879494:>3:r1=0; 3:r3=1; x=1; y=2; 3010364:>3:r1=2; 3:r3=1; x=2; y=2; 1738549:>3:r1=1; 3:r3=1; x=2; y=2; 21488279:>3:r1=2; 3:r3=0; x=1; y=1; 10397159:>3:r1=2; 3:r3=1; x=1; y=1; 13165787:>3:r1=1; 3:r3=1; x=2; y=1; 6391712:>3:r1=1; 3:r3=0; x=1; y=2; 13698386:>3:r1=0; 3:r3=1; x=2; y=2; 14360910:>3:r1=1; 3:r3=1; x=1; y=2; 1666476:>3:r1=0; 3:r3=0; x=2; y=2; 38008391:>3:r1=0; 3:r3=0; x=1; y=2; 43810583:>3:r1=2; 3:r3=1; x=2; y=1; 4241569:>3:r1=2; 3:r3=0; x=2; y=1; 23476913:>3:r1=0; 3:r3=0; x=2; y=1; 26189793:>3:r1=2; 3:r3=1; x=1; y=2; 21956529:>3:r1=1; 3:r3=1; x=1; y=1; 29718065:>3:r1=0; 3:r3=1; x=2; y=1; 31736835:>3:r1=0; 3:r3=0; x=1; y=1; 3815248:>3:r1=2; 3:r3=0; x=1; y=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=5f45b9c3dbe15f0ee4cff2cdc24284ec Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe SyncdRR Relax acsdrr001 No ACSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time acsdrr001 86.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr002.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr002 "Fre SyncdWW Wse Rfe SyncdRR" {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) | sync ; sync | | lwz r3,0(r4) ; li r3,1 | | ; stw r3,0(r4) | | ; exists (x=2 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,0(9) _litmus_P1_0_: li 6,2 _litmus_P1_1_: stw 6,0(9) _litmus_P0_0_: li 5,1 _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 acsdrr002 Allowed Histogram (9 states) 2903897:>2:r1=0; 2:r3=1; x=1; 50227597:>2:r1=1; 2:r3=1; x=1; 21658009:>2:r1=1; 2:r3=1; x=2; 40907384:>2:r1=2; 2:r3=1; x=2; 53610870:>2:r1=2; 2:r3=1; x=1; 99090512:>2:r1=0; 2:r3=0; x=1; 53616289:>2:r1=0; 2:r3=1; x=2; 46553956:>2:r1=2; 2:r3=0; x=1; 31431486:>2:r1=0; 2:r3=0; x=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=a261cdec98922b264d129a58ef893bdb Cycle=Fre SyncdWW Wse Rfe SyncdRR Relax acsdrr002 No ACSyncdRR Safe=Fre Wse SyncdWW Time acsdrr002 71.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr003.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr003 "Fre SyncdWR Fre SyncdWW Wse Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,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,1 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrr003 Allowed Histogram (21 states) 644054:>0:r3=1; 3:r1=0; 3:r3=1; y=1; 1874952:>0:r3=0; 3:r1=1; 3:r3=1; y=2; 5510766:>0:r3=1; 3:r1=0; 3:r3=1; y=2; 7270433:>0:r3=1; 3:r1=1; 3:r3=0; y=2; 29785038:>0:r3=0; 3:r1=0; 3:r3=1; y=1; 3810158:>0:r3=1; 3:r1=1; 3:r3=0; y=1; 8264173:>0:r3=1; 3:r1=2; 3:r3=1; y=1; 44827839:>0:r3=0; 3:r1=2; 3:r3=1; y=1; 13709904:>0:r3=1; 3:r1=1; 3:r3=1; y=2; 2910635:>0:r3=0; 3:r1=2; 3:r3=1; y=2; 28564593:>0:r3=1; 3:r1=0; 3:r3=0; y=1; 19878260:>0:r3=1; 3:r1=1; 3:r3=1; y=1; 28700017:>0:r3=0; 3:r1=0; 3:r3=0; y=1; 13597188:>0:r3=0; 3:r1=1; 3:r3=1; y=1; 25298407:>0:r3=1; 3:r1=2; 3:r3=1; y=2; 35798954:>0:r3=1; 3:r1=0; 3:r3=0; y=2; 22114563:>0:r3=1; 3:r1=2; 3:r3=0; y=1; 3018677:>0:r3=0; 3:r1=0; 3:r3=0; y=2; 14140821:>0:r3=0; 3:r1=0; 3:r3=1; y=2; 4207371:>0:r3=1; 3:r1=2; 3:r3=0; y=2; 6073197:>0:r3=0; 3:r1=2; 3:r3=0; y=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=b6db3fc589db44216c30ccbc4b5a9611 Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe SyncdRR Relax acsdrr003 No ACSyncdRR Safe=Fre Wse SyncdWW SyncdWR Time acsdrr003 85.01 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr004.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr004 "Fre SyncsWR Fre SyncdWW Wse Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 6,2 _litmus_P1_1_: stw 6,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 5,1 _litmus_P1_4_: stw 5,0(9) _litmus_P0_0_: li 11,1 _litmus_P0_1_: stw 11,0(9) _litmus_P0_2_: sync _litmus_P0_3_: lwz 6,0(9) Test acsdrr004 Allowed Histogram (39 states) 580659:>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 1021357:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 801493:>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 14511 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 54260 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 97249 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 583995:>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 97903 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2; 665922:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 1105496:>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 3294934:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 1466065:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 3072611:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1; 2999032:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 6447142:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 25454455:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 11968740:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 4151619:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 3220776:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 6402734:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 8616791:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1; 12642035:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 1300157:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2; 2817417:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 13610701:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 1803909:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 7045599:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 5786353:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1; 17528952:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 25405063:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 23844901:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 19639269:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2; 2597880:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 13317616:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 18723962:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 31427295:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 7344838:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2; 9877381:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 23168928:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=3e9c4d396fcad12ee5da6f76dcf812c7 Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe SyncdRR Relax acsdrr004 No ACSyncdRR Safe=Fre Wse SyncsWR SyncdWW Time acsdrr004 88.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr005.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr005 "Fre SyncdWW Wse LwSyncdWW Wse Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,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,1 _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 acsdrr005 Allowed Histogram (21 states) 807495:>3:r1=0; 3:r3=1; x=1; y=1; 1304661:>3:r1=0; 3:r3=0; x=2; y=2; 1943364:>3:r1=1; 3:r3=1; x=2; y=2; 2944471:>3:r1=2; 3:r3=1; x=2; y=2; 35085159:>3:r1=2; 3:r3=1; x=2; y=1; 3416619:>3:r1=2; 3:r3=0; x=2; y=1; 6646895:>3:r1=0; 3:r3=1; x=1; y=2; 17892842:>3:r1=1; 3:r3=1; x=1; y=2; 32128647:>3:r1=2; 3:r3=1; x=1; y=2; 19064423:>3:r1=0; 3:r3=0; x=2; y=1; 23094450:>3:r1=1; 3:r3=1; x=1; y=1; 12665612:>3:r1=0; 3:r3=1; x=2; y=2; 11486239:>3:r1=1; 3:r3=0; x=1; y=2; 22039703:>3:r1=2; 3:r3=0; x=1; y=1; 10848550:>3:r1=2; 3:r3=1; x=1; y=1; 32592020:>3:r1=0; 3:r3=0; x=1; y=1; 27580251:>3:r1=0; 3:r3=1; x=2; y=1; 3996766:>3:r1=1; 3:r3=0; x=1; y=1; 5966634:>3:r1=2; 3:r3=0; x=1; y=2; 35757125:>3:r1=0; 3:r3=0; x=1; y=2; 12738074:>3:r1=1; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=b6e9fe2e5db536ad9a06213fb6ed8db9 Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe SyncdRR Relax acsdrr005 No ACSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time acsdrr005 84.65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr006.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr006 "Fre LwSyncdWW Wse LwSyncdWW Wse Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,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,1 _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 acsdrr006 Allowed Histogram (21 states) 622989:>3:r1=0; 3:r3=1; x=1; y=1; 1854291:>3:r1=0; 3:r3=0; x=2; y=2; 3649296:>3:r1=1; 3:r3=0; x=1; y=1; 9755194:>3:r1=2; 3:r3=1; x=1; y=1; 2702375:>3:r1=1; 3:r3=1; x=2; y=2; 10651001:>3:r1=1; 3:r3=0; x=1; y=2; 5387760:>3:r1=2; 3:r3=0; x=1; y=2; 28063010:>3:r1=0; 3:r3=1; x=2; y=1; 17274928:>3:r1=1; 3:r3=1; x=1; y=2; 3767095:>3:r1=2; 3:r3=0; x=2; y=1; 4130712:>3:r1=2; 3:r3=1; x=2; y=2; 34825815:>3:r1=0; 3:r3=0; x=1; y=2; 19845796:>3:r1=2; 3:r3=0; x=1; y=1; 5846069:>3:r1=0; 3:r3=1; x=1; y=2; 29999692:>3:r1=0; 3:r3=0; x=1; y=1; 30752225:>3:r1=2; 3:r3=1; x=1; y=2; 38840320:>3:r1=2; 3:r3=1; x=2; y=1; 21391978:>3:r1=0; 3:r3=0; x=2; y=1; 14624957:>3:r1=0; 3:r3=1; x=2; y=2; 21395888:>3:r1=1; 3:r3=1; x=1; y=1; 14618609:>3:r1=1; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=04f3e54d9d70f9d6de8993f037ab8473 Cycle=Fre LwSyncdWW Wse LwSyncdWW Wse Rfe SyncdRR Relax acsdrr006 No ACSyncdRR Safe=Fre Wse LwSyncdWW Time acsdrr006 87.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr007.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr007 "Fre LwSyncdWW Wse Rfe SyncdRR" {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) | sync ; lwsync | | lwz r3,0(r4) ; li r3,1 | | ; stw r3,0(r4) | | ; exists (x=2 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,0(9) _litmus_P1_0_: li 6,2 _litmus_P1_1_: stw 6,0(9) _litmus_P0_0_: li 5,1 _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 acsdrr007 Allowed Histogram (9 states) 1520561:>2:r1=0; 2:r3=1; x=1; 43045286:>2:r1=1; 2:r3=1; x=1; 40123158:>2:r1=0; 2:r3=1; x=2; 49562431:>2:r1=2; 2:r3=1; x=1; 34662196:>2:r1=0; 2:r3=0; x=2; 33979081:>2:r1=1; 2:r3=1; x=2; 57659505:>2:r1=2; 2:r3=1; x=2; 44038639:>2:r1=2; 2:r3=0; x=1; 95409143:>2:r1=0; 2:r3=0; x=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=64b08d9964a91d502b8b10812d9b32b9 Cycle=Fre LwSyncdWW Wse Rfe SyncdRR Relax acsdrr007 No ACSyncdRR Safe=Fre Wse LwSyncdWW Time acsdrr007 71.73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr008.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr008 "Fre SyncdWR Fre LwSyncdWW Wse Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,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,1 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrr008 Allowed Histogram (21 states) 4418768:>0:r3=1; 3:r1=0; 3:r3=1; y=2; 3745307:>0:r3=0; 3:r1=2; 3:r3=1; y=2; 436577:>0:r3=1; 3:r1=0; 3:r3=1; y=1; 2637750:>0:r3=0; 3:r1=1; 3:r3=1; y=2; 4138416:>0:r3=1; 3:r1=1; 3:r3=0; y=1; 18896732:>0:r3=1; 3:r1=1; 3:r3=1; y=1; 6957289:>0:r3=1; 3:r1=2; 3:r3=1; y=1; 11715392:>0:r3=1; 3:r1=1; 3:r3=0; y=2; 16244783:>0:r3=1; 3:r1=1; 3:r3=1; y=2; 26265297:>0:r3=1; 3:r1=0; 3:r3=0; y=1; 15898375:>0:r3=0; 3:r1=1; 3:r3=1; y=1; 33351719:>0:r3=1; 3:r1=0; 3:r3=0; y=2; 39733139:>0:r3=0; 3:r1=2; 3:r3=1; y=1; 27103529:>0:r3=0; 3:r1=0; 3:r3=1; y=1; 3585810:>0:r3=0; 3:r1=0; 3:r3=0; y=2; 29210338:>0:r3=1; 3:r1=2; 3:r3=1; y=2; 5613505:>0:r3=0; 3:r1=2; 3:r3=0; y=1; 26996135:>0:r3=0; 3:r1=0; 3:r3=0; y=1; 16070037:>0:r3=0; 3:r1=0; 3:r3=1; y=2; 6210614:>0:r3=1; 3:r1=2; 3:r3=0; y=2; 20770488:>0:r3=1; 3:r1=2; 3:r3=0; y=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=78a292439dc422b6e8d30112bf3ced0e Cycle=Fre SyncdWR Fre LwSyncdWW Wse Rfe SyncdRR Relax acsdrr008 No ACSyncdRR Safe=Fre Wse SyncdWR LwSyncdWW Time acsdrr008 86.12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr009.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr009 "Fre SyncsWR Fre LwSyncdWW Wse Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 7,2 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: li 6,2 _litmus_P1_1_: stw 6,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 5,1 _litmus_P1_4_: stw 5,0(9) _litmus_P0_0_: li 11,1 _litmus_P0_1_: stw 11,0(9) _litmus_P0_2_: sync _litmus_P0_3_: lwz 6,0(9) Test acsdrr009 Allowed Histogram (39 states) 22763 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 756896:>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 1029537:>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 533465:>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 88082 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 115581:>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2; 1346584:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 387048:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 1164711:>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 1363574:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2; 1224379:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 57532 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 1000107:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 10389164:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 3448851:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 5140531:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 3400390:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1; 10925001:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1; 3934135:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 13149436:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 6471783:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 17153149:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2; 21988616:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 15546201:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 5025308:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 10889545:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 23267923:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 5792415:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 16604545:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 3574229:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 4951033:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 23499489:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 6379142:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2; 28332958:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 2792381:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 8415007:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1; 15834281:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 15475220:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 28529008:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=745664b5fbc00e7ca847ad37ec693890 Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe SyncdRR Relax acsdrr009 No ACSyncdRR Safe=Fre Wse SyncsWR LwSyncdWW Time acsdrr009 83.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr010.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr010 "Fre Rfe SyncdRR Fre Rfe SyncdRR" {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 ; sync | stw r1,0(r2) | sync | 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_P3_0_: li 8,1 _litmus_P3_1_: stw 8,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 4,0(9) _litmus_P1_0_: li 7,1 _litmus_P1_1_: stw 7,0(9) _litmus_P0_0_: lwz 3,0(11) _litmus_P0_1_: sync _litmus_P0_2_: lwz 4,0(9) Test acsdrr010 Allowed Histogram (15 states) 453039:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 5176719:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 54338084:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 21839246:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 6012484:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 22025069:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 20338750:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 26383751:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 25191034:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 5261368:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 5968078:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 26044882:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 20263145:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 25277555:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 55426796:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=636f71f6ac76c8070d3470d463d1e541 Cycle=Fre Rfe SyncdRR Fre Rfe SyncdRR Relax acsdrr010 No ACSyncdRR Safe=Fre Time acsdrr010 75.85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr011.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr011 "Fre SyncdWW Rfe SyncdRR Fre Rfe SyncdRR" {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) | sync | stw r1,0(r2) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 7,1 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 31,0(9) _litmus_P0_0_: li 6,1 _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 acsdrr011 Allowed Histogram (15 states) 1855972:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 5608621:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 32160272:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 22100641:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 2182940:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 821647:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 27340175:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 12592485:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 11954073:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 31544809:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 41005245:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 59659456:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 2111066:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 31812702:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 37249896:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=9ba8d06082edddfad8113101654d0430 Cycle=Fre SyncdWW Rfe SyncdRR Fre Rfe SyncdRR Relax acsdrr011 No ACSyncdRR Safe=Fre SyncdWW Time acsdrr011 83.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr012.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr012 "Fre SyncsWW Rfe SyncdRR Fre Rfe SyncdRR" {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) | sync | stw r1,0(r2) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 7,1 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 4,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P0_2_: sync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test acsdrr012 Allowed Histogram (35 states) 2 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 3254 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 220755:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 156395:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 1045615:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 531091:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 1023693:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 4182989:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 2176430:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 1968520:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 826701:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 5617831:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 3653410:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 2366392:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 2869432:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 1404881:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 2077183:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 2217262:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 4818755:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 21335613:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 2964571:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 5326525:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 22005202:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 6007908:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 21598175:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 20709469:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 4049719:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 5921079:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 19280652:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 26226927:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 12654130:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 40058950:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 17981978:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 56718510:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=36537b94a10ccfe23173e79705a28b83 Cycle=Fre SyncsWW Rfe SyncdRR Fre Rfe SyncdRR Relax acsdrr012 No ACSyncdRR Safe=Fre SyncsWW Time acsdrr012 83.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr013.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr013 "Fre LwSyncdWW Rfe SyncdRR Fre Rfe SyncdRR" {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) | sync | stw r1,0(r2) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 7,1 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 31,0(9) _litmus_P0_0_: li 6,1 _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 acsdrr013 Allowed Histogram (15 states) 1216265:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 1677143:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 39109493:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 24003236:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 2440479:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 27272796:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 30454676:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 57483243:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 42460300:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3951497:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 29149974:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 14381743:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 16528217:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 4974200:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 24896738:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; No Witnesses Positive: 0, Negative: 320000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=f7450a70568e1efcac71344b7c31e524 Cycle=Fre LwSyncdWW Rfe SyncdRR Fre Rfe SyncdRR Relax acsdrr013 No ACSyncdRR Safe=Fre LwSyncdWW Time acsdrr013 83.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr014.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr014 "Fre LwSyncsWW Rfe SyncdRR Fre Rfe SyncdRR" {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) | sync | stw r1,0(r2) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 7,1 _litmus_P2_1_: stw 7,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 4,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P0_2_: lwsync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test acsdrr014 Allowed Histogram (33 states) 849 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 73618 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 136544:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 234345:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 488814:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 204288:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 1092893:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 128753:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 1876874:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 692249:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 1070970:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 2327824:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 1853276:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 811112:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 2785270:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1697417:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 5526873:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 21690390:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 429303:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1010621:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 22831572:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 17325400:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 1111613:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 24268098:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 5400234:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 23814611:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 20264573:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 23879939:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 5822354:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 23389091:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 48824863:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 54941107:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 3994262:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=b700f92a76eb70d8c18d53f7af0a21d5 Cycle=Fre LwSyncsWW Rfe SyncdRR Fre Rfe SyncdRR Relax acsdrr014 No ACSyncdRR Safe=Fre LwSyncsWW Time acsdrr014 84.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr015.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr015 "Fre SyncdWW Wse SyncdWR Fre Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,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,1 _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 acsdrr015 Allowed Histogram (15 states) 2453159:>1:r3=0; 3:r1=0; 3:r3=0; x=2; 5097253:>1:r3=0; 3:r1=1; 3:r3=1; x=2; 3775013:>1:r3=1; 3:r1=1; 3:r3=0; x=2; 5651443:>1:r3=0; 3:r1=1; 3:r3=0; x=1; 23756661:>1:r3=1; 3:r1=0; 3:r3=1; x=2; 26452957:>1:r3=1; 3:r1=1; 3:r3=0; x=1; 18983219:>1:r3=1; 3:r1=0; 3:r3=0; x=2; 28319744:>1:r3=0; 3:r1=1; 3:r3=1; x=1; 31043277:>1:r3=1; 3:r1=1; 3:r3=1; x=1; 19393195:>1:r3=0; 3:r1=0; 3:r3=1; x=2; 516046:>1:r3=1; 3:r1=0; 3:r3=1; x=1; 27632734:>1:r3=1; 3:r1=0; 3:r3=0; x=1; 23228998:>1:r3=0; 3:r1=0; 3:r3=1; x=1; 47724175:>1:r3=1; 3:r1=1; 3:r3=1; x=2; 55972126:>1:r3=0; 3:r1=0; 3:r3=0; x=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=93405f0ed846673bae038ca9a3ad151b Cycle=Fre SyncdWW Wse SyncdWR Fre Rfe SyncdRR Relax acsdrr015 No ACSyncdRR Safe=Fre Wse SyncdWW SyncdWR Time acsdrr015 84.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr016.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr016 "Fre LwSyncdWW Wse SyncdWR Fre Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,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,1 _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 acsdrr016 Allowed Histogram (15 states) 352739:>1:r3=1; 3:r1=0; 3:r3=1; x=1; 3414580:>1:r3=0; 3:r1=0; 3:r3=0; x=2; 5287263:>1:r3=0; 3:r1=1; 3:r3=0; x=1; 4214543:>1:r3=1; 3:r1=1; 3:r3=0; x=2; 23920468:>1:r3=1; 3:r1=0; 3:r3=1; x=2; 21315984:>1:r3=1; 3:r1=0; 3:r3=0; x=2; 23697873:>1:r3=1; 3:r1=1; 3:r3=0; x=1; 22239790:>1:r3=0; 3:r1=0; 3:r3=1; x=2; 21582560:>1:r3=0; 3:r1=0; 3:r3=1; x=1; 6356430:>1:r3=0; 3:r1=1; 3:r3=1; x=2; 26943469:>1:r3=0; 3:r1=1; 3:r3=1; x=1; 25190810:>1:r3=1; 3:r1=0; 3:r3=0; x=1; 28235169:>1:r3=1; 3:r1=1; 3:r3=1; x=1; 53209794:>1:r3=1; 3:r1=1; 3:r3=1; x=2; 54038528:>1:r3=0; 3:r1=0; 3:r3=0; x=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=8a3aeefda3b897535b28a928e24ffa41 Cycle=Fre LwSyncdWW Wse SyncdWR Fre Rfe SyncdRR Relax acsdrr016 No ACSyncdRR Safe=Fre Wse SyncdWR LwSyncdWW Time acsdrr016 85.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr017.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr017 "Fre SyncdWR Fre Rfe SyncdRR" {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) | sync ; sync | | lwz r3,0(r4) ; lwz r3,0(r4) | | ; exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,0(9) _litmus_P1_0_: li 6,1 _litmus_P1_1_: stw 6,0(9) _litmus_P0_0_: li 4,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrr017 Allowed Histogram (8 states) 2 :>0:r3=0; 2:r1=1; 2:r3=0; 713218:>0:r3=1; 2:r1=0; 2:r3=1; 50063347:>0:r3=0; 2:r1=0; 2:r3=0; 48142340:>0:r3=1; 2:r1=1; 2:r3=0; 54129425:>0:r3=0; 2:r1=1; 2:r3=1; 88532285:>0:r3=1; 2:r1=1; 2:r3=1; 77244022:>0:r3=0; 2:r1=0; 2:r3=1; 81175361:>0:r3=1; 2:r1=0; 2:r3=0; Ok Witnesses Positive: 2, Negative: 399999998 Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=594d010ae884a7901d60ab5268a95257 Cycle=Fre SyncdWR Fre Rfe SyncdRR Relax acsdrr017 Ok ACSyncdRR Safe=Fre SyncdWR Time acsdrr017 74.50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr018.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr018 "Fre SyncdWR Fre SyncdWR Fre Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,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,1 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrr018 Allowed Histogram (15 states) 5622784:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0; 6304099:>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1; 23412971:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; 255473:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; 22955068:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1; 19760590:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; 6057682:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0; 22225175:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; 25699966:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; 25453056:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; 53088798:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; 54004862:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; 24994715:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; 5414170:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0; 24750591:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; No Witnesses Positive: 0, Negative: 320000000 Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=7694032af7eaa4c629a106dbe2fda3e2 Cycle=Fre SyncdWR Fre SyncdWR Fre Rfe SyncdRR Relax acsdrr018 No ACSyncdRR Safe=Fre SyncdWR Time acsdrr018 83.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr019.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr019 "Fre SyncsWR Fre SyncdWR Fre Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 7,1 _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_: lwz 4,0(9) _litmus_P0_0_: li 11,1 _litmus_P0_1_: stw 11,0(9) _litmus_P0_2_: sync _litmus_P0_3_: lwz 6,0(9) Test acsdrr019 Allowed Histogram (32 states) 3 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 36071 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 43207 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 32888 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 1744178:>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 2102970:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1023436:>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 1465338:>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 103516:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1428726:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 2545712:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 6255931:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 5723970:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 24862927:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1; 27901561:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 185370:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1; 4968633:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1; 3278481:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 9100092:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1; 7255277:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 678256:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1; 34863975:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 18601502:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1; 20165382:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1; 22862978:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 19145041:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1; 13525925:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1; 14025835:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 29636265:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1; 19394746:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 7865153:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 19176655:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1; No Witnesses Positive: 0, Negative: 320000000 Condition exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=a3b2b2fd87d8003094c276c1c7dc52d1 Cycle=Fre SyncsWR Fre SyncdWR Fre Rfe SyncdRR Relax acsdrr019 No ACSyncdRR Safe=Fre SyncsWR SyncdWR Time acsdrr019 82.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr020.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr020 "Fre SyncdWR Fre SyncsWR Fre Rfe SyncdRR" {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) | sync ; 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_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,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,1 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 4,0(9) Test acsdrr020 Allowed Histogram (48 states) 17 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; 111 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=1; 71 :>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; 5850 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; 6937 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 21925 :>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 82619 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 70777 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 2304380:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 116662:>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 390692:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 123183:>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 203868:>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; 132042:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 62427 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 628739:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 3075282:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 1161376:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; 2300857:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 171164:>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 1613605:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 9617226:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 2259855:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 1452352:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 6597900:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 3284055:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 10537360:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 10994535:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 15209518:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 19107636:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 9963654:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 7833931:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 7277846:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 5358890:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; 9132202:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 17943389:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 20608907:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 20871617:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 6587130:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 6529968:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; 12164208:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 16661363:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 17685826:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 18171824:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 15802977:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 5748967:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1; 16299398:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; 13824882:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=364b008b4e827c7da8277245f7998211 Cycle=Fre SyncdWR Fre SyncsWR Fre Rfe SyncdRR Relax acsdrr020 No ACSyncdRR Safe=Fre SyncsWR SyncdWR Time acsdrr020 89.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr021.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr021 "Fre SyncdWW Wse SyncdWW Rfe SyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | sync | lwz r3,0(r4) ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,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,1 _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 acsdrr021 Allowed Histogram (7 states) 9660234:>2:r1=1; 2:r3=1; x=2; 14022182:>2:r1=0; 2:r3=1; x=1; 133533707:>2:r1=0; 2:r3=0; x=1; 15230227:>2:r1=1; 2:r3=0; x=1; 33335530:>2:r1=0; 2:r3=0; x=2; 109972100:>2:r1=0; 2:r3=1; x=2; 84246020:>2:r1=1; 2:r3=1; x=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=5d5c1aae91591f0f085c166e6ff700e6 Cycle=Fre SyncdWW Wse SyncdWW Rfe SyncdRR Relax acsdrr021 No ACSyncdRR Safe=Fre Wse SyncdWW Time acsdrr021 72.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr022.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr022 "Fre LwSyncdWW Wse SyncdWW Rfe SyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; lwsync | sync | lwz r3,0(r4) ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,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,1 _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 acsdrr022 Allowed Histogram (7 states) 10800079:>2:r1=0; 2:r3=1; x=1; 12424286:>2:r1=1; 2:r3=1; x=2; 37939039:>2:r1=0; 2:r3=0; x=2; 14886321:>2:r1=1; 2:r3=0; x=1; 128887371:>2:r1=0; 2:r3=0; x=1; 78433092:>2:r1=1; 2:r3=1; x=1; 116629812:>2:r1=0; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=33d57db58ff4f0de2ca9b62adc3c44e3 Cycle=Fre LwSyncdWW Wse SyncdWW Rfe SyncdRR Relax acsdrr022 No ACSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time acsdrr022 75.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr023.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr023 "Fre SyncdWW Rfe SyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;} P0 | P1 ; li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync ; sync | lwz r3,0(r4) ; li r3,1 | ; stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 4,0(9) _litmus_P0_0_: li 6,1 _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 acsdrr023 Allowed Histogram (3 states) 107909890:>1:r1=0; 1:r3=1; 308272964:>1:r1=0; 1:r3=0; 223817146:>1:r1=1; 1:r3=1; No Witnesses Positive: 0, Negative: 640000000 Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated Hash=e29ebb6e64fa9079ba348c5180003cc2 Cycle=Fre SyncdWW Rfe SyncdRR Relax acsdrr023 No ACSyncdRR Safe=Fre SyncdWW Time acsdrr023 74.46 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr024.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr024 "Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR" {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,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | sync ; sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 6,1 _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_: lwz 31,0(9) _litmus_P0_0_: li 5,1 _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 acsdrr024 Allowed Histogram (15 states) 5779043:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 478576:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 11872872:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 12736935:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 435931:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 48753630:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 13213050:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 34111959:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 726142:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 21014541:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 35004260:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 72251753:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 50138057:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 12836134:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 647117:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; No Witnesses Positive: 0, Negative: 320000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=6614bb5f345fce6def5659d5fa2123d7 Cycle=Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR Relax acsdrr024 No ACSyncdRR Safe=Fre SyncdWW Time acsdrr024 93.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr025.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr025 "Fre SyncsWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=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) | sync | stw r1,0(r2) | sync ; sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; li r3,2 | | li r3,1 | ; stw r3,0(r2) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 5,1 _litmus_P2_1_: stw 5,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 4,1 _litmus_P2_4_: stw 4,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 4,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P0_2_: sync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test acsdrr025 Allowed Histogram (33 states) 545 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 857920:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 834379:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 587732:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 794924:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 972833:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 621715:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 723329:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 3565923:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 606395:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 4449203:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 1999391:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 8198563:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 791861:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 1155662:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 7094069:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 2202417:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 32778553:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 3796297:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 1292195:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 29386922:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 18108293:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 1037887:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 928936:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 2613027:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 22418470:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 21242284:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 10595663:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 4704625:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 13664961:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 63396645:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 24000560:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 34577821:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=54bc20dc4f311ade7a2f268864e2abfd Cycle=Fre SyncsWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR Relax acsdrr025 No ACSyncdRR Safe=Fre SyncsWW SyncdWW Time acsdrr025 92.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr026.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr026 "Fre LwSyncdWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR" {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,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | sync ; lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 6,1 _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_: lwz 31,0(9) _litmus_P0_0_: li 5,1 _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 acsdrr026 Allowed Histogram (15 states) 1155723:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 459925:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 15802946:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 4851189:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 10730640:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 11851528:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 24677657:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 1001088:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 37664278:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 32208261:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 19617157:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 47064722:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 42456476:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 69880071:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 578339:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; No Witnesses Positive: 0, Negative: 320000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=1e2ab3a033eb8d91c878eb2ef29c7240 Cycle=Fre LwSyncdWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR Relax acsdrr026 No ACSyncdRR Safe=Fre SyncdWW LwSyncdWW Time acsdrr026 93.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr027.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr027 "Fre LwSyncsWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=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) | sync | stw r1,0(r2) | sync ; lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; li r3,2 | | li r3,1 | ; stw r3,0(r2) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 5,1 _litmus_P2_1_: stw 5,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 4,1 _litmus_P2_4_: stw 4,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 4,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P0_2_: lwsync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test acsdrr027 Allowed Histogram (33 states) 224 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 134177:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 1121933:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 274414:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 104637:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 301864:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 198782:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 906005:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 1956064:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 2894418:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 2351115:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 299539:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 1582654:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 1537771:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 349954:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 248122:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 791479:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 2383133:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 464829:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 1525994:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 19708446:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 3465933:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 29112831:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 1644364:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 25422693:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 11027799:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 29648978:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 37960794:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 31076697:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 4313836:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 34174197:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 60761844:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 12254480:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=395dda6a76de9dcf7e101c7347e87098 Cycle=Fre LwSyncsWW Rfe SyncdRR Fre SyncdWW Rfe SyncdRR Relax acsdrr027 No ACSyncdRR Safe=Fre SyncdWW LwSyncsWW Time acsdrr027 92.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr028.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr028 "Fre SyncdWR Fre SyncdWW Rfe SyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | sync | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,1 | ; | stw r3,0(r4) | ; exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,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,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrr028 Allowed Histogram (7 states) 7873340:>0:r3=1; 2:r1=0; 2:r3=1; 116171164:>0:r3=0; 2:r1=0; 2:r3=1; 51567686:>0:r3=0; 2:r1=0; 2:r3=0; 76249804:>0:r3=1; 2:r1=1; 2:r3=1; 16715558:>0:r3=0; 2:r1=1; 2:r3=1; 114892356:>0:r3=1; 2:r1=0; 2:r3=0; 16530092:>0:r3=1; 2:r1=1; 2:r3=0; No Witnesses Positive: 0, Negative: 400000000 Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=253c3d0e979b12ac15c5e6729d565644 Cycle=Fre SyncdWR Fre SyncdWW Rfe SyncdRR Relax acsdrr028 No ACSyncdRR Safe=Fre SyncdWW SyncdWR Time acsdrr028 78.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr029.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr029 "Fre SyncsWR Fre SyncdWW Rfe SyncdRR" {0:r2=y; 1:r2=y; 1:r4=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) | sync ; sync | sync | lwz r3,0(r4) ; lwz r3,0(r2) | li r3,1 | ; | stw r3,0(r4) | ; exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,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 11,1 _litmus_P0_1_: stw 11,0(9) _litmus_P0_2_: sync _litmus_P0_3_: lwz 5,0(9) Test acsdrr029 Allowed Histogram (13 states) 110879:>0:r3=2; 2:r1=0; 2:r3=1; y=2; 2157720:>0:r3=2; 2:r1=1; 2:r3=2; y=2; 8960806:>0:r3=1; 2:r1=0; 2:r3=1; y=1; 70108913:>0:r3=1; 2:r1=1; 2:r3=1; y=1; 1071430:>0:r3=2; 2:r1=0; 2:r3=2; y=2; 64303621:>0:r3=1; 2:r1=0; 2:r3=1; y=2; 42233848:>0:r3=1; 2:r1=0; 2:r3=2; y=1; 8197924:>0:r3=2; 2:r1=0; 2:r3=0; y=2; 62346512:>0:r3=1; 2:r1=0; 2:r3=0; y=1; 14219212:>0:r3=1; 2:r1=1; 2:r3=2; y=2; 56892505:>0:r3=1; 2:r1=0; 2:r3=0; y=2; 54660486:>0:r3=1; 2:r1=0; 2:r3=2; y=2; 14736144:>0:r3=1; 2:r1=1; 2:r3=2; y=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=b11bf67f6ac9a0eb7e2bfc28b97cd05c Cycle=Fre SyncsWR Fre SyncdWW Rfe SyncdRR Relax acsdrr029 No ACSyncdRR Safe=Fre SyncsWR SyncdWW Time acsdrr029 76.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr030.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr030 "Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR" {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) | sync | stw r1,0(r2) | sync ; sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; li r3,2 | | li r3,2 | ; stw r3,0(r2) | | stw r3,0(r2) | ; exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 6,1 _litmus_P2_1_: stw 6,0(9) _litmus_P2_2_: sync _litmus_P2_3_: li 11,2 _litmus_P2_4_: stw 11,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 4,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P0_2_: sync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test acsdrr030 Allowed Histogram (72 states) 1196 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 1449 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 1729 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 1393 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 46613 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 2396 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 73343 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 1055 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 7602 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 285852:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 901746:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 757633:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 122825:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 270164:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 1610243:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 3043387:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 210781:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 325471:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 263207:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 541799:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 3719630:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 762400:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 569264:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1876255:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 324903:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 1240003:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 1690817:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1217486:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 2591396:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 2800958:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 1655195:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 287856:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 28381 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 48062 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 691731:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 4166873:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 212819:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 13760252:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 4397431:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 288585:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 713077:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 1142624:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 765149:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 116505:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 2001818:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 4462331:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 751287:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 254252:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 1751244:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 17672003:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 17130421:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 2782112:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 3603492:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 1306974:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 316619:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 5741780:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 910242:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 4174829:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 2424452:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 20450680:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 34258274:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 3890370:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 2077792:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 2969792:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 5787724:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 17663614:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 3956666:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 20105715:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 13627749:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 1994669:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 16687098:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 57708465:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=e437caed8f6d9647f946982642be159d Cycle=Fre SyncsWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR Relax acsdrr030 No ACSyncdRR Safe=Fre SyncsWW Time acsdrr030 95.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr031.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr031 "Fre LwSyncdWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR" {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) | sync | stw r1,0(r2) | sync ; lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; li r3,1 | | li r3,2 | ; stw r3,0(r4) | | stw r3,0(r2) | ; exists (y=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 6,1 _litmus_P2_1_: stw 6,0(9) _litmus_P2_2_: sync _litmus_P2_3_: li 11,2 _litmus_P2_4_: stw 11,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 31,0(9) _litmus_P0_0_: li 6,1 _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 acsdrr031 Allowed Histogram (33 states) 669 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 1118917:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; y=2; 658642:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 2022033:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 2239928:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; y=2; 20441487:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; y=2; 1443321:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 18627668:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; y=2; 1997750:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; y=2; 929550:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; y=2; 8564818:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 946002:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 3928578:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; y=2; 5021010:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; y=2; 1931229:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; y=2; 582291:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 1015581:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1240045:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; y=2; 4752975:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; y=2; 1102102:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 742640:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; y=2; 7340182:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 11342617:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; y=2; 1249602:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 18859653:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 4926800:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 33588950:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; y=2; 61404002:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 29856877:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 30973157:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; y=2; 1096341:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; y=2; 18875225:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; y=2; 21179358:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; y=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (y=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=a80182bdadf201f75f7bb65ee084fa69 Cycle=Fre LwSyncdWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR Relax acsdrr031 No ACSyncdRR Safe=Fre SyncsWW LwSyncdWW Time acsdrr031 90.75 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr032.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr032 "Fre LwSyncsWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR" {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) | sync | stw r1,0(r2) | sync ; lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; li r3,2 | | li r3,2 | ; stw r3,0(r2) | | stw r3,0(r2) | ; exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 6,1 _litmus_P2_1_: stw 6,0(9) _litmus_P2_2_: sync _litmus_P2_3_: li 11,2 _litmus_P2_4_: stw 11,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 4,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P0_2_: lwsync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test acsdrr032 Allowed Histogram (72 states) 553 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 543 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 1180 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 1372 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 2817 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 13242 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 460 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 2413 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 56277 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 141772:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 81413 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 41023 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 32469 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 23666 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 115575:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 362710:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 78531 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 102706:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 243476:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 271757:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 375809:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 181864:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 186836:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 55905 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 273361:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 111690:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 469326:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 1010502:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 694440:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 920758:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 2286076:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 1156853:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 893455:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 338963:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 121002:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 3553913:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 240238:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1915943:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 813468:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 2366448:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 355439:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 397072:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 1228843:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 1708307:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 2631002:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 2316293:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 695430:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 5079192:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 150408:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 1703541:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 1285069:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 2460769:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 5002190:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 2769604:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 2093283:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1745631:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 2506669:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 5304096:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 18406050:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 3563219:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 20859686:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 55195657:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 19381728:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 12477545:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 3356842:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 18354214:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 6009387:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 18342185:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 38553191:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 4509275:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 23614684:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 18402694:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=5dbd213a60e04f42d1a6588419a502dc Cycle=Fre LwSyncsWW Rfe SyncdRR Fre SyncsWW Rfe SyncdRR Relax acsdrr032 No ACSyncdRR Safe=Fre SyncsWW LwSyncsWW Time acsdrr032 91.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr033.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr033 "Fre SyncdWR Fre SyncsWW Rfe SyncdRR" {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) | sync ; sync | sync | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,2 | ; | stw r3,0(r2) | ; exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,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,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrr033 Allowed Histogram (15 states) 298284:>0:r3=1; 2:r1=0; 2:r3=1; x=2; 219679:>0:r3=2; 2:r1=0; 2:r3=1; x=2; 236159:>0:r3=1; 2:r1=1; 2:r3=0; x=2; 2830488:>0:r3=2; 2:r1=1; 2:r3=1; x=2; 2141766:>0:r3=1; 2:r1=1; 2:r3=1; x=2; 16543820:>0:r3=0; 2:r1=1; 2:r3=1; x=2; 7955000:>0:r3=2; 2:r1=1; 2:r3=0; x=2; 51378455:>0:r3=0; 2:r1=0; 2:r3=0; x=2; 37619429:>0:r3=0; 2:r1=2; 2:r3=1; x=2; 35907059:>0:r3=2; 2:r1=2; 2:r3=0; x=2; 3446830:>0:r3=1; 2:r1=2; 2:r3=1; x=2; 17950578:>0:r3=1; 2:r1=0; 2:r3=0; x=2; 84480521:>0:r3=2; 2:r1=2; 2:r3=1; x=2; 77746175:>0:r3=0; 2:r1=0; 2:r3=1; x=2; 61245757:>0:r3=2; 2:r1=0; 2:r3=0; x=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=9fee6cd32468b8b76fc6ca805e427cad Cycle=Fre SyncdWR Fre SyncsWW Rfe SyncdRR Relax acsdrr033 No ACSyncdRR Safe=Fre SyncsWW SyncdWR Time acsdrr033 78.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr034.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr034 "Fre SyncdWW Wse LwSyncdWW Rfe SyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | lwsync | lwz r3,0(r4) ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,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,1 _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 acsdrr034 Allowed Histogram (7 states) 8675554:>2:r1=0; 2:r3=1; x=1; 33964500:>2:r1=0; 2:r3=0; x=2; 105306412:>2:r1=0; 2:r3=1; x=2; 27191486:>2:r1=1; 2:r3=0; x=1; 12869541:>2:r1=1; 2:r3=1; x=2; 92423503:>2:r1=1; 2:r3=1; x=1; 119569004:>2:r1=0; 2:r3=0; x=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=27d7745baac632fe4aea9c285d538d4c Cycle=Fre SyncdWW Wse LwSyncdWW Rfe SyncdRR Relax acsdrr034 No ACSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time acsdrr034 76.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr035.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr035 "Fre LwSyncdWW Wse LwSyncdWW Rfe SyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; lwsync | lwsync | lwz r3,0(r4) ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,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,1 _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 acsdrr035 Allowed Histogram (7 states) 5542407:>2:r1=0; 2:r3=1; x=1; 17021722:>2:r1=1; 2:r3=1; x=2; 37160750:>2:r1=0; 2:r3=0; x=2; 25906168:>2:r1=1; 2:r3=0; x=1; 115725501:>2:r1=0; 2:r3=0; x=1; 86658268:>2:r1=1; 2:r3=1; x=1; 111985184:>2:r1=0; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=9477b1b1723232b68b25f79dd7a2be1b Cycle=Fre LwSyncdWW Wse LwSyncdWW Rfe SyncdRR Relax acsdrr035 No ACSyncdRR Safe=Fre Wse LwSyncdWW Time acsdrr035 76.40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr036.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr036 "Fre LwSyncdWW Rfe SyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;} P0 | P1 ; li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync ; lwsync | lwz r3,0(r4) ; li r3,1 | ; stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 4,0(9) _litmus_P0_0_: li 6,1 _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 acsdrr036 Allowed Histogram (3 states) 285411902:>1:r1=1; 1:r3=1; 307248173:>1:r1=0; 1:r3=0; 47339925:>1:r1=0; 1:r3=1; No Witnesses Positive: 0, Negative: 640000000 Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated Hash=b45ef7dfb9b495b3b934e3202a3ae026 Cycle=Fre LwSyncdWW Rfe SyncdRR Relax acsdrr036 No ACSyncdRR Safe=Fre LwSyncdWW Time acsdrr036 76.67 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr037.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr037 "Fre LwSyncdWW Rfe SyncdRR Fre LwSyncdWW Rfe SyncdRR" {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,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | sync ; lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 6,1 _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_: lwz 31,0(9) _litmus_P0_0_: li 5,1 _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 acsdrr037 Allowed Histogram (15 states) 877303:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 1167958:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 973276:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 1188566:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 13649919:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 4385281:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 14141571:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 35830138:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 17662559:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 16974610:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 36855900:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 40703227:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 27786492:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 66223039:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 41580161:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; No Witnesses Positive: 0, Negative: 320000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=3a636427bd7edc2c2ac8a1c2b3f4438b Cycle=Fre LwSyncdWW Rfe SyncdRR Fre LwSyncdWW Rfe SyncdRR Relax acsdrr037 No ACSyncdRR Safe=Fre LwSyncdWW Time acsdrr037 89.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr038.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr038 "Fre LwSyncsWW Rfe SyncdRR Fre LwSyncdWW Rfe SyncdRR" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=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) | sync | stw r1,0(r2) | sync ; lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ; li r3,2 | | li r3,1 | ; stw r3,0(r2) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 5,1 _litmus_P2_1_: stw 5,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 4,1 _litmus_P2_4_: stw 4,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 4,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P0_2_: lwsync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test acsdrr038 Allowed Histogram (33 states) 396 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 157967:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 107950:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 380776:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 216568:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 3531708:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 726315:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 609187:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 307810:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 2051980:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 1830069:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 2979170:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 545684:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 3757282:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 1100522:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 623773:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 2252201:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 1860077:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 3186458:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 23319003:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 27192356:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 171475:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 26947753:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 1286039:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 2815783:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 16899191:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 1305452:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 20753372:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 58284652:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 38662992:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 35995237:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 27248933:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 12891869:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=321edf48bccde0acdebe52eab9a80f96 Cycle=Fre LwSyncsWW Rfe SyncdRR Fre LwSyncdWW Rfe SyncdRR Relax acsdrr038 No ACSyncdRR Safe=Fre LwSyncsWW LwSyncdWW Time acsdrr038 92.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr039.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr039 "Fre SyncdWR Fre LwSyncdWW Rfe SyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync ; sync | lwsync | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,1 | ; | stw r3,0(r4) | ; exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,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,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrr039 Allowed Histogram (7 states) 3731598:>0:r3=1; 2:r1=0; 2:r3=1; 27210458:>0:r3=1; 2:r1=1; 2:r3=0; 51190605:>0:r3=0; 2:r1=0; 2:r3=0; 21644174:>0:r3=0; 2:r1=1; 2:r3=1; 111262369:>0:r3=0; 2:r1=0; 2:r3=1; 102919914:>0:r3=1; 2:r1=0; 2:r3=0; 82040882:>0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=4123ecd9a851b7f1f3f7bbe069dac98e Cycle=Fre SyncdWR Fre LwSyncdWW Rfe SyncdRR Relax acsdrr039 No ACSyncdRR Safe=Fre SyncdWR LwSyncdWW Time acsdrr039 77.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr040.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr040 "Fre SyncsWR Fre LwSyncdWW Rfe SyncdRR" {0:r2=y; 1:r2=y; 1:r4=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) | sync ; sync | lwsync | lwz r3,0(r4) ; lwz r3,0(r2) | li r3,1 | ; | stw r3,0(r4) | ; exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,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 11,1 _litmus_P0_1_: stw 11,0(9) _litmus_P0_2_: sync _litmus_P0_3_: lwz 5,0(9) Test acsdrr040 Allowed Histogram (13 states) 2400667:>0:r3=2; 2:r1=1; 2:r3=2; y=2; 125768:>0:r3=2; 2:r1=0; 2:r3=1; y=2; 3275159:>0:r3=1; 2:r1=0; 2:r3=1; y=1; 1015012:>0:r3=2; 2:r1=0; 2:r3=2; y=2; 7923588:>0:r3=2; 2:r1=0; 2:r3=0; y=2; 19842809:>0:r3=1; 2:r1=1; 2:r3=2; y=2; 29247710:>0:r3=1; 2:r1=0; 2:r3=2; y=1; 63255512:>0:r3=1; 2:r1=0; 2:r3=0; y=1; 62969052:>0:r3=1; 2:r1=0; 2:r3=1; y=2; 77765400:>0:r3=1; 2:r1=1; 2:r3=1; y=1; 56172710:>0:r3=1; 2:r1=0; 2:r3=0; y=2; 50003308:>0:r3=1; 2:r1=0; 2:r3=2; y=2; 26003305:>0:r3=1; 2:r1=1; 2:r3=2; y=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=69a9c426befcce92245a44ffe29944c4 Cycle=Fre SyncsWR Fre LwSyncdWW Rfe SyncdRR Relax acsdrr040 No ACSyncdRR Safe=Fre SyncsWR LwSyncdWW Time acsdrr040 76.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr041.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr041 "Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe SyncdRR" {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) | sync | stw r1,0(r2) | sync ; lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ; li r3,2 | | li r3,2 | ; stw r3,0(r2) | | stw r3,0(r2) | ; exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: sync _litmus_P3_2_: lwz 4,0(9) _litmus_P2_0_: li 6,1 _litmus_P2_1_: stw 6,0(9) _litmus_P2_2_: lwsync _litmus_P2_3_: li 11,2 _litmus_P2_4_: stw 11,0(9) _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 4,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P0_2_: lwsync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test acsdrr041 Allowed Histogram (72 states) 338 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 344 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 9221 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 383 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 263 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 259 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 536 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 22874 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 17632 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 17738 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 22922 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 6599 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 243672:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 34685 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 50999 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 165019:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 191072:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 112714:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 103690:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 36168 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 92797 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 107880:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 468452:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 224021:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 95322 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 1339255:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 1277497:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 111788:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 1312782:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 402898:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 104242:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 490561:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 2648762:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 1027780:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 3741241:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 4461185:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 409244:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 1344275:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 3269223:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 2457987:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 2666183:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 111298:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 103863:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 2343008:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 684830:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 3871354:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 47353 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 1820316:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 2362287:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1116681:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 22245985:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 997927:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 138442:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 258935:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 21364907:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 107421:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 1733067:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 2180891:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 43801553:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 635017:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 1180894:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 4546476:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 22219363:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 3030825:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 53182902:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 1009343:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 1298302:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 21589531:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 17159805:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 21302102:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 17247325:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 21217494:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; No Witnesses Positive: 0, Negative: 320000000 Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=16ba9e829ae27807908998bcbb8a074d Cycle=Fre LwSyncsWW Rfe SyncdRR Fre LwSyncsWW Rfe SyncdRR Relax acsdrr041 No ACSyncdRR Safe=Fre LwSyncsWW Time acsdrr041 94.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/acsdrr042.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC acsdrr042 "Fre SyncdWR Fre LwSyncsWW Rfe SyncdRR" {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) | sync ; sync | lwsync | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,2 | ; | stw r3,0(r2) | ; exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: sync _litmus_P2_2_: lwz 31,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,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test acsdrr042 Allowed Histogram (15 states) 19308 :>0:r3=1; 2:r1=1; 2:r3=0; x=2; 91283 :>0:r3=1; 2:r1=0; 2:r3=1; x=2; 421382:>0:r3=2; 2:r1=0; 2:r3=1; x=2; 417135:>0:r3=1; 2:r1=1; 2:r3=1; x=2; 881413:>0:r3=1; 2:r1=2; 2:r3=1; x=2; 6257733:>0:r3=0; 2:r1=1; 2:r3=1; x=2; 1765362:>0:r3=2; 2:r1=1; 2:r3=0; x=2; 6249393:>0:r3=1; 2:r1=0; 2:r3=0; x=2; 1838781:>0:r3=2; 2:r1=1; 2:r3=1; x=2; 45387243:>0:r3=2; 2:r1=2; 2:r3=0; x=2; 49157268:>0:r3=0; 2:r1=2; 2:r3=1; x=2; 51376228:>0:r3=0; 2:r1=0; 2:r3=0; x=2; 86124233:>0:r3=2; 2:r1=2; 2:r3=1; x=2; 76777757:>0:r3=0; 2:r1=0; 2:r3=1; x=2; 73235481:>0:r3=2; 2:r1=0; 2:r3=0; x=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=072bd75a46e56407102445eff71eb534 Cycle=Fre SyncdWR Fre LwSyncsWW Rfe SyncdRR Relax acsdrr042 No ACSyncdRR Safe=Fre SyncdWR LwSyncsWW Time acsdrr042 77.33 $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 18:59:31 GMT 2009