Mon Jan 24 01:46:36 CST 2011 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X14.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X14 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | sync | lwsync ; | li r3,1 | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; 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_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _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 X14 Allowed Histogram (15 states) 23916094:>0:r1=0; 0:r4=0; y=1; z=1; 17728180:>0:r1=1; 0:r4=0; y=1; z=1; 5030559:>0:r1=0; 0:r4=1; y=1; z=1; 23972292:>0:r1=1; 0:r4=1; y=1; z=1; 15844313:>0:r1=0; 0:r4=0; y=2; z=1; 1607312:>0:r1=1; 0:r4=0; y=2; z=1; 18326569:>0:r1=0; 0:r4=1; y=2; z=1; 23963320:>0:r1=1; 0:r4=1; y=2; z=1; 30570183:>0:r1=0; 0:r4=0; y=1; z=2; 1391881:>0:r1=1; 0:r4=0; y=1; z=2; 16114242:>0:r1=0; 0:r4=1; y=1; z=2; 11419052:>0:r1=1; 0:r4=1; y=1; z=2; 2167113:>0:r1=0; 0:r4=0; y=2; z=2; 6795561:>0:r1=0; 0:r4=1; y=2; z=2; 1153329:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=74664d9800a1cc765c71acb315cf55f7 Observation X14 Never 0 200000000 Time X14 90.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 28697137:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 5470953:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 8548238:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 19950024:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 5431676:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 10455620:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 5457758:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 9020691:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 11047871:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 260263:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 12608550:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 19658632:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 5209760:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 12356887:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 45825940:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=08b576a9816ca91b136efc84cb8198fe Observation Y00 Never 0 200000000 Time Y00 81.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 27013722:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 5649919:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 9773393:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 20529623:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 5943562:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 11838332:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 5755214:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 8909450:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 10844577:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 301862:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 13141246:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 19569160:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 5021287:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 11231281:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 44477372:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=27be645f8ce747a8241695ecd5d12775 Observation Y01 Never 0 200000000 Time Y01 82.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14750970:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 15478016:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 776775:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 21858756:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 17636255:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 2941576:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 13470950:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 44511429:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 27224146:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 2529822:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 7693716:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 15597507:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 3033692:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 8345893:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 4150497:>0:r1=1; 0:r4=1; 2:r1=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is NOT validated Hash=e299ccd513ee6b40ffc1479736b6d80f Observation Y02 Never 0 200000000 Time Y02 86.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 41438259:>0:r1=0; 0:r4=0; y=1; 18639961:>0:r1=1; 0:r4=0; y=1; 537411:>0:r1=0; 0:r4=1; y=1; 49733196:>0:r1=1; 0:r4=1; y=1; 20209354:>0:r1=0; 0:r4=0; y=2; 27497682:>0:r1=0; 0:r4=1; y=2; 41944137:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=fbc1c062cf6f3291c2ce205045bcf85e Observation Y03 Never 0 200000000 Time Y03 58.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15944573:>0:r1=0; 0:r4=0; y=1; z=1; 12415353:>0:r1=1; 0:r4=0; y=1; z=1; 786528:>0:r1=0; 0:r4=1; y=1; z=1; 20539964:>0:r1=1; 0:r4=1; y=1; z=1; 14933046:>0:r1=0; 0:r4=0; y=2; z=1; 2259464:>0:r1=1; 0:r4=0; y=2; z=1; 10176453:>0:r1=0; 0:r4=1; y=2; z=1; 39826279:>0:r1=1; 0:r4=1; y=2; z=1; 24387798:>0:r1=0; 0:r4=0; y=1; z=2; 5007425:>0:r1=1; 0:r4=0; y=1; z=2; 10512005:>0:r1=0; 0:r4=1; y=1; z=2; 23881874:>0:r1=1; 0:r4=1; y=1; z=2; 3516639:>0:r1=0; 0:r4=0; y=2; z=2; 9116661:>0:r1=0; 0:r4=1; y=2; z=2; 6695938:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=00bb906e6b50e3e5b6bc490a41e163e4 Observation Y04 Never 0 200000000 Time Y04 91.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 26404989:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 2022492:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 9654103:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 16695164:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 15222988:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 14345045:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 982232:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 20550401:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 3668825:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 9253576:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 4782431:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 16835724:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 3864415:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 12482353:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 43235262:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=2d110167698039bf55def82743b120ef Observation Y05 Never 0 200000000 Time Y05 88.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15757715:>0:r1=0; 0:r4=0; y=1; z=1; 13715251:>0:r1=1; 0:r4=0; y=1; z=1; 1778231:>0:r1=0; 0:r4=1; y=1; z=1; 25950902:>0:r1=1; 0:r4=1; y=1; z=1; 17225064:>0:r1=0; 0:r4=0; y=2; z=1; 3051773:>0:r1=1; 0:r4=0; y=2; z=1; 12607490:>0:r1=0; 0:r4=1; y=2; z=1; 43168458:>0:r1=1; 0:r4=1; y=2; z=1; 23216555:>0:r1=0; 0:r4=0; y=1; z=2; 2271611:>0:r1=1; 0:r4=0; y=1; z=2; 8807520:>0:r1=0; 0:r4=1; y=1; z=2; 15636555:>0:r1=1; 0:r4=1; y=1; z=2; 3311332:>0:r1=0; 0:r4=0; y=2; z=2; 8615257:>0:r1=0; 0:r4=1; y=2; z=2; 4886286:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5519b7e18d61900b26b6e20148fd6e5b Observation Y06 Never 0 200000000 Time Y06 92.16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15388779:>0:r1=0; 0:r4=0; 1:r3=0; 28407318:>0:r1=0; 0:r4=1; 1:r3=0; 27602404:>0:r1=1; 0:r4=1; 1:r3=0; 46157772:>0:r1=0; 0:r4=0; 1:r3=1; 21664939:>0:r1=1; 0:r4=0; 1:r3=1; 1476961:>0:r1=0; 0:r4=1; 1:r3=1; 59301827:>0:r1=1; 0:r4=1; 1:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=75dc62611c83cbf21aa9273aa6a41b23 Observation Y07 Never 0 200000000 Time Y07 58.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11847174:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 1360238:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 11862615:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 32456565:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 18005528:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 17268675:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 1098143:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 21309434:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 2496293:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 6854394:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 4047643:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 27291316:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 6056229:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 14548921:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 23496832:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=6f98559c8174fdcd1fe2a621ad7dc8d2 Observation Y08 Never 0 200000000 Time Y08 89.55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 2413014:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 6980318:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 2888616:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 28408176:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 2776355:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 13159464:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 18385534:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 13406340:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 1989633:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 13120529:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 35131287:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 17573420:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 18281890:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 1753414:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 23732010:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=f9c57151a878a2fb7ca88a7241079b1d Observation Y09 Never 0 200000000 Time Y09 85.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13126694:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 1566947:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 13514757:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 34630429:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 20002157:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 20683354:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 2117552:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 24401930:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 2019844:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 6190417:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 2940836:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 27301746:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 3108624:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 12681596:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 15713117:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=d987b1dfa9ff6dbc9cfc5646bda90ed3 Observation Y10 Never 0 200000000 Time Y10 89.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 43417555:>0:r1=0; 0:r4=0; y=1; 21298973:>0:r1=1; 0:r4=0; y=1; 1488464:>0:r1=0; 0:r4=1; y=1; 62850579:>0:r1=1; 0:r4=1; y=1; 18335646:>0:r1=0; 0:r4=0; y=2; 28641599:>0:r1=0; 0:r4=1; y=2; 23967184:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5506d17360dcb64cbec742d67fe4340e Observation Y11 Never 0 200000000 Time Y11 59.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 19582209:>0:r1=0; 0:r4=0; y=1; z=1; 16383743:>0:r1=1; 0:r4=0; y=1; z=1; 1780939:>0:r1=0; 0:r4=1; y=1; z=1; 24830683:>0:r1=1; 0:r4=1; y=1; z=1; 11245275:>0:r1=0; 0:r4=0; y=2; z=1; 1077047:>0:r1=1; 0:r4=0; y=2; z=1; 10732144:>0:r1=0; 0:r4=1; y=2; z=1; 30856169:>0:r1=1; 0:r4=1; y=2; z=1; 26632328:>0:r1=0; 0:r4=0; y=1; z=2; 5797714:>0:r1=1; 0:r4=0; y=1; z=2; 14251972:>0:r1=0; 0:r4=1; y=1; z=2; 24928743:>0:r1=1; 0:r4=1; y=1; z=2; 2385310:>0:r1=0; 0:r4=0; y=2; z=2; 6364790:>0:r1=0; 0:r4=1; y=2; z=2; 3150934:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=e74570fa8cc4ed49e2bc7eb3e6efaadc Observation Y12 Never 0 200000000 Time Y12 91.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 28847739:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 2200350:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 13453385:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 19337531:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 18712083:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 17656434:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 1947571:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 25875128:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 2282393:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 6948741:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 2903942:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 12447847:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 1752668:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 11688611:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 33945577:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=d514c17376c3fe56c7da249e5154e952 Observation Y13 Never 0 200000000 Time Y13 89.23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 21737421:>0:r1=0; 0:r4=0; y=1; z=1; 17982720:>0:r1=1; 0:r4=0; y=1; z=1; 3395582:>0:r1=0; 0:r4=1; y=1; z=1; 31581816:>0:r1=1; 0:r4=1; y=1; z=1; 12792675:>0:r1=0; 0:r4=0; y=2; z=1; 1292193:>0:r1=1; 0:r4=0; y=2; z=1; 12394187:>0:r1=0; 0:r4=1; y=2; z=1; 32299991:>0:r1=1; 0:r4=1; y=2; z=1; 23760720:>0:r1=0; 0:r4=0; y=1; z=2; 2495795:>0:r1=1; 0:r4=0; y=1; z=2; 13238801:>0:r1=0; 0:r4=1; y=1; z=2; 16919456:>0:r1=1; 0:r4=1; y=1; z=2; 2211725:>0:r1=0; 0:r4=0; y=2; z=2; 5647905:>0:r1=0; 0:r4=1; y=2; z=2; 2249013:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=db5bc36ebd8ef1745e795c6bdf75e423 Observation Y14 Never 0 200000000 Time Y14 93.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 29335726:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 5381359:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 9252794:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 19698273:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 5562569:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 11172917:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 5437740:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 9039480:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 10917897:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 521893:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 12885148:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 19631480:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 5559348:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 12210747:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 43392629:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=11eec175e5c988e350ebfc54fd0e2c1c Observation Y15 Never 0 200000000 Time Y15 83.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 40940471:>0:r1=0; 0:r3=0; y=1; 18806020:>0:r1=1; 0:r3=0; y=1; 617266:>0:r1=0; 0:r3=1; y=1; 51500046:>0:r1=1; 0:r3=1; y=1; 21236688:>0:r1=0; 0:r3=0; y=2; 25534151:>0:r1=0; 0:r3=1; y=2; 41365358:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=8e9853ba7646212616eafb737d8e71e4 Observation Y16 Never 0 200000000 Time Y16 59.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 16032028:>0:r1=0; 0:r3=0; y=1; z=1; 12698965:>0:r1=1; 0:r3=0; y=1; z=1; 773053:>0:r1=0; 0:r3=1; y=1; z=1; 20767937:>0:r1=1; 0:r3=1; y=1; z=1; 14956683:>0:r1=0; 0:r3=0; y=2; z=1; 2063448:>0:r1=1; 0:r3=0; y=2; z=1; 10354977:>0:r1=0; 0:r3=1; y=2; z=1; 38083180:>0:r1=1; 0:r3=1; y=2; z=1; 23150382:>0:r1=0; 0:r3=0; y=1; z=2; 4770247:>0:r1=1; 0:r3=0; y=1; z=2; 10980502:>0:r1=0; 0:r3=1; y=1; z=2; 24615778:>0:r1=1; 0:r3=1; y=1; z=2; 3712973:>0:r1=0; 0:r3=0; y=2; z=2; 9980774:>0:r1=0; 0:r3=1; y=2; z=2; 7059073:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=5dde3da66b8fd3eb942a6c2fb7e9050b Observation Y17 Never 0 200000000 Time Y17 91.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 26666023:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 2447967:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 8803613:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 17017847:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 15707261:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 14790201:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 959363:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 20462366:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 3481800:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 8900364:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 5057823:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 16745263:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 3725851:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 12567651:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 42666607:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=abfe8f96fb73d61f24cd4ed25c4cbe36 Observation Y18 Never 0 200000000 Time Y18 89.08 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 18065995:>0:r1=0; 0:r3=0; y=1; z=1; 15016983:>0:r1=1; 0:r3=0; y=1; z=1; 2216118:>0:r1=0; 0:r3=1; y=1; z=1; 25819362:>0:r1=1; 0:r3=1; y=1; z=1; 16517967:>0:r1=0; 0:r3=0; y=2; z=1; 2653513:>0:r1=1; 0:r3=0; y=2; z=1; 13913074:>0:r1=0; 0:r3=1; y=2; z=1; 40780394:>0:r1=1; 0:r3=1; y=2; z=1; 24025950:>0:r1=0; 0:r3=0; y=1; z=2; 2233173:>0:r1=1; 0:r3=0; y=1; z=2; 8595483:>0:r1=0; 0:r3=1; y=1; z=2; 14502449:>0:r1=1; 0:r3=1; y=1; z=2; 2840676:>0:r1=0; 0:r3=0; y=2; z=2; 8119487:>0:r1=0; 0:r3=1; y=2; z=2; 4699376:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=a4ab8a1891a2982f2576f75c35f64825 Observation Y19 Never 0 200000000 Time Y19 92.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 17759582:>0:r1=0; 0:r3=0; 1:r3=0; 29977676:>0:r1=0; 0:r3=1; 1:r3=0; 24881661:>0:r1=1; 0:r3=1; 1:r3=0; 44596752:>0:r1=0; 0:r3=0; 1:r3=1; 23735158:>0:r1=1; 0:r3=0; 1:r3=1; 1615853:>0:r1=0; 0:r3=1; 1:r3=1; 57433318:>0:r1=1; 0:r3=1; 1:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=310ba9b87ba9c8abbb2cb09115abba03 Observation Y20 Never 0 200000000 Time Y20 57.77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11987364:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 1586327:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 11502450:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 33769208:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 18113594:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 18353497:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 862068:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 19549035:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 2594877:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 6594550:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 3768503:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 28309173:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 6742171:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 13410449:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 22856734:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=63a4ff1b2a8c61b6b9352662bce3e8c9 Observation Y21 Never 0 200000000 Time Y21 88.91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 2255897:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 6833761:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 3023511:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 26661814:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 3436281:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 13458904:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 16860343:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 13335105:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 2198839:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 13134221:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 33554745:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 19779094:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 21212155:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 1986159:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 22269171:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=8a2b1f87ebce2fea7bdd4e78ab49e198 Observation Y22 Never 0 200000000 Time Y22 86.85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 12810766:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 1844951:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 12775712:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 35969935:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 19575193:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 20734556:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 1456646:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 23370049:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 2137312:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 6313102:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 3238906:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 28124760:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 3145605:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 11823186:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 16679321:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=34f72841a6635924e4f6e89a17ea5886 Observation Y23 Never 0 200000000 Time Y23 88.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 44091071:>0:r1=0; 0:r3=0; y=1; 21309308:>0:r1=1; 0:r3=0; y=1; 1938054:>0:r1=0; 0:r3=1; y=1; 63260294:>0:r1=1; 0:r3=1; y=1; 15998872:>0:r1=0; 0:r3=0; y=2; 27642384:>0:r1=0; 0:r3=1; y=2; 25760017:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=967cc1d43171137af345c68503a9bda3 Observation Y24 Never 0 200000000 Time Y24 59.61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 19521322:>0:r1=0; 0:r3=0; y=1; z=1; 15628289:>0:r1=1; 0:r3=0; y=1; z=1; 2187818:>0:r1=0; 0:r3=1; y=1; z=1; 25665277:>0:r1=1; 0:r3=1; y=1; z=1; 10904107:>0:r1=0; 0:r3=0; y=2; z=1; 1063810:>0:r1=1; 0:r3=0; y=2; z=1; 10915990:>0:r1=0; 0:r3=1; y=2; z=1; 29628424:>0:r1=1; 0:r3=1; y=2; z=1; 26043745:>0:r1=0; 0:r3=0; y=1; z=2; 5645289:>0:r1=1; 0:r3=0; y=1; z=2; 14615232:>0:r1=0; 0:r3=1; y=1; z=2; 26006612:>0:r1=1; 0:r3=1; y=1; z=2; 2720538:>0:r1=0; 0:r3=0; y=2; z=2; 6108897:>0:r1=0; 0:r3=1; y=2; z=2; 3344650:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=67d202536303d5d116d23867165f4ed6 Observation Y25 Never 0 200000000 Time Y25 92.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 27941087:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 2609600:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 12812034:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 19145228:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 20051006:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 19367848:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 2393865:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 26018395:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 2293355:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 5941651:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 2887832:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 12334736:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 1931653:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 12185736:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 32085974:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=44ca19804af93c9cee9c0f6acff5a2b0 Observation Y26 Never 0 200000000 Time Y26 90.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14162050:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 18699459:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 15450809:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 3604295:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 1047885:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 13856537:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 20504221:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 44875384:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 27182783:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 2975184:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 2395354:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 7797177:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 8254260:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 15210808:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 3983794:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ad65804aeb1597ba714e2328512d7995 Observation Y27 Never 0 200000000 Time Y27 86.50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8654237:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 20010271:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 10651824:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 5253208:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 204965:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 8408224:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 14319218:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 47682194:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 25345928:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 5446644:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 3848023:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 9224155:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 10155280:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 24367163:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 6428666:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=ce1b4a24ee0901b9de433860bfb46080 Observation Y28 Never 0 200000000 Time Y28 75.74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9153581:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 20529008:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 10365983:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 4788643:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 255155:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 8839987:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 14998173:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 46337731:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 26063769:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 5646847:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 3701566:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 9626909:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 10972898:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 22984486:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 5735264:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=8bc55273b7032305e0142605023bce2d Observation Y29 Never 0 200000000 Time Y29 76.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13473149:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 18419054:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 14497949:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 3449522:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 1019996:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 13912817:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 21980811:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 44251771:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 25591980:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 3416218:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 2320542:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 8955264:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 8548194:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 15821718:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 4341015:>0:r1=1; 2:r1=1; 2:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=3e1573bf73b4fdef87461b3565d66b20 Observation Y30 Never 0 200000000 Time Y30 87.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13685591:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 17917798:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 15320909:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 3396572:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 928563:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 13680434:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 21209949:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 43959543:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 28563633:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 3220169:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 2444295:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 7910870:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 8393306:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 15276321:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 4092047:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=e6774eda20819c8f372129af64bca016 Observation Y31 Never 0 200000000 Time Y31 86.70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 25531106:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 4696086:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 8939880:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 21025772:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 1528019:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 11104259:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 5167579:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 8483364:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 9321107:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 466625:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 9418929:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 17723319:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 5477552:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 18028635:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 53087768:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=a577eb9c8f1d583ecead3fdf77525a1e Observation Y32 Never 0 200000000 Time Y32 73.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 23471121:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 5159597:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 9494357:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 22727679:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 1688847:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 11506586:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 6523788:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 9061523:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 9897472:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 584180:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 10549786:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 17487867:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 6148414:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 16906381:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 48792402:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=eea22bd3e2446126dd9b287b5df5faca Observation Y33 Never 0 200000000 Time Y33 72.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9957189:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 20092176:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 13366505:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 4567329:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 558110:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 9538836:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 18778727:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 49153188:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 25327832:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 5155610:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 1955153:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 9391095:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 10385145:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 16604210:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 5168895:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=49482953dd91da1bcee183b3b0b006b8 Observation Y34 Never 0 200000000 Time Y34 76.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9992722:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 20334315:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 14060519:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 5087948:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 459756:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 9442258:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 18237192:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 48671790:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 25713788:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 4720760:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 2046357:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 8576999:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 10219279:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 16958328:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 5477989:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=1ab190404386bf69014d12d891f99e7c Observation Y35 Never 0 200000000 Time Y35 76.05 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 Mon Jan 24 02:36:56 CST 2011