Raw log

Tue Dec 22 17:39:11 GMT 2009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr000.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr000 "Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr000 Allowed Histogram (22 states) 2 :>3:r1=2; 3:r3=0; x=2; y=2; 1083877:>3:r1=0; 3:r3=1; x=1; y=1; 1159411:>3:r1=0; 3:r3=0; x=2; y=2; 1279765:>3:r1=1; 3:r3=1; x=2; y=2; 2253880:>3:r1=2; 3:r3=1; x=2; y=2; 4091116:>3:r1=2; 3:r3=0; x=2; y=1; 7608628:>3:r1=0; 3:r3=1; x=1; y=2; 6906699:>3:r1=1; 3:r3=0; x=1; y=2; 12177710:>3:r1=2; 3:r3=1; x=1; y=1; 3991249:>3:r1=2; 3:r3=0; x=1; y=2; 11218119:>3:r1=0; 3:r3=1; x=2; y=2; 3913781:>3:r1=1; 3:r3=0; x=1; y=1; 14084053:>3:r1=1; 3:r3=1; x=1; y=2; 10301617:>3:r1=1; 3:r3=1; x=2; y=1; 23873904:>3:r1=1; 3:r3=1; x=1; y=1; 36301745:>3:r1=0; 3:r3=0; x=1; y=1; 39616858:>3:r1=0; 3:r3=0; x=1; y=2; 38456787:>3:r1=2; 3:r3=1; x=2; y=1; 24743064:>3:r1=2; 3:r3=0; x=1; y=1; 20593683:>3:r1=0; 3:r3=0; x=2; y=1; 26593762:>3:r1=2; 3:r3=1; x=1; y=2; 29750290:>3:r1=0; 3:r3=1; x=2; y=1; Ok Witnesses Positive: 2, Negative: 319999998 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=7074ebf0a4e494a7c168353216394741 Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr000 Ok ACLwSyncdRR Safe=Fre Wse SyncdWW Time aclwdrr000 87.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr001.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr001 "Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | sync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr001 Allowed Histogram (22 states) 3 :>3:r1=2; 3:r3=0; x=2; y=2; 4686110:>3:r1=2; 3:r3=0; x=2; y=1; 715520:>3:r1=0; 3:r3=1; x=1; y=1; 1775413:>3:r1=1; 3:r3=1; x=2; y=2; 1761847:>3:r1=0; 3:r3=0; x=2; y=2; 4030259:>3:r1=2; 3:r3=0; x=1; y=2; 3690971:>3:r1=1; 3:r3=0; x=1; y=1; 6073931:>3:r1=0; 3:r3=1; x=1; y=2; 13432493:>3:r1=0; 3:r3=1; x=2; y=2; 6830146:>3:r1=1; 3:r3=0; x=1; y=2; 12589349:>3:r1=1; 3:r3=1; x=2; y=1; 38884646:>3:r1=0; 3:r3=0; x=1; y=2; 3031791:>3:r1=2; 3:r3=1; x=2; y=2; 13766363:>3:r1=1; 3:r3=1; x=1; y=2; 22457802:>3:r1=2; 3:r3=0; x=1; y=1; 32060616:>3:r1=0; 3:r3=0; x=1; y=1; 43291420:>3:r1=2; 3:r3=1; x=2; y=1; 9791571:>3:r1=2; 3:r3=1; x=1; y=1; 29894466:>3:r1=0; 3:r3=1; x=2; y=1; 24032109:>3:r1=0; 3:r3=0; x=2; y=1; 21674307:>3:r1=1; 3:r3=1; x=1; y=1; 25528867:>3:r1=2; 3:r3=1; x=1; y=2; Ok Witnesses Positive: 3, Negative: 319999997 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=42a8ec6eccd807ced6dea1376fc81b0b Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr001 Ok ACLwSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time aclwdrr001 86.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr002.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr002 "Fre SyncdWW Wse Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | | lwz r3,0(r4) ; li r3,1 | | ; stw r3,0(r4) | | ; exists (x=2 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: lwsync _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 aclwdrr002 Allowed Histogram (10 states) 33 :>2:r1=2; 2:r3=0; x=2; 2585350:>2:r1=0; 2:r3=1; x=1; 53214959:>2:r1=0; 2:r3=1; x=2; 101510626:>2:r1=0; 2:r3=0; x=1; 47190552:>2:r1=1; 2:r3=1; x=1; 40961900:>2:r1=2; 2:r3=1; x=2; 54232296:>2:r1=2; 2:r3=1; x=1; 47351768:>2:r1=2; 2:r3=0; x=1; 30691694:>2:r1=0; 2:r3=0; x=2; 22260822:>2:r1=1; 2:r3=1; x=2; Ok Witnesses Positive: 33, Negative: 399999967 Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is validated Hash=e86498b53008de1e6a240afbf078cd14 Cycle=Fre SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr002 Ok ACLwSyncdRR Safe=Fre Wse SyncdWW Time aclwdrr002 69.67 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr003.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr003 "Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr003 Allowed Histogram (22 states) 2 :>0:r3=0; 3:r1=2; 3:r3=0; y=2; 641677:>0:r3=1; 3:r1=0; 3:r3=1; y=1; 5383968:>0:r3=1; 3:r1=0; 3:r3=1; y=2; 13304795:>0:r3=1; 3:r1=1; 3:r3=1; y=2; 2818439:>0:r3=0; 3:r1=2; 3:r3=1; y=2; 29497501:>0:r3=1; 3:r1=0; 3:r3=0; y=1; 6411937:>0:r3=0; 3:r1=2; 3:r3=0; y=1; 7247302:>0:r3=1; 3:r1=1; 3:r3=0; y=2; 4072070:>0:r3=1; 3:r1=1; 3:r3=0; y=1; 19545238:>0:r3=1; 3:r1=1; 3:r3=1; y=1; 13235976:>0:r3=0; 3:r1=1; 3:r3=1; y=1; 36833176:>0:r3=1; 3:r1=0; 3:r3=0; y=2; 8086410:>0:r3=1; 3:r1=2; 3:r3=1; y=1; 2933139:>0:r3=0; 3:r1=0; 3:r3=0; y=2; 30144714:>0:r3=0; 3:r1=0; 3:r3=1; y=1; 43635466:>0:r3=0; 3:r1=2; 3:r3=1; y=1; 1772390:>0:r3=0; 3:r1=1; 3:r3=1; y=2; 24491497:>0:r3=1; 3:r1=2; 3:r3=1; y=2; 28750848:>0:r3=0; 3:r1=0; 3:r3=0; y=1; 14012599:>0:r3=0; 3:r1=0; 3:r3=1; y=2; 4297190:>0:r3=1; 3:r1=2; 3:r3=0; y=2; 22883666:>0:r3=1; 3:r1=2; 3:r3=0; y=1; Ok Witnesses Positive: 2, Negative: 319999998 Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=9599d8c79b2e28a1f015a74966a65bac Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr003 Ok ACLwSyncdRR Safe=Fre Wse SyncdWW SyncdWR Time aclwdrr003 85.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr004.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr004 "Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r2) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr004 Allowed Histogram (42 states) 5 :>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 2 :>0:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 5 :>0:r3=1; 3:r1=2; 3:r3=0; x=2; y=1; 917340:>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 643401:>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 17164 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 54275 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 755330:>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 98437 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 104884:>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2; 2842530:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 1606468:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 635144:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 6648621:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 12198686:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 1797825:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 2625450:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 1698682:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2; 2936675:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 9241705:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1; 6373026:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 1223521:>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 3893086:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 1138118:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 2989707:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 9270451:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 18872476:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2; 4204817:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 7509802:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2; 18052972:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 3170314:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1; 22733888:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; 11522055:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 7075239:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 5640049:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1; 23869003:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 25314673:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 14826225:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 12582357:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 17728710:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 25594753:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 31592129:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; Ok Witnesses Positive: 2, Negative: 319999998 Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=32cc2d7800b6941b57852b520691800f Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr004 Ok ACLwSyncdRR Safe=Fre Wse SyncsWR SyncdWW Time aclwdrr004 81.50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr005.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr005 "Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr005 Allowed Histogram (23 states) 3 :>3:r1=2; 3:r3=0; x=2; y=2; 19 :>3:r1=1; 3:r3=0; x=2; y=1; 1920923:>3:r1=1; 3:r3=1; x=2; y=2; 2945103:>3:r1=2; 3:r3=1; x=2; y=2; 664244:>3:r1=0; 3:r3=1; x=1; y=1; 1400416:>3:r1=0; 3:r3=0; x=2; y=2; 12439437:>3:r1=0; 3:r3=1; x=2; y=2; 5971225:>3:r1=0; 3:r3=1; x=1; y=2; 17062343:>3:r1=1; 3:r3=1; x=1; y=2; 9936513:>3:r1=2; 3:r3=1; x=1; y=1; 12485577:>3:r1=1; 3:r3=0; x=1; y=2; 22344866:>3:r1=1; 3:r3=1; x=1; y=1; 4347263:>3:r1=1; 3:r3=0; x=1; y=1; 6297001:>3:r1=2; 3:r3=0; x=1; y=2; 19678291:>3:r1=0; 3:r3=0; x=2; y=1; 27490907:>3:r1=0; 3:r3=1; x=2; y=1; 23099248:>3:r1=2; 3:r3=0; x=1; y=1; 36713622:>3:r1=0; 3:r3=0; x=1; y=2; 34781456:>3:r1=2; 3:r3=1; x=2; y=1; 3765346:>3:r1=2; 3:r3=0; x=2; y=1; 32703460:>3:r1=0; 3:r3=0; x=1; y=1; 31407636:>3:r1=2; 3:r3=1; x=1; y=2; 12545101:>3:r1=1; 3:r3=1; x=2; y=1; Ok Witnesses Positive: 3, Negative: 319999997 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=4867d1504e0b1c594b9643e48c015b80 Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr005 Ok ACLwSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time aclwdrr005 84.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr006.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr006 "Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | lwsync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr006 Allowed Histogram (24 states) 5 :>3:r1=1; 3:r3=0; x=2; y=2; 36 :>3:r1=1; 3:r3=0; x=2; y=1; 3 :>3:r1=2; 3:r3=0; x=2; y=2; 4082175:>3:r1=1; 3:r3=0; x=1; y=1; 5733549:>3:r1=2; 3:r3=0; x=1; y=2; 2740180:>3:r1=1; 3:r3=1; x=2; y=2; 2025783:>3:r1=0; 3:r3=0; x=2; y=2; 14398902:>3:r1=0; 3:r3=1; x=2; y=2; 4227520:>3:r1=2; 3:r3=0; x=2; y=1; 5105433:>3:r1=0; 3:r3=1; x=1; y=2; 28071050:>3:r1=0; 3:r3=1; x=2; y=1; 465607:>3:r1=0; 3:r3=1; x=1; y=1; 20845368:>3:r1=2; 3:r3=0; x=1; y=1; 20994340:>3:r1=1; 3:r3=1; x=1; y=1; 16438061:>3:r1=1; 3:r3=1; x=1; y=2; 14282731:>3:r1=1; 3:r3=1; x=2; y=1; 8787621:>3:r1=2; 3:r3=1; x=1; y=1; 4167415:>3:r1=2; 3:r3=1; x=2; y=2; 35778469:>3:r1=0; 3:r3=0; x=1; y=2; 30082466:>3:r1=0; 3:r3=0; x=1; y=1; 29945226:>3:r1=2; 3:r3=1; x=1; y=2; 22164315:>3:r1=0; 3:r3=0; x=2; y=1; 11657605:>3:r1=1; 3:r3=0; x=1; y=2; 38006140:>3:r1=2; 3:r3=1; x=2; y=1; Ok Witnesses Positive: 3, Negative: 319999997 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=7e01ecd8b2bc06ff5ba0d2b4e58340c6 Cycle=Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr006 Ok ACLwSyncdRR Safe=Fre Wse LwSyncdWW Time aclwdrr006 86.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr007.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr007 "Fre LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | | lwz r3,0(r4) ; li r3,1 | | ; stw r3,0(r4) | | ; exists (x=2 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: lwsync _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 aclwdrr007 Allowed Histogram (10 states) 42 :>2:r1=2; 2:r3=0; x=2; 1262992:>2:r1=0; 2:r3=1; x=1; 56257420:>2:r1=2; 2:r3=1; x=2; 46783342:>2:r1=2; 2:r3=0; x=1; 40260394:>2:r1=0; 2:r3=1; x=2; 45961394:>2:r1=2; 2:r3=1; x=1; 94671035:>2:r1=0; 2:r3=0; x=1; 44002931:>2:r1=1; 2:r3=1; x=1; 33587964:>2:r1=1; 2:r3=1; x=2; 37212486:>2:r1=0; 2:r3=0; x=2; Ok Witnesses Positive: 42, Negative: 399999958 Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is validated Hash=ba17863040d25a62a648bb8030bf59fd Cycle=Fre LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr007 Ok ACLwSyncdRR Safe=Fre Wse LwSyncdWW Time aclwdrr007 74.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr008.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr008 "Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr008 Allowed Histogram (24 states) 2 :>0:r3=0; 3:r1=1; 3:r3=0; y=2; 2 :>0:r3=0; 3:r1=2; 3:r3=0; y=2; 88 :>0:r3=0; 3:r1=1; 3:r3=0; y=1; 4156041:>0:r3=1; 3:r1=0; 3:r3=1; y=2; 380916:>0:r3=1; 3:r1=0; 3:r3=1; y=1; 15735510:>0:r3=1; 3:r1=1; 3:r3=1; y=2; 14982804:>0:r3=0; 3:r1=0; 3:r3=1; y=2; 21363329:>0:r3=1; 3:r1=2; 3:r3=0; y=1; 2567574:>0:r3=0; 3:r1=1; 3:r3=1; y=2; 3699375:>0:r3=0; 3:r1=2; 3:r3=1; y=2; 7062125:>0:r3=1; 3:r1=2; 3:r3=1; y=1; 38198734:>0:r3=0; 3:r1=2; 3:r3=1; y=1; 3407657:>0:r3=0; 3:r1=0; 3:r3=0; y=2; 18797348:>0:r3=1; 3:r1=1; 3:r3=1; y=1; 6416403:>0:r3=1; 3:r1=2; 3:r3=0; y=2; 4533697:>0:r3=1; 3:r1=1; 3:r3=0; y=1; 33780655:>0:r3=1; 3:r1=0; 3:r3=0; y=2; 28033967:>0:r3=0; 3:r1=0; 3:r3=1; y=1; 26448483:>0:r3=0; 3:r1=0; 3:r3=0; y=1; 29235460:>0:r3=1; 3:r1=2; 3:r3=1; y=2; 5823960:>0:r3=0; 3:r1=2; 3:r3=0; y=1; 15340195:>0:r3=0; 3:r1=1; 3:r3=1; y=1; 27417058:>0:r3=1; 3:r1=0; 3:r3=0; y=1; 12618617:>0:r3=1; 3:r1=1; 3:r3=0; y=2; Ok Witnesses Positive: 2, Negative: 319999998 Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=61bd93196401321b8fb91e15727e3c64 Cycle=Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr008 Ok ACLwSyncdRR Safe=Fre Wse SyncdWR LwSyncdWW Time aclwdrr008 88.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr009.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr009 "Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | | lwz r3,0(r4) ; lwz r3,0(r2) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr009 Allowed Histogram (44 states) 1 :>0:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 2 :>0:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 7 :>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 6 :>0:r3=1; 3:r1=2; 3:r3=0; x=2; y=1; 1 :>0:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 59318 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 24128 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 766180:>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 65120 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 940101:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 1001862:>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 543730:>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 1166103:>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 1414770:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2; 2697714:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 1261628:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 317149:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 4940314:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 3293736:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 115578:>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2; 3850414:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 6090158:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 3653435:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1; 5554567:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 1163912:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 12265894:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 23560960:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 15291809:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 5056772:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 6975483:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2; 15102963:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 11476116:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1; 10146233:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 3798252:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 10607855:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 5004651:>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 9123316:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1; 17065370:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2; 17347000:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 21631824:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 28142535:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; 15984500:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 23273048:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 29225485:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; Ok Witnesses Positive: 1, Negative: 319999999 Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=ab46080bf73ab92da49cdd6b27ede9b2 Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr009 Ok ACLwSyncdRR Safe=Fre Wse SyncsWR LwSyncdWW Time aclwdrr009 86.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr010.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr010 "Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; lwsync | stw r1,0(r2) | lwsync | stw r1,0(r2) ; lwz r3,0(r4) | | lwz r3,0(r4) | ; exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P3_0_: li 8,1 _litmus_P3_1_: stw 8,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: lwsync _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_: lwsync _litmus_P0_2_: lwz 4,0(9) Test aclwdrr010 Allowed Histogram (16 states) 16 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=0; 255875:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 57015841:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 6036588:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 24039092:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 24886214:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 6623156:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 22916416:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 19242913:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 6536360:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 22556867:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 19252025:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 5929719:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 25661155:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 25262916:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 53784847:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 16, Negative: 319999984 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=8ce05c9f86d49b2adfd5546bd471aa44 Cycle=Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr010 Ok ACLwSyncdRR Safe=Fre Time aclwdrr010 77.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr011.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr011 "Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; sync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,1 | | | ; stw r3,0(r4) | | | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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_: lwsync _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 aclwdrr011 Allowed Histogram (15 states) 974421:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 6586700:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 2270439:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 12554772:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 2409125:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 13024093:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 1341241:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 20791040:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 30490013:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 28614097:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 30556930:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 37803748:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 63128089:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 32489164:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 36966128:>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=064d7a96bedb614c156f5bd3adf783d8 Cycle=Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr011 No ACLwSyncdRR Safe=Fre SyncdWW Time aclwdrr011 83.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr012.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr012 "Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; sync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,2 | | | ; stw r3,0(r2) | | | ; exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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_: lwsync _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 aclwdrr012 Allowed Histogram (35 states) 2 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 9 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 4157 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 155683:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 107030:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 2906757:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 467354:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 928459:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 3534859:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 1958664:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 2340245:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 4489760:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1148197:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 5630265:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 2219855:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 1309409:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 2307933:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 5105752:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 12267412:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 897236:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 4940450:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 6869241:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 2626556:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 2848899:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 19601778:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 18772232:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 26917430:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 20264430:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 21572821:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 4488519:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 39619188:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 19320775:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 20815940:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 4561730:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 59000973:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; Ok Witnesses Positive: 2, Negative: 319999998 Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=992754280de579a7f5feb516274ac846 Cycle=Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr012 Ok ACLwSyncdRR Safe=Fre SyncsWW Time aclwdrr012 84.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr013.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr013 "Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,1 | | | ; stw r3,0(r4) | | | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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_: lwsync _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 aclwdrr013 Allowed Histogram (16 states) 40 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; 1180191:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 1556288:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 2664438:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 15090759:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 17075899:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 35463082:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 6112266:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 28427314:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 3995799:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 26556936:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 21685931:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 26358223:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 61522102:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 30250544:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 42060188:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; Ok Witnesses Positive: 40, Negative: 319999960 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=4eddb3c8ea9ccf8a71927b2e31094cad Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr013 Ok ACLwSyncdRR Safe=Fre LwSyncdWW Time aclwdrr013 84.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr014.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr014 "Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,2 | | | ; stw r3,0(r2) | | | ; exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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_: lwsync _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 aclwdrr014 Allowed Histogram (36 states) 1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 9 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 3 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 1129 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 61097 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 245243:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 1181965:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 490443:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 131601:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 144262:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 1157445:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 2534854:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 884861:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 145162:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 1927758:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1257521:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 1078884:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 2708349:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 783052:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 1985053:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 1852289:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 16455460:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 4405946:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 23811073:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 5673745:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 423750:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 19364716:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 5810088:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 23737182:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 6248905:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 22419977:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 24553624:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 23100699:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 21697308:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 46299160:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 57427386:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; Ok Witnesses Positive: 3, Negative: 319999997 Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=0363e525d1d5c107b6654781a780ef6a Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr014 Ok ACLwSyncdRR Safe=Fre LwSyncsWW Time aclwdrr014 81.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr015.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr015 "Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; li r3,1 | lwz r3,0(r4) | | ; stw r3,0(r4) | | | ; exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr015 Allowed Histogram (16 states) 5 :>1:r3=0; 3:r1=1; 3:r3=0; x=2; 415210:>1:r3=1; 3:r1=0; 3:r3=1; x=1; 2635982:>1:r3=0; 3:r1=0; 3:r3=0; x=2; 5089925:>1:r3=0; 3:r1=1; 3:r3=1; x=2; 27585589:>1:r3=0; 3:r1=1; 3:r3=1; x=1; 5978117:>1:r3=0; 3:r1=1; 3:r3=0; x=1; 23212474:>1:r3=1; 3:r1=0; 3:r3=1; x=2; 27624325:>1:r3=1; 3:r1=1; 3:r3=0; x=1; 19789194:>1:r3=1; 3:r1=0; 3:r3=0; x=2; 4158546:>1:r3=1; 3:r1=1; 3:r3=0; x=2; 27858411:>1:r3=1; 3:r1=0; 3:r3=0; x=1; 29831115:>1:r3=1; 3:r1=1; 3:r3=1; x=1; 22016435:>1:r3=0; 3:r1=0; 3:r3=1; x=1; 46961903:>1:r3=1; 3:r1=1; 3:r3=1; x=2; 19256537:>1:r3=0; 3:r1=0; 3:r3=1; x=2; 57586232:>1:r3=0; 3:r1=0; 3:r3=0; x=1; Ok Witnesses Positive: 5, Negative: 319999995 Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=61d664ae95ff6d97da76ebb37bc47ca3 Cycle=Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr015 Ok ACLwSyncdRR Safe=Fre Wse SyncdWW SyncdWR Time aclwdrr015 84.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr016.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr016 "Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | sync | | lwz r3,0(r4) ; li r3,1 | lwz r3,0(r4) | | ; stw r3,0(r4) | | | ; exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr016 Allowed Histogram (16 states) 4 :>1:r3=0; 3:r1=1; 3:r3=0; x=2; 263624:>1:r3=1; 3:r1=0; 3:r3=1; x=1; 3699260:>1:r3=0; 3:r1=0; 3:r3=0; x=2; 23593788:>1:r3=1; 3:r1=0; 3:r3=1; x=2; 20287812:>1:r3=0; 3:r1=0; 3:r3=1; x=1; 52403615:>1:r3=1; 3:r1=1; 3:r3=1; x=2; 5804840:>1:r3=0; 3:r1=1; 3:r3=0; x=1; 22324162:>1:r3=1; 3:r1=0; 3:r3=0; x=2; 4785876:>1:r3=1; 3:r1=1; 3:r3=0; x=2; 22062444:>1:r3=0; 3:r1=0; 3:r3=1; x=2; 26402508:>1:r3=0; 3:r1=1; 3:r3=1; x=1; 24931007:>1:r3=1; 3:r1=1; 3:r3=0; x=1; 55610386:>1:r3=0; 3:r1=0; 3:r3=0; x=1; 25054920:>1:r3=1; 3:r1=0; 3:r3=0; x=1; 26589015:>1:r3=1; 3:r1=1; 3:r3=1; x=1; 6186739:>1:r3=0; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 4, Negative: 319999996 Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=4947e9ed11cb60630be5b54900bf7b6c Cycle=Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr016 Ok ACLwSyncdRR Safe=Fre Wse SyncdWR LwSyncdWW Time aclwdrr016 82.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr017.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr017 "Fre SyncdWR Fre Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | | lwz r3,0(r4) ; lwz r3,0(r4) | | ; exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: lwsync _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 aclwdrr017 Allowed Histogram (8 states) 85 :>0:r3=0; 2:r1=1; 2:r3=0; 772688:>0:r3=1; 2:r1=0; 2:r3=1; 52863656:>0:r3=0; 2:r1=1; 2:r3=1; 86813163:>0:r3=1; 2:r1=1; 2:r3=1; 81633632:>0:r3=1; 2:r1=0; 2:r3=0; 49919104:>0:r3=1; 2:r1=1; 2:r3=0; 76996242:>0:r3=0; 2:r1=0; 2:r3=1; 51001430:>0:r3=0; 2:r1=0; 2:r3=0; Ok Witnesses Positive: 85, Negative: 399999915 Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=0dd8df1959f84e11508b32d374a44775 Cycle=Fre SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr017 Ok ACLwSyncdRR Safe=Fre SyncdWR Time aclwdrr017 70.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr018.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr018 "Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r4) | lwz r3,0(r4) | | ; exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr018 Allowed Histogram (16 states) 7 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=0; 207199:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; 22115661:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; 6315112:>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1; 52356026:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; 6082073:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0; 21922282:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; 24791114:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; 26619001:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; 24334694:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; 18450541:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; 6853884:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0; 55300060:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; 23000557:>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1; 5893322:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0; 25758467:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; Ok Witnesses Positive: 7, Negative: 319999993 Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=3fed6cc74892902ab28df779672578f8 Cycle=Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr018 Ok ACLwSyncdRR Safe=Fre SyncdWR Time aclwdrr018 84.62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr019.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr019 "Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r2) | lwz r3,0(r4) | | ; exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr019 Allowed Histogram (35 states) 1 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 1 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 9 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0; y=1; 21 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 873007:>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 29080 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 37221 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 47371 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 530341:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1; 172161:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1; 105742:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1231081:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 1714583:>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 2149657:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 1895145:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 6214666:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 1339337:>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 6276110:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 18586648:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1; 9525693:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1; 19431721:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1; 19245856:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1; 24707089:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1; 13284027:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1; 5199571:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1; 28720296:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 8021696:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 3146641:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 14138109:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 19557802:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 8099646:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 19866311:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1; 34197786:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 22231934:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 29423640:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1; Ok Witnesses Positive: 1, Negative: 319999999 Condition exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=660c5e262906b3ab9066962d8bf69882 Cycle=Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr019 Ok ACLwSyncdRR Safe=Fre SyncsWR SyncdWR Time aclwdrr019 84.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr020.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr020 "Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r4) | lwz r3,0(r2) | | ; exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: lwsync _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 aclwdrr020 Allowed Histogram (54 states) 1 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; 12 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0; x=1; 18 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 4 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; 3 :>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; 17 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; 4 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; 106 :>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; 239 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=1; 24321 :>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 66039 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 7016 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 129385:>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 597784:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 127192:>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 78744 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 429248:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 2682042:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 87321 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 169807:>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 217171:>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; 2541431:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 2987887:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 1585911:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 6558 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; 6298447:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1; 108023:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 17589180:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 10663995:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 6367838:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 9184584:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 13792308:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 16529916:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; 9287204:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 2515718:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 1844429:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 20612740:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 18668333:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 3168846:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 1321607:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; 10041007:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 17024764:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 15366735:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 17206063:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 18715961:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 20420854:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 7529593:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 6685548:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; 15256472:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 7090764:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 11989245:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 10237692:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 7077377:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 5666496:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; Ok Witnesses Positive: 4, Negative: 319999996 Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=bad92812900a1656a66221eff19f711e Cycle=Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR Relax aclwdrr020 Ok ACLwSyncdRR Safe=Fre SyncsWR SyncdWR Time aclwdrr020 84.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr021.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr021 "Fre SyncdWW Wse SyncdWW Rfe LwSyncdRR" {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) | lwsync ; 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_: lwsync _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 aclwdrr021 Allowed Histogram (7 states) 13203864:>2:r1=0; 2:r3=1; x=1; 9399127:>2:r1=1; 2:r3=1; x=2; 35045359:>2:r1=0; 2:r3=0; x=2; 16152874:>2:r1=1; 2:r3=0; x=1; 134985705:>2:r1=0; 2:r3=0; x=1; 108507764:>2:r1=0; 2:r3=1; x=2; 82705307:>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=aeec733dac4af8be94573c9aff9d0c10 Cycle=Fre SyncdWW Wse SyncdWW Rfe LwSyncdRR Relax aclwdrr021 No ACLwSyncdRR Safe=Fre Wse SyncdWW Time aclwdrr021 75.22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr022.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr022 "Fre LwSyncdWW Wse SyncdWW Rfe LwSyncdRR" {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) | lwsync ; 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_: lwsync _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 aclwdrr022 Allowed Histogram (7 states) 10020320:>2:r1=0; 2:r3=1; x=1; 12190912:>2:r1=1; 2:r3=1; x=2; 38733758:>2:r1=0; 2:r3=0; x=2; 76512959:>2:r1=1; 2:r3=1; x=1; 116080818:>2:r1=0; 2:r3=1; x=2; 130932903:>2:r1=0; 2:r3=0; x=1; 15528330:>2:r1=1; 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=fb989d16658311d76866354f8a671029 Cycle=Fre LwSyncdWW Wse SyncdWW Rfe LwSyncdRR Relax aclwdrr022 No ACLwSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time aclwdrr022 75.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr023.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr023 "Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync ; 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_: lwsync _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 aclwdrr023 Allowed Histogram (3 states) 222420686:>1:r1=1; 1:r3=1; 319325764:>1:r1=0; 1:r3=0; 98253550:>1:r1=0; 1:r3=1; No Witnesses Positive: 0, Negative: 640000000 Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated Hash=501f8f5a33589295352fe1de9678142b Cycle=Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr023 No ACLwSyncdRR Safe=Fre SyncdWW Time aclwdrr023 72.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr024.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr024 "Fre SyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; 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_: lwsync _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_: lwsync _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 aclwdrr024 Allowed Histogram (15 states) 733603:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 5296411:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 480182:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 515810:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 844297:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 12651120:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 32946526:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 48180518:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 11976966:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 49611664:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 13083465:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 19992240:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 13345706:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 34054883:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 76286609:>1:r1=0; 1:r3=0; 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=d941e505b27c9a2748aeb4651a9cb643 Cycle=Fre SyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr024 No ACLwSyncdRR Safe=Fre SyncdWW Time aclwdrr024 91.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr025.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr025 "Fre SyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; 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_: lwsync _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_: lwsync _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 aclwdrr025 Allowed Histogram (34 states) 1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 573 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 931502:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 540922:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 653305:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 1008429:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 937265:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 1834839:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 904232:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 822778:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 3525328:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 3810768:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 756655:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 1213954:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 4428289:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 1342843:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 7270801:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 2404962:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 874624:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 3059482:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 33317151:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 21740773:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 5010136:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 745974:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 8141076:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 24051728:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 66290856:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 21370664:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 1085292:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 13565069:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 32203330:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 28155181:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 10503462:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 17497756:>1:r1=0; 1:r3=1; 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=32b005fb973345d626b38029866e06f9 Cycle=Fre SyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr025 No ACLwSyncdRR Safe=Fre SyncsWW SyncdWW Time aclwdrr025 89.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr026.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr026 "Fre LwSyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; 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_: lwsync _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_: lwsync _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 aclwdrr026 Allowed Histogram (16 states) 5 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; 681020:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 1020755:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 501522:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 1405752:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 10728339:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 11705715:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 4342105:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 31041309:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 47080804:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 15866854:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 20078807:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 41708447:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 23172672:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 36980689:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 73685205:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; Ok Witnesses Positive: 5, Negative: 319999995 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=7a7cbc5359389bdb4170629397f77be6 Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr026 Ok ACLwSyncdRR Safe=Fre SyncdWW LwSyncdWW Time aclwdrr026 90.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr027.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr027 "Fre LwSyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; 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_: lwsync _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_: lwsync _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 aclwdrr027 Allowed Histogram (33 states) 166 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 234381:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 456512:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 200824:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 302352:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 118588:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 386670:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 1121208:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 1959726:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 3487854:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 275831:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 560501:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 1328939:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 1354998:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 4264038:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 2423892:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 1772310:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 2615533:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 10660468:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 31009284:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 1581000:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 319801:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 4523840:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 25964165:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 19453371:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 934918:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 11776436:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 63493113:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 31451850:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 1688748:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 27668990:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 29348354:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 37261339:>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=c2a2e1328465d78b88dcae553e33604e Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr027 No ACLwSyncdRR Safe=Fre SyncdWW LwSyncsWW Time aclwdrr027 89.95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr028.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr028 "Fre SyncdWR Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync ; 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_: lwsync _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 aclwdrr028 Allowed Histogram (7 states) 6887826:>0:r3=1; 2:r1=0; 2:r3=1; 16669072:>0:r3=0; 2:r1=1; 2:r3=1; 16374037:>0:r3=1; 2:r1=1; 2:r3=0; 117780227:>0:r3=1; 2:r1=0; 2:r3=0; 114868565:>0:r3=0; 2:r1=0; 2:r3=1; 53435546:>0:r3=0; 2:r1=0; 2:r3=0; 73984727:>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=eebdc6b096cdd9c24f38c118593f06bb Cycle=Fre SyncdWR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr028 No ACLwSyncdRR Safe=Fre SyncdWW SyncdWR Time aclwdrr028 75.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr029.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr029 "Fre SyncsWR Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync ; 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_: lwsync _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 aclwdrr029 Allowed Histogram (13 states) 2099587:>0:r3=2; 2:r1=1; 2:r3=2; y=2; 118948:>0:r3=2; 2:r1=0; 2:r3=1; y=2; 1119097:>0:r3=2; 2:r1=0; 2:r3=2; y=2; 8792527:>0:r3=1; 2:r1=0; 2:r3=1; y=1; 8231970:>0:r3=2; 2:r1=0; 2:r3=0; y=2; 69748406:>0:r3=1; 2:r1=1; 2:r3=1; y=1; 13995264:>0:r3=1; 2:r1=1; 2:r3=2; y=2; 41146625:>0:r3=1; 2:r1=0; 2:r3=2; y=1; 54001175:>0:r3=1; 2:r1=0; 2:r3=2; y=2; 58306300:>0:r3=1; 2:r1=0; 2:r3=0; y=2; 63437081:>0:r3=1; 2:r1=0; 2:r3=1; y=2; 13862829:>0:r3=1; 2:r1=1; 2:r3=2; y=1; 65140191:>0:r3=1; 2:r1=0; 2:r3=0; 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=4ab12861c7fd48307d5dbbb06073fa65 Cycle=Fre SyncsWR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr029 No ACLwSyncdRR Safe=Fre SyncsWR SyncdWW Time aclwdrr029 75.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr030.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr030 "Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; sync | lwz r3,0(r4) | 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_: lwsync _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_: lwsync _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 aclwdrr030 Allowed Histogram (76 states) 1 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 2 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 3 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 1458 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 1429 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 1431 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 8736 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 1632 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 2505 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 2282 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 10831 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 271595:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 106830:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 24520 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 289232:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 311932:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 229785:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 953712:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 74580 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 26675 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 714055:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 106444:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 1024705:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 255274:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 710123:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 807352:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 1309289:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 199235:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 586500:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 2631980:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 1717815:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 308254:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 756868:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 2084242:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 1614454:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 3794670:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 4105346:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 268876:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 301928:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 197268:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 1275589:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 1756162:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 774220:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 542482:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 1246749:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 5670518:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 2938841:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 13208169:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 218711:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 1222345:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 1690749:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 4215130:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 3842208:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 2777955:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 2158778:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 17795662:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 2168860:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 5389518:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 15680848:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 3865486:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 2167437:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 4333053:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 3627535:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 3529931:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 710610:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 20748282:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 59903322:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 17564901:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 33012614:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 2959969:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 13072793:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 4082606:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 16172733:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 20345618:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 3515766:>1:r1=2; 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=ee8538d5ca48a381e732df1d7c7a6726 Cycle=Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Relax aclwdrr030 No ACLwSyncdRR Safe=Fre SyncsWW Time aclwdrr030 96.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr031.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr031 "Fre LwSyncdWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | 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_: lwsync _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_: lwsync _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 aclwdrr031 Allowed Histogram (36 states) 14 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; y=2; 2 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; y=2; 14 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 725 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 420169:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 981920:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; y=2; 893295:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 993411:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; y=2; 1331656:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 774736:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 1579501:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 2157735:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 3504987:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; y=2; 1199450:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; y=2; 783642:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; y=2; 989895:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 4940489:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; y=2; 1703918:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; y=2; 1259789:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; y=2; 1466870:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 2450750:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; y=2; 7089636:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 17882666:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; y=2; 7762057:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 19202280:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; y=2; 4926911:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 19217772:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 4347063:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; y=2; 19587083:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; y=2; 30209934:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; y=2; 11647907:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; y=2; 29149494:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 21922136:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; y=2; 65158899:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 32075672:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; y=2; 2387522:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; y=2; Ok Witnesses Positive: 14, Negative: 319999986 Condition exists (y=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=7e70701bff0ff65c82954a7448132407 Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Relax aclwdrr031 Ok ACLwSyncdRR Safe=Fre SyncsWW LwSyncdWW Time aclwdrr031 90.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr032.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr032 "Fre LwSyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | 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_: lwsync _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_: lwsync _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 aclwdrr032 Allowed Histogram (75 states) 1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 6 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 328 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 279 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 3971 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 1273 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 1686 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 3278 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 2643 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 26884 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 520 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 8577 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 59997 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 112054:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 55960 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 178225:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 240305:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 320500:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 248589:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 47604 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 32358 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 271801:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 67181 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 332981:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 271126:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 834283:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 241692:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 559656:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 162455:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 2131642:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 68263 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 101057:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 402349:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 371999:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 2125264:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 129262:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 1027030:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 1061502:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 1880892:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 2207469:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 1163388:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 1224391:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 775676:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 146158:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 2592533:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 3255950:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 817179:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 5282839:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 3002953:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 1310550:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 1727909:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 363114:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 2254265:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 1741327:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 3835900:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 5358710:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 5476403:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 5159903:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 18084567:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 17343107:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 2617087:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 3561141:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 16788876:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 18539040:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 2348430:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 20886263:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 797329:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 4580793:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 12030586:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 37813468:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 57842124:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 3551510:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 23597220:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 18536368:>1:r1=0; 1:r3=0; 3:r1=2; 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=74930e6bce52d51f9df9817f8385847f Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Relax aclwdrr032 No ACLwSyncdRR Safe=Fre SyncsWW LwSyncsWW Time aclwdrr032 96.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr033.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr033 "Fre SyncdWR Fre SyncsWW Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | 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_: lwsync _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 aclwdrr033 Allowed Histogram (17 states) 25 :>0:r3=1; 2:r1=2; 2:r3=0; x=2; 69 :>0:r3=0; 2:r1=1; 2:r3=0; x=2; 289349:>0:r3=1; 2:r1=1; 2:r3=0; x=2; 2238842:>0:r3=1; 2:r1=1; 2:r3=1; x=2; 297062:>0:r3=1; 2:r1=0; 2:r3=1; x=2; 247507:>0:r3=2; 2:r1=0; 2:r3=1; x=2; 3302138:>0:r3=1; 2:r1=2; 2:r3=1; x=2; 2744269:>0:r3=2; 2:r1=1; 2:r3=1; x=2; 37593079:>0:r3=2; 2:r1=2; 2:r3=0; x=2; 53183117:>0:r3=0; 2:r1=0; 2:r3=0; x=2; 16195081:>0:r3=0; 2:r1=1; 2:r3=1; x=2; 8385830:>0:r3=2; 2:r1=1; 2:r3=0; x=2; 17775671:>0:r3=1; 2:r1=0; 2:r3=0; x=2; 38077045:>0:r3=0; 2:r1=2; 2:r3=1; x=2; 82229842:>0:r3=2; 2:r1=2; 2:r3=1; x=2; 76228695:>0:r3=0; 2:r1=0; 2:r3=1; x=2; 61212379:>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=9aeeb761b71ddabb3db56388750f2a1a Cycle=Fre SyncdWR Fre SyncsWW Rfe LwSyncdRR Relax aclwdrr033 No ACLwSyncdRR Safe=Fre SyncsWW SyncdWR Time aclwdrr033 76.98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr034.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr034 "Fre SyncdWW Wse LwSyncdWW Rfe LwSyncdRR" {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) | lwsync ; 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_: lwsync _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 aclwdrr034 Allowed Histogram (8 states) 124 :>2:r1=1; 2:r3=0; x=2; 7548577:>2:r1=0; 2:r3=1; x=1; 35168671:>2:r1=0; 2:r3=0; x=2; 12687420:>2:r1=1; 2:r3=1; x=2; 28364147:>2:r1=1; 2:r3=0; x=1; 104551695:>2:r1=0; 2:r3=1; x=2; 121179237:>2:r1=0; 2:r3=0; x=1; 90500129:>2:r1=1; 2:r3=1; x=1; Ok Witnesses Positive: 124, Negative: 399999876 Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=10939fdb629e01d3ec7a75f951037026 Cycle=Fre SyncdWW Wse LwSyncdWW Rfe LwSyncdRR Relax aclwdrr034 Ok ACLwSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time aclwdrr034 77.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr035.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr035 "Fre LwSyncdWW Wse LwSyncdWW Rfe LwSyncdRR" {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) | lwsync ; 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_: lwsync _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 aclwdrr035 Allowed Histogram (8 states) 94 :>2:r1=1; 2:r3=0; x=2; 38555216:>2:r1=0; 2:r3=0; x=2; 4846481:>2:r1=0; 2:r3=1; x=1; 27654304:>2:r1=1; 2:r3=0; x=1; 111320893:>2:r1=0; 2:r3=1; x=2; 116544681:>2:r1=0; 2:r3=0; x=1; 84467291:>2:r1=1; 2:r3=1; x=1; 16611040:>2:r1=1; 2:r3=1; x=2; Ok Witnesses Positive: 94, Negative: 399999906 Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=b62ccd86d3f88c50d13b5221a86b68a5 Cycle=Fre LwSyncdWW Wse LwSyncdWW Rfe LwSyncdRR Relax aclwdrr035 Ok ACLwSyncdRR Safe=Fre Wse LwSyncdWW Time aclwdrr035 75.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr036.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr036 "Fre LwSyncdWW Rfe LwSyncdRR" {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) | lwsync ; 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_: lwsync _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 aclwdrr036 Allowed Histogram (3 states) 41207261:>1:r1=0; 1:r3=1; 319426918:>1:r1=0; 1:r3=0; 279365821:>1:r1=1; 1:r3=1; No Witnesses Positive: 0, Negative: 640000000 Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated Hash=25520ac6610aa6339bae2caee0005d5b Cycle=Fre LwSyncdWW Rfe LwSyncdRR Relax aclwdrr036 No ACLwSyncdRR Safe=Fre LwSyncdWW Time aclwdrr036 72.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr037.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr037 "Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; 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_: lwsync _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_: lwsync _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 aclwdrr037 Allowed Histogram (16 states) 17 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; 1216652:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 1290201:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 1224664:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 14736499:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 39093055:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 32366301:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3361138:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 40006086:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 28782529:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 71743708:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 18399360:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 17699863:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 15446143:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 33485314:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 1148470:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; Ok Witnesses Positive: 17, Negative: 319999983 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=e45e2fb06db799317c9d3aeed10f6d45 Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Relax aclwdrr037 Ok ACLwSyncdRR Safe=Fre LwSyncdWW Time aclwdrr037 94.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr038.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr038 "Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; 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_: lwsync _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_: lwsync _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 aclwdrr038 Allowed Histogram (36 states) 4 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 5 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 43 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 552 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 196049:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 122989:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 699147:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 1663640:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 611792:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 2568354:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 363968:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 142463:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 2427449:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 2118111:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 186870:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 601536:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 2962590:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 370961:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 1030052:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 1978649:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 3606459:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 641517:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 1168906:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 3345164:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 19525624:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 1637302:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 33566271:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 26214430:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 37310892:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 61730019:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 4546770:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 13050811:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 27994624:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 24547910:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 25724728:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 17343349:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; Ok Witnesses Positive: 43, Negative: 319999957 Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=459d76f119641ec12aab94d071c86542 Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Relax aclwdrr038 Ok ACLwSyncdRR Safe=Fre LwSyncsWW LwSyncdWW Time aclwdrr038 90.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr039.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr039 "Fre SyncdWR Fre LwSyncdWW Rfe LwSyncdRR" {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) | lwsync ; 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_: lwsync _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 aclwdrr039 Allowed Histogram (8 states) 82 :>0:r3=0; 2:r1=1; 2:r3=0; 105238437:>0:r3=1; 2:r1=0; 2:r3=0; 3414681:>0:r3=1; 2:r1=0; 2:r3=1; 80145622:>0:r3=1; 2:r1=1; 2:r3=1; 110666645:>0:r3=0; 2:r1=0; 2:r3=1; 20453432:>0:r3=0; 2:r1=1; 2:r3=1; 27793672:>0:r3=1; 2:r1=1; 2:r3=0; 52287429:>0:r3=0; 2:r1=0; 2:r3=0; Ok Witnesses Positive: 82, Negative: 399999918 Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=9adf86efa9ed99398ed262e7a29cb549 Cycle=Fre SyncdWR Fre LwSyncdWW Rfe LwSyncdRR Relax aclwdrr039 Ok ACLwSyncdRR Safe=Fre SyncdWR LwSyncdWW Time aclwdrr039 75.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr040.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr040 "Fre SyncsWR Fre LwSyncdWW Rfe LwSyncdRR" {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) | lwsync ; 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_: lwsync _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 aclwdrr040 Allowed Histogram (13 states) 2530591:>0:r3=2; 2:r1=1; 2:r3=2; y=2; 121092:>0:r3=2; 2:r1=0; 2:r3=1; y=2; 3083892:>0:r3=1; 2:r1=0; 2:r3=1; y=1; 8367925:>0:r3=2; 2:r1=0; 2:r3=0; y=2; 65988194:>0:r3=1; 2:r1=0; 2:r3=0; y=1; 1118913:>0:r3=2; 2:r1=0; 2:r3=2; y=2; 62604275:>0:r3=1; 2:r1=0; 2:r3=1; y=2; 26181012:>0:r3=1; 2:r1=1; 2:r3=2; y=1; 49045481:>0:r3=1; 2:r1=0; 2:r3=2; y=2; 27005895:>0:r3=1; 2:r1=0; 2:r3=2; y=1; 57175058:>0:r3=1; 2:r1=0; 2:r3=0; y=2; 19507743:>0:r3=1; 2:r1=1; 2:r3=2; y=2; 77269929:>0:r3=1; 2:r1=1; 2:r3=1; 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=1a7c6d1dc4425965c5dae6a980780759 Cycle=Fre SyncsWR Fre LwSyncdWW Rfe LwSyncdRR Relax aclwdrr040 No ACLwSyncdRR Safe=Fre SyncsWR LwSyncdWW Time aclwdrr040 76.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr041.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr041 "Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | 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_: lwsync _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_: lwsync _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 aclwdrr041 Allowed Histogram (78 states) 1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 2 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 2 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 2 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 4 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 2 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 295 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 282 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 316 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 4343 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 669 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 1070 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 8467 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 12975 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 251 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 707 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 13959 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 11633 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 11626 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 89414 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 8335 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 356211:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 211521:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 220442:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 85813 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 117153:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 372145:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 130073:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 115546:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 155543:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 98775 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 362292:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 71479 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 219483:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 1221128:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 39462 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 1160298:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 80513 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 989872:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 716828:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 99997 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 1211920:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 5034487:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 1921332:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 23063794:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 2685981:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 1891782:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 106974:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 82896 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 1185775:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 993537:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 1167489:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 39775 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 100051:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 380689:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 2584538:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 2561552:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 19873838:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 4998094:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 1972741:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 43293755:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 1996288:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 4989907:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 19317449:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 16132155:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 755131:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 2862945:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 1935496:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 22346671:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 16261994:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 23329869:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 4899836:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 968520:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 55684228:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 1885785:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 886184:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 22211442:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 1396171:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; Ok Witnesses Positive: 2, Negative: 319999998 Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is validated Hash=f658f820f1d5e1aea992b078ad3de29c Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW Rfe LwSyncdRR Relax aclwdrr041 Ok ACLwSyncdRR Safe=Fre LwSyncsWW Time aclwdrr041 93.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr042.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr042 "Fre SyncdWR Fre LwSyncsWW Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | 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_: lwsync _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 aclwdrr042 Allowed Histogram (18 states) 6 :>0:r3=0; 2:r1=1; 2:r3=0; x=2; 13 :>0:r3=0; 2:r1=2; 2:r3=0; x=2; 1734 :>0:r3=1; 2:r1=2; 2:r3=0; x=2; 386043:>0:r3=2; 2:r1=0; 2:r3=1; x=2; 83823 :>0:r3=1; 2:r1=0; 2:r3=1; x=2; 932784:>0:r3=1; 2:r1=2; 2:r3=1; x=2; 28345 :>0:r3=1; 2:r1=1; 2:r3=0; x=2; 2182860:>0:r3=2; 2:r1=1; 2:r3=0; x=2; 440626:>0:r3=1; 2:r1=1; 2:r3=1; x=2; 1642877:>0:r3=2; 2:r1=1; 2:r3=1; x=2; 6619671:>0:r3=0; 2:r1=1; 2:r3=1; x=2; 47099765:>0:r3=2; 2:r1=2; 2:r3=0; x=2; 48207572:>0:r3=0; 2:r1=2; 2:r3=1; x=2; 6460701:>0:r3=1; 2:r1=0; 2:r3=0; x=2; 52065151:>0:r3=0; 2:r1=0; 2:r3=0; x=2; 73483985:>0:r3=2; 2:r1=0; 2:r3=0; x=2; 84450831:>0:r3=2; 2:r1=2; 2:r3=1; x=2; 75913213:>0:r3=0; 2:r1=0; 2:r3=1; x=2; Ok Witnesses Positive: 13, Negative: 399999987 Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is validated Hash=9862f681ad48c0682ff709f0b167939f Cycle=Fre SyncdWR Fre LwSyncsWW Rfe LwSyncdRR Relax aclwdrr042 Ok ACLwSyncdRR Safe=Fre SyncdWR LwSyncsWW Time aclwdrr042 80.13 $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:38:40 GMT 2009