lun jan 24 16:43:44 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) 149304226:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 9342523:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 56575099:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 66332988:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 9361946:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 59247551:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 11269122:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 56502558:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 59099955:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 2544304:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 57573052:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 66265012:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 11177531:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 57589023:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 127815110:>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 161.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 135135311:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 7909694:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 53324490:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 61447894:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 7362366:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 47597817:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 7874309:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 51859387:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 53518225:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 2056602:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 47654219:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 88709404:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 17064479:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 72836364:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 145649439:>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 161.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) 84816049:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 63600649:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 4935550:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 74735953:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 51416673:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 7520130:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 67169762:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 119342803:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 138772408:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 8378968:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 56508495:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 64362453:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 5755053:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 46575444:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 6109610:>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 150.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 236356361:>0:r1=0; 0:r4=0; y=1; 127071838:>0:r1=1; 0:r4=0; y=1; 10697720:>0:r1=0; 0:r4=1; y=1; 202622497:>0:r1=1; 0:r4=1; y=1; 102618663:>0:r1=0; 0:r4=0; y=2; 192052665:>0:r1=0; 0:r4=1; y=2; 128580256:>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 125.63 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 85142787:>0:r1=0; 0:r4=0; y=1; z=1; 62921942:>0:r1=1; 0:r4=0; y=1; z=1; 4991762:>0:r1=0; 0:r4=1; y=1; z=1; 70740015:>0:r1=1; 0:r4=1; y=1; z=1; 59838837:>0:r1=0; 0:r4=0; y=2; z=1; 9205694:>0:r1=1; 0:r4=0; y=2; z=1; 66207241:>0:r1=0; 0:r4=1; y=2; z=1; 129235430:>0:r1=1; 0:r4=1; y=2; z=1; 126688233:>0:r1=0; 0:r4=0; y=1; z=2; 6598465:>0:r1=1; 0:r4=0; y=1; z=2; 54227660:>0:r1=0; 0:r4=1; y=1; z=2; 63581773:>0:r1=1; 0:r4=1; y=1; z=2; 7067949:>0:r1=0; 0:r4=0; y=2; z=2; 46648677:>0:r1=0; 0:r4=1; y=2; z=2; 6903535:>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 152.75 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 139168873:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 5073179:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 54112947:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 55774164:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 75773914:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 64246886:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 6057637:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 69354597:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 8613124:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 54950525:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 11791404:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 60396490:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 9965688:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 63958424:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 120762148:>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 158.32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 98860299:>0:r1=0; 0:r4=0; y=1; z=1; 62986339:>0:r1=1; 0:r4=0; y=1; z=1; 8203106:>0:r1=0; 0:r4=1; y=1; z=1; 77667991:>0:r1=1; 0:r4=1; y=1; z=1; 64493606:>0:r1=0; 0:r4=0; y=2; z=1; 9770398:>0:r1=1; 0:r4=0; y=2; z=1; 77282633:>0:r1=0; 0:r4=1; y=2; z=1; 137373620:>0:r1=1; 0:r4=1; y=2; z=1; 109943021:>0:r1=0; 0:r4=0; y=1; z=2; 4540453:>0:r1=1; 0:r4=0; y=1; z=2; 51710434:>0:r1=0; 0:r4=1; y=1; z=2; 51755327:>0:r1=1; 0:r4=1; y=1; z=2; 5652158:>0:r1=0; 0:r4=0; y=2; z=2; 35723729:>0:r1=0; 0:r4=1; y=2; z=2; 4036886:>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 169.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 129549971:>0:r1=0; 0:r4=0; 1:r3=0; 189131108:>0:r1=0; 0:r4=1; 1:r3=0; 124764966:>0:r1=1; 0:r4=1; 1:r3=0; 208609016:>0:r1=0; 0:r4=0; 1:r3=1; 130915190:>0:r1=1; 0:r4=0; 1:r3=1; 14149282:>0:r1=0; 0:r4=1; 1:r3=1; 202880467:>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 133.05 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 64209063:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 11262133:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 65216378:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 126346479:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 82135757:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 68386733:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 7439725:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 61385900:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 11239297:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 42994399:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 5426322:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 130714284:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 7480601:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 53565035:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 62197894:>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 171.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14162420:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 52568495:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 11489256:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 137843544:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 6050415:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 52839714:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 56124015:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 65009852:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 13342810:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 60763083:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 122646684:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 71119088:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 68274608:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 7655888:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 60110128:>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 153.50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 71347553:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 12734248:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 76363063:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 134432989:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 95528815:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 67999063:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 10521306:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 66754507:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 8331949:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 33566589:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 3340862:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 113071918:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 5236528:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 49642644:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 51127966:>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 170.87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 247668431:>0:r1=0; 0:r4=0; y=1; 131046582:>0:r1=1; 0:r4=0; y=1; 25032110:>0:r1=0; 0:r4=1; y=1; 215760354:>0:r1=1; 0:r4=1; y=1; 90654877:>0:r1=0; 0:r4=0; y=2; 179712527:>0:r1=0; 0:r4=1; y=2; 110125119:>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 132.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 97750511:>0:r1=0; 0:r4=0; y=1; z=1; 69127796:>0:r1=1; 0:r4=0; y=1; z=1; 9592305:>0:r1=0; 0:r4=1; y=1; z=1; 84512497:>0:r1=1; 0:r4=1; y=1; z=1; 47454061:>0:r1=0; 0:r4=0; y=2; z=1; 7221472:>0:r1=1; 0:r4=0; y=2; z=1; 62595201:>0:r1=0; 0:r4=1; y=2; z=1; 111611962:>0:r1=1; 0:r4=1; y=2; z=1; 132768130:>0:r1=0; 0:r4=0; y=1; z=2; 7135774:>0:r1=1; 0:r4=0; y=1; z=2; 58942759:>0:r1=0; 0:r4=1; y=1; z=2; 65076402:>0:r1=1; 0:r4=1; y=1; z=2; 4169158:>0:r1=0; 0:r4=0; y=2; z=2; 37448867:>0:r1=0; 0:r4=1; y=2; z=2; 4593105:>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 160.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 145846225:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 5562093:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 59853879:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 58185099:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 88399462:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 71445796:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 9951639:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 81766100:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 4877614:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 46090663:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 8818137:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 47917342:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 7772174:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 60591526:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 102922251:>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 149.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 113830372:>0:r1=0; 0:r4=0; y=1; z=1; 69445032:>0:r1=1; 0:r4=0; y=1; z=1; 13461673:>0:r1=0; 0:r4=1; y=1; z=1; 93244660:>0:r1=1; 0:r4=1; y=1; z=1; 50589359:>0:r1=0; 0:r4=0; y=2; z=1; 7684571:>0:r1=1; 0:r4=0; y=2; z=1; 72432242:>0:r1=0; 0:r4=1; y=2; z=1; 118236877:>0:r1=1; 0:r4=1; y=2; z=1; 114197929:>0:r1=0; 0:r4=0; y=1; z=2; 4958423:>0:r1=1; 0:r4=0; y=1; z=2; 54325568:>0:r1=0; 0:r4=1; y=1; z=2; 52545504:>0:r1=1; 0:r4=1; y=1; z=2; 3437679:>0:r1=0; 0:r4=0; y=2; z=2; 28660258:>0:r1=0; 0:r4=1; y=2; z=2; 2949853:>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 157.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 122298397:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 6441154:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 48724059:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 82000608:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 6234300:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 42736886:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 12450416:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 48786764:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 43244982:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 1679551:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 61789364:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 81149549:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 12199580:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 60904508:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 169359882:>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 137.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 230999629:>0:r1=0; 0:r3=0; y=1; 109214245:>0:r1=1; 0:r3=0; y=1; 9281219:>0:r1=0; 0:r3=1; y=1; 227907604:>0:r1=1; 0:r3=1; y=1; 100261029:>0:r1=0; 0:r3=0; y=2; 178596965:>0:r1=0; 0:r3=1; y=2; 143739309:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=8e9853ba7646212616eafb737d8e71e4 Observation Y16 Never 0 1000000000 Time Y16 126.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 80561596:>0:r1=0; 0:r3=0; y=1; z=1; 51080213:>0:r1=1; 0:r3=0; y=1; z=1; 4469662:>0:r1=0; 0:r3=1; y=1; z=1; 90465738:>0:r1=1; 0:r3=1; y=1; z=1; 53216206:>0:r1=0; 0:r3=0; y=2; z=1; 5918993:>0:r1=1; 0:r3=0; y=2; z=1; 54497687:>0:r1=0; 0:r3=1; y=2; z=1; 142678332:>0:r1=1; 0:r3=1; y=2; z=1; 114834786:>0:r1=0; 0:r3=0; y=1; z=2; 5018376:>0:r1=1; 0:r3=0; y=1; z=2; 50705536:>0:r1=0; 0:r3=1; y=1; z=2; 84604826:>0:r1=1; 0:r3=1; y=1; z=2; 6107798:>0:r1=0; 0:r3=0; y=2; z=2; 44320889:>0:r1=0; 0:r3=1; y=2; z=2; 11519362:>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 165.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 124778420:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 3941279:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 49928630:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 74778341:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 71158843:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 51184772:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 5316703:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 89478624:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 7404839:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 48767728:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 17493013:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 55616664:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 6905640:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 53789166:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 139457338:>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 149.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 94512205:>0:r1=0; 0:r3=0; y=1; z=1; 50976651:>0:r1=1; 0:r3=0; y=1; z=1; 7177058:>0:r1=0; 0:r3=1; y=1; z=1; 101279797:>0:r1=1; 0:r3=1; y=1; z=1; 56436325:>0:r1=0; 0:r3=0; y=2; z=1; 6116192:>0:r1=1; 0:r3=0; y=2; z=1; 64708294:>0:r1=0; 0:r3=1; y=2; z=1; 151878740:>0:r1=1; 0:r3=1; y=2; z=1; 99222355:>0:r1=0; 0:r3=0; y=1; z=2; 3377045:>0:r1=1; 0:r3=0; y=1; z=2; 48429624:>0:r1=0; 0:r3=1; y=1; z=2; 70117831:>0:r1=1; 0:r3=1; y=1; z=2; 4746167:>0:r1=0; 0:r3=0; y=2; z=2; 33583420:>0:r1=0; 0:r3=1; y=2; z=2; 7438296:>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 154.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 126473957:>0:r1=0; 0:r3=0; 1:r3=0; 175093965:>0:r1=0; 0:r3=1; 1:r3=0; 141570562:>0:r1=1; 0:r3=1; 1:r3=0; 203899844:>0:r1=0; 0:r3=0; 1:r3=1; 113384649:>0:r1=1; 0:r3=0; 1:r3=1; 11391987:>0:r1=0; 0:r3=1; 1:r3=1; 228185036:>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 119.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 60453879:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 7886709:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 54250797:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 143379480:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 76186311:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 55044265:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 6082043:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 82319785:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 10622159:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 39655425:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 8992110:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 114184211:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 5919457:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 49633532:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 85389837:>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 150.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13547709:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 46674543:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 16313297:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 120650476:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 4647533:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 48816029:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 76623983:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 61911723:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 9605546:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 51099155:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 143290587:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 65715030:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 54555517:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 6468601:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 80080271:>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 138.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 65806694:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 8593398:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 63826815:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 152849255:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 88737285:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 54891945:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 8757781:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 91089291:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 7758860:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 31002592:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 6104953:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 99874769:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 4022025:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 46671383:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 70012954:>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 152.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 242023422:>0:r1=0; 0:r3=0; y=1; 112464072:>0:r1=1; 0:r3=0; y=1; 21336473:>0:r1=0; 0:r3=1; y=1; 245927546:>0:r1=1; 0:r3=1; y=1; 88726089:>0:r1=0; 0:r3=0; y=2; 166552709:>0:r1=0; 0:r3=1; y=2; 122969689:>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 127.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 92652542:>0:r1=0; 0:r3=0; y=1; z=1; 55760361:>0:r1=1; 0:r3=0; y=1; z=1; 8426335:>0:r1=0; 0:r3=1; y=1; z=1; 107572985:>0:r1=1; 0:r3=1; y=1; z=1; 41590630:>0:r1=0; 0:r3=0; y=2; z=1; 4375307:>0:r1=1; 0:r3=0; y=2; z=1; 51393261:>0:r1=0; 0:r3=1; y=2; z=1; 123826160:>0:r1=1; 0:r3=1; y=2; z=1; 119826641:>0:r1=0; 0:r3=0; y=1; z=2; 5378920:>0:r1=1; 0:r3=0; y=1; z=2; 55287761:>0:r1=0; 0:r3=1; y=1; z=2; 87968341:>0:r1=1; 0:r3=1; y=1; z=2; 3561634:>0:r1=0; 0:r3=0; y=2; z=2; 34564493:>0:r1=0; 0:r3=1; y=2; z=2; 7814629:>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 152.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 130660265:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 4297445:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 55395566:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 78930721:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 82456338:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 56958652:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 8424874:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 104214281:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 4274614:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 40864111:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 13180427:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 44172685:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 5273130:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 50387643:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 120509248:>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 151.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 80844135:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 45977239:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 50853610:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 4867803:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 4076199:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 54934978:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 93250026:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 135286979:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 123712299:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 4621594:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 6703811:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 52459985:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 43058442:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 88672580:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 10680320:>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 149.23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 67724941:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 78017061:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 59442676:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 13643385:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 2093325:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 70033038:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 54359192:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 147423202:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 125754948:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 10673251:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 5222045:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 49725697:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 45701257:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 62599250:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 7586732:>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 127.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 64550472:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 73426082:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 47368027:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 9661645:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 1862058:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 59176293:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 69039679:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 167502544:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 110727406:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 9710615:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 4011155:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 47283291:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 41887964:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 82208804:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 11583965:>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 128.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 83469884:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 50718733:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 62981679:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 7205934:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 4714057:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 66330463:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 74743803:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 118690089:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 140146238:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 5855440:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 8515489:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 57367318:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 47816442:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 65053972:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 6390459:>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 149.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 79499122:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 46454045:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 50172941:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 4824745:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 3949302:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 55067078:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 93176127:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 135789207:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 123640724:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 4831658:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 6662141:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 52627127:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 43563646:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 88829805:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 10912332:>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 149.12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 127608281:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 12898634:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 63598895:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 79548607:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 4528113:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 58536596:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 15229368:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 48130240:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 49534342:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 2988425:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 67398471:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 57765559:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 9403108:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 54889832:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 147941529:>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 118.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 115083160:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 11790580:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 59855037:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 74123646:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 3475472:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 46475549:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 10833640:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 45894193:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 44897308:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 2603402:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 56362371:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 75369381:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 14224450:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 69924419:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 169087392:>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 118.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 76231222:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 82422072:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 58986786:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 14843264:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 4000804:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 75558718:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 60087841:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 151484034:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 115718516:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 9171147:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 3805715:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 47145413:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 39989757:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 54772696:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 5782015:>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 128.22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 72180953:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 76855020:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 46783068:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 10399292:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 3471803:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 63974420:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 76783435:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 173002037:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 102185149:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 8363740:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 2871162:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 45016007:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 36653734:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 72230306:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 9229874:>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 128.96 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 lun jan 24 18:10:54 CET 2011