lun jan 24 12:31:14 CET 2011 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y00.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y00 "Rf*e DpAddrdR Fre LwSyncdWW Rf*e DpAddrdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | DIY01: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | xor r3,r1,r1 | lwsync ; lwzx r4,r3,r5 | li r3,1 | lwzx r4,r3,r5 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stwcx. r1,r0,r2 | stw r3,0(r4) ; bne DIY00 | | bne DIY01 | ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: xor 10,30,30 _litmus_P0_3_: lwzx 31,10,9 _litmus_P0_4_: stwcx. 30,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: LitDIY01: _litmus_P2_1_: lwarx 30,0,11 _litmus_P2_2_: xor 10,30,30 _litmus_P2_3_: lwzx 31,10,9 _litmus_P2_4_: stwcx. 30,0,11 _litmus_P2_5_: bne LitDIY01 Test Y00 Allowed Histogram (15 states) 96294707:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 13175330:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 39225181:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 87767078:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 13088965:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 38026946:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 17760772:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 39371714:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 38008672:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 1319562:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 51191844:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 87619324:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 17541064:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 50820263:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 208788578:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=08b576a9816ca91b136efc84cb8198fe Observation Y00 Never 0 800000000 Time Y00 179.04 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y01.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y01 "Rf*e DpAddrdR Fre LwSyncdWW Rf*e DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | DIY01: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | cmpw r1,r1 | lwsync ; lwzx r4,r3,r5 | li r3,1 | beq LC02 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | LC02: | stw r3,0(r4) ; bne DIY00 | | isync | ; | | lwz r3,0(r4) | ; | | stwcx. r1,r0,r2 | ; | | bne DIY01 | ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: xor 10,30,30 _litmus_P0_3_: lwzx 31,10,9 _litmus_P0_4_: stwcx. 30,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: LitDIY01: _litmus_P2_1_: lwarx 3,0,11 _litmus_P2_2_: cmpw 3,3 _litmus_P2_3_: beq LitLC02 _litmus_P2_4_: LitLC02: _litmus_P2_5_: isync _litmus_P2_6_: lwz 31,0(9) _litmus_P2_7_: stwcx. 3,0,11 _litmus_P2_8_: bne LitDIY01 Test Y01 Allowed Histogram (15 states) 88606029:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 12074722:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 37288860:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 80117898:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 12406335:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 35088179:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 14948945:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 38642235:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 37503063:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 1289267:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 49107800:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 95446505:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 20246095:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 57140341:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 220093726:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=27be645f8ce747a8241695ecd5d12775 Observation Y01 Never 0 800000000 Time Y01 178.65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y02.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y02 "Rf*e DpAddrdR Fre LwSyncdWW Rf*e DpCtrldW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | DIY01: | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | stwcx. r1,r0,r2 | lwsync ; lwzx r4,r3,r5 | li r3,1 | bne DIY01 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | cmpw r1,r1 | stw r3,0(r4) ; bne DIY00 | | beq LC02 | ; | | LC02: | ; | | li r3,1 | ; | | stw r3,0(r4) | ; exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: LitDIY01: _litmus_P2_1_: lwarx 3,0,11 _litmus_P2_2_: stwcx. 3,0,11 _litmus_P2_3_: bne LitDIY01 _litmus_P2_4_: cmpw 3,3 _litmus_P2_5_: beq LitLC02 _litmus_P2_6_: LitLC02: _litmus_P2_7_: li 30,1 _litmus_P2_8_: stw 30,0(9) Test Y02 Allowed Histogram (15 states) 70773030:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 48291030:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 4649970:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 94395797:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 61062283:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 9556388:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 47962259:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 173875423:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 93278544:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 12529891:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 39459613:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 82916955:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 7483441:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 35936167:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 17829209:>0:r1=1; 0:r4=1; 2:r1=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is NOT validated Hash=e299ccd513ee6b40ffc1479736b6d80f Observation Y02 Never 0 800000000 Time Y02 183.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y03.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y03 "Rf*e DpAddrdR Fre LwSyncdWW Wse LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 27,0,11 _litmus_P0_2_: xor 10,27,27 _litmus_P0_3_: lwzx 28,10,9 _litmus_P0_4_: stwcx. 27,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y03 Allowed Histogram (7 states) 223487902:>0:r1=0; 0:r4=0; y=1; 91460380:>0:r1=1; 0:r4=0; y=1; 11538992:>0:r1=0; 0:r4=1; y=1; 280338804:>0:r1=1; 0:r4=1; y=1; 93255710:>0:r1=0; 0:r4=0; y=2; 146206860:>0:r1=0; 0:r4=1; y=2; 153711352:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=fbc1c062cf6f3291c2ce205045bcf85e Observation Y03 Never 0 1000000000 Time Y03 127.22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y04.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y04 "Rf*e DpAddrdR Fre LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,2 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | lwsync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | | ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y04 Allowed Histogram (15 states) 75597097:>0:r1=0; 0:r4=0; y=1; z=1; 54092531:>0:r1=1; 0:r4=0; y=1; z=1; 4540221:>0:r1=0; 0:r4=1; y=1; z=1; 107323341:>0:r1=1; 0:r4=1; y=1; z=1; 52282955:>0:r1=0; 0:r4=0; y=2; z=1; 8381701:>0:r1=1; 0:r4=0; y=2; z=1; 41609744:>0:r1=0; 0:r4=1; y=2; z=1; 152385618:>0:r1=1; 0:r4=1; y=2; z=1; 93858466:>0:r1=0; 0:r4=0; y=1; z=2; 11145067:>0:r1=1; 0:r4=0; y=1; z=2; 49290721:>0:r1=0; 0:r4=1; y=1; z=2; 91894373:>0:r1=1; 0:r4=1; y=1; z=2; 8666066:>0:r1=0; 0:r4=0; y=2; z=2; 33086908:>0:r1=0; 0:r4=1; y=2; z=2; 15845191:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=00bb906e6b50e3e5b6bc490a41e163e4 Observation Y04 Never 0 800000000 Time Y04 211.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y05.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y05 "Rf*e DpAddrdR Fre LwSyncdWW Wse SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,2 | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | sync | lwsync ; lwzx r4,r3,r5 | li r3,1 | lwz r3,0(r4) | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | | stw r3,0(r4) ; bne DIY00 | | | ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test Y05 Allowed Histogram (15 states) 93460741:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 9599248:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 41349869:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 73828432:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 72915074:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 51657194:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 5314046:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 102071229:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 9764977:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 37471730:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 18996670:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 57800517:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 10428021:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 45395118:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 169947134:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=2d110167698039bf55def82743b120ef Observation Y05 Never 0 800000000 Time Y05 185.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y06.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y06 "Rf*e DpAddrdR Fre LwSyncdWW Wse SyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,2 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | sync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | | ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y06 Allowed Histogram (15 states) 85072748:>0:r1=0; 0:r4=0; y=1; z=1; 54362433:>0:r1=1; 0:r4=0; y=1; z=1; 7953421:>0:r1=0; 0:r4=1; y=1; z=1; 115599618:>0:r1=1; 0:r4=1; y=1; z=1; 56700608:>0:r1=0; 0:r4=0; y=2; z=1; 9197019:>0:r1=1; 0:r4=0; y=2; z=1; 48785434:>0:r1=0; 0:r4=1; y=2; z=1; 166199815:>0:r1=1; 0:r4=1; y=2; z=1; 84995239:>0:r1=0; 0:r4=0; y=1; z=2; 8425147:>0:r1=1; 0:r4=0; y=1; z=2; 39443304:>0:r1=0; 0:r4=1; y=1; z=2; 67174139:>0:r1=1; 0:r4=1; y=1; z=2; 7263622:>0:r1=0; 0:r4=0; y=2; z=2; 33231228:>0:r1=0; 0:r4=1; y=2; z=2; 15596225:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5519b7e18d61900b26b6e20148fd6e5b Observation Y06 Never 0 800000000 Time Y06 212.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y07.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y07 "Rf*e DpAddrdR Fre SyncdWR Fre LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | lwsync ; lwzx r4,r3,r5 | lwz r3,0(r4) | li r3,1 ; stwcx. r1,r0,r2 | | stw r3,0(r4) ; bne DIY00 | | ; exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 31,1 _litmus_P1_1_: stw 31,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 30,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: xor 10,30,30 _litmus_P0_3_: lwzx 31,10,9 _litmus_P0_4_: stwcx. 30,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y07 Allowed Histogram (7 states) 94995652:>0:r1=0; 0:r4=0; 1:r3=0; 136184323:>0:r1=0; 0:r4=1; 1:r3=0; 143778144:>0:r1=1; 0:r4=1; 1:r3=0; 224858650:>0:r1=0; 0:r4=0; 1:r3=1; 101938210:>0:r1=1; 0:r4=0; 1:r3=1; 16527909:>0:r1=0; 0:r4=1; 1:r3=1; 281717112:>0:r1=1; 0:r4=1; 1:r3=1; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=75dc62611c83cbf21aa9273aa6a41b23 Observation Y07 Never 0 1000000000 Time Y07 122.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y08.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y08 "Rf*e DpAddrdR Fre SyncdWR Fre LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | lwsync | lwsync ; lwzx r4,r3,r5 | lwz r3,0(r4) | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | | ; exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y08 Allowed Histogram (15 states) 48934104:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 8817731:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 39092201:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 132327206:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 79862735:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 67333724:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 6058130:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 108106101:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 7991054:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 30506959:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 14040043:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 103137689:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 15573427:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 46419644:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 91799252:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=6f98559c8174fdcd1fe2a621ad7dc8d2 Observation Y08 Never 0 800000000 Time Y08 186.79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y09.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y09 "Rf*e DpAddrdR Fre SyncdWR Fre SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,1 | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | sync | lwsync ; lwzx r4,r3,r5 | lwz r3,0(r4) | lwz r3,0(r4) | li r3,1 ; stwcx. r1,r0,r2 | | | stw r3,0(r4) ; bne DIY00 | | | ; exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 31,1 _litmus_P1_1_: stw 31,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: xor 10,30,30 _litmus_P0_3_: lwzx 31,10,9 _litmus_P0_4_: stwcx. 30,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test Y09 Allowed Histogram (15 states) 9571804:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 33052292:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 15841119:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 98505733:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 12328783:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 43107492:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 77546182:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 55767629:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 11046303:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 42203759:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 146509623:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 77136042:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 64124161:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 6658251:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 106600827:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=f9c57151a878a2fb7ca88a7241079b1d Observation Y09 Never 0 800000000 Time Y09 178.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y10.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y10 "Rf*e DpAddrdR Fre SyncdWR Fre SyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | sync | lwsync ; lwzx r4,r3,r5 | lwz r3,0(r4) | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | | ; exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y10 Allowed Histogram (15 states) 52688725:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 9671520:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 44169326:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 139756205:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 90395709:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 69213437:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 9374556:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 120944561:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 6449086:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 26367907:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 10885494:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 90645150:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 11442989:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 43676166:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 74319169:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=d987b1dfa9ff6dbc9cfc5646bda90ed3 Observation Y10 Never 0 800000000 Time Y10 186.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y11.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y11 "Rf*e DpAddrdR Fre SyncdWW Wse LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 27,0,11 _litmus_P0_2_: xor 10,27,27 _litmus_P0_3_: lwzx 28,10,9 _litmus_P0_4_: stwcx. 27,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y11 Allowed Histogram (7 states) 238346561:>0:r1=0; 0:r4=0; y=1; 94850081:>0:r1=1; 0:r4=0; y=1; 25556293:>0:r1=0; 0:r4=1; y=1; 299746047:>0:r1=1; 0:r4=1; y=1; 81145010:>0:r1=0; 0:r4=0; y=2; 133822677:>0:r1=0; 0:r4=1; y=2; 126533331:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5506d17360dcb64cbec742d67fe4340e Observation Y11 Never 0 1000000000 Time Y11 126.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y12.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y12 "Rf*e DpAddrdR Fre SyncdWW Wse LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,2 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | lwsync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | | ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y12 Allowed Histogram (15 states) 84100219:>0:r1=0; 0:r4=0; y=1; z=1; 60524509:>0:r1=1; 0:r4=0; y=1; z=1; 8505073:>0:r1=0; 0:r4=1; y=1; z=1; 123182825:>0:r1=1; 0:r4=1; y=1; z=1; 46096558:>0:r1=0; 0:r4=0; y=2; z=1; 7016401:>0:r1=1; 0:r4=0; y=2; z=1; 39438400:>0:r1=0; 0:r4=1; y=2; z=1; 130450535:>0:r1=1; 0:r4=1; y=2; z=1; 98266733:>0:r1=0; 0:r4=0; y=1; z=2; 12434632:>0:r1=1; 0:r4=0; y=1; z=2; 51457385:>0:r1=0; 0:r4=1; y=1; z=2; 92593894:>0:r1=1; 0:r4=1; y=1; z=2; 6709723:>0:r1=0; 0:r4=0; y=2; z=2; 27201173:>0:r1=0; 0:r4=1; y=2; z=2; 12021940:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=e74570fa8cc4ed49e2bc7eb3e6efaadc Observation Y12 Never 0 800000000 Time Y12 213.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y13.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y13 "Rf*e DpAddrdR Fre SyncdWW Wse SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,2 | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | sync | lwsync ; lwzx r4,r3,r5 | li r3,1 | lwz r3,0(r4) | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | | stw r3,0(r4) ; bne DIY00 | | | ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test Y13 Allowed Histogram (15 states) 95848746:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 10213539:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 50226734:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 80918773:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 82590734:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 57596137:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 9461519:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 122233341:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 7209764:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 28477315:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 12748638:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 50429573:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 8397559:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 41594430:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 142053198:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=d514c17376c3fe56c7da249e5154e952 Observation Y13 Never 0 800000000 Time Y13 185.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y14.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y14 "Rf*e DpAddrdR Fre SyncdWW Wse SyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,2 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | sync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | | ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y14 Allowed Histogram (15 states) 93783985:>0:r1=0; 0:r4=0; y=1; z=1; 60780845:>0:r1=1; 0:r4=0; y=1; z=1; 11936640:>0:r1=0; 0:r4=1; y=1; z=1; 134483514:>0:r1=1; 0:r4=1; y=1; z=1; 48972333:>0:r1=0; 0:r4=0; y=2; z=1; 7457194:>0:r1=1; 0:r4=0; y=2; z=1; 43591084:>0:r1=0; 0:r4=1; y=2; z=1; 138030157:>0:r1=1; 0:r4=1; y=2; z=1; 87731759:>0:r1=0; 0:r4=0; y=1; z=2; 9251488:>0:r1=1; 0:r4=0; y=1; z=2; 48378526:>0:r1=0; 0:r4=1; y=1; z=2; 76857729:>0:r1=1; 0:r4=1; y=1; z=2; 5307901:>0:r1=0; 0:r4=0; y=2; z=2; 23813770:>0:r1=0; 0:r4=1; y=2; z=2; 9623075:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=db5bc36ebd8ef1745e795c6bdf75e423 Observation Y14 Never 0 800000000 Time Y14 212.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y15.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y15 "Rf*e DpCtrlIsyncdR Fre LwSyncdWW Rf*e DpCtrlIsyncdR Fre LwSyncdWW" {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 ; DIY00: | li r1,1 | DIY02: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; cmpw r1,r1 | lwsync | cmpw r1,r1 | lwsync ; beq LC01 | li r3,1 | beq LC03 | li r3,1 ; LC01: | stw r3,0(r4) | LC03: | stw r3,0(r4) ; isync | | isync | ; lwz r3,0(r4) | | lwz r3,0(r4) | ; stwcx. r1,r0,r2 | | stwcx. r1,r0,r2 | ; bne DIY00 | | bne DIY02 | ; exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: cmpw 30,30 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 31,0(9) _litmus_P0_7_: stwcx. 30,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: LitDIY02: _litmus_P2_1_: lwarx 3,0,11 _litmus_P2_2_: cmpw 3,3 _litmus_P2_3_: beq LitLC03 _litmus_P2_4_: LitLC03: _litmus_P2_5_: isync _litmus_P2_6_: lwz 31,0(9) _litmus_P2_7_: stwcx. 3,0,11 _litmus_P2_8_: bne LitDIY02 Test Y15 Allowed Histogram (15 states) 82665128:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 11756186:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 36962716:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 87697734:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 11958970:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 35102746:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 17618598:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 36789980:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 34693556:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 1269527:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 55125263:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 87401423:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 17258467:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 53920670:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 229779036:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=11eec175e5c988e350ebfc54fd0e2c1c Observation Y15 Never 0 800000000 Time Y15 177.55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y16.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y16 "Rf*e DpCtrlIsyncdR Fre LwSyncdWW Wse LwSyncdWW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | lwsync | lwsync ; beq LC01 | li r3,1 | li r3,1 ; LC01: | stw r3,0(r4) | stw r3,0(r4) ; isync | | ; lwz r3,0(r4) | | ; stwcx. r1,r0,r2 | | ; bne DIY00 | | ; exists (y=2 /\ 0:r1=1 /\ 0:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y16 Allowed Histogram (7 states) 212753425:>0:r1=0; 0:r3=0; y=1; 84031956:>0:r1=1; 0:r3=0; y=1; 11353864:>0:r1=0; 0:r3=1; y=1; 298230149:>0:r1=1; 0:r3=1; y=1; 86416921:>0:r1=0; 0:r3=0; y=2; 144078759:>0:r1=0; 0:r3=1; y=2; 163134926:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=8e9853ba7646212616eafb737d8e71e4 Observation Y16 Never 0 1000000000 Time Y16 126.05 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y17.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y17 "Rf*e DpCtrlIsyncdR Fre LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW" {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 ; DIY00: | li r1,1 | li r1,2 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | lwsync | lwsync | lwsync ; beq LC01 | li r3,1 | li r3,1 | li r3,1 ; LC01: | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y17 Allowed Histogram (15 states) 73005859:>0:r1=0; 0:r3=0; y=1; z=1; 49643659:>0:r1=1; 0:r3=0; y=1; z=1; 4808102:>0:r1=0; 0:r3=1; y=1; z=1; 115947600:>0:r1=1; 0:r3=1; y=1; z=1; 46863234:>0:r1=0; 0:r3=0; y=2; z=1; 6762134:>0:r1=1; 0:r3=0; y=2; z=1; 41165553:>0:r1=0; 0:r3=1; y=2; z=1; 155397437:>0:r1=1; 0:r3=1; y=2; z=1; 89142332:>0:r1=0; 0:r3=0; y=1; z=2; 10636732:>0:r1=1; 0:r3=0; y=1; z=2; 49007480:>0:r1=0; 0:r3=1; y=1; z=2; 99300914:>0:r1=1; 0:r3=1; y=1; z=2; 7649971:>0:r1=0; 0:r3=0; y=2; z=2; 32837466:>0:r1=0; 0:r3=1; y=2; z=2; 17831527:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=5dde3da66b8fd3eb942a6c2fb7e9050b Observation Y17 Never 0 800000000 Time Y17 214.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y18.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y18 "Rf*e DpCtrlIsyncdR Fre LwSyncdWW Wse SyncdWR Fre LwSyncdWW" {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 ; DIY00: | li r1,1 | li r1,2 | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | lwsync | sync | lwsync ; beq LC01 | li r3,1 | lwz r3,0(r4) | li r3,1 ; LC01: | stw r3,0(r4) | | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test Y18 Allowed Histogram (15 states) 86839149:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 9288005:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 40091421:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 81484269:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 69785352:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 47212663:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 5129577:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 111940246:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 8504616:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 36048894:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 22011156:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 51740148:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 8813116:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 43083124:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 178028264:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=abfe8f96fb73d61f24cd4ed25c4cbe36 Observation Y18 Never 0 800000000 Time Y18 186.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y19.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y19 "Rf*e DpCtrlIsyncdR Fre LwSyncdWW Wse SyncdWW Wse LwSyncdWW" {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 ; DIY00: | li r1,1 | li r1,2 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | lwsync | sync | lwsync ; beq LC01 | li r3,1 | li r3,1 | li r3,1 ; LC01: | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y19 Allowed Histogram (15 states) 81396832:>0:r1=0; 0:r3=0; y=1; z=1; 49237170:>0:r1=1; 0:r3=0; y=1; z=1; 7876171:>0:r1=0; 0:r3=1; y=1; z=1; 126168484:>0:r1=1; 0:r3=1; y=1; z=1; 49965152:>0:r1=0; 0:r3=0; y=2; z=1; 7501898:>0:r1=1; 0:r3=0; y=2; z=1; 46561178:>0:r1=0; 0:r3=1; y=2; z=1; 172415584:>0:r1=1; 0:r3=1; y=2; z=1; 79351149:>0:r1=0; 0:r3=0; y=1; z=2; 8100510:>0:r1=1; 0:r3=0; y=1; z=2; 39163605:>0:r1=0; 0:r3=1; y=1; z=2; 76499343:>0:r1=1; 0:r3=1; y=1; z=2; 6133849:>0:r1=0; 0:r3=0; y=2; z=2; 31646434:>0:r1=0; 0:r3=1; y=2; z=2; 17982641:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=a4ab8a1891a2982f2576f75c35f64825 Observation Y19 Never 0 800000000 Time Y19 213.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y20.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y20 "Rf*e DpCtrlIsyncdR Fre SyncdWR Fre LwSyncdWW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | sync | lwsync ; beq LC01 | lwz r3,0(r4) | li r3,1 ; LC01: | | stw r3,0(r4) ; isync | | ; lwz r3,0(r4) | | ; stwcx. r1,r0,r2 | | ; bne DIY00 | | ; exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 31,1 _litmus_P1_1_: stw 31,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 30,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: cmpw 30,30 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 31,0(9) _litmus_P0_7_: stwcx. 30,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y20 Allowed Histogram (7 states) 90793780:>0:r1=0; 0:r3=0; 1:r3=0; 130289982:>0:r1=0; 0:r3=1; 1:r3=0; 154241854:>0:r1=1; 0:r3=1; 1:r3=0; 212406431:>0:r1=0; 0:r3=0; 1:r3=1; 92744093:>0:r1=1; 0:r3=0; 1:r3=1; 14870627:>0:r1=0; 0:r3=1; 1:r3=1; 304653233:>0:r1=1; 0:r3=1; 1:r3=1; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=310ba9b87ba9c8abbb2cb09115abba03 Observation Y20 Never 0 1000000000 Time Y20 121.65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y21.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y21 "Rf*e DpCtrlIsyncdR Fre SyncdWR Fre LwSyncdWW Wse LwSyncdWW" {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 ; DIY00: | li r1,1 | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | sync | lwsync | lwsync ; beq LC01 | lwz r3,0(r4) | li r3,1 | li r3,1 ; LC01: | | stw r3,0(r4) | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y21 Allowed Histogram (15 states) 46822069:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 7506337:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 37096250:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 139280880:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 74346236:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 61068213:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 5770142:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 118523924:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 7663188:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 29418625:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 15741074:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 95747432:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 14267364:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 45122483:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 101625783:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=63a4ff1b2a8c61b6b9352662bce3e8c9 Observation Y21 Never 0 800000000 Time Y21 187.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y22.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y22 "Rf*e DpCtrlIsyncdR Fre SyncdWR Fre SyncdWR Fre LwSyncdWW" {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 ; DIY00: | li r1,1 | li r1,1 | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | sync | sync | lwsync ; beq LC01 | lwz r3,0(r4) | lwz r3,0(r4) | li r3,1 ; LC01: | | | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 31,1 _litmus_P1_1_: stw 31,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: cmpw 30,30 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 31,0(9) _litmus_P0_7_: stwcx. 30,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test Y22 Allowed Histogram (15 states) 8777761:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 31040759:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 17539859:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 90990983:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 11498042:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 41488703:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 86740159:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 51516143:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 9139075:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 39108173:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 156436075:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 72365143:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 58438727:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 6374004:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 118546394:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=8a2b1f87ebce2fea7bdd4e78ab49e198 Observation Y22 Never 0 800000000 Time Y22 178.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y23.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y23 "Rf*e DpCtrlIsyncdR Fre SyncdWR Fre SyncdWW Wse LwSyncdWW" {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 ; DIY00: | li r1,1 | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | sync | sync | lwsync ; beq LC01 | lwz r3,0(r4) | li r3,1 | li r3,1 ; LC01: | | stw r3,0(r4) | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y23 Allowed Histogram (15 states) 49769736:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 7829533:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 41289508:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 148083752:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 82768106:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 60819656:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 8657121:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 132700949:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 6254346:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 25748955:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 12868174:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 85140133:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 10588716:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 42810007:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 84671308:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=34f72841a6635924e4f6e89a17ea5886 Observation Y23 Never 0 800000000 Time Y23 187.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y24.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y24 "Rf*e DpCtrlIsyncdR Fre SyncdWW Wse LwSyncdWW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | sync | lwsync ; beq LC01 | li r3,1 | li r3,1 ; LC01: | stw r3,0(r4) | stw r3,0(r4) ; isync | | ; lwz r3,0(r4) | | ; stwcx. r1,r0,r2 | | ; bne DIY00 | | ; exists (y=2 /\ 0:r1=1 /\ 0:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y24 Allowed Histogram (7 states) 225153703:>0:r1=0; 0:r3=0; y=1; 85093349:>0:r1=1; 0:r3=0; y=1; 24238274:>0:r1=0; 0:r3=1; y=1; 323252258:>0:r1=1; 0:r3=1; y=1; 75353677:>0:r1=0; 0:r3=0; y=2; 131066298:>0:r1=0; 0:r3=1; y=2; 135842441:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=967cc1d43171137af345c68503a9bda3 Observation Y24 Never 0 1000000000 Time Y24 126.95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y25.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y25 "Rf*e DpCtrlIsyncdR Fre SyncdWW Wse LwSyncdWW Wse LwSyncdWW" {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 ; DIY00: | li r1,1 | li r1,2 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | sync | lwsync | lwsync ; beq LC01 | li r3,1 | li r3,1 | li r3,1 ; LC01: | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y25 Allowed Histogram (15 states) 79818054:>0:r1=0; 0:r3=0; y=1; z=1; 53771652:>0:r1=1; 0:r3=0; y=1; z=1; 8324420:>0:r1=0; 0:r3=1; y=1; z=1; 134340735:>0:r1=1; 0:r3=1; y=1; z=1; 40597899:>0:r1=0; 0:r3=0; y=2; z=1; 5445983:>0:r1=1; 0:r3=0; y=2; z=1; 37019478:>0:r1=0; 0:r3=1; y=2; z=1; 133422673:>0:r1=1; 0:r3=1; y=2; z=1; 91115618:>0:r1=0; 0:r3=0; y=1; z=2; 11977452:>0:r1=1; 0:r3=0; y=1; z=2; 51520957:>0:r1=0; 0:r3=1; y=1; z=2; 105638255:>0:r1=1; 0:r3=1; y=1; z=2; 5921498:>0:r1=0; 0:r3=0; y=2; z=2; 26888702:>0:r1=0; 0:r3=1; y=2; z=2; 14196624:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=67d202536303d5d116d23867165f4ed6 Observation Y25 Never 0 800000000 Time Y25 215.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y26.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y26 "Rf*e DpCtrlIsyncdR Fre SyncdWW Wse SyncdWR Fre LwSyncdWW" {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 ; DIY00: | li r1,1 | li r1,2 | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | sync | sync | lwsync ; beq LC01 | li r3,1 | lwz r3,0(r4) | li r3,1 ; LC01: | stw r3,0(r4) | | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test Y26 Allowed Histogram (15 states) 88038839:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 9931913:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 47703123:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 90531870:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 77028183:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 52525695:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 8914785:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 134401491:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 6404921:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 27225874:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 14362687:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 44891720:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 6795368:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 39629844:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 151613687:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=44ca19804af93c9cee9c0f6acff5a2b0 Observation Y26 Never 0 800000000 Time Y26 186.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y27.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y27 "Rf*e DpCtrldW Wse LwSyncdWW Rf*e DpCtrlIsyncdR Fre LwSyncdWW" {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 ; DIY00: | li r1,2 | DIY02: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; stwcx. r1,r0,r2 | lwsync | cmpw r1,r1 | lwsync ; bne DIY00 | li r3,1 | beq LC03 | li r3,1 ; cmpw r1,r1 | stw r3,0(r4) | LC03: | stw r3,0(r4) ; beq LC01 | | isync | ; LC01: | | lwz r3,0(r4) | ; li r3,1 | | stwcx. r1,r0,r2 | ; stw r3,0(r4) | | bne DIY02 | ; exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 3,0,11 _litmus_P0_2_: stwcx. 3,0,11 _litmus_P0_3_: bne LitDIY00 _litmus_P0_4_: cmpw 3,3 _litmus_P0_5_: beq LitLC01 _litmus_P0_6_: LitLC01: _litmus_P0_7_: li 30,1 _litmus_P0_8_: stw 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: LitDIY02: _litmus_P2_1_: lwarx 28,0,11 _litmus_P2_2_: cmpw 28,28 _litmus_P2_3_: beq LitLC03 _litmus_P2_4_: LitLC03: _litmus_P2_5_: isync _litmus_P2_6_: lwz 30,0(9) _litmus_P2_7_: stwcx. 28,0,11 _litmus_P2_8_: bne LitDIY02 Test Y27 Allowed Histogram (15 states) 67576547:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 55440127:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 43714584:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 7910308:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 4726021:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 46582823:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 103637005:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 180302042:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 86193335:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 6493797:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 11626801:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 39457171:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 35435595:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 90397174:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 20506670:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ad65804aeb1597ba714e2328512d7995 Observation Y27 Never 0 800000000 Time Y27 183.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y28.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y28 "Rfe LwSyncdRW Wse LwSyncdWW Rf*e DpAddrdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r5=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | DIY00: ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwarx r1,r0,r2 ; | li r3,1 | lwsync | xor r3,r1,r1 ; | stw r3,0(r4) | li r3,1 | lwzx r4,r3,r5 ; | | stw r3,0(r4) | stwcx. r1,r0,r2 ; | | | bne DIY00 ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: lwsync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: LitDIY00: _litmus_P3_1_: lwarx 28,0,11 _litmus_P3_2_: xor 10,28,28 _litmus_P3_3_: lwzx 30,10,9 _litmus_P3_4_: stwcx. 28,0,11 _litmus_P3_5_: bne LitDIY00 _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y28 Allowed Histogram (15 states) 60136189:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 77673719:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 42305641:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 11874299:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 3705751:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 49001683:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 85381573:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 198457987:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 80443557:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 13241127:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 8898788:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 38729318:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 33146218:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 80474707:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 16529443:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=ce1b4a24ee0901b9de433860bfb46080 Observation Y28 Never 0 800000000 Time Y28 156.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y29.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y29 "Rfe LwSyncdRW Wse LwSyncdWW Rf*e DpCtrlIsyncdR Fre" {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,2 | DIY00: ; stw r1,0(r2) | lwsync | stw r1,0(r2) | lwarx r1,r0,r2 ; | li r3,1 | lwsync | cmpw r1,r1 ; | stw r3,0(r4) | li r3,1 | beq LC01 ; | | stw r3,0(r4) | LC01: ; | | | isync ; | | | lwz r3,0(r4) ; | | | stwcx. r1,r0,r2 ; | | | bne DIY00 ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: lwsync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: LitDIY00: _litmus_P3_1_: lwarx 28,0,11 _litmus_P3_2_: cmpw 28,28 _litmus_P3_3_: beq LitLC01 _litmus_P3_4_: LitLC01: _litmus_P3_5_: isync _litmus_P3_6_: lwz 30,0(9) _litmus_P3_7_: stwcx. 28,0,11 _litmus_P3_8_: bne LitDIY00 _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y29 Allowed Histogram (15 states) 56617166:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 69778724:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 38701914:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 10203624:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 3737069:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 48919360:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 91873024:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 205513080:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 74763909:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 11652352:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 8524835:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 38929513:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 33870707:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 87973897:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 18940826:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=8bc55273b7032305e0142605023bce2d Observation Y29 Never 0 800000000 Time Y29 156.22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y30.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y30 "Rf*e PodRW Wse LwSyncdWW Rf*e DpAddrdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,2 | DIY01: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; stwcx. r1,r0,r2 | lwsync | xor r3,r1,r1 | lwsync ; bne DIY00 | li r3,1 | lwzx r4,r3,r5 | li r3,1 ; li r3,1 | stw r3,0(r4) | stwcx. r1,r0,r2 | stw r3,0(r4) ; stw r3,0(r4) | | bne DIY01 | ; exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) Generated assembler _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 3,0,11 _litmus_P0_2_: stwcx. 3,0,11 _litmus_P0_3_: bne LitDIY00 _litmus_P0_4_: li 30,1 _litmus_P0_5_: stw 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: LitDIY01: _litmus_P2_1_: lwarx 28,0,11 _litmus_P2_2_: xor 10,28,28 _litmus_P2_3_: lwzx 30,10,9 _litmus_P2_4_: stwcx. 28,0,11 _litmus_P2_5_: bne LitDIY01 Test Y30 Allowed Histogram (15 states) 71082436:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 60967839:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 47932264:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 9254732:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 4584656:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 48122850:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 94747475:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 173437631:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 92913835:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 7425197:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 12774778:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 39470050:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 35978932:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 83311184:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 17996141:>0:r1=1; 2:r1=1; 2:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=3e1573bf73b4fdef87461b3565d66b20 Observation Y30 Never 0 800000000 Time Y30 183.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y31.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y31 "Rf*e PodRW Wse LwSyncdWW Rf*e DpCtrlIsyncdR Fre LwSyncdWW" {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 ; DIY00: | li r1,2 | DIY01: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; stwcx. r1,r0,r2 | lwsync | cmpw r1,r1 | lwsync ; bne DIY00 | li r3,1 | beq LC02 | li r3,1 ; li r3,1 | stw r3,0(r4) | LC02: | stw r3,0(r4) ; stw r3,0(r4) | | isync | ; | | lwz r3,0(r4) | ; | | stwcx. r1,r0,r2 | ; | | bne DIY01 | ; exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 3,0,11 _litmus_P0_2_: stwcx. 3,0,11 _litmus_P0_3_: bne LitDIY00 _litmus_P0_4_: li 30,1 _litmus_P0_5_: stw 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: LitDIY01: _litmus_P2_1_: lwarx 28,0,11 _litmus_P2_2_: cmpw 28,28 _litmus_P2_3_: beq LitLC02 _litmus_P2_4_: LitLC02: _litmus_P2_5_: isync _litmus_P2_6_: lwz 30,0(9) _litmus_P2_7_: stwcx. 28,0,11 _litmus_P2_8_: bne LitDIY01 Test Y31 Allowed Histogram (15 states) 67312165:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 56069391:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 43779069:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 8077599:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 4560650:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 45471510:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 102556413:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 181904437:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 86268029:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 6440864:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 11677003:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 38308608:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 35478070:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 91068050:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 21028142:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=e6774eda20819c8f372129af64bca016 Observation Y31 Never 0 800000000 Time Y31 183.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y32.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y32 "Rfe SyncdRR Fre LwSyncdWW Rf*e DpAddrdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r5=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | DIY00: ; stw r1,0(r2) | sync | stw r1,0(r2) | lwarx r1,r0,r2 ; | lwz r3,0(r4) | lwsync | xor r3,r1,r1 ; | | li r3,1 | lwzx r4,r3,r5 ; | | stw r3,0(r4) | stwcx. r1,r0,r2 ; | | | bne DIY00 ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 31,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P3_0_: LitDIY00: _litmus_P3_1_: lwarx 30,0,11 _litmus_P3_2_: xor 10,30,30 _litmus_P3_3_: lwzx 31,10,9 _litmus_P3_4_: stwcx. 30,0,11 _litmus_P3_5_: bne LitDIY00 _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y32 Allowed Histogram (15 states) 77332395:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 13771469:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 60177757:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 81947360:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 8209798:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 38243739:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 14051550:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 37586071:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 32112329:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 4188588:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 52668677:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 73422869:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 15195810:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 74835676:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 216255912:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=a577eb9c8f1d583ecead3fdf77525a1e Observation Y32 Never 0 800000000 Time Y32 149.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y33.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y33 "Rfe SyncdRR Fre LwSyncdWW Rf*e DpCtrlIsyncdR Fre" {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 | DIY00: ; stw r1,0(r2) | sync | stw r1,0(r2) | lwarx r1,r0,r2 ; | lwz r3,0(r4) | lwsync | cmpw r1,r1 ; | | li r3,1 | beq LC01 ; | | stw r3,0(r4) | LC01: ; | | | isync ; | | | lwz r3,0(r4) ; | | | stwcx. r1,r0,r2 ; | | | bne DIY00 ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 31,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P3_0_: LitDIY00: _litmus_P3_1_: lwarx 3,0,11 _litmus_P3_2_: cmpw 3,3 _litmus_P3_3_: beq LitLC01 _litmus_P3_4_: LitLC01: _litmus_P3_5_: isync _litmus_P3_6_: lwz 31,0(9) _litmus_P3_7_: stwcx. 3,0,11 _litmus_P3_8_: bne LitDIY00 _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y33 Allowed Histogram (15 states) 72677280:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 11772486:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 56917402:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 72351458:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 7831520:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 34803294:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 11386936:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 37172086:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 32206146:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 4331327:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 54226456:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 78863307:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 16721006:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 82467904:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 226271392:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=eea22bd3e2446126dd9b287b5df5faca Observation Y33 Never 0 800000000 Time Y33 147.97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y34.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y34 "Rfe SyncdRW Wse LwSyncdWW Rf*e DpAddrdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r5=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | DIY00: ; stw r1,0(r2) | sync | stw r1,0(r2) | lwarx r1,r0,r2 ; | li r3,1 | lwsync | xor r3,r1,r1 ; | stw r3,0(r4) | li r3,1 | lwzx r4,r3,r5 ; | | stw r3,0(r4) | stwcx. r1,r0,r2 ; | | | bne DIY00 ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: LitDIY00: _litmus_P3_1_: lwarx 28,0,11 _litmus_P3_2_: xor 10,28,28 _litmus_P3_3_: lwzx 30,10,9 _litmus_P3_4_: stwcx. 28,0,11 _litmus_P3_5_: bne LitDIY00 _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y34 Allowed Histogram (15 states) 64168645:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 82635209:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 41319205:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 13061624:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 5763575:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 52324100:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 87776726:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 211196449:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 73580551:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 12007154:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 6966377:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 36017498:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 30552303:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 68457926:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 14172658:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=49482953dd91da1bcee183b3b0b006b8 Observation Y34 Never 0 800000000 Time Y34 156.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y35.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y35 "Rfe SyncdRW Wse LwSyncdWW Rf*e DpCtrlIsyncdR Fre" {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,2 | DIY00: ; stw r1,0(r2) | sync | stw r1,0(r2) | lwarx r1,r0,r2 ; | li r3,1 | lwsync | cmpw r1,r1 ; | stw r3,0(r4) | li r3,1 | beq LC01 ; | | stw r3,0(r4) | LC01: ; | | | isync ; | | | lwz r3,0(r4) ; | | | stwcx. r1,r0,r2 ; | | | bne DIY00 ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: LitDIY00: _litmus_P3_1_: lwarx 28,0,11 _litmus_P3_2_: cmpw 28,28 _litmus_P3_3_: beq LitLC01 _litmus_P3_4_: LitLC01: _litmus_P3_5_: isync _litmus_P3_6_: lwz 30,0(9) _litmus_P3_7_: stwcx. 28,0,11 _litmus_P3_8_: bne LitDIY00 _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y35 Allowed Histogram (15 states) 60110211:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 74834245:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 38123094:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 11352031:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 5873473:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 53254194:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 94178113:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 218726325:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 68708446:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 10678619:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 6756631:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 36155334:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 31114852:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 74244129:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 15890303:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=1ab190404386bf69014d12d891f99e7c Observation Y35 Never 0 800000000 Time Y35 156.16 Revision 6782, version 3.00+1 Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 100000 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 1000 #endif #ifndef AVAIL #define AVAIL 0 #endif /* gcc options: -D_GNU_SOURCE -Wall -std=gnu99 -O -m32 -pthread */ /* barrier: user */ /* launch: changing */ /* cache: false */ /* call: false */ /* affinity: incr0 */ /* randomise_affinity: false */ /* prealloc: false */ /* memory: indirect */ /* safer: true */ /* preload: true */ /* para: self */ /* speedcheck: false */ /* proc used: 0 */ GCCOPTS="-D_GNU_SOURCE -Wall -std=gnu99 -O -m32 -pthread" LITMUSOPTS=-rm +ra lun jan 24 14:15:59 CET 2011