Thu Dec 24 11:41:52 CET 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_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwz r8,0(r2) Test podrr000 Allowed Histogram (4 states) 12 :>1:r1=1; 1:r3=0; 907067:>1:r1=0; 1:r3=1; 914289:>1:r1=0; 1:r3=0; 178632:>1:r1=1; 1:r3=1; Ok Witnesses Positive: 12, Negative: 1999988 Condition exists (1:r1=1 /\ 1:r3=0) is validated Hash=78d7a77bf8b1a9bd43cfddf06e35d5d3 Cycle=Fre SyncdWW Rfe PodRR Relax podrr000 Ok PodRR Safe=Fre BCSyncdWW Time podrr000 1.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwz r8,0(r2) _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwz r8,0(r2) Test podrr001 Allowed Histogram (15 states) 133 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 713 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 137 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 1513 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 11399 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 19954 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 43152 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 79625 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 167987:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 41701 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 89857 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 282215:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 131944:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 42966 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 86704 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; No Witnesses Positive: 0, Negative: 1000000 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 2.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r9,1 _litmus_P0_1_: stw r9,0(r2) _litmus_P0_2_: sync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwz r8,0(r2) _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwz r8,0(r2) Test podrr002 Allowed Histogram (33 states) 7 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 1 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 12 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 13 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 764 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 209 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 186 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 457 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 389 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 17623 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 2660 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 1044 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 57877 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 9954 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 7777 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 9766 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 36953 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 851 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 82117 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 32435 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 40354 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 31099 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 28578 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 6768 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 95901 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 92575 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 4591 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 12285 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 5144 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 97862 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 273468:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 35106 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 15174 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; No Witnesses Positive: 0, Negative: 1000000 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 2.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r10,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r8,1 _litmus_P1_3_: stw r8,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwz r8,0(r2) Test podrr003 Allowed Histogram (7 states) 13116 :>1:r1=0; 2:r1=1; 2:r3=0; 262559:>1:r1=0; 2:r1=0; 2:r3=1; 162359:>1:r1=1; 2:r1=0; 2:r3=1; 361405:>1:r1=0; 2:r1=0; 2:r3=0; 197687:>1:r1=0; 2:r1=1; 2:r3=1; 691 :>1:r1=1; 2:r1=1; 2:r3=1; 2183 :>1:r1=1; 2:r1=0; 2:r3=0; No Witnesses Positive: 0, Negative: 1000000 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 1.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r8,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r10,1 _litmus_P1_3_: stw r10,0(r2) _litmus_P2_0_: lwz r8,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r10,1 _litmus_P2_3_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwz r8,0(r2) Test podrr004 Allowed Histogram (15 states) 1 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; 116 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; 347 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; 209 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; 487 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; 303 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; 4414 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; 30379 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; 124958:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; 314727:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; 126784:>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; 188057:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; 113220:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; 16316 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; 79682 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; No Witnesses Positive: 0, Negative: 1000000 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 2.04 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r9,1 _litmus_P0_1_: stw r9,0(r2) _litmus_P0_2_: sync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r8,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r10,1 _litmus_P1_3_: stw r10,0(r2) _litmus_P2_0_: lwz r8,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r10,1 _litmus_P2_3_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwz r8,0(r2) Test podrr005 Allowed Histogram (31 states) 2 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; z=2; 5 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; z=2; 7 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; z=2; 22 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; z=2; 184 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; z=2; 2 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; z=2; 35 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; z=2; 265 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; z=2; 486 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; z=2; 533 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; z=2; 736 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; z=2; 10352 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; z=2; 37872 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; z=2; 7469 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; z=2; 46930 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; z=2; 9478 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; z=2; 8501 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; z=2; 26498 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; z=2; 7716 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; z=2; 28860 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; z=2; 22790 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; z=2; 25612 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; z=2; 40525 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; z=2; 196621:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; z=2; 39265 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; z=2; 128036:>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; z=2; 51574 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; z=2; 149647:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; z=2; 22848 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; z=2; 117124:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; z=2; 20005 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; z=2; No Witnesses Positive: 0, Negative: 1000000 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 2.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r9,1 _litmus_P0_1_: stw r9,0(r2) _litmus_P0_2_: sync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r10,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r8,1 _litmus_P1_3_: stw r8,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwz r8,0(r2) Test podrr006 Allowed Histogram (17 states) 1 :>1:r1=1; 2:r1=1; 2:r3=1; y=2; 3 :>1:r1=2; 2:r1=1; 2:r3=1; y=2; 2 :>1:r1=1; 2:r1=1; 2:r3=0; y=2; 19 :>1:r1=1; 2:r1=0; 2:r3=1; y=2; 2612 :>1:r1=0; 2:r1=0; 2:r3=2; y=2; 8596 :>1:r1=2; 2:r1=0; 2:r3=0; y=2; 45433 :>1:r1=2; 2:r1=0; 2:r3=1; y=2; 13402 :>1:r1=1; 2:r1=1; 2:r3=2; y=2; 29935 :>1:r1=0; 2:r1=1; 2:r3=0; y=2; 99624 :>1:r1=1; 2:r1=0; 2:r3=2; y=2; 37281 :>1:r1=0; 2:r1=0; 2:r3=1; y=2; 154835:>1:r1=1; 2:r1=0; 2:r3=0; y=2; 189601:>1:r1=0; 2:r1=1; 2:r3=1; y=2; 162598:>1:r1=0; 2:r1=0; 2:r3=0; y=2; 45632 :>1:r1=0; 2:r1=1; 2:r3=2; y=2; 11564 :>1:r1=2; 2:r1=1; 2:r3=2; y=2; 198862:>1:r1=2; 2:r1=0; 2:r3=2; y=2; No Witnesses Positive: 0, Negative: 1000000 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 1.54 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r10,0(r2) _litmus_P1_1_: sync _litmus_P1_2_: li r9,2 _litmus_P1_3_: stw r9,0(r2) _litmus_P2_0_: lwz r8,0(r9) _litmus_P2_1_: sync _litmus_P2_2_: li r10,1 _litmus_P2_3_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwz r8,0(r2) Test podrr007 Allowed Histogram (30 states) 1 :>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=0; x=2; 185 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; 20 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=2; 94 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=1; 68 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2; 259 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; 1314 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; 333 :>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=2; 626 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; x=2; 1761 :>1:r1=1; 2:r1=2; 3:r1=0; 3:r3=1; x=2; 1057 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=1; 9221 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; 7769 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=1; 4869 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=0; x=1; 20937 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; x=2; 12926 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; 34483 :>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=1; 33892 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; 61525 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; 10291 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; 81814 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; 79074 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; 63480 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; 133001:>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=0; x=1; 192477:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; 29752 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; 68763 :>1:r1=0; 2:r1=2; 3:r1=1; 3:r3=1; x=1; 87967 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; 41970 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; 20071 :>1:r1=0; 2:r1=2; 3:r1=0; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 1000000 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 2.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r9,1 _litmus_P0_1_: stw r9,0(r2) _litmus_P0_2_: sync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P2_2_: sync _litmus_P2_3_: li r11,2 _litmus_P2_4_: stw r11,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwz r8,0(r2) Test podrr008 Allowed Histogram (75 states) 1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 5 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 2 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 4 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 3 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 10 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 2 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 21 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 3 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 3 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 2 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 81 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 20 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 4 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 15 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 6 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 9 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 29 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 87 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 230 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 141 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 29 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 57 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 295 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 997 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 380 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 2490 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 290 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 2369 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 274 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 2613 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 9498 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 1791 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 2341 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 1631 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 4078 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 5063 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 7313 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 15675 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 8388 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 3681 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 45447 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 32721 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 20639 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 3777 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 4270 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 21354 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 19320 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 3936 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 13470 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 10430 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 31609 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 12553 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 16729 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 19599 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 12502 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 48511 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 9909 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 18556 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 40730 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 3579 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 10172 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 53451 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 137571:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 30129 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 53172 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 8918 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 34217 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 11876 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 3142 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 31124 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 19533 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 62029 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 85093 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; No Witnesses Positive: 0, Negative: 1000000 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 4.05 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r10,0(r2) _litmus_P1_1_: sync _litmus_P1_2_: li r9,2 _litmus_P1_3_: stw r9,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwz r8,0(r2) Test podrr009 Allowed Histogram (16 states) 6 :>1:r1=0; 2:r1=2; 2:r3=0; x=2; 12 :>1:r1=0; 2:r1=1; 2:r3=0; x=2; 28 :>1:r1=0; 2:r1=1; 2:r3=0; x=1; 677 :>1:r1=1; 2:r1=0; 2:r3=0; x=2; 61430 :>1:r1=0; 2:r1=2; 2:r3=1; x=2; 72568 :>1:r1=0; 2:r1=2; 2:r3=0; x=1; 67621 :>1:r1=1; 2:r1=1; 2:r3=1; x=2; 287404:>1:r1=0; 2:r1=0; 2:r3=0; x=1; 59545 :>1:r1=0; 2:r1=1; 2:r3=1; x=2; 19152 :>1:r1=0; 2:r1=0; 2:r3=1; x=1; 221090:>1:r1=0; 2:r1=2; 2:r3=1; x=1; 31986 :>1:r1=1; 2:r1=0; 2:r3=1; x=2; 45422 :>1:r1=0; 2:r1=0; 2:r3=0; x=2; 39979 :>1:r1=0; 2:r1=1; 2:r3=1; x=1; 4105 :>1:r1=1; 2:r1=2; 2:r3=1; x=2; 88975 :>1:r1=0; 2:r1=0; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 1000000 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 1.46 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r8,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r10,1 _litmus_P1_3_: stw r10,0(r2) _litmus_P2_0_: lwz r10,0(r2) _litmus_P2_1_: sync _litmus_P2_2_: li r9,2 _litmus_P2_3_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwz r8,0(r2) Test podrr010 Allowed Histogram (30 states) 1 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; y=2; 24 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=1; y=2; 56 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=2; 211 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=2; 399 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; y=1; 147 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=2; 6830 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; y=1; 1011 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=1; y=1; 665 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; y=2; 6006 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; y=2; 31443 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=2; 11112 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=2; 105124:>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; y=1; 17496 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; y=1; 36964 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; y=2; 8995 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=2; 6460 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=2; 1789 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; y=2; 17612 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; y=2; 13636 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=2; 2695 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; y=1; 113965:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; y=1; 118049:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=2; 78954 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; y=2; 104930:>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; y=1; 41521 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=2; 53618 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; y=2; 179926:>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; y=1; 24013 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; y=1; 16348 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; y=1; No Witnesses Positive: 0, Negative: 1000000 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 2.46 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_P0_0_: li r9,1 _litmus_P0_1_: stw r9,0(r2) _litmus_P0_2_: sync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r8,0(r9) _litmus_P1_1_: sync _litmus_P1_2_: li r10,1 _litmus_P1_3_: stw r10,0(r2) _litmus_P2_0_: lwz r10,0(r2) _litmus_P2_1_: sync _litmus_P2_2_: li r9,2 _litmus_P2_3_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwz r8,0(r2) Test podrr011 Allowed Histogram (67 states) 1 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2; 1 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2; 1 :>1:r1=1; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2; 2 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2; 3 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2; 1 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2; 1 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2; 30 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2; 8 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2; 40 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2; 12 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2; 78 :>1:r1=1; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2; 3 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2; 89 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2; 18 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2; 420 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2; 401 :>1:r1=2; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2; 222 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2; 81 :>1:r1=2; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2; 355 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=1; x=2; y=2; 2509 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=1; y=2; 137 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2; 6833 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=2; x=2; y=2; 1060 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=0; x=2; y=2; 1390 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2; 2315 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2; 10132 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=2; y=2; 6505 :>1:r1=1; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2; 303 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2; 624 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2; 13387 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2; 17860 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=0; x=2; y=2; 5231 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2; 1224 :>1:r1=0; 2:r1=1; 3:r1=2; 3:r3=1; x=2; y=2; 9758 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=2; y=2; 7153 :>1:r1=2; 2:r1=1; 3:r1=0; 3:r3=2; x=2; y=2; 2348 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=1; y=2; 1095 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2; 6305 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=1; x=2; y=2; 2026 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2; 5565 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=1; x=2; y=2; 385 :>1:r1=1; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2; 30264 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2; 82388 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=2; x=2; y=2; 17707 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2; 21091 :>1:r1=0; 2:r1=1; 3:r1=0; 3:r3=0; x=2; y=2; 4043 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=1; x=2; y=2; 8494 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=1; x=1; y=2; 3915 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2; 6376 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=2; y=2; 10459 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=2; y=2; 15580 :>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2; 69709 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2; 83596 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=2; y=2; 1020 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2; 12042 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2; 42009 :>1:r1=0; 2:r1=1; 3:r1=1; 3:r3=0; x=2; y=2; 52914 :>1:r1=0; 2:r1=0; 3:r1=2; 3:r3=0; x=1; y=2; 55712 :>1:r1=2; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2; 42476 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2; 2539 :>1:r1=0; 2:r1=0; 3:r1=0; 3:r3=2; x=2; y=2; 109907:>1:r1=1; 2:r1=0; 3:r1=2; 3:r3=2; x=1; y=2; 109679:>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=2; x=1; y=2; 83898 :>1:r1=1; 2:r1=0; 3:r1=0; 3:r3=0; x=1; y=2; 3390 :>1:r1=0; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2; 2256 :>1:r1=2; 2:r1=0; 3:r1=1; 3:r3=2; x=1; y=2; 22624 :>1:r1=2; 2:r1=0; 3:r1=0; 3:r3=1; x=1; y=2; No Witnesses Positive: 0, Negative: 1000000 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 3.81 $Revision: 3163 $ Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 1000000 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 1 #endif #ifndef N_EXE #define N_EXE (4 < N ? 1 : 4 / N) #endif /* gcc options: -Wall -std=gnu99 */ /* barrier: user */ /* tread start/join: changing */ /* memory: indirect */ /* safer: false */ /* preload: true */ /* para: self */ /* changes: false */ /* speedcheck: false */ /* proc used: 4 */ GCCOPTS="-Wall -std=gnu99 " LITMUSOPTS= Thu Dec 24 11:42:20 CET 2009