Wed Dec 23 13:42:11 NFT 2009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr000.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr000 "Fre SyncdWW Rfe PosRR DpdR PosRR" {0:r2=y; 0:r4=x; 1:r2=x; 1:r6=y;} P0 | P1 ; li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwz r3,0(r2) ; sync | xor r4,r3,r3 ; li r3,1 | lwzx r5,r4,r6 ; stw r3,0(r4) | lwz r7,0(r6) ; exists (1:r1=1 /\ 1:r3=0 /\ 1:r5=0 /\ 1:r7=0) Generated assembler _litmus_P1_0_: lwz 25,0(11) _litmus_P1_1_: lwz 29,0(11) _litmus_P1_2_: xor 6,29,29 _litmus_P1_3_: lwzx 8,6,9 _litmus_P1_4_: lwz 7,0(9) _litmus_P0_0_: li 5,1 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test posrr000 Allowed Histogram (5 states) 222 :>1:r1=0; 1:r3=0; 1:r5=0; 1:r7=1; 549 :>1:r1=0; 1:r3=1; 1:r5=1; 1:r7=1; 4714328:>1:r1=0; 1:r3=0; 1:r5=1; 1:r7=1; 15772664:>1:r1=0; 1:r3=0; 1:r5=0; 1:r7=0; 11512237:>1:r1=1; 1:r3=1; 1:r5=1; 1:r7=1; No Witnesses Positive: 0, Negative: 32000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 1:r5=0 /\ 1:r7=0) is NOT validated Hash=dca4403d3afb34d355df5cfe6b045e45 Cycle=Fre SyncdWW Rfe PosRR DpdR PosRR Relax posrr000 No PosRR Safe=Fre DpdR BCSyncdWW Time posrr000 1.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr001.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr001 "Fre SyncdWW Rfe SyncdRW Rfe PosRR DpdR PosRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r6=z;} P0 | P1 | P2 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | lwz r3,0(r2) ; sync | li r3,1 | xor r4,r3,r3 ; li r3,1 | stw r3,0(r4) | lwzx r5,r4,r6 ; stw r3,0(r4) | | lwz r7,0(r6) ; exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0 /\ 2:r5=0 /\ 2:r7=0) Generated assembler _litmus_P2_0_: lwz 24,0(11) _litmus_P2_1_: lwz 29,0(11) _litmus_P2_2_: xor 6,29,29 _litmus_P2_3_: lwzx 8,6,9 _litmus_P2_4_: lwz 7,0(9) _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: li 4,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test posrr001 Allowed Histogram (13 states) 16 :>1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; 2:r7=1; 20 :>1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; 2:r7=1; 108 :>1:r1=1; 2:r1=0; 2:r3=1; 2:r5=1; 2:r7=1; 64 :>1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; 2:r7=0; 157 :>1:r1=0; 2:r1=0; 2:r3=1; 2:r5=1; 2:r7=1; 91 :>1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; 2:r7=1; 1954260:>1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; 2:r7=0; 575215:>1:r1=0; 2:r1=0; 2:r3=0; 2:r5=1; 2:r7=1; 4802886:>1:r1=0; 2:r1=1; 2:r3=1; 2:r5=1; 2:r7=1; 1779234:>1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; 2:r7=0; 4460878:>1:r1=1; 2:r1=0; 2:r3=0; 2:r5=1; 2:r7=1; 6140902:>1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; 2:r7=0; 1286169:>1:r1=1; 2:r1=1; 2:r3=1; 2:r5=1; 2:r7=1; No Witnesses Positive: 0, Negative: 21000000 Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0 /\ 2:r5=0 /\ 2:r7=0) is NOT validated Hash=bda3ebc8e325ea91e8b0f345967e27a9 Cycle=Fre SyncdWW Rfe SyncdRW Rfe PosRR DpdR PosRR Relax posrr001 No PosRR Safe=Fre DpdR BCSyncdWW BCSyncdRW Time posrr001 2.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr002.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr002 "Fre SyncdWW Rfe DpdR PosRR" {0:r2=y; 0:r4=x; 1:r2=x; 1:r5=y;} P0 | P1 ; li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 ; sync | lwzx r4,r3,r5 ; li r3,1 | lwz r6,0(r5) ; stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r4=0 /\ 1:r6=0) Generated assembler _litmus_P1_0_: lwz 27,0(11) _litmus_P1_1_: xor 7,27,27 _litmus_P1_2_: lwzx 29,7,9 _litmus_P1_3_: lwz 8,0(9) _litmus_P0_0_: li 5,1 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test posrr002 Allowed Histogram (4 states) 246 :>1:r1=0; 1:r4=0; 1:r6=1; 5001606:>1:r1=0; 1:r4=1; 1:r6=1; 15782228:>1:r1=0; 1:r4=0; 1:r6=0; 11215920:>1:r1=1; 1:r4=1; 1:r6=1; No Witnesses Positive: 0, Negative: 32000000 Condition exists (1:r1=1 /\ 1:r4=0 /\ 1:r6=0) is NOT validated Hash=aa763fab21553ece116fd280efdc92e3 Cycle=Fre SyncdWW Rfe DpdR PosRR Relax posrr002 No PosRR Safe=Fre DpdR BCSyncdWW Time posrr002 1.67 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr003.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr003 "DpdR Fre SyncdWW Rfe DpdR PosRR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r5=z; 1:r9=x;} P0 | P1 ; li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 ; sync | lwzx r4,r3,r5 ; li r3,1 | lwz r6,0(r5) ; stw r3,0(r4) | xor r7,r6,r6 ; | lwzx r8,r7,r9 ; exists (1:r1=1 /\ 1:r8=0) Generated assembler _litmus_P1_0_: lwz 24,0(10) _litmus_P1_1_: xor 29,24,24 _litmus_P1_2_: lwzx 7,29,11 _litmus_P1_3_: lwz 6,0(11) _litmus_P1_4_: xor 5,6,6 _litmus_P1_5_: lwzx 25,5,9 _litmus_P0_0_: li 4,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test posrr003 Allowed Histogram (3 states) 11353673:>1:r1=1; 1:r8=1; 15521601:>1:r1=0; 1:r8=0; 5124726:>1:r1=0; 1:r8=1; No Witnesses Positive: 0, Negative: 32000000 Condition exists (1:r1=1 /\ 1:r8=0) is NOT validated Hash=b660291ec0b800081e710e7f87d96ef9 Cycle=DpdR Fre SyncdWW Rfe DpdR PosRR Relax posrr003 No PosRR Safe=Fre DpdR BCSyncdWW Time posrr003 1.85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr004.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr004 "Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z;} P0 | P1 | P2 ; li r1,1 | 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) | lwz r6,0(r5) ; stw r3,0(r4) | | ; exists (1:r1=1 /\ 2:r1=1 /\ 2:r4=0 /\ 2:r6=0) Generated assembler _litmus_P2_0_: lwz 26,0(11) _litmus_P2_1_: xor 7,26,26 _litmus_P2_2_: lwzx 29,7,9 _litmus_P2_3_: lwz 8,0(9) _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: li 4,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test posrr004 Allowed Histogram (10 states) 18 :>1:r1=1; 2:r1=0; 2:r4=0; 2:r6=1; 19 :>1:r1=0; 2:r1=1; 2:r4=0; 2:r6=1; 95 :>1:r1=0; 2:r1=0; 2:r4=0; 2:r6=1; 2000283:>1:r1=0; 2:r1=1; 2:r4=0; 2:r6=0; 534167:>1:r1=0; 2:r1=0; 2:r4=1; 2:r6=1; 6175039:>1:r1=0; 2:r1=0; 2:r4=0; 2:r6=0; 1203212:>1:r1=1; 2:r1=1; 2:r4=1; 2:r6=1; 4752079:>1:r1=0; 2:r1=1; 2:r4=1; 2:r6=1; 1864849:>1:r1=1; 2:r1=0; 2:r4=0; 2:r6=0; 4470239:>1:r1=1; 2:r1=0; 2:r4=1; 2:r6=1; No Witnesses Positive: 0, Negative: 21000000 Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r4=0 /\ 2:r6=0) is NOT validated Hash=dc1e41e1ec2673d57c366537084bc1c4 Cycle=Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR Relax posrr004 No PosRR Safe=Fre DpdR BCSyncdWW BCSyncdRW Time posrr004 2.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr005.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr005 "DpdR Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r5=a; 2:r9=x;} P0 | P1 | P2 ; li r1,1 | 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) | lwz r6,0(r5) ; stw r3,0(r4) | | xor r7,r6,r6 ; | | lwzx r8,r7,r9 ; exists (1:r1=1 /\ 2:r1=1 /\ 2:r8=0) Generated assembler _litmus_P2_0_: lwz 23,0(10) _litmus_P2_1_: xor 25,23,23 _litmus_P2_2_: lwzx 7,25,11 _litmus_P2_3_: lwz 6,0(11) _litmus_P2_4_: xor 5,6,6 _litmus_P2_5_: lwzx 24,5,9 _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: li 31,1 _litmus_P0_1_: stw 31,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test posrr005 Allowed Histogram (7 states) 1219685:>1:r1=1; 2:r1=1; 2:r8=1; 4338919:>1:r1=1; 2:r1=0; 2:r8=1; 5045894:>1:r1=0; 2:r1=1; 2:r8=1; 1901813:>1:r1=0; 2:r1=1; 2:r8=0; 622733:>1:r1=0; 2:r1=0; 2:r8=1; 6104725:>1:r1=0; 2:r1=0; 2:r8=0; 1766231:>1:r1=1; 2:r1=0; 2:r8=0; No Witnesses Positive: 0, Negative: 21000000 Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r8=0) is NOT validated Hash=8d0831339733254b3c8a1735bb7650c7 Cycle=DpdR Fre SyncdWW Rfe SyncdRW Rfe DpdR PosRR Relax posrr005 No PosRR Safe=Fre DpdR BCSyncdWW BCSyncdRW Time posrr005 2.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr006.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr006 "Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe DpdR PosRR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r5=a;} 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 | 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) | lwz r6,0(r5) ; stw r3,0(r4) | | | ; exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r4=0 /\ 3:r6=0) Generated assembler _litmus_P3_0_: lwz 27,0(11) _litmus_P3_1_: xor 7,27,27 _litmus_P3_2_: lwzx 29,7,9 _litmus_P3_3_: lwz 8,0(9) _litmus_P2_0_: lwz 30,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 31,1 _litmus_P2_3_: stw 31,0(9) _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: li 4,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test posrr006 Allowed Histogram (21 states) 1 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r4=0; 3:r6=1; 2 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r4=0; 3:r6=1; 11 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r4=0; 3:r6=1; 14 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r4=0; 3:r6=1; 25 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r4=0; 3:r6=1; 37 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r4=0; 3:r6=1; 131201:>1:r1=0; 2:r1=1; 3:r1=1; 3:r4=0; 3:r6=0; 62851 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r4=1; 3:r6=1; 146087:>1:r1=1; 2:r1=0; 3:r1=1; 3:r4=0; 3:r6=0; 113536:>1:r1=1; 2:r1=1; 3:r1=0; 3:r4=0; 3:r6=0; 823876:>1:r1=1; 2:r1=1; 3:r1=0; 3:r4=1; 3:r6=1; 125093:>1:r1=0; 2:r1=0; 3:r1=0; 3:r4=1; 3:r6=1; 1365719:>1:r1=1; 2:r1=0; 3:r1=0; 3:r4=1; 3:r6=1; 784574:>1:r1=0; 2:r1=1; 3:r1=1; 3:r4=1; 3:r6=1; 1578233:>1:r1=0; 2:r1=0; 3:r1=1; 3:r4=1; 3:r6=1; 1348774:>1:r1=0; 2:r1=1; 3:r1=0; 3:r4=1; 3:r6=1; 1926147:>1:r1=0; 2:r1=0; 3:r1=0; 3:r4=0; 3:r6=0; 1355444:>1:r1=0; 2:r1=0; 3:r1=1; 3:r4=0; 3:r6=0; 3054690:>1:r1=0; 2:r1=1; 3:r1=0; 3:r4=0; 3:r6=0; 2018980:>1:r1=1; 2:r1=0; 3:r1=1; 3:r4=1; 3:r6=1; 1164705:>1:r1=1; 2:r1=0; 3:r1=0; 3:r4=0; 3:r6=0; No Witnesses Positive: 0, Negative: 16000000 Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r4=0 /\ 3:r6=0) is NOT validated Hash=2669164f7a2ad6879aaa11955c600dc5 Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe DpdR PosRR Relax posrr006 No PosRR Safe=Fre DpdR BCSyncdWW BCSyncdRW Time posrr006 2.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr007.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr007 "Fre SyncdWW Rfe PosRR Fre SyncdWW Rfe PosRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwz r3,0(r2) | stw r1,0(r2) | lwz r3,0(r2) ; sync | | sync | ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) Generated assembler _litmus_P3_0_: lwz 31,0(9) _litmus_P3_1_: lwz 11,0(9) _litmus_P2_0_: li 5,2 _litmus_P2_1_: stw 5,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 4,1 _litmus_P2_4_: stw 4,0(9) _litmus_P1_0_: lwz 31,0(9) _litmus_P1_1_: lwz 11,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test posrr007 Allowed Histogram (77 states) 1 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 1 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 1 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 1 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1; 1 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1; 5 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=1; 2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 4 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2; 3 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1; 2 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=1; y=1; 4 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=2; 6 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 1 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=1; 2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 4 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 9 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=1; y=2; 1 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 3 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=1; 20 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 14 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=1; y=1; 9 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 19 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 21 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 5 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 14 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 9 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 24 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1; 18 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1; 7 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=1; 12 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 51 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2; 18 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1; 8 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 32 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 7 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 37 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; 80 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1; 23 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=1; y=2; 11 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1; 1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 63 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=1; 66 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 9 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=1; y=1; 34 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 25 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=1; 38 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=1; 9 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 33 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=1; y=1; 44 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 57 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 241688:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=2; 243428:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=2; 252646:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 218476:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=1; 197589:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=1; 174109:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=1; 496451:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 452271:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=1; y=1; 400736:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 420547:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=1; 165454:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 62032 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=1; 1026619:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 191995:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 418960:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 165097:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; y=2; 165581:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 1169737:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=1; 313712:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=1; y=1; 316933:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=1; 1237067:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=1; 1664279:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=1; 1401870:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 1283216:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=1; y=2; 1233818:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 1123273:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=1; y=2; 961547:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=1; No Witnesses Positive: 0, Negative: 16000000 Condition exists (x=2 /\ y=2 /\ 1:r1=1 /\ 1:r3=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated Hash=dd5096b6f2bf4363a180ba8c94b71b97 Cycle=Fre SyncdWW Rfe PosRR Fre SyncdWW Rfe PosRR Relax posrr007 No PosRR Safe=Fre BCSyncdWW Time posrr007 2.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr008.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr008 "DpdR Fre SyncdWW Rfe PosRR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r6=x;} P0 | P1 ; li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwz r3,0(r2) ; sync | xor r4,r3,r3 ; li r3,1 | lwzx r5,r4,r6 ; stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0 /\ 1:r5=0) Generated assembler _litmus_P1_0_: lwz 27,0(11) _litmus_P1_1_: lwz 29,0(11) _litmus_P1_2_: xor 7,29,29 _litmus_P1_3_: lwzx 8,7,9 _litmus_P0_0_: li 5,1 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test posrr008 Allowed Histogram (4 states) 843 :>1:r1=0; 1:r3=1; 1:r5=1; 11585538:>1:r1=1; 1:r3=1; 1:r5=1; 4663929:>1:r1=0; 1:r3=0; 1:r5=1; 15749690:>1:r1=0; 1:r3=0; 1:r5=0; No Witnesses Positive: 0, Negative: 32000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 1:r5=0) is NOT validated Hash=2ca85242fec82e5b95f9a9a93b21e48a Cycle=DpdR Fre SyncdWW Rfe PosRR Relax posrr008 No PosRR Safe=Fre DpdR BCSyncdWW Time posrr008 1.73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr009.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr009 "Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe PosRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r5=y; 2:r2=y; 2:r4=z; 3:r2=z;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) | lwz r3,0(r2) ; sync | lwzx r4,r3,r5 | sync | ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1) Generated assembler _litmus_P3_0_: lwz 31,0(9) _litmus_P3_1_: lwz 11,0(9) _litmus_P2_0_: li 5,1 _litmus_P2_1_: stw 5,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 4,1 _litmus_P2_4_: stw 4,0(9) _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: xor 8,30,30 _litmus_P1_2_: lwzx 31,8,9 _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test posrr009 Allowed Histogram (38 states) 4 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=1; z=1; 4 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=1; 3 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=2; z=2; 15 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=1; 20 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=2; 4 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=1; 2 :>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=1; z=2; 8 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=1; z=1; 9 :>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=2; z=2; 30 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=1; z=1; 18 :>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=2; z=2; 57 :>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=2; z=2; 9 :>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=2; z=2; 38 :>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=1; z=1; 69 :>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=1; z=1; 24 :>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=2; z=2; 34 :>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=1; z=1; 160976:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=2; 67811 :>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=1; 260262:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=2; 467237:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=2; 332641:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=2; 109412:>1:r1=1; 1:r4=0; 3:r1=1; 3:r3=1; z=1; 224169:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=2; 1398528:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=2; 188477:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=1; 1350914:>1:r1=0; 1:r4=1; 3:r1=1; 3:r3=1; z=2; 356822:>1:r1=0; 1:r4=1; 3:r1=0; 3:r3=0; z=1; 1284843:>1:r1=1; 1:r4=1; 3:r1=2; 3:r3=2; z=1; 795208:>1:r1=1; 1:r4=1; 3:r1=0; 3:r3=0; z=1; 705683:>1:r1=0; 1:r4=0; 3:r1=1; 3:r3=1; z=1; 1065307:>1:r1=1; 1:r4=1; 3:r1=1; 3:r3=1; z=1; 1011385:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=2; 1449963:>1:r1=0; 1:r4=0; 3:r1=2; 3:r3=2; z=1; 1043791:>1:r1=1; 1:r4=0; 3:r1=2; 3:r3=2; z=1; 1107991:>1:r1=0; 1:r4=1; 3:r1=2; 3:r3=2; z=2; 2449350:>1:r1=0; 1:r4=0; 3:r1=0; 3:r3=0; z=1; 168882:>1:r1=1; 1:r4=0; 3:r1=0; 3:r3=0; z=1; No Witnesses Positive: 0, Negative: 16000000 Condition exists (z=2 /\ 1:r1=1 /\ 1:r4=0 /\ 3:r1=1 /\ 3:r3=1) is NOT validated Hash=b445d37d77e5c3f9fac5d5dce20158ec Cycle=Fre SyncdWW Rfe DpdR Fre SyncdWW Rfe PosRR Relax posrr009 No PosRR Safe=Fre DpdR BCSyncdWW Time posrr009 4.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr010.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr010 "Fre SyncdWW Rfe SyncdRW Rfe PosRR" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y;} P0 | P1 | P2 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | lwz r3,0(r2) ; sync | li r3,1 | ; li r3,1 | stw r3,0(r4) | ; stw r3,0(r4) | | ; exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 2:r3=1) Generated assembler _litmus_P2_0_: lwz 31,0(9) _litmus_P2_1_: lwz 11,0(9) _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: li 4,2 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test posrr010 Allowed Histogram (18 states) 12 :>1:r1=1; 2:r1=0; 2:r3=2; y=1; 8 :>1:r1=0; 2:r1=0; 2:r3=2; y=1; 8 :>1:r1=1; 2:r1=0; 2:r3=1; y=1; 101 :>1:r1=1; 2:r1=2; 2:r3=1; y=1; 43 :>1:r1=0; 2:r1=0; 2:r3=1; y=1; 172 :>1:r1=0; 2:r1=0; 2:r3=1; y=2; 30 :>1:r1=0; 2:r1=2; 2:r3=1; y=1; 98 :>1:r1=0; 2:r1=1; 2:r3=2; y=2; 52 :>1:r1=0; 2:r1=0; 2:r3=2; y=2; 452920:>1:r1=0; 2:r1=2; 2:r3=2; y=1; 2049858:>1:r1=0; 2:r1=1; 2:r3=1; y=1; 2210692:>1:r1=0; 2:r1=1; 2:r3=1; y=2; 1189343:>1:r1=1; 2:r1=1; 2:r3=1; y=1; 2302544:>1:r1=0; 2:r1=0; 2:r3=0; y=1; 3899130:>1:r1=0; 2:r1=0; 2:r3=0; y=2; 2813791:>1:r1=0; 2:r1=2; 2:r3=2; y=2; 4325208:>1:r1=1; 2:r1=2; 2:r3=2; y=1; 1755990:>1:r1=1; 2:r1=0; 2:r3=0; y=1; No Witnesses Positive: 0, Negative: 21000000 Condition exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 2:r3=1) is NOT validated Hash=5b3cfa45c2982145969071c6dab1a9d9 Cycle=Fre SyncdWW Rfe SyncdRW Rfe PosRR Relax posrr010 No PosRR Safe=Fre BCSyncdWW BCSyncdRW Time posrr010 5.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr011.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr011 "DpdR Fre SyncdWW Rfe SyncdRW Rfe PosRR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r6=x;} P0 | P1 | P2 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | lwz r3,0(r2) ; sync | li r3,1 | xor r4,r3,r3 ; li r3,1 | stw r3,0(r4) | lwzx r5,r4,r6 ; stw r3,0(r4) | | ; exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0 /\ 2:r5=0) Generated assembler _litmus_P2_0_: lwz 26,0(11) _litmus_P2_1_: lwz 29,0(11) _litmus_P2_2_: xor 7,29,29 _litmus_P2_3_: lwzx 8,7,9 _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: li 31,1 _litmus_P0_1_: stw 31,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test posrr011 Allowed Histogram (10 states) 94 :>1:r1=0; 2:r1=0; 2:r3=1; 2:r5=0; 60 :>1:r1=1; 2:r1=0; 2:r3=1; 2:r5=1; 252 :>1:r1=0; 2:r1=0; 2:r3=1; 2:r5=1; 1189696:>1:r1=1; 2:r1=1; 2:r3=1; 2:r5=1; 1710840:>1:r1=0; 2:r1=1; 2:r3=1; 2:r5=0; 1720465:>1:r1=1; 2:r1=0; 2:r3=0; 2:r5=0; 686355:>1:r1=0; 2:r1=0; 2:r3=0; 2:r5=1; 5040614:>1:r1=0; 2:r1=1; 2:r3=1; 2:r5=1; 4696910:>1:r1=1; 2:r1=0; 2:r3=0; 2:r5=1; 5954714:>1:r1=0; 2:r1=0; 2:r3=0; 2:r5=0; No Witnesses Positive: 0, Negative: 21000000 Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0 /\ 2:r5=0) is NOT validated Hash=8b1358e772205e1d07c702e088c475e5 Cycle=DpdR Fre SyncdWW Rfe SyncdRW Rfe PosRR Relax posrr011 No PosRR Safe=Fre DpdR BCSyncdWW BCSyncdRW Time posrr011 4.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr012.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr012 "Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PosRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z;} P0 | P1 | P2 | P3 ; li r1,2 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | lwz r3,0(r2) ; sync | li r3,1 | li r3,1 | ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) | ; stw r3,0(r4) | | | ; exists (z=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=1) Generated assembler _litmus_P3_0_: lwz 31,0(9) _litmus_P3_1_: lwz 11,0(9) _litmus_P2_0_: lwz 30,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 31,1 _litmus_P2_3_: stw 31,0(9) _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: li 5,2 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test posrr012 Allowed Histogram (42 states) 2 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2; 1 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=1; 2 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=1; 1 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=1; 4 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=1; 9 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=1; 9 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2; 5 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; z=1; 4 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=1; 18 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=1; 26 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2; 35 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; z=1; 21 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2; 38 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=1; 78 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2; 69 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; z=1; 12 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2; 10 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2; 1 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2; 24 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; z=1; 11 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2; 59604 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=1; 210866:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2; 191921:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; z=2; 105574:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=1; 453987:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; z=2; 103509:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; z=1; 589613:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=1; 274769:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2; 325607:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=1; 2135112:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=1; 1225999:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; z=2; 736526:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; z=1; 423562:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=1; 176655:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2; 1206604:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; z=1; 761082:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=1; 1269294:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; z=1; 960240:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2; 1574848:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=1; 1653448:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2; 1560800:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2; No Witnesses Positive: 0, Negative: 16000000 Condition exists (z=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=1) is NOT validated Hash=2707402f3cf9f20b1f649906e5dcb239 Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PosRR Relax posrr012 No PosRR Safe=Fre BCSyncdWW BCSyncdRW Time posrr012 4.71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/posrr013.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC posrr013 "DpdR Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PosRR" {0:r2=x; 0:r4=y; 1:r2=y; 1:r4=z; 2:r2=z; 2:r4=a; 3:r2=a; 3:r6=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 | lwz r3,0(r2) ; sync | li r3,1 | li r3,1 | xor r4,r3,r3 ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) | lwzx r5,r4,r6 ; stw r3,0(r4) | | | ; exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0 /\ 3:r5=0) Generated assembler _litmus_P3_0_: lwz 27,0(11) _litmus_P3_1_: lwz 29,0(11) _litmus_P3_2_: xor 7,29,29 _litmus_P3_3_: lwzx 8,7,9 _litmus_P2_0_: lwz 30,0(11) _litmus_P2_1_: sync _litmus_P2_2_: li 31,1 _litmus_P2_3_: stw 31,0(9) _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 31,1 _litmus_P1_3_: stw 31,0(9) _litmus_P0_0_: li 4,1 _litmus_P0_1_: stw 4,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 3,1 _litmus_P0_4_: stw 3,0(9) Test posrr013 Allowed Histogram (22 states) 4 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; 3:r5=0; 1 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; 3:r5=0; 52 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; 3:r5=1; 31 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; 3:r5=1; 44 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; 3:r5=1; 31 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; 3:r5=0; 13 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; 3:r5=1; 96771 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; 3:r5=0; 108039:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; 3:r5=0; 73651 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; 3:r5=1; 860341:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; 3:r5=1; 120960:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; 3:r5=0; 849235:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; 3:r5=1; 1076004:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; 3:r5=0; 1847691:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; 3:r5=0; 157357:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; 3:r5=1; 2878452:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; 3:r5=0; 1735803:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; 3:r5=1; 2204086:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; 3:r5=1; 1541055:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; 3:r5=1; 1324879:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; 3:r5=1; 1125500:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; 3:r5=0; No Witnesses Positive: 0, Negative: 16000000 Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0 /\ 3:r5=0) is NOT validated Hash=c740edf890395d3b09045a9e97a8f79e Cycle=DpdR Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PosRR Relax posrr013 No PosRR Safe=Fre DpdR BCSyncdWW BCSyncdRW Time posrr013 7.43 $Revision: 3163 $ Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 100000 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 10 #endif #ifndef N_EXE #define N_EXE (64 < N ? 1 : 64 / N) #endif /* gcc options: -Wall -std=gnu99 -O -pthread -maix64 */ /* barrier: user */ /* tread start/join: changing */ /* memory: indirect */ /* safer: false */ /* preload: true */ /* para: self */ /* changes: false */ /* speedcheck: false */ /* proc used: 64 */ GCCOPTS="-Wall -std=gnu99 -O -pthread -maix64" LITMUSOPTS= Wed Dec 23 13:42:58 NFT 2009