dim jan 23 20:46:40 CET 2011 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X00.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X00 "Rfe DpAddrdR Fre LwSyncdWW Rfe 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 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r5 | lwsync ; | li r3,1 | | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; 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_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _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_: lwz 30,0(11) _litmus_P2_1_: xor 10,30,30 _litmus_P2_2_: lwzx 31,10,9 Test X00 Allowed Histogram (16 states) 169933687:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 10923482:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 75981583:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 54586726:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 10761147:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 168 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=0; 50375510:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 6970475:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 74005921:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 51352894:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 6161558:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 70027989:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 53482971:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 7164273:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 69313874:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 88957742:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; Ok Witnesses Positive: 168, Negative: 799999832 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is validated Hash=6559e19d9e37619f3f8bf433a5805105 Observation X00 Sometimes 168 799999832 Time X00 150.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X01.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X01 "Rfe DpAddrdR Fre LwSyncdWW Rfe 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 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | beq LC00 | lwsync ; | li r3,1 | LC00: | li r3,1 ; | stw r3,0(r4) | isync | stw r3,0(r4) ; | | lwz r3,0(r4) | ; 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_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _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_: lwz 3,0(11) _litmus_P2_1_: cmpw 3,3 _litmus_P2_2_: beq LitLC00 _litmus_P2_3_: LitLC00: _litmus_P2_4_: isync _litmus_P2_5_: lwz 31,0(9) Test X01 Allowed Histogram (16 states) 152304405:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 9746955:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 72167626:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 50247501:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 9385467:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 166 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=0; 46058853:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 6116438:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 90419858:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 52203415:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 10402450:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 74215237:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 55764124:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 7535544:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 72912706:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 90519255:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 166, Negative: 799999834 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=2dd158f1ef0b66595a56ff21c6e00a13 Observation X01 Sometimes 166 799999834 Time X01 151.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X02.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X02 "Rfe DpAddrdR Fre LwSyncdWW Rfe 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 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | beq LC00 | lwsync ; | li r3,1 | LC00: | li r3,1 ; | stw r3,0(r4) | li r3,1 | stw r3,0(r4) ; | | 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_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: cmpw 3,3 _litmus_P2_2_: beq LitLC00 _litmus_P2_3_: LitLC00: _litmus_P2_4_: li 30,1 _litmus_P2_5_: stw 30,0(9) Test X02 Allowed Histogram (16 states) 86592843:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 53126743:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 8482281:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 72931653:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 53987651:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 7073627:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 71339608:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 91481933:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 155140046:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 11050684:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 80656456:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 53588936:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 9700717:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 44 :>0:r1=1; 0:r4=0; 2:r1=1; z=2; 40821114:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 4025664:>0:r1=1; 0:r4=1; 2:r1=1; z=2; Ok Witnesses Positive: 44, Negative: 799999956 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is validated Hash=ddaab862216f1c9eafeceba074a24928 Observation X02 Sometimes 44 799999956 Time X02 164.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X03.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X03 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | lwsync ; | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) ; 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_: lwz 27,0(11) _litmus_P0_1_: xor 10,27,27 _litmus_P0_2_: lwzx 28,10,9 _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 X03 Allowed Histogram (8 states) 268418675:>0:r1=0; 0:r4=0; y=1; 96449781:>0:r1=1; 0:r4=0; y=1; 19652278:>0:r1=0; 0:r4=1; y=1; 201657659:>0:r1=1; 0:r4=1; y=1; 104842577:>0:r1=0; 0:r4=0; y=2; 4607 :>0:r1=1; 0:r4=0; y=2; 237942479:>0:r1=0; 0:r4=1; y=2; 71031944:>0:r1=1; 0:r4=1; y=2; Ok Witnesses Positive: 4607, Negative: 999995393 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=979eb45568765c8b5bb24cb8beb2a694 Observation X03 Sometimes 4607 999995393 Time X03 113.65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X04.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X04 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | lwsync | lwsync ; | li r3,1 | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X04 Allowed Histogram (16 states) 94005382:>0:r1=0; 0:r4=0; y=1; z=1; 55383249:>0:r1=1; 0:r4=0; y=1; z=1; 8417702:>0:r1=0; 0:r4=1; y=1; z=1; 71680626:>0:r1=1; 0:r4=1; y=1; z=1; 62292882:>0:r1=0; 0:r4=0; y=2; z=1; 9509758:>0:r1=1; 0:r4=0; y=2; z=1; 82156009:>0:r1=0; 0:r4=1; y=2; z=1; 98947769:>0:r1=1; 0:r4=1; y=2; z=1; 136407701:>0:r1=0; 0:r4=0; y=1; z=2; 8629819:>0:r1=1; 0:r4=0; y=1; z=2; 66217465:>0:r1=0; 0:r4=1; y=1; z=2; 40933984:>0:r1=1; 0:r4=1; y=1; z=2; 9984634:>0:r1=0; 0:r4=0; y=2; z=2; 70 :>0:r1=1; 0:r4=0; y=2; z=2; 49323905:>0:r1=0; 0:r4=1; y=2; z=2; 6109045:>0:r1=1; 0:r4=1; y=2; z=2; Ok Witnesses Positive: 70, Negative: 799999930 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=bbe86be3ef3c2131f0d4681c0ccd31a8 Observation X04 Sometimes 70 799999930 Time X04 170.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X05.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X05 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | sync | lwsync ; | li r3,1 | lwz r3,0(r4) | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; 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_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,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_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X05 Allowed Histogram (16 states) 130546320:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 3724571:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 57744553:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 29250284:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 91592523:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 54946704:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 8871466:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 70902217:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 12590042:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 167 :>0:r1=1; 0:r4=0; 2:r3=0; y=2; 53130807:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 6970011:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 74128834:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 11003071:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 86503529:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 108094901:>0:r1=1; 0:r4=1; 2:r3=1; y=2; Ok Witnesses Positive: 167, Negative: 799999833 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is validated Hash=2f45a04baa1582caaf7bebb0f6429fad Observation X05 Sometimes 167 799999833 Time X05 168.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X06.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X06 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | sync | lwsync ; | li r3,1 | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X06 Allowed Histogram (16 states) 103238968:>0:r1=0; 0:r4=0; y=1; z=1; 56380627:>0:r1=1; 0:r4=0; y=1; z=1; 14522430:>0:r1=0; 0:r4=1; y=1; z=1; 76540258:>0:r1=1; 0:r4=1; y=1; z=1; 71822966:>0:r1=0; 0:r4=0; y=2; z=1; 10932051:>0:r1=1; 0:r4=0; y=2; z=1; 93250312:>0:r1=0; 0:r4=1; y=2; z=1; 110420322:>0:r1=1; 0:r4=1; y=2; z=1; 118379465:>0:r1=0; 0:r4=0; y=1; z=2; 3582823:>0:r1=1; 0:r4=0; y=1; z=2; 55020776:>0:r1=0; 0:r4=1; y=1; z=2; 27000392:>0:r1=1; 0:r4=1; y=1; z=2; 9800283:>0:r1=0; 0:r4=0; y=2; z=2; 42 :>0:r1=1; 0:r4=0; y=2; z=2; 44608289:>0:r1=0; 0:r4=1; y=2; z=2; 4499996:>0:r1=1; 0:r4=1; y=2; z=2; Ok Witnesses Positive: 42, Negative: 799999958 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=2f7e7e797a32b772dba41a2c989f624e Observation X06 Sometimes 42 799999958 Time X06 171.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X07.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X07 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | lwsync ; | lwz r3,0(r4) | li r3,1 ; | | stw r3,0(r4) ; 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_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,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 X07 Allowed Histogram (8 states) 106875126:>0:r1=0; 0:r4=0; 1:r3=0; 6460 :>0:r1=1; 0:r4=0; 1:r3=0; 224178699:>0:r1=0; 0:r4=1; 1:r3=0; 50451112:>0:r1=1; 0:r4=1; 1:r3=0; 270732970:>0:r1=0; 0:r4=0; 1:r3=1; 103703020:>0:r1=1; 0:r4=0; 1:r3=1; 33995642:>0:r1=0; 0:r4=1; 1:r3=1; 210056971:>0:r1=1; 0:r4=1; 1:r3=1; Ok Witnesses Positive: 6460, Negative: 999993540 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is validated Hash=27f80466ebe5b987c02fd5b2375e9014 Observation X07 Sometimes 6460 999993540 Time X07 108.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X08.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X08 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,1 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | lwsync | lwsync ; | lwz r3,0(r4) | li r3,1 | li r3,1 ; | | stw r3,0(r4) | stw r3,0(r4) ; 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_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,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 X08 Allowed Histogram (16 states) 61528366:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 9667125:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 80586738:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 91212237:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 100292548:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 60035102:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 10329138:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 68750058:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 9537831:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 170 :>0:r1=1; 0:r4=0; 1:r3=0; z=2; 37243517:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 3118604:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 145932075:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 10560474:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 68333294:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 42872723:>0:r1=1; 0:r4=1; 1:r3=1; z=2; Ok Witnesses Positive: 170, Negative: 799999830 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is validated Hash=c693aeac120b5ebe47aca8096f1cefc4 Observation X08 Sometimes 170 799999830 Time X08 169.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X09.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X09 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,1 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | sync | lwsync ; | lwz r3,0(r4) | lwz r3,0(r4) | li r3,1 ; | | | stw r3,0(r4) ; 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_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _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 X09 Allowed Histogram (16 states) 10779823:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 262 :>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=0; 40925010:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 4110733:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 132741328:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 4031401:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 71606898:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 31802192:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 68587793:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 11090190:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 80587334:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 92480202:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 100813544:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 59328512:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 13399980:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 77714798:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; Ok Witnesses Positive: 262, Negative: 799999738 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is validated Hash=25130932b014cac34245d116a5f68876 Observation X09 Sometimes 262 799999738 Time X09 155.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X10.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X10 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,1 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | sync | lwsync ; | lwz r3,0(r4) | li r3,1 | li r3,1 ; | | stw r3,0(r4) | stw r3,0(r4) ; 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_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,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 X10 Allowed Histogram (16 states) 68219192:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 10619055:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 85527437:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 95476641:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 113744005:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 59868918:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 16522456:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 79352492:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 8692646:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 99 :>0:r1=1; 0:r4=0; 1:r3=0; z=2; 33858510:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 2447389:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 124271707:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 4182391:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 66223450:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 30993612:>0:r1=1; 0:r4=1; 1:r3=1; z=2; Ok Witnesses Positive: 99, Negative: 799999901 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is validated Hash=6da0ade67698eb3fe55496c10e533d9d Observation X10 Sometimes 99 799999901 Time X10 170.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X11.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X11 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | lwsync ; | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) ; 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_: lwz 27,0(11) _litmus_P0_1_: xor 10,27,27 _litmus_P0_2_: lwzx 28,10,9 _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 X11 Allowed Histogram (8 states) 286477889:>0:r1=0; 0:r4=0; y=1; 103670011:>0:r1=1; 0:r4=0; y=1; 52863550:>0:r1=0; 0:r4=1; y=1; 217870450:>0:r1=1; 0:r4=1; y=1; 87849382:>0:r1=0; 0:r4=0; y=2; 2891 :>0:r1=1; 0:r4=0; y=2; 206341243:>0:r1=0; 0:r4=1; y=2; 44924584:>0:r1=1; 0:r4=1; y=2; Ok Witnesses Positive: 2891, Negative: 999997109 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=2e151daaab42138b8c478ba081d896ed Observation X11 Sometimes 2891 999997109 Time X11 114.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X12.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X12 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | lwsync | lwsync ; | li r3,1 | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X12 Allowed Histogram (16 states) 104549584:>0:r1=0; 0:r4=0; y=1; z=1; 62700956:>0:r1=1; 0:r4=0; y=1; z=1; 16009680:>0:r1=0; 0:r4=1; y=1; z=1; 83026663:>0:r1=1; 0:r4=1; y=1; z=1; 52363886:>0:r1=0; 0:r4=0; y=2; z=1; 8411496:>0:r1=1; 0:r4=0; y=2; z=1; 75312296:>0:r1=0; 0:r4=1; y=2; z=1; 81157185:>0:r1=1; 0:r4=1; y=2; z=1; 143563503:>0:r1=0; 0:r4=0; y=1; z=2; 10082865:>0:r1=1; 0:r4=0; y=1; z=2; 73037544:>0:r1=0; 0:r4=1; y=1; z=2; 43783340:>0:r1=1; 0:r4=1; y=1; z=2; 7584781:>0:r1=0; 0:r4=0; y=2; z=2; 47 :>0:r1=1; 0:r4=0; y=2; z=2; 35342426:>0:r1=0; 0:r4=1; y=2; z=2; 3073748:>0:r1=1; 0:r4=1; y=2; z=2; Ok Witnesses Positive: 47, Negative: 799999953 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=449f3e0ad9111a8f4431787ea3e14c01 Observation X12 Sometimes 47 799999953 Time X12 171.95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X13.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X13 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | sync | lwsync ; | li r3,1 | lwz r3,0(r4) | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; 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_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,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_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X13 Allowed Histogram (16 states) 137024977:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 4002829:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 72457810:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 33502206:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 107022620:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 61153656:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 17509289:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 88414083:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 8799065:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 67 :>0:r1=1; 0:r4=0; 2:r3=0; y=2; 39378335:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 4073097:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 58306372:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 9066835:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 75792003:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 83496756:>0:r1=1; 0:r4=1; 2:r3=1; y=2; Ok Witnesses Positive: 67, Negative: 799999933 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is validated Hash=e039602c16d523ecfdb1a0b4937a34a6 Observation X13 Sometimes 67 799999933 Time X13 169.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X14.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X14 "Rfe DpAddrdR Fre SyncdWW Wse SyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | sync | lwsync ; | li r3,1 | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X14 Allowed Histogram (16 states) 117654162:>0:r1=0; 0:r4=0; y=1; z=1; 62643602:>0:r1=1; 0:r4=0; y=1; z=1; 23209431:>0:r1=0; 0:r4=1; y=1; z=1; 93902801:>0:r1=1; 0:r4=1; y=1; z=1; 57308658:>0:r1=0; 0:r4=0; y=2; z=1; 9161291:>0:r1=1; 0:r4=0; y=2; z=1; 80368473:>0:r1=0; 0:r4=1; y=2; z=1; 85241227:>0:r1=1; 0:r4=1; y=2; z=1; 123906451:>0:r1=0; 0:r4=0; y=1; z=2; 3854029:>0:r1=1; 0:r4=0; y=1; z=2; 70271026:>0:r1=0; 0:r4=1; y=1; z=2; 31399751:>0:r1=1; 0:r4=1; y=1; z=2; 6800194:>0:r1=0; 0:r4=0; y=2; z=2; 15 :>0:r1=1; 0:r4=0; y=2; z=2; 31873286:>0:r1=0; 0:r4=1; y=2; z=2; 2405603:>0:r1=1; 0:r4=1; y=2; z=2; Ok Witnesses Positive: 15, Negative: 799999985 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=74664d9800a1cc765c71acb315cf55f7 Observation X14 Sometimes 15 799999985 Time X14 172.08 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X15.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X15 "Rfe DpCtrlIsyncdR Fre LwSyncdWW Rfe 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 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; beq LC00 | lwsync | beq LC01 | lwsync ; LC00: | li r3,1 | LC01: | li r3,1 ; isync | stw r3,0(r4) | isync | stw r3,0(r4) ; lwz r3,0(r4) | | lwz r3,0(r4) | ; 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_: lwz 30,0(11) _litmus_P0_1_: cmpw 30,30 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 31,0(9) _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_: lwz 3,0(11) _litmus_P2_1_: cmpw 3,3 _litmus_P2_2_: beq LitLC01 _litmus_P2_3_: LitLC01: _litmus_P2_4_: isync _litmus_P2_5_: lwz 31,0(9) Test X15 Allowed Histogram (16 states) 134216294:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 8414881:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 89009168:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 51683444:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 8276592:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 120 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=0; 46833152:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 6360842:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 88518607:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 47188290:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 16273011:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 77969761:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 50902194:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 6355780:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 77107688:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 90890176:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 120, Negative: 799999880 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=a488ac47b1a88d9c3f30dcee477424e5 Observation X15 Sometimes 120 799999880 Time X15 152.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X16.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X16 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | lwsync | lwsync ; LC00: | li r3,1 | li r3,1 ; isync | stw r3,0(r4) | stw r3,0(r4) ; lwz r3,0(r4) | | ; 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_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 30,0(9) _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 X16 Allowed Histogram (8 states) 262632291:>0:r1=0; 0:r3=0; y=1; 83957150:>0:r1=1; 0:r3=0; y=1; 38582240:>0:r1=0; 0:r3=1; y=1; 201686212:>0:r1=1; 0:r3=1; y=1; 100071475:>0:r1=0; 0:r3=0; y=2; 5620 :>0:r1=1; 0:r3=0; y=2; 244748002:>0:r1=0; 0:r3=1; y=2; 68317010:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 5620, Negative: 999994380 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=7cfc2b26a1cbcdd15d0fab061a637ce4 Observation X16 Sometimes 5620 999994380 Time X16 115.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X17.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X17 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | lwsync | lwsync | lwsync ; LC00: | li r3,1 | li r3,1 | li r3,1 ; isync | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; lwz r3,0(r4) | | | ; 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_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 30,0(9) _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X17 Allowed Histogram (16 states) 90035989:>0:r1=0; 0:r3=0; y=1; z=1; 50281091:>0:r1=1; 0:r3=0; y=1; z=1; 13433863:>0:r1=0; 0:r3=1; y=1; z=1; 72110864:>0:r1=1; 0:r3=1; y=1; z=1; 59460355:>0:r1=0; 0:r3=0; y=2; z=1; 8174232:>0:r1=1; 0:r3=0; y=2; z=1; 87647233:>0:r1=0; 0:r3=1; y=2; z=1; 100290693:>0:r1=1; 0:r3=1; y=2; z=1; 122238435:>0:r1=0; 0:r3=0; y=1; z=2; 8211282:>0:r1=1; 0:r3=0; y=1; z=2; 78242826:>0:r1=0; 0:r3=1; y=1; z=2; 42473171:>0:r1=1; 0:r3=1; y=1; z=2; 9166150:>0:r1=0; 0:r3=0; y=2; z=2; 121 :>0:r1=1; 0:r3=0; y=2; z=2; 51416865:>0:r1=0; 0:r3=1; y=2; z=2; 6816830:>0:r1=1; 0:r3=1; y=2; z=2; Ok Witnesses Positive: 121, Negative: 799999879 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=8ece2ae907eaa93a2cebf24dcb08cf79 Observation X17 Sometimes 121 799999879 Time X17 169.32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X18.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X18 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | lwsync | sync | lwsync ; LC00: | li r3,1 | lwz r3,0(r4) | li r3,1 ; isync | stw r3,0(r4) | | stw r3,0(r4) ; lwz r3,0(r4) | | | ; 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_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 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_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X18 Allowed Histogram (16 states) 118020465:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 3218669:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 73282186:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 30199900:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 88345661:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 50169995:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 13552737:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 74886789:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 11058605:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 166 :>0:r1=1; 0:r3=0; 2:r3=0; y=2; 54340345:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 7278868:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 66449090:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 9282710:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 92588544:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 107325270:>0:r1=1; 0:r3=1; 2:r3=1; y=2; Ok Witnesses Positive: 166, Negative: 799999834 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is validated Hash=773f6798f908e0cd810f3e878df07bab Observation X18 Sometimes 166 799999834 Time X18 168.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X19.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X19 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | lwsync | sync | lwsync ; LC00: | li r3,1 | li r3,1 | li r3,1 ; isync | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; lwz r3,0(r4) | | | ; 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_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 30,0(9) _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X19 Allowed Histogram (16 states) 99374071:>0:r1=0; 0:r3=0; y=1; z=1; 51554063:>0:r1=1; 0:r3=0; y=1; z=1; 20725240:>0:r1=0; 0:r3=1; y=1; z=1; 79133297:>0:r1=1; 0:r3=1; y=1; z=1; 67618851:>0:r1=0; 0:r3=0; y=2; z=1; 9312306:>0:r1=1; 0:r3=0; y=2; z=1; 101055413:>0:r1=0; 0:r3=1; y=2; z=1; 111538509:>0:r1=1; 0:r3=1; y=2; z=1; 105881255:>0:r1=0; 0:r3=0; y=1; z=2; 2987386:>0:r1=1; 0:r3=0; y=1; z=2; 65647855:>0:r1=0; 0:r3=1; y=1; z=2; 27138523:>0:r1=1; 0:r3=1; y=1; z=2; 8860616:>0:r1=0; 0:r3=0; y=2; z=2; 54 :>0:r1=1; 0:r3=0; y=2; z=2; 44488417:>0:r1=0; 0:r3=1; y=2; z=2; 4684144:>0:r1=1; 0:r3=1; y=2; z=2; Ok Witnesses Positive: 54, Negative: 799999946 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=811f0a85dc5f811c7436b53d2ca9c449 Observation X19 Sometimes 54 799999946 Time X19 171.04 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X20.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X20 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | sync | lwsync ; LC00: | lwz r3,0(r4) | li r3,1 ; isync | | stw r3,0(r4) ; lwz r3,0(r4) | | ; 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_: lwz 30,0(11) _litmus_P0_1_: cmpw 30,30 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 31,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 X20 Allowed Histogram (8 states) 104807617:>0:r1=0; 0:r3=0; 1:r3=0; 8033 :>0:r1=1; 0:r3=0; 1:r3=0; 230864670:>0:r1=0; 0:r3=1; 1:r3=0; 49626937:>0:r1=1; 0:r3=1; 1:r3=0; 265991127:>0:r1=0; 0:r3=0; 1:r3=1; 91828623:>0:r1=1; 0:r3=0; 1:r3=1; 42063387:>0:r1=0; 0:r3=1; 1:r3=1; 214809606:>0:r1=1; 0:r3=1; 1:r3=1; Ok Witnesses Positive: 8033, Negative: 999991967 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is validated Hash=0c99e9e00ef12798cd94e468d7533fcb Observation X20 Sometimes 8033 999991967 Time X20 108.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X21.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X21 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,1 | li r1,2 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | sync | lwsync | lwsync ; LC00: | lwz r3,0(r4) | li r3,1 | li r3,1 ; isync | | stw r3,0(r4) | stw r3,0(r4) ; lwz r3,0(r4) | | | ; 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_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 30,0(9) _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,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 X21 Allowed Histogram (16 states) 60224284:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 8672016:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 83505054:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 91627044:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 97726656:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 54520189:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 13435831:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 72348978:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 9305763:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 255 :>0:r1=1; 0:r3=0; 1:r3=0; z=2; 37278499:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 3323808:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 132162819:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 9645735:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 81641073:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 44581996:>0:r1=1; 0:r3=1; 1:r3=1; z=2; Ok Witnesses Positive: 255, Negative: 799999745 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is validated Hash=10b56f844965b778138fc256080a6cb2 Observation X21 Sometimes 255 799999745 Time X21 170.27 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X22.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X22 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,1 | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | sync | sync | lwsync ; LC00: | lwz r3,0(r4) | lwz r3,0(r4) | li r3,1 ; isync | | | stw r3,0(r4) ; lwz r3,0(r4) | | | ; 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_: lwz 30,0(11) _litmus_P0_1_: cmpw 30,30 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 31,0(9) _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 X22 Allowed Histogram (16 states) 10372139:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 130 :>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=0; 41838064:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 4331681:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 119286314:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 3292493:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 85423659:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 32519429:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 65493686:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 9393739:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 84138386:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 93372308:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 97637822:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 53323082:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 17694588:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 81882480:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; Ok Witnesses Positive: 130, Negative: 799999870 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is validated Hash=e7fc832a2e4b347328216cfab07885d9 Observation X22 Sometimes 130 799999870 Time X22 154.75 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X23.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X23 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,1 | li r1,2 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | sync | sync | lwsync ; LC00: | lwz r3,0(r4) | li r3,1 | li r3,1 ; isync | | stw r3,0(r4) | stw r3,0(r4) ; lwz r3,0(r4) | | | ; 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_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 30,0(9) _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,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 X23 Allowed Histogram (16 states) 66269747:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 9687082:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 88882149:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 96789656:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 109018169:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 55093285:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 21929419:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 83437295:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 8282553:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 138 :>0:r1=1; 0:r3=0; 1:r3=0; z=2; 33787893:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 2679618:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 110881670:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 3425094:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 78283105:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 31553127:>0:r1=1; 0:r3=1; 1:r3=1; z=2; Ok Witnesses Positive: 138, Negative: 799999862 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is validated Hash=86fcf34749ab0aa370ea66e6893791a0 Observation X23 Sometimes 138 799999862 Time X23 170.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X24.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X24 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | sync | lwsync ; LC00: | li r3,1 | li r3,1 ; isync | stw r3,0(r4) | stw r3,0(r4) ; lwz r3,0(r4) | | ; 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_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 30,0(9) _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 X24 Allowed Histogram (8 states) 282860433:>0:r1=0; 0:r3=0; y=1; 89149297:>0:r1=1; 0:r3=0; y=1; 66192970:>0:r1=0; 0:r3=1; y=1; 220889666:>0:r1=1; 0:r3=1; y=1; 86361621:>0:r1=0; 0:r3=0; y=2; 3353 :>0:r1=1; 0:r3=0; y=2; 210462966:>0:r1=0; 0:r3=1; y=2; 44079694:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 3353, Negative: 999996647 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=1a78bce42911eadebdb22805402de8eb Observation X24 Sometimes 3353 999996647 Time X24 114.04 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X25.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X25 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | sync | lwsync | lwsync ; LC00: | li r3,1 | li r3,1 | li r3,1 ; isync | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; lwz r3,0(r4) | | | ; 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_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 30,0(9) _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X25 Allowed Histogram (16 states) 102009377:>0:r1=0; 0:r3=0; y=1; z=1; 56071308:>0:r1=1; 0:r3=0; y=1; z=1; 19755274:>0:r1=0; 0:r3=1; y=1; z=1; 85149796:>0:r1=1; 0:r3=1; y=1; z=1; 51185593:>0:r1=0; 0:r3=0; y=2; z=1; 7405114:>0:r1=1; 0:r3=0; y=2; z=1; 78495995:>0:r1=0; 0:r3=1; y=2; z=1; 82181053:>0:r1=1; 0:r3=1; y=2; z=1; 130232948:>0:r1=0; 0:r3=0; y=1; z=2; 9419364:>0:r1=1; 0:r3=0; y=1; z=2; 85979525:>0:r1=0; 0:r3=1; y=1; z=2; 45719729:>0:r1=1; 0:r3=1; y=1; z=2; 7231583:>0:r1=0; 0:r3=0; y=2; z=2; 73 :>0:r1=1; 0:r3=0; y=2; z=2; 35866611:>0:r1=0; 0:r3=1; y=2; z=2; 3296657:>0:r1=1; 0:r3=1; y=2; z=2; Ok Witnesses Positive: 73, Negative: 799999927 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=629e26a0c6f613b14043edf57727b702 Observation X25 Sometimes 73 799999927 Time X25 171.85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X26.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X26 "Rfe 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 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | sync | sync | lwsync ; LC00: | li r3,1 | lwz r3,0(r4) | li r3,1 ; isync | stw r3,0(r4) | | stw r3,0(r4) ; lwz r3,0(r4) | | | ; 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_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 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_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X26 Allowed Histogram (16 states) 123484316:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 3472678:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 87796507:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 34768664:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 102693290:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 55388205:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 22820658:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 92480023:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 8214793:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 37 :>0:r1=1; 0:r3=0; 2:r3=0; y=2; 40141980:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 4285749:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 54120385:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 7842091:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 78526510:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 83964114:>0:r1=1; 0:r3=1; 2:r3=1; y=2; Ok Witnesses Positive: 37, Negative: 799999963 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is validated Hash=54da285ce144acabc337e28ea8958874 Observation X26 Sometimes 37 799999963 Time X26 169.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X27.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X27 "Rfe DpCtrldW Wse LwSyncdWW Rfe 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 ; lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; beq LC00 | lwsync | beq LC01 | lwsync ; LC00: | li r3,1 | LC01: | li r3,1 ; li r3,1 | stw r3,0(r4) | isync | stw r3,0(r4) ; stw r3,0(r4) | | lwz r3,0(r4) | ; 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_: lwz 3,0(11) _litmus_P0_1_: cmpw 3,3 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _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_: lwz 28,0(11) _litmus_P2_1_: cmpw 28,28 _litmus_P2_2_: beq LitLC01 _litmus_P2_3_: LitLC01: _litmus_P2_4_: isync _litmus_P2_5_: lwz 30,0(9) Test X27 Allowed Histogram (16 states) 87367854:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 49941022:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 47365187:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 5913158:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 13827274:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 76413499:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 75227358:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 92025637:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 137237743:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 8850546:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 9619603:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 68 :>0:r1=1; 2:r1=1; 2:r3=0; x=2; 94570981:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 42018532:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 55156183:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 4465355:>0:r1=1; 2:r1=1; 2:r3=1; x=2; Ok Witnesses Positive: 68, Negative: 799999932 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=ffa63368caa391807dee9905d20510c6 Observation X27 Sometimes 68 799999932 Time X27 164.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X28.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X28 "Rfe LwSyncdRW Wse LwSyncdWW Rfe 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 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ; | li r3,1 | lwsync | lwzx r4,r3,r5 ; | stw r3,0(r4) | li r3,1 | ; | | stw r3,0(r4) | ; 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_: lwz 28,0(11) _litmus_P3_1_: xor 10,28,28 _litmus_P3_2_: lwzx 30,10,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 X28 Allowed Histogram (16 states) 69360668:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 93952296:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 43924458:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 16805203:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 3568480:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 83101860:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 53025520:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 127888004:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 125598739:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 14307107:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 7387945:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 222 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 64636289:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 49431582:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 41337987:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 5673640:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 222, Negative: 799999778 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=4adca431a2784b4aa9df91b1fc3b1666 Observation X28 Sometimes 222 799999778 Time X28 149.87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X29.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X29 "Rfe LwSyncdRW Wse LwSyncdWW Rfe 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 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | cmpw r1,r1 ; | li r3,1 | lwsync | beq LC00 ; | stw r3,0(r4) | li r3,1 | LC00: ; | | stw r3,0(r4) | isync ; | | | lwz r3,0(r4) ; 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_: lwz 28,0(11) _litmus_P3_1_: cmpw 28,28 _litmus_P3_2_: beq LitLC00 _litmus_P3_3_: LitLC00: _litmus_P3_4_: isync _litmus_P3_5_: lwz 30,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 X29 Allowed Histogram (16 states) 66678388:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 89320728:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 40379663:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 15052922:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 7689232:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 89570713:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 54826759:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 128025002:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 116013269:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 13560569:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 6489287:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 284 :>1:r1=1; 3:r1=1; 3:r3=0; x=2; 74090235:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 50194351:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 42014139:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 6094459:>1:r1=1; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 284, Negative: 799999716 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=cd58719fd03bc8a841de06004867cb05 Observation X29 Sometimes 284 799999716 Time X29 150.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X30.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X30 "Rfe PodRW Wse LwSyncdWW Rfe 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 ; lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) | li r1,1 ; li r3,1 | stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) ; stw r3,0(r4) | lwsync | lwzx r4,r3,r5 | lwsync ; | li r3,1 | | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; 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_: lwz 3,0(11) _litmus_P0_1_: li 30,1 _litmus_P0_2_: 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_: lwz 28,0(11) _litmus_P2_1_: xor 10,28,28 _litmus_P2_2_: lwzx 30,10,9 Test X30 Allowed Histogram (16 states) 87858082:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 54065946:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 52064302:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 6918809:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 8204764:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 71733429:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 72112657:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 91750516:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 154641022:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 9778351:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 10975619:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 74 :>0:r1=1; 2:r1=1; 2:r4=0; x=2; 79543258:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 42477866:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 53462476:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 4412829:>0:r1=1; 2:r1=1; 2:r4=1; x=2; Ok Witnesses Positive: 74, Negative: 799999926 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is validated Hash=a0f55fa2291a072f015a1f0b83d20074 Observation X30 Sometimes 74 799999926 Time X30 163.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X31.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X31 "Rfe PodRW Wse LwSyncdWW Rfe 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 ; lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) | li r1,1 ; li r3,1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; stw r3,0(r4) | lwsync | beq LC00 | lwsync ; | li r3,1 | LC00: | li r3,1 ; | stw r3,0(r4) | isync | stw r3,0(r4) ; | | lwz r3,0(r4) | ; 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_: lwz 3,0(11) _litmus_P0_1_: li 30,1 _litmus_P0_2_: 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_: lwz 28,0(11) _litmus_P2_1_: cmpw 28,28 _litmus_P2_2_: beq LitLC00 _litmus_P2_3_: LitLC00: _litmus_P2_4_: isync _litmus_P2_5_: lwz 30,0(9) Test X31 Allowed Histogram (16 states) 84829462:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 49880646:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 47607430:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 5953298:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 13327952:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 76903525:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 74701248:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 91987058:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 139150913:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 8812141:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 9643611:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 75 :>0:r1=1; 2:r1=1; 2:r3=0; x=2; 94943418:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 42817030:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 54836529:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 4605664:>0:r1=1; 2:r1=1; 2:r3=1; x=2; Ok Witnesses Positive: 75, Negative: 799999925 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=ffb6dc3e13fae7c7e7811955e241147b Observation X31 Sometimes 75 799999925 Time X31 166.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X32.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X32 "Rfe SyncdRR Fre LwSyncdWW Rfe 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 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | xor r3,r1,r1 ; | lwz r3,0(r4) | lwsync | lwzx r4,r3,r5 ; | | li r3,1 | ; | | stw r3,0(r4) | ; 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_: lwz 30,0(11) _litmus_P3_1_: xor 10,30,30 _litmus_P3_2_: lwzx 31,10,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 X32 Allowed Histogram (16 states) 107757727:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 16088722:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 81881698:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 98358944:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 2968555:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 348 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=0; 47535481:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 15642122:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 58014873:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 45435355:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 7183181:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 87141759:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 30430670:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 4898651:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 63960459:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 132701455:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; Ok Witnesses Positive: 348, Negative: 799999652 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=abdf662fb230128532b66df78e4a75f1 Observation X32 Sometimes 348 799999652 Time X32 139.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X33.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X33 "Rfe SyncdRR Fre LwSyncdWW Rfe 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 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | cmpw r1,r1 ; | lwz r3,0(r4) | lwsync | beq LC00 ; | | li r3,1 | LC00: ; | | stw r3,0(r4) | isync ; | | | lwz r3,0(r4) ; 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_: lwz 3,0(11) _litmus_P3_1_: cmpw 3,3 _litmus_P3_2_: beq LitLC00 _litmus_P3_3_: LitLC00: _litmus_P3_4_: isync _litmus_P3_5_: lwz 31,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 X33 Allowed Histogram (16 states) 102296208:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 14110336:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 78067120:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 89122460:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 2538768:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 431 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; 43317823:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 13479060:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 70181051:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 47051046:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 12988246:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 97249052:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 27023045:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 5174896:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 65727739:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 131672719:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; Ok Witnesses Positive: 431, Negative: 799999569 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=c86889a7cdc1c89457a71c414046d8c0 Observation X33 Sometimes 431 799999569 Time X33 139.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X34.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X34 "Rfe SyncdRW Wse LwSyncdWW Rfe 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 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | xor r3,r1,r1 ; | li r3,1 | lwsync | lwzx r4,r3,r5 ; | stw r3,0(r4) | li r3,1 | ; | | stw r3,0(r4) | ; 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_: lwz 28,0(11) _litmus_P3_1_: xor 10,28,28 _litmus_P3_2_: lwzx 30,10,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 X34 Allowed Histogram (16 states) 81483318:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 102448033:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 46829520:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 17716718:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 8412067:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 89676598:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 62345473:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 136511360:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 103031904:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 14691312:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 3111480:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 158 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 60291810:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 42517573:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 26807231:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 4125445:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 158, Negative: 799999842 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=8db91522dc421fe43a7baf7aff0de837 Observation X34 Sometimes 158 799999842 Time X34 150.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X35.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X35 "Rfe SyncdRW Wse LwSyncdWW Rfe 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 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | cmpw r1,r1 ; | li r3,1 | lwsync | beq LC00 ; | stw r3,0(r4) | li r3,1 | LC00: ; | | stw r3,0(r4) | isync ; | | | lwz r3,0(r4) ; 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_: lwz 28,0(11) _litmus_P3_1_: cmpw 28,28 _litmus_P3_2_: beq LitLC00 _litmus_P3_3_: LitLC00: _litmus_P3_4_: isync _litmus_P3_5_: lwz 30,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 X35 Allowed Histogram (16 states) 76944466:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 95273269:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 43315600:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 15919180:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 13135140:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 97744429:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 64484844:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 136068164:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 98362488:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 13625977:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 2762446:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 200 :>1:r1=1; 3:r1=1; 3:r3=0; x=2; 66971477:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 43494714:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 27424076:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 4473530:>1:r1=1; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 200, Negative: 799999800 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=00744a65cf189719eb1309a79c27a2ca Observation X35 Sometimes 200 799999800 Time X35 151.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y00.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y00 "Rf*e DpAddrdR Fre LwSyncdWW Rf*e DpAddrdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | DIY01: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | xor r3,r1,r1 | lwsync ; lwzx r4,r3,r5 | li r3,1 | lwzx r4,r3,r5 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stwcx. r1,r0,r2 | stw r3,0(r4) ; bne DIY00 | | bne DIY01 | ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: xor 10,30,30 _litmus_P0_3_: lwzx 31,10,9 _litmus_P0_4_: stwcx. 30,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: LitDIY01: _litmus_P2_1_: lwarx 30,0,11 _litmus_P2_2_: xor 10,30,30 _litmus_P2_3_: lwzx 31,10,9 _litmus_P2_4_: stwcx. 30,0,11 _litmus_P2_5_: bne LitDIY01 Test Y00 Allowed Histogram (15 states) 120730221:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 16781280:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 45955363:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 74607827:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 16765488:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 48020909:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 17806611:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 43973802:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 48032759:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 1623070:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 46864745:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 75049127:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 17742096:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 46790091:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 179256611:>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 155.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 105006080:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 15445342:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 45440979:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 70394115:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 16969648:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 40294702:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 12552834:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 42745806:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 46285536:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 1461028:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 41671744:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 91076593:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 20821778:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 55662709:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 194171106:>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 156.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 75166373:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 61544741:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 4008625:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 83435386:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 55891269:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 10313360:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 49813002:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 161089017:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 117649423:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 11784858:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 40400119:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 58625119:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 9271449:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 45532301:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 15474958:>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 168.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 229128045:>0:r1=0; 0:r4=0; y=1; 109386850:>0:r1=1; 0:r4=0; y=1; 8786250:>0:r1=0; 0:r4=1; y=1; 240817625:>0:r1=1; 0:r4=1; y=1; 100634689:>0:r1=0; 0:r4=0; y=2; 153089612:>0:r1=0; 0:r4=1; y=2; 158156929:>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 116.40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 78258512:>0:r1=0; 0:r4=0; y=1; z=1; 59549663:>0:r1=1; 0:r4=0; y=1; z=1; 3896657:>0:r1=0; 0:r4=1; y=1; z=1; 87195085:>0:r1=1; 0:r4=1; y=1; z=1; 53882946:>0:r1=0; 0:r4=0; y=2; z=1; 9478351:>0:r1=1; 0:r4=0; y=2; z=1; 45833881:>0:r1=0; 0:r4=1; y=2; z=1; 144161529:>0:r1=1; 0:r4=1; y=2; z=1; 108988473:>0:r1=0; 0:r4=0; y=1; z=2; 15178960:>0:r1=1; 0:r4=0; y=1; z=2; 50382726:>0:r1=0; 0:r4=1; y=1; z=2; 76082625:>0:r1=1; 0:r4=1; y=1; z=2; 9340929:>0:r1=0; 0:r4=0; y=2; z=2; 41427011:>0:r1=0; 0:r4=1; y=2; z=2; 16342652:>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 170.87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 114347798:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 9621618:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 47031956:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 57312967:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 76332440:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 62515330:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 5464455:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 87065081:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 10650786:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 44766138:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 16698831:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 55695345:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 11309721:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 49124378:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 152063156:>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 170.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 86969839:>0:r1=0; 0:r4=0; y=1; z=1; 63874046:>0:r1=1; 0:r4=0; y=1; z=1; 8219539:>0:r1=0; 0:r4=1; y=1; z=1; 95173350:>0:r1=1; 0:r4=1; y=1; z=1; 57685032:>0:r1=0; 0:r4=0; y=2; z=1; 11046642:>0:r1=1; 0:r4=0; y=2; z=1; 53409722:>0:r1=0; 0:r4=1; y=2; z=1; 160471641:>0:r1=1; 0:r4=1; y=2; z=1; 101245123:>0:r1=0; 0:r4=0; y=1; z=2; 9136462:>0:r1=1; 0:r4=0; y=1; z=2; 43405325:>0:r1=0; 0:r4=1; y=1; z=2; 51835584:>0:r1=1; 0:r4=1; y=1; z=2; 8289497:>0:r1=0; 0:r4=0; y=2; z=2; 37999938:>0:r1=0; 0:r4=1; y=2; z=2; 11238260:>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 172.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 108800121:>0:r1=0; 0:r4=0; 1:r3=0; 154258893:>0:r1=0; 0:r4=1; 1:r3=0; 125538917:>0:r1=1; 0:r4=1; 1:r3=0; 221381182:>0:r1=0; 0:r4=0; 1:r3=1; 116833359:>0:r1=1; 0:r4=0; 1:r3=1; 17960261:>0:r1=0; 0:r4=1; 1:r3=1; 255227267:>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 109.70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 55083842:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 10993444:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 49570895:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 129633706:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 77745277:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 66482211:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 5746431:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 87801267:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 9772750:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 32150225:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 8343866:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 116277185:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 17577206:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 53891402:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 78930293:>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 170.81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 10582412:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 35390598:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 10416627:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 113287954:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 10028715:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 55063541:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 63851262:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 57045783:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 11698863:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 50335433:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 131732034:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 76944202:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 68557187:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 7810842:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 97254547:>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 156.67 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 58323971:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 12267380:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 54081721:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 134806175:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 87141780:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 71046976:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 9797330:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 101389477:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 8443317:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 29437611:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 6648226:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 106221174:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 9852685:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 51776307:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 58765870:>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 171.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y11.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y11 "Rf*e DpAddrdR Fre SyncdWW Wse LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 27,0,11 _litmus_P0_2_: xor 10,27,27 _litmus_P0_3_: lwzx 28,10,9 _litmus_P0_4_: stwcx. 27,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y11 Allowed Histogram (7 states) 240944373:>0:r1=0; 0:r4=0; y=1; 117410467:>0:r1=1; 0:r4=0; y=1; 25795121:>0:r1=0; 0:r4=1; y=1; 269107907:>0:r1=1; 0:r4=1; y=1; 89116884:>0:r1=0; 0:r4=0; y=2; 143620633:>0:r1=0; 0:r4=1; y=2; 114004615:>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 116.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 84830149:>0:r1=0; 0:r4=0; y=1; z=1; 66444012:>0:r1=1; 0:r4=0; y=1; z=1; 7857639:>0:r1=0; 0:r4=1; y=1; z=1; 103424681:>0:r1=1; 0:r4=1; y=1; z=1; 47843405:>0:r1=0; 0:r4=0; y=2; z=1; 8738833:>0:r1=1; 0:r4=0; y=2; z=1; 46553621:>0:r1=0; 0:r4=1; y=2; z=1; 117366490:>0:r1=1; 0:r4=1; y=2; z=1; 114425243:>0:r1=0; 0:r4=0; y=1; z=2; 17194722:>0:r1=1; 0:r4=0; y=1; z=2; 57283307:>0:r1=0; 0:r4=1; y=1; z=2; 81304387:>0:r1=1; 0:r4=1; y=1; z=2; 7689040:>0:r1=0; 0:r4=0; y=2; z=2; 30856315:>0:r1=0; 0:r4=1; y=2; z=2; 8188156:>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 171.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 118072584:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 10346613:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 57314225:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 65232123:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 83586577:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 69378263:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 9611258:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 109434562:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 8605031:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 34394845:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 9779178:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 48679726:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 9735332:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 48098861:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 117730822:>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 170.74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 94136247:>0:r1=0; 0:r4=0; y=1; z=1; 70258544:>0:r1=1; 0:r4=0; y=1; z=1; 12419496:>0:r1=0; 0:r4=1; y=1; z=1; 118772441:>0:r1=1; 0:r4=1; y=1; z=1; 50648809:>0:r1=0; 0:r4=0; y=2; z=1; 9465535:>0:r1=1; 0:r4=0; y=2; z=1; 51122837:>0:r1=0; 0:r4=1; y=2; z=1; 123528573:>0:r1=1; 0:r4=1; y=2; z=1; 104481067:>0:r1=0; 0:r4=0; y=1; z=2; 9768508:>0:r1=1; 0:r4=0; y=1; z=2; 54095630:>0:r1=0; 0:r4=1; y=1; z=2; 59916709:>0:r1=1; 0:r4=1; y=1; z=2; 6685986:>0:r1=0; 0:r4=0; y=2; z=2; 28156290:>0:r1=0; 0:r4=1; y=2; z=2; 6543328:>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 174.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 93388095:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 15794222:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 42969886:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 85724531:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 15685109:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 39898124:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 14994656:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 41552672:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 39979841:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 1352292:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 50143213:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 84850788:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 15093732:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 50155050:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 208417789:>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 157.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 225192923:>0:r1=0; 0:r3=0; y=1; 88045698:>0:r1=1; 0:r3=0; y=1; 9064711:>0:r1=0; 0:r3=1; y=1; 265572626:>0:r1=1; 0:r3=1; y=1; 96230813:>0:r1=0; 0:r3=0; y=2; 143662375:>0:r1=0; 0:r3=1; y=2; 172230854:>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 117.01 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 76029403:>0:r1=0; 0:r3=0; y=1; z=1; 50800079:>0:r1=1; 0:r3=0; y=1; z=1; 3951197:>0:r1=0; 0:r3=1; y=1; z=1; 102873868:>0:r1=1; 0:r3=1; y=1; z=1; 50569551:>0:r1=0; 0:r3=0; y=2; z=1; 6519413:>0:r1=1; 0:r3=0; y=2; z=1; 42353096:>0:r1=0; 0:r3=1; y=2; z=1; 151618817:>0:r1=1; 0:r3=1; y=2; z=1; 97797441:>0:r1=0; 0:r3=0; y=1; z=2; 14015919:>0:r1=1; 0:r3=0; y=1; z=2; 49154491:>0:r1=0; 0:r3=1; y=1; z=2; 89391303:>0:r1=1; 0:r3=1; y=1; z=2; 8382040:>0:r1=0; 0:r3=0; y=2; z=2; 38624473:>0:r1=0; 0:r3=1; y=2; z=2; 17918909:>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 173.86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 99880976:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 10294951:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 45498245:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 71365918:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 72514395:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 52479889:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 4788374:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 102338908:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 9658258:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 42610701:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 19871028:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 52640132:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 8109356:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 44176413:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 163772456:>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 171.87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 82191720:>0:r1=0; 0:r3=0; y=1; z=1; 53926104:>0:r1=1; 0:r3=0; y=1; z=1; 7236210:>0:r1=0; 0:r3=1; y=1; z=1; 112113303:>0:r1=1; 0:r3=1; y=1; z=1; 53656641:>0:r1=0; 0:r3=0; y=2; z=1; 7680090:>0:r1=1; 0:r3=0; y=2; z=1; 48917702:>0:r1=0; 0:r3=1; y=2; z=1; 168978748:>0:r1=1; 0:r3=1; y=2; z=1; 91231964:>0:r1=0; 0:r3=0; y=1; z=2; 9406015:>0:r1=1; 0:r3=0; y=1; z=2; 42987011:>0:r1=0; 0:r3=1; y=1; z=2; 64067968:>0:r1=1; 0:r3=1; y=1; z=2; 7469455:>0:r1=0; 0:r3=0; y=2; z=2; 36904248:>0:r1=0; 0:r3=1; y=2; z=2; 13232821:>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 175.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 102643242:>0:r1=0; 0:r3=0; 1:r3=0; 146997732:>0:r1=0; 0:r3=1; 1:r3=0; 137467768:>0:r1=1; 0:r3=1; 1:r3=0; 216438059:>0:r1=0; 0:r3=0; 1:r3=1; 93392567:>0:r1=1; 0:r3=0; 1:r3=1; 11821843:>0:r1=0; 0:r3=1; 1:r3=1; 291238789:>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 110.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 52988974:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 7236218:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 43224933:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 142666030:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 75096831:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 55724585:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 4474409:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 104961028:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 9098442:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 31252266:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 10077039:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 100376798:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 15893740:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 52975658:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 93953049:>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 172.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9937079:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 33865375:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 12685735:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 98106549:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 11068339:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 52314949:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 79286775:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 54892547:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 8244690:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 43394785:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 145871264:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 72089527:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 58138079:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 5994256:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 114110051:>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 158.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 55625910:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 7808415:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 47194194:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 149282750:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 81012130:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 58981285:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 7869922:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 120478092:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 8033528:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 28939404:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 8385092:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 91753669:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 10146073:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 51217930:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 73271606:>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 173.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 235826868:>0:r1=0; 0:r3=0; y=1; 93950079:>0:r1=1; 0:r3=0; y=1; 19742116:>0:r1=0; 0:r3=1; y=1; 305283522:>0:r1=1; 0:r3=1; y=1; 85216627:>0:r1=0; 0:r3=0; y=2; 136498264:>0:r1=0; 0:r3=1; y=2; 123482524:>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 116.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 81967285:>0:r1=0; 0:r3=0; y=1; z=1; 56024236:>0:r1=1; 0:r3=0; y=1; z=1; 6578691:>0:r1=0; 0:r3=1; y=1; z=1; 122936916:>0:r1=1; 0:r3=1; y=1; z=1; 44795698:>0:r1=0; 0:r3=0; y=2; z=1; 5916580:>0:r1=1; 0:r3=0; y=2; z=1; 41309469:>0:r1=0; 0:r3=1; y=2; z=1; 126206027:>0:r1=1; 0:r3=1; y=2; z=1; 101652591:>0:r1=0; 0:r3=0; y=1; z=2; 15744289:>0:r1=1; 0:r3=0; y=1; z=2; 54851853:>0:r1=0; 0:r3=1; y=1; z=2; 95576036:>0:r1=1; 0:r3=1; y=1; z=2; 7028560:>0:r1=0; 0:r3=0; y=2; z=2; 29834114:>0:r1=0; 0:r3=1; y=2; z=2; 9577655:>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 175.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 103066266:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 10989389:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 54958552:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 80833985:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 78616277:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 57993457:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 7510795:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 129449600:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 7826426:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 32917339:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 12005767:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 46038806:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 6640159:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 41743568:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 129409614:>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 172.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y27.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y27 "Rf*e DpCtrldW Wse LwSyncdWW Rf*e DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,2 | DIY02: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; stwcx. r1,r0,r2 | lwsync | cmpw r1,r1 | lwsync ; bne DIY00 | li r3,1 | beq LC03 | li r3,1 ; cmpw r1,r1 | stw r3,0(r4) | LC03: | stw r3,0(r4) ; beq LC01 | | isync | ; LC01: | | lwz r3,0(r4) | ; li r3,1 | | stwcx. r1,r0,r2 | ; stw r3,0(r4) | | bne DIY02 | ; exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 3,0,11 _litmus_P0_2_: stwcx. 3,0,11 _litmus_P0_3_: bne LitDIY00 _litmus_P0_4_: cmpw 3,3 _litmus_P0_5_: beq LitLC01 _litmus_P0_6_: LitLC01: _litmus_P0_7_: li 30,1 _litmus_P0_8_: stw 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: LitDIY02: _litmus_P2_1_: lwarx 28,0,11 _litmus_P2_2_: cmpw 28,28 _litmus_P2_3_: beq LitLC03 _litmus_P2_4_: LitLC03: _litmus_P2_5_: isync _litmus_P2_6_: lwz 30,0(9) _litmus_P2_7_: stwcx. 28,0,11 _litmus_P2_8_: bne LitDIY02 Test Y27 Allowed Histogram (15 states) 73116161:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 51656742:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 52236787:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 7266556:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 3360256:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 44671883:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 97693933:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 171129675:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 104382531:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 7964364:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 12536251:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 39607901:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 44334775:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 72088116:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 17954069:>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 168.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 54581583:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 82826832:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 48499220:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 18408971:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 1803695:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 43834722:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 66160514:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 177691754:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 100445876:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 14372018:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 14136976:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 40586849:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 40956927:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 81114517:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 14579546:>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 151.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 52700890:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 81384226:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 41824566:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 14059303:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 1847388:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 40553649:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 73497991:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 187029078:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 90566840:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 13870018:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 14126929:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 40114930:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 39704624:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 92178970:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 16540598:>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 152.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 76106756:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 54369668:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 61487063:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 9995948:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 3796174:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 49864812:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 84182259:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 159657940:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 118891785:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 9201126:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 11880924:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 39217446:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 46730984:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 58625645:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 15991470:>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 167.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 73618446:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 51686030:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 51980360:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 7177116:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 3385231:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 44821650:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 97516865:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 170839922:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 104662704:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 8085549:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 12259913:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 39543572:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 44830311:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 71237280:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 18355051:>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 168.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 97773390:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 13706413:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 66887952:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 75148091:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 8453758:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 55972795:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 16649923:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 39144651:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 38374201:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 4168001:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 47075822:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 60486120:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 12721285:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 77848034:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 185589564:>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 142.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 89792519:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 12653174:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 61546259:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 71432825:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 9115190:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 49140443:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 12178386:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 38921581:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 37930360:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 3497785:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 41876878:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 69585089:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 14679004:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 90549351:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 197101156:>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 180.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) 63905758:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 83358749:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 54574933:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 18896673:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 4320061:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 48793206:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 77147173:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 189775104:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 93904361:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 13255038:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 8408990:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 37439703:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 36339293:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 59196985:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 10683973:>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 152.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 58728446:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 81291921:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 48494835:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 14327834:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 3820084:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 44689898:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 88483894:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 199543783:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 85896036:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 12672544:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 8870612:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 37889068:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 35855088:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 67214477:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 12221480:>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 152.78 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 dim jan 23 23:53:18 CET 2011