dim jan 23 13:12:05 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) 127048802:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 11438405:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 83828911:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 55979379:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 11532114:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 658 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=0; 45591373:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 7551797:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 84394709:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 45527763:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 16632048:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 72859905:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 54766470:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 7383506:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 71487873:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 103976287:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; Ok Witnesses Positive: 658, Negative: 799999342 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is validated Hash=6559e19d9e37619f3f8bf433a5805105 Observation X00 Sometimes 658 799999342 Time X00 148.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 112144671:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 9196296:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 78770328:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 47801598:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 9258117:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 667 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=0; 39770744:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 6373960:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 94109106:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 47786625:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 21526316:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 80116651:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 58187811:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 8382114:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 77850436:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 108724560:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 667, Negative: 799999333 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=2dd158f1ef0b66595a56ff21c6e00a13 Observation X01 Sometimes 667 799999333 Time X01 149.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 88843148:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 49092260:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 17804970:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 78535503:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 52269681:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 6956732:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 69237801:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 100105982:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 124137844:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 13193127:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 85543753:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 57254255:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 10359055:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 169 :>0:r1=1; 0:r4=0; 2:r1=1; z=2; 40652566:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 6013154:>0:r1=1; 0:r4=1; 2:r1=1; z=2; Ok Witnesses Positive: 169, Negative: 799999831 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is validated Hash=ddaab862216f1c9eafeceba074a24928 Observation X02 Sometimes 169 799999831 Time X02 160.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 260740783:>0:r1=0; 0:r4=0; y=1; 88670035:>0:r1=1; 0:r4=0; y=1; 42037539:>0:r1=0; 0:r4=1; y=1; 231665945:>0:r1=1; 0:r4=1; y=1; 98657901:>0:r1=0; 0:r4=0; y=2; 10806 :>0:r1=1; 0:r4=0; y=2; 212716779:>0:r1=0; 0:r4=1; y=2; 65500212:>0:r1=1; 0:r4=1; y=2; Ok Witnesses Positive: 10806, Negative: 999989194 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=979eb45568765c8b5bb24cb8beb2a694 Observation X03 Sometimes 10806 999989194 Time X03 104.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 97418409:>0:r1=0; 0:r4=0; y=1; z=1; 52297029:>0:r1=1; 0:r4=0; y=1; z=1; 19109435:>0:r1=0; 0:r4=1; y=1; z=1; 90332802:>0:r1=1; 0:r4=1; y=1; z=1; 58400390:>0:r1=0; 0:r4=0; y=2; z=1; 7971727:>0:r1=1; 0:r4=0; y=2; z=1; 73053143:>0:r1=0; 0:r4=1; y=2; z=1; 106682328:>0:r1=1; 0:r4=1; y=2; z=1; 106624811:>0:r1=0; 0:r4=0; y=1; z=2; 7129482:>0:r1=1; 0:r4=0; y=1; z=2; 80100049:>0:r1=0; 0:r4=1; y=1; z=2; 47090439:>0:r1=1; 0:r4=1; y=1; z=2; 9815283:>0:r1=0; 0:r4=0; y=2; z=2; 204 :>0:r1=1; 0:r4=0; y=2; z=2; 37905845:>0:r1=0; 0:r4=1; y=2; z=2; 6068624:>0:r1=1; 0:r4=1; y=2; z=2; Ok Witnesses Positive: 204, Negative: 799999796 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=bbe86be3ef3c2131f0d4681c0ccd31a8 Observation X04 Sometimes 204 799999796 Time X04 190.54 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 97025647:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 5440935:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 64400802:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 32233552:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 100584697:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 50626352:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 24398748:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 83069947:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 10753345:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 408 :>0:r1=1; 0:r4=0; 2:r3=0; y=2; 43652339:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 7267477:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 69590980:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 11202487:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 84782001:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 114970283:>0:r1=1; 0:r4=1; 2:r3=1; y=2; Ok Witnesses Positive: 408, Negative: 799999592 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is validated Hash=2f45a04baa1582caaf7bebb0f6429fad Observation X05 Sometimes 408 799999592 Time X05 162.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 106040058:>0:r1=0; 0:r4=0; y=1; z=1; 52068590:>0:r1=1; 0:r4=0; y=1; z=1; 24843160:>0:r1=0; 0:r4=1; y=1; z=1; 92555452:>0:r1=1; 0:r4=1; y=1; z=1; 63164825:>0:r1=0; 0:r4=0; y=2; z=1; 8950871:>0:r1=1; 0:r4=0; y=2; z=1; 81741071:>0:r1=0; 0:r4=1; y=2; z=1; 114984727:>0:r1=1; 0:r4=1; y=2; z=1; 94289243:>0:r1=0; 0:r4=0; y=1; z=2; 5618560:>0:r1=1; 0:r4=0; y=1; z=2; 63602475:>0:r1=0; 0:r4=1; y=1; z=2; 35365988:>0:r1=1; 0:r4=1; y=1; z=2; 9093476:>0:r1=0; 0:r4=0; y=2; z=2; 151 :>0:r1=1; 0:r4=0; y=2; z=2; 41043057:>0:r1=0; 0:r4=1; y=2; z=2; 6638296:>0:r1=1; 0:r4=1; y=2; z=2; Ok Witnesses Positive: 151, Negative: 799999849 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=2f7e7e797a32b772dba41a2c989f624e Observation X06 Sometimes 151 799999849 Time X06 192.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 94799256:>0:r1=0; 0:r4=0; 1:r3=0; 14164 :>0:r1=1; 0:r4=0; 1:r3=0; 198911914:>0:r1=0; 0:r4=1; 1:r3=0; 57139200:>0:r1=1; 0:r4=1; 1:r3=0; 272529280:>0:r1=0; 0:r4=0; 1:r3=1; 101265985:>0:r1=1; 0:r4=0; 1:r3=1; 52030798:>0:r1=0; 0:r4=1; 1:r3=1; 223309403:>0:r1=1; 0:r4=1; 1:r3=1; Ok Witnesses Positive: 14164, Negative: 999985836 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is validated Hash=27f80466ebe5b987c02fd5b2375e9014 Observation X07 Sometimes 14164 999985836 Time X07 102.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 53445101:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 9317494:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 70829768:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 82786508:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 109966626:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 66299163:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 24627276:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 90081767:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 8182843:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 346 :>0:r1=1; 0:r4=0; 1:r3=0; z=2; 33094608:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 4666122:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 118438283:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 9203959:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 76864436:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 42195700:>0:r1=1; 0:r4=1; 1:r3=1; z=2; Ok Witnesses Positive: 346, Negative: 799999654 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is validated Hash=c693aeac120b5ebe47aca8096f1cefc4 Observation X08 Sometimes 346 799999654 Time X08 165.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8805898:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 282 :>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=0; 34825865:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 5312822:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 102212772:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 6836728:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 72039222:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 33467796:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 60670493:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 11015088:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 75605924:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 91416460:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 113403832:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 62567967:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 31118922:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 90699929:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; Ok Witnesses Positive: 282, Negative: 799999718 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is validated Hash=25130932b014cac34245d116a5f68876 Observation X09 Sometimes 282 799999718 Time X09 156.87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 57917451:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 9934301:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 74485676:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 87812421:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 120628602:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 65803882:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 31736225:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 95529134:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 7341017:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 148 :>0:r1=1; 0:r4=0; 1:r3=0; z=2; 29304506:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 3875449:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 101915620:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 7055580:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 71559038:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 35100950:>0:r1=1; 0:r4=1; 1:r3=1; z=2; Ok Witnesses Positive: 148, Negative: 799999852 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is validated Hash=6da0ade67698eb3fe55496c10e533d9d Observation X10 Sometimes 148 799999852 Time X10 168.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 279978832:>0:r1=0; 0:r4=0; y=1; 93571322:>0:r1=1; 0:r4=0; y=1; 66653484:>0:r1=0; 0:r4=1; y=1; 235043951:>0:r1=1; 0:r4=1; y=1; 85869926:>0:r1=0; 0:r4=0; y=2; 6891 :>0:r1=1; 0:r4=0; y=2; 187241411:>0:r1=0; 0:r4=1; y=2; 51634183:>0:r1=1; 0:r4=1; y=2; Ok Witnesses Positive: 6891, Negative: 999993109 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=2e151daaab42138b8c478ba081d896ed Observation X11 Sometimes 6891 999993109 Time X11 104.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 106110023:>0:r1=0; 0:r4=0; y=1; z=1; 58067899:>0:r1=1; 0:r4=0; y=1; z=1; 26001785:>0:r1=0; 0:r4=1; y=1; z=1; 101595428:>0:r1=1; 0:r4=1; y=1; z=1; 51898385:>0:r1=0; 0:r4=0; y=2; z=1; 7297845:>0:r1=1; 0:r4=0; y=2; z=1; 65752384:>0:r1=0; 0:r4=1; y=2; z=1; 91545338:>0:r1=1; 0:r4=1; y=2; z=1; 110814855:>0:r1=0; 0:r4=0; y=1; z=2; 7936460:>0:r1=1; 0:r4=0; y=1; z=2; 81120261:>0:r1=0; 0:r4=1; y=1; z=2; 47684747:>0:r1=1; 0:r4=1; y=1; z=2; 7657054:>0:r1=0; 0:r4=0; y=2; z=2; 118 :>0:r1=1; 0:r4=0; y=2; z=2; 31579459:>0:r1=0; 0:r4=1; y=2; z=2; 4937959:>0:r1=1; 0:r4=1; y=2; z=2; Ok Witnesses Positive: 118, Negative: 799999882 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=449f3e0ad9111a8f4431787ea3e14c01 Observation X12 Sometimes 118 799999882 Time X12 191.65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 98902479:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 5976527:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 76801335:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 36627259:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 111019017:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 56919539:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 33283836:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 97088835:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 8051589:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 195 :>0:r1=1; 0:r4=0; 2:r3=0; y=2; 30702237:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 4663635:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 60358918:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 9808616:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 72630260:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 97165723:>0:r1=1; 0:r4=1; 2:r3=1; y=2; Ok Witnesses Positive: 195, Negative: 799999805 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is validated Hash=e039602c16d523ecfdb1a0b4937a34a6 Observation X13 Sometimes 195 799999805 Time X13 166.32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 116641797:>0:r1=0; 0:r4=0; y=1; z=1; 57240867:>0:r1=1; 0:r4=0; y=1; z=1; 32460855:>0:r1=0; 0:r4=1; y=1; z=1; 107334107:>0:r1=1; 0:r4=1; y=1; z=1; 55154381:>0:r1=0; 0:r4=0; y=2; z=1; 7842807:>0:r1=1; 0:r4=0; y=2; z=1; 69655168:>0:r1=0; 0:r4=1; y=2; z=1; 95192853:>0:r1=1; 0:r4=1; y=2; z=1; 96772018:>0:r1=0; 0:r4=0; y=1; z=2; 5884227:>0:r1=1; 0:r4=0; y=1; z=2; 76915025:>0:r1=0; 0:r4=1; y=1; z=2; 40016318:>0:r1=1; 0:r4=1; y=1; z=2; 6719962:>0:r1=0; 0:r4=0; y=2; z=2; 87 :>0:r1=1; 0:r4=0; y=2; z=2; 28114248:>0:r1=0; 0:r4=1; y=2; z=2; 4055280:>0:r1=1; 0:r4=1; y=2; z=2; Ok Witnesses Positive: 87, Negative: 799999913 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=74664d9800a1cc765c71acb315cf55f7 Observation X14 Sometimes 87 799999913 Time X14 193.97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 100130223:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 7332514:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 88239001:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 49817820:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 7526925:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 505 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=0; 40510917:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 6890162:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 87986524:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 39915716:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 29342513:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 86170395:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 50343565:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 6750307:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 87290487:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 111752426:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 505, Negative: 799999495 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=a488ac47b1a88d9c3f30dcee477424e5 Observation X15 Sometimes 505 799999495 Time X15 149.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 247528818:>0:r1=0; 0:r3=0; y=1; 75083201:>0:r1=1; 0:r3=0; y=1; 61145026:>0:r1=0; 0:r3=1; y=1; 239130124:>0:r1=1; 0:r3=1; y=1; 85457761:>0:r1=0; 0:r3=0; y=2; 8460 :>0:r1=1; 0:r3=0; y=2; 225408984:>0:r1=0; 0:r3=1; y=2; 66237626:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 8460, Negative: 999991540 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=7cfc2b26a1cbcdd15d0fab061a637ce4 Observation X16 Sometimes 8460 999991540 Time X16 104.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 92522785:>0:r1=0; 0:r3=0; y=1; z=1; 46301971:>0:r1=1; 0:r3=0; y=1; z=1; 24530561:>0:r1=0; 0:r3=1; y=1; z=1; 94935442:>0:r1=1; 0:r3=1; y=1; z=1; 52584719:>0:r1=0; 0:r3=0; y=2; z=1; 6976982:>0:r1=1; 0:r3=0; y=2; z=1; 81423409:>0:r1=0; 0:r3=1; y=2; z=1; 110665426:>0:r1=1; 0:r3=1; y=2; z=1; 96147536:>0:r1=0; 0:r3=0; y=1; z=2; 6099851:>0:r1=1; 0:r3=0; y=1; z=2; 85800317:>0:r1=0; 0:r3=1; y=1; z=2; 49104027:>0:r1=1; 0:r3=1; y=1; z=2; 7875049:>0:r1=0; 0:r3=0; y=2; z=2; 150 :>0:r1=1; 0:r3=0; y=2; z=2; 38541838:>0:r1=0; 0:r3=1; y=2; z=2; 6489937:>0:r1=1; 0:r3=1; y=2; z=2; Ok Witnesses Positive: 150, Negative: 799999850 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=8ece2ae907eaa93a2cebf24dcb08cf79 Observation X17 Sometimes 150 799999850 Time X17 190.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 89307223:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 4573355:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 73645762:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 34946973:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 92363935:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 44016441:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 31292415:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 89119740:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 8710450:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 360 :>0:r1=1; 0:r3=0; 2:r3=0; y=2; 45238341:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 8096099:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 58303278:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 9223197:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 92096398:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 119066033:>0:r1=1; 0:r3=1; 2:r3=1; y=2; Ok Witnesses Positive: 360, Negative: 799999640 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is validated Hash=773f6798f908e0cd810f3e878df07bab Observation X18 Sometimes 360 799999640 Time X18 164.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 99651309:>0:r1=0; 0:r3=0; y=1; z=1; 45702061:>0:r1=1; 0:r3=0; y=1; z=1; 30271320:>0:r1=0; 0:r3=1; y=1; z=1; 98064058:>0:r1=1; 0:r3=1; y=1; z=1; 56978915:>0:r1=0; 0:r3=0; y=2; z=1; 7805047:>0:r1=1; 0:r3=0; y=2; z=1; 90782427:>0:r1=0; 0:r3=1; y=2; z=1; 120202891:>0:r1=1; 0:r3=1; y=2; z=1; 83747132:>0:r1=0; 0:r3=0; y=1; z=2; 4575800:>0:r1=1; 0:r3=0; y=1; z=2; 69211485:>0:r1=0; 0:r3=1; y=1; z=2; 36906055:>0:r1=1; 0:r3=1; y=1; z=2; 7267332:>0:r1=0; 0:r3=0; y=2; z=2; 115 :>0:r1=1; 0:r3=0; y=2; z=2; 41390776:>0:r1=0; 0:r3=1; y=2; z=2; 7443277:>0:r1=1; 0:r3=1; y=2; z=2; Ok Witnesses Positive: 115, Negative: 799999885 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=811f0a85dc5f811c7436b53d2ca9c449 Observation X19 Sometimes 115 799999885 Time X19 193.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 86511183:>0:r1=0; 0:r3=0; 1:r3=0; 12665 :>0:r1=1; 0:r3=0; 1:r3=0; 206157767:>0:r1=0; 0:r3=1; 1:r3=0; 59094317:>0:r1=1; 0:r3=1; 1:r3=0; 257345545:>0:r1=0; 0:r3=0; 1:r3=1; 85521167:>0:r1=1; 0:r3=0; 1:r3=1; 66135583:>0:r1=0; 0:r3=1; 1:r3=1; 239221773:>0:r1=1; 0:r3=1; 1:r3=1; Ok Witnesses Positive: 12665, Negative: 999987335 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is validated Hash=0c99e9e00ef12798cd94e468d7533fcb Observation X20 Sometimes 12665 999987335 Time X20 103.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 47679576:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 7538822:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 74262703:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 86411474:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 104233456:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 58226031:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 31179774:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 97661517:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 7240207:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 273 :>0:r1=1; 0:r3=0; 1:r3=0; z=2; 33135699:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 5344053:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 107649381:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 8507497:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 83396191:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 47533346:>0:r1=1; 0:r3=1; 1:r3=1; z=2; Ok Witnesses Positive: 273, Negative: 799999727 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is validated Hash=10b56f844965b778138fc256080a6cb2 Observation X21 Sometimes 273 799999727 Time X21 167.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7799979:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 272 :>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=0; 35224328:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 5893788:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 94338454:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 5687846:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 78505491:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 36701212:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 53700888:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 9070084:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 80159436:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 95533226:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 104921301:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 55452722:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 37108153:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 99902820:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; Ok Witnesses Positive: 272, Negative: 799999728 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is validated Hash=e7fc832a2e4b347328216cfab07885d9 Observation X22 Sometimes 272 799999728 Time X22 154.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 51871523:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 8275318:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 79706685:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 89869482:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 114572139:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 57410564:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 39893387:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 104429060:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 6657604:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 124 :>0:r1=1; 0:r3=0; 1:r3=0; z=2; 29899231:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 4287713:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 91704840:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 5790643:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 78185592:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 37446095:>0:r1=1; 0:r3=1; 1:r3=1; z=2; Ok Witnesses Positive: 124, Negative: 799999876 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is validated Hash=86fcf34749ab0aa370ea66e6893791a0 Observation X23 Sometimes 124 799999876 Time X23 167.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 264254898:>0:r1=0; 0:r3=0; y=1; 79179457:>0:r1=1; 0:r3=0; y=1; 83883568:>0:r1=0; 0:r3=1; y=1; 245635161:>0:r1=1; 0:r3=1; y=1; 76741513:>0:r1=0; 0:r3=0; y=2; 5915 :>0:r1=1; 0:r3=0; y=2; 196964003:>0:r1=0; 0:r3=1; y=2; 53335485:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 5915, Negative: 999994085 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=1a78bce42911eadebdb22805402de8eb Observation X24 Sometimes 5915 999994085 Time X24 107.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 100320221:>0:r1=0; 0:r3=0; y=1; z=1; 51397112:>0:r1=1; 0:r3=0; y=1; z=1; 31732577:>0:r1=0; 0:r3=1; y=1; z=1; 107636838:>0:r1=1; 0:r3=1; y=1; z=1; 46445318:>0:r1=0; 0:r3=0; y=2; z=1; 6315267:>0:r1=1; 0:r3=0; y=2; z=1; 72417779:>0:r1=0; 0:r3=1; y=2; z=1; 93867518:>0:r1=1; 0:r3=1; y=2; z=1; 98534711:>0:r1=0; 0:r3=0; y=1; z=2; 6645595:>0:r1=1; 0:r3=0; y=1; z=2; 90325705:>0:r1=0; 0:r3=1; y=1; z=2; 50382850:>0:r1=1; 0:r3=1; y=1; z=2; 6308311:>0:r1=0; 0:r3=0; y=2; z=2; 109 :>0:r1=1; 0:r3=0; y=2; z=2; 32288836:>0:r1=0; 0:r3=1; y=2; z=2; 5381253:>0:r1=1; 0:r3=1; y=2; z=2; Ok Witnesses Positive: 109, Negative: 799999891 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=629e26a0c6f613b14043edf57727b702 Observation X25 Sometimes 109 799999891 Time X25 193.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 91723985:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 4913274:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 85994733:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 38739833:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 102633526:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 49213871:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 41288308:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 104500576:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 6897638:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 161 :>0:r1=1; 0:r3=0; 2:r3=0; y=2; 32488416:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 5162797:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 51070187:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 7744850:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 78383370:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 99244475:>0:r1=1; 0:r3=1; 2:r3=1; y=2; Ok Witnesses Positive: 161, Negative: 799999839 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is validated Hash=54da285ce144acabc337e28ea8958874 Observation X26 Sometimes 161 799999839 Time X26 168.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 86491308:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 42991562:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 41711770:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 5265856:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 24984419:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 74811367:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 87738510:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 101223738:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 108188460:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 7450281:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 10652839:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 114 :>0:r1=1; 2:r1=1; 2:r3=0; x=2; 98966475:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 39089350:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 64040214:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 6393737:>0:r1=1; 2:r1=1; 2:r3=1; x=2; Ok Witnesses Positive: 114, Negative: 799999886 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=ffa63368caa391807dee9905d20510c6 Observation X27 Sometimes 114 799999886 Time X27 158.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 75303203:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 91730038:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 40000112:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 13038950:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 12840983:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 90398703:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 68278518:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 144551729:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 92937190:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 15363703:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 5083829:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 1031 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 64688195:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 43024353:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 35921833:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 6837630:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 1031, Negative: 799998969 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=4adca431a2784b4aa9df91b1fc3b1666 Observation X28 Sometimes 1031 799998969 Time X28 137.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 70649656:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 83908342:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 35871921:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 11361004:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 17258745:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 98524683:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 72082814:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 146086065:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 83433980:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 13737028:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 4449970:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 866 :>1:r1=1; 3:r1=1; 3:r3=0; x=2; 72182378:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 43858947:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 38636036:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 7957565:>1:r1=1; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 866, Negative: 799999134 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=cd58719fd03bc8a841de06004867cb05 Observation X29 Sometimes 866 799999134 Time X29 139.50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 89789979:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 51313994:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 48523391:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 6751558:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 18315129:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 68647144:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 80824828:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 100300866:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 122210672:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 9928080:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 13207557:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 158 :>0:r1=1; 2:r1=1; 2:r4=0; x=2; 85935928:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 38482300:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 59801114:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 5967302:>0:r1=1; 2:r1=1; 2:r4=1; x=2; Ok Witnesses Positive: 158, Negative: 799999842 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is validated Hash=a0f55fa2291a072f015a1f0b83d20074 Observation X30 Sometimes 158 799999842 Time X30 159.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 84771243:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 43457369:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 41823560:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 5251529:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 24850803:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 76258016:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 87859433:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 100922890:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 108537875:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 7595043:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 11038686:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 110 :>0:r1=1; 2:r1=1; 2:r3=0; x=2; 97500451:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 39353982:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 64364212:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 6414798:>0:r1=1; 2:r1=1; 2:r3=1; x=2; Ok Witnesses Positive: 110, Negative: 799999890 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=ffb6dc3e13fae7c7e7811955e241147b Observation X31 Sometimes 110 799999890 Time X31 158.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 80471758:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 15385426:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 77014449:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 99025633:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 4977500:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 1146 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=0; 36555728:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 15201008:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 60596508:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 40564338:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 16597439:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 98547775:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 33386772:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 6063483:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 59216897:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 156394140:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; Ok Witnesses Positive: 1146, Negative: 799998854 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=abdf662fb230128532b66df78e4a75f1 Observation X32 Sometimes 1146 799998854 Time X32 131.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 71707145:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 12895585:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 73259695:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 87564782:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 4100460:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 858 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; 32251524:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 12409146:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 67420746:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 41126219:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 23296002:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 110471322:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 33547515:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 6913376:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 64401202:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 158634423:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; Ok Witnesses Positive: 858, Negative: 799999142 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=c86889a7cdc1c89457a71c414046d8c0 Observation X33 Sometimes 858 799999142 Time X33 127.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 80105073:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 97317614:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 39810664:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 14506378:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 18112979:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 95323210:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 66387000:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 151583215:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 81668309:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 15176328:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 4126174:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 773 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 58494890:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 41356488:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 30022952:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 6007953:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 773, Negative: 799999227 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=8db91522dc421fe43a7baf7aff0de837 Observation X34 Sometimes 773 799999227 Time X34 140.74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 76693961:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 88012451:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 35225648:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 12337394:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 22678124:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 103075541:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 71463128:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 155888805:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 73950969:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 12770886:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 3612488:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 884 :>1:r1=1; 3:r1=1; 3:r3=0; x=2; 64213939:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 40835330:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 32372461:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 6867991:>1:r1=1; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 884, Negative: 799999116 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=00744a65cf189719eb1309a79c27a2ca Observation X35 Sometimes 884 799999116 Time X35 141.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 92560683:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 14362579:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 46719855:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 81415037:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 14758545:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 40492978:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 17690351:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 45539409:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 39447515:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 3674134:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 56582624:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 81291576:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 17409846:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 57361453:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 190693415:>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 154.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 82903993:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 12554739:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 41111306:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 69972235:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 12991250:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 35274127:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 14437854:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 43657345:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 38330521:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 3407845:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 52797936:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 94713351:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 21562200:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 66347477:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 209937821:>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 162.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 75532478:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 50446932:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 8172603:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 98887748:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 56283262:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 9636501:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 50263658:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 157708508:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 92505895:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 13683280:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 45807370:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 75335151:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 8890136:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 38546297:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 18300181:>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 163.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 226518019:>0:r1=0; 0:r4=0; y=1; 91274970:>0:r1=1; 0:r4=0; y=1; 20308133:>0:r1=0; 0:r4=1; y=1; 286355660:>0:r1=1; 0:r4=1; y=1; 90104172:>0:r1=0; 0:r4=0; y=2; 148682721:>0:r1=0; 0:r4=1; y=2; 136756325:>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 108.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 83077355:>0:r1=0; 0:r4=0; y=1; z=1; 54335976:>0:r1=1; 0:r4=0; y=1; z=1; 9516807:>0:r1=0; 0:r4=1; y=1; z=1; 116947401:>0:r1=1; 0:r4=1; y=1; z=1; 52814653:>0:r1=0; 0:r4=0; y=2; z=1; 8332459:>0:r1=1; 0:r4=0; y=2; z=1; 45481753:>0:r1=0; 0:r4=1; y=2; z=1; 144067067:>0:r1=1; 0:r4=1; y=2; z=1; 85250242:>0:r1=0; 0:r4=0; y=1; z=2; 11245882:>0:r1=1; 0:r4=0; y=1; z=2; 52791097:>0:r1=0; 0:r4=1; y=1; z=2; 84453775:>0:r1=1; 0:r4=1; y=1; z=2; 8411566:>0:r1=0; 0:r4=0; y=2; z=2; 30041571:>0:r1=0; 0:r4=1; y=2; z=2; 13232396:>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 194.08 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 85004894:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 9295979:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 44517194:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 60493574:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 84140053:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 55094559:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 12458070:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 111002460:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 9340563:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 34808912:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 15938692:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 57448204:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 11087651:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 52553774:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 156815421:>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 165.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 89664437:>0:r1=0; 0:r4=0; y=1; z=1; 55232798:>0:r1=1; 0:r4=0; y=1; z=1; 12510083:>0:r1=0; 0:r4=1; y=1; z=1; 119362230:>0:r1=1; 0:r4=1; y=1; z=1; 55508973:>0:r1=0; 0:r4=0; y=2; z=1; 9501271:>0:r1=1; 0:r4=0; y=2; z=1; 49397895:>0:r1=0; 0:r4=1; y=2; z=1; 158334179:>0:r1=1; 0:r4=1; y=2; z=1; 79789240:>0:r1=0; 0:r4=0; y=1; z=2; 9173894:>0:r1=1; 0:r4=0; y=1; z=2; 42606039:>0:r1=0; 0:r4=1; y=1; z=2; 63243483:>0:r1=1; 0:r4=1; y=1; z=2; 7518734:>0:r1=0; 0:r4=0; y=2; z=2; 33132778:>0:r1=0; 0:r4=1; y=2; z=2; 15023966:>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 196.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 86685372:>0:r1=0; 0:r4=0; 1:r3=0; 132828806:>0:r1=0; 0:r4=1; 1:r3=0; 124342882:>0:r1=1; 0:r4=1; 1:r3=0; 234380926:>0:r1=0; 0:r4=0; 1:r3=1; 103847088:>0:r1=1; 0:r4=0; 1:r3=1; 29117221:>0:r1=0; 0:r4=1; 1:r3=1; 288797705:>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 104.80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 46410523:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 9128645:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 43354806:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 115412836:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 91704678:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 71175293:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 13881095:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 120941948:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 7321428:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 26120713:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 10648815:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 97138057:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 15208955:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 51626066:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 79926142:>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 168.46 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8174617:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 27695513:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 12304108:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 89131444:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 11159846:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 48449590:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 65059557:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 51557149:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 10954827:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 45534166:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 128113388:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 93547460:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 68177086:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 16398763:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 123742486:>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 157.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 50390449:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 9901038:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 46425958:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 122221223:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 99937759:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 72011951:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 17353901:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 128451582:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 6838782:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 24695128:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 9134817:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 87599964:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 11410564:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 48503993:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 65122891:>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 173.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 238835515:>0:r1=0; 0:r4=0; y=1; 95664596:>0:r1=1; 0:r4=0; y=1; 36810820:>0:r1=0; 0:r4=1; y=1; 301081891:>0:r1=1; 0:r4=1; y=1; 80833342:>0:r1=0; 0:r4=0; y=2; 133644706:>0:r1=0; 0:r4=1; y=2; 113129130:>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 108.27 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 89450782:>0:r1=0; 0:r4=0; y=1; z=1; 59375101:>0:r1=1; 0:r4=0; y=1; z=1; 13307762:>0:r1=0; 0:r4=1; y=1; z=1; 128545614:>0:r1=1; 0:r4=1; y=1; z=1; 47525924:>0:r1=0; 0:r4=0; y=2; z=1; 7691152:>0:r1=1; 0:r4=0; y=2; z=1; 42160364:>0:r1=0; 0:r4=1; y=2; z=1; 125148827:>0:r1=1; 0:r4=1; y=2; z=1; 90423133:>0:r1=0; 0:r4=0; y=1; z=2; 12163565:>0:r1=1; 0:r4=0; y=1; z=2; 54921300:>0:r1=0; 0:r4=1; y=1; z=2; 85559003:>0:r1=1; 0:r4=1; y=1; z=2; 6913682:>0:r1=0; 0:r4=0; y=2; z=2; 26045766:>0:r1=0; 0:r4=1; y=2; z=2; 10768025:>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 194.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 88652733:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 9888379:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 54673973:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 67812854:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 92540036:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 60881376:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 17872531:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 129739807:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 7353247:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 26363807:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 9961136:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 50091091:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 9519497:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 46649531:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 128000002:>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 168.05 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 97583148:>0:r1=0; 0:r4=0; y=1; z=1; 60355369:>0:r1=1; 0:r4=0; y=1; z=1; 17274291:>0:r1=0; 0:r4=1; y=1; z=1; 139537755:>0:r1=1; 0:r4=1; y=1; z=1; 49175364:>0:r1=0; 0:r4=0; y=2; z=1; 8131239:>0:r1=1; 0:r4=0; y=2; z=1; 45190484:>0:r1=0; 0:r4=1; y=2; z=1; 129365455:>0:r1=1; 0:r4=1; y=2; z=1; 81231399:>0:r1=0; 0:r4=0; y=1; z=2; 9456002:>0:r1=1; 0:r4=0; y=1; z=2; 52235947:>0:r1=0; 0:r4=1; y=1; z=2; 71890770:>0:r1=1; 0:r4=1; y=1; z=2; 6064656:>0:r1=0; 0:r4=0; y=2; z=2; 23726029:>0:r1=0; 0:r4=1; y=2; z=2; 8782092:>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 194.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 73010322:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 11789806:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 39803694:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 81434979:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 11750494:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 34893555:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 18473553:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 39303018:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 34852818:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 3068673:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 61803782:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 82299181:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 18487900:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 62249366:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 226778859:>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 163.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 209841203:>0:r1=0; 0:r3=0; y=1; 80260746:>0:r1=1; 0:r3=0; y=1; 20114751:>0:r1=0; 0:r3=1; y=1; 315326559:>0:r1=1; 0:r3=1; y=1; 78875155:>0:r1=0; 0:r3=0; y=2; 140659653:>0:r1=0; 0:r3=1; y=2; 154921933:>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 108.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y17.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y17 "Rf*e DpCtrlIsyncdR Fre LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,2 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | lwsync | lwsync | lwsync ; beq LC01 | li r3,1 | li r3,1 | li r3,1 ; LC01: | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y17 Allowed Histogram (15 states) 76780456:>0:r1=0; 0:r3=0; y=1; z=1; 48128228:>0:r1=1; 0:r3=0; y=1; z=1; 9205577:>0:r1=0; 0:r3=1; y=1; z=1; 132825475:>0:r1=1; 0:r3=1; y=1; z=1; 43548260:>0:r1=0; 0:r3=0; y=2; z=1; 6306933:>0:r1=1; 0:r3=0; y=2; z=1; 42231670:>0:r1=0; 0:r3=1; y=2; z=1; 150512550:>0:r1=1; 0:r3=1; y=2; z=1; 78650287:>0:r1=0; 0:r3=0; y=1; z=2; 10438922:>0:r1=1; 0:r3=0; y=1; z=2; 50856084:>0:r1=0; 0:r3=1; y=1; z=2; 97558448:>0:r1=1; 0:r3=1; y=1; z=2; 6963312:>0:r1=0; 0:r3=0; y=2; z=2; 29469546:>0:r1=0; 0:r3=1; y=2; z=2; 16524252:>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 194.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 74445417:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 8809431:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 42384729:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 72360525:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 75040834:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 48038170:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 11938911:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 130633979:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 7644641:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 32922551:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 19752937:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 48501089:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 9204854:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 49032114:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 169289818:>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 169.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 81662782:>0:r1=0; 0:r3=0; y=1; z=1; 48535497:>0:r1=1; 0:r3=0; y=1; z=1; 12155207:>0:r1=0; 0:r3=1; y=1; z=1; 139143762:>0:r1=1; 0:r3=1; y=1; z=1; 45997687:>0:r1=0; 0:r3=0; y=2; z=1; 7438172:>0:r1=1; 0:r3=0; y=2; z=1; 46842057:>0:r1=0; 0:r3=1; y=2; z=1; 164289299:>0:r1=1; 0:r3=1; y=2; z=1; 71778013:>0:r1=0; 0:r3=0; y=1; z=2; 8532632:>0:r1=1; 0:r3=0; y=1; z=2; 42456751:>0:r1=0; 0:r3=1; y=1; z=2; 75081966:>0:r1=1; 0:r3=1; y=1; z=2; 6351999:>0:r1=0; 0:r3=0; y=2; z=2; 31696051:>0:r1=0; 0:r3=1; y=2; z=2; 18038125:>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 195.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 80947981:>0:r1=0; 0:r3=0; 1:r3=0; 128177787:>0:r1=0; 0:r3=1; 1:r3=0; 138741334:>0:r1=1; 0:r3=1; 1:r3=0; 212298693:>0:r1=0; 0:r3=0; 1:r3=1; 91790471:>0:r1=1; 0:r3=0; 1:r3=1; 25965903:>0:r1=0; 0:r3=1; 1:r3=1; 322077831:>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 105.71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 41674571:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 7496043:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 39773632:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 125668579:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 80092768:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 60704210:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 12710462:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 137978092:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 7000878:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 25797564:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 13428124:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 87474443:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 13602619:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 50785795:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 95812220:>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.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7130196:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 25572143:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 14830157:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 76630303:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 10802265:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 45096427:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 78570364:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 45727062:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 9497929:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 42884853:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 142420843:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 81120332:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 59872736:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 15078601:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 144765789:>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 159.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 43135056:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 7893440:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 42012022:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 132408367:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 87311524:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 61640071:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 15974145:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 152155650:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 6014914:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 23332378:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 11399201:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 77351766:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 10201175:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 48228904:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 80941387:>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 171.73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 217638737:>0:r1=0; 0:r3=0; y=1; 82462896:>0:r1=1; 0:r3=0; y=1; 33352585:>0:r1=0; 0:r3=1; y=1; 339414700:>0:r1=1; 0:r3=1; y=1; 71330670:>0:r1=0; 0:r3=0; y=2; 129274754:>0:r1=0; 0:r3=1; y=2; 126525658:>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 108.54 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 81396582:>0:r1=0; 0:r3=0; y=1; z=1; 51592497:>0:r1=1; 0:r3=0; y=1; z=1; 12807568:>0:r1=0; 0:r3=1; y=1; z=1; 148440062:>0:r1=1; 0:r3=1; y=1; z=1; 39575807:>0:r1=0; 0:r3=0; y=2; z=1; 5800485:>0:r1=1; 0:r3=0; y=2; z=1; 39074422:>0:r1=0; 0:r3=1; y=2; z=1; 131999984:>0:r1=1; 0:r3=1; y=2; z=1; 80842334:>0:r1=0; 0:r3=0; y=1; z=2; 11443294:>0:r1=1; 0:r3=0; y=1; z=2; 52511638:>0:r1=0; 0:r3=1; y=1; z=2; 101011749:>0:r1=1; 0:r3=1; y=1; z=2; 5675505:>0:r1=0; 0:r3=0; y=2; z=2; 24755767:>0:r1=0; 0:r3=1; y=2; z=2; 13072306:>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 196.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 78424338:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 9220032:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 52126399:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 83219688:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 81254724:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 52604678:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 16029712:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 149134938:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 6208739:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 25373013:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 13026749:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 42375146:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 7741240:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 42542711:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 140717893:>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 171.65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 68380511:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 48129451:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 43844923:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 7554798:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 7947194:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 46841511:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 114461818:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 168977271:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 82263838:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 7302781:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 12487072:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 43909030:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 37037444:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 88687400:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 22174958:>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 164.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 61767594:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 80363491:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 43079031:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 13541917:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 6923584:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 55243934:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 86161048:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 191373402:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 75251303:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 14587102:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 8769590:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 42303278:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 36093942:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 68973209:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 15567575:>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 141.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 55607952:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 67941876:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 38525578:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 11241083:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 6740542:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 54417038:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 97949636:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 205134369:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 67324665:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 11705614:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 8481386:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 39568335:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 34709447:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 81189359:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 19463120:>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 144.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 75483459:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 56891214:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 49696716:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 9554530:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 8219237:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 50599800:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 100273847:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 157569241:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 90625876:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 8794416:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 13616999:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 45329061:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 38546005:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 75945189:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 18854410:>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 160.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 67470856:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 48044897:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 43603833:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 7452875:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 7683375:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 46575949:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 115496748:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 169240901:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 80472757:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 7266523:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 12526913:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 43738698:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 36540557:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 90470511:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 23414607:>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 165.24 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 68557392:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 13820207:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 65564567:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 83659394:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 7555854:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 40366558:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 14855774:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 38043478:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 33197816:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 9168769:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 60141975:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 61661732:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 14142497:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 78326361:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 210937626:>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 131.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 63528486:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 11180466:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 58461548:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 69293473:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 7735921:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 37070001:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 12896478:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 36671837:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 33193472:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 8600378:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 59874873:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 70791175:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 18021226:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 89555465:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 223125201:>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 137.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 66961851:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 84596658:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 42998487:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 15215261:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 9661352:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 58500223:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 87863460:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 202106408:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 67879288:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 13830723:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 6905337:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 38088910:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 34189301:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 57548586:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 13654155:>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 140.91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 59698322:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 70815533:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 39097533:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 12603372:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 9308452:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 57794065:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 99896224:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 217763869:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 61311569:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 11007511:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 6865719:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 35699954:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 32888649:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 67873902:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 17375326:>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 145.31 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 dim jan 23 16:18:24 CET 2011