Raw log

Wed Dec 23 07:45:34 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) 71 :>3:r1=0; 3:r3=0; x=2; y=2; 234 :>3:r1=2; 3:r3=1; x=2; y=2; 245 :>3:r1=1; 3:r3=1; x=2; y=2; 13238 :>3:r1=2; 3:r3=0; x=1; y=2; 28293 :>3:r1=1; 3:r3=0; x=1; y=1; 43425 :>3:r1=1; 3:r3=0; x=1; y=2; 17715 :>3:r1=0; 3:r3=1; x=2; y=2; 12197 :>3:r1=2; 3:r3=0; x=2; y=1; 370130:>3:r1=0; 3:r3=0; x=1; y=2; 394316:>3:r1=0; 3:r3=0; x=2; y=1; 2839643:>3:r1=2; 3:r3=1; x=2; y=1; 1687846:>3:r1=1; 3:r3=1; x=1; y=1; 880230:>3:r1=2; 3:r3=1; x=1; y=2; 910109:>3:r1=1; 3:r3=1; x=1; y=2; 851326:>3:r1=0; 3:r3=1; x=1; y=2; 929092:>3:r1=2; 3:r3=0; x=1; y=1; 864080:>3:r1=0; 3:r3=1; x=1; y=1; 4410238:>3:r1=2; 3:r3=1; x=1; y=1; 4631227:>3:r1=0; 3:r3=0; x=1; y=1; 104164:>3:r1=1; 3:r3=1; x=2; y=1; 1012181:>3:r1=0; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 20000000 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 43.81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 733 :>3:r1=2; 3:r3=1; x=2; y=2; 888 :>3:r1=0; 3:r3=0; x=2; y=2; 10736 :>3:r1=2; 3:r3=0; x=1; y=2; 687 :>3:r1=1; 3:r3=1; x=2; y=2; 27602 :>3:r1=1; 3:r3=0; x=1; y=1; 34562 :>3:r1=2; 3:r3=0; x=2; y=1; 37225 :>3:r1=1; 3:r3=0; x=1; y=2; 495233:>3:r1=0; 3:r3=0; x=1; y=2; 56325 :>3:r1=0; 3:r3=1; x=2; y=2; 960038:>3:r1=2; 3:r3=0; x=1; y=1; 569615:>3:r1=0; 3:r3=1; x=1; y=2; 871281:>3:r1=1; 3:r3=1; x=1; y=2; 1097585:>3:r1=0; 3:r3=0; x=2; y=1; 3467983:>3:r1=2; 3:r3=1; x=1; y=1; 1524398:>3:r1=1; 3:r3=1; x=1; y=1; 1048706:>3:r1=2; 3:r3=1; x=1; y=2; 1561313:>3:r1=0; 3:r3=1; x=2; y=1; 579455:>3:r1=0; 3:r3=1; x=1; y=1; 3885198:>3:r1=0; 3:r3=0; x=1; y=1; 114239:>3:r1=1; 3:r3=1; x=2; y=1; 3656198:>3:r1=2; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 20000000 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 41.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13271 :>2:r1=0; 2:r3=0; x=2; 334654:>2:r1=2; 2:r3=1; x=2; 1376358:>2:r1=0; 2:r3=1; x=2; 2792857:>2:r1=2; 2:r3=0; x=1; 358688:>2:r1=1; 2:r3=1; x=2; 1789533:>2:r1=0; 2:r3=1; x=1; 6486851:>2:r1=0; 2:r3=0; x=1; 1808570:>2:r1=1; 2:r3=1; x=1; 5039218:>2:r1=2; 2:r3=1; x=1; No Witnesses Positive: 0, Negative: 20000000 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 27.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 452 :>0:r3=0; 3:r1=2; 3:r3=1; y=2; 558 :>0:r3=0; 3:r1=1; 3:r3=1; y=2; 156 :>0:r3=0; 3:r1=0; 3:r3=0; y=2; 12357 :>0:r3=1; 3:r1=2; 3:r3=0; y=2; 43692 :>0:r3=1; 3:r1=1; 3:r3=0; y=2; 41194 :>0:r3=0; 3:r1=0; 3:r3=1; y=2; 476006:>0:r3=1; 3:r1=1; 3:r3=1; y=2; 54404 :>0:r3=1; 3:r1=1; 3:r3=0; y=1; 91167 :>0:r3=0; 3:r1=1; 3:r3=1; y=1; 671649:>0:r3=1; 3:r1=0; 3:r3=0; y=2; 28197 :>0:r3=0; 3:r1=2; 3:r3=0; y=1; 1822682:>0:r3=0; 3:r1=0; 3:r3=1; y=1; 516747:>0:r3=1; 3:r1=2; 3:r3=1; y=2; 590575:>0:r3=0; 3:r1=0; 3:r3=0; y=1; 954264:>0:r3=1; 3:r1=0; 3:r3=1; y=2; 1666723:>0:r3=1; 3:r1=2; 3:r3=0; y=1; 2481666:>0:r3=0; 3:r1=2; 3:r3=1; y=1; 3432701:>0:r3=1; 3:r1=2; 3:r3=1; y=1; 4815259:>0:r3=1; 3:r1=0; 3:r3=0; y=1; 1567393:>0:r3=1; 3:r1=1; 3:r3=1; y=1; 732158:>0:r3=1; 3:r1=0; 3:r3=1; y=1; No Witnesses Positive: 0, Negative: 20000000 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 40.62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (39 states) 1 :>0:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 2811 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 402 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 542 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 253 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2; 2101 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 44119 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2; 926 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 1173 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 102 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 12279 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 5948 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 8713 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1; 106995:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 46001 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1; 296481:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 272591:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 353 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 185456:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2; 44253 :>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 790600:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 287021:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 68488 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 895394:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 1500812:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 1284440:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2; 3013706:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 278146:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 186577:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1; 594228:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 1026951:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 2331250:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 1202603:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 1031697:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; 1418694:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 905431:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; 1303469:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 497057:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 351936:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; No Witnesses Positive: 0, Negative: 20000000 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 50.87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 116 :>3:r1=0; 3:r3=0; x=2; y=2; 8974 :>3:r1=2; 3:r3=0; x=2; y=1; 2162 :>3:r1=2; 3:r3=1; x=2; y=2; 82886 :>3:r1=2; 3:r3=0; x=1; y=2; 51795 :>3:r1=1; 3:r3=0; x=1; y=1; 1934 :>3:r1=1; 3:r3=1; x=2; y=2; 38221 :>3:r1=0; 3:r3=1; x=2; y=2; 385729:>3:r1=0; 3:r3=0; x=2; y=1; 1565507:>3:r1=2; 3:r3=0; x=1; y=1; 678790:>3:r1=0; 3:r3=0; x=1; y=2; 824632:>3:r1=0; 3:r3=1; x=1; y=1; 1274130:>3:r1=1; 3:r3=1; x=1; y=2; 228081:>3:r1=1; 3:r3=0; x=1; y=2; 2093737:>3:r1=2; 3:r3=1; x=1; y=2; 1263323:>3:r1=0; 3:r3=1; x=2; y=1; 3324580:>3:r1=2; 3:r3=1; x=1; y=1; 638089:>3:r1=0; 3:r3=1; x=1; y=2; 1411040:>3:r1=1; 3:r3=1; x=1; y=1; 4010047:>3:r1=0; 3:r3=0; x=1; y=1; 131332:>3:r1=1; 3:r3=1; x=2; y=1; 1984895:>3:r1=2; 3:r3=1; x=2; y=1; No Witnesses Positive: 0, Negative: 20000000 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 40.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 37860 :>3:r1=1; 3:r3=0; x=1; y=1; 3382 :>3:r1=0; 3:r3=0; x=2; y=2; 6331 :>3:r1=1; 3:r3=1; x=2; y=2; 7493 :>3:r1=2; 3:r3=1; x=2; y=2; 33840 :>3:r1=2; 3:r3=0; x=2; y=1; 68291 :>3:r1=2; 3:r3=0; x=1; y=2; 396614:>3:r1=0; 3:r3=0; x=1; y=2; 201726:>3:r1=1; 3:r3=0; x=1; y=2; 1071152:>3:r1=2; 3:r3=0; x=1; y=1; 387111:>3:r1=1; 3:r3=1; x=2; y=1; 1518474:>3:r1=1; 3:r3=1; x=1; y=2; 952146:>3:r1=0; 3:r3=0; x=2; y=1; 1811116:>3:r1=2; 3:r3=1; x=1; y=2; 292638:>3:r1=0; 3:r3=1; x=1; y=1; 327627:>3:r1=0; 3:r3=1; x=1; y=2; 1275330:>3:r1=0; 3:r3=1; x=2; y=1; 3615047:>3:r1=2; 3:r3=1; x=2; y=1; 2965712:>3:r1=2; 3:r3=1; x=1; y=1; 3680998:>3:r1=0; 3:r3=0; x=1; y=1; 1224901:>3:r1=1; 3:r3=1; x=1; y=1; 122211:>3:r1=0; 3:r3=1; x=2; y=2; No Witnesses Positive: 0, Negative: 20000000 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 42.12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 134747:>2:r1=0; 2:r3=0; x=2; 1341503:>2:r1=2; 2:r3=0; x=1; 2298924:>2:r1=1; 2:r3=1; x=2; 5031774:>2:r1=2; 2:r3=1; x=1; 620523:>2:r1=0; 2:r3=1; x=1; 6368014:>2:r1=0; 2:r3=0; x=1; 1549074:>2:r1=1; 2:r3=1; x=1; 2028233:>2:r1=2; 2:r3=1; x=2; 627208:>2:r1=0; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 20000000 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 25.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 798 :>0:r3=0; 3:r1=0; 3:r3=0; y=2; 118381:>0:r3=1; 3:r1=1; 3:r3=0; y=1; 20080 :>0:r3=0; 3:r1=1; 3:r3=1; y=2; 155382:>0:r3=1; 3:r1=2; 3:r3=0; y=2; 21708 :>0:r3=0; 3:r1=2; 3:r3=1; y=2; 104976:>0:r3=0; 3:r1=0; 3:r3=1; y=2; 181318:>0:r3=0; 3:r1=1; 3:r3=1; y=1; 432072:>0:r3=1; 3:r1=1; 3:r3=0; y=2; 493437:>0:r3=0; 3:r1=0; 3:r3=0; y=1; 19767 :>0:r3=0; 3:r1=2; 3:r3=0; y=1; 1069779:>0:r3=1; 3:r1=1; 3:r3=1; y=2; 654757:>0:r3=1; 3:r1=0; 3:r3=0; y=2; 481618:>0:r3=1; 3:r1=0; 3:r3=1; y=2; 2076883:>0:r3=1; 3:r1=2; 3:r3=0; y=1; 1480827:>0:r3=1; 3:r1=2; 3:r3=1; y=2; 2190348:>0:r3=0; 3:r1=2; 3:r3=1; y=1; 1720626:>0:r3=0; 3:r1=0; 3:r3=1; y=1; 2639620:>0:r3=1; 3:r1=2; 3:r3=1; y=1; 4274236:>0:r3=1; 3:r1=0; 3:r3=0; y=1; 1382305:>0:r3=1; 3:r1=1; 3:r3=1; y=1; 481082:>0:r3=1; 3:r1=0; 3:r3=1; y=1; No Witnesses Positive: 0, Negative: 20000000 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 41.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 4419 :>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 4510 :>0:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 453 :>0:r3=2; 3:r1=2; 3:r3=1; x=1; y=2; 3725 :>0:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 29698 :>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=2; 27233 :>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=1; 209473:>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=1; 16088 :>0:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 3494 :>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 242114:>0:r3=1; 3:r1=2; 3:r3=0; x=1; y=1; 79 :>0:r3=2; 3:r1=0; 3:r3=1; x=1; y=2; 54280 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=1; 79467 :>0:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 16397 :>0:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 86069 :>0:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 536081:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=1; 364823:>0:r3=1; 3:r1=0; 3:r3=0; x=2; y=1; 206707:>0:r3=2; 3:r1=2; 3:r3=0; x=1; y=2; 316111:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 738922:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=2; 163693:>0:r3=1; 3:r1=0; 3:r3=2; x=2; y=1; 1326457:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=1; 147884:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=1; 270318:>0:r3=1; 3:r1=0; 3:r3=1; x=2; y=1; 1432590:>0:r3=2; 3:r1=0; 3:r3=0; x=1; y=2; 916312:>0:r3=1; 3:r1=0; 3:r3=2; x=1; y=2; 1099787:>0:r3=2; 3:r1=2; 3:r3=2; x=1; y=2; 1189472:>0:r3=1; 3:r1=1; 3:r3=1; x=1; y=1; 68316 :>0:r3=2; 3:r1=0; 3:r3=2; x=1; y=2; 111379:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=1; 2599714:>0:r3=1; 3:r1=2; 3:r3=2; x=1; y=2; 1399662:>0:r3=1; 3:r1=1; 3:r3=1; x=2; y=1; 769931:>0:r3=1; 3:r1=2; 3:r3=1; x=1; y=2; 2027562:>0:r3=1; 3:r1=0; 3:r3=0; x=1; y=1; 1725252:>0:r3=1; 3:r1=2; 3:r3=1; x=2; y=1; 119683:>0:r3=2; 3:r1=1; 3:r3=2; x=1; y=2; 920700:>0:r3=1; 3:r1=1; 3:r3=2; x=1; y=2; 771145:>0:r3=1; 3:r1=0; 3:r3=1; x=1; y=2; No Witnesses Positive: 0, Negative: 20000000 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 50.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 52877 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 140113:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 131242:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 65635 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 823001:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 78820 :>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 1353018:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 1852469:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 509675:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 1480536:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 2400126:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 6308999:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; 1861228:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 2595928:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 346333:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; No Witnesses Positive: 0, Negative: 20000000 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 30.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 80 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 1226 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 3718 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 173771:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 38384 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 1161504:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 174590:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 2417164:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 1339030:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 1082488:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 4627952:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 707918:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 4210631:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 1950549:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 2110995:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; No Witnesses Positive: 0, Negative: 20000000 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 35.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 26 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 1759 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 1089 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 288 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 1855 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 107584:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 55734 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 34139 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 287358:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 14784 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 11322 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 164582:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 87036 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 33129 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 50883 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 474687:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 355188:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 786860:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1382699:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 116763:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 505714:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 1089216:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 1279044:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1496845:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 1073291:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 1418464:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 963804:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 204857:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 2418151:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 1446762:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 3244305:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 891775:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; No Witnesses Positive: 0, Negative: 20000000 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 44.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 3950 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 4479 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 13046 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 178424:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 1027746:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 132243:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 422502:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 913476:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 2368072:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 3787034:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 4139105:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 1892125:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 628950:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 2881905:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 1606943:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; No Witnesses Positive: 0, Negative: 20000000 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 34.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (32 states) 1 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 20 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 9 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 1273 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 4715 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 1264 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 38795 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 6162 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 122260:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 118188:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 72219 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 37373 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 45072 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 14147 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 13386 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 96327 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 662935:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 179152:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 67619 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 525071:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 1327022:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 46899 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 191806:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 1990257:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 1332105:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 342757:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 1537899:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1612035:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 153830:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 2293890:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 5416425:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1749087:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; No Witnesses Positive: 0, Negative: 20000000 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 43.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 93 :>1:r3=0; 3:r1=0; 3:r3=0; x=2; 790 :>1:r3=0; 3:r1=1; 3:r3=1; x=2; 63725 :>1:r3=0; 3:r1=1; 3:r3=0; x=1; 21470 :>1:r3=0; 3:r1=0; 3:r3=1; x=2; 708823:>1:r3=0; 3:r1=0; 3:r3=0; x=1; 1030380:>1:r3=0; 3:r1=1; 3:r3=1; x=1; 4813580:>1:r3=1; 3:r1=1; 3:r3=1; x=1; 1462347:>1:r3=1; 3:r1=0; 3:r3=1; x=2; 481263:>1:r3=1; 3:r1=0; 3:r3=0; x=2; 103427:>1:r3=1; 3:r1=1; 3:r3=0; x=2; 2037825:>1:r3=1; 3:r1=1; 3:r3=0; x=1; 1373997:>1:r3=0; 3:r1=0; 3:r3=1; x=1; 4516882:>1:r3=1; 3:r1=0; 3:r3=0; x=1; 2737113:>1:r3=1; 3:r1=1; 3:r3=1; x=2; 648285:>1:r3=1; 3:r1=0; 3:r3=1; x=1; No Witnesses Positive: 0, Negative: 20000000 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 35.62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1741 :>1:r3=0; 3:r1=0; 3:r3=0; x=2; 4402 :>1:r3=0; 3:r1=1; 3:r3=1; x=2; 74521 :>1:r3=0; 3:r1=1; 3:r3=0; x=1; 74914 :>1:r3=0; 3:r1=0; 3:r3=1; x=2; 164797:>1:r3=1; 3:r1=1; 3:r3=0; x=2; 1394472:>1:r3=1; 3:r1=1; 3:r3=0; x=1; 1289502:>1:r3=1; 3:r1=0; 3:r3=0; x=2; 863823:>1:r3=0; 3:r1=0; 3:r3=0; x=1; 1085672:>1:r3=0; 3:r1=1; 3:r3=1; x=1; 1509563:>1:r3=1; 3:r1=0; 3:r3=1; x=2; 322741:>1:r3=1; 3:r1=0; 3:r3=1; x=1; 3599574:>1:r3=1; 3:r1=1; 3:r3=1; x=1; 3743066:>1:r3=1; 3:r1=0; 3:r3=0; x=1; 4444414:>1:r3=1; 3:r1=1; 3:r3=1; x=2; 1426798:>1:r3=0; 3:r1=0; 3:r3=1; x=1; No Witnesses Positive: 0, Negative: 20000000 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 36.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 3256052:>0:r3=1; 2:r1=1; 2:r3=0; 1517191:>0:r3=0; 2:r1=0; 2:r3=1; 41300 :>0:r3=0; 2:r1=0; 2:r3=0; 1110041:>0:r3=1; 2:r1=0; 2:r3=1; 6422360:>0:r3=1; 2:r1=0; 2:r3=0; 1417327:>0:r3=0; 2:r1=1; 2:r3=1; 6235729:>0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 20000000 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 23.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 448 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=0; 48351 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=0; 56397 :>0:r3=0; 1:r3=0; 3:r1=0; 3:r3=1; 152541:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=0; 3819 :>0:r3=0; 1:r3=0; 3:r1=1; 3:r3=1; 651197:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; 2500169:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; 1762747:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; 1101254:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; 1444649:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; 3733268:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; 822791:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; 4321584:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; 2890621:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; 510164:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; No Witnesses Positive: 0, Negative: 20000000 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 36.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (31 states) 1 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 1981 :>0:r3=2; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 1091 :>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 33666 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=1; 121 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 139631:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 7935 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 432858:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; y=1; 45413 :>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=2; y=2; 25082 :>0:r3=2; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 59164 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=1; 436364:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=1; 2050 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 399560:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 1067520:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 5048 :>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 1504263:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; y=1; 546092:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=1; 142930:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=1; 454009:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=2; y=2; 1893779:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 1061037:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=2; y=2; 1352874:>0:r3=1; 1:r3=0; 3:r1=0; 3:r3=1; y=1; 1275478:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 1046792:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 88108 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=2; y=2; 2191653:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; y=1; 898870:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 323218:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=2; y=1; 1247183:>0:r3=1; 1:r3=0; 3:r1=1; 3:r3=1; y=1; 3316229:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=2; y=2; No Witnesses Positive: 0, Negative: 20000000 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 45.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (45 states) 3 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 1 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; 28 :>0:r3=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 12 :>0:r3=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 40 :>0:r3=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 8 :>0:r3=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 798 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 129 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; 3399 :>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 5863 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 216 :>0:r3=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; 25578 :>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; 24471 :>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 6087 :>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 5210 :>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; 192324:>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 22901 :>0:r3=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 62871 :>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 1055392:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; 402162:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=0; x=1; 650567:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 391706:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 190971:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 918059:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; 1676343:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=0; x=1; 225069:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 165205:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 439181:>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 156970:>0:r3=2; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 1076353:>0:r3=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; 195712:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; 1083396:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 168844:>0:r3=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 401983:>0:r3=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; 439797:>0:r3=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; 143360:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=1; x=1; 1027923:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; 1066716:>0:r3=1; 1:r3=1; 3:r1=2; 3:r3=1; x=1; 433302:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=0; x=2; 1668977:>0:r3=1; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 2645014:>0:r3=1; 1:r3=1; 3:r1=0; 3:r3=0; x=1; 2274713:>0:r3=2; 1:r3=1; 3:r1=2; 3:r3=1; x=2; 467924:>0:r3=2; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 237458:>0:r3=0; 1:r3=1; 3:r1=1; 3:r3=1; x=1; 46964 :>0:r3=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 20000000 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 48.05 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 55715 :>2:r1=1; 2:r3=0; x=1; 127993:>2:r1=0; 2:r3=0; x=2; 3549793:>2:r1=0; 2:r3=1; x=2; 6401391:>2:r1=0; 2:r3=0; x=1; 3300253:>2:r1=1; 2:r3=1; x=1; 10621 :>2:r1=1; 2:r3=1; x=2; 6554234:>2:r1=0; 2:r3=1; x=1; No Witnesses Positive: 0, Negative: 20000000 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 30.66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 55132 :>2:r1=1; 2:r3=0; x=1; 361610:>2:r1=0; 2:r3=0; x=2; 5417846:>2:r1=0; 2:r3=1; x=2; 6324545:>2:r1=0; 2:r3=0; x=1; 3588432:>2:r1=1; 2:r3=1; x=1; 21062 :>2:r1=1; 2:r3=1; x=2; 4231373:>2:r1=0; 2:r3=1; x=1; No Witnesses Positive: 0, Negative: 20000000 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 29.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 19151842:>1:r1=0; 1:r3=0; 3160018:>1:r1=1; 1:r3=1; 17688140:>1:r1=0; 1:r3=1; No Witnesses Positive: 0, Negative: 40000000 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 18.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 77 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 142 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 703 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 708 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 309810:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 125045:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 96086 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 1803675:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 2557855:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3024588:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 4123943:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 4862722:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 232461:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 428143:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 2434042:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; No Witnesses Positive: 0, Negative: 20000000 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 39.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 58 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 109 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 2768 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 1025 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 93 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 2675 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 1183 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 127 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 1067 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 1064 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 561 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 17012 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 65494 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 36583 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 656448:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 86937 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 920506:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 958676:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 159259:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 1548336:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 637398:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 443742:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 2464439:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 3273436:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 1281741:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 1710566:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 846737:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 599655:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 2590354:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 295073:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 684603:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 712275:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; No Witnesses Positive: 0, Negative: 20000000 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 49.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 395 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 402 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 1199 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 13438 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 103006:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 408230:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 515484:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 1910885:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 2475332:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 3716828:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 1760828:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 4249327:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 704357:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 716970:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; 3423319:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; No Witnesses Positive: 0, Negative: 20000000 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 39.46 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (32 states) 9 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 8 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 87 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 45 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 30 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 434 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 29 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 1426 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 1011 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 3372 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 2543 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 38414 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 17372 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 56153 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 55181 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 79642 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 98006 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 14587 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 272535:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 1294511:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 392505:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 1288415:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 1767099:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 59551 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 1518679:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 113186:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 2303453:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 105242:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 3793016:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 566288:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 1598523:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 4558648:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; No Witnesses Positive: 0, Negative: 20000000 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 46.66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 50207 :>0:r3=1; 2:r1=1; 2:r3=0; 243057:>0:r3=0; 2:r1=0; 2:r3=0; 4177415:>0:r3=0; 2:r1=0; 2:r3=1; 7453540:>0:r3=1; 2:r1=0; 2:r3=0; 2541621:>0:r3=1; 2:r1=1; 2:r3=1; 18207 :>0:r3=0; 2:r1=1; 2:r3=1; 5515953:>0:r3=1; 2:r1=0; 2:r3=1; No Witnesses Positive: 0, Negative: 20000000 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 29.23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 65 :>0:r3=2; 2:r1=0; 2:r3=1; y=2; 11680 :>0:r3=2; 2:r1=1; 2:r3=2; y=2; 35930 :>0:r3=1; 2:r1=1; 2:r3=2; y=1; 2343405:>0:r3=1; 2:r1=0; 2:r3=0; y=1; 724365:>0:r3=1; 2:r1=0; 2:r3=0; y=2; 244036:>0:r3=1; 2:r1=0; 2:r3=2; y=1; 2804233:>0:r3=2; 2:r1=0; 2:r3=0; y=2; 5449462:>0:r3=1; 2:r1=0; 2:r3=2; y=2; 2511570:>0:r3=1; 2:r1=0; 2:r3=1; y=1; 1301336:>0:r3=1; 2:r1=0; 2:r3=1; y=2; 4053075:>0:r3=1; 2:r1=1; 2:r3=1; y=1; 117531:>0:r3=1; 2:r1=1; 2:r3=2; y=2; 403312:>0:r3=2; 2:r1=0; 2:r3=2; y=2; No Witnesses Positive: 0, Negative: 20000000 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 28.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (71 states) 1 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 5 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 7 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 22 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 20 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 317 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 170 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 38 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 309 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 166 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 93 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 80 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 12 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 72 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 4526 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 128 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 150 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 327 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 3921 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 16090 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 5913 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 1249 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 4444 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 5739 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 25273 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 23593 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 8782 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 38301 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 67931 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 66959 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 290088:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 9280 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 51686 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 108816:>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 5589 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 41643 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 38261 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 57408 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 14055 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 182890:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 25517 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 580478:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 1167416:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 76038 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 419353:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 488482:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 196552:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 562649:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 146567:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 19690 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 1201384:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 12233 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 240476:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 167044:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 789347:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 643247:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 937700:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 249217:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 892039:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 170487:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 814018:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 970505:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 1120158:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 907054:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 329430:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 182392:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 702474:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 1181712:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 1156340:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1464644:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 1111003:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; No Witnesses Positive: 0, Negative: 20000000 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 82.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 2 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 127 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; y=2; 201 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 15268 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 375 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=1; y=2; 8305 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; y=2; 8963 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; y=2; 5394 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 2011 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; y=2; 2694 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 110741:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; y=2; 7093 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; y=2; 408 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; y=2; 79233 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; y=2; 237980:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; y=2; 776733:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; y=2; 1118113:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 393054:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; y=2; 984393:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; y=2; 1383096:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; y=2; 234880:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; y=2; 1530860:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; y=2; 425897:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; y=2; 1403157:>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; y=2; 1293147:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; y=2; 83668 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; y=2; 2543274:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; y=2; 524352:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; y=2; 703724:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; y=2; 627072:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; y=2; 2366742:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; y=2; 1057361:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; y=2; 2071682:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; y=2; No Witnesses Positive: 0, Negative: 20000000 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 48.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (69 states) 4 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 1 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 5 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 5 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 8 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 11 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 6 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 74 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 8 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 16 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 39 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 262 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 14 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 697 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 2840 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 10 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 4543 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 6626 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 2320 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 9940 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 3946 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 478 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 7940 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 5107 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 5484 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 4005 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 1334 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 18948 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 17214 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 10444 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 51665 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 9821 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 63447 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 5158 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 39985 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 105934:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 10805 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 22193 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 570792:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 32923 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 90152 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 25570 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 7521 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 113777:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 360217:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 183471:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 143021:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 830840:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 379681:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 856059:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 111043:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 112055:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 44483 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 200812:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 971520:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 1076303:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 111305:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 212886:>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 1437808:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 693077:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 2037803:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 1239854:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 17920 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 1579356:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1225097:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 1354292:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 381838:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 3070996:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 116191:>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; No Witnesses Positive: 0, Negative: 20000000 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 79.81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 73 :>0:r3=1; 2:r1=1; 2:r3=0; x=2; 556 :>0:r3=1; 2:r1=1; 2:r3=1; x=2; 87688 :>0:r3=0; 2:r1=0; 2:r3=0; x=2; 74510 :>0:r3=2; 2:r1=1; 2:r3=0; x=2; 846521:>0:r3=1; 2:r1=0; 2:r3=0; x=2; 1056069:>0:r3=0; 2:r1=1; 2:r3=1; x=2; 1430789:>0:r3=1; 2:r1=0; 2:r3=1; x=2; 1203161:>0:r3=1; 2:r1=2; 2:r3=1; x=2; 1240018:>0:r3=2; 2:r1=1; 2:r3=1; x=2; 1844061:>0:r3=0; 2:r1=0; 2:r3=1; x=2; 1049804:>0:r3=2; 2:r1=2; 2:r3=0; x=2; 125846:>0:r3=2; 2:r1=0; 2:r3=1; x=2; 5361386:>0:r3=2; 2:r1=2; 2:r3=1; x=2; 230941:>0:r3=0; 2:r1=2; 2:r3=1; x=2; 5448577:>0:r3=2; 2:r1=0; 2:r3=0; x=2; No Witnesses Positive: 0, Negative: 20000000 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 31.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 42232 :>2:r1=1; 2:r3=1; x=2; 59924 :>2:r1=0; 2:r3=0; x=2; 170389:>2:r1=1; 2:r3=0; x=1; 2905430:>2:r1=0; 2:r3=1; x=2; 4895171:>2:r1=0; 2:r3=1; x=1; 5755927:>2:r1=1; 2:r3=1; x=1; 6170927:>2:r1=0; 2:r3=0; x=1; No Witnesses Positive: 0, Negative: 20000000 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 30.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 111715:>2:r1=1; 2:r3=0; x=1; 269252:>2:r1=0; 2:r3=0; x=2; 2476197:>2:r1=0; 2:r3=1; x=1; 5389482:>2:r1=0; 2:r3=1; x=2; 5629343:>2:r1=1; 2:r3=1; x=1; 87918 :>2:r1=1; 2:r3=1; x=2; 6036093:>2:r1=0; 2:r3=0; x=1; No Witnesses Positive: 0, Negative: 20000000 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 30.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13967721:>1:r1=1; 1:r3=1; 19284699:>1:r1=0; 1:r3=0; 6747580:>1:r1=0; 1:r3=1; No Witnesses Positive: 0, Negative: 40000000 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 19.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11447 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 8129 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 2770 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 2281 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 345379:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 260146:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 734439:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 1940965:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 641320:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3175956:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3300567:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 1261644:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 3830932:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 3358560:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 1125465:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 20000000 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 39.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (32 states) 9 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 6 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 26 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 284 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 1196 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 2770 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 6364 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 2036 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; z=2; 11680 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 52913 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 15507 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 1928 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; z=2; 24091 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 15464 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 122794:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; z=2; 59225 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 101297:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 206407:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; z=2; 54442 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 63830 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; z=2; 330583:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 207920:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; z=2; 534962:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; z=2; 1251899:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; z=2; 1520763:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 337943:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 1987031:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 3580442:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; z=2; 3360422:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; z=2; 2006181:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; z=2; 2652279:>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; z=2; 1487306:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; z=2; No Witnesses Positive: 0, Negative: 20000000 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 47.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 318233:>0:r3=1; 2:r1=1; 2:r3=0; 246265:>0:r3=0; 2:r1=0; 2:r3=0; 4454767:>0:r3=0; 2:r1=0; 2:r3=1; 6620229:>0:r3=1; 2:r1=0; 2:r3=0; 4839319:>0:r3=1; 2:r1=1; 2:r3=1; 108895:>0:r3=0; 2:r1=1; 2:r3=1; 3412292:>0:r3=1; 2:r1=0; 2:r3=1; No Witnesses Positive: 0, Negative: 20000000 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 27.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 75 :>0:r3=2; 2:r1=0; 2:r3=1; y=2; 67574 :>0:r3=1; 2:r1=1; 2:r3=2; y=1; 534461:>0:r3=1; 2:r1=0; 2:r3=0; y=2; 37622 :>0:r3=2; 2:r1=1; 2:r3=2; y=2; 2628098:>0:r3=2; 2:r1=0; 2:r3=0; y=2; 402053:>0:r3=2; 2:r1=0; 2:r3=2; y=2; 1556481:>0:r3=1; 2:r1=0; 2:r3=1; y=1; 1030369:>0:r3=1; 2:r1=0; 2:r3=1; y=2; 5150756:>0:r3=1; 2:r1=0; 2:r3=2; y=2; 2658162:>0:r3=1; 2:r1=0; 2:r3=0; y=1; 4921077:>0:r3=1; 2:r1=1; 2:r3=1; y=1; 709877:>0:r3=1; 2:r1=1; 2:r3=2; y=2; 303395:>0:r3=1; 2:r1=0; 2:r3=2; y=1; No Witnesses Positive: 0, Negative: 20000000 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 28.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (65 states) 1 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 11 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 1 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 1 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 2 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=1; x=2; y=2; 7 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 18 :>1:r1=2; 1:r3=1; 3:r1=1; 3:r3=2; x=2; y=2; 3 :>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; x=2; y=2; 1019 :>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 15 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 345 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 1 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 231 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1431 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; x=2; y=2; 1082 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 2512 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 12082 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 1589 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=1; x=2; y=2; 1418 :>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=1; x=2; y=2; 419 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 621 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=0; x=2; y=2; 24007 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 753 :>1:r1=1; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 1254 :>1:r1=1; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 184967:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 7623 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; x=2; y=2; 5265 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 2115 :>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 6666 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=0; x=2; y=2; 27286 :>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 94510 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=1; x=2; y=2; 86132 :>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 11146 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; x=2; y=2; 12393 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 8858 :>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 83393 :>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 17298 :>1:r1=2; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 51690 :>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=0; x=2; y=2; 9071 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 112472:>1:r1=2; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 23203 :>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=1; x=2; y=2; 112332:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 12504 :>1:r1=0; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 1921 :>1:r1=1; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 160871:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=1; x=2; y=2; 36273 :>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 175285:>1:r1=2; 1:r3=1; 3:r1=0; 3:r3=2; x=2; y=2; 74585 :>1:r1=2; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 607870:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=0; x=2; y=2; 188411:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; x=2; y=2; 502585:>1:r1=2; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 1540768:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 867090:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; x=2; y=2; 179618:>1:r1=1; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 1476822:>1:r1=0; 1:r3=0; 3:r1=2; 3:r3=2; x=2; y=2; 316974:>1:r1=1; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 38316 :>1:r1=0; 1:r3=1; 3:r1=2; 3:r3=2; x=2; y=2; 182850:>1:r1=2; 1:r3=2; 3:r1=1; 3:r3=2; x=2; y=2; 2090742:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=2; x=2; y=2; 1376813:>1:r1=2; 1:r3=2; 3:r1=0; 3:r3=2; x=2; y=2; 260552:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; x=2; y=2; 398970:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=2; x=2; y=2; 1924016:>1:r1=0; 1:r3=2; 3:r1=0; 3:r3=0; x=2; y=2; 1418358:>1:r1=0; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; 5262563:>1:r1=2; 1:r3=2; 3:r1=2; 3:r3=2; x=2; y=2; No Witnesses Positive: 0, Negative: 20000000 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 82.32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 7 :>0:r3=1; 2:r1=1; 2:r3=0; x=2; 52 :>0:r3=1; 2:r1=1; 2:r3=1; x=2; 8876 :>0:r3=2; 2:r1=1; 2:r3=0; x=2; 143390:>0:r3=1; 2:r1=0; 2:r3=0; x=2; 484648:>0:r3=0; 2:r1=1; 2:r3=1; x=2; 110656:>0:r3=0; 2:r1=0; 2:r3=0; x=2; 742142:>0:r3=0; 2:r1=2; 2:r3=1; x=2; 224324:>0:r3=2; 2:r1=1; 2:r3=1; x=2; 438040:>0:r3=1; 2:r1=0; 2:r3=1; x=2; 1671209:>0:r3=0; 2:r1=0; 2:r3=1; x=2; 2125343:>0:r3=2; 2:r1=2; 2:r3=0; x=2; 1186311:>0:r3=2; 2:r1=0; 2:r3=1; x=2; 6450655:>0:r3=2; 2:r1=2; 2:r3=1; x=2; 239712:>0:r3=1; 2:r1=2; 2:r3=1; x=2; 6174635:>0:r3=2; 2:r1=0; 2:r3=0; x=2; No Witnesses Positive: 0, Negative: 20000000 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 30.44 $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=-r 20 Wed Dec 23 08:14:02 CET 2009