lun fév 7 16:12:05 CET 2011 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y00.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y00 "Rf*e DpAddrdR Fre LwSyncdWW Rf*e DpAddrdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | DIY01: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | xor r3,r1,r1 | lwsync ; lwzx r4,r3,r5 | li r3,1 | lwzx r4,r3,r5 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stwcx. r1,r0,r2 | stw r3,0(r4) ; bne DIY00 | | bne DIY01 | ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: xor 10,30,30 _litmus_P0_3_: lwzx 31,10,9 _litmus_P0_4_: stwcx. 30,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: LitDIY01: _litmus_P2_1_: lwarx 30,0,11 _litmus_P2_2_: xor 10,30,30 _litmus_P2_3_: lwzx 31,10,9 _litmus_P2_4_: stwcx. 30,0,11 _litmus_P2_5_: bne LitDIY01 Test Y00 Allowed Histogram (15 states) 107247316:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 13134081:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 42109198:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 69723873:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 12585543:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 47130091:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 21210339:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 41592127:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 47122800:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 3424423:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 60670878:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 69842618:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 21241563:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 60473006:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 182492144:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=08b576a9816ca91b136efc84cb8198fe Observation Y00 Never 0 800000000 Time Y00 168.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) 98427233:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 11428326:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 37119518:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 60137048:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 12248885:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 45226425:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 19225819:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 40982531:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 46870515:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 3336968:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 60735742:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 76876413:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 23944442:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 68993573:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 194446562:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=27be645f8ce747a8241695ecd5d12775 Observation Y01 Never 0 800000000 Time Y01 167.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 70820126:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 60707465:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 9116147:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 110611370:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 44116660:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 10406243:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 55414305:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 139792090:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 109961122:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 11134010:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 49375852:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 71908191:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 5769823:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 36840650:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 14025946:>0:r1=1; 0:r4=1; 2:r1=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is NOT validated Hash=e299ccd513ee6b40ffc1479736b6d80f Observation Y02 Never 0 800000000 Time Y02 174.97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 222466552:>0:r1=0; 0:r4=0; y=1; 103120991:>0:r1=1; 0:r4=0; y=1; 21507973:>0:r1=0; 0:r4=1; y=1; 283300955:>0:r1=1; 0:r4=1; y=1; 79225995:>0:r1=0; 0:r4=0; y=2; 160335394:>0:r1=0; 0:r4=1; y=2; 130042140:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=fbc1c062cf6f3291c2ce205045bcf85e Observation Y03 Never 0 1000000000 Time Y03 118.75 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 76831693:>0:r1=0; 0:r4=0; y=1; z=1; 64205251:>0:r1=1; 0:r4=0; y=1; z=1; 10322099:>0:r1=0; 0:r4=1; y=1; z=1; 121094431:>0:r1=1; 0:r4=1; y=1; z=1; 42086053:>0:r1=0; 0:r4=0; y=2; z=1; 9717232:>0:r1=1; 0:r4=0; y=2; z=1; 54747229:>0:r1=0; 0:r4=1; y=2; z=1; 134541847:>0:r1=1; 0:r4=1; y=2; z=1; 94229447:>0:r1=0; 0:r4=0; y=1; z=2; 10889799:>0:r1=1; 0:r4=0; y=1; z=2; 55045335:>0:r1=0; 0:r4=1; y=1; z=2; 76668657:>0:r1=1; 0:r4=1; y=1; z=2; 5745105:>0:r1=0; 0:r4=0; y=2; z=2; 32670127:>0:r1=0; 0:r4=1; y=2; z=2; 11205695:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=00bb906e6b50e3e5b6bc490a41e163e4 Observation Y04 Never 0 800000000 Time Y04 196.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 101521428:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 9376486:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 44752854:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 59640444:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 77540381:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 61360243:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 11666177:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 109266719:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 6748736:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 39437539:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 16760252:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 46896308:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 12164223:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 56362352:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 146505858:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=2d110167698039bf55def82743b120ef Observation Y05 Never 0 800000000 Time Y05 180.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 88322488:>0:r1=0; 0:r4=0; y=1; z=1; 65858324:>0:r1=1; 0:r4=0; y=1; z=1; 14492597:>0:r1=0; 0:r4=1; y=1; z=1; 125762429:>0:r1=1; 0:r4=1; y=1; z=1; 44326351:>0:r1=0; 0:r4=0; y=2; z=1; 10928539:>0:r1=1; 0:r4=0; y=2; z=1; 59949992:>0:r1=0; 0:r4=1; y=2; z=1; 150705276:>0:r1=1; 0:r4=1; y=2; z=1; 87392324:>0:r1=0; 0:r4=0; y=1; z=2; 7948783:>0:r1=1; 0:r4=0; y=1; z=2; 41254047:>0:r1=0; 0:r4=1; y=1; z=2; 53361684:>0:r1=1; 0:r4=1; y=1; z=2; 4792863:>0:r1=0; 0:r4=0; y=2; z=2; 33196363:>0:r1=0; 0:r4=1; y=2; z=2; 11707940:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5519b7e18d61900b26b6e20148fd6e5b Observation Y06 Never 0 800000000 Time Y06 199.81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 89280465:>0:r1=0; 0:r4=0; 1:r3=0; 154290944:>0:r1=0; 0:r4=1; 1:r3=0; 121784292:>0:r1=1; 0:r4=1; 1:r3=0; 222144076:>0:r1=0; 0:r4=0; 1:r3=1; 115832844:>0:r1=1; 0:r4=0; 1:r3=1; 24146231:>0:r1=0; 0:r4=1; 1:r3=1; 272521148:>0:r1=1; 0:r4=1; 1:r3=1; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=75dc62611c83cbf21aa9273aa6a41b23 Observation Y07 Never 0 1000000000 Time Y07 114.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) 43482298:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 10510454:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 50604965:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 120362188:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 83275155:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 73651873:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 12043056:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 119200919:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 6767683:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 29575880:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 9748675:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 104491123:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 13611808:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 49544929:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 73128994:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=6f98559c8174fdcd1fe2a621ad7dc8d2 Observation Y08 Never 0 800000000 Time Y08 180.95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7680948:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 32326928:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 11088740:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 102032953:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 11236934:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 48811659:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 66630571:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 46857657:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 12450408:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 52493274:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 125947762:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 81148146:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 71567526:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 12905196:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 116821298:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=f9c57151a878a2fb7ca88a7241079b1d Observation Y09 Never 0 800000000 Time Y09 171.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 45674148:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 11484826:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 54644270:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 124712975:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 95219428:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 75444725:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 16781958:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 132647536:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 5654268:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 26853923:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 8117200:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 92289543:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 9175781:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 45181110:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 56118309:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=d987b1dfa9ff6dbc9cfc5646bda90ed3 Observation Y10 Never 0 800000000 Time Y10 179.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 235323813:>0:r1=0; 0:r4=0; y=1; 104919596:>0:r1=1; 0:r4=0; y=1; 40837901:>0:r1=0; 0:r4=1; y=1; 306217367:>0:r1=1; 0:r4=1; y=1; 69301660:>0:r1=0; 0:r4=0; y=2; 145835061:>0:r1=0; 0:r4=1; y=2; 97564602:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5506d17360dcb64cbec742d67fe4340e Observation Y11 Never 0 1000000000 Time Y11 118.62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 85134787:>0:r1=0; 0:r4=0; y=1; z=1; 67970467:>0:r1=1; 0:r4=0; y=1; z=1; 14929049:>0:r1=0; 0:r4=1; y=1; z=1; 141140215:>0:r1=1; 0:r4=1; y=1; z=1; 38028710:>0:r1=0; 0:r4=0; y=2; z=1; 7908718:>0:r1=1; 0:r4=0; y=2; z=1; 51256701:>0:r1=0; 0:r4=1; y=2; z=1; 110579588:>0:r1=1; 0:r4=1; y=2; z=1; 99221626:>0:r1=0; 0:r4=0; y=1; z=2; 10863630:>0:r1=1; 0:r4=0; y=1; z=2; 56371660:>0:r1=0; 0:r4=1; y=1; z=2; 78126066:>0:r1=1; 0:r4=1; y=1; z=2; 4539781:>0:r1=0; 0:r4=0; y=2; z=2; 26075265:>0:r1=0; 0:r4=1; y=2; z=2; 7853737:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=e74570fa8cc4ed49e2bc7eb3e6efaadc Observation Y12 Never 0 800000000 Time Y12 199.70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 103698210:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 9520234:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 57386118:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 70148957:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 84568572:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 66116228:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 16795106:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 132133492:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 5661850:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 28453212:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 8818449:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 41133405:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 10101698:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 51691325:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 113773144:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=d514c17376c3fe56c7da249e5154e952 Observation Y13 Never 0 800000000 Time Y13 181.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 94498584:>0:r1=0; 0:r4=0; y=1; z=1; 69360239:>0:r1=1; 0:r4=0; y=1; z=1; 19890177:>0:r1=0; 0:r4=1; y=1; z=1; 152443023:>0:r1=1; 0:r4=1; y=1; z=1; 40146791:>0:r1=0; 0:r4=0; y=2; z=1; 8807226:>0:r1=1; 0:r4=0; y=2; z=1; 55095978:>0:r1=0; 0:r4=1; y=2; z=1; 115359306:>0:r1=1; 0:r4=1; y=2; z=1; 88995330:>0:r1=0; 0:r4=0; y=1; z=2; 8295236:>0:r1=1; 0:r4=0; y=1; z=2; 52092571:>0:r1=0; 0:r4=1; y=1; z=2; 61267122:>0:r1=1; 0:r4=1; y=1; z=2; 3844595:>0:r1=0; 0:r4=0; y=2; z=2; 23339496:>0:r1=0; 0:r4=1; y=2; z=2; 6564326:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=db5bc36ebd8ef1745e795c6bdf75e423 Observation Y14 Never 0 800000000 Time Y14 201.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 93021271:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 11597459:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 36485948:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 66442899:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 11300902:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 45202360:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 21067958:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 36094140:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 46326669:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 3135169:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 67075141:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 66360216:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 21497714:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 65540770:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 208851384:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=11eec175e5c988e350ebfc54fd0e2c1c Observation Y15 Never 0 800000000 Time Y15 170.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 197980484:>0:r1=0; 0:r3=0; y=1; 100834654:>0:r1=1; 0:r3=0; y=1; 20483451:>0:r1=0; 0:r3=1; y=1; 311501038:>0:r1=1; 0:r3=1; y=1; 69771739:>0:r1=0; 0:r3=0; y=2; 159966978:>0:r1=0; 0:r3=1; y=2; 139461656:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=8e9853ba7646212616eafb737d8e71e4 Observation Y16 Never 0 1000000000 Time Y16 118.54 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 68237911:>0:r1=0; 0:r3=0; y=1; z=1; 60299527:>0:r1=1; 0:r3=0; y=1; z=1; 10321275:>0:r1=0; 0:r3=1; y=1; z=1; 134340653:>0:r1=1; 0:r3=1; y=1; z=1; 34665403:>0:r1=0; 0:r3=0; y=2; z=1; 8911588:>0:r1=1; 0:r3=0; y=2; z=1; 54239909:>0:r1=0; 0:r3=1; y=2; z=1; 141458353:>0:r1=1; 0:r3=1; y=2; z=1; 89217207:>0:r1=0; 0:r3=0; y=1; z=2; 10604934:>0:r1=1; 0:r3=0; y=1; z=2; 54099865:>0:r1=0; 0:r3=1; y=1; z=2; 84364740:>0:r1=1; 0:r3=1; y=1; z=2; 4826631:>0:r1=0; 0:r3=0; y=2; z=2; 32218941:>0:r1=0; 0:r3=1; y=2; z=2; 12193063:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=5dde3da66b8fd3eb942a6c2fb7e9050b Observation Y17 Never 0 800000000 Time Y17 201.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y18.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y18 "Rf*e DpCtrlIsyncdR Fre LwSyncdWW Wse SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,2 | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | lwsync | sync | lwsync ; beq LC01 | li r3,1 | lwz r3,0(r4) | li r3,1 ; LC01: | stw r3,0(r4) | | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test Y18 Allowed Histogram (15 states) 92515917:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 9317713:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 45318850:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 67945968:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 67799690:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 57691162:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 11013512:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 122976146:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 5699384:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 39075578:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 19029553:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 39074088:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 11128079:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 54456923:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 156957437:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=abfe8f96fb73d61f24cd4ed25c4cbe36 Observation Y18 Never 0 800000000 Time Y18 181.22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 77959819:>0:r1=0; 0:r3=0; y=1; z=1; 61366931:>0:r1=1; 0:r3=0; y=1; z=1; 14793503:>0:r1=0; 0:r3=1; y=1; z=1; 141397273:>0:r1=1; 0:r3=1; y=1; z=1; 36968475:>0:r1=0; 0:r3=0; y=2; z=1; 9127721:>0:r1=1; 0:r3=0; y=2; z=1; 59098697:>0:r1=0; 0:r3=1; y=2; z=1; 155074615:>0:r1=1; 0:r3=1; y=2; z=1; 83204035:>0:r1=0; 0:r3=0; y=1; z=2; 7463385:>0:r1=1; 0:r3=0; y=1; z=2; 43365380:>0:r1=0; 0:r3=1; y=1; z=2; 59657376:>0:r1=1; 0:r3=1; y=1; z=2; 4018401:>0:r1=0; 0:r3=0; y=2; z=2; 33799746:>0:r1=0; 0:r3=1; y=2; z=2; 12704643:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=a4ab8a1891a2982f2576f75c35f64825 Observation Y19 Never 0 800000000 Time Y19 202.67 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 83310119:>0:r1=0; 0:r3=0; 1:r3=0; 156128236:>0:r1=0; 0:r3=1; 1:r3=0; 127998903:>0:r1=1; 0:r3=1; 1:r3=0; 200170563:>0:r1=0; 0:r3=0; 1:r3=1; 112939373:>0:r1=1; 0:r3=0; 1:r3=1; 22517806:>0:r1=0; 0:r3=1; 1:r3=1; 296935000:>0:r1=1; 0:r3=1; 1:r3=1; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=310ba9b87ba9c8abbb2cb09115abba03 Observation Y20 Never 0 1000000000 Time Y20 116.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 37851978:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 9637690:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 51148458:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 128037216:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 71859896:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 69076743:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 11556305:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 132951935:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 6026072:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 30853238:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 11111832:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 96972767:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 12960065:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 49840056:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 80115749:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=63a4ff1b2a8c61b6b9352662bce3e8c9 Observation Y21 Never 0 800000000 Time Y21 184.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 6514193:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 31455437:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 11753931:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 93704639:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 11052160:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 47757937:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 74479226:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 40418331:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 11562419:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 53152124:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 137169678:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 68931021:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 70093245:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 12266152:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 129689507:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=8a2b1f87ebce2fea7bdd4e78ab49e198 Observation Y22 Never 0 800000000 Time Y22 172.73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 38520469:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 9519311:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 54760144:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 130574290:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 81782656:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 71026796:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 15616381:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 150261976:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 5009410:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 27487891:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 9148314:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 86638152:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 9139826:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 46739953:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 63774431:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=34f72841a6635924e4f6e89a17ea5886 Observation Y23 Never 0 800000000 Time Y23 182.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 210061687:>0:r1=0; 0:r3=0; y=1; 102918287:>0:r1=1; 0:r3=0; y=1; 39024935:>0:r1=0; 0:r3=1; y=1; 337936632:>0:r1=1; 0:r3=1; y=1; 61843652:>0:r1=0; 0:r3=0; y=2; 143658357:>0:r1=0; 0:r3=1; y=2; 104556450:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=967cc1d43171137af345c68503a9bda3 Observation Y24 Never 0 1000000000 Time Y24 119.67 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 75115541:>0:r1=0; 0:r3=0; y=1; z=1; 67087538:>0:r1=1; 0:r3=0; y=1; z=1; 14565750:>0:r1=0; 0:r3=1; y=1; z=1; 156923316:>0:r1=1; 0:r3=1; y=1; z=1; 30202635:>0:r1=0; 0:r3=0; y=2; z=1; 7509571:>0:r1=1; 0:r3=0; y=2; z=1; 47413098:>0:r1=0; 0:r3=1; y=2; z=1; 112684971:>0:r1=1; 0:r3=1; y=2; z=1; 93584788:>0:r1=0; 0:r3=0; y=1; z=2; 11549099:>0:r1=1; 0:r3=0; y=1; z=2; 57569075:>0:r1=0; 0:r3=1; y=1; z=2; 86623689:>0:r1=1; 0:r3=1; y=1; z=2; 3751739:>0:r1=0; 0:r3=0; y=2; z=2; 26350483:>0:r1=0; 0:r3=1; y=2; z=2; 9068707:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=67d202536303d5d116d23867165f4ed6 Observation Y25 Never 0 800000000 Time Y25 202.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 96177950:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 10258881:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 56269378:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 77604423:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 74227314:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 64962690:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 15402332:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 147577341:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 4715294:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 27513978:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 10183935:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 34701098:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 9665308:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 48516494:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 122223584:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=44ca19804af93c9cee9c0f6acff5a2b0 Observation Y26 Never 0 800000000 Time Y26 182.98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 62515812:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 36863103:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 59799833:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 9372322:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 9042389:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 52937678:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 123515883:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 146765651:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 100990988:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 4706175:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 11415976:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 48783237:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 36198768:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 81027333:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 16064852:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ad65804aeb1597ba714e2328512d7995 Observation Y27 Never 0 800000000 Time Y27 176.97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 61458411:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 61698238:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 55181305:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 15915037:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 5848376:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 61293126:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 87529146:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 186073369:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 90739231:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 9894680:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 8703792:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 34475053:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 43840793:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 57736118:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 19613325:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=ce1b4a24ee0901b9de433860bfb46080 Observation Y28 Never 0 800000000 Time Y28 152.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 53578053:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 53295132:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 53013350:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 14609309:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 5891437:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 60838674:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 95342734:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 196606131:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 85715858:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 8943622:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 8417458:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 35305743:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 44207700:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 62975922:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 21258877:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=8bc55273b7032305e0142605023bce2d Observation Y29 Never 0 800000000 Time Y29 150.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 71006494:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 43949026:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 59767940:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 9880460:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 9472520:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 55842190:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 111187040:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 137374673:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 109248784:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 5872140:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 11134610:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 50449529:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 37507852:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 72988867:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 14317875:>0:r1=1; 2:r1=1; 2:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=3e1573bf73b4fdef87461b3565d66b20 Observation Y30 Never 0 800000000 Time Y30 176.24 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 61515321:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 37430959:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 57073763:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 9159490:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 9235116:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 55575140:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 123106694:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 147265877:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 101337992:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 4691883:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 10878871:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 49289362:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 36068118:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 81756863:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 15614551:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=e6774eda20819c8f372129af64bca016 Observation Y31 Never 0 800000000 Time Y31 175.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 93305545:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 10091044:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 61547670:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 60595073:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 8150427:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 52538939:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 16394298:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 35407066:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 41744657:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 7622165:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 61072843:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 56285156:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 18489789:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 86932745:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 189822583:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=a577eb9c8f1d583ecead3fdf77525a1e Observation Y32 Never 0 800000000 Time Y32 144.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 89767830:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 9181527:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 54836893:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 52901785:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 7976689:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 51040321:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 14083249:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 36328622:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 43205714:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 7535213:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 59392273:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 60719752:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 20194531:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 95877100:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 196958501:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=eea22bd3e2446126dd9b287b5df5faca Observation Y33 Never 0 800000000 Time Y33 144.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 66594772:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 64410694:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 55421718:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 16855029:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 8462749:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 65158560:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 89299752:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 196394021:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 83004737:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 9454931:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 6992771:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 33141327:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 40250291:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 48897385:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 15661263:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=49482953dd91da1bcee183b3b0b006b8 Observation Y34 Never 0 800000000 Time Y34 151.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 58997572:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 56529882:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 52660960:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 15277611:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 8354635:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 62654286:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 98959130:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 208390253:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 79206484:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 8460685:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 6663021:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 32737340:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 39504970:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 54108666:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 17494505:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=1ab190404386bf69014d12d891f99e7c Observation Y35 Never 0 800000000 Time Y35 149.24 Revision 6801:6804M, version 4.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= lun fév 7 17:52:15 CET 2011