Mon Dec 28 11:16:15 GMT 2009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe036.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe036 "SyncdWW Wse SyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;} P0 | P1 ; li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) ; sync | sync ; li r3,1 | li r3,1 ; stw r3,0(r4) | stw r3,0(r4) ; exists (x=2 /\ y=2) Generated assembler _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 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test safe036 Allowed Histogram (3 states) 48560450:>x=1; y=1; 295519368:>x=2; y=1; 295920182:>x=1; y=2; No Witnesses Positive: 0, Negative: 640000000 Condition exists (x=2 /\ y=2) is NOT validated Hash=b13e0c20b3a95ec28cc7a23efa1563b6 Cycle=SyncdWW Wse SyncdWW Wse Relax safe036 No Safe=Wse SyncdWW Time safe036 76.71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe037.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe037 "SyncdWW Wse SyncdWW Wse SyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,2 | li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; sync | sync | sync ; li r3,1 | li r3,1 | li r3,1 ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (x=2 /\ y=2 /\ z=2) Generated assembler _litmus_P2_0_: li 5,2 _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_: 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 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test safe037 Allowed Histogram (7 states) 6456410:>x=1; y=1; z=1; 23679741:>x=2; y=2; z=1; 23603928:>x=2; y=1; z=2; 107479688:>x=1; y=2; z=1; 107390947:>x=2; y=1; z=1; 107519380:>x=1; y=1; z=2; 23869906:>x=1; y=2; z=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated Hash=29e092e26d25015c351a682f181e1b0f Cycle=SyncdWW Wse SyncdWW Wse SyncdWW Wse Relax safe037 No Safe=Wse SyncdWW Time safe037 74.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe038.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe038 "LwSyncdWW Wse SyncdWW Wse SyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,2 | li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; sync | sync | lwsync ; li r3,1 | li r3,1 | li r3,1 ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (x=2 /\ y=2 /\ z=2) Generated assembler _litmus_P2_0_: li 5,2 _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_: 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 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test safe038 Allowed Histogram (7 states) 112429352:>x=2; y=1; z=1; 22752092:>x=1; y=2; z=2; 26617479:>x=2; y=1; z=2; 5481657:>x=1; y=1; z=1; 29406373:>x=2; y=2; z=1; 100012740:>x=1; y=2; z=1; 103300307:>x=1; y=1; z=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated Hash=9fdaf07975754951c834724222b34025 Cycle=LwSyncdWW Wse SyncdWW Wse SyncdWW Wse Relax safe038 No Safe=Wse SyncdWW LwSyncdWW Time safe038 79.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe040.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe040 "SyncdWR Fre SyncdWW Wse SyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,1 | li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; sync | sync | sync ; li r3,1 | li r3,1 | lwz r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | ; exists (y=2 /\ z=2 /\ 2:r3=0) Generated assembler _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,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 4,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test safe040 Allowed Histogram (7 states) 3504011:>2:r3=1; y=1; z=1; 39145465:>2:r3=0; y=1; z=2; 23778105:>2:r3=1; y=2; z=2; 33126923:>2:r3=0; y=2; z=1; 112257508:>2:r3=0; y=1; z=1; 93111011:>2:r3=1; y=1; z=2; 95076977:>2:r3=1; y=2; z=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (y=2 /\ z=2 /\ 2:r3=0) is NOT validated Hash=60904a5b2739e8950875099ac77c27af Cycle=SyncdWR Fre SyncdWW Wse SyncdWW Wse Relax safe040 No Safe=Fre Wse SyncdWW SyncdWR Time safe040 75.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe045.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe045 "LwSyncdWW Wse SyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;} P0 | P1 ; li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) ; sync | lwsync ; li r3,1 | li r3,1 ; stw r3,0(r4) | stw r3,0(r4) ; exists (x=2 /\ y=2) Generated assembler _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 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test safe045 Allowed Histogram (3 states) 32096337:>x=1; y=1; 295851182:>x=1; y=2; 312052481:>x=2; y=1; No Witnesses Positive: 0, Negative: 640000000 Condition exists (x=2 /\ y=2) is NOT validated Hash=68b87fd4beebe403e166c8646f0170ab Cycle=LwSyncdWW Wse SyncdWW Wse Relax safe045 No Safe=Wse SyncdWW LwSyncdWW Time safe045 78.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe046.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe046 "LwSyncdWW Wse LwSyncdWW Wse SyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,2 | li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwsync | sync | lwsync ; li r3,1 | li r3,1 | li r3,1 ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (x=2 /\ y=2 /\ z=2) Generated assembler _litmus_P2_0_: li 5,2 _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_: 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 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test safe046 Allowed Histogram (7 states) 3843560:>x=1; y=1; z=1; 34336403:>x=2; y=2; z=1; 26197992:>x=2; y=1; z=2; 104807324:>x=1; y=2; z=1; 106495730:>x=2; y=1; z=1; 95606258:>x=1; y=1; z=2; 28712733:>x=1; y=2; z=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated Hash=ef787314c1fb4635934ec5bee20106c0 Cycle=LwSyncdWW Wse LwSyncdWW Wse SyncdWW Wse Relax safe046 No Safe=Wse SyncdWW LwSyncdWW Time safe046 76.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe048.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe048 "SyncdWR Fre LwSyncdWW Wse SyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,1 | li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwsync | sync | sync ; li r3,1 | li r3,1 | lwz r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | ; exists (y=2 /\ z=2 /\ 2:r3=0) Generated assembler _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,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 4,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test safe048 Allowed Histogram (7 states) 2338458:>2:r3=1; y=1; z=1; 30531551:>2:r3=1; y=2; z=2; 38974562:>2:r3=0; y=1; z=2; 107110328:>2:r3=0; y=1; z=1; 85094279:>2:r3=1; y=1; z=2; 97553842:>2:r3=1; y=2; z=1; 38396980:>2:r3=0; y=2; z=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (y=2 /\ z=2 /\ 2:r3=0) is NOT validated Hash=fded52f6a8a54c4d9bf3c0cde8ee353b Cycle=SyncdWR Fre LwSyncdWW Wse SyncdWW Wse Relax safe048 No Safe=Fre Wse SyncdWW SyncdWR LwSyncdWW Time safe048 75.01 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe069.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe069 "SyncdWR Fre SyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;} P0 | P1 ; li r1,1 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) ; sync | sync ; li r3,1 | lwz r3,0(r4) ; stw r3,0(r4) | ; exists (y=2 /\ 1:r3=0) Generated assembler _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 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 safe069 Allowed Histogram (3 states) 34000083:>1:r3=1; y=1; 297763653:>1:r3=1; y=2; 308236264:>1:r3=0; y=1; No Witnesses Positive: 0, Negative: 640000000 Condition exists (y=2 /\ 1:r3=0) is NOT validated Hash=7da20a2ab953c9d18488d3f4e7841bb2 Cycle=SyncdWR Fre SyncdWW Wse Relax safe069 No Safe=Fre Wse SyncdWW SyncdWR Time safe069 79.63 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe070.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe070 "LwSyncdWW Wse SyncdWR Fre SyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,2 | li r1,1 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; sync | sync | lwsync ; lwz r3,0(r4) | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) ; exists (x=2 /\ z=2 /\ 0:r3=0) Generated assembler _litmus_P2_0_: li 5,2 _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_: 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 31,2 _litmus_P0_1_: stw 31,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test safe070 Allowed Histogram (7 states) 2864832:>0:r3=1; x=1; z=1; 27199162:>0:r3=1; x=2; z=2; 95122068:>0:r3=1; x=2; z=1; 104257900:>0:r3=0; x=1; z=1; 47334093:>0:r3=0; x=2; z=1; 32157584:>0:r3=0; x=1; z=2; 91064361:>0:r3=1; x=1; z=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ z=2 /\ 0:r3=0) is NOT validated Hash=41c68cedc1ddadab686061c793b3d241 Cycle=LwSyncdWW Wse SyncdWR Fre SyncdWW Wse Relax safe070 No Safe=Fre Wse SyncdWW SyncdWR LwSyncdWW Time safe070 74.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe072.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe072 "SyncdWR Fre SyncdWR Fre SyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,1 | li r1,1 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; sync | sync | sync ; lwz r3,0(r4) | li r3,1 | lwz r3,0(r4) ; | stw r3,0(r4) | ; exists (z=2 /\ 0:r3=0 /\ 2:r3=0) Generated assembler _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,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 31,1 _litmus_P0_1_: stw 31,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test safe072 Allowed Histogram (7 states) 38983634:>0:r3=1; 2:r3=0; z=2; 33120430:>0:r3=0; 2:r3=1; z=2; 1528304:>0:r3=1; 2:r3=1; z=1; 94312343:>0:r3=1; 2:r3=0; z=1; 99905212:>0:r3=0; 2:r3=1; z=1; 52166848:>0:r3=0; 2:r3=0; z=1; 79983229:>0:r3=1; 2:r3=1; z=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (z=2 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=545ab7a6a327dd4d73e4f0fc0d60719e Cycle=SyncdWR Fre SyncdWR Fre SyncdWW Wse Relax safe072 No Safe=Fre Wse SyncdWW SyncdWR Time safe072 77.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe077.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe077 "SyncdWR Fre SyncsWR Fre SyncdWW Wse" {0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=x;} P0 | P1 | P2 ; li r1,1 | li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; sync | sync | sync ; lwz r3,0(r2) | li r3,1 | lwz r3,0(r4) ; | stw r3,0(r4) | ; exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,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 4,0(9) Test safe077 Allowed Histogram (13 states) 120450:>0:r3=2; 2:r3=1; x=2; y=1; 2834455:>0:r3=2; 2:r3=2; x=2; y=2; 7267682:>0:r3=2; 2:r3=0; x=2; y=1; 1547676:>0:r3=1; 2:r3=1; x=1; y=1; 63347983:>0:r3=1; 2:r3=0; x=1; y=1; 630719:>0:r3=2; 2:r3=2; x=2; y=1; 19414404:>0:r3=1; 2:r3=2; x=1; y=1; 63181155:>0:r3=1; 2:r3=1; x=2; y=1; 79137347:>0:r3=1; 2:r3=1; x=1; y=2; 33707676:>0:r3=1; 2:r3=2; x=2; y=2; 36872194:>0:r3=1; 2:r3=2; x=2; y=1; 36028325:>0:r3=1; 2:r3=2; x=1; y=2; 55909934:>0:r3=1; 2:r3=0; x=2; y=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0) is NOT validated Hash=90440690a11b718ea7844fef30ba96c5 Cycle=SyncdWR Fre SyncsWR Fre SyncdWW Wse Relax safe077 No Safe=Fre Wse SyncsWR SyncdWW SyncdWR Time safe077 76.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe135.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe135 "LwSyncdWW Wse LwSyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;} P0 | P1 ; li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) ; lwsync | lwsync ; li r3,1 | li r3,1 ; stw r3,0(r4) | stw r3,0(r4) ; exists (x=2 /\ y=2) Generated assembler _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 6,2 _litmus_P0_1_: stw 6,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 5,1 _litmus_P0_4_: stw 5,0(9) Test safe135 Allowed Histogram (3 states) 310216154:>x=2; y=1; 312094136:>x=1; y=2; 17689710:>x=1; y=1; No Witnesses Positive: 0, Negative: 640000000 Condition exists (x=2 /\ y=2) is NOT validated Hash=829af8195a1482485057a881cab011a8 Cycle=LwSyncdWW Wse LwSyncdWW Wse Relax safe135 No Safe=Wse LwSyncdWW Time safe135 77.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe136.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe136 "LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,2 | li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwsync | lwsync | lwsync ; li r3,1 | li r3,1 | li r3,1 ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (x=2 /\ y=2 /\ z=2) Generated assembler _litmus_P2_0_: li 5,2 _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_: 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 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test safe136 Allowed Histogram (7 states) 1983907:>x=1; y=1; z=1; 34286675:>x=2; y=2; z=1; 34516054:>x=1; y=2; z=2; 98107492:>x=1; y=1; z=2; 98423295:>x=2; y=1; z=1; 34417524:>x=2; y=1; z=2; 98265053:>x=1; y=2; z=1; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ y=2 /\ z=2) is NOT validated Hash=20a6a34b6dc3f52d89ffdf88575062ca Cycle=LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW Wse Relax safe136 No Safe=Wse LwSyncdWW Time safe136 75.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe138.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe138 "SyncdWR Fre LwSyncdWW Wse LwSyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,1 | li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwsync | lwsync | sync ; li r3,1 | li r3,1 | lwz r3,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | ; exists (y=2 /\ z=2 /\ 2:r3=0) Generated assembler _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,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 4,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: lwsync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test safe138 Allowed Histogram (7 states) 1243675:>2:r3=1; y=1; z=1; 34854038:>2:r3=1; y=2; z=2; 37605243:>2:r3=0; y=2; z=1; 87702574:>2:r3=1; y=1; z=2; 92947081:>2:r3=1; y=2; z=1; 99033881:>2:r3=0; y=1; z=1; 46613508:>2:r3=0; y=1; z=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (y=2 /\ z=2 /\ 2:r3=0) is NOT validated Hash=d9622bc66160015a9bfad53625a07803 Cycle=SyncdWR Fre LwSyncdWW Wse LwSyncdWW Wse Relax safe138 No Safe=Fre Wse SyncdWR LwSyncdWW Time safe138 74.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe158.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe158 "SyncdWR Fre LwSyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;} P0 | P1 ; li r1,1 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) ; lwsync | sync ; li r3,1 | lwz r3,0(r4) ; stw r3,0(r4) | ; exists (y=2 /\ 1:r3=0) Generated assembler _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 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 safe158 Allowed Histogram (3 states) 19349560:>1:r3=1; y=1; 305742414:>1:r3=0; y=1; 314908026:>1:r3=1; y=2; No Witnesses Positive: 0, Negative: 640000000 Condition exists (y=2 /\ 1:r3=0) is NOT validated Hash=178cdf8fa414f9851e5cbee2c97136b0 Cycle=SyncdWR Fre LwSyncdWW Wse Relax safe158 No Safe=Fre Wse SyncdWR LwSyncdWW Time safe158 79.04 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe160.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe160 "SyncdWR Fre SyncdWR Fre LwSyncdWW Wse" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,1 | li r1,1 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; sync | lwsync | sync ; lwz r3,0(r4) | li r3,1 | lwz r3,0(r4) ; | stw r3,0(r4) | ; exists (z=2 /\ 0:r3=0 /\ 2:r3=0) Generated assembler _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,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 31,1 _litmus_P0_1_: stw 31,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test safe160 Allowed Histogram (7 states) 37585913:>0:r3=0; 2:r3=1; z=2; 772902:>0:r3=1; 2:r3=1; z=1; 50180652:>0:r3=0; 2:r3=0; z=1; 82832467:>0:r3=1; 2:r3=1; z=2; 95193481:>0:r3=0; 2:r3=1; z=1; 86397651:>0:r3=1; 2:r3=0; z=1; 47036934:>0:r3=1; 2:r3=0; z=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (z=2 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=1aec03977a16ccd6a8c5fc1afed64860 Cycle=SyncdWR Fre SyncdWR Fre LwSyncdWW Wse Relax safe160 No Safe=Fre Wse SyncdWR LwSyncdWW Time safe160 76.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe165.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe165 "SyncdWR Fre SyncsWR Fre LwSyncdWW Wse" {0:r2=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=x;} P0 | P1 | P2 ; li r1,1 | li r1,2 | li r1,2 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; sync | lwsync | sync ; lwz r3,0(r2) | li r3,1 | lwz r3,0(r4) ; | stw r3,0(r4) | ; exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,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 4,0(9) Test safe165 Allowed Histogram (13 states) 3492390:>0:r3=2; 2:r3=2; x=2; y=2; 129506:>0:r3=2; 2:r3=1; x=2; y=1; 365462:>0:r3=2; 2:r3=2; x=2; y=1; 480022:>0:r3=1; 2:r3=1; x=1; y=1; 11925755:>0:r3=1; 2:r3=2; x=1; y=1; 44075010:>0:r3=1; 2:r3=2; x=1; y=2; 7382724:>0:r3=2; 2:r3=0; x=2; y=1; 64325205:>0:r3=1; 2:r3=0; x=1; y=1; 33585038:>0:r3=1; 2:r3=2; x=2; y=1; 61365696:>0:r3=1; 2:r3=1; x=2; y=1; 54791376:>0:r3=1; 2:r3=0; x=2; y=1; 38173324:>0:r3=1; 2:r3=2; x=2; y=2; 79908492:>0:r3=1; 2:r3=1; x=1; y=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 2:r3=0) is NOT validated Hash=c2358315f3b0a52cdef1288bea12e53f Cycle=SyncdWR Fre SyncsWR Fre LwSyncdWW Wse Relax safe165 No Safe=Fre Wse SyncsWR SyncdWR LwSyncdWW Time safe165 71.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe358.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe358 "SyncdWR Fre SyncdWR Fre" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;} P0 | P1 ; li r1,1 | li r1,1 ; stw r1,0(r2) | stw r1,0(r2) ; sync | sync ; lwz r3,0(r4) | lwz r3,0(r4) ; exists (0:r3=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 5,1 _litmus_P1_1_: stw 5,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 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 safe358 Allowed Histogram (3 states) 24364849:>0:r3=1; 1:r3=1; 308141726:>0:r3=1; 1:r3=0; 307493425:>0:r3=0; 1:r3=1; No Witnesses Positive: 0, Negative: 640000000 Condition exists (0:r3=0 /\ 1:r3=0) is NOT validated Hash=5db67b28ae44dfb0497cda13c245c4e4 Cycle=SyncdWR Fre SyncdWR Fre Relax safe358 No Safe=Fre SyncdWR Time safe358 72.86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe359.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe359 "SyncdWR Fre SyncdWR Fre SyncdWR Fre" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=x;} P0 | P1 | P2 ; li r1,1 | li r1,1 | li r1,1 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; sync | sync | sync ; lwz r3,0(r4) | lwz r3,0(r4) | lwz r3,0(r4) ; exists (0:r3=0 /\ 1:r3=0 /\ 2:r3=0) Generated assembler _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,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 31,1 _litmus_P0_1_: stw 31,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test safe359 Allowed Histogram (7 states) 449982:>0:r3=1; 1:r3=1; 2:r3=1; 80378665:>0:r3=0; 1:r3=1; 2:r3=1; 80359694:>0:r3=1; 1:r3=0; 2:r3=1; 52158278:>0:r3=0; 1:r3=1; 2:r3=0; 52802180:>0:r3=0; 1:r3=0; 2:r3=1; 52896630:>0:r3=1; 1:r3=0; 2:r3=0; 80954571:>0:r3=1; 1:r3=1; 2:r3=0; No Witnesses Positive: 0, Negative: 400000000 Condition exists (0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=1bb05ee290fb3d2f94afc422c308bf1a Cycle=SyncdWR Fre SyncdWR Fre SyncdWR Fre Relax safe359 No Safe=Fre SyncdWR Time safe359 77.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/safe360.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC safe360 "SyncsWR Fre SyncdWR Fre SyncdWR Fre" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;} P0 | P1 | P2 ; li r1,2 | li r1,1 | li r1,1 ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; sync | sync | sync ; lwz r3,0(r4) | lwz r3,0(r4) | lwz r3,0(r2) ; exists (y=2 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=1) Generated assembler _litmus_P2_0_: li 11,1 _litmus_P2_1_: stw 11,0(9) _litmus_P2_2_: sync _litmus_P2_3_: lwz 5,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 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: lwz 3,0(9) Test safe360 Allowed Histogram (13 states) 125606:>0:r3=1; 1:r3=2; 2:r3=2; y=2; 3641634:>0:r3=0; 1:r3=2; 2:r3=2; y=2; 128343:>0:r3=1; 1:r3=1; 2:r3=2; y=2; 8466943:>0:r3=1; 1:r3=0; 2:r3=2; y=2; 63054989:>0:r3=1; 1:r3=1; 2:r3=1; y=2; 61483009:>0:r3=1; 1:r3=0; 2:r3=1; y=1; 297563:>0:r3=1; 1:r3=1; 2:r3=1; y=1; 49721961:>0:r3=0; 1:r3=2; 2:r3=1; y=1; 18403336:>0:r3=1; 1:r3=2; 2:r3=1; y=2; 6077556:>0:r3=1; 1:r3=2; 2:r3=1; y=1; 52178920:>0:r3=0; 1:r3=2; 2:r3=1; y=2; 80029264:>0:r3=0; 1:r3=1; 2:r3=1; y=1; 56390876:>0:r3=1; 1:r3=0; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 400000000 Condition exists (y=2 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=1) is NOT validated Hash=73d6bfa4ac7e4a6fa2da6911e5f8c2e3 Cycle=SyncsWR Fre SyncdWR Fre SyncdWR Fre Relax safe360 No Safe=Fre SyncsWR SyncdWR Time safe360 76.76 $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= Mon Dec 28 11:41:42 GMT 2009