Sat Jan 22 09:04:00 CST 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) 36679084:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 1421759:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 19423739:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 9621499:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 1402274:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 1 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=0; 14614848:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 2387722:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 19285946:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 14576012:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 1517071:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 23743048:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 9600639:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 2511601:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 23629884:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 19584873:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is validated Hash=6559e19d9e37619f3f8bf433a5805105 Observation X00 Sometimes 1 199999999 Time X00 94.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 35918378:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 1435838:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 19179988:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 9816473:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 1595941:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 15612972:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 2841307:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 18779243:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 14340542:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 1343481:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 24132331:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 9578331:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 2488030:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 23424259:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 19512886:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=2dd158f1ef0b66595a56ff21c6e00a13 Observation X01 Never 0 200000000 Time X01 94.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 19695622:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 13420058:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 1721805:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 21648171:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 10197871:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 2212852:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 24179575:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 20929622:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 35127741:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 2705160:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 18877249:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 12469046:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 1257626:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 13647893:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 1909709:>0:r1=1; 0:r4=1; 2:r1=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is NOT validated Hash=ddaab862216f1c9eafeceba074a24928 Observation X02 Never 0 200000000 Time X02 97.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 49892979:>0:r1=0; 0:r4=0; y=1; 20501652:>0:r1=1; 0:r4=0; y=1; 3083099:>0:r1=0; 0:r4=1; y=1; 40922502:>0:r1=1; 0:r4=1; y=1; 15101071:>0:r1=0; 0:r4=0; y=2; 1 :>0:r1=1; 0:r4=0; y=2; 54071552:>0:r1=0; 0:r4=1; y=2; 16427144:>0:r1=1; 0:r4=1; y=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=979eb45568765c8b5bb24cb8beb2a694 Observation X03 Sometimes 1 199999999 Time X03 75.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 20610891:>0:r1=0; 0:r4=0; y=1; z=1; 13063525:>0:r1=1; 0:r4=0; y=1; z=1; 1373324:>0:r1=0; 0:r4=1; y=1; z=1; 19855333:>0:r1=1; 0:r4=1; y=1; z=1; 9697701:>0:r1=0; 0:r4=0; y=2; z=1; 2031588:>0:r1=1; 0:r4=0; y=2; z=1; 25808367:>0:r1=0; 0:r4=1; y=2; z=1; 22666324:>0:r1=1; 0:r4=1; y=2; z=1; 34633316:>0:r1=0; 0:r4=0; y=1; z=2; 2244799:>0:r1=1; 0:r4=0; y=1; z=2; 17717284:>0:r1=0; 0:r4=1; y=1; z=2; 11544372:>0:r1=1; 0:r4=1; y=1; z=2; 947013:>0:r1=0; 0:r4=0; y=2; z=2; 15535887:>0:r1=0; 0:r4=1; y=2; z=2; 2270276:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=bbe86be3ef3c2131f0d4681c0ccd31a8 Observation X04 Never 0 200000000 Time X04 107.77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 33037361:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 1308158:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 16965141:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 8156420:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 20751582:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 13395526:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 1593690:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 19638232:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 1018576:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 13233155:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 2087628:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 13198124:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 3514988:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 27663853:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 24437566:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=2f45a04baa1582caaf7bebb0f6429fad Observation X05 Never 0 200000000 Time X05 102.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 22937384:>0:r1=0; 0:r4=0; y=1; z=1; 14389444:>0:r1=1; 0:r4=0; y=1; z=1; 3388809:>0:r1=0; 0:r4=1; y=1; z=1; 23966410:>0:r1=1; 0:r4=1; y=1; z=1; 11481411:>0:r1=0; 0:r4=0; y=2; z=1; 2611001:>0:r1=1; 0:r4=0; y=2; z=1; 28978680:>0:r1=0; 0:r4=1; y=2; z=1; 26649670:>0:r1=1; 0:r4=1; y=2; z=1; 31591897:>0:r1=0; 0:r4=0; y=1; z=2; 1225133:>0:r1=1; 0:r4=0; y=1; z=2; 13781386:>0:r1=0; 0:r4=1; y=1; z=2; 6311927:>0:r1=1; 0:r4=1; y=1; z=2; 764151:>0:r1=0; 0:r4=0; y=2; z=2; 11044366:>0:r1=0; 0:r4=1; y=2; z=2; 878331:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=2f7e7e797a32b772dba41a2c989f624e Observation X06 Never 0 200000000 Time X06 108.40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (7 states) 18699433:>0:r1=0; 0:r4=0; 1:r3=0; 47779526:>0:r1=0; 0:r4=1; 1:r3=0; 13150404:>0:r1=1; 0:r4=1; 1:r3=0; 50438588:>0:r1=0; 0:r4=0; 1:r3=1; 21573123:>0:r1=1; 0:r4=0; 1:r3=1; 4973187:>0:r1=0; 0:r4=1; 1:r3=1; 43385739:>0:r1=1; 0:r4=1; 1:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=27f80466ebe5b987c02fd5b2375e9014 Observation X07 Never 0 200000000 Time X07 74.97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 11570416:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 1908201:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 23132115:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 22468588:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 22014643:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 16363506:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 775943:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 17299942:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 2038873:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 10942454:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 1145608:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 37894766:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 2804407:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 17748779:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 11891759:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=c693aeac120b5ebe47aca8096f1cefc4 Observation X08 Never 0 200000000 Time X08 101.85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 1161120:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 9363457:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 1142349:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 32914311:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 1630653:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 19898031:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 10300152:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 12371114:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 2149980:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 24162322:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 22664365:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 24499695:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 16545141:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 1129632:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 20067678:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=25130932b014cac34245d116a5f68876 Observation X09 Never 0 200000000 Time X09 99.16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 12909651:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 2094963:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 26083602:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 23541016:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 26143086:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 17731962:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 2559419:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 23217139:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 987828:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 8098836:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 782878:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 30844177:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 1256525:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 16696816:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 7052102:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=6da0ade67698eb3fe55496c10e533d9d Observation X10 Never 0 200000000 Time X10 101.61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (7 states) 52116912:>0:r1=0; 0:r4=0; y=1; 20166126:>0:r1=1; 0:r4=0; y=1; 7425019:>0:r1=0; 0:r4=1; y=1; 48072303:>0:r1=1; 0:r4=1; y=1; 15439733:>0:r1=0; 0:r4=0; y=2; 45200592:>0:r1=0; 0:r4=1; y=2; 11579315:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=2e151daaab42138b8c478ba081d896ed Observation X11 Never 0 200000000 Time X11 76.08 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 23772594:>0:r1=0; 0:r4=0; y=1; z=1; 15648690:>0:r1=1; 0:r4=0; y=1; z=1; 3295180:>0:r1=0; 0:r4=1; y=1; z=1; 22029452:>0:r1=1; 0:r4=1; y=1; z=1; 8455266:>0:r1=0; 0:r4=0; y=2; z=1; 1483819:>0:r1=1; 0:r4=0; y=2; z=1; 21027971:>0:r1=0; 0:r4=1; y=2; z=1; 18897971:>0:r1=1; 0:r4=1; y=2; z=1; 36640827:>0:r1=0; 0:r4=0; y=1; z=2; 2859219:>0:r1=1; 0:r4=0; y=1; z=2; 20759429:>0:r1=0; 0:r4=1; y=1; z=2; 13108825:>0:r1=1; 0:r4=1; y=1; z=2; 1113429:>0:r1=0; 0:r4=0; y=2; z=2; 9852347:>0:r1=0; 0:r4=1; y=2; z=2; 1054981:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=449f3e0ad9111a8f4431787ea3e14c01 Observation X12 Never 0 200000000 Time X12 108.87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 33740969:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 1418936:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 21565561:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 9760043:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 25368402:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 16340068:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 3767945:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 23985264:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 681590:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 8992955:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 848054:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 9492741:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 1739881:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 23453128:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 18844463:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=e039602c16d523ecfdb1a0b4937a34a6 Observation X13 Never 0 200000000 Time X13 102.01 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X14.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X14 "Rfe DpAddrdR Fre SyncdWW Wse SyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | sync | lwsync ; | li r3,1 | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X14 Allowed Histogram (15 states) 27107995:>0:r1=0; 0:r4=0; y=1; z=1; 17147404:>0:r1=1; 0:r4=0; y=1; z=1; 5018473:>0:r1=0; 0:r4=1; y=1; z=1; 28096157:>0:r1=1; 0:r4=1; y=1; z=1; 9171330:>0:r1=0; 0:r4=0; y=2; z=1; 1618926:>0:r1=1; 0:r4=0; y=2; z=1; 23704918:>0:r1=0; 0:r4=1; y=2; z=1; 20114018:>0:r1=1; 0:r4=1; y=2; z=1; 31580077:>0:r1=0; 0:r4=0; y=1; z=2; 1380194:>0:r1=1; 0:r4=0; y=1; z=2; 18391422:>0:r1=0; 0:r4=1; y=1; z=2; 7776779:>0:r1=1; 0:r4=1; y=1; z=2; 570684:>0:r1=0; 0:r4=0; y=2; z=2; 7506489:>0:r1=0; 0:r4=1; y=2; z=2; 815134:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=74664d9800a1cc765c71acb315cf55f7 Observation X14 Never 0 200000000 Time X14 109.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 36350176:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 1496722:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 19669598:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 9694805:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 1730689:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 15488124:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 2795510:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 19070747:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 14835686:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 1716105:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 22605837:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 9742007:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 2784154:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 22841487:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 19178353:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=a488ac47b1a88d9c3f30dcee477424e5 Observation X15 Never 0 200000000 Time X15 94.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 49398478:>0:r1=0; 0:r3=0; y=1; 21782619:>0:r1=1; 0:r3=0; y=1; 3177078:>0:r1=0; 0:r3=1; y=1; 40080568:>0:r1=1; 0:r3=1; y=1; 15127309:>0:r1=0; 0:r3=0; y=2; 4 :>0:r1=1; 0:r3=0; y=2; 54743532:>0:r1=0; 0:r3=1; y=2; 15690412:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 4, Negative: 199999996 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=7cfc2b26a1cbcdd15d0fab061a637ce4 Observation X16 Sometimes 4 199999996 Time X16 74.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 20928749:>0:r1=0; 0:r3=0; y=1; z=1; 14239893:>0:r1=1; 0:r3=0; y=1; z=1; 1063228:>0:r1=0; 0:r3=1; y=1; z=1; 17495267:>0:r1=1; 0:r3=1; y=1; z=1; 11235451:>0:r1=0; 0:r3=0; y=2; z=1; 2938358:>0:r1=1; 0:r3=0; y=2; z=1; 25324393:>0:r1=0; 0:r3=1; y=2; z=1; 24022518:>0:r1=1; 0:r3=1; y=2; z=1; 33858735:>0:r1=0; 0:r3=0; y=1; z=2; 2510382:>0:r1=1; 0:r3=0; y=1; z=2; 17185897:>0:r1=0; 0:r3=1; y=1; z=2; 11422121:>0:r1=1; 0:r3=1; y=1; z=2; 1136437:>0:r1=0; 0:r3=0; y=2; z=2; 14200961:>0:r1=0; 0:r3=1; y=2; z=2; 2437610:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=8ece2ae907eaa93a2cebf24dcb08cf79 Observation X17 Never 0 200000000 Time X17 108.01 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 34149912:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 1478187:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 16450063:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 7858954:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 20309197:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 13737079:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 1204669:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 18787657:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 1159917:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 13380016:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 1904511:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 13035248:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 3766854:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 28035616:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 24742120:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=773f6798f908e0cd810f3e878df07bab Observation X18 Never 0 200000000 Time X18 102.01 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 22417887:>0:r1=0; 0:r3=0; y=1; z=1; 14733865:>0:r1=1; 0:r3=0; y=1; z=1; 3721388:>0:r1=0; 0:r3=1; y=1; z=1; 22275927:>0:r1=1; 0:r3=1; y=1; z=1; 14116332:>0:r1=0; 0:r3=0; y=2; z=1; 3600723:>0:r1=1; 0:r3=0; y=2; z=1; 28221102:>0:r1=0; 0:r3=1; y=2; z=1; 27455541:>0:r1=1; 0:r3=1; y=2; z=1; 28765606:>0:r1=0; 0:r3=0; y=1; z=2; 1363072:>0:r1=1; 0:r3=0; y=1; z=2; 13500700:>0:r1=0; 0:r3=1; y=1; z=2; 6508006:>0:r1=1; 0:r3=1; y=1; z=2; 1187374:>0:r1=0; 0:r3=0; y=2; z=2; 11213568:>0:r1=0; 0:r3=1; y=2; z=2; 918909:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=811f0a85dc5f811c7436b53d2ca9c449 Observation X19 Never 0 200000000 Time X19 108.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 18944214:>0:r1=0; 0:r3=0; 1:r3=0; 3 :>0:r1=1; 0:r3=0; 1:r3=0; 47727644:>0:r1=0; 0:r3=1; 1:r3=0; 13468896:>0:r1=1; 0:r3=1; 1:r3=0; 50618683:>0:r1=0; 0:r3=0; 1:r3=1; 23542171:>0:r1=1; 0:r3=0; 1:r3=1; 4473678:>0:r1=0; 0:r3=1; 1:r3=1; 41224711:>0:r1=1; 0:r3=1; 1:r3=1; Ok Witnesses Positive: 3, Negative: 199999997 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is validated Hash=0c99e9e00ef12798cd94e468d7533fcb Observation X20 Sometimes 3 199999997 Time X20 74.63 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 11350492:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 2212262:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 23075135:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 22140482:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 23156115:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 17661665:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 707020:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 16711618:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 1473086:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 9636141:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 995782:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 38314537:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 3061987:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 18128633:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 11375045:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=10b56f844965b778138fc256080a6cb2 Observation X21 Never 0 200000000 Time X21 101.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 1267324:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 9401672:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 972180:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 33467152:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 1630576:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 19832122:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 9726193:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 12639964:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 2470057:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 23924072:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 22679403:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 24266084:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 17896393:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 956469:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 18870339:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=e7fc832a2e4b347328216cfab07885d9 Observation X22 Never 0 200000000 Time X22 99.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 12789501:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 2299938:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 25098767:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 23945328:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 25893947:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 18496700:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 2285544:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 22291805:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 1009973:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 8145795:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 791076:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 32083762:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 1388544:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 16426547:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 7052773:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=86fcf34749ab0aa370ea66e6893791a0 Observation X23 Never 0 200000000 Time X23 101.87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 51850625:>0:r1=0; 0:r3=0; y=1; 22824867:>0:r1=1; 0:r3=0; y=1; 7022461:>0:r1=0; 0:r3=1; y=1; 44633764:>0:r1=1; 0:r3=1; y=1; 15429606:>0:r1=0; 0:r3=0; y=2; 2 :>0:r1=1; 0:r3=0; y=2; 46258041:>0:r1=0; 0:r3=1; y=2; 11980634:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 2, Negative: 199999998 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=1a78bce42911eadebdb22805402de8eb Observation X24 Sometimes 2 199999998 Time X24 75.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 23871045:>0:r1=0; 0:r3=0; y=1; z=1; 16657165:>0:r1=1; 0:r3=0; y=1; z=1; 3289957:>0:r1=0; 0:r3=1; y=1; z=1; 21306223:>0:r1=1; 0:r3=1; y=1; z=1; 8583546:>0:r1=0; 0:r3=0; y=2; z=1; 1810917:>0:r1=1; 0:r3=0; y=2; z=1; 21846286:>0:r1=0; 0:r3=1; y=2; z=1; 18787063:>0:r1=1; 0:r3=1; y=2; z=1; 35804760:>0:r1=0; 0:r3=0; y=1; z=2; 2945668:>0:r1=1; 0:r3=0; y=1; z=2; 20855413:>0:r1=0; 0:r3=1; y=1; z=2; 13103830:>0:r1=1; 0:r3=1; y=1; z=2; 1026544:>0:r1=0; 0:r3=0; y=2; z=2; 9115808:>0:r1=0; 0:r3=1; y=2; z=2; 995775:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=629e26a0c6f613b14043edf57727b702 Observation X25 Never 0 200000000 Time X25 108.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 33956577:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 1586362:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 22180118:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 9816885:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 24585222:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 17066896:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 3856820:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 22027029:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 810403:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 9402075:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 938056:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 9758072:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 2245492:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 23257034:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 18512959:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=54da285ce144acabc337e28ea8958874 Observation X26 Never 0 200000000 Time X26 101.91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 20081952:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 9833003:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 14748689:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 2497874:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 1523252:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 24342671:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 21076980:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 20390489:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 36286748:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 1019071:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 2948587:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 17607110:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 13474967:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 12289797:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 1878810:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ffa63368caa391807dee9905d20510c6 Observation X27 Never 0 200000000 Time X27 97.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13263518:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 17943224:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 11296643:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 4503260:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 439916:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 23431970:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 14268067:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 35088208:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 32366568:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 2443799:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 1632307:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 1 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 14439712:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 15515727:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 10523177:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 2843903:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=4adca431a2784b4aa9df91b1fc3b1666 Observation X28 Sometimes 1 199999999 Time X28 84.95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 13526560:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 17849025:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 12010401:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 4794525:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 394723:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 21968011:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 13280403:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 34250994:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 34467154:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 2840430:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 1860239:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 13573514:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 16297111:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 10241282:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 2645628:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=cd58719fd03bc8a841de06004867cb05 Observation X29 Never 0 200000000 Time X29 85.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 18916247:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 9731262:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 13537614:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 2123381:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 1666081:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 25012330:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 21911150:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 21025266:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 36054241:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 1054949:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 2860985:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 18078166:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 13317372:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 12788603:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 1922353:>0:r1=1; 2:r1=1; 2:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=a0f55fa2291a072f015a1f0b83d20074 Observation X30 Never 0 200000000 Time X30 97.61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 19347118:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 10050498:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 14430346:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 2521857:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 1398191:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 24511125:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 20621085:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 20661361:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 36101296:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 1141957:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 3015174:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 18359301:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 13540872:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 12351501:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 1948318:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ffb6dc3e13fae7c7e7811955e241147b Observation X31 Never 0 200000000 Time X31 97.86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32325698:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 2951229:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 13270643:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 18401183:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 1159006:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=0; 11243337:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 5262224:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 14186374:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 15915434:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 756400:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 23505596:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 7781417:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 2980847:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 13090372:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 37170239:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=abdf662fb230128532b66df78e4a75f1 Observation X32 Sometimes 1 199999999 Time X32 82.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31970126:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 2922591:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 13371159:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 19214240:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 1296354:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 1 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; 12114413:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 5588953:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 13522080:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 15047579:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 719835:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 23053515:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 7901928:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 2642207:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 12824586:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 37810433:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=c86889a7cdc1c89457a71c414046d8c0 Observation X33 Sometimes 1 199999999 Time X33 83.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14146137:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 18522812:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 12263150:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 4741144:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 1036425:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 23792653:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 15059589:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 37991230:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 32225823:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 2146693:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 906585:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 1 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 13346725:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 14427297:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 6915055:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 2478681:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=8db91522dc421fe43a7baf7aff0de837 Observation X34 Sometimes 1 199999999 Time X34 85.50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14109908:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 18651559:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 12746893:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 4977014:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 887056:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 23467742:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 14973569:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 37730667:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 31574755:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 2341636:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 1117187:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 1 :>1:r1=1; 3:r1=1; 3:r3=0; x=2; 13084459:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 14557818:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 7301455:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 2478281:>1:r1=1; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=00744a65cf189719eb1309a79c27a2ca Observation X35 Sometimes 1 199999999 Time X35 85.24 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31783527:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 2293398:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 6728227:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 14334390:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 2306757:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 13771285:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 6523442:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 6795450:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 13850822:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 51037 :>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 16077375:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 14106712:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 6504628:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 15711040:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 49161910:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=08b576a9816ca91b136efc84cb8198fe Observation Y00 Never 0 200000000 Time Y00 98.05 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32299971:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 2175392:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 6857391:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 14842692:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 2560899:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 14662799:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 7291385:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 6216310:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 12684287:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 50243 :>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 16544170:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 13698533:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 6395806:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 14720796:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 48999326:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=27be645f8ce747a8241695ecd5d12775 Observation Y01 Never 0 200000000 Time Y01 97.66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 12382830:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 17544914:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 442851:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 23588640:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 11661225:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 4861449:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 16973326:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 42939131:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 29147394:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 2561788:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 8406214:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 16113853:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 1156134:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 8365907:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 3854344:>0:r1=1; 0:r4=1; 2:r1=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is NOT validated Hash=e299ccd513ee6b40ffc1479736b6d80f Observation Y02 Never 0 200000000 Time Y02 101.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 37318748:>0:r1=0; 0:r4=0; y=1; 23647067:>0:r1=1; 0:r4=0; y=1; 512271:>0:r1=0; 0:r4=1; y=1; 51676795:>0:r1=1; 0:r4=1; y=1; 16052423:>0:r1=0; 0:r4=0; y=2; 36590957:>0:r1=0; 0:r4=1; y=2; 34201739:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=fbc1c062cf6f3291c2ce205045bcf85e Observation Y03 Never 0 200000000 Time Y03 77.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13369572:>0:r1=0; 0:r4=0; y=1; z=1; 16300681:>0:r1=1; 0:r4=0; y=1; z=1; 244370:>0:r1=0; 0:r4=1; y=1; z=1; 22581925:>0:r1=1; 0:r4=1; y=1; z=1; 9626009:>0:r1=0; 0:r4=0; y=2; z=1; 3379280:>0:r1=1; 0:r4=0; y=2; z=1; 13775929:>0:r1=0; 0:r4=1; y=2; z=1; 37732555:>0:r1=1; 0:r4=1; y=2; z=1; 26289635:>0:r1=0; 0:r4=0; y=1; z=2; 3637306:>0:r1=1; 0:r4=0; y=1; z=2; 10575766:>0:r1=0; 0:r4=1; y=1; z=2; 23979088:>0:r1=1; 0:r4=1; y=1; z=2; 1467825:>0:r1=0; 0:r4=0; y=2; z=2; 10857740:>0:r1=0; 0:r4=1; y=2; z=2; 6182319:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=00bb906e6b50e3e5b6bc490a41e163e4 Observation Y04 Never 0 200000000 Time Y04 110.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) 30500555:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 2160839:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 9644051:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 18297866:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 13114887:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 16179865:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 340344:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 24468428:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 1345807:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 10734705:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 5772541:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 9470255:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 4123632:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 14670848:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 39175377:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=2d110167698039bf55def82743b120ef Observation Y05 Never 0 200000000 Time Y05 103.87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14848485:>0:r1=0; 0:r4=0; y=1; z=1; 16512637:>0:r1=1; 0:r4=0; y=1; z=1; 1263791:>0:r1=0; 0:r4=1; y=1; z=1; 29401454:>0:r1=1; 0:r4=1; y=1; z=1; 10281068:>0:r1=0; 0:r4=0; y=2; z=1; 3704751:>0:r1=1; 0:r4=0; y=2; z=1; 16142129:>0:r1=0; 0:r4=1; y=2; z=1; 42859521:>0:r1=1; 0:r4=1; y=2; z=1; 26887940:>0:r1=0; 0:r4=0; y=1; z=2; 1979845:>0:r1=1; 0:r4=0; y=1; z=2; 8603622:>0:r1=0; 0:r4=1; y=1; z=2; 14635505:>0:r1=1; 0:r4=1; y=1; z=2; 1088501:>0:r1=0; 0:r4=0; y=2; z=2; 9043858:>0:r1=0; 0:r4=1; y=2; z=2; 2746893:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5519b7e18d61900b26b6e20148fd6e5b Observation Y06 Never 0 200000000 Time Y06 110.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 16300255:>0:r1=0; 0:r4=0; 1:r3=0; 35243270:>0:r1=0; 0:r4=1; 1:r3=0; 28538263:>0:r1=1; 0:r4=1; 1:r3=0; 38215099:>0:r1=0; 0:r4=0; 1:r3=1; 27654841:>0:r1=1; 0:r4=0; 1:r3=1; 517895:>0:r1=0; 0:r4=1; 1:r3=1; 53530377:>0:r1=1; 0:r4=1; 1:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=75dc62611c83cbf21aa9273aa6a41b23 Observation Y07 Never 0 200000000 Time Y07 76.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8792552:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 2207208:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 14892151:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 33288872:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 15041976:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 19174909:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 229692:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 23395665:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 1123344:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 7904468:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 3564093:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 28704953:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 4175896:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 12072970:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 25431251:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=6f98559c8174fdcd1fe2a621ad7dc8d2 Observation Y08 Never 0 200000000 Time Y08 103.86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 906576:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 7795570:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 3197854:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 30604398:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 2457690:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 11781107:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 20719972:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 9181590:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 2644584:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 15299641:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 35175332:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 15562857:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 18924400:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 307071:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 25441358:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=f9c57151a878a2fb7ca88a7241079b1d Observation Y09 Never 0 200000000 Time Y09 102.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y10.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y10 "Rf*e DpAddrdR Fre SyncdWR Fre SyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | sync | lwsync ; lwzx r4,r3,r5 | lwz r3,0(r4) | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | | ; exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: sync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y10 Allowed Histogram (15 states) 9152850:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 2558222:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 16060537:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 35249162:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 17226753:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 21185877:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 556520:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 30219249:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 758353:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 6856060:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 2700297:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 28068235:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 2176911:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 10622309:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 16608665:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=d987b1dfa9ff6dbc9cfc5646bda90ed3 Observation Y10 Never 0 200000000 Time Y10 104.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 38869646:>0:r1=0; 0:r4=0; y=1; 24766639:>0:r1=1; 0:r4=0; y=1; 1314661:>0:r1=0; 0:r4=1; y=1; 59508517:>0:r1=1; 0:r4=1; y=1; 14311099:>0:r1=0; 0:r4=0; y=2; 36638558:>0:r1=0; 0:r4=1; y=2; 24590880:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5506d17360dcb64cbec742d67fe4340e Observation Y11 Never 0 200000000 Time Y11 77.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15862185:>0:r1=0; 0:r4=0; y=1; z=1; 19884783:>0:r1=1; 0:r4=0; y=1; z=1; 881024:>0:r1=0; 0:r4=1; y=1; z=1; 28747653:>0:r1=1; 0:r4=1; y=1; z=1; 6296945:>0:r1=0; 0:r4=0; y=2; z=1; 2079974:>0:r1=1; 0:r4=0; y=2; z=1; 13801481:>0:r1=0; 0:r4=1; y=2; z=1; 28846546:>0:r1=1; 0:r4=1; y=2; z=1; 28402370:>0:r1=0; 0:r4=0; y=1; z=2; 4202384:>0:r1=1; 0:r4=0; y=1; z=2; 13332595:>0:r1=0; 0:r4=1; y=1; z=2; 26544612:>0:r1=1; 0:r4=1; y=1; z=2; 630103:>0:r1=0; 0:r4=0; y=2; z=2; 7318052:>0:r1=0; 0:r4=1; y=2; z=2; 3169293:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=e74570fa8cc4ed49e2bc7eb3e6efaadc Observation Y12 Never 0 200000000 Time Y12 110.79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30714439:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 2381764:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 13028276:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 21156518:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 16244106:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 19022105:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 1074302:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 30971820:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 684544:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 7830779:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 2725840:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 7193674:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 2128082:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 15497161:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 29346590:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=d514c17376c3fe56c7da249e5154e952 Observation Y13 Never 0 200000000 Time Y13 104.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 18782811:>0:r1=0; 0:r4=0; y=1; z=1; 20608982:>0:r1=1; 0:r4=0; y=1; z=1; 1412430:>0:r1=0; 0:r4=1; y=1; z=1; 36822563:>0:r1=1; 0:r4=1; y=1; z=1; 7216589:>0:r1=0; 0:r4=0; y=2; z=1; 2063354:>0:r1=1; 0:r4=0; y=2; z=1; 15484037:>0:r1=0; 0:r4=1; y=2; z=1; 30643216:>0:r1=1; 0:r4=1; y=2; z=1; 27214993:>0:r1=0; 0:r4=0; y=1; z=2; 2140421:>0:r1=1; 0:r4=0; y=1; z=2; 11623531:>0:r1=0; 0:r4=1; y=1; z=2; 17007877:>0:r1=1; 0:r4=1; y=1; z=2; 428816:>0:r1=0; 0:r4=0; y=2; z=2; 6301907:>0:r1=0; 0:r4=1; y=2; z=2; 2248473:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=db5bc36ebd8ef1745e795c6bdf75e423 Observation Y14 Never 0 200000000 Time Y14 110.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31716963:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 2719000:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 6950626:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 14714388:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 2853732:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 14478061:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 7241110:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 6962441:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 14096244:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 48550 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 15085801:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 14715031:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 7020949:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 14583791:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 46813313:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=11eec175e5c988e350ebfc54fd0e2c1c Observation Y15 Never 0 200000000 Time Y15 98.73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 37798843:>0:r1=0; 0:r3=0; y=1; 25486276:>0:r1=1; 0:r3=0; y=1; 534713:>0:r1=0; 0:r3=1; y=1; 50834018:>0:r1=1; 0:r3=1; y=1; 15503428:>0:r1=0; 0:r3=0; y=2; 33734980:>0:r1=0; 0:r3=1; y=2; 36107742:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=8e9853ba7646212616eafb737d8e71e4 Observation Y16 Never 0 200000000 Time Y16 77.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 12694990:>0:r1=0; 0:r3=0; y=1; z=1; 16173718:>0:r1=1; 0:r3=0; y=1; z=1; 236069:>0:r1=0; 0:r3=1; y=1; z=1; 22101265:>0:r1=1; 0:r3=1; y=1; z=1; 9765924:>0:r1=0; 0:r3=0; y=2; z=1; 3608921:>0:r1=1; 0:r3=0; y=2; z=1; 13519642:>0:r1=0; 0:r3=1; y=2; z=1; 38222711:>0:r1=1; 0:r3=1; y=2; z=1; 27770858:>0:r1=0; 0:r3=0; y=1; z=2; 3726565:>0:r1=1; 0:r3=0; y=1; z=2; 10280630:>0:r1=0; 0:r3=1; y=1; z=2; 23189322:>0:r1=1; 0:r3=1; y=1; z=2; 1706500:>0:r1=0; 0:r3=0; y=2; z=2; 10896613:>0:r1=0; 0:r3=1; y=2; z=2; 6106272:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=5dde3da66b8fd3eb942a6c2fb7e9050b Observation Y17 Never 0 200000000 Time Y17 110.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31066462:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 2466361:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 9109593:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 17423114:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 13771160:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 17299552:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 398762:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 23950656:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 1157283:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 10411559:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 5320617:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 9579980:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 4272865:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 15182735:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 38589301:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=abfe8f96fb73d61f24cd4ed25c4cbe36 Observation Y18 Never 0 200000000 Time Y18 104.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15779119:>0:r1=0; 0:r3=0; y=1; z=1; 18526763:>0:r1=1; 0:r3=0; y=1; z=1; 1139426:>0:r1=0; 0:r3=1; y=1; z=1; 29510210:>0:r1=1; 0:r3=1; y=1; z=1; 10425827:>0:r1=0; 0:r3=0; y=2; z=1; 4140118:>0:r1=1; 0:r3=0; y=2; z=1; 15453672:>0:r1=0; 0:r3=1; y=2; z=1; 41225368:>0:r1=1; 0:r3=1; y=2; z=1; 26790636:>0:r1=0; 0:r3=0; y=1; z=2; 2227465:>0:r1=1; 0:r3=0; y=1; z=2; 7956790:>0:r1=0; 0:r3=1; y=1; z=2; 14107263:>0:r1=1; 0:r3=1; y=1; z=2; 1089834:>0:r1=0; 0:r3=0; y=2; z=2; 8613491:>0:r1=0; 0:r3=1; y=2; z=2; 3014018:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=a4ab8a1891a2982f2576f75c35f64825 Observation Y19 Never 0 200000000 Time Y19 111.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 16937254:>0:r1=0; 0:r3=0; 1:r3=0; 36324850:>0:r1=0; 0:r3=1; 1:r3=0; 26788908:>0:r1=1; 0:r3=1; 1:r3=0; 38579186:>0:r1=0; 0:r3=0; 1:r3=1; 26626275:>0:r1=1; 0:r3=0; 1:r3=1; 500609:>0:r1=0; 0:r3=1; 1:r3=1; 54242918:>0:r1=1; 0:r3=1; 1:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=310ba9b87ba9c8abbb2cb09115abba03 Observation Y20 Never 0 200000000 Time Y20 76.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y21.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y21 "Rf*e DpCtrlIsyncdR Fre SyncdWR Fre LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | sync | lwsync | lwsync ; beq LC01 | lwz r3,0(r4) | li r3,1 | li r3,1 ; LC01: | | stw r3,0(r4) | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y21 Allowed Histogram (15 states) 8956863:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 2544338:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 15618211:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 33542058:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 14808653:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 20806860:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 248172:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 20817625:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 1141744:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 8179039:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 3379463:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 30988140:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 4548181:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 11367938:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 23052715:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=63a4ff1b2a8c61b6b9352662bce3e8c9 Observation Y21 Never 0 200000000 Time Y21 103.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 952681:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 7563330:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 3303711:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 29135365:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 2794815:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 10889215:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 20481149:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 9395253:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 2736625:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 16640155:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 33840964:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 15637692:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 20813117:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 327890:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 25488038:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=8a2b1f87ebce2fea7bdd4e78ab49e198 Observation Y22 Never 0 200000000 Time Y22 100.32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9859018:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 2825895:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 16717822:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 35028584:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 17522315:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 22261784:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 559691:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 28743658:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 837211:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 6773149:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 2680503:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 27852772:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 2326384:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 10430635:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 15580579:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=34f72841a6635924e4f6e89a17ea5886 Observation Y23 Never 0 200000000 Time Y23 103.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 38749487:>0:r1=0; 0:r3=0; y=1; 26789892:>0:r1=1; 0:r3=0; y=1; 1418453:>0:r1=0; 0:r3=1; y=1; 58536429:>0:r1=1; 0:r3=1; y=1; 13928846:>0:r1=0; 0:r3=0; y=2; 35516938:>0:r1=0; 0:r3=1; y=2; 25059955:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=967cc1d43171137af345c68503a9bda3 Observation Y24 Never 0 200000000 Time Y24 77.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15726009:>0:r1=0; 0:r3=0; y=1; z=1; 19810327:>0:r1=1; 0:r3=0; y=1; z=1; 918486:>0:r1=0; 0:r3=1; y=1; z=1; 28984801:>0:r1=1; 0:r3=1; y=1; z=1; 6594351:>0:r1=0; 0:r3=0; y=2; z=1; 2083941:>0:r1=1; 0:r3=0; y=2; z=1; 13954080:>0:r1=0; 0:r3=1; y=2; z=1; 28519441:>0:r1=1; 0:r3=1; y=2; z=1; 29338064:>0:r1=0; 0:r3=0; y=1; z=2; 4254282:>0:r1=1; 0:r3=0; y=1; z=2; 12442970:>0:r1=0; 0:r3=1; y=1; z=2; 25946003:>0:r1=1; 0:r3=1; y=1; z=2; 727410:>0:r1=0; 0:r3=0; y=2; z=2; 7674272:>0:r1=0; 0:r3=1; y=2; z=2; 3025563:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=67d202536303d5d116d23867165f4ed6 Observation Y25 Never 0 200000000 Time Y25 110.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31440189:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 2604491:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 12542052:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 20692674:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 16647143:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 19932906:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 1143462:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 30735239:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 637875:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 7622791:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 2699797:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 6982733:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 2196858:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 15471648:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 28650142:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=44ca19804af93c9cee9c0f6acff5a2b0 Observation Y26 Never 0 200000000 Time Y26 103.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11402312:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 11978676:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 17549849:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 5355177:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 461511:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 16971794:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 22044750:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 43268867:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 30774891:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 1204204:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 2647676:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 8186724:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 8212389:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 16144180:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 3797000:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ad65804aeb1597ba714e2328512d7995 Observation Y27 Never 0 200000000 Time Y27 101.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8365094:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 13293381:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 14101574:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 5123208:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 40697 :>1:r1=0; 3:r1=0; 3:r4=1; x=1; 12910075:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 17426927:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 48864355:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 27914287:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 2426911:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 2825672:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 7850845:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 12185092:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 20577025:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 6094857:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=ce1b4a24ee0901b9de433860bfb46080 Observation Y28 Never 0 200000000 Time Y28 87.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8662419:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 13561576:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 14360490:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 5556276:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 50188 :>1:r1=0; 3:r1=0; 3:r3=1; x=1; 12672153:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 17020556:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 48879014:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 27147077:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 2569993:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 3117967:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 7876473:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 12069342:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 20336966:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 6119510:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=8bc55273b7032305e0142605023bce2d Observation Y29 Never 0 200000000 Time Y29 87.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11262033:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 11557508:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 16758886:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 4586739:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 350383:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 17262547:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 24011250:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 44269483:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 30272593:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 1129894:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 2594815:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 8082375:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 7996106:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 16430200:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 3435188:>0:r1=1; 2:r1=1; 2:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=3e1573bf73b4fdef87461b3565d66b20 Observation Y30 Never 0 200000000 Time Y30 101.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11539056:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 12705560:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 17380777:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 5077252:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 429878:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 17658728:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 22507768:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 43196850:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 28501201:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 1342294:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 2666390:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 8577847:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 8520483:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 16278246:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 3617670:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=e6774eda20819c8f372129af64bca016 Observation Y31 Never 0 200000000 Time Y31 101.18 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 29049198:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 2614148:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 7865156:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 12907570:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 2165928:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 14395734:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 6194724:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 7700216:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 13113372:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 74805 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 13943561:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 16144311:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 5882661:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 16610485:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 51338131:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=a577eb9c8f1d583ecead3fdf77525a1e Observation Y32 Never 0 200000000 Time Y32 84.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 29586504:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 2951617:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 8322329:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 13758789:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 2317573:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 14634993:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 6458555:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 7797732:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 12722372:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 83157 :>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 13845843:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 16028887:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 5679730:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 15280343:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 50531576:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=eea22bd3e2446126dd9b287b5df5faca Observation Y33 Never 0 200000000 Time Y33 84.65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8537352:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 13367772:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 14656910:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 5649094:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 182220:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 14514612:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 18436764:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 52343544:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 28825943:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 2197065:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 1711277:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 7558084:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 11746912:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 15115572:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 5156879:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=49482953dd91da1bcee183b3b0b006b8 Observation Y34 Never 0 200000000 Time Y34 86.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9155246:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 13776789:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 15507465:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 6021350:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 161881:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 14227932:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 17660487:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 51242623:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 28676667:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 2265955:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 1898666:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 7573174:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 11867924:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 14821047:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 5142794:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=1ab190404386bf69014d12d891f99e7c Observation Y35 Never 0 200000000 Time Y35 86.89 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=+ra Sat Jan 22 10:58:53 CST 2011