Mon Jan 11 13:45:08 CET 2010 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr000.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr000 "Fre SyncdWW Rfe DpdR PodRW PosWR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 1:r7=z;} P0 | P1 ; li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 ; sync | lwzx r4,r3,r5 ; li r3,1 | li r6,1 ; stw r3,0(r4) | stw r6,0(r7) ; | lwz r8,0(r7) ; exists (z=2 /\ 1:r1=1 /\ 1:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r22,0(r11) _litmus_P1_1_: xor r24,r22,r22 _litmus_P1_2_: lwzx r10,r24,r9 _litmus_P1_3_: li r8,1 _litmus_P1_4_: stw r8,0(r2) _litmus_P1_5_: lwz r23,0(r2) Test podrwposwr000 Allowed Histogram (4 states) 1356674:>1:r1=0; 1:r8=1; z=1; 144209:>1:r1=1; 1:r8=1; z=1; 499031:>1:r1=0; 1:r8=1; z=2; 86 :>1:r1=0; 1:r8=2; z=2; No Witnesses Positive: 0, Negative: 2000000 Condition exists (z=2 /\ 1:r1=1 /\ 1:r8=1) is NOT validated Hash=de34f0775aba87820d8467bc9dc735f3 Cycle=Fre SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr000 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW Time podrwposwr000 1.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr001.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr001 "Fre SyncdWW Rfe DpdR PodRW PosWR Fre SyncdWW Rfe DpdR PodRW PosWR" {0:r2=c; 0:r4=x; 1:r2=x; 1:r5=y; 1:r7=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=b; 3:r7=c;} 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 ; sync | lwzx r4,r3,r5 | sync | lwzx r4,r3,r5 ; li r3,1 | li r6,1 | li r3,1 | li r6,1 ; stw r3,0(r4) | stw r6,0(r7) | stw r3,0(r4) | stw r6,0(r7) ; | lwz r8,0(r7) | | lwz r8,0(r7) ; exists (c=2 /\ z=2 /\ 1:r1=1 /\ 1:r8=1 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r22,0(r11) _litmus_P1_1_: xor r24,r22,r22 _litmus_P1_2_: lwzx r10,r24,r9 _litmus_P1_3_: li r8,1 _litmus_P1_4_: stw r8,0(r2) _litmus_P1_5_: lwz r23,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr001 Allowed Histogram (17 states) 401935:>1:r1=0; 1:r8=1; 3:r1=0; 3:r8=1; c=1; z=1; 130276:>1:r1=1; 1:r8=1; 3:r1=0; 3:r8=1; c=1; z=1; 174558:>1:r1=0; 1:r8=1; 3:r1=1; 3:r8=1; c=1; z=1; 15627 :>1:r1=1; 1:r8=1; 3:r1=1; 3:r8=1; c=1; z=1; 157294:>1:r1=0; 1:r8=1; 3:r1=0; 3:r8=1; c=2; z=1; 2280 :>1:r1=1; 1:r8=1; 3:r1=0; 3:r8=1; c=2; z=1; 1089 :>1:r1=0; 1:r8=1; 3:r1=1; 3:r8=1; c=2; z=1; 3 :>1:r1=1; 1:r8=1; 3:r1=1; 3:r8=1; c=2; z=1; 2 :>1:r1=0; 1:r8=1; 3:r1=0; 3:r8=2; c=2; z=1; 1 :>1:r1=0; 1:r8=1; 3:r1=1; 3:r8=2; c=2; z=1; 103586:>1:r1=0; 1:r8=1; 3:r1=0; 3:r8=1; c=1; z=2; 520 :>1:r1=1; 1:r8=1; 3:r1=0; 3:r8=1; c=1; z=2; 5012 :>1:r1=0; 1:r8=1; 3:r1=1; 3:r8=1; c=1; z=2; 8 :>1:r1=1; 1:r8=1; 3:r1=1; 3:r8=1; c=1; z=2; 7806 :>1:r1=0; 1:r8=1; 3:r1=0; 3:r8=1; c=2; z=2; 2 :>1:r1=1; 1:r8=1; 3:r1=0; 3:r8=1; c=2; z=2; 1 :>1:r1=0; 1:r8=1; 3:r1=0; 3:r8=2; c=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (c=2 /\ z=2 /\ 1:r1=1 /\ 1:r8=1 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=bb8b5ec082212a099fa932ba69254ce3 Cycle=Fre SyncdWW Rfe DpdR PodRW PosWR Fre SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr001 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW Time podrwposwr001 2.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr002.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr002 "Fre SyncdWW Rfe PodRW PosWR Fre SyncdWW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 | stw r1,0(r2) | xor r3,r1,r1 ; sync | stw r3,0(r4) | sync | lwzx r4,r3,r5 ; li r3,1 | lwz r5,0(r4) | li r3,1 | li r6,1 ; stw r3,0(r4) | | stw r3,0(r4) | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ y=2 /\ 1:r1=1 /\ 1:r5=1 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r26,0(r9) _litmus_P1_1_: li r11,1 _litmus_P1_2_: stw r11,0(r2) _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr002 Allowed Histogram (17 states) 153556:>1:r1=0; 1:r5=1; 3:r1=0; 3:r8=1; b=1; y=1; 94540 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r8=1; b=1; y=1; 189630:>1:r1=0; 1:r5=1; 3:r1=1; 3:r8=1; b=1; y=1; 14794 :>1:r1=1; 1:r5=1; 3:r1=1; 3:r8=1; b=1; y=1; 120424:>1:r1=0; 1:r5=1; 3:r1=0; 3:r8=1; b=2; y=1; 1187 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r8=1; b=2; y=1; 202 :>1:r1=0; 1:r5=1; 3:r1=1; 3:r8=1; b=2; y=1; 311649:>1:r1=0; 1:r5=1; 3:r1=0; 3:r8=1; b=1; y=2; 8175 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r8=1; b=1; y=2; 85 :>1:r1=0; 1:r5=2; 3:r1=0; 3:r8=1; b=1; y=2; 3918 :>1:r1=0; 1:r5=1; 3:r1=1; 3:r8=1; b=1; y=2; 19 :>1:r1=1; 1:r5=1; 3:r1=1; 3:r8=1; b=1; y=2; 2 :>1:r1=0; 1:r5=2; 3:r1=1; 3:r8=1; b=1; y=2; 101798:>1:r1=0; 1:r5=1; 3:r1=0; 3:r8=1; b=2; y=2; 1 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r8=1; b=2; y=2; 18 :>1:r1=0; 1:r5=2; 3:r1=0; 3:r8=1; b=2; y=2; 2 :>1:r1=0; 1:r5=1; 3:r1=1; 3:r8=1; b=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ y=2 /\ 1:r1=1 /\ 1:r5=1 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=b357546e4d09fd381f9e48380d4bb1b2 Cycle=Fre SyncdWW Rfe PodRW PosWR Fre SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr002 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW Time podrwposwr002 2.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr003.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr003 "Fre SyncdWW Rfe PodRW PosWR DpdR Fre SyncdWW Rfe DpdR PodRW PosWR" {0:r2=c; 0:r4=x; 1:r2=x; 1:r4=y; 1:r8=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=b; 3:r7=c;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 | stw r1,0(r2) | xor r3,r1,r1 ; sync | stw r3,0(r4) | sync | lwzx r4,r3,r5 ; li r3,1 | lwz r5,0(r4) | li r3,1 | li r6,1 ; stw r3,0(r4) | xor r6,r5,r5 | stw r3,0(r4) | stw r6,0(r7) ; | lwzx r7,r6,r8 | | lwz r8,0(r7) ; exists (c=2 /\ 1:r1=1 /\ 1:r7=0 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r22,0(r11) _litmus_P1_1_: li r24,1 _litmus_P1_2_: stw r24,0(r9) _litmus_P1_3_: lwz r10,0(r9) _litmus_P1_4_: xor r8,r10,r10 _litmus_P1_5_: lwzx r23,r8,r2 _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr003 Allowed Histogram (18 states) 269026:>1:r1=0; 1:r7=0; 3:r1=0; 3:r8=1; c=1; 21073 :>1:r1=1; 1:r7=0; 3:r1=0; 3:r8=1; c=1; 207079:>1:r1=0; 1:r7=1; 3:r1=0; 3:r8=1; c=1; 110543:>1:r1=1; 1:r7=1; 3:r1=0; 3:r8=1; c=1; 34038 :>1:r1=0; 1:r7=0; 3:r1=1; 3:r8=1; c=1; 448 :>1:r1=1; 1:r7=0; 3:r1=1; 3:r8=1; c=1; 141826:>1:r1=0; 1:r7=1; 3:r1=1; 3:r8=1; c=1; 11032 :>1:r1=1; 1:r7=1; 3:r1=1; 3:r8=1; c=1; 91186 :>1:r1=0; 1:r7=0; 3:r1=0; 3:r8=1; c=2; 396 :>1:r1=1; 1:r7=0; 3:r1=0; 3:r8=1; c=2; 107319:>1:r1=0; 1:r7=1; 3:r1=0; 3:r8=1; c=2; 5357 :>1:r1=1; 1:r7=1; 3:r1=0; 3:r8=1; c=2; 28 :>1:r1=0; 1:r7=0; 3:r1=1; 3:r8=1; c=2; 611 :>1:r1=0; 1:r7=1; 3:r1=1; 3:r8=1; c=2; 8 :>1:r1=1; 1:r7=1; 3:r1=1; 3:r8=1; c=2; 18 :>1:r1=0; 1:r7=0; 3:r1=0; 3:r8=2; c=2; 11 :>1:r1=0; 1:r7=1; 3:r1=0; 3:r8=2; c=2; 1 :>1:r1=0; 1:r7=1; 3:r1=1; 3:r8=2; c=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (c=2 /\ 1:r1=1 /\ 1:r7=0 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=3a9e6ab0575e817c7ba95eb14086eea8 Cycle=Fre SyncdWW Rfe PodRW PosWR DpdR Fre SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr003 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW Time podrwposwr003 2.18 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr004.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr004 "Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} 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 ; sync | lwzx r4,r3,r5 | sync | lwzx r4,r3,r5 ; li r3,1 | | li r3,1 | li r6,1 ; stw r3,0(r4) | | stw r3,0(r4) | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r26,0(r9) _litmus_P1_1_: xor r11,r26,r26 _litmus_P1_2_: lwzx r27,r11,r2 _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr004 Allowed Histogram (15 states) 333584:>1:r1=0; 1:r4=0; 3:r1=0; 3:r8=1; b=1; 9969 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r8=1; b=1; 161277:>1:r1=0; 1:r4=1; 3:r1=0; 3:r8=1; b=1; 71803 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r8=1; b=1; 20082 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r8=1; b=1; 93 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r8=1; b=1; 173356:>1:r1=0; 1:r4=1; 3:r1=1; 3:r8=1; b=1; 18423 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r8=1; b=1; 21354 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r8=1; b=2; 1 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r8=1; b=2; 187013:>1:r1=0; 1:r4=1; 3:r1=0; 3:r8=1; b=2; 2767 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r8=1; b=2; 3 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r8=1; b=2; 257 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r8=1; b=2; 18 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r8=2; b=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=7fb4f3887be4df1da142eb0733de7c36 Cycle=Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr004 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW Time podrwposwr004 2.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr005.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr005 "Fre SyncdWR Fre SyncdWW Rfe DpdR PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 2:r7=a;} P0 | P1 | P2 ; li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ; sync | sync | lwzx r4,r3,r5 ; lwz r3,0(r4) | li r3,1 | li r6,1 ; | stw r3,0(r4) | stw r6,0(r7) ; | | lwz r8,0(r7) ; exists (a=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r27,1 _litmus_P1_4_: stw r27,0(r2) _litmus_P2_0_: lwz r21,0(r11) _litmus_P2_1_: xor r23,r21,r21 _litmus_P2_2_: lwzx r10,r23,r9 _litmus_P2_3_: li r8,1 _litmus_P2_4_: stw r8,0(r2) _litmus_P2_5_: lwz r22,0(r2) Test podrwposwr005 Allowed Histogram (7 states) 229570:>0:r3=0; 2:r1=0; 2:r8=1; a=1; 390377:>0:r3=1; 2:r1=0; 2:r8=1; a=1; 1832 :>0:r3=0; 2:r1=1; 2:r8=1; a=1; 157183:>0:r3=1; 2:r1=1; 2:r8=1; a=1; 11914 :>0:r3=0; 2:r1=0; 2:r8=1; a=2; 208988:>0:r3=1; 2:r1=0; 2:r8=1; a=2; 136 :>0:r3=1; 2:r1=1; 2:r8=1; a=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r8=1) is NOT validated Hash=6749f8414aad82ee286645f01befbeb5 Cycle=Fre SyncdWR Fre SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr005 No [PodRW,PosWR] Safe=Fre SyncdWR DpdR BCSyncdWW Time podrwposwr005 1.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr006.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr006 "Fre SyncdWR Fre SyncdWR Fre SyncdWW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ; sync | sync | sync | lwzx r4,r3,r5 ; lwz r3,0(r4) | lwz r3,0(r4) | li r3,1 | li r6,1 ; | | stw r3,0(r4) | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ 0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr006 Allowed Histogram (18 states) 15434 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r8=1; b=1; 236618:>0:r3=1; 1:r3=0; 3:r1=0; 3:r8=1; b=1; 138224:>0:r3=0; 1:r3=1; 3:r1=0; 3:r8=1; b=1; 213525:>0:r3=1; 1:r3=1; 3:r1=0; 3:r8=1; b=1; 111 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r8=1; b=1; 3375 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r8=1; b=1; 32218 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r8=1; b=1; 151062:>0:r3=1; 1:r3=1; 3:r1=1; 3:r8=1; b=1; 7 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r8=1; b=2; 22994 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r8=1; b=2; 9015 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r8=1; b=2; 177239:>0:r3=1; 1:r3=1; 3:r1=0; 3:r8=1; b=2; 1 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r8=1; b=2; 159 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r8=1; b=2; 1 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r8=2; b=2; 3 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r8=2; b=2; 1 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r8=2; b=2; 13 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r8=2; b=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ 0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=7fd03b3defb9d6213343ca85fa975e24 Cycle=Fre SyncdWR Fre SyncdWR Fre SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr006 No [PodRW,PosWR] Safe=Fre SyncdWR DpdR BCSyncdWW Time podrwposwr006 2.01 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr007.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr007 "Fre SyncdWW Wse SyncdWR Fre SyncdWW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ; sync | sync | sync | lwzx r4,r3,r5 ; li r3,1 | lwz r3,0(r4) | li r3,1 | li r6,1 ; stw r3,0(r4) | | stw r3,0(r4) | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr007 Allowed Histogram (14 states) 209095:>1:r3=0; 3:r1=0; 3:r8=1; b=1; x=1; 297153:>1:r3=1; 3:r1=0; 3:r8=1; b=1; x=1; 8715 :>1:r3=0; 3:r1=1; 3:r8=1; b=1; x=1; 193857:>1:r3=1; 3:r1=1; 3:r8=1; b=1; x=1; 8501 :>1:r3=0; 3:r1=0; 3:r8=1; b=2; x=1; 106378:>1:r3=1; 3:r1=0; 3:r8=1; b=2; x=1; 3 :>1:r3=0; 3:r1=1; 3:r8=1; b=2; x=1; 246 :>1:r3=1; 3:r1=1; 3:r8=1; b=2; x=1; 1 :>1:r3=1; 3:r1=0; 3:r8=2; b=2; x=1; 4431 :>1:r3=0; 3:r1=0; 3:r8=1; b=1; x=2; 130759:>1:r3=1; 3:r1=0; 3:r8=1; b=1; x=2; 67 :>1:r3=0; 3:r1=1; 3:r8=1; b=1; x=2; 40318 :>1:r3=1; 3:r1=1; 3:r8=1; b=1; x=2; 476 :>1:r3=1; 3:r1=0; 3:r8=1; b=2; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=e0d280dcb1e849df2259fcdb3f869ad7 Cycle=Fre SyncdWW Wse SyncdWR Fre SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr007 No [PodRW,PosWR] Safe=Fre Wse SyncdWW SyncdWR DpdR BCSyncdWW Time podrwposwr007 2.23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr008.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr008 "Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | xor r3,r1,r1 ; sync | lwz r3,0(r4) | sync | lwzx r4,r3,r5 ; li r3,1 | | li r3,1 | li r6,1 ; stw r3,0(r4) | | stw r3,0(r4) | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: lwz r28,0(r2) _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr008 Allowed Histogram (14 states) 309033:>1:r1=0; 1:r3=0; 3:r1=0; 3:r8=1; b=1; 3835 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r8=1; b=1; 219842:>1:r1=0; 1:r3=1; 3:r1=0; 3:r8=1; b=1; 97236 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r8=1; b=1; 1720 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r8=1; b=1; 41 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r8=1; b=1; 153600:>1:r1=0; 1:r3=1; 3:r1=1; 3:r8=1; b=1; 8184 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r8=1; b=1; 60617 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r8=1; b=2; 144508:>1:r1=0; 1:r3=1; 3:r1=0; 3:r8=1; b=2; 1221 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r8=1; b=2; 139 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r8=1; b=2; 9 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r8=2; b=2; 15 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r8=2; b=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=76a1d4e56495b08e47aa2a4a79623a4a Cycle=Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr008 No [PodRW,PosWR] Safe=Fre SyncdRR DpdR BCSyncdWW Time podrwposwr008 1.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr009.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr009 "Fre SyncdWW Rfe PodRW PosWR DpdW Wse SyncdWW Rfe DpdR PodRW PosWR" {0:r2=c; 0:r4=x; 1:r2=x; 1:r4=y; 1:r8=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r5=b; 3:r7=c;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 | stw r1,0(r2) | xor r3,r1,r1 ; sync | stw r3,0(r4) | sync | lwzx r4,r3,r5 ; li r3,1 | lwz r5,0(r4) | li r3,1 | li r6,1 ; stw r3,0(r4) | xor r6,r5,r5 | stw r3,0(r4) | stw r6,0(r7) ; | li r7,1 | | lwz r8,0(r7) ; | stwx r7,r6,r8 | | ; exists (c=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r23,0(r11) _litmus_P1_1_: li r25,1 _litmus_P1_2_: stw r25,0(r9) _litmus_P1_3_: lwz r24,0(r9) _litmus_P1_4_: xor r10,r24,r24 _litmus_P1_5_: li r8,1 _litmus_P1_6_: stwx r8,r10,r2 _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr009 Allowed Histogram (17 states) 274793:>1:r1=0; 3:r1=0; 3:r8=1; c=1; z=1; 72600 :>1:r1=1; 3:r1=0; 3:r8=1; c=1; z=1; 204496:>1:r1=0; 3:r1=1; 3:r8=1; c=1; z=1; 24744 :>1:r1=1; 3:r1=1; 3:r8=1; c=1; z=1; 158070:>1:r1=0; 3:r1=0; 3:r8=1; c=2; z=1; 5122 :>1:r1=1; 3:r1=0; 3:r8=1; c=2; z=1; 1329 :>1:r1=0; 3:r1=1; 3:r8=1; c=2; z=1; 2 :>1:r1=1; 3:r1=1; 3:r8=1; c=2; z=1; 3 :>1:r1=0; 3:r1=0; 3:r8=2; c=2; z=1; 223511:>1:r1=0; 3:r1=0; 3:r8=1; c=1; z=2; 3588 :>1:r1=1; 3:r1=0; 3:r8=1; c=1; z=2; 25297 :>1:r1=0; 3:r1=1; 3:r8=1; c=1; z=2; 61 :>1:r1=1; 3:r1=1; 3:r8=1; c=1; z=2; 6361 :>1:r1=0; 3:r1=0; 3:r8=1; c=2; z=2; 3 :>1:r1=1; 3:r1=0; 3:r8=1; c=2; z=2; 18 :>1:r1=0; 3:r1=1; 3:r8=1; c=2; z=2; 2 :>1:r1=0; 3:r1=0; 3:r8=2; c=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (c=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=27e687c3515e841d603cb115b4e3f5e8 Cycle=Fre SyncdWW Rfe PodRW PosWR DpdW Wse SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr009 No [PodRW,PosWR] Safe=Fre Wse DpdW DpdR BCSyncdWW Time podrwposwr009 2.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr010.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr010 "Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} 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 ; sync | li r4,1 | sync | lwzx r4,r3,r5 ; li r3,1 | stwx r4,r3,r5 | li r3,1 | li r6,1 ; stw r3,0(r4) | | stw r3,0(r4) | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: xor r28,r27,r27 _litmus_P1_2_: li r11,1 _litmus_P1_3_: stwx r11,r28,r2 _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr010 Allowed Histogram (14 states) 188349:>1:r1=0; 3:r1=0; 3:r8=1; b=1; y=1; 112787:>1:r1=1; 3:r1=0; 3:r8=1; b=1; y=1; 216551:>1:r1=0; 3:r1=1; 3:r8=1; b=1; y=1; 53345 :>1:r1=1; 3:r1=1; 3:r8=1; b=1; y=1; 134222:>1:r1=0; 3:r1=0; 3:r8=1; b=2; y=1; 594 :>1:r1=1; 3:r1=0; 3:r8=1; b=2; y=1; 149 :>1:r1=0; 3:r1=1; 3:r8=1; b=2; y=1; 1 :>1:r1=0; 3:r1=0; 3:r8=2; b=2; y=1; 233760:>1:r1=0; 3:r1=0; 3:r8=1; b=1; y=2; 3966 :>1:r1=1; 3:r1=0; 3:r8=1; b=1; y=2; 44994 :>1:r1=0; 3:r1=1; 3:r8=1; b=1; y=2; 43 :>1:r1=1; 3:r1=1; 3:r8=1; b=1; y=2; 11224 :>1:r1=0; 3:r1=0; 3:r8=1; b=2; y=2; 15 :>1:r1=0; 3:r1=1; 3:r8=1; b=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=60d4f3f7d95c4a1a64be9f8b48cd468f Cycle=Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr010 No [PodRW,PosWR] Safe=Fre Wse DpdW DpdR BCSyncdWW Time podrwposwr010 2.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr011.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr011 "Fre SyncdWW Wse SyncdWW Rfe DpdR PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 2:r7=a;} 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 ; sync | sync | lwzx r4,r3,r5 ; li r3,1 | li r3,1 | li r6,1 ; stw r3,0(r4) | stw r3,0(r4) | stw r6,0(r7) ; | | lwz r8,0(r7) ; exists (a=2 /\ x=2 /\ 2:r1=1 /\ 2:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r27,1 _litmus_P0_4_: stw r27,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r27,1 _litmus_P1_4_: stw r27,0(r2) _litmus_P2_0_: lwz r21,0(r11) _litmus_P2_1_: xor r23,r21,r21 _litmus_P2_2_: lwzx r10,r23,r9 _litmus_P2_3_: li r8,1 _litmus_P2_4_: stw r8,0(r2) _litmus_P2_5_: lwz r22,0(r2) Test podrwposwr011 Allowed Histogram (10 states) 409962:>2:r1=0; 2:r8=1; a=1; x=1; 215769:>2:r1=1; 2:r8=1; a=1; x=1; 255445:>2:r1=0; 2:r8=1; a=2; x=1; 549 :>2:r1=1; 2:r8=1; a=2; x=1; 18 :>2:r1=0; 2:r8=2; a=2; x=1; 1 :>2:r1=1; 2:r8=2; a=2; x=1; 111285:>2:r1=0; 2:r8=1; a=1; x=2; 3260 :>2:r1=1; 2:r8=1; a=1; x=2; 3710 :>2:r1=0; 2:r8=1; a=2; x=2; 1 :>2:r1=0; 2:r8=2; a=2; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ x=2 /\ 2:r1=1 /\ 2:r8=1) is NOT validated Hash=6812a4f46d2627d05fd2b2c903875746 Cycle=Fre SyncdWW Wse SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr011 No [PodRW,PosWR] Safe=Fre Wse SyncdWW DpdR BCSyncdWW Time podrwposwr011 1.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr012.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr012 "Fre SyncdWR Fre SyncdWW Wse SyncdWW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ; sync | sync | sync | lwzx r4,r3,r5 ; lwz r3,0(r4) | li r3,1 | li r3,1 | li r6,1 ; | stw r3,0(r4) | stw r3,0(r4) | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ y=2 /\ 0:r3=0 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr012 Allowed Histogram (15 states) 197233:>0:r3=0; 3:r1=0; 3:r8=1; b=1; y=1; 292221:>0:r3=1; 3:r1=0; 3:r8=1; b=1; y=1; 31840 :>0:r3=0; 3:r1=1; 3:r8=1; b=1; y=1; 183557:>0:r3=1; 3:r1=1; 3:r8=1; b=1; y=1; 2152 :>0:r3=0; 3:r1=0; 3:r8=1; b=2; y=1; 58065 :>0:r3=1; 3:r1=0; 3:r8=1; b=2; y=1; 1 :>0:r3=0; 3:r1=1; 3:r8=1; b=2; y=1; 407 :>0:r3=1; 3:r1=1; 3:r8=1; b=2; y=1; 7380 :>0:r3=0; 3:r1=0; 3:r8=1; b=1; y=2; 213643:>0:r3=1; 3:r1=0; 3:r8=1; b=1; y=2; 80 :>0:r3=0; 3:r1=1; 3:r8=1; b=1; y=2; 1808 :>0:r3=1; 3:r1=1; 3:r8=1; b=1; y=2; 1 :>0:r3=0; 3:r1=0; 3:r8=1; b=2; y=2; 11611 :>0:r3=1; 3:r1=0; 3:r8=1; b=2; y=2; 1 :>0:r3=1; 3:r1=1; 3:r8=1; b=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ y=2 /\ 0:r3=0 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=71036f6017d192189ca47fc4b8e1f811 Cycle=Fre SyncdWR Fre SyncdWW Wse SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr012 No [PodRW,PosWR] Safe=Fre Wse SyncdWW SyncdWR DpdR BCSyncdWW Time podrwposwr012 2.23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr013.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr013 "Fre SyncdWW Wse SyncdWW Wse SyncdWW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | xor r3,r1,r1 ; sync | sync | sync | lwzx r4,r3,r5 ; li r3,1 | li r3,1 | li r3,1 | li r6,1 ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ x=2 /\ y=2 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr013 Allowed Histogram (15 states) 250612:>3:r1=0; 3:r8=1; b=1; x=1; y=1; 209842:>3:r1=1; 3:r8=1; b=1; x=1; y=1; 196171:>3:r1=0; 3:r8=1; b=2; x=1; y=1; 62 :>3:r1=1; 3:r8=1; b=2; x=1; y=1; 20 :>3:r1=0; 3:r8=2; b=2; x=1; y=1; 120919:>3:r1=0; 3:r8=1; b=1; x=2; y=1; 40556 :>3:r1=1; 3:r8=1; b=1; x=2; y=1; 741 :>3:r1=0; 3:r8=1; b=2; x=2; y=1; 172383:>3:r1=0; 3:r8=1; b=1; x=1; y=2; 221 :>3:r1=1; 3:r8=1; b=1; x=1; y=2; 8056 :>3:r1=0; 3:r8=1; b=2; x=1; y=2; 4 :>3:r1=0; 3:r8=2; b=2; x=1; y=2; 411 :>3:r1=0; 3:r8=1; b=1; x=2; y=2; 1 :>3:r1=1; 3:r8=1; b=1; x=2; y=2; 1 :>3:r1=0; 3:r8=1; b=2; x=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ x=2 /\ y=2 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=2874b390989aa5fdecb80ca498d15ae2 Cycle=Fre SyncdWW Wse SyncdWW Wse SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr013 No [PodRW,PosWR] Safe=Fre Wse SyncdWW DpdR BCSyncdWW Time podrwposwr013 2.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr014.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr014 "Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | xor r3,r1,r1 ; sync | li r3,1 | sync | lwzx r4,r3,r5 ; li r3,1 | stw r3,0(r4) | li r3,1 | li r6,1 ; stw r3,0(r4) | | stw r3,0(r4) | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r28,1 _litmus_P1_3_: stw r28,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr014 Allowed Histogram (13 states) 308409:>1:r1=0; 3:r1=0; 3:r8=1; b=1; y=1; 120580:>1:r1=1; 3:r1=0; 3:r8=1; b=1; y=1; 216262:>1:r1=0; 3:r1=1; 3:r8=1; b=1; y=1; 30758 :>1:r1=1; 3:r1=1; 3:r8=1; b=1; y=1; 67840 :>1:r1=0; 3:r1=0; 3:r8=1; b=2; y=1; 634 :>1:r1=1; 3:r1=0; 3:r8=1; b=2; y=1; 302 :>1:r1=0; 3:r1=1; 3:r8=1; b=2; y=1; 1 :>1:r1=0; 3:r1=0; 3:r8=2; b=2; y=1; 236659:>1:r1=0; 3:r1=0; 3:r8=1; b=1; y=2; 2015 :>1:r1=1; 3:r1=0; 3:r8=1; b=1; y=2; 4910 :>1:r1=0; 3:r1=1; 3:r8=1; b=1; y=2; 17 :>1:r1=1; 3:r1=1; 3:r8=1; b=1; y=2; 11613 :>1:r1=0; 3:r1=0; 3:r8=1; b=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=bfef89c4a0b4a39d057900045bdf574b Cycle=Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe DpdR PodRW PosWR Relax podrwposwr014 No [PodRW,PosWR] Safe=Fre Wse SyncdRW DpdR BCSyncdWW Time podrwposwr014 2.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr015.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr015 "Fre SyncdWW Rfe SyncdRW Rfe DpdR PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 2:r7=a;} P0 | P1 | P2 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | xor r3,r1,r1 ; sync | li r3,1 | lwzx r4,r3,r5 ; li r3,1 | stw r3,0(r4) | li r6,1 ; stw r3,0(r4) | | stw r6,0(r7) ; | | lwz r8,0(r7) ; exists (a=2 /\ 1:r1=1 /\ 2:r1=1 /\ 2:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r27,1 _litmus_P0_4_: stw r27,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r28,1 _litmus_P1_3_: stw r28,0(r2) _litmus_P2_0_: lwz r21,0(r11) _litmus_P2_1_: xor r23,r21,r21 _litmus_P2_2_: lwzx r10,r23,r9 _litmus_P2_3_: li r8,1 _litmus_P2_4_: stw r8,0(r2) _litmus_P2_5_: lwz r22,0(r2) Test podrwposwr015 Allowed Histogram (7 states) 543818:>1:r1=0; 2:r1=0; 2:r8=1; a=1; 78557 :>1:r1=1; 2:r1=0; 2:r8=1; a=1; 112152:>1:r1=0; 2:r1=1; 2:r8=1; a=1; 696 :>1:r1=1; 2:r1=1; 2:r8=1; a=1; 263902:>1:r1=0; 2:r1=0; 2:r8=1; a=2; 540 :>1:r1=1; 2:r1=0; 2:r8=1; a=2; 335 :>1:r1=0; 2:r1=1; 2:r8=1; a=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ 1:r1=1 /\ 2:r1=1 /\ 2:r8=1) is NOT validated Hash=9db63ed8b622d1d85b3a6d2ccc8db148 Cycle=Fre SyncdWW Rfe SyncdRW Rfe DpdR PodRW PosWR Relax podrwposwr015 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW BCSyncdRW Time podrwposwr015 1.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr016.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr016 "Fre SyncdWR Fre SyncdWW Rfe SyncdRW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | xor r3,r1,r1 ; sync | sync | li r3,1 | lwzx r4,r3,r5 ; lwz r3,0(r4) | li r3,1 | stw r3,0(r4) | li r6,1 ; | stw r3,0(r4) | | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: lwz r27,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r28,1 _litmus_P2_3_: stw r28,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr016 Allowed Histogram (17 states) 192528:>0:r3=0; 2:r1=0; 3:r1=0; 3:r8=1; b=1; 237628:>0:r3=1; 2:r1=0; 3:r1=0; 3:r8=1; b=1; 5186 :>0:r3=0; 2:r1=1; 3:r1=0; 3:r8=1; b=1; 106991:>0:r3=1; 2:r1=1; 3:r1=0; 3:r8=1; b=1; 54653 :>0:r3=0; 2:r1=0; 3:r1=1; 3:r8=1; b=1; 203521:>0:r3=1; 2:r1=0; 3:r1=1; 3:r8=1; b=1; 26 :>0:r3=0; 2:r1=1; 3:r1=1; 3:r8=1; b=1; 2372 :>0:r3=1; 2:r1=1; 3:r1=1; 3:r8=1; b=1; 7310 :>0:r3=0; 2:r1=0; 3:r1=0; 3:r8=1; b=2; 167186:>0:r3=1; 2:r1=0; 3:r1=0; 3:r8=1; b=2; 1 :>0:r3=0; 2:r1=1; 3:r1=0; 3:r8=1; b=2; 22124 :>0:r3=1; 2:r1=1; 3:r1=0; 3:r8=1; b=2; 1 :>0:r3=0; 2:r1=0; 3:r1=1; 3:r8=1; b=2; 459 :>0:r3=1; 2:r1=0; 3:r1=1; 3:r8=1; b=2; 1 :>0:r3=1; 2:r1=1; 3:r1=1; 3:r8=1; b=2; 2 :>0:r3=0; 2:r1=0; 3:r1=0; 3:r8=2; b=2; 11 :>0:r3=1; 2:r1=0; 3:r1=0; 3:r8=2; b=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=370d47d5790ee8b332d0eee0530bd0b6 Cycle=Fre SyncdWR Fre SyncdWW Rfe SyncdRW Rfe DpdR PodRW PosWR Relax podrwposwr016 No [PodRW,PosWR] Safe=Fre SyncdWR DpdR BCSyncdWW BCSyncdRW Time podrwposwr016 1.95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr017.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr017 "Fre SyncdWW Wse SyncdWW Rfe SyncdRW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | xor r3,r1,r1 ; sync | sync | li r3,1 | lwzx r4,r3,r5 ; li r3,1 | li r3,1 | stw r3,0(r4) | li r6,1 ; stw r3,0(r4) | stw r3,0(r4) | | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: lwz r27,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r28,1 _litmus_P2_3_: stw r28,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr017 Allowed Histogram (14 states) 279674:>2:r1=0; 3:r1=0; 3:r8=1; b=1; x=1; 96598 :>2:r1=1; 3:r1=0; 3:r8=1; b=1; x=1; 225516:>2:r1=0; 3:r1=1; 3:r8=1; b=1; x=1; 1163 :>2:r1=1; 3:r1=1; 3:r8=1; b=1; x=1; 157443:>2:r1=0; 3:r1=0; 3:r8=1; b=2; x=1; 7021 :>2:r1=1; 3:r1=0; 3:r8=1; b=2; x=1; 97 :>2:r1=0; 3:r1=1; 3:r8=1; b=2; x=1; 1 :>2:r1=0; 3:r1=0; 3:r8=2; b=2; x=1; 132855:>2:r1=0; 3:r1=0; 3:r8=1; b=1; x=2; 813 :>2:r1=1; 3:r1=0; 3:r8=1; b=1; x=2; 98628 :>2:r1=0; 3:r1=1; 3:r8=1; b=1; x=2; 6 :>2:r1=1; 3:r1=1; 3:r8=1; b=1; x=2; 182 :>2:r1=0; 3:r1=0; 3:r8=1; b=2; x=2; 3 :>2:r1=0; 3:r1=1; 3:r8=1; b=2; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=29cfb974bdeccadd1d609c19cb52cad8 Cycle=Fre SyncdWW Wse SyncdWW Rfe SyncdRW Rfe DpdR PodRW PosWR Relax podrwposwr017 No [PodRW,PosWR] Safe=Fre Wse SyncdWW DpdR BCSyncdWW BCSyncdRW Time podrwposwr017 2.16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr018.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr018 "Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe DpdR PodRW PosWR" {0:r2=b; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a; 3:r7=b;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | xor r3,r1,r1 ; sync | li r3,1 | li r3,1 | lwzx r4,r3,r5 ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) | li r6,1 ; stw r3,0(r4) | | | stw r6,0(r7) ; | | | lwz r8,0(r7) ; exists (b=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r8=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r28,1 _litmus_P1_3_: stw r28,0(r2) _litmus_P2_0_: lwz r27,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r28,1 _litmus_P2_3_: stw r28,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: xor r24,r22,r22 _litmus_P3_2_: lwzx r10,r24,r9 _litmus_P3_3_: li r8,1 _litmus_P3_4_: stw r8,0(r2) _litmus_P3_5_: lwz r23,0(r2) Test podrwposwr018 Allowed Histogram (15 states) 232997:>1:r1=0; 2:r1=0; 3:r1=0; 3:r8=1; b=1; 119358:>1:r1=1; 2:r1=0; 3:r1=0; 3:r8=1; b=1; 211625:>1:r1=0; 2:r1=1; 3:r1=0; 3:r8=1; b=1; 966 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r8=1; b=1; 191517:>1:r1=0; 2:r1=0; 3:r1=1; 3:r8=1; b=1; 21930 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r8=1; b=1; 475 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r8=1; b=1; 1 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r8=1; b=1; 181720:>1:r1=0; 2:r1=0; 3:r1=0; 3:r8=1; b=2; 1048 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r8=1; b=2; 38159 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r8=1; b=2; 1 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r8=1; b=2; 189 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r8=1; b=2; 11 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r8=2; b=2; 3 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r8=2; b=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (b=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r8=1) is NOT validated Hash=4a2cb2426fd918bcf64efa0fbf334c9a Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe DpdR PodRW PosWR Relax podrwposwr018 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW BCSyncdRW Time podrwposwr018 1.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr019.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr019 "Fre SyncdWW Rfe PodRW PosWR" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;} P0 | P1 ; li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 ; sync | stw r3,0(r4) ; li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | ; exists (y=2 /\ 1:r1=1 /\ 1:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r26,0(r9) _litmus_P1_1_: li r11,1 _litmus_P1_2_: stw r11,0(r2) _litmus_P1_3_: lwz r27,0(r2) Test podrwposwr019 Allowed Histogram (4 states) 974139:>1:r1=0; 1:r5=1; y=1; 77667 :>1:r1=1; 1:r5=1; y=1; 948188:>1:r1=0; 1:r5=1; y=2; 6 :>1:r1=0; 1:r5=2; y=2; No Witnesses Positive: 0, Negative: 2000000 Condition exists (y=2 /\ 1:r1=1 /\ 1:r5=1) is NOT validated Hash=e1a05a735e2af62156abbb450cbe4050 Cycle=Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr019 No [PodRW,PosWR] Safe=Fre BCSyncdWW Time podrwposwr019 1.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr020.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr020 "Fre SyncdWW Rfe PodRW PosWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 | stw r1,0(r2) | li r3,1 ; sync | stw r3,0(r4) | sync | stw r3,0(r4) ; li r3,1 | lwz r5,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (a=2 /\ y=2 /\ 1:r1=1 /\ 1:r5=1 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r26,0(r9) _litmus_P1_1_: li r11,1 _litmus_P1_2_: stw r11,0(r2) _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr020 Allowed Histogram (21 states) 104418:>1:r1=0; 1:r5=1; 3:r1=0; 3:r5=1; a=1; y=1; 150462:>1:r1=1; 1:r5=1; 3:r1=0; 3:r5=1; a=1; y=1; 105345:>1:r1=0; 1:r5=1; 3:r1=1; 3:r5=1; a=1; y=1; 46532 :>1:r1=1; 1:r5=1; 3:r1=1; 3:r5=1; a=1; y=1; 262034:>1:r1=0; 1:r5=1; 3:r1=0; 3:r5=1; a=2; y=1; 7612 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r5=1; a=2; y=1; 12292 :>1:r1=0; 1:r5=1; 3:r1=1; 3:r5=1; a=2; y=1; 8 :>1:r1=1; 1:r5=1; 3:r1=1; 3:r5=1; a=2; y=1; 27 :>1:r1=0; 1:r5=1; 3:r1=0; 3:r5=2; a=2; y=1; 2 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r5=2; a=2; y=1; 189805:>1:r1=0; 1:r5=1; 3:r1=0; 3:r5=1; a=1; y=2; 6697 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r5=1; a=1; y=2; 22 :>1:r1=0; 1:r5=2; 3:r1=0; 3:r5=1; a=1; y=2; 14607 :>1:r1=0; 1:r5=1; 3:r1=1; 3:r5=1; a=1; y=2; 2 :>1:r1=1; 1:r5=1; 3:r1=1; 3:r5=1; a=1; y=2; 4 :>1:r1=0; 1:r5=2; 3:r1=1; 3:r5=1; a=1; y=2; 99986 :>1:r1=0; 1:r5=1; 3:r1=0; 3:r5=1; a=2; y=2; 78 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r5=1; a=2; y=2; 24 :>1:r1=0; 1:r5=2; 3:r1=0; 3:r5=1; a=2; y=2; 28 :>1:r1=0; 1:r5=1; 3:r1=1; 3:r5=1; a=2; y=2; 15 :>1:r1=0; 1:r5=1; 3:r1=0; 3:r5=2; a=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ y=2 /\ 1:r1=1 /\ 1:r5=1 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=55e0dc77e839b18b16089d0a95ebef97 Cycle=Fre SyncdWW Rfe PodRW PosWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr020 No [PodRW,PosWR] Safe=Fre BCSyncdWW Time podrwposwr020 2.04 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr021.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr021 "DpdR Fre SyncdWW Rfe PodRW PosWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 | stw r1,0(r2) | li r3,1 ; sync | stw r3,0(r4) | sync | stw r3,0(r4) ; li r3,1 | lwz r5,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (z=2 /\ 1:r1=1 /\ 1:r5=1 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r28,1 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r26,0(r9) _litmus_P1_1_: li r11,1 _litmus_P1_2_: stw r11,0(r2) _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: li r24,1 _litmus_P3_2_: stw r24,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r23,r8,r2 Test podrwposwr021 Allowed Histogram (19 states) 255336:>1:r1=0; 1:r5=1; 3:r1=0; 3:r7=0; z=1; 9883 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r7=0; z=1; 4543 :>1:r1=0; 1:r5=1; 3:r1=1; 3:r7=0; z=1; 5 :>1:r1=1; 1:r5=1; 3:r1=1; 3:r7=0; z=1; 114740:>1:r1=0; 1:r5=1; 3:r1=0; 3:r7=1; z=1; 145208:>1:r1=1; 1:r5=1; 3:r1=0; 3:r7=1; z=1; 146405:>1:r1=0; 1:r5=1; 3:r1=1; 3:r7=1; z=1; 26109 :>1:r1=1; 1:r5=1; 3:r1=1; 3:r7=1; z=1; 67204 :>1:r1=0; 1:r5=1; 3:r1=0; 3:r7=0; z=2; 22 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r7=0; z=2; 26 :>1:r1=0; 1:r5=2; 3:r1=0; 3:r7=0; z=2; 125 :>1:r1=0; 1:r5=1; 3:r1=1; 3:r7=0; z=2; 200340:>1:r1=0; 1:r5=1; 3:r1=0; 3:r7=1; z=2; 11078 :>1:r1=1; 1:r5=1; 3:r1=0; 3:r7=1; z=2; 45 :>1:r1=0; 1:r5=2; 3:r1=0; 3:r7=1; z=2; 9 :>1:r1=1; 1:r5=2; 3:r1=0; 3:r7=1; z=2; 18905 :>1:r1=0; 1:r5=1; 3:r1=1; 3:r7=1; z=2; 12 :>1:r1=1; 1:r5=1; 3:r1=1; 3:r7=1; z=2; 5 :>1:r1=0; 1:r5=2; 3:r1=1; 3:r7=1; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 1:r5=1 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=be452c40a366d7f569ebf0a838c206ca Cycle=DpdR Fre SyncdWW Rfe PodRW PosWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr021 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW Time podrwposwr021 1.95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr022.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr022 "DpdW Wse SyncdWW Rfe PodRW PosWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 | stw r1,0(r2) | li r3,1 ; sync | stw r3,0(r4) | sync | stw r3,0(r4) ; li r3,1 | lwz r5,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ z=2 /\ 1:r1=1 /\ 1:r5=1 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r26,0(r9) _litmus_P1_1_: li r11,1 _litmus_P1_2_: stw r11,0(r2) _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr022 Allowed Histogram (20 states) 76775 :>1:r1=0; 1:r5=1; 3:r1=0; x=1; z=1; 134097:>1:r1=1; 1:r5=1; 3:r1=0; x=1; z=1; 166685:>1:r1=0; 1:r5=1; 3:r1=1; x=1; z=1; 7086 :>1:r1=1; 1:r5=1; 3:r1=1; x=1; z=1; 162628:>1:r1=0; 1:r5=1; 3:r1=0; x=2; z=1; 9600 :>1:r1=1; 1:r5=1; 3:r1=0; x=2; z=1; 3852 :>1:r1=0; 1:r5=1; 3:r1=1; x=2; z=1; 1 :>1:r1=1; 1:r5=1; 3:r1=1; x=2; z=1; 253690:>1:r1=0; 1:r5=1; 3:r1=0; x=1; z=2; 37222 :>1:r1=1; 1:r5=1; 3:r1=0; x=1; z=2; 250 :>1:r1=0; 1:r5=2; 3:r1=0; x=1; z=2; 53 :>1:r1=1; 1:r5=2; 3:r1=0; x=1; z=2; 4154 :>1:r1=0; 1:r5=1; 3:r1=1; x=1; z=2; 93 :>1:r1=1; 1:r5=1; 3:r1=1; x=1; z=2; 4 :>1:r1=0; 1:r5=2; 3:r1=1; x=1; z=2; 1 :>1:r1=1; 1:r5=2; 3:r1=1; x=1; z=2; 143558:>1:r1=0; 1:r5=1; 3:r1=0; x=2; z=2; 60 :>1:r1=1; 1:r5=1; 3:r1=0; x=2; z=2; 187 :>1:r1=0; 1:r5=2; 3:r1=0; x=2; z=2; 4 :>1:r1=0; 1:r5=1; 3:r1=1; x=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 1:r5=1 /\ 3:r1=1) is NOT validated Hash=d07200dfdc6b7ffba60e71b31b4afa6f Cycle=DpdW Wse SyncdWW Rfe PodRW PosWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr022 No [PodRW,PosWR] Safe=Fre Wse DpdW BCSyncdWW Time podrwposwr022 2.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr023.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr023 "DpdR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 1:r8=x;} P0 | P1 ; li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 ; sync | stw r3,0(r4) ; li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | xor r6,r5,r5 ; | lwzx r7,r6,r8 ; exists (1:r1=1 /\ 1:r7=0) Generated assembler _litmus_P0_0_: li r30,1 _litmus_P0_1_: stw r30,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r23,0(r11) _litmus_P1_1_: li r25,1 _litmus_P1_2_: stw r25,0(r9) _litmus_P1_3_: lwz r10,0(r9) _litmus_P1_4_: xor r8,r10,r10 _litmus_P1_5_: lwzx r24,r8,r2 Test podrwposwr023 Allowed Histogram (4 states) 920733:>1:r1=0; 1:r7=0; 178 :>1:r1=1; 1:r7=0; 813107:>1:r1=0; 1:r7=1; 265982:>1:r1=1; 1:r7=1; Ok Witnesses Positive: 178, Negative: 1999822 Condition exists (1:r1=1 /\ 1:r7=0) is validated Hash=35db93d049ff2602711978cfa4ebd6bb Cycle=DpdR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr023 Ok [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW Time podrwposwr023 1.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr024.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr024 "DpdR Fre SyncdWW Rfe PodRW PosWR DpdR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 1:r8=a; 2:r2=a; 2:r4=b; 3:r2=b; 3:r4=c; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 | stw r1,0(r2) | li r3,1 ; sync | stw r3,0(r4) | sync | stw r3,0(r4) ; li r3,1 | lwz r5,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | xor r6,r5,r5 | stw r3,0(r4) | xor r6,r5,r5 ; | lwzx r7,r6,r8 | | lwzx r7,r6,r8 ; exists (1:r1=1 /\ 1:r7=0 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r30,1 _litmus_P0_1_: stw r30,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r23,0(r11) _litmus_P1_1_: li r25,1 _litmus_P1_2_: stw r25,0(r9) _litmus_P1_3_: lwz r10,0(r9) _litmus_P1_4_: xor r8,r10,r10 _litmus_P1_5_: lwzx r24,r8,r2 _litmus_P2_0_: li r30,1 _litmus_P2_1_: stw r30,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r24,r8,r2 Test podrwposwr024 Allowed Histogram (15 states) 101649:>1:r1=0; 1:r7=0; 3:r1=0; 3:r7=0; 132 :>1:r1=1; 1:r7=0; 3:r1=0; 3:r7=0; 179930:>1:r1=0; 1:r7=1; 3:r1=0; 3:r7=0; 13592 :>1:r1=1; 1:r7=1; 3:r1=0; 3:r7=0; 613 :>1:r1=0; 1:r7=0; 3:r1=1; 3:r7=0; 20135 :>1:r1=0; 1:r7=1; 3:r1=1; 3:r7=0; 78 :>1:r1=1; 1:r7=1; 3:r1=1; 3:r7=0; 259711:>1:r1=0; 1:r7=0; 3:r1=0; 3:r7=1; 11657 :>1:r1=1; 1:r7=0; 3:r1=0; 3:r7=1; 138643:>1:r1=0; 1:r7=1; 3:r1=0; 3:r7=1; 75355 :>1:r1=1; 1:r7=1; 3:r1=0; 3:r7=1; 36300 :>1:r1=0; 1:r7=0; 3:r1=1; 3:r7=1; 101 :>1:r1=1; 1:r7=0; 3:r1=1; 3:r7=1; 146833:>1:r1=0; 1:r7=1; 3:r1=1; 3:r7=1; 15271 :>1:r1=1; 1:r7=1; 3:r1=1; 3:r7=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r7=0 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=6d9c7c70e2dd54acb35c9042e36adb32 Cycle=DpdR Fre SyncdWW Rfe PodRW PosWR DpdR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr024 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW Time podrwposwr024 1.85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr025.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr025 "DpdW Wse SyncdWW Rfe PodRW PosWR DpdR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 1:r8=a; 2:r2=a; 2:r4=b; 3:r2=b; 3:r4=c; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 | stw r1,0(r2) | li r3,1 ; sync | stw r3,0(r4) | sync | stw r3,0(r4) ; li r3,1 | lwz r5,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | xor r6,r5,r5 | stw r3,0(r4) | xor r6,r5,r5 ; | lwzx r7,r6,r8 | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ 1:r1=1 /\ 1:r7=0 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r22,0(r11) _litmus_P1_1_: li r24,1 _litmus_P1_2_: stw r24,0(r9) _litmus_P1_3_: lwz r10,0(r9) _litmus_P1_4_: xor r8,r10,r10 _litmus_P1_5_: lwzx r23,r8,r2 _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr025 Allowed Histogram (15 states) 266995:>1:r1=0; 1:r7=0; 3:r1=0; x=1; 10644 :>1:r1=1; 1:r7=0; 3:r1=0; x=1; 157227:>1:r1=0; 1:r7=1; 3:r1=0; x=1; 106913:>1:r1=1; 1:r7=1; 3:r1=0; x=1; 36462 :>1:r1=0; 1:r7=0; 3:r1=1; x=1; 63 :>1:r1=1; 1:r7=0; 3:r1=1; x=1; 125746:>1:r1=0; 1:r7=1; 3:r1=1; x=1; 24639 :>1:r1=1; 1:r7=1; 3:r1=1; x=1; 54145 :>1:r1=0; 1:r7=0; 3:r1=0; x=2; 323 :>1:r1=1; 1:r7=0; 3:r1=0; x=2; 196280:>1:r1=0; 1:r7=1; 3:r1=0; x=2; 15148 :>1:r1=1; 1:r7=1; 3:r1=0; x=2; 69 :>1:r1=0; 1:r7=0; 3:r1=1; x=2; 5320 :>1:r1=0; 1:r7=1; 3:r1=1; x=2; 26 :>1:r1=1; 1:r7=1; 3:r1=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 1:r1=1 /\ 1:r7=0 /\ 3:r1=1) is NOT validated Hash=818f9c03e437ee15839006897915a9aa Cycle=DpdW Wse SyncdWW Rfe PodRW PosWR DpdR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr025 No [PodRW,PosWR] Safe=Fre Wse DpdW DpdR BCSyncdWW Time podrwposwr025 2.12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr026.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr026 "Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | li r3,1 ; sync | lwzx r4,r3,r5 | sync | stw r3,0(r4) ; li r3,1 | | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (a=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r26,0(r9) _litmus_P1_1_: xor r11,r26,r26 _litmus_P1_2_: lwzx r27,r11,r2 _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr026 Allowed Histogram (17 states) 218507:>1:r1=0; 1:r4=0; 3:r1=0; 3:r5=1; a=1; 16641 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r5=1; a=1; 62220 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r5=1; a=1; 167431:>1:r1=1; 1:r4=1; 3:r1=0; 3:r5=1; a=1; 3813 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r5=1; a=1; 2 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r5=1; a=1; 141719:>1:r1=0; 1:r4=1; 3:r1=1; 3:r5=1; a=1; 9159 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r5=1; a=1; 111600:>1:r1=0; 1:r4=0; 3:r1=0; 3:r5=1; a=2; 933 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r5=1; a=2; 192507:>1:r1=0; 1:r4=1; 3:r1=0; 3:r5=1; a=2; 67154 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r5=1; a=2; 10 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r5=1; a=2; 8278 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r5=1; a=2; 4 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r5=1; a=2; 14 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r5=2; a=2; 8 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r5=2; a=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=275666370df7ed99407e310788ddd232 Cycle=Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr026 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW Time podrwposwr026 1.74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr027.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr027 "DpdR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=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) | li r3,1 ; sync | lwzx r4,r3,r5 | sync | stw r3,0(r4) ; li r3,1 | | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r30,1 _litmus_P0_1_: stw r30,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: xor r11,r27,r27 _litmus_P1_2_: lwzx r30,r11,r2 _litmus_P2_0_: li r4,1 _litmus_P2_1_: stw r4,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r24,r8,r2 Test podrwposwr027 Allowed Histogram (15 states) 47587 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r7=0; 21 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r7=0; 185860:>1:r1=0; 1:r4=1; 3:r1=0; 3:r7=0; 28306 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r7=0; 20 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r7=0; 1790 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r7=0; 3 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r7=0; 294311:>1:r1=0; 1:r4=0; 3:r1=0; 3:r7=1; 9657 :>1:r1=1; 1:r4=0; 3:r1=0; 3:r7=1; 157745:>1:r1=0; 1:r4=1; 3:r1=0; 3:r7=1; 65339 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r7=1; 27812 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r7=1; 44 :>1:r1=1; 1:r4=0; 3:r1=1; 3:r7=1; 160601:>1:r1=0; 1:r4=1; 3:r1=1; 3:r7=1; 20904 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r7=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=f961b60e093edbcd0892f005e4c3eccd Cycle=DpdR Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr027 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW Time podrwposwr027 1.66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr028.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr028 "DpdW Wse SyncdWW Rfe DpdR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} 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) | li r3,1 ; sync | lwzx r4,r3,r5 | sync | stw r3,0(r4) ; li r3,1 | | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r26,0(r9) _litmus_P1_1_: xor r11,r26,r26 _litmus_P1_2_: lwzx r27,r11,r2 _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr028 Allowed Histogram (14 states) 301549:>1:r1=0; 1:r4=0; 3:r1=0; x=1; 13676 :>1:r1=1; 1:r4=0; 3:r1=0; x=1; 109665:>1:r1=0; 1:r4=1; 3:r1=0; x=1; 102030:>1:r1=1; 1:r4=1; 3:r1=0; x=1; 13286 :>1:r1=0; 1:r4=0; 3:r1=1; x=1; 43 :>1:r1=1; 1:r4=0; 3:r1=1; x=1; 176082:>1:r1=0; 1:r4=1; 3:r1=1; x=1; 8177 :>1:r1=1; 1:r4=1; 3:r1=1; x=1; 100067:>1:r1=0; 1:r4=0; 3:r1=0; x=2; 8 :>1:r1=1; 1:r4=0; 3:r1=0; x=2; 166832:>1:r1=0; 1:r4=1; 3:r1=0; x=2; 6389 :>1:r1=1; 1:r4=1; 3:r1=0; x=2; 13 :>1:r1=0; 1:r4=0; 3:r1=1; x=2; 2183 :>1:r1=0; 1:r4=1; 3:r1=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1) is NOT validated Hash=100fe79acea0c659173693e7910964aa Cycle=DpdW Wse SyncdWW Rfe DpdR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr028 No [PodRW,PosWR] Safe=Fre Wse DpdW DpdR BCSyncdWW Time podrwposwr028 1.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr029.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr029 "Fre SyncdWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | stw r3,0(r4) ; lwz r3,0(r4) | li r3,1 | lwz r5,0(r4) ; | stw r3,0(r4) | ; exists (z=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r27,1 _litmus_P1_4_: stw r27,0(r2) _litmus_P2_0_: lwz r25,0(r9) _litmus_P2_1_: li r11,1 _litmus_P2_2_: stw r11,0(r2) _litmus_P2_3_: lwz r26,0(r2) Test podrwposwr029 Allowed Histogram (9 states) 216892:>0:r3=0; 2:r1=0; 2:r5=1; z=1; 199605:>0:r3=1; 2:r1=0; 2:r5=1; z=1; 5225 :>0:r3=0; 2:r1=1; 2:r5=1; z=1; 251319:>0:r3=1; 2:r1=1; 2:r5=1; z=1; 16166 :>0:r3=0; 2:r1=0; 2:r5=1; z=2; 309685:>0:r3=1; 2:r1=0; 2:r5=1; z=2; 1090 :>0:r3=1; 2:r1=1; 2:r5=1; z=2; 1 :>0:r3=0; 2:r1=0; 2:r5=2; z=2; 17 :>0:r3=1; 2:r1=0; 2:r5=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r5=1) is NOT validated Hash=7bcfb2074b4288f5116655fc59e2693d Cycle=Fre SyncdWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr029 No [PodRW,PosWR] Safe=Fre SyncdWR BCSyncdWW Time podrwposwr029 1.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr030.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr030 "DpdR Fre SyncdWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 2:r8=x;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | stw r3,0(r4) ; lwz r3,0(r4) | li r3,1 | lwz r5,0(r4) ; | stw r3,0(r4) | xor r6,r5,r5 ; | | lwzx r7,r6,r8 ; exists (0:r3=0 /\ 2:r1=1 /\ 2:r7=0) Generated assembler _litmus_P0_0_: li r30,1 _litmus_P0_1_: stw r30,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r30,1 _litmus_P1_1_: stw r30,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: lwz r22,0(r11) _litmus_P2_1_: li r24,1 _litmus_P2_2_: stw r24,0(r9) _litmus_P2_3_: lwz r10,0(r9) _litmus_P2_4_: xor r8,r10,r10 _litmus_P2_5_: lwzx r23,r8,r2 Test podrwposwr030 Allowed Histogram (7 states) 52968 :>0:r3=0; 2:r1=0; 2:r7=0; 454371:>0:r3=1; 2:r1=0; 2:r7=0; 16347 :>0:r3=1; 2:r1=1; 2:r7=0; 272126:>0:r3=0; 2:r1=0; 2:r7=1; 134683:>0:r3=1; 2:r1=0; 2:r7=1; 1480 :>0:r3=0; 2:r1=1; 2:r7=1; 68025 :>0:r3=1; 2:r1=1; 2:r7=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r7=0) is NOT validated Hash=49af5736723e09ed1e4f51bd7b63a6a1 Cycle=DpdR Fre SyncdWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr030 No [PodRW,PosWR] Safe=Fre SyncdWR DpdR BCSyncdWW Time podrwposwr030 1.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr031.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr031 "Fre SyncdWR Fre SyncdWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; lwz r3,0(r4) | lwz r3,0(r4) | li r3,1 | lwz r5,0(r4) ; | | stw r3,0(r4) | ; exists (a=2 /\ 0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr031 Allowed Histogram (15 states) 691 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r5=1; a=1; 192096:>0:r3=1; 1:r3=0; 3:r1=0; 3:r5=1; a=1; 202343:>0:r3=0; 1:r3=1; 3:r1=0; 3:r5=1; a=1; 90506 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r5=1; a=1; 2 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r5=1; a=1; 1445 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r5=1; a=1; 99559 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r5=1; a=1; 144318:>0:r3=1; 1:r3=1; 3:r1=1; 3:r5=1; a=1; 115 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r5=1; a=2; 14993 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r5=1; a=2; 29621 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r5=1; a=2; 219301:>0:r3=1; 1:r3=1; 3:r1=0; 3:r5=1; a=2; 18 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r5=1; a=2; 12 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r5=1; a=2; 4980 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r5=1; a=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ 0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=146dd5508d3fcfb982d1233d084cbdd3 Cycle=Fre SyncdWR Fre SyncdWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr031 No [PodRW,PosWR] Safe=Fre SyncdWR BCSyncdWW Time podrwposwr031 1.80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr032.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr032 "DpdR Fre SyncdWR Fre SyncdWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; lwz r3,0(r4) | lwz r3,0(r4) | li r3,1 | lwz r5,0(r4) ; | | stw r3,0(r4) | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r30,1 _litmus_P0_1_: stw r30,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r29,0(r2) _litmus_P1_0_: li r30,1 _litmus_P1_1_: stw r30,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r3,0(r2) _litmus_P2_0_: li r4,1 _litmus_P2_1_: stw r4,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r24,r8,r2 Test podrwposwr032 Allowed Histogram (15 states) 69 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r7=0; 34963 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r7=0; 31948 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r7=0; 201269:>0:r3=1; 1:r3=1; 3:r1=0; 3:r7=0; 17 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r7=0; 16 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r7=0; 5698 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r7=0; 19637 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r7=1; 200568:>0:r3=1; 1:r3=0; 3:r1=0; 3:r7=1; 97621 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r7=1; 198485:>0:r3=1; 1:r3=1; 3:r1=0; 3:r7=1; 52 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r7=1; 5733 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r7=1; 36687 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r7=1; 167237:>0:r3=1; 1:r3=1; 3:r1=1; 3:r7=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=c0150ff916c761067419d1bdc686ac94 Cycle=DpdR Fre SyncdWR Fre SyncdWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr032 No [PodRW,PosWR] Safe=Fre SyncdWR DpdR BCSyncdWW Time podrwposwr032 1.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr033.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr033 "DpdW Wse SyncdWR Fre SyncdWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; lwz r3,0(r4) | lwz r3,0(r4) | li r3,1 | lwz r5,0(r4) ; | | stw r3,0(r4) | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ 0:r3=0 /\ 1:r3=0 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr033 Allowed Histogram (15 states) 11362 :>0:r3=0; 1:r3=0; 3:r1=0; x=1; 208290:>0:r3=1; 1:r3=0; 3:r1=0; x=1; 180159:>0:r3=0; 1:r3=1; 3:r1=0; x=1; 139255:>0:r3=1; 1:r3=1; 3:r1=0; x=1; 27 :>0:r3=0; 1:r3=0; 3:r1=1; x=1; 1747 :>0:r3=1; 1:r3=0; 3:r1=1; x=1; 70452 :>0:r3=0; 1:r3=1; 3:r1=1; x=1; 158559:>0:r3=1; 1:r3=1; 3:r1=1; x=1; 77 :>0:r3=0; 1:r3=0; 3:r1=0; x=2; 10906 :>0:r3=1; 1:r3=0; 3:r1=0; x=2; 11343 :>0:r3=0; 1:r3=1; 3:r1=0; x=2; 207602:>0:r3=1; 1:r3=1; 3:r1=0; x=2; 2 :>0:r3=1; 1:r3=0; 3:r1=1; x=2; 4 :>0:r3=0; 1:r3=1; 3:r1=1; x=2; 215 :>0:r3=1; 1:r3=1; 3:r1=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=0 /\ 3:r1=1) is NOT validated Hash=1e516922bc221761f817098fa259a99b Cycle=DpdW Wse SyncdWR Fre SyncdWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr033 No [PodRW,PosWR] Safe=Fre Wse SyncdWR DpdW BCSyncdWW Time podrwposwr033 1.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr034.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr034 "DpdW Wse SyncdWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 2:r8=x;} P0 | P1 | P2 ; li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | stw r3,0(r4) ; lwz r3,0(r4) | li r3,1 | lwz r5,0(r4) ; | stw r3,0(r4) | xor r6,r5,r5 ; | | li r7,1 ; | | stwx r7,r6,r8 ; exists (x=2 /\ 0:r3=0 /\ 2:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r27,1 _litmus_P1_4_: stw r27,0(r2) _litmus_P2_0_: lwz r22,0(r11) _litmus_P2_1_: li r24,1 _litmus_P2_2_: stw r24,0(r9) _litmus_P2_3_: lwz r23,0(r9) _litmus_P2_4_: xor r10,r23,r23 _litmus_P2_5_: li r8,1 _litmus_P2_6_: stwx r8,r10,r2 Test podrwposwr034 Allowed Histogram (7 states) 150049:>0:r3=0; 2:r1=0; x=1; 386981:>0:r3=1; 2:r1=0; x=1; 3015 :>0:r3=0; 2:r1=1; x=1; 135613:>0:r3=1; 2:r1=1; x=1; 14095 :>0:r3=0; 2:r1=0; x=2; 308271:>0:r3=1; 2:r1=0; x=2; 1976 :>0:r3=1; 2:r1=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=1) is NOT validated Hash=f390a1388968ca32887a6abe001693ab Cycle=DpdW Wse SyncdWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr034 No [PodRW,PosWR] Safe=Fre Wse SyncdWR DpdW BCSyncdWW Time podrwposwr034 1.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr035.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr035 "Fre SyncdWW Wse SyncdWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; li r3,1 | lwz r3,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (a=2 /\ x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr035 Allowed Histogram (19 states) 126638:>1:r3=0; 3:r1=0; 3:r5=1; a=1; x=1; 197439:>1:r3=1; 3:r1=0; 3:r5=1; a=1; x=1; 1636 :>1:r3=0; 3:r1=1; 3:r5=1; a=1; x=1; 163600:>1:r3=1; 3:r1=1; 3:r5=1; a=1; x=1; 77165 :>1:r3=0; 3:r1=0; 3:r5=1; a=2; x=1; 258007:>1:r3=1; 3:r1=0; 3:r5=1; a=2; x=1; 9 :>1:r3=0; 3:r1=1; 3:r5=1; a=2; x=1; 13208 :>1:r3=1; 3:r1=1; 3:r5=1; a=2; x=1; 101 :>1:r3=0; 3:r1=0; 3:r5=2; a=2; x=1; 124 :>1:r3=1; 3:r1=0; 3:r5=2; a=2; x=1; 47 :>1:r3=1; 3:r1=1; 3:r5=2; a=2; x=1; 1808 :>1:r3=0; 3:r1=0; 3:r5=1; a=1; x=2; 127320:>1:r3=1; 3:r1=0; 3:r5=1; a=1; x=2; 1 :>1:r3=0; 3:r1=1; 3:r5=1; a=1; x=2; 3134 :>1:r3=1; 3:r1=1; 3:r5=1; a=1; x=2; 62 :>1:r3=0; 3:r1=0; 3:r5=1; a=2; x=2; 29692 :>1:r3=1; 3:r1=0; 3:r5=1; a=2; x=2; 4 :>1:r3=1; 3:r1=1; 3:r5=1; a=2; x=2; 5 :>1:r3=1; 3:r1=0; 3:r5=2; a=2; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=d3175bd4c32a5d16340327a2c9f928d0 Cycle=Fre SyncdWW Wse SyncdWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr035 No [PodRW,PosWR] Safe=Fre Wse SyncdWW SyncdWR BCSyncdWW Time podrwposwr035 2.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr036.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr036 "DpdR Fre SyncdWW Wse SyncdWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; li r3,1 | lwz r3,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (y=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r28,1 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: li r24,1 _litmus_P3_2_: stw r24,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r23,r8,r2 Test podrwposwr036 Allowed Histogram (15 states) 44855 :>1:r3=0; 3:r1=0; 3:r7=0; y=1; 193128:>1:r3=1; 3:r1=0; 3:r7=0; y=1; 38 :>1:r3=0; 3:r1=1; 3:r7=0; y=1; 23349 :>1:r3=1; 3:r1=1; 3:r7=0; y=1; 241708:>1:r3=0; 3:r1=0; 3:r7=1; y=1; 137346:>1:r3=1; 3:r1=0; 3:r7=1; y=1; 14835 :>1:r3=0; 3:r1=1; 3:r7=1; y=1; 175688:>1:r3=1; 3:r1=1; 3:r7=1; y=1; 119 :>1:r3=0; 3:r1=0; 3:r7=0; y=2; 45986 :>1:r3=1; 3:r1=0; 3:r7=0; y=2; 37 :>1:r3=1; 3:r1=1; 3:r7=0; y=2; 12169 :>1:r3=0; 3:r1=0; 3:r7=1; y=2; 71786 :>1:r3=1; 3:r1=0; 3:r7=1; y=2; 65 :>1:r3=0; 3:r1=1; 3:r7=1; y=2; 38891 :>1:r3=1; 3:r1=1; 3:r7=1; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=7d879b228a4e5b3418fb2d1c879f2f73 Cycle=DpdR Fre SyncdWW Wse SyncdWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr036 No [PodRW,PosWR] Safe=Fre Wse SyncdWW SyncdWR DpdR BCSyncdWW Time podrwposwr036 2.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr037.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr037 "DpdW Wse SyncdWW Wse SyncdWR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; li r3,1 | lwz r3,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ y=2 /\ 1:r3=0 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r27,0(r2) _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr037 Allowed Histogram (13 states) 252321:>1:r3=0; 3:r1=0; x=1; y=1; 260154:>1:r3=1; 3:r1=0; x=1; y=1; 3025 :>1:r3=0; 3:r1=1; x=1; y=1; 190597:>1:r3=1; 3:r1=1; x=1; y=1; 11379 :>1:r3=0; 3:r1=0; x=2; y=1; 187161:>1:r3=1; 3:r1=0; x=2; y=1; 1 :>1:r3=0; 3:r1=1; x=2; y=1; 464 :>1:r3=1; 3:r1=1; x=2; y=1; 8330 :>1:r3=0; 3:r1=0; x=1; y=2; 64178 :>1:r3=1; 3:r1=0; x=1; y=2; 18 :>1:r3=0; 3:r1=1; x=1; y=2; 14570 :>1:r3=1; 3:r1=1; x=1; y=2; 7802 :>1:r3=1; 3:r1=0; x=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 1:r3=0 /\ 3:r1=1) is NOT validated Hash=5875a50f182a4121735cbf70792ab709 Cycle=DpdW Wse SyncdWW Wse SyncdWR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr037 No [PodRW,PosWR] Safe=Fre Wse SyncdWW SyncdWR DpdW BCSyncdWW Time podrwposwr037 2.24 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr038.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr038 "Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | li r3,1 ; sync | lwz r3,0(r4) | sync | stw r3,0(r4) ; li r3,1 | | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (a=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: lwz r28,0(r2) _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr038 Allowed Histogram (17 states) 192594:>1:r1=0; 1:r3=0; 3:r1=0; 3:r5=1; a=1; 2170 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r5=1; a=1; 143423:>1:r1=0; 1:r3=1; 3:r1=0; 3:r5=1; a=1; 147324:>1:r1=1; 1:r3=1; 3:r1=0; 3:r5=1; a=1; 9319 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r5=1; a=1; 1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r5=1; a=1; 121490:>1:r1=0; 1:r3=1; 3:r1=1; 3:r5=1; a=1; 31138 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r5=1; a=1; 47187 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r5=1; a=2; 105 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r5=1; a=2; 280417:>1:r1=0; 1:r3=1; 3:r1=0; 3:r5=1; a=2; 11742 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r5=1; a=2; 13 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r5=1; a=2; 13067 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r5=1; a=2; 7 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r5=1; a=2; 1 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r5=2; a=2; 2 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r5=2; a=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=d41f3bfcc0ff1586faee36e78c85749d Cycle=Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr038 No [PodRW,PosWR] Safe=Fre SyncdRR BCSyncdWW Time podrwposwr038 1.77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr039.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr039 "DpdR Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | li r3,1 ; sync | lwz r3,0(r4) | sync | stw r3,0(r4) ; li r3,1 | | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r30,1 _litmus_P0_1_: stw r30,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: lwz r30,0(r2) _litmus_P2_0_: li r4,1 _litmus_P2_1_: stw r4,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r24,r8,r2 Test podrwposwr039 Allowed Histogram (15 states) 110012:>1:r1=0; 1:r3=0; 3:r1=0; 3:r7=0; 5 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r7=0; 228122:>1:r1=0; 1:r3=1; 3:r1=0; 3:r7=0; 1459 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r7=0; 72 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r7=0; 9568 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r7=0; 9 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r7=0; 162488:>1:r1=0; 1:r3=0; 3:r1=0; 3:r7=1; 3623 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r7=1; 164657:>1:r1=0; 1:r3=1; 3:r1=0; 3:r7=1; 115260:>1:r1=1; 1:r3=1; 3:r1=0; 3:r7=1; 6814 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r7=1; 35 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r7=1; 188296:>1:r1=0; 1:r3=1; 3:r1=1; 3:r7=1; 9580 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r7=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=ee9c5a30747c9de5a196b4f19e95ee4f Cycle=DpdR Fre SyncdWW Rfe SyncdRR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr039 No [PodRW,PosWR] Safe=Fre SyncdRR DpdR BCSyncdWW Time podrwposwr039 1.71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr040.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr040 "DpdW Wse SyncdWW Rfe SyncdRR Fre SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | li r3,1 ; sync | lwz r3,0(r4) | sync | stw r3,0(r4) ; li r3,1 | | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: lwz r28,0(r2) _litmus_P2_0_: li r28,1 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr040 Allowed Histogram (15 states) 271314:>1:r1=0; 1:r3=0; 3:r1=0; x=1; 6753 :>1:r1=1; 1:r3=0; 3:r1=0; x=1; 170652:>1:r1=0; 1:r3=1; 3:r1=0; x=1; 98460 :>1:r1=1; 1:r3=1; 3:r1=0; x=1; 7052 :>1:r1=0; 1:r3=0; 3:r1=1; x=1; 22 :>1:r1=1; 1:r3=0; 3:r1=1; x=1; 168869:>1:r1=0; 1:r3=1; 3:r1=1; x=1; 5896 :>1:r1=1; 1:r3=1; 3:r1=1; x=1; 70642 :>1:r1=0; 1:r3=0; 3:r1=0; x=2; 3 :>1:r1=1; 1:r3=0; 3:r1=0; x=2; 194372:>1:r1=0; 1:r3=1; 3:r1=0; x=2; 4312 :>1:r1=1; 1:r3=1; 3:r1=0; x=2; 3 :>1:r1=0; 1:r3=0; 3:r1=1; x=2; 1649 :>1:r1=0; 1:r3=1; 3:r1=1; x=2; 1 :>1:r1=1; 1:r3=1; 3:r1=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=1) is NOT validated Hash=cc510750b806cf6c66951089a70118e7 Cycle=DpdW Wse SyncdWW Rfe SyncdRR Fre SyncdWW Rfe PodRW PosWR Relax podrwposwr040 No [PodRW,PosWR] Safe=Fre Wse SyncdRR DpdW BCSyncdWW Time podrwposwr040 1.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr041.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr041 "DpdW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 1:r8=x;} P0 | P1 ; li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 ; sync | stw r3,0(r4) ; li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | xor r6,r5,r5 ; | li r7,1 ; | stwx r7,r6,r8 ; exists (x=2 /\ 1:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r23,0(r11) _litmus_P1_1_: li r25,1 _litmus_P1_2_: stw r25,0(r9) _litmus_P1_3_: lwz r24,0(r9) _litmus_P1_4_: xor r10,r24,r24 _litmus_P1_5_: li r8,1 _litmus_P1_6_: stwx r8,r10,r2 Test podrwposwr041 Allowed Histogram (3 states) 1096483:>1:r1=0; x=1; 124581:>1:r1=1; x=1; 778936:>1:r1=0; x=2; No Witnesses Positive: 0, Negative: 2000000 Condition exists (x=2 /\ 1:r1=1) is NOT validated Hash=6e8e900c2b83d8c31eed9011e4b437df Cycle=DpdW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr041 No [PodRW,PosWR] Safe=Wse DpdW BCSyncdWW Time podrwposwr041 1.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr042.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr042 "DpdW Wse SyncdWW Rfe PodRW PosWR DpdW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 1:r8=a; 2:r2=a; 2:r4=b; 3:r2=b; 3:r4=c; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | li r3,1 | stw r1,0(r2) | li r3,1 ; sync | stw r3,0(r4) | sync | stw r3,0(r4) ; li r3,1 | lwz r5,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | xor r6,r5,r5 | stw r3,0(r4) | xor r6,r5,r5 ; | li r7,1 | | li r7,1 ; | stwx r7,r6,r8 | | stwx r7,r6,r8 ; exists (a=2 /\ x=2 /\ 1:r1=1 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r23,0(r11) _litmus_P1_1_: li r25,1 _litmus_P1_2_: stw r25,0(r9) _litmus_P1_3_: lwz r24,0(r9) _litmus_P1_4_: xor r10,r24,r24 _litmus_P1_5_: li r8,1 _litmus_P1_6_: stwx r8,r10,r2 _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr042 Allowed Histogram (15 states) 178873:>1:r1=0; 3:r1=0; a=1; x=1; 176573:>1:r1=1; 3:r1=0; a=1; x=1; 110736:>1:r1=0; 3:r1=1; a=1; x=1; 9931 :>1:r1=1; 3:r1=1; a=1; x=1; 187955:>1:r1=0; 3:r1=0; a=2; x=1; 9238 :>1:r1=1; 3:r1=0; a=2; x=1; 16390 :>1:r1=0; 3:r1=1; a=2; x=1; 5 :>1:r1=1; 3:r1=1; a=2; x=1; 203542:>1:r1=0; 3:r1=0; a=1; x=2; 13714 :>1:r1=1; 3:r1=0; a=1; x=2; 7339 :>1:r1=0; 3:r1=1; a=1; x=2; 1 :>1:r1=1; 3:r1=1; a=1; x=2; 85593 :>1:r1=0; 3:r1=0; a=2; x=2; 62 :>1:r1=1; 3:r1=0; a=2; x=2; 48 :>1:r1=0; 3:r1=1; a=2; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ x=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated Hash=733c7ee4a395b6a594b929037974531e Cycle=DpdW Wse SyncdWW Rfe PodRW PosWR DpdW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr042 No [PodRW,PosWR] Safe=Wse DpdW BCSyncdWW Time podrwposwr042 2.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr043.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr043 "Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | li r3,1 ; sync | li r4,1 | sync | stw r3,0(r4) ; li r3,1 | stwx r4,r3,r5 | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (a=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: xor r28,r27,r27 _litmus_P1_2_: li r11,1 _litmus_P1_3_: stwx r11,r28,r2 _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr043 Allowed Histogram (19 states) 86909 :>1:r1=0; 3:r1=0; 3:r5=1; a=1; y=1; 163967:>1:r1=1; 3:r1=0; 3:r5=1; a=1; y=1; 156394:>1:r1=0; 3:r1=1; 3:r5=1; a=1; y=1; 44814 :>1:r1=1; 3:r1=1; 3:r5=1; a=1; y=1; 244021:>1:r1=0; 3:r1=0; 3:r5=1; a=2; y=1; 4578 :>1:r1=1; 3:r1=0; 3:r5=1; a=2; y=1; 15243 :>1:r1=0; 3:r1=1; 3:r5=1; a=2; y=1; 12 :>1:r1=1; 3:r1=1; 3:r5=1; a=2; y=1; 115 :>1:r1=0; 3:r1=0; 3:r5=2; a=2; y=1; 1 :>1:r1=1; 3:r1=0; 3:r5=2; a=2; y=1; 17 :>1:r1=0; 3:r1=1; 3:r5=2; a=2; y=1; 148407:>1:r1=0; 3:r1=0; 3:r5=1; a=1; y=2; 408 :>1:r1=1; 3:r1=0; 3:r5=1; a=1; y=2; 1234 :>1:r1=0; 3:r1=1; 3:r5=1; a=1; y=2; 1 :>1:r1=1; 3:r1=1; 3:r5=1; a=1; y=2; 133690:>1:r1=0; 3:r1=0; 3:r5=1; a=2; y=2; 6 :>1:r1=1; 3:r1=0; 3:r5=1; a=2; y=2; 9 :>1:r1=0; 3:r1=1; 3:r5=1; a=2; y=2; 174 :>1:r1=0; 3:r1=0; 3:r5=2; a=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=05a688e240c347b642552edc53d9026a Cycle=Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr043 No [PodRW,PosWR] Safe=Fre Wse DpdW BCSyncdWW Time podrwposwr043 1.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr044.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr044 "DpdR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=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) | li r3,1 ; sync | li r4,1 | sync | stw r3,0(r4) ; li r3,1 | stwx r4,r3,r5 | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r28,1 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: xor r28,r27,r27 _litmus_P1_2_: li r11,1 _litmus_P1_3_: stwx r11,r28,r2 _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: li r24,1 _litmus_P3_2_: stw r24,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r23,r8,r2 Test podrwposwr044 Allowed Histogram (15 states) 196564:>1:r1=0; 3:r1=0; 3:r7=0; z=1; 1648 :>1:r1=1; 3:r1=0; 3:r7=0; z=1; 13347 :>1:r1=0; 3:r1=1; 3:r7=0; z=1; 13 :>1:r1=1; 3:r1=1; 3:r7=0; z=1; 72746 :>1:r1=0; 3:r1=0; 3:r7=1; z=1; 111052:>1:r1=1; 3:r1=0; 3:r7=1; z=1; 203425:>1:r1=0; 3:r1=1; 3:r7=1; z=1; 24491 :>1:r1=1; 3:r1=1; 3:r7=1; z=1; 108846:>1:r1=0; 3:r1=0; 3:r7=0; z=2; 18 :>1:r1=1; 3:r1=0; 3:r7=0; z=2; 393 :>1:r1=0; 3:r1=1; 3:r7=0; z=2; 247427:>1:r1=0; 3:r1=0; 3:r7=1; z=2; 9825 :>1:r1=1; 3:r1=0; 3:r7=1; z=2; 10162 :>1:r1=0; 3:r1=1; 3:r7=1; z=2; 43 :>1:r1=1; 3:r1=1; 3:r7=1; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=17fe6d05dfd2d888bcfbc02c4a1e157a Cycle=DpdR Fre SyncdWW Rfe DpdW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr044 No [PodRW,PosWR] Safe=Fre Wse DpdW DpdR BCSyncdWW Time podrwposwr044 1.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr045.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr045 "DpdW Wse SyncdWW Rfe DpdW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=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) | li r3,1 ; sync | li r4,1 | sync | stw r3,0(r4) ; li r3,1 | stwx r4,r3,r5 | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: xor r28,r27,r27 _litmus_P1_2_: li r11,1 _litmus_P1_3_: stwx r11,r28,r2 _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr045 Allowed Histogram (13 states) 174062:>1:r1=0; 3:r1=0; x=1; z=1; 110550:>1:r1=1; 3:r1=0; x=1; z=1; 143883:>1:r1=0; 3:r1=1; x=1; z=1; 5307 :>1:r1=1; 3:r1=1; x=1; z=1; 186471:>1:r1=0; 3:r1=0; x=2; z=1; 4113 :>1:r1=1; 3:r1=0; x=2; z=1; 354 :>1:r1=0; 3:r1=1; x=2; z=1; 227717:>1:r1=0; 3:r1=0; x=1; z=2; 1222 :>1:r1=1; 3:r1=0; x=1; z=2; 1417 :>1:r1=0; 3:r1=1; x=1; z=2; 144902:>1:r1=0; 3:r1=0; x=2; z=2; 1 :>1:r1=1; 3:r1=0; x=2; z=2; 1 :>1:r1=0; 3:r1=1; x=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated Hash=03e540a72a340ceb830fd01cde95c0eb Cycle=DpdW Wse SyncdWW Rfe DpdW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr045 No [PodRW,PosWR] Safe=Wse DpdW BCSyncdWW Time podrwposwr045 2.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr046.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr046 "Fre SyncdWW Wse SyncdWW Rfe PodRW PosWR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | stw r3,0(r4) ; li r3,1 | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ z=2 /\ 2:r1=1 /\ 2:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r27,1 _litmus_P0_4_: stw r27,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r27,1 _litmus_P1_4_: stw r27,0(r2) _litmus_P2_0_: lwz r25,0(r9) _litmus_P2_1_: li r11,1 _litmus_P2_2_: stw r11,0(r2) _litmus_P2_3_: lwz r26,0(r2) Test podrwposwr046 Allowed Histogram (9 states) 260902:>2:r1=0; 2:r5=1; x=1; z=1; 110572:>2:r1=1; 2:r5=1; x=1; z=1; 254627:>2:r1=0; 2:r5=1; x=2; z=1; 109 :>2:r1=1; 2:r5=1; x=2; z=1; 369310:>2:r1=0; 2:r5=1; x=1; z=2; 2043 :>2:r1=1; 2:r5=1; x=1; z=2; 39 :>2:r1=0; 2:r5=2; x=1; z=2; 2 :>2:r1=1; 2:r5=2; x=1; z=2; 2396 :>2:r1=0; 2:r5=1; x=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ z=2 /\ 2:r1=1 /\ 2:r5=1) is NOT validated Hash=7df5dcfb9023484a5716af7b1b47dd3d Cycle=Fre SyncdWW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr046 No [PodRW,PosWR] Safe=Fre Wse SyncdWW BCSyncdWW Time podrwposwr046 1.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr047.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr047 "DpdR Fre SyncdWW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 2:r8=x;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | stw r3,0(r4) ; li r3,1 | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | xor r6,r5,r5 ; | | lwzx r7,r6,r8 ; exists (y=2 /\ 2:r1=1 /\ 2:r7=0) Generated assembler _litmus_P0_0_: li r28,1 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r27,1 _litmus_P0_4_: stw r27,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r27,1 _litmus_P1_4_: stw r27,0(r2) _litmus_P2_0_: lwz r21,0(r11) _litmus_P2_1_: li r23,1 _litmus_P2_2_: stw r23,0(r9) _litmus_P2_3_: lwz r10,0(r9) _litmus_P2_4_: xor r8,r10,r10 _litmus_P2_5_: lwzx r22,r8,r2 Test podrwposwr047 Allowed Histogram (7 states) 372654:>2:r1=0; 2:r7=0; y=1; 10588 :>2:r1=1; 2:r7=0; y=1; 321952:>2:r1=0; 2:r7=1; y=1; 131709:>2:r1=1; 2:r7=1; y=1; 9521 :>2:r1=0; 2:r7=0; y=2; 152390:>2:r1=0; 2:r7=1; y=2; 1186 :>2:r1=1; 2:r7=1; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 2:r1=1 /\ 2:r7=0) is NOT validated Hash=55a2fb4c4757f04bbb1cccf767c94665 Cycle=DpdR Fre SyncdWW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr047 No [PodRW,PosWR] Safe=Fre Wse SyncdWW DpdR BCSyncdWW Time podrwposwr047 1.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr048.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr048 "Fre SyncdWR Fre SyncdWW Wse SyncdWW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; lwz r3,0(r4) | li r3,1 | li r3,1 | lwz r5,0(r4) ; | stw r3,0(r4) | stw r3,0(r4) | ; exists (a=2 /\ y=2 /\ 0:r3=0 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr048 Allowed Histogram (18 states) 199816:>0:r3=0; 3:r1=0; 3:r5=1; a=1; y=1; 118786:>0:r3=1; 3:r1=0; 3:r5=1; a=1; y=1; 6421 :>0:r3=0; 3:r1=1; 3:r5=1; a=1; y=1; 139589:>0:r3=1; 3:r1=1; 3:r5=1; a=1; y=1; 79569 :>0:r3=0; 3:r1=0; 3:r5=1; a=2; y=1; 246788:>0:r3=1; 3:r1=0; 3:r5=1; a=2; y=1; 7 :>0:r3=0; 3:r1=1; 3:r5=1; a=2; y=1; 3953 :>0:r3=1; 3:r1=1; 3:r5=1; a=2; y=1; 6 :>0:r3=0; 3:r1=0; 3:r5=2; a=2; y=1; 172 :>0:r3=1; 3:r1=0; 3:r5=2; a=2; y=1; 15 :>0:r3=1; 3:r1=1; 3:r5=2; a=2; y=1; 4223 :>0:r3=0; 3:r1=0; 3:r5=1; a=1; y=2; 119343:>0:r3=1; 3:r1=0; 3:r5=1; a=1; y=2; 2 :>0:r3=0; 3:r1=1; 3:r5=1; a=1; y=2; 197 :>0:r3=1; 3:r1=1; 3:r5=1; a=1; y=2; 189 :>0:r3=0; 3:r1=0; 3:r5=1; a=2; y=2; 80796 :>0:r3=1; 3:r1=0; 3:r5=1; a=2; y=2; 128 :>0:r3=1; 3:r1=0; 3:r5=2; a=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ y=2 /\ 0:r3=0 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=e04b88b43b1050e15e89030e4c1f5b5b Cycle=Fre SyncdWR Fre SyncdWW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr048 No [PodRW,PosWR] Safe=Fre Wse SyncdWW SyncdWR BCSyncdWW Time podrwposwr048 2.01 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr049.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr049 "DpdR Fre SyncdWR Fre SyncdWW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; lwz r3,0(r4) | li r3,1 | li r3,1 | lwz r5,0(r4) ; | stw r3,0(r4) | stw r3,0(r4) | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (z=2 /\ 0:r3=0 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r28,1 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: li r24,1 _litmus_P3_2_: stw r24,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r23,r8,r2 Test podrwposwr049 Allowed Histogram (15 states) 13350 :>0:r3=0; 3:r1=0; 3:r7=0; z=1; 262954:>0:r3=1; 3:r1=0; 3:r7=0; z=1; 174 :>0:r3=0; 3:r1=1; 3:r7=0; z=1; 51917 :>0:r3=1; 3:r1=1; 3:r7=0; z=1; 138349:>0:r3=0; 3:r1=0; 3:r7=1; z=1; 109892:>0:r3=1; 3:r1=0; 3:r7=1; z=1; 27546 :>0:r3=0; 3:r1=1; 3:r7=1; z=1; 167653:>0:r3=1; 3:r1=1; 3:r7=1; z=1; 22 :>0:r3=0; 3:r1=0; 3:r7=0; z=2; 131705:>0:r3=1; 3:r1=0; 3:r7=0; z=2; 133 :>0:r3=1; 3:r1=1; 3:r7=0; z=2; 12480 :>0:r3=0; 3:r1=0; 3:r7=1; z=2; 79296 :>0:r3=1; 3:r1=0; 3:r7=1; z=2; 28 :>0:r3=0; 3:r1=1; 3:r7=1; z=2; 4501 :>0:r3=1; 3:r1=1; 3:r7=1; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 0:r3=0 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=55bf8f810c5ea1212374e1b2e8161b8e Cycle=DpdR Fre SyncdWR Fre SyncdWW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr049 No [PodRW,PosWR] Safe=Fre Wse SyncdWW SyncdWR DpdR BCSyncdWW Time podrwposwr049 1.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr050.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr050 "DpdW Wse SyncdWR Fre SyncdWW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; lwz r3,0(r4) | li r3,1 | li r3,1 | lwz r5,0(r4) ; | stw r3,0(r4) | stw r3,0(r4) | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ z=2 /\ 0:r3=0 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr050 Allowed Histogram (14 states) 79902 :>0:r3=0; 3:r1=0; x=1; z=1; 288121:>0:r3=1; 3:r1=0; x=1; z=1; 37220 :>0:r3=0; 3:r1=1; x=1; z=1; 181344:>0:r3=1; 3:r1=1; x=1; z=1; 15321 :>0:r3=0; 3:r1=0; x=2; z=1; 200207:>0:r3=1; 3:r1=0; x=2; z=1; 1 :>0:r3=0; 3:r1=1; x=2; z=1; 625 :>0:r3=1; 3:r1=1; x=2; z=1; 10049 :>0:r3=0; 3:r1=0; x=1; z=2; 169988:>0:r3=1; 3:r1=0; x=1; z=2; 11 :>0:r3=0; 3:r1=1; x=1; z=2; 739 :>0:r3=1; 3:r1=1; x=1; z=2; 4 :>0:r3=0; 3:r1=0; x=2; z=2; 16468 :>0:r3=1; 3:r1=0; x=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ z=2 /\ 0:r3=0 /\ 3:r1=1) is NOT validated Hash=ea3b1eab4e35fba01b3bd92328dba56a Cycle=DpdW Wse SyncdWR Fre SyncdWW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr050 No [PodRW,PosWR] Safe=Fre Wse SyncdWW SyncdWR DpdW BCSyncdWW Time podrwposwr050 2.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr051.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr051 "DpdW Wse SyncdWW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 2:r8=x;} P0 | P1 | P2 ; li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | stw r3,0(r4) ; li r3,1 | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | xor r6,r5,r5 ; | | li r7,1 ; | | stwx r7,r6,r8 ; exists (x=2 /\ y=2 /\ 2:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r27,1 _litmus_P0_4_: stw r27,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r27,1 _litmus_P1_4_: stw r27,0(r2) _litmus_P2_0_: lwz r22,0(r11) _litmus_P2_1_: li r24,1 _litmus_P2_2_: stw r24,0(r9) _litmus_P2_3_: lwz r23,0(r9) _litmus_P2_4_: xor r10,r23,r23 _litmus_P2_5_: li r8,1 _litmus_P2_6_: stwx r8,r10,r2 Test podrwposwr051 Allowed Histogram (7 states) 344994:>2:r1=0; x=1; y=1; 125470:>2:r1=1; x=1; y=1; 300087:>2:r1=0; x=2; y=1; 1518 :>2:r1=1; x=2; y=1; 217682:>2:r1=0; x=1; y=2; 729 :>2:r1=1; x=1; y=2; 9520 :>2:r1=0; x=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 2:r1=1) is NOT validated Hash=9aec2c2919069d75c74033d4b32c5db8 Cycle=DpdW Wse SyncdWW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr051 No [PodRW,PosWR] Safe=Wse SyncdWW DpdW BCSyncdWW Time podrwposwr051 1.71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr052.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr052 "Fre SyncdWW Wse SyncdWW Wse SyncdWW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; li r3,1 | li r3,1 | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) | ; exists (a=2 /\ x=2 /\ y=2 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr052 Allowed Histogram (17 states) 148150:>3:r1=0; 3:r5=1; a=1; x=1; y=1; 160245:>3:r1=1; 3:r5=1; a=1; x=1; y=1; 218470:>3:r1=0; 3:r5=1; a=2; x=1; y=1; 12009 :>3:r1=1; 3:r5=1; a=2; x=1; y=1; 7 :>3:r1=0; 3:r5=2; a=2; x=1; y=1; 140793:>3:r1=0; 3:r5=1; a=1; x=2; y=1; 49898 :>3:r1=1; 3:r5=1; a=1; x=2; y=1; 31543 :>3:r1=0; 3:r5=1; a=2; x=2; y=1; 15 :>3:r1=1; 3:r5=1; a=2; x=2; y=1; 191023:>3:r1=0; 3:r5=1; a=1; x=1; y=2; 2399 :>3:r1=1; 3:r5=1; a=1; x=1; y=2; 41024 :>3:r1=0; 3:r5=1; a=2; x=1; y=2; 2 :>3:r1=1; 3:r5=1; a=2; x=1; y=2; 4 :>3:r1=0; 3:r5=2; a=2; x=1; y=2; 4379 :>3:r1=0; 3:r5=1; a=1; x=2; y=2; 1 :>3:r1=1; 3:r5=1; a=1; x=2; y=2; 38 :>3:r1=0; 3:r5=1; a=2; x=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ x=2 /\ y=2 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=bfea1f518cadd97de98badd7e7b63d57 Cycle=Fre SyncdWW Wse SyncdWW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr052 No [PodRW,PosWR] Safe=Fre Wse SyncdWW BCSyncdWW Time podrwposwr052 2.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr053.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr053 "DpdR Fre SyncdWW Wse SyncdWW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; li r3,1 | li r3,1 | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (y=2 /\ z=2 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r28,1 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: li r24,1 _litmus_P3_2_: stw r24,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r23,r8,r2 Test podrwposwr053 Allowed Histogram (15 states) 274920:>3:r1=0; 3:r7=0; y=1; z=1; 35330 :>3:r1=1; 3:r7=0; y=1; z=1; 188376:>3:r1=0; 3:r7=1; y=1; z=1; 173911:>3:r1=1; 3:r7=1; y=1; z=1; 4326 :>3:r1=0; 3:r7=0; y=2; z=1; 26 :>3:r1=1; 3:r7=0; y=2; z=1; 118379:>3:r1=0; 3:r7=1; y=2; z=1; 28262 :>3:r1=1; 3:r7=1; y=2; z=1; 97888 :>3:r1=0; 3:r7=0; y=1; z=2; 6 :>3:r1=1; 3:r7=0; y=1; z=2; 76111 :>3:r1=0; 3:r7=1; y=1; z=2; 1564 :>3:r1=1; 3:r7=1; y=1; z=2; 3 :>3:r1=0; 3:r7=0; y=2; z=2; 895 :>3:r1=0; 3:r7=1; y=2; z=2; 3 :>3:r1=1; 3:r7=1; y=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ z=2 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=c38b543ccf5b0305f6c2367676153dfc Cycle=DpdR Fre SyncdWW Wse SyncdWW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr053 No [PodRW,PosWR] Safe=Fre Wse SyncdWW DpdR BCSyncdWW Time podrwposwr053 2.18 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr054.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr054 "DpdW Wse SyncdWW Wse SyncdWW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | li r3,1 ; sync | sync | sync | stw r3,0(r4) ; li r3,1 | li r3,1 | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ y=2 /\ z=2 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr054 Allowed Histogram (13 states) 234252:>3:r1=0; x=1; y=1; z=1; 186602:>3:r1=1; x=1; y=1; z=1; 248430:>3:r1=0; x=2; y=1; z=1; 2540 :>3:r1=1; x=2; y=1; z=1; 126818:>3:r1=0; x=1; y=2; z=1; 14000 :>3:r1=1; x=1; y=2; z=1; 1755 :>3:r1=0; x=2; y=2; z=1; 2 :>3:r1=1; x=2; y=2; z=1; 124110:>3:r1=0; x=1; y=1; z=2; 2591 :>3:r1=1; x=1; y=1; z=2; 57345 :>3:r1=0; x=2; y=1; z=2; 1554 :>3:r1=0; x=1; y=2; z=2; 1 :>3:r1=1; x=1; y=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ z=2 /\ 3:r1=1) is NOT validated Hash=8b76158b9d72d52afaeda3c52efb51cc Cycle=DpdW Wse SyncdWW Wse SyncdWW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr054 No [PodRW,PosWR] Safe=Wse SyncdWW DpdW BCSyncdWW Time podrwposwr054 2.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr055.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr055 "Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | li r3,1 ; sync | li r3,1 | sync | stw r3,0(r4) ; li r3,1 | stw r3,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (a=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r28,1 _litmus_P1_3_: stw r28,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr055 Allowed Histogram (19 states) 127467:>1:r1=0; 3:r1=0; 3:r5=1; a=1; y=1; 140187:>1:r1=1; 3:r1=0; 3:r5=1; a=1; y=1; 139281:>1:r1=0; 3:r1=1; 3:r5=1; a=1; y=1; 7035 :>1:r1=1; 3:r1=1; 3:r5=1; a=1; y=1; 293966:>1:r1=0; 3:r1=0; 3:r5=1; a=2; y=1; 16525 :>1:r1=1; 3:r1=0; 3:r5=1; a=2; y=1; 14168 :>1:r1=0; 3:r1=1; 3:r5=1; a=2; y=1; 24 :>1:r1=1; 3:r1=1; 3:r5=1; a=2; y=1; 217 :>1:r1=0; 3:r1=0; 3:r5=2; a=2; y=1; 3 :>1:r1=1; 3:r1=0; 3:r5=2; a=2; y=1; 14 :>1:r1=0; 3:r1=1; 3:r5=2; a=2; y=1; 87468 :>1:r1=0; 3:r1=0; 3:r5=1; a=1; y=2; 1496 :>1:r1=1; 3:r1=0; 3:r5=1; a=1; y=2; 458 :>1:r1=0; 3:r1=1; 3:r5=1; a=1; y=2; 1 :>1:r1=1; 3:r1=1; 3:r5=1; a=1; y=2; 171390:>1:r1=0; 3:r1=0; 3:r5=1; a=2; y=2; 18 :>1:r1=1; 3:r1=0; 3:r5=1; a=2; y=2; 5 :>1:r1=0; 3:r1=1; 3:r5=1; a=2; y=2; 277 :>1:r1=0; 3:r1=0; 3:r5=2; a=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ y=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=0cd4b2e6bf0b9a0aa2e4bbd0534e33b0 Cycle=Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr055 No [PodRW,PosWR] Safe=Fre Wse SyncdRW BCSyncdWW Time podrwposwr055 2.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr056.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr056 "DpdR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | li r3,1 ; sync | li r3,1 | sync | stw r3,0(r4) ; li r3,1 | stw r3,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r28,1 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r28,1 _litmus_P1_3_: stw r28,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: li r24,1 _litmus_P3_2_: stw r24,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r23,r8,r2 Test podrwposwr056 Allowed Histogram (15 states) 251007:>1:r1=0; 3:r1=0; 3:r7=0; z=1; 9920 :>1:r1=1; 3:r1=0; 3:r7=0; z=1; 5253 :>1:r1=0; 3:r1=1; 3:r7=0; z=1; 17 :>1:r1=1; 3:r1=1; 3:r7=0; z=1; 140585:>1:r1=0; 3:r1=0; 3:r7=1; z=1; 134746:>1:r1=1; 3:r1=0; 3:r7=1; z=1; 189524:>1:r1=0; 3:r1=1; 3:r7=1; z=1; 30175 :>1:r1=1; 3:r1=1; 3:r7=1; z=1; 52928 :>1:r1=0; 3:r1=0; 3:r7=0; z=2; 9 :>1:r1=1; 3:r1=0; 3:r7=0; z=2; 108 :>1:r1=0; 3:r1=1; 3:r7=0; z=2; 179465:>1:r1=0; 3:r1=0; 3:r7=1; z=2; 4257 :>1:r1=1; 3:r1=0; 3:r7=1; z=2; 2000 :>1:r1=0; 3:r1=1; 3:r7=1; z=2; 6 :>1:r1=1; 3:r1=1; 3:r7=1; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=7be01dd6ac9e30579fb0a00b67fd8ddc Cycle=DpdR Fre SyncdWW Rfe SyncdRW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr056 No [PodRW,PosWR] Safe=Fre Wse SyncdRW DpdR BCSyncdWW Time podrwposwr056 1.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr057.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr057 "DpdW Wse SyncdWW Rfe SyncdRW Wse SyncdWW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | li r3,1 ; sync | li r3,1 | sync | stw r3,0(r4) ; li r3,1 | stw r3,0(r4) | li r3,1 | lwz r5,0(r4) ; stw r3,0(r4) | | stw r3,0(r4) | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r28,1 _litmus_P1_3_: stw r28,0(r2) _litmus_P2_0_: li r28,2 _litmus_P2_1_: stw r28,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r3,1 _litmus_P2_4_: stw r3,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr057 Allowed Histogram (13 states) 248337:>1:r1=0; 3:r1=0; x=1; z=1; 114407:>1:r1=1; 3:r1=0; x=1; z=1; 176198:>1:r1=0; 3:r1=1; x=1; z=1; 15915 :>1:r1=1; 3:r1=1; x=1; z=1; 213445:>1:r1=0; 3:r1=0; x=2; z=1; 5828 :>1:r1=1; 3:r1=0; x=2; z=1; 132 :>1:r1=0; 3:r1=1; x=2; z=1; 184770:>1:r1=0; 3:r1=0; x=1; z=2; 530 :>1:r1=1; 3:r1=0; x=1; z=2; 504 :>1:r1=0; 3:r1=1; x=1; z=2; 39931 :>1:r1=0; 3:r1=0; x=2; z=2; 2 :>1:r1=1; 3:r1=0; x=2; z=2; 1 :>1:r1=0; 3:r1=1; x=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ z=2 /\ 1:r1=1 /\ 3:r1=1) is NOT validated Hash=fcc1ee22a472fe244cf93ef66666ec98 Cycle=DpdW Wse SyncdWW Rfe SyncdRW Wse SyncdWW Rfe PodRW PosWR Relax podrwposwr057 No [PodRW,PosWR] Safe=Wse SyncdRW DpdW BCSyncdWW Time podrwposwr057 2.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr058.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr058 "Fre SyncdWW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | li r3,1 ; sync | li r3,1 | stw r3,0(r4) ; li r3,1 | stw r3,0(r4) | lwz r5,0(r4) ; stw r3,0(r4) | | ; exists (z=2 /\ 1:r1=1 /\ 2:r1=1 /\ 2:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r27,1 _litmus_P0_4_: stw r27,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r28,1 _litmus_P1_3_: stw r28,0(r2) _litmus_P2_0_: lwz r25,0(r9) _litmus_P2_1_: li r11,1 _litmus_P2_2_: stw r11,0(r2) _litmus_P2_3_: lwz r26,0(r2) Test podrwposwr058 Allowed Histogram (9 states) 178015:>1:r1=0; 2:r1=0; 2:r5=1; z=1; 236920:>1:r1=1; 2:r1=0; 2:r5=1; z=1; 232362:>1:r1=0; 2:r1=1; 2:r5=1; z=1; 151 :>1:r1=1; 2:r1=1; 2:r5=1; z=1; 344916:>1:r1=0; 2:r1=0; 2:r5=1; z=2; 1149 :>1:r1=1; 2:r1=0; 2:r5=1; z=2; 6458 :>1:r1=0; 2:r1=1; 2:r5=1; z=2; 27 :>1:r1=0; 2:r1=0; 2:r5=2; z=2; 2 :>1:r1=0; 2:r1=1; 2:r5=2; z=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (z=2 /\ 1:r1=1 /\ 2:r1=1 /\ 2:r5=1) is NOT validated Hash=68656b16d803b6bb2fb47fc0780d1c25 Cycle=Fre SyncdWW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr058 No [PodRW,PosWR] Safe=Fre BCSyncdWW BCSyncdRW Time podrwposwr058 1.32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr059.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr059 "DpdR Fre SyncdWW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 2:r8=x;} P0 | P1 | P2 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | li r3,1 ; sync | li r3,1 | stw r3,0(r4) ; li r3,1 | stw r3,0(r4) | lwz r5,0(r4) ; stw r3,0(r4) | | xor r6,r5,r5 ; | | lwzx r7,r6,r8 ; exists (1:r1=1 /\ 2:r1=1 /\ 2:r7=0) Generated assembler _litmus_P0_0_: li r30,1 _litmus_P0_1_: stw r30,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r29,1 _litmus_P0_4_: stw r29,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r30,1 _litmus_P1_3_: stw r30,0(r2) _litmus_P2_0_: lwz r22,0(r11) _litmus_P2_1_: li r24,1 _litmus_P2_2_: stw r24,0(r9) _litmus_P2_3_: lwz r10,0(r9) _litmus_P2_4_: xor r8,r10,r10 _litmus_P2_5_: lwzx r23,r8,r2 Test podrwposwr059 Allowed Histogram (7 states) 449786:>1:r1=0; 2:r1=0; 2:r7=0; 5490 :>1:r1=1; 2:r1=0; 2:r7=0; 60043 :>1:r1=0; 2:r1=1; 2:r7=0; 243664:>1:r1=0; 2:r1=0; 2:r7=1; 57908 :>1:r1=1; 2:r1=0; 2:r7=1; 182860:>1:r1=0; 2:r1=1; 2:r7=1; 249 :>1:r1=1; 2:r1=1; 2:r7=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r7=0) is NOT validated Hash=8f6c6501090e086cd3addf1fdcb18d11 Cycle=DpdR Fre SyncdWW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr059 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW BCSyncdRW Time podrwposwr059 1.22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr060.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr060 "Fre SyncdWR Fre SyncdWW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | li r3,1 ; sync | sync | li r3,1 | stw r3,0(r4) ; lwz r3,0(r4) | li r3,1 | stw r3,0(r4) | lwz r5,0(r4) ; | stw r3,0(r4) | | ; exists (a=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: lwz r27,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r28,1 _litmus_P2_3_: stw r28,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr060 Allowed Histogram (15 states) 78827 :>0:r3=0; 2:r1=0; 3:r1=0; 3:r5=1; a=1; 207933:>0:r3=1; 2:r1=0; 3:r1=0; 3:r5=1; a=1; 6030 :>0:r3=0; 2:r1=1; 3:r1=0; 3:r5=1; a=1; 124598:>0:r3=1; 2:r1=1; 3:r1=0; 3:r5=1; a=1; 37392 :>0:r3=0; 2:r1=0; 3:r1=1; 3:r5=1; a=1; 236692:>0:r3=1; 2:r1=0; 3:r1=1; 3:r5=1; a=1; 3 :>0:r3=0; 2:r1=1; 3:r1=1; 3:r5=1; a=1; 2323 :>0:r3=1; 2:r1=1; 3:r1=1; 3:r5=1; a=1; 25699 :>0:r3=0; 2:r1=0; 3:r1=0; 3:r5=1; a=2; 234303:>0:r3=1; 2:r1=0; 3:r1=0; 3:r5=1; a=2; 24 :>0:r3=0; 2:r1=1; 3:r1=0; 3:r5=1; a=2; 29336 :>0:r3=1; 2:r1=1; 3:r1=0; 3:r5=1; a=2; 22 :>0:r3=0; 2:r1=0; 3:r1=1; 3:r5=1; a=2; 16812 :>0:r3=1; 2:r1=0; 3:r1=1; 3:r5=1; a=2; 6 :>0:r3=1; 2:r1=1; 3:r1=1; 3:r5=1; a=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=15a0ccebd11bdd4489de83d3aafbe8cb Cycle=Fre SyncdWR Fre SyncdWW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr060 No [PodRW,PosWR] Safe=Fre SyncdWR BCSyncdWW BCSyncdRW Time podrwposwr060 1.77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr061.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr061 "DpdR Fre SyncdWR Fre SyncdWW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | li r3,1 ; sync | sync | li r3,1 | stw r3,0(r4) ; lwz r3,0(r4) | li r3,1 | stw r3,0(r4) | lwz r5,0(r4) ; | stw r3,0(r4) | | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (0:r3=0 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r30,1 _litmus_P0_1_: stw r30,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r29,0(r2) _litmus_P1_0_: li r4,1 _litmus_P1_1_: stw r4,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: lwz r3,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r30,1 _litmus_P2_3_: stw r30,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r24,r8,r2 Test podrwposwr061 Allowed Histogram (14 states) 11702 :>0:r3=0; 2:r1=0; 3:r1=0; 3:r7=0; 253986:>0:r3=1; 2:r1=0; 3:r1=0; 3:r7=0; 8 :>0:r3=0; 2:r1=1; 3:r1=0; 3:r7=0; 71865 :>0:r3=1; 2:r1=1; 3:r1=0; 3:r7=0; 74 :>0:r3=0; 2:r1=0; 3:r1=1; 3:r7=0; 2813 :>0:r3=1; 2:r1=0; 3:r1=1; 3:r7=0; 184154:>0:r3=0; 2:r1=0; 3:r1=0; 3:r7=1; 171514:>0:r3=1; 2:r1=0; 3:r1=0; 3:r7=1; 1756 :>0:r3=0; 2:r1=1; 3:r1=0; 3:r7=1; 110065:>0:r3=1; 2:r1=1; 3:r1=0; 3:r7=1; 31048 :>0:r3=0; 2:r1=0; 3:r1=1; 3:r7=1; 160742:>0:r3=1; 2:r1=0; 3:r1=1; 3:r7=1; 1 :>0:r3=0; 2:r1=1; 3:r1=1; 3:r7=1; 272 :>0:r3=1; 2:r1=1; 3:r1=1; 3:r7=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (0:r3=0 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=31fa36aa0f213f190f74f474cda12603 Cycle=DpdR Fre SyncdWR Fre SyncdWW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr061 No [PodRW,PosWR] Safe=Fre SyncdWR DpdR BCSyncdWW BCSyncdRW Time podrwposwr061 1.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr062.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr062 "DpdW Wse SyncdWR Fre SyncdWW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | li r3,1 ; sync | sync | li r3,1 | stw r3,0(r4) ; lwz r3,0(r4) | li r3,1 | stw r3,0(r4) | lwz r5,0(r4) ; | stw r3,0(r4) | | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r27,0(r2) _litmus_P1_0_: li r28,1 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: lwz r27,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r28,1 _litmus_P2_3_: stw r28,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr062 Allowed Histogram (15 states) 143101:>0:r3=0; 2:r1=0; 3:r1=0; x=1; 188561:>0:r3=1; 2:r1=0; 3:r1=0; x=1; 9792 :>0:r3=0; 2:r1=1; 3:r1=0; x=1; 100767:>0:r3=1; 2:r1=1; 3:r1=0; x=1; 53450 :>0:r3=0; 2:r1=0; 3:r1=1; x=1; 212926:>0:r3=1; 2:r1=0; 3:r1=1; x=1; 12 :>0:r3=0; 2:r1=1; 3:r1=1; x=1; 2251 :>0:r3=1; 2:r1=1; 3:r1=1; x=1; 13762 :>0:r3=0; 2:r1=0; 3:r1=0; x=2; 236291:>0:r3=1; 2:r1=0; 3:r1=0; x=2; 2 :>0:r3=0; 2:r1=1; 3:r1=0; x=2; 35449 :>0:r3=1; 2:r1=1; 3:r1=0; x=2; 13 :>0:r3=0; 2:r1=0; 3:r1=1; x=2; 3622 :>0:r3=1; 2:r1=0; 3:r1=1; x=2; 1 :>0:r3=1; 2:r1=1; 3:r1=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=7324b05f2b14ceacb9b3f42d76280b5e Cycle=DpdW Wse SyncdWR Fre SyncdWW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr062 No [PodRW,PosWR] Safe=Fre Wse SyncdWR DpdW BCSyncdWW BCSyncdRW Time podrwposwr062 1.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr063.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr063 "DpdW Wse SyncdWW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 2:r8=x;} P0 | P1 | P2 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | li r3,1 ; sync | li r3,1 | stw r3,0(r4) ; li r3,1 | stw r3,0(r4) | lwz r5,0(r4) ; stw r3,0(r4) | | xor r6,r5,r5 ; | | li r7,1 ; | | stwx r7,r6,r8 ; exists (x=2 /\ 1:r1=1 /\ 2:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r27,1 _litmus_P0_4_: stw r27,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r28,1 _litmus_P1_3_: stw r28,0(r2) _litmus_P2_0_: lwz r22,0(r11) _litmus_P2_1_: li r24,1 _litmus_P2_2_: stw r24,0(r9) _litmus_P2_3_: lwz r23,0(r9) _litmus_P2_4_: xor r10,r23,r23 _litmus_P2_5_: li r8,1 _litmus_P2_6_: stwx r8,r10,r2 Test podrwposwr063 Allowed Histogram (7 states) 307562:>1:r1=0; 2:r1=0; x=1; 87653 :>1:r1=1; 2:r1=0; x=1; 300307:>1:r1=0; 2:r1=1; x=1; 1820 :>1:r1=1; 2:r1=1; x=1; 296473:>1:r1=0; 2:r1=0; x=2; 4232 :>1:r1=1; 2:r1=0; x=2; 1953 :>1:r1=0; 2:r1=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=1) is NOT validated Hash=7b09c06e97b34055e0a5d36831e6ef32 Cycle=DpdW Wse SyncdWW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr063 No [PodRW,PosWR] Safe=Wse DpdW BCSyncdWW BCSyncdRW Time podrwposwr063 1.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr064.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr064 "Fre SyncdWW Wse SyncdWW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | li r3,1 ; sync | sync | li r3,1 | stw r3,0(r4) ; li r3,1 | li r3,1 | stw r3,0(r4) | lwz r5,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (a=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: lwz r27,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r28,1 _litmus_P2_3_: stw r28,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr064 Allowed Histogram (17 states) 202659:>2:r1=0; 3:r1=0; 3:r5=1; a=1; x=1; 87986 :>2:r1=1; 3:r1=0; 3:r5=1; a=1; x=1; 127500:>2:r1=0; 3:r1=1; 3:r5=1; a=1; x=1; 292 :>2:r1=1; 3:r1=1; 3:r5=1; a=1; x=1; 305893:>2:r1=0; 3:r1=0; 3:r5=1; a=2; x=1; 37768 :>2:r1=1; 3:r1=0; 3:r5=1; a=2; x=1; 11365 :>2:r1=0; 3:r1=1; 3:r5=1; a=2; x=1; 157 :>2:r1=0; 3:r1=0; 3:r5=2; a=2; x=1; 57 :>2:r1=1; 3:r1=0; 3:r5=2; a=2; x=1; 22 :>2:r1=0; 3:r1=1; 3:r5=2; a=2; x=1; 175610:>2:r1=0; 3:r1=0; 3:r5=1; a=1; x=2; 380 :>2:r1=1; 3:r1=0; 3:r5=1; a=1; x=2; 27425 :>2:r1=0; 3:r1=1; 3:r5=1; a=1; x=2; 22855 :>2:r1=0; 3:r1=0; 3:r5=1; a=2; x=2; 22 :>2:r1=1; 3:r1=0; 3:r5=1; a=2; x=2; 2 :>2:r1=0; 3:r1=1; 3:r5=1; a=2; x=2; 7 :>2:r1=0; 3:r1=0; 3:r5=2; a=2; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ x=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=32f79072f51fc242aba7813bce1b7774 Cycle=Fre SyncdWW Wse SyncdWW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr064 No [PodRW,PosWR] Safe=Fre Wse SyncdWW BCSyncdWW BCSyncdRW Time podrwposwr064 2.01 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr065.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr065 "DpdR Fre SyncdWW Wse SyncdWW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | li r3,1 ; sync | sync | li r3,1 | stw r3,0(r4) ; li r3,1 | li r3,1 | stw r3,0(r4) | lwz r5,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (y=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r28,1 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: lwz r27,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r28,1 _litmus_P2_3_: stw r28,0(r2) _litmus_P3_0_: lwz r22,0(r11) _litmus_P3_1_: li r24,1 _litmus_P3_2_: stw r24,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r23,r8,r2 Test podrwposwr065 Allowed Histogram (15 states) 277972:>2:r1=0; 3:r1=0; 3:r7=0; y=1; 82744 :>2:r1=1; 3:r1=0; 3:r7=0; y=1; 44620 :>2:r1=0; 3:r1=1; 3:r7=0; y=1; 75 :>2:r1=1; 3:r1=1; 3:r7=0; y=1; 104640:>2:r1=0; 3:r1=0; 3:r7=1; y=1; 75199 :>2:r1=1; 3:r1=0; 3:r7=1; y=1; 197024:>2:r1=0; 3:r1=1; 3:r7=1; y=1; 7131 :>2:r1=1; 3:r1=1; 3:r7=1; y=1; 10635 :>2:r1=0; 3:r1=0; 3:r7=0; y=2; 58 :>2:r1=1; 3:r1=0; 3:r7=0; y=2; 201 :>2:r1=0; 3:r1=1; 3:r7=0; y=2; 137036:>2:r1=0; 3:r1=0; 3:r7=1; y=2; 4451 :>2:r1=1; 3:r1=0; 3:r7=1; y=2; 58202 :>2:r1=0; 3:r1=1; 3:r7=1; y=2; 12 :>2:r1=1; 3:r1=1; 3:r7=1; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=5f84c88857f0167827685b01f3dd5c56 Cycle=DpdR Fre SyncdWW Wse SyncdWW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr065 No [PodRW,PosWR] Safe=Fre Wse SyncdWW DpdR BCSyncdWW BCSyncdRW Time podrwposwr065 1.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr066.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr066 "DpdW Wse SyncdWW Wse SyncdWW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | sync | li r3,1 ; sync | sync | li r3,1 | stw r3,0(r4) ; li r3,1 | li r3,1 | stw r3,0(r4) | lwz r5,0(r4) ; stw r3,0(r4) | stw r3,0(r4) | | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ y=2 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: li r28,2 _litmus_P1_1_: stw r28,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r3,1 _litmus_P1_4_: stw r3,0(r2) _litmus_P2_0_: lwz r27,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r28,1 _litmus_P2_3_: stw r28,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr066 Allowed Histogram (14 states) 241106:>2:r1=0; 3:r1=0; x=1; y=1; 129609:>2:r1=1; 3:r1=0; x=1; y=1; 234143:>2:r1=0; 3:r1=1; x=1; y=1; 2293 :>2:r1=1; 3:r1=1; x=1; y=1; 219830:>2:r1=0; 3:r1=0; x=2; y=1; 24294 :>2:r1=1; 3:r1=0; x=2; y=1; 3139 :>2:r1=0; 3:r1=1; x=2; y=1; 100193:>2:r1=0; 3:r1=0; x=1; y=2; 3462 :>2:r1=1; 3:r1=0; x=1; y=2; 34377 :>2:r1=0; 3:r1=1; x=1; y=2; 6 :>2:r1=1; 3:r1=1; x=1; y=2; 7541 :>2:r1=0; 3:r1=0; x=2; y=2; 1 :>2:r1=1; 3:r1=0; x=2; y=2; 6 :>2:r1=0; 3:r1=1; x=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=db6594df13d2d30b55141e514c468add Cycle=DpdW Wse SyncdWW Wse SyncdWW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr066 No [PodRW,PosWR] Safe=Wse SyncdWW DpdW BCSyncdWW BCSyncdRW Time podrwposwr066 2.18 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr067.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr067 "Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | li r3,1 ; sync | li r3,1 | li r3,1 | stw r3,0(r4) ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) | lwz r5,0(r4) ; stw r3,0(r4) | | | ; exists (a=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r5=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r28,1 _litmus_P1_3_: stw r28,0(r2) _litmus_P2_0_: lwz r27,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r28,1 _litmus_P2_3_: stw r28,0(r2) _litmus_P3_0_: lwz r26,0(r9) _litmus_P3_1_: li r11,1 _litmus_P3_2_: stw r11,0(r2) _litmus_P3_3_: lwz r27,0(r2) Test podrwposwr067 Allowed Histogram (14 states) 125555:>1:r1=0; 2:r1=0; 3:r1=0; 3:r5=1; a=1; 159040:>1:r1=1; 2:r1=0; 3:r1=0; 3:r5=1; a=1; 127866:>1:r1=0; 2:r1=1; 3:r1=0; 3:r5=1; a=1; 5360 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r5=1; a=1; 173668:>1:r1=0; 2:r1=0; 3:r1=1; 3:r5=1; a=1; 12183 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r5=1; a=1; 1489 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r5=1; a=1; 265187:>1:r1=0; 2:r1=0; 3:r1=0; 3:r5=1; a=2; 17021 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r5=1; a=2; 91133 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r5=1; a=2; 41 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r5=1; a=2; 21450 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r5=1; a=2; 6 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r5=1; a=2; 1 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r5=1; a=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (a=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r5=1) is NOT validated Hash=fd1bef2991c7aa40765379cba8de428a Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr067 No [PodRW,PosWR] Safe=Fre BCSyncdWW BCSyncdRW Time podrwposwr067 1.74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr068.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr068 "DpdR Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | li r3,1 ; sync | li r3,1 | li r3,1 | stw r3,0(r4) ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) | lwz r5,0(r4) ; stw r3,0(r4) | | | xor r6,r5,r5 ; | | | lwzx r7,r6,r8 ; exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r7=0) Generated assembler _litmus_P0_0_: li r30,1 _litmus_P0_1_: stw r30,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r3,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r30,1 _litmus_P1_3_: stw r30,0(r2) _litmus_P2_0_: lwz r3,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r30,1 _litmus_P2_3_: stw r30,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r10,0(r9) _litmus_P3_4_: xor r8,r10,r10 _litmus_P3_5_: lwzx r24,r8,r2 Test podrwposwr068 Allowed Histogram (15 states) 258463:>1:r1=0; 2:r1=0; 3:r1=0; 3:r7=0; 18174 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r7=0; 73416 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r7=0; 7 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r7=0; 9198 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r7=0; 10 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r7=0; 16 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r7=0; 158549:>1:r1=0; 2:r1=0; 3:r1=0; 3:r7=1; 153344:>1:r1=1; 2:r1=0; 3:r1=0; 3:r7=1; 125767:>1:r1=0; 2:r1=1; 3:r1=0; 3:r7=1; 2404 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r7=1; 177187:>1:r1=0; 2:r1=0; 3:r1=1; 3:r7=1; 20787 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r7=1; 2677 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r7=1; 1 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r7=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r7=0) is NOT validated Hash=f8d8afed03ee40148c7923646872b840 Cycle=DpdR Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr068 No [PodRW,PosWR] Safe=Fre DpdR BCSyncdWW BCSyncdRW Time podrwposwr068 1.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrwposwr069.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrwposwr069 "DpdW Wse SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRW PosWR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r4=b; 3:r8=x;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | li r3,1 ; sync | li r3,1 | li r3,1 | stw r3,0(r4) ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) | lwz r5,0(r4) ; stw r3,0(r4) | | | xor r6,r5,r5 ; | | | li r7,1 ; | | | stwx r7,r6,r8 ; exists (x=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1) Generated assembler _litmus_P0_0_: li r28,2 _litmus_P0_1_: stw r28,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r3,1 _litmus_P0_4_: stw r3,0(r2) _litmus_P1_0_: lwz r27,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r28,1 _litmus_P1_3_: stw r28,0(r2) _litmus_P2_0_: lwz r27,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r28,1 _litmus_P2_3_: stw r28,0(r2) _litmus_P3_0_: lwz r23,0(r11) _litmus_P3_1_: li r25,1 _litmus_P3_2_: stw r25,0(r9) _litmus_P3_3_: lwz r24,0(r9) _litmus_P3_4_: xor r10,r24,r24 _litmus_P3_5_: li r8,1 _litmus_P3_6_: stwx r8,r10,r2 Test podrwposwr069 Allowed Histogram (14 states) 174996:>1:r1=0; 2:r1=0; 3:r1=0; x=1; 131981:>1:r1=1; 2:r1=0; 3:r1=0; x=1; 147883:>1:r1=0; 2:r1=1; 3:r1=0; x=1; 2411 :>1:r1=1; 2:r1=1; 3:r1=0; x=1; 238403:>1:r1=0; 2:r1=0; 3:r1=1; x=1; 56358 :>1:r1=1; 2:r1=0; 3:r1=1; x=1; 2294 :>1:r1=0; 2:r1=1; 3:r1=1; x=1; 220019:>1:r1=0; 2:r1=0; 3:r1=0; x=2; 2291 :>1:r1=1; 2:r1=0; 3:r1=0; x=2; 22543 :>1:r1=0; 2:r1=1; 3:r1=0; x=2; 1 :>1:r1=1; 2:r1=1; 3:r1=0; x=2; 817 :>1:r1=0; 2:r1=0; 3:r1=1; x=2; 2 :>1:r1=1; 2:r1=0; 3:r1=1; x=2; 1 :>1:r1=0; 2:r1=1; 3:r1=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1) is NOT validated Hash=ba18cc28f265bff5a5354d13d0d60469 Cycle=DpdW Wse SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRW PosWR Relax podrwposwr069 No [PodRW,PosWR] Safe=Wse DpdW BCSyncdWW BCSyncdRW Time podrwposwr069 1.88 $Revision: 3269 $ 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 -O */ /* barrier: user */ /* launch: changing */ /* memory: indirect */ /* safer: true */ /* preload: true */ /* para: self */ /* speedcheck: false */ /* proc used: 4 */ GCCOPTS="-Wall -std=gnu99 -O" LITMUSOPTS= Mon Jan 11 13:47:22 CET 2010