Mon Jan 24 10:14:42 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) 17122848:>0:r1=0; 0:r4=0; y=1; z=1; 16018737:>0:r1=1; 0:r4=0; y=1; z=1; 3832892:>0:r1=0; 0:r4=1; y=1; z=1; 37669855:>0:r1=1; 0:r4=1; y=1; z=1; 15764452:>0:r1=0; 0:r4=0; y=2; z=1; 22405 :>0:r1=1; 0:r4=0; y=2; z=1; 17802497:>0:r1=0; 0:r4=1; y=2; z=1; 28397768:>0:r1=1; 0:r4=1; y=2; z=1; 33307118:>0:r1=0; 0:r4=0; y=1; z=2; 14267 :>0:r1=1; 0:r4=0; y=1; z=2; 27944651:>0:r1=0; 0:r4=1; y=1; z=2; 1840889:>0:r1=1; 0:r4=1; y=1; z=2; 24458 :>0:r1=0; 0:r4=0; y=2; z=2; 228494:>0:r1=0; 0:r4=1; y=2; z=2; 8669 :>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 96.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33073472:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 44409 :>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 90410 :>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 31396290:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 42645 :>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 328564:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 2987399:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 153317:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 286597:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 150410:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 3930156:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 31098300:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 3195574:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 4009617:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 89212840:>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.79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33053676:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 44242 :>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 101968:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 31826884:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 42984 :>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 393677:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 2897234:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 128194:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 279648:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 146878:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 4034800:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 31050483:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 3243409:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 3905411:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 88850512:>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 81.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8371118:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 2021079:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 197658:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 28232424:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 22832040:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 1200580:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 3348416:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 74172423:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 33116783:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 23147 :>0:r1=1; 0:r4=0; 2:r1=0; z=2; 192580:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 11810332:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 30535 :>0:r1=0; 0:r4=0; 2:r1=1; z=2; 668338:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 13782547:>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 90.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 40435839:>0:r1=0; 0:r4=0; y=1; 21720719:>0:r1=1; 0:r4=0; y=1; 432792:>0:r1=0; 0:r4=1; y=1; 46155966:>0:r1=1; 0:r4=1; y=1; 23726356:>0:r1=0; 0:r4=0; y=2; 31929182:>0:r1=0; 0:r4=1; y=2; 35599146:>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 74.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 12645823:>0:r1=0; 0:r4=0; y=1; z=1; 3143590:>0:r1=1; 0:r4=0; y=1; z=1; 718811:>0:r1=0; 0:r4=1; y=1; z=1; 33087201:>0:r1=1; 0:r4=1; y=1; z=1; 17550571:>0:r1=0; 0:r4=0; y=2; z=1; 493242:>0:r1=1; 0:r4=0; y=2; z=1; 14267907:>0:r1=0; 0:r4=1; y=2; z=1; 33840351:>0:r1=1; 0:r4=1; y=2; z=1; 24582792:>0:r1=0; 0:r4=0; y=1; z=2; 49883 :>0:r1=1; 0:r4=0; y=1; z=2; 4091479:>0:r1=0; 0:r4=1; y=1; z=2; 37926419:>0:r1=1; 0:r4=1; y=1; z=2; 887916:>0:r1=0; 0:r4=0; y=2; z=2; 1975894:>0:r1=0; 0:r4=1; y=2; z=2; 14738121:>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 95.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32977561:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 20681 :>0:r1=1; 0:r4=0; 2:r3=0; y=1; 251415:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 16803014:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 10437567:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 2401389:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 773067:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 43305739:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 30635 :>0:r1=0; 0:r4=0; 2:r3=0; y=2; 808864:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 15118688:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 20894231:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 936274:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 13799119:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 41441756:>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 94.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8251609:>0:r1=0; 0:r4=0; y=1; z=1; 2217948:>0:r1=1; 0:r4=0; y=1; z=1; 952202:>0:r1=0; 0:r4=1; y=1; z=1; 48438000:>0:r1=1; 0:r4=1; y=1; z=1; 23078222:>0:r1=0; 0:r4=0; y=2; z=1; 1458341:>0:r1=1; 0:r4=0; y=2; z=1; 15245470:>0:r1=0; 0:r4=1; y=2; z=1; 45559598:>0:r1=1; 0:r4=1; y=2; z=1; 25925229:>0:r1=0; 0:r4=0; y=1; z=2; 29541 :>0:r1=1; 0:r4=0; y=1; z=2; 3014743:>0:r1=0; 0:r4=1; y=1; z=2; 15703801:>0:r1=1; 0:r4=1; y=1; z=2; 33157 :>0:r1=0; 0:r4=0; y=2; z=2; 585499:>0:r1=0; 0:r4=1; y=2; z=2; 9506640:>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 95.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 22780891:>0:r1=0; 0:r4=0; 1:r3=0; 30997749:>0:r1=0; 0:r4=1; 1:r3=0; 29116630:>0:r1=1; 0:r4=1; 1:r3=0; 42501662:>0:r1=0; 0:r4=0; 1:r3=1; 23572334:>0:r1=1; 0:r4=0; 1:r3=1; 399885:>0:r1=0; 0:r4=1; 1:r3=1; 50630849:>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 71.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15537916:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 14197 :>0:r1=1; 0:r4=0; 1:r3=0; z=1; 16113430:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 30546509:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 15391938:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 3999490:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 87415 :>0:r1=0; 0:r4=1; 1:r3=1; z=1; 34216371:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 633882:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 767724:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 28645 :>0:r1=1; 0:r4=1; 1:r3=0; z=2; 28103068:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 210596:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 3845718:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 50503101:>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 93.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 26936 :>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 67377 :>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 120839:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 33014044:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 21671 :>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 1004459:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 32171931:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 16170438:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 14551 :>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 16576811:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 33505459:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 15001387:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 3821670:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 315840:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 48166587:>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.65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 16323726:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 14201 :>0:r1=1; 0:r4=0; 1:r3=0; z=1; 16260424:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 31861935:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 15571298:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 3783709:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 411607:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 58158272:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 27316 :>0:r1=0; 0:r4=0; 1:r3=0; z=2; 67063 :>0:r1=0; 0:r4=1; 1:r3=0; z=2; 122237:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 28550735:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 26859 :>0:r1=1; 0:r4=0; 1:r3=1; z=2; 3011280:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 25809338:>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 94.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) 42831136:>0:r1=0; 0:r4=0; y=1; 22256525:>0:r1=1; 0:r4=0; y=1; 692672:>0:r1=0; 0:r4=1; y=1; 53546588:>0:r1=1; 0:r4=1; y=1; 21066034:>0:r1=0; 0:r4=0; y=2; 31949596:>0:r1=0; 0:r4=1; y=2; 27657449:>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 76.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15168571:>0:r1=0; 0:r4=0; y=1; z=1; 3870144:>0:r1=1; 0:r4=0; y=1; z=1; 357544:>0:r1=0; 0:r4=1; y=1; z=1; 38538127:>0:r1=1; 0:r4=1; y=1; z=1; 15276729:>0:r1=0; 0:r4=0; y=2; z=1; 14329 :>0:r1=1; 0:r4=0; y=2; z=1; 14346889:>0:r1=0; 0:r4=1; y=2; z=1; 27671264:>0:r1=1; 0:r4=1; y=2; z=1; 27300378:>0:r1=0; 0:r4=0; y=1; z=2; 157758:>0:r1=1; 0:r4=0; y=1; z=2; 5039244:>0:r1=0; 0:r4=1; y=1; z=2; 50196036:>0:r1=1; 0:r4=1; y=1; z=2; 909711:>0:r1=0; 0:r4=0; y=2; z=2; 1125718:>0:r1=0; 0:r4=1; y=2; z=2; 27558 :>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 96.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33206885:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 19340 :>0:r1=1; 0:r4=0; 2:r3=0; y=1; 639810:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 32300273:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 15312763:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 3333275:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 677132:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 52906622:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 26743 :>0:r1=0; 0:r4=0; 2:r3=0; y=2; 68320 :>0:r1=0; 0:r4=1; 2:r3=0; y=2; 148951:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 16186805:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 13676 :>0:r1=1; 0:r4=0; 2:r3=1; y=2; 13329805:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 31829600:>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 95.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15350021:>0:r1=0; 0:r4=0; y=1; z=1; 3717800:>0:r1=1; 0:r4=0; y=1; z=1; 718533:>0:r1=0; 0:r4=1; y=1; z=1; 62362374:>0:r1=1; 0:r4=1; y=1; z=1; 16183577:>0:r1=0; 0:r4=0; y=2; z=1; 13395 :>0:r1=1; 0:r4=0; y=2; z=1; 13877048:>0:r1=0; 0:r4=1; y=2; z=1; 31111679:>0:r1=1; 0:r4=1; y=2; z=1; 30487219:>0:r1=0; 0:r4=0; y=1; z=2; 28054 :>0:r1=1; 0:r4=0; y=1; z=2; 2160126:>0:r1=0; 0:r4=1; y=1; z=2; 23769751:>0:r1=1; 0:r4=1; y=1; z=2; 26609 :>0:r1=0; 0:r4=0; y=2; z=2; 64145 :>0:r1=0; 0:r4=1; y=2; z=2; 129669:>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 96.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33055330:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 43815 :>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 113771:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 31875107:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 44155 :>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 544787:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 2890574:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 154125:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 436328:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 150309:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 3775597:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 31382760:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 3069575:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 4316505:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 88147262:>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 81.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 41165454:>0:r1=0; 0:r3=0; y=1; 23380490:>0:r1=1; 0:r3=0; y=1; 411666:>0:r1=0; 0:r3=1; y=1; 44029202:>0:r1=1; 0:r3=1; y=1; 23887002:>0:r1=0; 0:r3=0; y=2; 31534349:>0:r1=0; 0:r3=1; y=2; 35591837:>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 74.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11473921:>0:r1=0; 0:r3=0; y=1; z=1; 2658187:>0:r1=1; 0:r3=0; y=1; z=1; 650431:>0:r1=0; 0:r3=1; y=1; z=1; 32402799:>0:r1=1; 0:r3=1; y=1; z=1; 19387274:>0:r1=0; 0:r3=0; y=2; z=1; 673714:>0:r1=1; 0:r3=0; y=2; z=1; 14432800:>0:r1=0; 0:r3=1; y=2; z=1; 34514902:>0:r1=1; 0:r3=1; y=2; z=1; 24057821:>0:r1=0; 0:r3=0; y=1; z=2; 56463 :>0:r1=1; 0:r3=0; y=1; z=2; 3949821:>0:r1=0; 0:r3=1; y=1; z=2; 38179188:>0:r1=1; 0:r3=1; y=1; z=2; 720074:>0:r1=0; 0:r3=0; y=2; z=2; 1581673:>0:r1=0; 0:r3=1; y=2; z=2; 15260932:>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 95.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33134085:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 21472 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 149347:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 16739183:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 11518866:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 2502038:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 795635:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 43878326:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 30205 :>0:r1=0; 0:r3=0; 2:r3=0; y=2; 495731:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 15455393:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 20416188:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 674626:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 13802413:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 40386492:>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 93.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9528939:>0:r1=0; 0:r3=0; y=1; z=1; 2507008:>0:r1=1; 0:r3=0; y=1; z=1; 804372:>0:r1=0; 0:r3=1; y=1; z=1; 47947966:>0:r1=1; 0:r3=1; y=1; z=1; 22002932:>0:r1=0; 0:r3=0; y=2; z=1; 1142816:>0:r1=1; 0:r3=0; y=2; z=1; 15129518:>0:r1=0; 0:r3=1; y=2; z=1; 45590807:>0:r1=1; 0:r3=1; y=2; z=1; 31381732:>0:r1=0; 0:r3=0; y=1; z=2; 27864 :>0:r1=1; 0:r3=0; y=1; z=2; 932624:>0:r1=0; 0:r3=1; y=1; z=2; 12439876:>0:r1=1; 0:r3=1; y=1; z=2; 32325 :>0:r1=0; 0:r3=0; y=2; z=2; 647667:>0:r1=0; 0:r3=1; y=2; z=2; 9883554:>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 95.95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 22832569:>0:r1=0; 0:r3=0; 1:r3=0; 30878995:>0:r1=0; 0:r3=1; 1:r3=0; 28831702:>0:r1=1; 0:r3=1; 1:r3=0; 42946728:>0:r1=0; 0:r3=0; 1:r3=1; 25116306:>0:r1=1; 0:r3=0; 1:r3=1; 443771:>0:r1=0; 0:r3=1; 1:r3=1; 48949929:>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 71.46 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15698467:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 13812 :>0:r1=1; 0:r3=0; 1:r3=0; z=1; 16221327:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 30602029:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 15718387:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 3680815:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 69453 :>0:r1=0; 0:r3=1; 1:r3=1; z=1; 33941646:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 606120:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 759312:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 28011 :>0:r1=1; 0:r3=1; 1:r3=0; z=2; 27982093:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 230657:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 3979504:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 50468367:>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 93.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 27298 :>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 68042 :>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 121948:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 32984486:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 22791 :>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 565058:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 32242185:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 16436397:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 14371 :>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 16437696:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 33802839:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 15520013:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 3643280:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 345016:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 47768580:>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.23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 16314363:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 13281 :>0:r1=1; 0:r3=0; 1:r3=0; z=1; 16422353:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 32977812:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 16094889:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 3509612:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 387191:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 56483559:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 27089 :>0:r1=0; 0:r3=0; 1:r3=0; z=2; 63535 :>0:r1=0; 0:r3=1; 1:r3=0; z=2; 132560:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 32232743:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 32093 :>0:r1=1; 0:r3=0; 1:r3=1; z=2; 790414:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 24518506:>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 93.81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 43474629:>0:r1=0; 0:r3=0; y=1; 24548048:>0:r1=1; 0:r3=0; y=1; 694824:>0:r1=0; 0:r3=1; y=1; 51335105:>0:r1=1; 0:r3=1; y=1; 21194132:>0:r1=0; 0:r3=0; y=2; 31199753:>0:r1=0; 0:r3=1; y=2; 27553509:>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 75.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15425705:>0:r1=0; 0:r3=0; y=1; z=1; 3828509:>0:r1=1; 0:r3=0; y=1; z=1; 393202:>0:r1=0; 0:r3=1; y=1; z=1; 38278817:>0:r1=1; 0:r3=1; y=1; z=1; 15593352:>0:r1=0; 0:r3=0; y=2; z=1; 14198 :>0:r1=1; 0:r3=0; y=2; z=1; 14428281:>0:r1=0; 0:r3=1; y=2; z=1; 28071748:>0:r1=1; 0:r3=1; y=2; z=1; 27038450:>0:r1=0; 0:r3=0; y=1; z=2; 168900:>0:r1=1; 0:r3=0; y=1; z=2; 5031828:>0:r1=0; 0:r3=1; y=1; z=2; 50188914:>0:r1=1; 0:r3=1; y=1; z=2; 717695:>0:r1=0; 0:r3=0; y=2; z=2; 792750:>0:r1=0; 0:r3=1; y=2; z=2; 27651 :>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 96.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33333144:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 20210 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 388111:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 32523210:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 15897544:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 3221427:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 679112:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 52452854:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 26901 :>0:r1=0; 0:r3=0; 2:r3=0; y=2; 66962 :>0:r1=0; 0:r3=1; 2:r3=0; y=2; 138474:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 16224868:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 13605 :>0:r1=1; 0:r3=0; 2:r3=1; y=2; 13423578:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 31590000:>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 95.24 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 6977880:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 24680329:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 1718124:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 1588031:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 199075:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 3882083:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 26229360:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 77349439:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 33256613:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 34068 :>0:r1=1; 2:r1=0; 2:r3=0; x=2; 25597 :>0:r1=0; 2:r1=1; 2:r3=0; x=2; 62737 :>0:r1=0; 2:r1=0; 2:r3=1; x=2; 727658:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 12273936:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 10995070:>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 90.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1324941:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 30494489:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 1056945:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 5896754:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 246527:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 3357808:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 11685403:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 78301031:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 27597162:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 53280 :>1:r1=1; 3:r1=0; 3:r4=0; x=2; 46198 :>1:r1=0; 3:r1=1; 3:r4=0; x=2; 2038005:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 289984:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 35926643:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 1684830:>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 84.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1336089:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 30967496:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 1024102:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 6264282:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 281332:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 3795005:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 12878179:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 75815150:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 28023472:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 58575 :>1:r1=1; 3:r1=0; 3:r3=0; x=2; 44083 :>1:r1=0; 3:r1=1; 3:r3=0; x=2; 1739295:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 272686:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 35879528:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 1620726:>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 84.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 6685428:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 25005881:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 1491216:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 1324574:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 168118:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 3629027:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 26285337:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 78701245:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 32987827:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 34030 :>0:r1=1; 2:r1=0; 2:r4=0; x=2; 23531 :>0:r1=0; 2:r1=1; 2:r4=0; x=2; 78576 :>0:r1=0; 2:r1=0; 2:r4=1; x=2; 535169:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 13158021:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 9892020:>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 90.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 6891796:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 25170571:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 1455418:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 1457995:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 168904:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 3759986:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 26075097:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 78337812:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 33155638:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 33928 :>0:r1=1; 2:r1=0; 2:r3=0; x=2; 24227 :>0:r1=0; 2:r1=1; 2:r3=0; x=2; 64611 :>0:r1=0; 2:r1=0; 2:r3=1; x=2; 482611:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 12974460:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 9946946:>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 90.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32775381:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 66093 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 5220621:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 23196342:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 22916 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 1066100:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 4594396:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 287337:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 307924:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 478973:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 6690426:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 15117621:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 7078482:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 23220727:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 79876661:>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 74.61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32703646:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 80029 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 5424748:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 23888748:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 23403 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 997961:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 4700211:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 243800:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 297195:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 573838:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 6508668:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 15210774:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 6831574:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 24485377:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 78030028:>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 74.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7356349:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 21237258:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 1364516:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 6604450:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 433758:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 6362991:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 21681555:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 79870956:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 29842617:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 46076 :>1:r1=1; 3:r1=0; 3:r4=0; x=2; 27436 :>1:r1=0; 3:r1=1; 3:r4=0; x=2; 1247061:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 253959:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 18001823:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 5669195:>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 84.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7476031:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 22121165:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 1200743:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 6876517:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 589487:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 6288573:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 24068622:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 76338028:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 29931357:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 56066 :>1:r1=1; 3:r1=0; 3:r3=0; x=2; 25720 :>1:r1=0; 3:r1=1; 3:r3=0; x=2; 919141:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 251774:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 18342345:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 5514431:>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 85.75 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 -s 1000 -r 100k -i 4 Mon Jan 24 11:08:34 CST 2011