Wed Dec 23 18:57:31 CET 2009 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr000.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr000 "Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR" {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 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 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_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr000 Allowed Histogram (21 states) 3 :>3:r1=0; 3:r3=0; x=2; y=2; 18 :>3:r1=1; 3:r3=1; x=2; y=2; 436 :>3:r1=2; 3:r3=0; x=1; y=2; 695 :>3:r1=1; 3:r3=0; x=1; y=1; 1609 :>3:r1=0; 3:r3=1; x=2; y=2; 15592 :>3:r1=0; 3:r3=0; x=2; y=1; 374 :>3:r1=2; 3:r3=0; x=2; y=1; 2702 :>3:r1=1; 3:r3=1; x=2; y=1; 3148 :>3:r1=1; 3:r3=0; x=1; y=2; 22440 :>3:r1=2; 3:r3=0; x=1; y=1; 16101 :>3:r1=1; 3:r3=1; x=1; y=2; 43426 :>3:r1=2; 3:r3=1; x=1; y=2; 43673 :>3:r1=0; 3:r3=1; x=2; y=1; 28340 :>3:r1=0; 3:r3=0; x=1; y=2; 152493:>3:r1=2; 3:r3=1; x=2; y=1; 216009:>3:r1=2; 3:r3=1; x=1; y=1; 62280 :>3:r1=0; 3:r3=1; x=1; y=1; 32388 :>3:r1=0; 3:r3=1; x=1; y=2; 256908:>3:r1=0; 3:r3=0; x=1; y=1; 101345:>3:r1=1; 3:r3=1; x=1; y=1; 20 :>3:r1=2; 3:r3=1; x=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=7074ebf0a4e494a7c168353216394741 Cycle=Fre SyncdWW Wse SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr000 No ACLwSyncdRR Safe=Fre Wse SyncdWW Time aclwdrr000 2.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr001.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr001 "Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR" {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 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | sync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr001 Allowed Histogram (21 states) 101 :>3:r1=1; 3:r3=1; x=2; y=2; 80 :>3:r1=1; 3:r3=0; x=1; y=1; 108 :>3:r1=2; 3:r3=1; x=2; y=2; 20 :>3:r1=0; 3:r3=0; x=2; y=2; 193 :>3:r1=2; 3:r3=0; x=1; y=2; 3635 :>3:r1=1; 3:r3=0; x=1; y=2; 890 :>3:r1=2; 3:r3=0; x=2; y=1; 22888 :>3:r1=2; 3:r3=0; x=1; y=1; 50669 :>3:r1=0; 3:r3=0; x=1; y=2; 22696 :>3:r1=1; 3:r3=1; x=1; y=2; 70931 :>3:r1=0; 3:r3=0; x=2; y=1; 76811 :>3:r1=2; 3:r3=1; x=1; y=2; 29582 :>3:r1=1; 3:r3=1; x=1; y=1; 21296 :>3:r1=0; 3:r3=1; x=1; y=2; 170121:>3:r1=2; 3:r3=1; x=2; y=1; 153949:>3:r1=2; 3:r3=1; x=1; y=1; 114511:>3:r1=0; 3:r3=1; x=2; y=1; 37847 :>3:r1=0; 3:r3=1; x=1; y=1; 209933:>3:r1=0; 3:r3=0; x=1; y=1; 8566 :>3:r1=1; 3:r3=1; x=2; y=1; 5173 :>3:r1=0; 3:r3=1; x=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=42a8ec6eccd807ced6dea1376fc81b0b Cycle=Fre LwSyncdWW Wse SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr001 No ACLwSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time aclwdrr001 2.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr002.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr002 "Fre SyncdWW Wse Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | | lwz r3,0(r4) ; li r3,1 | | ; stw r3,0(r4) | | ; exists (x=2 /\ 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_: li r9,2 _litmus_P1_1_: stw r9,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr002 Allowed Histogram (9 states) 180 :>2:r1=0; 2:r3=0; x=2; 16328 :>2:r1=2; 2:r3=0; x=1; 23654 :>2:r1=1; 2:r3=1; x=2; 99142 :>2:r1=0; 2:r3=1; x=2; 320719:>2:r1=2; 2:r3=1; x=1; 326370:>2:r1=0; 2:r3=0; x=1; 102907:>2:r1=1; 2:r3=1; x=1; 17730 :>2:r1=2; 2:r3=1; x=2; 92970 :>2:r1=0; 2:r3=1; x=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=e86498b53008de1e6a240afbf078cd14 Cycle=Fre SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr002 No ACLwSyncdRR Safe=Fre Wse SyncdWW Time aclwdrr002 1.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr003.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr003 "Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR" {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 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r8,0(r2) _litmus_P1_0_: li r11,1 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr003 Allowed Histogram (21 states) 15 :>0:r3=0; 3:r1=2; 3:r3=1; y=2; 13 :>0:r3=0; 3:r1=0; 3:r3=0; y=2; 23 :>0:r3=0; 3:r1=1; 3:r3=1; y=2; 227 :>0:r3=1; 3:r1=1; 3:r3=0; y=1; 194 :>0:r3=1; 3:r1=2; 3:r3=0; y=2; 3120 :>0:r3=0; 3:r1=1; 3:r3=1; y=1; 5217 :>0:r3=1; 3:r1=1; 3:r3=0; y=2; 2150 :>0:r3=0; 3:r1=2; 3:r3=0; y=1; 2380 :>0:r3=0; 3:r1=0; 3:r3=1; y=2; 37463 :>0:r3=1; 3:r1=2; 3:r3=1; y=2; 72940 :>0:r3=1; 3:r1=0; 3:r3=0; y=2; 24170 :>0:r3=1; 3:r1=1; 3:r3=1; y=2; 41514 :>0:r3=0; 3:r1=0; 3:r3=0; y=1; 21254 :>0:r3=1; 3:r1=0; 3:r3=1; y=2; 119854:>0:r3=0; 3:r1=0; 3:r3=1; y=1; 44851 :>0:r3=1; 3:r1=2; 3:r3=0; y=1; 145728:>0:r3=0; 3:r1=2; 3:r3=1; y=1; 39030 :>0:r3=1; 3:r1=0; 3:r3=1; y=1; 253471:>0:r3=1; 3:r1=0; 3:r3=0; y=1; 29487 :>0:r3=1; 3:r1=1; 3:r3=1; y=1; 156899:>0:r3=1; 3:r1=2; 3:r3=1; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=9599d8c79b2e28a1f015a74966a65bac Cycle=Fre SyncdWR Fre SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr003 No ACLwSyncdRR Safe=Fre Wse SyncdWW SyncdWR Time aclwdrr003 2.12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr004.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr004 "Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR" {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 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r2) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 0:r3=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_: lwz r10,0(r2) _litmus_P1_0_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr004 Allowed Histogram (36 states) 19 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 41 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 244 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 17 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2; 250 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1; 952 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 1419 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2; 4272 :>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 2930 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1; 28 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 3479 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 29 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 3130 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1; 68 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 19463 :>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 298 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 5357 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 15224 :>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 6232 :>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2; 501 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 112820:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2; 35930 :>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 60975 :>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 46398 :>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 6330 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 5047 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 88498 :>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 130777:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 72571 :>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; 74318 :>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 72203 :>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 110236:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 12540 :>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 41637 :>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 13775 :>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 51992 :>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=32cc2d7800b6941b57852b520691800f Cycle=Fre SyncsWR Fre SyncdWW Wse Rfe LwSyncdRR Relax aclwdrr004 No ACLwSyncdRR Safe=Fre Wse SyncsWR SyncdWW Time aclwdrr004 2.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr005.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr005 "Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR" {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 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 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_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr005 Allowed Histogram (21 states) 5 :>3:r1=0; 3:r3=0; x=2; y=2; 36 :>3:r1=1; 3:r3=1; x=2; y=2; 580 :>3:r1=0; 3:r3=1; x=2; y=2; 111 :>3:r1=2; 3:r3=1; x=2; y=2; 2122 :>3:r1=2; 3:r3=0; x=1; y=2; 410 :>3:r1=1; 3:r3=0; x=1; y=1; 7803 :>3:r1=0; 3:r3=0; x=2; y=1; 104 :>3:r1=2; 3:r3=0; x=2; y=1; 11777 :>3:r1=1; 3:r3=0; x=1; y=2; 7532 :>3:r1=2; 3:r3=0; x=1; y=1; 8437 :>3:r1=0; 3:r3=1; x=1; y=2; 12365 :>3:r1=0; 3:r3=1; x=1; y=1; 108842:>3:r1=1; 3:r3=1; x=1; y=2; 70458 :>3:r1=1; 3:r3=1; x=1; y=1; 173806:>3:r1=2; 3:r3=1; x=2; y=1; 15322 :>3:r1=0; 3:r3=0; x=1; y=2; 213012:>3:r1=2; 3:r3=1; x=1; y=1; 80288 :>3:r1=2; 3:r3=1; x=1; y=2; 228902:>3:r1=0; 3:r3=0; x=1; y=1; 32626 :>3:r1=1; 3:r3=1; x=2; y=1; 25462 :>3:r1=0; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=4867d1504e0b1c594b9643e48c015b80 Cycle=Fre SyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr005 No ACLwSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time aclwdrr005 2.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr006.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr006 "Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR" {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 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | lwsync | | lwz r3,0(r4) ; li r3,1 | li r3,1 | | ; stw r3,0(r4) | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr006 Allowed Histogram (21 states) 105 :>3:r1=1; 3:r3=0; x=1; y=1; 165 :>3:r1=0; 3:r3=0; x=2; y=2; 1251 :>3:r1=2; 3:r3=0; x=1; y=2; 503 :>3:r1=1; 3:r3=1; x=2; y=2; 334 :>3:r1=2; 3:r3=0; x=2; y=1; 13186 :>3:r1=1; 3:r3=0; x=1; y=2; 559 :>3:r1=2; 3:r3=1; x=2; y=2; 20139 :>3:r1=2; 3:r3=0; x=1; y=1; 13957 :>3:r1=0; 3:r3=1; x=2; y=2; 39804 :>3:r1=1; 3:r3=1; x=1; y=1; 32050 :>3:r1=0; 3:r3=0; x=1; y=2; 123174:>3:r1=2; 3:r3=1; x=1; y=2; 90370 :>3:r1=0; 3:r3=1; x=2; y=1; 54138 :>3:r1=0; 3:r3=0; x=2; y=1; 24372 :>3:r1=0; 3:r3=1; x=1; y=1; 18011 :>3:r1=0; 3:r3=1; x=1; y=2; 153744:>3:r1=2; 3:r3=1; x=1; y=1; 59989 :>3:r1=1; 3:r3=1; x=1; y=2; 183171:>3:r1=0; 3:r3=0; x=1; y=1; 24990 :>3:r1=1; 3:r3=1; x=2; y=1; 145988:>3:r1=2; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=7e01ecd8b2bc06ff5ba0d2b4e58340c6 Cycle=Fre LwSyncdWW Wse LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr006 No ACLwSyncdRR Safe=Fre Wse LwSyncdWW Time aclwdrr006 2.27 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr007.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr007 "Fre LwSyncdWW Wse Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | | lwz r3,0(r4) ; li r3,1 | | ; stw r3,0(r4) | | ; exists (x=2 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r9,2 _litmus_P1_1_: stw r9,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr007 Allowed Histogram (9 states) 3299 :>2:r1=2; 2:r3=0; x=1; 32507 :>2:r1=0; 2:r3=1; x=2; 86291 :>2:r1=1; 2:r3=1; x=2; 22481 :>2:r1=0; 2:r3=1; x=1; 244275:>2:r1=2; 2:r3=1; x=1; 320675:>2:r1=0; 2:r3=0; x=1; 141304:>2:r1=1; 2:r3=1; x=1; 143827:>2:r1=2; 2:r3=1; x=2; 5341 :>2:r1=0; 2:r3=0; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=ba17863040d25a62a648bb8030bf59fd Cycle=Fre LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr007 No ACLwSyncdRR Safe=Fre Wse LwSyncdWW Time aclwdrr007 1.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr008.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr008 "Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR" {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 | li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r8,0(r2) _litmus_P1_0_: li r11,1 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr008 Allowed Histogram (21 states) 4 :>0:r3=0; 3:r1=0; 3:r3=0; y=2; 411 :>0:r3=0; 3:r1=2; 3:r3=0; y=1; 2363 :>0:r3=0; 3:r1=2; 3:r3=1; y=2; 1919 :>0:r3=1; 3:r1=1; 3:r3=0; y=1; 14373 :>0:r3=0; 3:r1=1; 3:r3=1; y=1; 4109 :>0:r3=1; 3:r1=2; 3:r3=0; y=2; 6369 :>0:r3=0; 3:r1=0; 3:r3=1; y=2; 23346 :>0:r3=0; 3:r1=0; 3:r3=0; y=1; 65857 :>0:r3=1; 3:r1=1; 3:r3=1; y=2; 88428 :>0:r3=0; 3:r1=2; 3:r3=1; y=1; 40062 :>0:r3=0; 3:r1=0; 3:r3=1; y=1; 24483 :>0:r3=1; 3:r1=1; 3:r3=0; y=2; 18998 :>0:r3=1; 3:r1=0; 3:r3=0; y=2; 53038 :>0:r3=1; 3:r1=0; 3:r3=1; y=2; 205060:>0:r3=1; 3:r1=2; 3:r3=1; y=1; 71304 :>0:r3=1; 3:r1=2; 3:r3=1; y=2; 32223 :>0:r3=1; 3:r1=2; 3:r3=0; y=1; 43364 :>0:r3=1; 3:r1=0; 3:r3=1; y=1; 226960:>0:r3=1; 3:r1=0; 3:r3=0; y=1; 76045 :>0:r3=1; 3:r1=1; 3:r3=1; y=1; 1284 :>0:r3=0; 3:r1=1; 3:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 0:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=61bd93196401321b8fb91e15727e3c64 Cycle=Fre SyncdWR Fre LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr008 No ACLwSyncdRR Safe=Fre Wse SyncdWR LwSyncdWW Time aclwdrr008 2.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr009.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr009 "Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR" {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 | li r1,2 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | | lwz r3,0(r4) ; lwz r3,0(r2) | li r3,1 | | ; | stw r3,0(r4) | | ; exists (x=2 /\ y=2 /\ 0:r3=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_: lwz r10,0(r2) _litmus_P1_0_: li r11,2 _litmus_P1_1_: stw r11,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r10,1 _litmus_P1_4_: stw r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr009 Allowed Histogram (38 states) 39 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 7 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2; 28 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 1104 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1; 158 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 182 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 157 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 149 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 338 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2; 1607 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 6019 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 4387 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1; 3572 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1; 6182 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 4756 :>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2; 29239 :>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 8926 :>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 79768 :>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2; 35966 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 1630 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 42700 :>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 6259 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 32621 :>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 5567 :>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 5810 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 119397:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; 31505 :>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 60669 :>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 112080:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 42253 :>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 49581 :>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 96194 :>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 112093:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 5138 :>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 78012 :>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 3452 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 6266 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 6189 :>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ y=2 /\ 0:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=ab46080bf73ab92da49cdd6b27ede9b2 Cycle=Fre SyncsWR Fre LwSyncdWW Wse Rfe LwSyncdRR Relax aclwdrr009 No ACLwSyncdRR Safe=Fre Wse SyncsWR LwSyncdWW Time aclwdrr009 2.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr010.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr010 "Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y; 3:r2=y;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; lwsync | stw r1,0(r2) | lwsync | stw r1,0(r2) ; lwz r3,0(r4) | | lwz r3,0(r4) | ; exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: lwz r7,0(r9) _litmus_P0_1_: lwsync _litmus_P0_2_: lwz r8,0(r2) _litmus_P1_0_: li r9,1 _litmus_P1_1_: stw r9,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) _litmus_P3_0_: li r9,1 _litmus_P3_1_: stw r9,0(r2) Test aclwdrr010 Allowed Histogram (15 states) 3061 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 781 :>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 8925 :>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 6383 :>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 135648:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 40228 :>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 172797:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 34981 :>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 7721 :>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 37754 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 2265 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 109808:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 80800 :>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 32050 :>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 326798:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=8ce05c9f86d49b2adfd5546bd471aa44 Cycle=Fre Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr010 No ACLwSyncdRR Safe=Fre Time aclwdrr010 1.61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr011.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr011 "Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {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) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; sync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,1 | | | ; 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_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr011 Allowed Histogram (15 states) 114 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 4 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 121 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 3922 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 3858 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 50556 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 18994 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 40118 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 166516:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 213261:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 245820:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 101497:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3985 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 107423:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 43811 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=064d7a96bedb614c156f5bd3adf783d8 Cycle=Fre SyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr011 No ACLwSyncdRR Safe=Fre SyncdWW Time aclwdrr011 1.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr012.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr012 "Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; sync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,2 | | | ; stw r3,0(r2) | | | ; exists (y=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_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr012 Allowed Histogram (33 states) 1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 2 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 27 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 32 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 9 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 12 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 74 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 240 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 644 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 3449 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 8288 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 1639 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 26920 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 5781 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 1635 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 659 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 27228 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 21102 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 10756 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 6027 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 25178 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 21064 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 52313 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 28192 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 96262 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 26458 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 2868 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 94874 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 107649:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 136721:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 12672 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 189021:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 92203 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=992754280de579a7f5feb516274ac846 Cycle=Fre SyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr012 No ACLwSyncdRR Safe=Fre SyncsWW Time aclwdrr012 2.32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr013.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr013 "Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {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) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,1 | | | ; stw r3,0(r4) | | | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr013 Allowed Histogram (15 states) 17 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 188 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 785 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 649 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 6551 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 21751 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 20883 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 74384 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 82948 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 137794:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 212339:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 215713:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 30693 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 180064:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 15241 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=4eddb3c8ea9ccf8a71927b2e31094cad Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr013 No ACLwSyncdRR Safe=Fre LwSyncdWW Time aclwdrr013 1.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr014.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr014 "Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | | lwz r3,0(r4) ; li r3,2 | | | ; stw r3,0(r2) | | | ; exists (y=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_: lwsync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr014 Allowed Histogram (30 states) 1 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 18 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 106 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 40 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 426 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 3200 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 469 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 579 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 7883 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 2324 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1111 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 3823 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 1699 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 2821 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 10109 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 548 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 4267 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 720 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 15465 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 85744 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 29713 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 2862 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 8593 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 106678:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 68083 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 87270 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 80433 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 130843:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 312017:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 32155 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 1:r1=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=0363e525d1d5c107b6654781a780ef6a Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre Rfe LwSyncdRR Relax aclwdrr014 No ACLwSyncdRR Safe=Fre LwSyncsWW Time aclwdrr014 2.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr015.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr015 "Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR" {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 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; li r3,1 | lwz r3,0(r4) | | ; stw r3,0(r4) | | | ; exists (x=2 /\ 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_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr015 Allowed Histogram (15 states) 4 :>1:r3=0; 3:r1=0; 3:r3=0; x=2; 60 :>1:r3=0; 3:r1=1; 3:r3=1; x=2; 1078 :>1:r3=1; 3:r1=1; 3:r3=0; x=2; 1862 :>1:r3=0; 3:r1=1; 3:r3=0; x=1; 2208 :>1:r3=0; 3:r1=0; 3:r3=1; x=2; 33282 :>1:r3=0; 3:r1=0; 3:r3=0; x=1; 20526 :>1:r3=1; 3:r1=0; 3:r3=0; x=2; 22332 :>1:r3=1; 3:r1=1; 3:r3=0; x=1; 53233 :>1:r3=1; 3:r1=0; 3:r3=1; x=1; 53704 :>1:r3=0; 3:r1=1; 3:r3=1; x=1; 42499 :>1:r3=0; 3:r1=0; 3:r3=1; x=1; 317328:>1:r3=1; 3:r1=1; 3:r3=1; x=1; 233755:>1:r3=1; 3:r1=0; 3:r3=0; x=1; 168667:>1:r3=1; 3:r1=1; 3:r3=1; x=2; 49462 :>1:r3=1; 3:r1=0; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=61d664ae95ff6d97da76ebb37bc47ca3 Cycle=Fre SyncdWW Wse SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr015 No ACLwSyncdRR Safe=Fre Wse SyncdWW SyncdWR Time aclwdrr015 1.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr016.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr016 "Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR" {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 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | sync | | lwz r3,0(r4) ; li r3,1 | lwz r3,0(r4) | | ; stw r3,0(r4) | | | ; exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr016 Allowed Histogram (15 states) 19 :>1:r3=0; 3:r1=0; 3:r3=0; x=2; 1915 :>1:r3=1; 3:r1=1; 3:r3=0; x=2; 1121 :>1:r3=0; 3:r1=1; 3:r3=0; x=1; 9019 :>1:r3=1; 3:r1=1; 3:r3=0; x=1; 245 :>1:r3=0; 3:r1=1; 3:r3=1; x=2; 2580 :>1:r3=0; 3:r1=0; 3:r3=1; x=2; 28742 :>1:r3=0; 3:r1=1; 3:r3=1; x=1; 71405 :>1:r3=0; 3:r1=0; 3:r3=0; x=1; 51151 :>1:r3=1; 3:r1=0; 3:r3=0; x=2; 79160 :>1:r3=1; 3:r1=0; 3:r3=1; x=2; 160072:>1:r3=1; 3:r1=1; 3:r3=1; x=1; 93522 :>1:r3=0; 3:r1=0; 3:r3=1; x=1; 215423:>1:r3=1; 3:r1=0; 3:r3=0; x=1; 267519:>1:r3=1; 3:r1=1; 3:r3=1; x=2; 18107 :>1:r3=1; 3:r1=0; 3:r3=1; x=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=4947e9ed11cb60630be5b54900bf7b6c Cycle=Fre LwSyncdWW Wse SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr016 No ACLwSyncdRR Safe=Fre Wse SyncdWR LwSyncdWW Time aclwdrr016 1.98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr017.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr017 "Fre SyncdWR Fre Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | | lwz r3,0(r4) ; lwz r3,0(r4) | | ; exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r8,1 _litmus_P0_1_: stw r8,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r10,0(r2) _litmus_P1_0_: li r9,1 _litmus_P1_1_: stw r9,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr017 Allowed Histogram (7 states) 1443 :>0:r3=0; 2:r1=0; 2:r3=0; 65067 :>0:r3=1; 2:r1=1; 2:r3=0; 322534:>0:r3=1; 2:r1=0; 2:r3=0; 86911 :>0:r3=0; 2:r1=0; 2:r3=1; 62609 :>0:r3=1; 2:r1=0; 2:r3=1; 67356 :>0:r3=0; 2:r1=1; 2:r3=1; 394080:>0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=0dd8df1959f84e11508b32d374a44775 Cycle=Fre SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr017 No ACLwSyncdRR Safe=Fre SyncdWR Time aclwdrr017 1.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr018.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr018 "Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR" {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 | li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r4) | lwz r3,0(r4) | | ; exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r8,0(r2) _litmus_P1_0_: li r10,1 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr018 Allowed Histogram (15 states) 18 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0; 1512 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0; 1419 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0; 4383 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1; 232 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1; 56460 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; 31529 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; 34795 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; 42829 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; 21156 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; 61335 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; 219901:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; 265274:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; 28410 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; 230747:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (0:r3=0 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=3fed6cc74892902ab28df779672578f8 Cycle=Fre SyncdWR Fre SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr018 No ACLwSyncdRR Safe=Fre SyncdWR Time aclwdrr018 1.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr019.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr019 "Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR" {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 | li r1,2 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r2) | lwz r3,0(r4) | | ; exists (y=2 /\ 0:r3=1 /\ 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_: lwz r10,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr019 Allowed Histogram (30 states) 28 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 121 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 42 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 180 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 26 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 135 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 5131 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 1488 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1; 3254 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 938 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1; 1238 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 4779 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 12280 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1; 15956 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1; 37227 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 4850 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1; 6531 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 12840 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1; 77248 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1; 50668 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 5102 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1; 17483 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1; 135603:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 32160 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 47165 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 116110:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 62031 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1; 135927:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1; 149829:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 63630 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 0:r3=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=660c5e262906b3ab9066962d8bf69882 Cycle=Fre SyncsWR Fre SyncdWR Fre Rfe LwSyncdRR Relax aclwdrr019 No ACLwSyncdRR Safe=Fre SyncsWR SyncdWR Time aclwdrr019 2.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr020.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr020 "Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 3:r2=x; 3:r4=y;} 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) | lwsync ; sync | sync | | lwz r3,0(r4) ; lwz r3,0(r4) | lwz r3,0(r2) | | ; exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r8,0(r2) _litmus_P1_0_: li r9,1 _litmus_P1_1_: stw r9,0(r2) _litmus_P1_2_: sync _litmus_P1_3_: lwz r10,0(r2) _litmus_P2_0_: li r9,2 _litmus_P2_1_: stw r9,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr020 Allowed Histogram (41 states) 1 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 1 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 5 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; 22 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 82 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 174 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; 89 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 876 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 2199 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 67 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 1012 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1; 682 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 3008 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 1836 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 15355 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; 2749 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 1809 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; 38275 :>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 24198 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 6465 :>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 16133 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 11196 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 105847:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 19069 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; 29273 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 5448 :>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 21331 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 11101 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 47171 :>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 24895 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 10250 :>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 50296 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 81808 :>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 13725 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 474 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 84752 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 160675:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 139795:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 43074 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 16302 :>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 8480 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 0:r3=0 /\ 1:r3=1 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=bad92812900a1656a66221eff19f711e Cycle=Fre SyncdWR Fre SyncsWR Fre Rfe LwSyncdRR Relax aclwdrr020 No ACLwSyncdRR Safe=Fre SyncsWR SyncdWR Time aclwdrr020 2.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr021.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr021 "Fre SyncdWW Wse SyncdWW Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | lwz r3,0(r4) ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr021 Allowed Histogram (7 states) 333 :>2:r1=1; 2:r3=1; x=2; 1868 :>2:r1=1; 2:r3=0; x=1; 6381 :>2:r1=0; 2:r3=0; x=2; 220998:>2:r1=0; 2:r3=1; x=2; 254772:>2:r1=0; 2:r3=1; x=1; 202527:>2:r1=1; 2:r3=1; x=1; 313121:>2:r1=0; 2:r3=0; x=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=aeec733dac4af8be94573c9aff9d0c10 Cycle=Fre SyncdWW Wse SyncdWW Rfe LwSyncdRR Relax aclwdrr021 No ACLwSyncdRR Safe=Fre Wse SyncdWW Time aclwdrr021 1.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr022.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr022 "Fre LwSyncdWW Wse SyncdWW Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | sync | lwz r3,0(r4) ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr022 Allowed Histogram (7 states) 2973 :>2:r1=1; 2:r3=0; x=1; 15462 :>2:r1=0; 2:r3=0; x=2; 307936:>2:r1=0; 2:r3=1; x=2; 203800:>2:r1=0; 2:r3=1; x=1; 145460:>2:r1=1; 2:r3=1; x=1; 844 :>2:r1=1; 2:r3=1; x=2; 323525:>2:r1=0; 2:r3=0; x=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=fb989d16658311d76866354f8a671029 Cycle=Fre LwSyncdWW Wse SyncdWW Rfe LwSyncdRR Relax aclwdrr022 No ACLwSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time aclwdrr022 1.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr023.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr023 "Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync ; sync | lwz r3,0(r4) ; li r3,1 | ; stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) Test aclwdrr023 Allowed Histogram (3 states) 146770:>1:r1=1; 1:r3=1; 973589:>1:r1=0; 1:r3=0; 879641:>1:r1=0; 1:r3=1; No Witnesses Positive: 0, Negative: 2000000 Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated Hash=501f8f5a33589295352fe1de9678142b Cycle=Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr023 No ACLwSyncdRR Safe=Fre SyncdWW Time aclwdrr023 1.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr024.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr024 "Fre SyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr024 Allowed Histogram (15 states) 5 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 12 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 86 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 3 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 10285 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3882 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 5299 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 24518 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 155657:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 82755 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 123071:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 239139:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 201111:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 22232 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 131945:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=d941e505b27c9a2748aeb4651a9cb643 Cycle=Fre SyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr024 No ACLwSyncdRR Safe=Fre SyncdWW Time aclwdrr024 2.12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr025.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr025 "Fre SyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; 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_: lwsync _litmus_P1_2_: 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_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr025 Allowed Histogram (32 states) 1 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 5 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 7 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 32 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 29 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 9 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 47 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 41 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 18 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 1030 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 66 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 90 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 3926 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 463 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 2787 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 34447 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 65900 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 71167 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 46994 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 44657 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 104654:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 63200 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 97739 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 118394:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 9942 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 16404 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 86466 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 37059 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 28636 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 8321 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 36863 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 120606:>1:r1=2; 1:r3=1; 3:r1=0; 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=32b005fb973345d626b38029866e06f9 Cycle=Fre SyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr025 No ACLwSyncdRR Safe=Fre SyncsWW SyncdWW Time aclwdrr025 2.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr026.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr026 "Fre LwSyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr026 Allowed Histogram (14 states) 8 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 9 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 871 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 5279 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 6189 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 13596 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 148171:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 184779:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 128717:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 147170:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 81334 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 195478:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 65032 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 23367 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=7a7cbc5359389bdb4170629397f77be6 Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr026 No ACLwSyncdRR Safe=Fre SyncdWW LwSyncdWW Time aclwdrr026 2.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr027.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr027 "Fre LwSyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; 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_: lwsync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: sync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr027 Allowed Histogram (29 states) 2 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 1 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 6 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 13 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 39 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 161 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 23 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 195 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 3657 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 749 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 1359 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 4891 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 1195 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 24420 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 20804 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 1174 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 1320 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 3669 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 6907 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 52496 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 6297 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 69469 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 25403 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 77899 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 146436:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 161963:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 195794:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 81766 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 111892:>1:r1=2; 1:r3=0; 3:r1=0; 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=c2a2e1328465d78b88dcae553e33604e Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr027 No ACLwSyncdRR Safe=Fre SyncdWW LwSyncsWW Time aclwdrr027 2.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr028.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr028 "Fre SyncdWR Fre SyncdWW Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,1 | ; | stw r3,0(r4) | ; exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r8,1 _litmus_P0_1_: stw r8,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r10,0(r2) _litmus_P1_0_: li r10,1 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr028 Allowed Histogram (7 states) 4735 :>0:r3=0; 2:r1=0; 2:r3=0; 1805 :>0:r3=1; 2:r1=1; 2:r3=0; 238039:>0:r3=1; 2:r1=0; 2:r3=1; 364437:>0:r3=1; 2:r1=0; 2:r3=0; 179392:>0:r3=1; 2:r1=1; 2:r3=1; 1437 :>0:r3=0; 2:r1=1; 2:r3=1; 210155:>0:r3=0; 2:r1=0; 2:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=eebdc6b096cdd9c24f38c118593f06bb Cycle=Fre SyncdWR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr028 No ACLwSyncdRR Safe=Fre SyncdWW SyncdWR Time aclwdrr028 1.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr029.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr029 "Fre SyncsWR Fre SyncdWW Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | lwz r3,0(r4) ; lwz r3,0(r2) | li r3,1 | ; | stw r3,0(r4) | ; exists (y=2 /\ 0:r3=1 /\ 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_: lwz r10,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: sync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr029 Allowed Histogram (13 states) 8 :>0:r3=2; 2:r1=0; 2:r3=1; y=2; 1010 :>0:r3=1; 2:r1=1; 2:r3=2; y=1; 290 :>0:r3=2; 2:r1=1; 2:r3=2; y=2; 31520 :>0:r3=1; 2:r1=0; 2:r3=0; y=2; 10026 :>0:r3=1; 2:r1=0; 2:r3=2; y=1; 118398:>0:r3=1; 2:r1=0; 2:r3=0; y=1; 255842:>0:r3=1; 2:r1=0; 2:r3=2; y=2; 87773 :>0:r3=1; 2:r1=0; 2:r3=1; y=2; 15705 :>0:r3=2; 2:r1=0; 2:r3=2; y=2; 140037:>0:r3=2; 2:r1=0; 2:r3=0; y=2; 238419:>0:r3=1; 2:r1=1; 2:r3=1; y=1; 5667 :>0:r3=1; 2:r1=1; 2:r3=2; y=2; 95305 :>0:r3=1; 2:r1=0; 2:r3=1; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=4ab12861c7fd48307d5dbbb06073fa65 Cycle=Fre SyncsWR Fre SyncdWW Rfe LwSyncdRR Relax aclwdrr029 No ACLwSyncdRR Safe=Fre SyncsWR SyncdWW Time aclwdrr029 1.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr030.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr030 "Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; sync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; 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_: lwsync _litmus_P1_2_: 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_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr030 Allowed Histogram (65 states) 1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 2 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 5 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 166 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 5 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 9 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 416 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 8 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 5 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 32 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 478 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 402 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 30 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 62 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 426 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 3 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 1306 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 20 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 2029 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1016 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 382 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 580 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 625 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 4877 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 965 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 783 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 7264 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 2127 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 7606 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 4654 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 13 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 2956 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 18980 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 3141 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 234 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 4319 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 12684 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 9846 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 15509 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 18799 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 14187 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 17680 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 44815 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 50891 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 44498 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 49998 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 11402 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 55614 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1432 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 28253 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 1306 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 70281 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 35134 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 63454 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 13418 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 10047 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 2047 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 29084 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 28787 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 36549 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 13397 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 103012:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 40073 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 35579 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 76297 :>1:r1=2; 1:r3=2; 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=ee8538d5ca48a381e732df1d7c7a6726 Cycle=Fre SyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Relax aclwdrr030 No ACLwSyncdRR Safe=Fre SyncsWW Time aclwdrr030 3.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr031.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr031 "Fre LwSyncdWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR" {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) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; li r3,1 | | li r3,2 | ; stw r3,0(r4) | | stw r3,0(r2) | ; exists (y=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li 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_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr031 Allowed Histogram (33 states) 1 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 7 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 21 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 54 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; y=2; 144 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; y=2; 51 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 1004 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; y=2; 947 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 146 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; y=2; 1205 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; y=2; 10427 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; y=2; 3799 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 3100 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; y=2; 11879 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; y=2; 908 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 10567 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; y=2; 13080 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 140165:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 35956 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 19695 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; y=2; 2881 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; y=2; 12491 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 141055:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 59576 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; y=2; 78197 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 66227 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; y=2; 95130 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; y=2; 148581:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; y=2; 38601 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 5301 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; y=2; 41147 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; y=2; 57656 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 1:r1=1 /\ 1:r3=0 /\ 3:r1=2 /\ 3:r3=0) is NOT validated Hash=7e70701bff0ff65c82954a7448132407 Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Relax aclwdrr031 No ACLwSyncdRR Safe=Fre SyncsWW LwSyncdWW Time aclwdrr031 2.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr032.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr032 "Fre LwSyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | sync | lwz r3,0(r4) ; 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_: lwsync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: 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_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr032 Allowed Histogram (59 states) 3 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 2 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 2 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 14 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 115 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 22 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 2266 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 135 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 381 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 334 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 2394 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 184 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 127 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 41 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 63 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 340 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 464 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 192 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 121 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 1786 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 147 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 2254 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 469 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 2404 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 231 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 3305 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 482 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 254 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 4369 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 6330 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 7739 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 5888 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 552 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 17069 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 5515 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 4682 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 1327 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 13496 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 2793 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 49752 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 86708 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 14983 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 7121 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 44316 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 72049 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 10072 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 11047 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 8115 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 83800 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 72866 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 98862 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 2511 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 41051 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 43361 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 7606 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 73711 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 11345 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 148849:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 23583 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 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=74930e6bce52d51f9df9817f8385847f Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre SyncsWW Rfe LwSyncdRR Relax aclwdrr032 No ACLwSyncdRR Safe=Fre SyncsWW LwSyncsWW Time aclwdrr032 3.61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr033.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr033 "Fre SyncdWR Fre SyncsWW Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | sync | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,2 | ; | stw r3,0(r2) | ; exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r8,1 _litmus_P0_1_: stw r8,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r10,0(r2) _litmus_P1_0_: li r9,1 _litmus_P1_1_: stw r9,0(r2) _litmus_P1_2_: sync _litmus_P1_3_: li r11,2 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr033 Allowed Histogram (15 states) 2 :>0:r3=1; 2:r1=1; 2:r3=0; x=2; 39 :>0:r3=1; 2:r1=1; 2:r3=1; x=2; 2957 :>0:r3=0; 2:r1=0; 2:r3=0; x=2; 2797 :>0:r3=2; 2:r1=1; 2:r3=0; x=2; 61201 :>0:r3=0; 2:r1=1; 2:r3=1; x=2; 27095 :>0:r3=2; 2:r1=2; 2:r3=0; x=2; 63995 :>0:r3=1; 2:r1=2; 2:r3=1; x=2; 24903 :>0:r3=1; 2:r1=0; 2:r3=0; x=2; 82971 :>0:r3=0; 2:r1=0; 2:r3=1; x=2; 292473:>0:r3=2; 2:r1=0; 2:r3=0; x=2; 60793 :>0:r3=1; 2:r1=0; 2:r3=1; x=2; 6773 :>0:r3=2; 2:r1=0; 2:r3=1; x=2; 295504:>0:r3=2; 2:r1=2; 2:r3=1; x=2; 6036 :>0:r3=0; 2:r1=2; 2:r3=1; x=2; 72461 :>0:r3=2; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=9aeeb761b71ddabb3db56388750f2a1a Cycle=Fre SyncdWR Fre SyncsWW Rfe LwSyncdRR Relax aclwdrr033 No ACLwSyncdRR Safe=Fre SyncsWW SyncdWR Time aclwdrr033 1.61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr034.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr034 "Fre SyncdWW Wse LwSyncdWW Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | lwz r3,0(r4) ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr034 Allowed Histogram (7 states) 4965 :>2:r1=0; 2:r3=0; x=2; 3181 :>2:r1=1; 2:r3=0; x=1; 219349:>2:r1=0; 2:r3=1; x=2; 194243:>2:r1=0; 2:r3=1; x=1; 274810:>2:r1=1; 2:r3=1; x=1; 1313 :>2:r1=1; 2:r3=1; x=2; 302139:>2:r1=0; 2:r3=0; x=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=10939fdb629e01d3ec7a75f951037026 Cycle=Fre SyncdWW Wse LwSyncdWW Rfe LwSyncdRR Relax aclwdrr034 No ACLwSyncdRR Safe=Fre Wse SyncdWW LwSyncdWW Time aclwdrr034 1.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr035.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr035 "Fre LwSyncdWW Wse LwSyncdWW Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; lwsync | lwsync | lwz r3,0(r4) ; li r3,1 | li r3,1 | ; stw r3,0(r4) | stw r3,0(r4) | ; exists (x=2 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r10,1 _litmus_P0_1_: stw r10,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r11,1 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr035 Allowed Histogram (7 states) 2389 :>2:r1=1; 2:r3=0; x=1; 12474 :>2:r1=0; 2:r3=0; x=2; 288362:>2:r1=0; 2:r3=1; x=2; 294147:>2:r1=0; 2:r3=0; x=1; 283830:>2:r1=1; 2:r3=1; x=1; 2558 :>2:r1=1; 2:r3=1; x=2; 116240:>2:r1=0; 2:r3=1; x=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=b62ccd86d3f88c50d13b5221a86b68a5 Cycle=Fre LwSyncdWW Wse LwSyncdWW Rfe LwSyncdRR Relax aclwdrr035 No ACLwSyncdRR Safe=Fre Wse LwSyncdWW Time aclwdrr035 1.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr036.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr036 "Fre LwSyncdWW Rfe LwSyncdRR" {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) | lwsync ; lwsync | lwz r3,0(r4) ; li r3,1 | ; stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) Test aclwdrr036 Allowed Histogram (3 states) 335204:>1:r1=0; 1:r3=1; 697740:>1:r1=1; 1:r3=1; 967056:>1:r1=0; 1:r3=0; No Witnesses Positive: 0, Negative: 2000000 Condition exists (1:r1=1 /\ 1:r3=0) is NOT validated Hash=25520ac6610aa6339bae2caee0005d5b Cycle=Fre LwSyncdWW Rfe LwSyncdRR Relax aclwdrr036 No ACLwSyncdRR Safe=Fre LwSyncdWW Time aclwdrr036 1.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr037.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr037 "Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ; li r3,1 | | li r3,1 | ; stw r3,0(r4) | | stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P0_0_: li r11,1 _litmus_P0_1_: stw r11,0(r9) _litmus_P0_2_: lwsync _litmus_P0_3_: li r10,1 _litmus_P0_4_: stw r10,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr037 Allowed Histogram (15 states) 162 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 141 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 444 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 373 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 14010 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 7338 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 19605 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 156983:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 32762 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 132644:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 74675 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 170430:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 174999:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 162223:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 53211 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=e45e2fb06db799317c9d3aeed10f6d45 Cycle=Fre LwSyncdWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Relax aclwdrr037 No ACLwSyncdRR Safe=Fre LwSyncdWW Time aclwdrr037 2.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr038.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr038 "Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ; 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_: lwsync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r11,1 _litmus_P2_1_: stw r11,0(r9) _litmus_P2_2_: lwsync _litmus_P2_3_: li r10,1 _litmus_P2_4_: stw r10,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr038 Allowed Histogram (30 states) 3 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 16 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 5 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 23 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 328 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 152 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 218 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 126 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 10150 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 8550 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 2089 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 3628 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 18383 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 556 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 32132 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 793 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 4108 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 50140 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 6558 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 4813 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 393 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 14942 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 51648 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 132190:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 6019 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 172508:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 89018 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 150569:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 143395:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 96547 :>1:r1=2; 1:r3=0; 3:r1=0; 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=459d76f119641ec12aab94d071c86542 Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncdWW Rfe LwSyncdRR Relax aclwdrr038 No ACLwSyncdRR Safe=Fre LwSyncsWW LwSyncdWW Time aclwdrr038 2.40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr039.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr039 "Fre SyncdWR Fre LwSyncdWW Rfe LwSyncdRR" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,1 | ; | stw r3,0(r4) | ; exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r8,1 _litmus_P0_1_: stw r8,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r10,0(r2) _litmus_P1_0_: li r10,1 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr039 Allowed Histogram (7 states) 4029 :>0:r3=1; 2:r1=1; 2:r3=0; 12396 :>0:r3=0; 2:r1=0; 2:r3=0; 246702:>0:r3=0; 2:r1=0; 2:r3=1; 308973:>0:r3=1; 2:r1=0; 2:r3=0; 271370:>0:r3=1; 2:r1=1; 2:r3=1; 5659 :>0:r3=0; 2:r1=1; 2:r3=1; 150871:>0:r3=1; 2:r1=0; 2:r3=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=9adf86efa9ed99398ed262e7a29cb549 Cycle=Fre SyncdWR Fre LwSyncdWW Rfe LwSyncdRR Relax aclwdrr039 No ACLwSyncdRR Safe=Fre SyncdWR LwSyncdWW Time aclwdrr039 1.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr040.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr040 "Fre SyncsWR Fre LwSyncdWW Rfe LwSyncdRR" {0:r2=y; 1:r2=y; 1:r4=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | lwz r3,0(r4) ; lwz r3,0(r2) | li r3,1 | ; | stw r3,0(r4) | ; exists (y=2 /\ 0:r3=1 /\ 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_: lwz r10,0(r2) _litmus_P1_0_: li r10,2 _litmus_P1_1_: stw r10,0(r9) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,1 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr040 Allowed Histogram (13 states) 20 :>0:r3=2; 2:r1=0; 2:r3=1; y=2; 1430 :>0:r3=1; 2:r1=1; 2:r3=2; y=1; 1000 :>0:r3=2; 2:r1=1; 2:r3=2; y=2; 15340 :>0:r3=2; 2:r1=0; 2:r3=2; y=2; 10890 :>0:r3=1; 2:r1=0; 2:r3=2; y=1; 137113:>0:r3=1; 2:r1=0; 2:r3=0; y=1; 25550 :>0:r3=1; 2:r1=0; 2:r3=0; y=2; 128467:>0:r3=2; 2:r1=0; 2:r3=0; y=2; 250486:>0:r3=1; 2:r1=0; 2:r3=2; y=2; 74586 :>0:r3=1; 2:r1=0; 2:r3=1; y=2; 272720:>0:r3=1; 2:r1=1; 2:r3=1; y=1; 21481 :>0:r3=1; 2:r1=1; 2:r3=2; y=2; 60917 :>0:r3=1; 2:r1=0; 2:r3=1; y=1; No Witnesses Positive: 0, Negative: 1000000 Condition exists (y=2 /\ 0:r3=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=1a7c6d1dc4425965c5dae6a980780759 Cycle=Fre SyncsWR Fre LwSyncdWW Rfe LwSyncdRR Relax aclwdrr040 No ACLwSyncdRR Safe=Fre SyncsWR LwSyncdWW Time aclwdrr040 1.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr041.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr041 "Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW Rfe LwSyncdRR" {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) | lwsync | stw r1,0(r2) | lwsync ; lwsync | lwz r3,0(r4) | lwsync | lwz r3,0(r4) ; 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_: lwsync _litmus_P0_3_: li r11,2 _litmus_P0_4_: stw r11,0(r2) _litmus_P1_0_: lwz r7,0(r9) _litmus_P1_1_: lwsync _litmus_P1_2_: lwz r8,0(r2) _litmus_P2_0_: li r9,1 _litmus_P2_1_: stw r9,0(r2) _litmus_P2_2_: lwsync _litmus_P2_3_: li r11,2 _litmus_P2_4_: stw r11,0(r2) _litmus_P3_0_: lwz r7,0(r9) _litmus_P3_1_: lwsync _litmus_P3_2_: lwz r8,0(r2) Test aclwdrr041 Allowed Histogram (58 states) 1 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 1 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 1 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 12 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 9 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 23 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 15 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 148 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 16 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 63 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 20 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 42 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 87 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 39 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 273 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 209 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 140 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 244 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 177 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 69 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 741 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 1866 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 5546 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 537 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 6443 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 494 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 738 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 1260 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 936 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 2884 :>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 12575 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 4258 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 726 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 10461 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 4404 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 1308 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 4071 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 1232 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 648 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 10886 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 9555 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 18721 :>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 1544 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 1598 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 23291 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 7212 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 4130 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 7363 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 29051 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 40137 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 3192 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 52795 :>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 109972:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 6069 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 87193 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 55141 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 325564:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 143869:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; 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=f658f820f1d5e1aea992b078ad3de29c Cycle=Fre LwSyncsWW Rfe LwSyncdRR Fre LwSyncsWW Rfe LwSyncdRR Relax aclwdrr041 No ACLwSyncdRR Safe=Fre LwSyncsWW Time aclwdrr041 3.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/aclwdrr042.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC aclwdrr042 "Fre SyncdWR Fre LwSyncsWW Rfe LwSyncdRR" {0:r2=y; 0:r4=x; 1:r2=x; 2:r2=x; 2:r4=y;} P0 | P1 | P2 ; li r1,1 | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | stw r1,0(r2) | lwsync ; sync | lwsync | lwz r3,0(r4) ; lwz r3,0(r4) | li r3,2 | ; | stw r3,0(r2) | ; exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) Generated assembler _litmus_P0_0_: li r8,1 _litmus_P0_1_: stw r8,0(r9) _litmus_P0_2_: sync _litmus_P0_3_: lwz r10,0(r2) _litmus_P1_0_: li r9,1 _litmus_P1_1_: stw r9,0(r2) _litmus_P1_2_: lwsync _litmus_P1_3_: li r11,2 _litmus_P1_4_: stw r11,0(r2) _litmus_P2_0_: lwz r7,0(r9) _litmus_P2_1_: lwsync _litmus_P2_2_: lwz r8,0(r2) Test aclwdrr042 Allowed Histogram (14 states) 3 :>0:r3=1; 2:r1=1; 2:r3=1; x=2; 319 :>0:r3=2; 2:r1=1; 2:r3=0; x=2; 9747 :>0:r3=1; 2:r1=0; 2:r3=0; x=2; 9402 :>0:r3=2; 2:r1=1; 2:r3=1; x=2; 56092 :>0:r3=2; 2:r1=2; 2:r3=0; x=2; 7539 :>0:r3=1; 2:r1=2; 2:r3=1; x=2; 103119:>0:r3=0; 2:r1=0; 2:r3=1; x=2; 7213 :>0:r3=0; 2:r1=0; 2:r3=0; x=2; 38145 :>0:r3=1; 2:r1=0; 2:r3=1; x=2; 21937 :>0:r3=0; 2:r1=1; 2:r3=1; x=2; 299481:>0:r3=2; 2:r1=0; 2:r3=0; x=2; 338920:>0:r3=2; 2:r1=2; 2:r3=1; x=2; 28629 :>0:r3=0; 2:r1=2; 2:r3=1; x=2; 79454 :>0:r3=2; 2:r1=0; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 1000000 Condition exists (x=2 /\ 0:r3=0 /\ 2:r1=2 /\ 2:r3=0) is NOT validated Hash=9862f681ad48c0682ff709f0b167939f Cycle=Fre SyncdWR Fre LwSyncsWW Rfe LwSyncdRR Relax aclwdrr042 No ACLwSyncdRR Safe=Fre SyncdWR LwSyncsWW Time aclwdrr042 1.54 $Revision: 3163 $ Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 1000000 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 1 #endif #ifndef N_EXE #define N_EXE (4 < N ? 1 : 4 / N) #endif /* gcc options: -Wall -std=gnu99 */ /* barrier: user */ /* tread start/join: changing */ /* memory: indirect */ /* safer: false */ /* preload: true */ /* para: self */ /* changes: false */ /* speedcheck: false */ /* proc used: 4 */ GCCOPTS="-Wall -std=gnu99 " LITMUSOPTS= Wed Dec 23 18:59:00 CET 2009