Raw log

Mon Dec 28 22:21:40 NFT 2009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr000.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr000 "Fre SyncdWW Rfe PodRR" {0:r2=y; 0:r4=x; 1:r2=x; 1:r4=y;} P0 | P1 ; li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwz r3,0(r4) ; sync | ; li r3,1 | ; stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0) Generated assembler _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: lwz 31,0(9) _litmus_P0_0_: li 5,1 _litmus_P0_1_: stw 5,0(11) _litmus_P0_2_: sync _litmus_P0_3_: li 4,1 _litmus_P0_4_: stw 4,0(9) Test podrr000 Allowed Histogram (3 states) 46174402:>1:r1=0; 1:r3=1; 116105932:>1:r1=1; 1:r3=1; 157719666:>1:r1=0; 1:r3=0; No Witnesses Positive: 0, Negative: 320000000 Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated Hash=78d7a77bf8b1a9bd43cfddf06e35d5d3 Cycle=Fre SyncdWW Rfe PodRR Relax podrr000 No PodRR Safe=Fre BCSyncdWW Time podrr000 14.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr001.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr001 "Fre SyncdWW Rfe PodRR Fre SyncdWW Rfe PodRR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ; sync | | sync | ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 30,0(11) _litmus_P3_1_: lwz 31,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_: lwz 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 podrr001 Allowed Histogram (15 states) 2016791:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 1253759:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 11333775:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 849146:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 10119037:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 2164828:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 11878728:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 17739595:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 12473451:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 35350563:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 15192425:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 12910905:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 15694399:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 9790694:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 1231904:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; No Witnesses Positive: 0, Negative: 160000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=2e6b2a124722ed948c8f7dc35dc4b80f Cycle=Fre SyncdWW Rfe PodRR Fre SyncdWW Rfe PodRR Relax podrr001 No PodRR Safe=Fre BCSyncdWW Time podrr001 22.81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr002.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr002 "Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ; sync | | sync | ; li r3,2 | | li r3,1 | ; stw r3,0(r2) | | stw r3,0(r4) | ; exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 30,0(11) _litmus_P3_1_: lwz 31,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: lwz 31,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P0_2_: sync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test podrr002 Allowed Histogram (33 states) 17093 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 344395:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 1090610:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 536350:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 419124:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 803521:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 818157:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 1088733:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 2479767:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 2283455:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 1994269:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 526883:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 35802 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 1316733:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 1937200:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 89151 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 713376:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 10607993:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 1047053:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 434208:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 136370:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 754292:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 19722275:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 7622942:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 1628087:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 12170326:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 9081859:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 13638419:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 6714009:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 3528318:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 13091964:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 32170179:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 11157087:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; No Witnesses Positive: 0, Negative: 160000000 Condition exists (z=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=c594109cf9f75c58c9eec5a696ceb0a0 Cycle=Fre SyncsWW Rfe PodRR Fre SyncdWW Rfe PodRR Relax podrr002 No PodRR Safe=Fre BCSyncsWW BCSyncdWW Time podrr002 22.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr003.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr003 "Fre SyncdWW Rfe SyncdRW Rfe PodRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | lwz r3,0(r4) ; sync | li r3,1 | ; li r3,1 | stw r3,0(r4) | ; stw r3,0(r4) | | ; exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 30,0(11) _litmus_P2_1_: lwz 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 podrr003 Allowed Histogram (7 states) 21202998:>1:r1=0; 2:r1=1; 2:r3=0; 12822697:>1:r1=1; 2:r1=1; 2:r3=1; 5311334:>1:r1=0; 2:r1=0; 2:r3=1; 60083580:>1:r1=0; 2:r1=0; 2:r3=0; 47115028:>1:r1=0; 2:r1=1; 2:r3=1; 44560416:>1:r1=1; 2:r1=0; 2:r3=1; 18903947:>1:r1=1; 2:r1=0; 2:r3=0; No Witnesses Positive: 0, Negative: 210000000 Condition exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=3d48b5b0d8516d3d909b0a4f66959c71 Cycle=Fre SyncdWW Rfe SyncdRW Rfe PodRR Relax podrr003 No PodRR Safe=Fre BCSyncdWW BCSyncdRW Time podrr003 18.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr004.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr004 "Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | lwz r3,0(r4) ; sync | li r3,1 | li r3,1 | ; li r3,1 | stw r3,0(r4) | stw r3,0(r4) | ; stw r3,0(r4) | | | ; exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 30,0(11) _litmus_P3_1_: lwz 31,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 podrr004 Allowed Histogram (15 states) 702585:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; 1412186:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; 8154241:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; 1200536:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; 1183713:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; 8202425:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; 11184909:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; 18227953:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; 13439758:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; 15756333:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; 13483571:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; 21964630:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; 30196847:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; 13459161:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; 1431152:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; No Witnesses Positive: 0, Negative: 160000000 Condition exists (1:r1=1 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=b2067185c885838837d33372d57790fb Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR Relax podrr004 No PodRR Safe=Fre BCSyncdWW BCSyncdRW Time podrr004 22.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr005.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr005 "Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | lwz r3,0(r4) ; sync | li r3,1 | li r3,1 | ; li r3,2 | stw r3,0(r4) | stw r3,0(r4) | ; stw r3,0(r2) | | | ; exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 30,0(11) _litmus_P3_1_: lwz 31,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 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P0_2_: sync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test podrr005 Allowed Histogram (33 states) 78604 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2; 356311:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2; 6390 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; z=2; 183627:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2; 542379:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2; 331777:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2; 513497:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2; 687996:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2; 1230295:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2; 1195279:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; z=2; 1225077:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2; 585041:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2; 2730094:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2; 109898:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2; 1251531:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2; 1952353:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2; 8049112:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2; 786690:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2; 486710:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2; 1230067:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2; 2198684:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2; 459929:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2; 8903513:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2; 13360351:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2; 9938511:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2; 12282219:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2; 24904946:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2; 27973911:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2; 12236873:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2; 6736289:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2; 15430534:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2; 411028:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2; 1630484:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2; No Witnesses Positive: 0, Negative: 160000000 Condition exists (z=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=1a4d6f8ada041391fb8c242b28f54910 Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncdRW Rfe PodRR Relax podrr005 No PodRR Safe=Fre BCSyncsWW BCSyncdRW Time podrr005 21.85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr006.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr006 "Fre SyncsWW Rfe SyncdRW Rfe PodRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | lwz r3,0(r4) ; sync | li r3,1 | ; li r3,2 | stw r3,0(r4) | ; stw r3,0(r2) | | ; exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 30,0(11) _litmus_P2_1_: lwz 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,1 _litmus_P0_1_: stw 5,0(9) _litmus_P0_2_: sync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test podrr006 Allowed Histogram (15 states) 282633:>1:r1=0; 2:r1=0; 2:r3=1; y=2; 258036:>1:r1=1; 2:r1=1; 2:r3=1; y=2; 859397:>1:r1=1; 2:r1=0; 2:r3=2; y=2; 2626187:>1:r1=1; 2:r1=1; 2:r3=2; y=2; 3181453:>1:r1=2; 2:r1=0; 2:r3=1; y=2; 1198334:>1:r1=0; 2:r1=0; 2:r3=2; y=2; 4452400:>1:r1=1; 2:r1=0; 2:r3=0; y=2; 4152297:>1:r1=0; 2:r1=1; 2:r3=1; y=2; 2165829:>1:r1=1; 2:r1=0; 2:r3=1; y=2; 28352297:>1:r1=2; 2:r1=0; 2:r3=0; y=2; 43458469:>1:r1=2; 2:r1=0; 2:r3=2; y=2; 18621465:>1:r1=2; 2:r1=1; 2:r3=2; y=2; 31888410:>1:r1=0; 2:r1=1; 2:r3=2; y=2; 22248770:>1:r1=0; 2:r1=1; 2:r3=0; y=2; 46254023:>1:r1=0; 2:r1=0; 2:r3=0; y=2; No Witnesses Positive: 0, Negative: 210000000 Condition exists (y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=f5e5097c67500c52603a1c0158bb8551 Cycle=Fre SyncsWW Rfe SyncdRW Rfe PodRR Relax podrr006 No PodRR Safe=Fre BCSyncsWW BCSyncdRW Time podrr006 18.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr007.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr007 "Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR" {0:r2=z; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} 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(r4) ; sync | li r3,2 | li r3,1 | ; li r3,1 | stw r3,0(r2) | stw r3,0(r4) | ; stw r3,0(r4) | | | ; exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 30,0(11) _litmus_P3_1_: lwz 31,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 3,0(9) _litmus_P1_1_: sync _litmus_P1_2_: li 10,2 _litmus_P1_3_: stw 10,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 podrr007 Allowed Histogram (31 states) 1083488:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2; 261961:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; 683892:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; 1392497:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2; 1564813:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; 2875148:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; 646248:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; 1092636:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; 4501121:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; 1250189:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1; 2175555:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2; 6852905:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; 2961673:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2; 4478450:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; 12914933:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; 1761267:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; 12179182:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; 10640469:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; 2470156:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1; 704827:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; 4756030:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; 9025330:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1; 1384548:>1:r1=1; 2:r1=2; 3:r1=1; 3:r3=1; x=2; 8524379:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1; 5348207:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1; 10906044:>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2; 14792944:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; 1234798:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1; 12055409:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; 253489:>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2; 19227412:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1; No Witnesses Positive: 0, Negative: 160000000 Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=c22fcb545cb7b0f7f27c11adc702bd5e Cycle=Fre SyncdWW Rfe SyncsRW Rfe SyncdRW Rfe PodRR Relax podrr007 No PodRR Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW Time podrr007 22.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr008.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr008 "Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwz r3,0(r4) | stw r1,0(r2) | lwz r3,0(r4) ; sync | | sync | ; li r3,2 | | li r3,2 | ; stw r3,0(r2) | | stw r3,0(r2) | ; exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 30,0(11) _litmus_P3_1_: lwz 31,0(9) _litmus_P2_0_: li 5,1 _litmus_P2_1_: stw 5,0(9) _litmus_P2_2_: sync _litmus_P2_3_: li 11,2 _litmus_P2_4_: stw 11,0(9) _litmus_P1_0_: lwz 30,0(11) _litmus_P1_1_: lwz 31,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P0_2_: sync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test podrr008 Allowed Histogram (73 states) 71 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 225 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 204 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 526 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 1763 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 1872 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 5012 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 5399 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 8369 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 16804 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 38994 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 7227 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 31950 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 152164:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 10055 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 9304 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 47244 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 109269:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 160526:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 137576:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 39965 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 128889:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 33692 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 60315 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 96233 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 120011:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 53377 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 1018923:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 225203:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 712176:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 780767:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 215176:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 124731:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 652088:>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 588507:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 696948:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 1219093:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 842212:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 853482:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 1049817:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 1421289:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 733944:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 374888:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 724571:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 826017:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 1138630:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 654357:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 745228:>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1190094:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 1144811:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 653708:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 727958:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 5963756:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 853828:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 639615:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 1441148:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 1177376:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 1096972:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 3680052:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 3724391:>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 974887:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 10351348:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 29205517:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 6177103:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 3969701:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 5851851:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 3989955:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 11228388:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 5913569:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 11182681:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 10224535:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 21761672:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; No Witnesses Positive: 0, Negative: 160000000 Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=58c192e74d841e0ccb20b3014a58a473 Cycle=Fre SyncsWW Rfe PodRR Fre SyncsWW Rfe PodRR Relax podrr008 No PodRR Safe=Fre BCSyncsWW Time podrr008 22.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr009.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr009 "Fre SyncdWW Rfe SyncsRW Rfe PodRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | lwz r3,0(r4) ; sync | li r3,2 | ; li r3,1 | stw r3,0(r2) | ; stw r3,0(r4) | | ; exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P2_0_: lwz 30,0(11) _litmus_P2_1_: lwz 31,0(9) _litmus_P1_0_: lwz 31,0(9) _litmus_P1_1_: sync _litmus_P1_2_: li 10,2 _litmus_P1_3_: stw 10,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 podrr009 Allowed Histogram (14 states) 33 :>1:r1=0; 2:r1=2; 2:r3=0; x=2; 3079569:>1:r1=0; 2:r1=1; 2:r3=1; x=2; 4786405:>1:r1=0; 2:r1=0; 2:r3=1; x=2; 5766080:>1:r1=0; 2:r1=2; 2:r3=1; x=2; 15107790:>1:r1=0; 2:r1=2; 2:r3=1; x=1; 17573184:>1:r1=1; 2:r1=0; 2:r3=0; x=2; 24057370:>1:r1=0; 2:r1=1; 2:r3=1; x=1; 11823406:>1:r1=0; 2:r1=0; 2:r3=0; x=2; 10461109:>1:r1=1; 2:r1=0; 2:r3=1; x=2; 52880889:>1:r1=0; 2:r1=0; 2:r3=0; x=1; 23825512:>1:r1=1; 2:r1=1; 2:r3=1; x=2; 17675775:>1:r1=0; 2:r1=2; 2:r3=0; x=1; 3778966:>1:r1=0; 2:r1=0; 2:r3=1; x=1; 19183912:>1:r1=1; 2:r1=2; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 210000000 Condition exists (x=2 /\ 1:r1=1 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=d6249053a9b844d8e7a3045b38500a3a Cycle=Fre SyncdWW Rfe SyncsRW Rfe PodRR Relax podrr009 No PodRR Safe=Fre BCSyncsRW BCSyncdWW Time podrr009 17.97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr010.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr010 "Fre SyncdWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | lwz r3,0(r4) ; sync | li r3,1 | li r3,2 | ; li r3,1 | stw r3,0(r4) | stw r3,0(r2) | ; stw r3,0(r4) | | | ; exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 30,0(11) _litmus_P3_1_: lwz 31,0(9) _litmus_P2_0_: lwz 3,0(9) _litmus_P2_1_: sync _litmus_P2_2_: li 10,2 _litmus_P2_3_: stw 10,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,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 podrr010 Allowed Histogram (32 states) 1 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=2; 527609:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2; 470129:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2; 1235376:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2; 563855:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2; 590321:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1; 1913533:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2; 1367674:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; y=2; 1293931:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2; 1502764:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2; 1112902:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2; 3330957:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2; 678519:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2; 570481:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2; 2568621:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1; 2630083:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2; 7053759:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1; 5169934:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2; 3217708:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2; 5321819:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2; 1291977:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1; 11091498:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1; 6900705:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2; 10508078:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1; 14346751:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1; 10567849:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2; 11469456:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2; 14634651:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1; 6132324:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1; 3382502:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1; 18289375:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2; 10264858:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1; No Witnesses Positive: 0, Negative: 160000000 Condition exists (y=2 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=fcb68021656d7cbdb455ef5bd2648d65 Cycle=Fre SyncdWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR Relax podrr010 No PodRR Safe=Fre BCSyncsRW BCSyncdWW BCSyncdRW Time podrr010 21.80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for ./src/podrr011.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC podrr011 "Fre SyncsWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 3:r2=x; 3:r4=y;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | lwz r1,0(r2) | lwz r1,0(r2) ; stw r1,0(r2) | sync | sync | lwz r3,0(r4) ; sync | li r3,1 | li r3,2 | ; li r3,2 | stw r3,0(r4) | stw r3,0(r2) | ; stw r3,0(r2) | | | ; exists (x=2 /\ y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P3_0_: lwz 30,0(11) _litmus_P3_1_: lwz 31,0(9) _litmus_P2_0_: lwz 3,0(9) _litmus_P2_1_: sync _litmus_P2_2_: li 10,2 _litmus_P2_3_: stw 10,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 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P0_2_: sync _litmus_P0_3_: li 11,2 _litmus_P0_4_: stw 11,0(9) Test podrr011 Allowed Histogram (66 states) 5590 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2; 8614 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2; 84293 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2; 55383 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2; 50218 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2; 56718 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2; 197667:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2; 31802 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2; 147557:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2; 273279:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2; 10368 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2; 114613:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2; 131942:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2; 48085 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2; 148188:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2; 79678 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2; 349134:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2; 361674:>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2; 325584:>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2; 210494:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2; 259885:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2; 1014423:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2; 97161 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2; 128813:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2; 156907:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2; 388494:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2; 237850:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2; 360790:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2; 769681:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2; 865031:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2; 617698:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2; 544322:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2; 307036:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2; 619575:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2; 2004032:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2; 1005850:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2; 2996944:>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2; 2318232:>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2; 3610126:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2; 692444:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2; 420510:>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2; 847557:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2; 765237:>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2; 412217:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2; 530994:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2; 997811:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2; 5341724:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2; 2727508:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2; 1640607:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2; 596484:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2; 4408833:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2; 2910244:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2; 7074443:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2; 5640671:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2; 2273173:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2; 2011615:>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2; 6969400:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2; 2840148:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2; 15882428:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2; 8099657:>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2; 9225835:>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2; 10154364:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2; 14004392:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2; 15455207:>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2; 9838524:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2; 7244242:>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2; No Witnesses Positive: 0, Negative: 160000000 Condition exists (x=2 /\ y=2 /\ 1:r1=2 /\ 2:r1=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=a463a88f960487eded38b9c473eec1b5 Cycle=Fre SyncsWW Rfe SyncdRW Rfe SyncsRW Rfe PodRR Relax podrr011 No PodRR Safe=Fre BCSyncsWW BCSyncsRW BCSyncdRW Time podrr011 21.61 $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=-r 100 Mon Dec 28 22:25:48 NFT 2009