Wed Dec 23 18:59:00 CET 2009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww000.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww000 "DpdW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=x;} P0 | P1 ; li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 ; lwsync | li r4,1 ; li r3,1 | stwx r4,r3,r5 ; stw r3,0(r4) | ; exists (x=2 /\ 1:r1=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: xor r11,r7,r7 _litmus_P1_2_: li r8,1 _litmus_P1_3_: stwx r8,r11,r2 Test bclwdww000 Allowed Histogram (3 states) 408049:>1:r1=0; x=1; 623830:>1:r1=1; x=1; 968121:>1:r1=0; x=2; No Witnesses Positive: 0, Negative: 2000000 Condition exists (x=2 /\ 1:r1=1) is NOT validated Hash=c704ed5593f60a49b6fe2873fbc99877 Cycle=DpdW Wse LwSyncdWW Rfe Relax bclwdww000 No BCLwSyncdWW Safe=Wse DpdW Time bclwdww000 1.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww001.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww001 "DpdW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | li r4,1 | lwsync | li r4,1 ; li r3,1 | stwx r4,r3,r5 | li r3,1 | stwx r4,r3,r5 ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: xor r11,r7,r7 _litmus_P1_2_: li r8,1 _litmus_P1_3_: stwx r8,r11,r2 _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: xor r11,r7,r7 _litmus_P3_2_: li r8,1 _litmus_P3_3_: stwx r8,r11,r2 Test bclwdww001 Allowed Histogram (15 states) 51 :>1:r1=1; 3:r1=1; x=1; z=2; 146 :>1:r1=0; 3:r1=1; x=2; z=2; 371 :>1:r1=1; 3:r1=0; x=2; z=2; 56 :>1:r1=1; 3:r1=1; x=2; z=1; 2439 :>1:r1=0; 3:r1=1; x=1; z=2; 5301 :>1:r1=1; 3:r1=0; x=1; z=2; 21838 :>1:r1=0; 3:r1=1; x=2; z=1; 32569 :>1:r1=1; 3:r1=0; x=2; z=1; 140742:>1:r1=0; 3:r1=0; x=2; z=2; 160348:>1:r1=0; 3:r1=0; x=1; z=2; 192287:>1:r1=1; 3:r1=0; x=1; z=1; 56487 :>1:r1=0; 3:r1=0; x=1; z=1; 184814:>1:r1=0; 3:r1=0; x=2; z=1; 30934 :>1:r1=1; 3:r1=1; x=1; z=1; 171617:>1:r1=0; 3:r1=1; x=1; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated Hash=d6ca5faa9797f1b1addda6b4fc107253 Cycle=DpdW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe Relax bclwdww001 No BCLwSyncdWW Safe=Wse DpdW Time bclwdww001 2.22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww002.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww002 "LwSyncdRW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ; lwsync | li r4,1 | lwsync | li r3,1 ; li r3,1 | stwx r4,r3,r5 | li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: xor r11,r7,r7 _litmus_P1_2_: li r8,1 _litmus_P1_3_: stwx r8,r11,r2 _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r8,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: li r10,1 _litmus_P3_3_: stw r10,0(r2) Test bclwdww002 Allowed Histogram (15 states) 11 :>1:r1=1; 3:r1=1; x=1; z=2; 63 :>1:r1=1; 3:r1=0; x=2; z=2; 58 :>1:r1=1; 3:r1=1; x=2; z=1; 562 :>1:r1=0; 3:r1=1; x=2; z=2; 31890 :>1:r1=0; 3:r1=1; x=2; z=1; 10864 :>1:r1=1; 3:r1=0; x=1; z=2; 120154:>1:r1=0; 3:r1=0; x=2; z=2; 13142 :>1:r1=1; 3:r1=0; x=2; z=1; 153793:>1:r1=0; 3:r1=1; x=1; z=1; 39253 :>1:r1=0; 3:r1=1; x=1; z=2; 213924:>1:r1=0; 3:r1=0; x=2; z=1; 47856 :>1:r1=0; 3:r1=0; x=1; z=1; 141918:>1:r1=0; 3:r1=0; x=1; z=2; 82244 :>1:r1=1; 3:r1=1; x=1; z=1; 144268:>1:r1=1; 3:r1=0; x=1; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated Hash=f222837c1b9c320fc4731d82df04c0c8 Cycle=LwSyncdRW Wse LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe Relax bclwdww002 No BCLwSyncdWW Safe=Wse LwSyncdRW DpdW Time bclwdww002 2.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww003.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww003 "DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | li r4,1 | lwsync | lwzx r4,r3,r5 ; li r3,1 | stwx r4,r3,r5 | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: xor r11,r7,r7 _litmus_P1_2_: li r8,1 _litmus_P1_3_: stwx r8,r11,r2 _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r6,0(r9) _litmus_P3_1_: xor r11,r6,r6 _litmus_P3_2_: lwzx r7,r11,r2 Test bclwdww003 Allowed Histogram (15 states) 136 :>1:r1=1; 3:r1=1; 3:r4=1; z=2; 237 :>1:r1=1; 3:r1=1; 3:r4=0; z=1; 252 :>1:r1=0; 3:r1=1; 3:r4=0; z=2; 7403 :>1:r1=1; 3:r1=0; 3:r4=1; z=2; 332 :>1:r1=1; 3:r1=0; 3:r4=0; z=2; 4150 :>1:r1=0; 3:r1=1; 3:r4=1; z=2; 12256 :>1:r1=0; 3:r1=1; 3:r4=0; z=1; 6124 :>1:r1=1; 3:r1=0; 3:r4=0; z=1; 184688:>1:r1=0; 3:r1=0; 3:r4=1; z=2; 149667:>1:r1=0; 3:r1=0; 3:r4=0; z=1; 79711 :>1:r1=0; 3:r1=0; 3:r4=1; z=1; 199456:>1:r1=0; 3:r1=1; 3:r4=1; z=1; 173849:>1:r1=0; 3:r1=0; 3:r4=0; z=2; 48215 :>1:r1=1; 3:r1=1; 3:r4=1; z=1; 133524:>1:r1=1; 3:r1=0; 3:r4=1; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=13e9eff5346eb465cffd68e7d2363168 Cycle=DpdR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe Relax bclwdww003 No BCLwSyncdWW Safe=Fre Wse DpdW DpdR Time bclwdww003 2.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww004.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww004 "DpsR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe" {0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | li r4,1 | lwsync | lwzx r4,r3,r2 ; li r3,1 | stwx r4,r3,r5 | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: xor r11,r7,r7 _litmus_P1_2_: li r8,1 _litmus_P1_3_: stwx r8,r11,r2 _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r2) _litmus_P3_1_: xor r11,r7,r7 _litmus_P3_2_: lwzx r9,r11,r2 Test bclwdww004 Allowed Histogram (39 states) 1 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=2; 1 :>1:r1=1; 3:r1=1; 3:r4=2; y=1; z=2; 1 :>1:r1=0; 3:r1=1; 3:r4=2; y=2; z=2; 4 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=2; 7 :>1:r1=1; 3:r1=2; 3:r4=1; y=2; z=1; 3 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1; 12 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2; 10 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2; 26 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2; 60 :>1:r1=0; 3:r1=2; 3:r4=1; y=2; z=1; 81 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1; 66 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1; 23 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1; 70 :>1:r1=0; 3:r1=2; 3:r4=1; y=1; z=1; 116 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1; 79 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1; 67 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1; 484 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2; 70 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1; 149 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1; 1358 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2; 3159 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2; 4925 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2; 10777 :>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1; 25330 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1; 6086 :>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2; 13117 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1; 21188 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1; 29559 :>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2; 80676 :>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2; 32013 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1; 80688 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2; 183618:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1; 80739 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2; 66467 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1; 205866:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1; 136919:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1; 16172 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1; 13 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated Hash=819caebc895b4fb2e9c9cb702b8483e8 Cycle=DpsR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe Relax bclwdww004 No BCLwSyncdWW Safe=Fre Wse DpsR DpdW Time bclwdww004 2.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww005.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww005 "LwSyncdRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ; lwsync | li r4,1 | lwsync | lwz r3,0(r4) ; li r3,1 | stwx r4,r3,r5 | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: xor r11,r7,r7 _litmus_P1_2_: li r8,1 _litmus_P1_3_: stwx r8,r11,r2 _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test bclwdww005 Allowed Histogram (15 states) 25 :>1:r1=1; 3:r1=1; 3:r3=1; z=2; 31 :>1:r1=1; 3:r1=1; 3:r3=0; z=1; 70 :>1:r1=0; 3:r1=1; 3:r3=0; z=2; 232 :>1:r1=1; 3:r1=0; 3:r3=0; z=2; 16002 :>1:r1=1; 3:r1=0; 3:r3=1; z=2; 45980 :>1:r1=1; 3:r1=0; 3:r3=0; z=1; 16643 :>1:r1=0; 3:r1=1; 3:r3=0; z=1; 129168:>1:r1=0; 3:r1=0; 3:r3=0; z=2; 164613:>1:r1=0; 3:r1=1; 3:r3=1; z=1; 13387 :>1:r1=0; 3:r1=1; 3:r3=1; z=2; 162467:>1:r1=1; 3:r1=0; 3:r3=1; z=1; 175712:>1:r1=0; 3:r1=0; 3:r3=1; z=2; 68165 :>1:r1=0; 3:r1=0; 3:r3=1; z=1; 51262 :>1:r1=1; 3:r1=1; 3:r3=1; z=1; 156243:>1:r1=0; 3:r1=0; 3:r3=0; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=1b7673dab67cdeed3a93a9f78642c123 Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe Relax bclwdww005 No BCLwSyncdWW Safe=Fre Wse LwSyncdRR DpdW Time bclwdww005 2.05 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww006.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww006 "LwSyncsRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe" {0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ; lwsync | li r4,1 | lwsync | lwz r3,0(r2) ; li r3,1 | stwx r4,r3,r5 | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: xor r11,r7,r7 _litmus_P1_2_: li r8,1 _litmus_P1_3_: stwx r8,r11,r2 _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r8,0(r2) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r9,0(r2) Test bclwdww006 Allowed Histogram (40 states) 2 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=2; 4 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2; 3 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2; 17 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1; 11 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1; 19 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1; 242 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1; 66 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2; 410 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1; 68 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1; 1311 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2; 925 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1; 378 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1; 902 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1; 2498 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1; 1030 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2; 2242 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2; 92 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1; 408 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2; 1635 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2; 848 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2; 9428 :>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1; 227 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1; 15845 :>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2; 3039 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2; 4665 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2; 5913 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1; 31124 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1; 16966 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1; 126970:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2; 80873 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1; 163472:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1; 94624 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2; 46251 :>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2; 57853 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2; 25864 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1; 141870:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1; 116570:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1; 44525 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1; 810 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated Hash=355c23adb39c4f8a03f27206e6d5ad02 Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpdW Wse LwSyncdWW Rfe Relax bclwdww006 No BCLwSyncdWW Safe=Fre Wse LwSyncsRR DpdW Time bclwdww006 2.86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww007.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww007 "DpdW Wse LwSyncdWW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | lwsync | li r4,1 ; li r3,1 | li r3,1 | stwx r4,r3,r5 ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ y=2 /\ 2:r1=1) Generated assembler _litmus_P0_0_: li r10,2 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: xor r11,r7,r7 _litmus_P2_2_: li r8,1 _litmus_P2_3_: stwx r8,r11,r2 Test bclwdww007 Allowed Histogram (7 states) 2790 :>2:r1=1; x=2; y=1; 1707 :>2:r1=1; x=1; y=2; 11728 :>2:r1=0; x=2; y=2; 307681:>2:r1=0; x=1; y=2; 90716 :>2:r1=0; x=1; y=1; 278220:>2:r1=1; x=1; y=1; 307158:>2:r1=0; x=2; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated Hash=c71f30898deb2fe2dc12be48ca126717 Cycle=DpdW Wse LwSyncdWW Wse LwSyncdWW Rfe Relax bclwdww007 No BCLwSyncdWW Safe=Wse LwSyncdWW DpdW Time bclwdww007 1.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww008.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww008 "LwSyncdRW Wse LwSyncdWW Wse LwSyncdWW Rfe" {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 | lwz 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 /\ 2:r1=1) Generated assembler _litmus_P0_0_: li r10,2 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r10,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: li r8,1 _litmus_P2_3_: stw r8,0(r2) Test bclwdww008 Allowed Histogram (7 states) 2927 :>2:r1=1; x=2; y=1; 14582 :>2:r1=0; x=2; y=2; 313527:>2:r1=0; x=1; y=2; 294833:>2:r1=0; x=2; y=1; 267663:>2:r1=1; x=1; y=1; 1254 :>2:r1=1; x=1; y=2; 105214:>2:r1=0; x=1; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated Hash=82e869524c51deb209a9e10f0c829a0c Cycle=LwSyncdRW Wse LwSyncdWW Wse LwSyncdWW Rfe Relax bclwdww008 No BCLwSyncdWW Safe=Wse LwSyncdWW LwSyncdRW Time bclwdww008 1.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww009.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww009 "DpdR Fre LwSyncdWW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=x;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | lwsync | lwzx r4,r3,r5 ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (y=2 /\ 2:r1=1 /\ 2:r4=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r6,0(r9) _litmus_P2_1_: xor r11,r6,r6 _litmus_P2_2_: lwzx r7,r11,r2 Test bclwdww009 Allowed Histogram (7 states) 5519 :>2:r1=1; 2:r4=0; y=1; 19282 :>2:r1=0; 2:r4=0; y=2; 299486:>2:r1=0; 2:r4=1; y=2; 315688:>2:r1=0; 2:r4=0; y=1; 274230:>2:r1=1; 2:r4=1; y=1; 1606 :>2:r1=1; 2:r4=1; y=2; 84189 :>2:r1=0; 2:r4=1; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=2e3c762333e6fd2b122415c163d1229a Cycle=DpdR Fre LwSyncdWW Wse LwSyncdWW Rfe Relax bclwdww009 No BCLwSyncdWW Safe=Fre Wse LwSyncdWW DpdR Time bclwdww009 1.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww010.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww010 "DpsR Fre LwSyncdWW Wse LwSyncdWW Rfe" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | lwsync | lwzx r4,r3,r2 ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1) Generated assembler _litmus_P0_0_: li r10,2 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r2) _litmus_P2_1_: xor r11,r7,r7 _litmus_P2_2_: lwzx r9,r11,r2 Test bclwdww010 Allowed Histogram (18 states) 61 :>2:r1=2; 2:r4=1; x=2; y=1; 16 :>2:r1=0; 2:r4=2; x=2; y=1; 1 :>2:r1=0; 2:r4=1; x=2; y=1; 49 :>2:r1=0; 2:r4=1; x=1; y=2; 126 :>2:r1=0; 2:r4=1; x=1; y=1; 861 :>2:r1=1; 2:r4=2; x=1; y=2; 334 :>2:r1=2; 2:r4=1; x=1; y=1; 86 :>2:r1=0; 2:r4=2; x=1; y=2; 16935 :>2:r1=0; 2:r4=0; x=2; y=1; 28613 :>2:r1=1; 2:r4=1; x=1; y=1; 282137:>2:r1=2; 2:r4=2; x=2; y=1; 54691 :>2:r1=0; 2:r4=0; x=1; y=2; 123666:>2:r1=1; 2:r4=1; x=1; y=2; 65541 :>2:r1=2; 2:r4=2; x=1; y=1; 291402:>2:r1=0; 2:r4=0; x=1; y=1; 133494:>2:r1=2; 2:r4=2; x=1; y=2; 1913 :>2:r1=1; 2:r4=1; x=2; y=1; 74 :>2:r1=0; 2:r4=2; x=1; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r4=1) is NOT validated Hash=3b6264a86335c33f3b93e442e8f4ad38 Cycle=DpsR Fre LwSyncdWW Wse LwSyncdWW Rfe Relax bclwdww010 No BCLwSyncdWW Safe=Fre Wse LwSyncdWW DpsR Time bclwdww010 1.71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww011.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww011 "LwSyncdRR Fre LwSyncdWW Wse LwSyncdWW Rfe" {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 | 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 (y=2 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test bclwdww011 Allowed Histogram (7 states) 13187 :>2:r1=0; 2:r3=0; y=2; 7075 :>2:r1=1; 2:r3=0; y=1; 100340:>2:r1=0; 2:r3=1; y=1; 317770:>2:r1=0; 2:r3=0; y=1; 266967:>2:r1=1; 2:r3=1; y=1; 1356 :>2:r1=1; 2:r3=1; y=2; 293305:>2:r1=0; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=cf3c12d91d4069a3e06aed8f569c6ba5 Cycle=LwSyncdRR Fre LwSyncdWW Wse LwSyncdWW Rfe Relax bclwdww011 No BCLwSyncdWW Safe=Fre Wse LwSyncdWW LwSyncdRR Time bclwdww011 1.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww012.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww012 "LwSyncsRR Fre LwSyncdWW Wse LwSyncdWW Rfe" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | lwsync | lwz r3,0(r2) ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1) Generated assembler _litmus_P0_0_: li r10,2 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r8,0(r2) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r9,0(r2) Test bclwdww012 Allowed Histogram (18 states) 6 :>2:r1=0; 2:r3=1; x=2; y=1; 38 :>2:r1=0; 2:r3=2; x=2; y=1; 95 :>2:r1=1; 2:r3=2; x=1; y=2; 129 :>2:r1=2; 2:r3=1; x=2; y=1; 109 :>2:r1=2; 2:r3=1; x=1; y=1; 2989 :>2:r1=0; 2:r3=2; x=1; y=2; 3321 :>2:r1=0; 2:r3=1; x=1; y=1; 459 :>2:r1=0; 2:r3=1; x=1; y=2; 1261 :>2:r1=1; 2:r3=1; x=2; y=1; 106557:>2:r1=1; 2:r3=1; x=1; y=2; 16571 :>2:r1=0; 2:r3=0; x=2; y=1; 61986 :>2:r1=2; 2:r3=2; x=1; y=1; 76594 :>2:r1=0; 2:r3=0; x=1; y=2; 279954:>2:r1=2; 2:r3=2; x=2; y=1; 302237:>2:r1=0; 2:r3=0; x=1; y=1; 123014:>2:r1=2; 2:r3=2; x=1; y=2; 23368 :>2:r1=1; 2:r3=1; x=1; y=1; 1312 :>2:r1=0; 2:r3=2; x=1; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 2:r3=1) is NOT validated Hash=e7d627c7adc87ac2502ce1f2b46f87c5 Cycle=LwSyncsRR Fre LwSyncdWW Wse LwSyncdWW Rfe Relax bclwdww012 No BCLwSyncdWW Safe=Fre Wse LwSyncsRR LwSyncdWW Time bclwdww012 1.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww013.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww013 "LwSyncdRW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;} P0 | P1 ; li r1,2 | lwz 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 /\ 1:r1=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r8,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: li r10,1 _litmus_P1_3_: stw r10,0(r2) Test bclwdww013 Allowed Histogram (3 states) 606767:>1:r1=1; x=1; 842839:>1:r1=0; x=2; 550394:>1:r1=0; x=1; No Witnesses Positive: 0, Negative: 2000000 Condition exists (x=2 /\ 1:r1=1) is NOT validated Hash=4d1c1648955365c08b4c97b22a8d5408 Cycle=LwSyncdRW Wse LwSyncdWW Rfe Relax bclwdww013 No BCLwSyncdWW Safe=Wse LwSyncdRW Time bclwdww013 1.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww014.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww014 "LwSyncdRW Wse LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | li r3,1 | lwsync | li r3,1 ; li r3,1 | stw r3,0(r4) | li r3,1 | stw r3,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r8,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: li r10,1 _litmus_P1_3_: stw r10,0(r2) _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r8,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: li r10,1 _litmus_P3_3_: stw r10,0(r2) Test bclwdww014 Allowed Histogram (15 states) 72 :>1:r1=1; 3:r1=0; x=2; z=2; 84 :>1:r1=0; 3:r1=1; x=2; z=2; 42 :>1:r1=1; 3:r1=1; x=2; z=1; 50 :>1:r1=1; 3:r1=1; x=1; z=2; 9527 :>1:r1=1; 3:r1=0; x=2; z=1; 3898 :>1:r1=1; 3:r1=0; x=1; z=2; 1740 :>1:r1=0; 3:r1=1; x=1; z=2; 17768 :>1:r1=0; 3:r1=1; x=2; z=1; 135383:>1:r1=0; 3:r1=0; x=2; z=2; 78441 :>1:r1=0; 3:r1=0; x=1; z=1; 172539:>1:r1=0; 3:r1=0; x=1; z=2; 189595:>1:r1=0; 3:r1=0; x=2; z=1; 178454:>1:r1=1; 3:r1=0; x=1; z=1; 30123 :>1:r1=1; 3:r1=1; x=1; z=1; 182284:>1:r1=0; 3:r1=1; x=1; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated Hash=d40b4d76f7e7419bc76f118bb3639055 Cycle=LwSyncdRW Wse LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe Relax bclwdww014 No BCLwSyncdWW Safe=Wse LwSyncdRW Time bclwdww014 2.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww015.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww015 "DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | li r3,1 | lwsync | lwzx r4,r3,r5 ; li r3,1 | stw r3,0(r4) | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r8,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: li r10,1 _litmus_P1_3_: stw r10,0(r2) _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r6,0(r9) _litmus_P3_1_: xor r11,r6,r6 _litmus_P3_2_: lwzx r7,r11,r2 Test bclwdww015 Allowed Histogram (15 states) 62 :>1:r1=0; 3:r1=1; 3:r4=0; z=2; 75 :>1:r1=1; 3:r1=0; 3:r4=0; z=2; 50 :>1:r1=1; 3:r1=1; 3:r4=1; z=2; 54 :>1:r1=1; 3:r1=1; 3:r4=0; z=1; 11252 :>1:r1=1; 3:r1=0; 3:r4=1; z=2; 11550 :>1:r1=0; 3:r1=1; 3:r4=1; z=2; 11681 :>1:r1=0; 3:r1=1; 3:r4=0; z=1; 85369 :>1:r1=0; 3:r1=0; 3:r4=0; z=2; 127371:>1:r1=1; 3:r1=0; 3:r4=1; z=1; 59671 :>1:r1=1; 3:r1=0; 3:r4=0; z=1; 46239 :>1:r1=0; 3:r1=0; 3:r4=1; z=1; 190238:>1:r1=0; 3:r1=0; 3:r4=1; z=2; 166942:>1:r1=0; 3:r1=0; 3:r4=0; z=1; 121353:>1:r1=1; 3:r1=1; 3:r4=1; z=1; 168093:>1:r1=0; 3:r1=1; 3:r4=1; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=ed6f4c8d626a404d3601d3a343adac19 Cycle=DpdR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe Relax bclwdww015 No BCLwSyncdWW Safe=Fre Wse LwSyncdRW DpdR Time bclwdww015 2.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww016.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww016 "DpsR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | li r3,1 | lwsync | lwzx r4,r3,r2 ; li r3,1 | stw r3,0(r4) | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r8,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: li r10,1 _litmus_P1_3_: stw r10,0(r2) _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r2) _litmus_P3_1_: xor r11,r7,r7 _litmus_P3_2_: lwzx r9,r11,r2 Test bclwdww016 Allowed Histogram (32 states) 1 :>1:r1=1; 3:r1=2; 3:r4=1; y=1; z=1; 1 :>1:r1=1; 3:r1=0; 3:r4=2; y=2; z=1; 23 :>1:r1=1; 3:r1=1; 3:r4=1; y=2; z=1; 1 :>1:r1=0; 3:r1=1; 3:r4=2; y=1; z=2; 10 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=1; 23 :>1:r1=1; 3:r1=0; 3:r4=2; y=1; z=1; 5 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=2; 17 :>1:r1=0; 3:r1=0; 3:r4=1; y=1; z=2; 3 :>1:r1=0; 3:r1=0; 3:r4=1; y=2; z=1; 28 :>1:r1=1; 3:r1=0; 3:r4=1; y=1; z=1; 113 :>1:r1=1; 3:r1=0; 3:r4=0; y=2; z=1; 465 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=2; 38 :>1:r1=0; 3:r1=0; 3:r4=2; y=1; z=1; 562 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=2; 346 :>1:r1=0; 3:r1=0; 3:r4=2; y=2; z=1; 14863 :>1:r1=1; 3:r1=2; 3:r4=2; y=2; z=1; 763 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=2; 1447 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=2; 13964 :>1:r1=0; 3:r1=1; 3:r4=1; y=2; z=1; 18630 :>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=2; 54571 :>1:r1=1; 3:r1=0; 3:r4=0; y=1; z=1; 9357 :>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=2; 74149 :>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=2; 81576 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=2; 93120 :>1:r1=0; 3:r1=2; 3:r4=2; y=2; z=1; 24843 :>1:r1=0; 3:r1=1; 3:r4=1; y=1; z=1; 82482 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=2; 43399 :>1:r1=0; 3:r1=2; 3:r4=2; y=1; z=1; 154590:>1:r1=0; 3:r1=0; 3:r4=0; y=2; z=1; 139520:>1:r1=0; 3:r1=0; 3:r4=0; y=1; z=1; 29433 :>1:r1=1; 3:r1=1; 3:r4=1; y=1; z=1; 161657:>1:r1=1; 3:r1=2; 3:r4=2; y=1; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated Hash=cda2e0cac993408d5ce399f8c3bf25da Cycle=DpsR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe Relax bclwdww016 No BCLwSyncdWW Safe=Fre Wse LwSyncdRW DpsR Time bclwdww016 2.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww017.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww017 "LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | li r3,1 | lwsync | lwz r3,0(r4) ; li r3,1 | stw r3,0(r4) | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r8,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: li r10,1 _litmus_P1_3_: stw r10,0(r2) _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test bclwdww017 Allowed Histogram (15 states) 51 :>1:r1=1; 3:r1=1; 3:r3=1; z=2; 52 :>1:r1=0; 3:r1=1; 3:r3=0; z=2; 184 :>1:r1=1; 3:r1=1; 3:r3=0; z=1; 233 :>1:r1=1; 3:r1=0; 3:r3=0; z=2; 8391 :>1:r1=0; 3:r1=1; 3:r3=1; z=2; 5609 :>1:r1=1; 3:r1=0; 3:r3=1; z=2; 12887 :>1:r1=0; 3:r1=1; 3:r3=0; z=1; 28553 :>1:r1=1; 3:r1=0; 3:r3=0; z=1; 142737:>1:r1=1; 3:r1=0; 3:r3=1; z=1; 74416 :>1:r1=0; 3:r1=0; 3:r3=1; z=1; 187852:>1:r1=0; 3:r1=0; 3:r3=1; z=2; 178093:>1:r1=0; 3:r1=1; 3:r3=1; z=1; 112670:>1:r1=0; 3:r1=0; 3:r3=0; z=2; 70828 :>1:r1=1; 3:r1=1; 3:r3=1; z=1; 177444:>1:r1=0; 3:r1=0; 3:r3=0; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=bc3782a4ff957f30ebb76bfb73a82170 Cycle=LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe Relax bclwdww017 No BCLwSyncdWW Safe=Fre Wse LwSyncdRW LwSyncdRR Time bclwdww017 2.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww018.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww018 "LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | li r3,1 | lwsync | lwz r3,0(r2) ; li r3,1 | stw r3,0(r4) | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r8,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: li r10,1 _litmus_P1_3_: stw r10,0(r2) _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r8,0(r2) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r9,0(r2) Test bclwdww018 Allowed Histogram (39 states) 3 :>1:r1=1; 3:r1=2; 3:r3=1; y=2; z=1; 9 :>1:r1=1; 3:r1=0; 3:r3=2; y=2; z=1; 28 :>1:r1=1; 3:r1=1; 3:r3=2; y=1; z=2; 191 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=1; 158 :>1:r1=1; 3:r1=0; 3:r3=0; y=2; z=1; 5 :>1:r1=1; 3:r1=1; 3:r3=1; y=2; z=1; 5 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=2; 84 :>1:r1=0; 3:r1=2; 3:r3=1; y=2; z=1; 1099 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=2; 596 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=2; 149 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=2; 1143 :>1:r1=0; 3:r1=1; 3:r3=2; y=1; z=2; 2961 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=2; 234 :>1:r1=0; 3:r1=2; 3:r3=1; y=1; z=1; 3 :>1:r1=0; 3:r1=0; 3:r3=2; y=2; z=2; 572 :>1:r1=1; 3:r1=2; 3:r3=1; y=1; z=1; 314 :>1:r1=1; 3:r1=0; 3:r3=2; y=1; z=1; 70 :>1:r1=0; 3:r1=0; 3:r3=1; y=2; z=1; 407 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=2; 315 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=2; 480 :>1:r1=1; 3:r1=0; 3:r3=1; y=1; z=1; 3411 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=2; 2067 :>1:r1=0; 3:r1=0; 3:r3=1; y=1; z=1; 20815 :>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=2; 11152 :>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=2; 67257 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=2; 5979 :>1:r1=0; 3:r1=1; 3:r3=1; y=2; z=1; 7781 :>1:r1=1; 3:r1=2; 3:r3=2; y=2; z=1; 917 :>1:r1=0; 3:r1=0; 3:r3=2; y=1; z=1; 20967 :>1:r1=0; 3:r1=1; 3:r3=1; y=1; z=1; 68525 :>1:r1=0; 3:r1=2; 3:r3=2; y=2; z=1; 28463 :>1:r1=1; 3:r1=0; 3:r3=0; y=1; z=1; 139179:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=2; 156584:>1:r1=0; 3:r1=0; 3:r3=0; y=2; z=1; 85600 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=2; 164124:>1:r1=1; 3:r1=2; 3:r3=2; y=1; z=1; 35279 :>1:r1=0; 3:r1=2; 3:r3=2; y=1; z=1; 133534:>1:r1=0; 3:r1=0; 3:r3=0; y=1; z=1; 39540 :>1:r1=1; 3:r1=1; 3:r3=1; y=1; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated Hash=090f9e7edaad20d00811f89adff27ed2 Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRW Wse LwSyncdWW Rfe Relax bclwdww018 No BCLwSyncdWW Safe=Fre Wse LwSyncsRR LwSyncdRW Time bclwdww018 3.01 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww019.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww019 "DpdR Fre LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=x;} P0 | P1 ; li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 ; lwsync | lwzx r4,r3,r5 ; li r3,1 | ; stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r4=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r6,0(r9) _litmus_P1_1_: xor r11,r6,r6 _litmus_P1_2_: lwzx r7,r11,r2 Test bclwdww019 Allowed Histogram (3 states) 392778:>1:r1=0; 1:r4=1; 910520:>1:r1=0; 1:r4=0; 696702:>1:r1=1; 1:r4=1; No Witnesses Positive: 0, Negative: 2000000 Condition exists (1:r1=1 /\ 1:r4=0) is NOT validated Hash=76deedad5ea71bc51dc86d1d5214c15b Cycle=DpdR Fre LwSyncdWW Rfe Relax bclwdww019 No BCLwSyncdWW Safe=Fre DpdR Time bclwdww019 1.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww020.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww020 "DpdR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r5 ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r6,0(r9) _litmus_P1_1_: xor r11,r6,r6 _litmus_P1_2_: lwzx r7,r11,r2 _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r6,0(r9) _litmus_P3_1_: xor r11,r6,r6 _litmus_P3_2_: lwzx r7,r11,r2 Test bclwdww020 Allowed Histogram (15 states) 322 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=0; 701 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; 293 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; 260 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=0; 14356 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=0; 6213 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=1; 3590 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; 19287 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; 176801:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; 170651:>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; 171055:>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; 67663 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; 157554:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; 156987:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; 54267 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=95bd88b4aecb95238880fff470fdbcc8 Cycle=DpdR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe Relax bclwdww020 No BCLwSyncdWW Safe=Fre DpdR Time bclwdww020 2.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww021.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww021 "DpsR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe" {0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r2 ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r6,0(r9) _litmus_P1_1_: xor r11,r6,r6 _litmus_P1_2_: lwzx r7,r11,r2 _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r2) _litmus_P3_1_: xor r11,r7,r7 _litmus_P3_2_: lwzx r9,r11,r2 Test bclwdww021 Allowed Histogram (35 states) 1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=2; 2 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=1; z=1; 5 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=1; z=1; 15 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=2; 33 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r4=1; z=1; 10 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=2; 16 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; z=1; 5 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=2; z=2; 110 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r4=0; z=1; 10 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; z=1; 42 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; z=1; 63 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; z=1; 119 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=1; z=1; 99 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=2; z=1; 959 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=2; 196 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; z=1; 4681 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=2; 113 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=1; z=1; 22052 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=2; 5146 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=2; 27371 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; z=1; 2335 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=2; 32324 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=1; 9619 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=2; 181459:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; z=1; 87136 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; z=1; 68108 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=2; 81044 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=2; 124511:>1:r1=0; 1:r4=1; 3:r1=0; 3:r4=0; z=1; 67223 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r4=1; z=2; 31152 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; z=1; 170483:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; z=1; 40922 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; z=1; 28426 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; z=1; 14210 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r4=2; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r4=1) is NOT validated Hash=26c4ea0f855245b74a15911ba593704d Cycle=DpsR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe Relax bclwdww021 No BCLwSyncdWW Safe=Fre DpsR DpdR Time bclwdww021 2.73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww022.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww022 "LwSyncdRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ; lwsync | lwzx r4,r3,r5 | lwsync | lwz r3,0(r4) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r6,0(r9) _litmus_P1_1_: xor r11,r6,r6 _litmus_P1_2_: lwzx r7,r11,r2 _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test bclwdww022 Allowed Histogram (15 states) 77 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; 267 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; 714 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; 81 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; 11699 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=0; 3429 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=1; 16462 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; 165107:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; 149714:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; 208657:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; 207159:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; 76187 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; 64857 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; 18005 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; 77585 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=18c468c9529c924b0b9eadcf19d0bf8c Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe Relax bclwdww022 No BCLwSyncdWW Safe=Fre LwSyncdRR DpdR Time bclwdww022 2.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww023.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww023 "LwSyncsRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe" {0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ; lwsync | lwzx r4,r3,r5 | lwsync | lwz r3,0(r2) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r6,0(r9) _litmus_P1_1_: xor r11,r6,r6 _litmus_P1_2_: lwzx r7,r11,r2 _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r8,0(r2) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r9,0(r2) Test bclwdww023 Allowed Histogram (38 states) 1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2; 2 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1; 10 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=2; z=1; 9 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1; 15 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1; 14 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2; 127 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2; 19 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1; 66 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2; 83 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1; 105 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1; 146 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2; 418 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1; 1408 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1; 644 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=1; 286 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1; 401 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1; 662 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1; 2614 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2; 1176 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2; 4851 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2; 14589 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1; 652 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2; 29118 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1; 8045 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2; 5289 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2; 35342 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1; 96675 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1; 70881 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2; 25008 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2; 74350 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2; 31851 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1; 164528:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1; 66860 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2; 182068:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1; 134062:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1; 14236 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1; 33389 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated Hash=cc14d1f72457a494131d0111d5791792 Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpdR Fre LwSyncdWW Rfe Relax bclwdww023 No BCLwSyncdWW Safe=Fre LwSyncsRR DpdR Time bclwdww023 2.91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww024.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww024 "DpsR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 ; lwsync | lwzx r4,r3,r2 | lwsync | lwzx r4,r3,r2 ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r2) _litmus_P1_1_: xor r11,r7,r7 _litmus_P1_2_: lwzx r9,r11,r2 _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r2) _litmus_P3_1_: xor r11,r7,r7 _litmus_P3_2_: lwzx r9,r11,r2 Test bclwdww024 Allowed Histogram (52 states) 1 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=1; x=1; y=1; 1 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=2; y=1; 1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1; 3 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1; 2 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1; 1 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1; 1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1; 1 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=1; x=1; y=1; 2 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2; 2 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=1; y=1; 2 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=2; x=2; y=1; 10 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=2; x=1; y=2; 30 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=2; 7 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=2; x=1; y=1; 26 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=2; y=1; 19 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=1; 2 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2; 38 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=2; 7 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2; 44 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=1; 16 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=1; x=1; y=1; 54 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1; 45 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=2; x=1; y=2; 72 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=1; x=1; y=2; 390 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=2; 64 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=1; x=1; y=1; 815 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=2; 432 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=2; y=1; 1270 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=2; y=1; 579 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=2; y=1; 13347 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=2; 2026 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=2; y=1; 13670 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=2; 26904 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=2; y=1; 13949 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=1; y=1; 39015 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r4=1; x=1; y=1; 8325 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=1; 16236 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=1; 41611 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=2; 17991 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r4=0; x=1; y=1; 14413 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=2; 63975 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=2; 55693 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=2; y=1; 49391 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r4=2; x=1; y=2; 134363:>1:r1=1; 1:r4=1; 3:r1=2; 3:r4=2; x=2; y=1; 63682 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r4=0; x=1; y=1; 50480 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=1; y=1; 112612:>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=1; y=2; 20730 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r4=2; x=2; y=1; 24830 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r4=1; x=1; y=1; 8580 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r4=1; x=2; y=1; 204240:>1:r1=0; 1:r4=0; 3:r1=0; 3:r4=0; x=1; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r4=1) is NOT validated Hash=d9cb89dae7c1c7340715ada64130ec5d Cycle=DpsR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe Relax bclwdww024 No BCLwSyncdWW Safe=Fre DpsR Time bclwdww024 3.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww025.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww025 "LwSyncdRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ; lwsync | lwzx r4,r3,r2 | lwsync | lwz r3,0(r4) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r2) _litmus_P1_1_: xor r11,r7,r7 _litmus_P1_2_: lwzx r9,r11,r2 _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test bclwdww025 Allowed Histogram (32 states) 1 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=1; 1 :>1:r1=2; 1:r4=1; 3:r1=1; 3:r3=1; y=1; 2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=2; 2 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=2; 9 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; y=1; 4 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=1; y=2; 4 :>1:r1=0; 1:r4=2; 3:r1=1; 3:r3=1; y=1; 2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; y=1; 4 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; y=1; 4 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=1; 15 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; y=2; 379 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=0; y=1; 53 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=0; y=1; 1689 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=2; 1529 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=2; 24253 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=2; 3028 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=2; 2914 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=2; 2634 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=0; y=1; 20753 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; y=1; 22792 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=1; 49065 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=2; 85271 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; y=2; 139264:>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; y=1; 110489:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=2; 119429:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; y=1; 148567:>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=1; 30858 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; y=1; 154440:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; y=1; 10645 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; y=1; 66470 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; y=1; 5430 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=9e35ea0c011a355376ee19a400e99599 Cycle=LwSyncdRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe Relax bclwdww025 No BCLwSyncdWW Safe=Fre LwSyncdRR DpsR Time bclwdww025 2.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww026.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww026 "LwSyncsRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwsync ; lwsync | lwzx r4,r3,r2 | lwsync | lwz r3,0(r2) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r2) _litmus_P1_1_: xor r11,r7,r7 _litmus_P1_2_: lwzx r9,r11,r2 _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r8,0(r2) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r9,0(r2) Test bclwdww026 Allowed Histogram (64 states) 2 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1; 3 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=2; y=1; 1 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=2; 1 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1; 2 :>1:r1=0; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2; 1 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1; 3 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2; 4 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; x=1; y=2; 1 :>1:r1=2; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2; 2 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2; 1 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1; 3 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1; 9 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=2; y=1; 5 :>1:r1=0; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1; 24 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1; 23 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=2; y=1; 10 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=1; x=1; y=1; 15 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=2; y=1; 33 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=2; y=1; 24 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; x=1; y=2; 13 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=2; y=1; 14 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=2; y=1; 241 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=2; 713 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=2; 197 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=2; 15 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; x=1; y=1; 140 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=1; 1038 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=2; y=1; 88 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; x=1; y=2; 1018 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=2; x=1; y=2; 831 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=2; y=1; 1000 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; x=1; y=1; 5201 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; x=1; y=1; 1048 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=2; 43 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; x=1; y=1; 4850 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=2; y=1; 1611 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=1; 1154 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=1; x=1; y=2; 3279 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=2; y=1; 98 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=1; 6707 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=2; 1599 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=2; y=1; 19968 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=2; 1159 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; x=1; y=1; 11176 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=1; 17665 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=1; y=1; 20664 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=2; y=1; 7127 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=1; 5643 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=2; 34066 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=1; 98891 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=1; y=2; 65518 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=2; y=1; 69729 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; x=1; y=1; 52211 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=1; y=2; 64474 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=2; 125243:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; x=2; y=1; 211206:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; x=1; y=1; 25798 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=0; x=1; y=2; 53953 :>1:r1=2; 1:r4=2; 3:r1=2; 3:r3=2; x=2; y=1; 19468 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; x=1; y=1; 27682 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; x=1; y=1; 27366 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; x=1; y=1; 7600 :>1:r1=2; 1:r4=2; 3:r1=1; 3:r3=1; x=2; y=1; 2328 :>1:r1=2; 1:r4=2; 3:r1=0; 3:r3=2; x=1; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r4=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated Hash=1d532d0bb6dcdffd3b5563101102cb60 Cycle=LwSyncsRR Fre LwSyncdWW Rfe DpsR Fre LwSyncdWW Rfe Relax bclwdww026 No BCLwSyncdWW Safe=Fre LwSyncsRR DpsR Time bclwdww026 3.65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww027.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww027 "LwSyncdRR Fre LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=x;} 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_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) Test bclwdww027 Allowed Histogram (3 states) 279303:>1:r1=0; 1:r3=1; 957698:>1:r1=0; 1:r3=0; 762999:>1:r1=1; 1:r3=1; No Witnesses Positive: 0, Negative: 2000000 Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated Hash=9db44a87c6f0512eb7b557fa626432dc Cycle=LwSyncdRR Fre LwSyncdWW Rfe Relax bclwdww027 No BCLwSyncdWW Safe=Fre LwSyncdRR Time bclwdww027 1.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww028.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww028 "LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=x;} 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_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test bclwdww028 Allowed Histogram (15 states) 12 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 25 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 303 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 1350 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 18498 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 29524 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 14992 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 45286 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 163743:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 168575:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 169893:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 146607:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 156704:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 26225 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 58263 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=55921b82d0e8bcbda1b708c97c7b56b3 Cycle=LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe Relax bclwdww028 No BCLwSyncdWW Safe=Fre LwSyncdRR Time bclwdww028 2.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww029.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww029 "LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;} P0 | P1 | P2 | P3 ; li r1,2 | 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(r2) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r8,0(r2) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r9,0(r2) Test bclwdww029 Allowed Histogram (38 states) 2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 3 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 31 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 4 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=1; 4 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=1; 42 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=1; 7 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; z=1; 356 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=1; 187 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; z=1; 144 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=1; 622 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=1; 150 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=1; 991 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 481 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; z=1; 2601 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=1; 529 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 983 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 201 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 1103 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=1; 9595 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; z=1; 2684 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 2126 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 3169 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=2; 18946 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=1; 9420 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=2; 2868 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=1; 48287 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 26009 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=1; 140480:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=1; 168245:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; z=1; 47405 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 82329 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; z=1; 81116 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=2; 130633:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 33420 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; z=1; 138883:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=1; 3708 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 42236 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated Hash=ed3e4f2d7ea7b66a761b0ef9aadf9b30 Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe Relax bclwdww029 No BCLwSyncdWW Safe=Fre LwSyncsRR LwSyncdRR Time bclwdww029 2.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/bclwdww030.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC bclwdww030 "LwSyncsRR Fre LwSyncdWW Rfe LwSyncsRR Fre LwSyncdWW Rfe" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r2) | lwsync | lwz r3,0(r2) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) Generated assembler _litmus_P0_0_: li r11,2 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r8,0(r2) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r9,0(r2) _litmus_P2_0_: li r11,2 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r8,0(r2) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r9,0(r2) Test bclwdww030 Allowed Histogram (94 states) 1 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1; 2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 1 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 1 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1; 4 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 1 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1; 3 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1; 4 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 1 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 2 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1; 26 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2; 16 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1; 5 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 6 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; 1 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1; 6 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1; 10 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1; 3 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2; 20 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 10 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 41 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1; 24 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 3 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1; 91 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1; 27 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 135 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 13 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 18 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 3 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 18 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1; 15 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 49 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1; 10 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1; 152 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2; 64 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 70 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 92 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 31 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 106 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2; 172 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 13 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 118 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 112 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1; 293 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 26 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 159 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 714 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2; 880 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 166 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 147 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1; 824 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1; 1042 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 40 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 56 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 286 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 1703 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 138 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 1322 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1; 716 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 984 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 272 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 150 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1; 1416 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1; 4027 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1; 882 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1; 24 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 1003 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 6224 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1; 2500 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 1285 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1; 22427 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1; 1535 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2; 22805 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1; 618 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1; 7302 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2; 6464 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2; 63285 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 33657 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 8765 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1; 36490 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1; 10307 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 17093 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 14045 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1; 118009:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 17700 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 51778 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1; 80946 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2; 101631:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2; 64529 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1; 212790:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1; 57613 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1; 14694 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 6732 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1; 6 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated Hash=affa727dfb200dd46b9b0942598eb58d Cycle=LwSyncsRR Fre LwSyncdWW Rfe LwSyncsRR Fre LwSyncdWW Rfe Relax bclwdww030 No BCLwSyncdWW Safe=Fre LwSyncsRR Time bclwdww030 5.19 $Revision: 3163 $ Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 1000000 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 1 #endif #ifndef N_EXE #define N_EXE (4 < N ? 1 : 4 / N) #endif /* gcc options: -Wall -std=gnu99 */ /* barrier: user */ /* tread start/join: changing */ /* memory: indirect */ /* safer: false */ /* preload: true */ /* para: self */ /* changes: false */ /* speedcheck: false */ /* proc used: 4 */ GCCOPTS="-Wall -std=gnu99 " LITMUSOPTS= Wed Dec 23 19:00:10 CET 2009