Sat Jan 22 20:00:22 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) 33849835:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 224302:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 13369989:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 23031787:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 215739:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 18 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=0; 7465261:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 4898420:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 13075072:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 7421616:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 3238335:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 29583538:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 22789275:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 5425055:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 29495925:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 5915833:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; Ok Witnesses Positive: 18, Negative: 199999982 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is validated Hash=6559e19d9e37619f3f8bf433a5805105 Observation X00 Sometimes 18 199999982 Time X00 83.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X01.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X01 "Rfe DpAddrdR Fre LwSyncdWW Rfe DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | beq LC00 | lwsync ; | li r3,1 | LC00: | li r3,1 ; | stw r3,0(r4) | isync | stw r3,0(r4) ; | | lwz r3,0(r4) | ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: cmpw 3,3 _litmus_P2_2_: beq LitLC00 _litmus_P2_3_: LitLC00: _litmus_P2_4_: isync _litmus_P2_5_: lwz 31,0(9) Test X01 Allowed Histogram (16 states) 33978664:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 221360:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 13512805:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 23110600:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 219562:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 12 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=0; 7504114:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 4868039:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 13231227:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 7468111:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 3199254:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 29554931:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 22553629:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 5403904:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 29313311:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 5860477:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 12, Negative: 199999988 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=2dd158f1ef0b66595a56ff21c6e00a13 Observation X01 Sometimes 12 199999988 Time X01 83.05 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 20180952:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 10084346:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 4619371:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 30554241:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 15996711:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 2168037:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 27905978:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 7028044:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 32557498:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 283456:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 16159518:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 25072041:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 326670:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 5359408:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 1703729:>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 91.80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (7 states) 51369399:>0:r1=0; 0:r4=0; y=1; 18210925:>0:r1=1; 0:r4=0; y=1; 4178575:>0:r1=0; 0:r4=1; y=1; 41462701:>0:r1=1; 0:r4=1; y=1; 15774661:>0:r1=0; 0:r4=0; y=2; 57874550:>0:r1=0; 0:r4=1; y=2; 11129189:>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=979eb45568765c8b5bb24cb8beb2a694 Observation X03 Never 0 200000000 Time X03 73.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 17581198:>0:r1=0; 0:r4=0; y=1; z=1; 9076258:>0:r1=1; 0:r4=0; y=1; z=1; 2874408:>0:r1=0; 0:r4=1; y=1; z=1; 29632592:>0:r1=1; 0:r4=1; y=1; z=1; 12011602:>0:r1=0; 0:r4=0; y=2; z=1; 3204798:>0:r1=1; 0:r4=0; y=2; z=1; 20545828:>0:r1=0; 0:r4=1; y=2; z=1; 14421777:>0:r1=1; 0:r4=1; y=2; z=1; 34430700:>0:r1=0; 0:r4=0; y=1; z=2; 482051:>0:r1=1; 0:r4=0; y=1; z=2; 12812060:>0:r1=0; 0:r4=1; y=1; z=2; 19551764:>0:r1=1; 0:r4=1; y=1; z=2; 3359204:>0:r1=0; 0:r4=0; y=2; z=2; 12461367:>0:r1=0; 0:r4=1; y=2; z=2; 7554393:>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 98.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X05.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X05 "Rfe DpAddrdR Fre LwSyncdWW Wse SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | sync | lwsync ; | li r3,1 | lwz r3,0(r4) | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X05 Allowed Histogram (16 states) 32893187:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 103957:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 12801494:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 5383666:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 12801111:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 5385499:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 2974241:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 30334346:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 32239 :>0:r1=0; 0:r4=0; 2:r3=0; y=2; 1 :>0:r1=1; 0:r4=0; 2:r3=0; y=2; 3602547:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 5004007:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 25391847:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 9190042:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 37263679:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 16838137:>0:r1=1; 0:r4=1; 2:r3=1; y=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is validated Hash=2f45a04baa1582caaf7bebb0f6429fad Observation X05 Sometimes 1 199999999 Time X05 96.50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13976664:>0:r1=0; 0:r4=0; y=1; z=1; 7491362:>0:r1=1; 0:r4=0; y=1; z=1; 7047886:>0:r1=0; 0:r4=1; y=1; z=1; 38242594:>0:r1=1; 0:r4=1; y=1; z=1; 21813642:>0:r1=0; 0:r4=0; y=2; z=1; 6727124:>0:r1=1; 0:r4=0; y=2; z=1; 33593491:>0:r1=0; 0:r4=1; y=2; z=1; 25775103:>0:r1=1; 0:r4=1; y=2; z=1; 33447313:>0:r1=0; 0:r4=0; y=1; z=2; 23866 :>0:r1=1; 0:r4=0; y=1; z=2; 4190863:>0:r1=0; 0:r4=1; y=1; z=2; 3636299:>0:r1=1; 0:r4=1; y=1; z=2; 28730 :>0:r1=0; 0:r4=0; y=2; z=2; 2505113:>0:r1=0; 0:r4=1; y=2; z=2; 1499950:>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 98.08 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X07.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X07 "Rfe DpAddrdR Fre SyncdWR Fre LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; lwz r1,0(r2) | li r1,1 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | lwsync ; | lwz r3,0(r4) | li r3,1 ; | | stw r3,0(r4) ; exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 31,1 _litmus_P1_1_: stw 31,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 30,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X07 Allowed Histogram (8 states) 17195441:>0:r1=0; 0:r4=0; 1:r3=0; 1 :>0:r1=1; 0:r4=0; 1:r3=0; 46855373:>0:r1=0; 0:r4=1; 1:r3=0; 6354695:>0:r1=1; 0:r4=1; 1:r3=0; 52771683:>0:r1=0; 0:r4=0; 1:r3=1; 19544938:>0:r1=1; 0:r4=0; 1:r3=1; 8913254:>0:r1=0; 0:r4=1; 1:r3=1; 48364615:>0:r1=1; 0:r4=1; 1:r3=1; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is validated Hash=27f80466ebe5b987c02fd5b2375e9014 Observation X07 Sometimes 1 199999999 Time X07 72.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7283433:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 34976 :>0:r1=1; 0:r4=0; 1:r3=0; z=1; 22469541:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 10141903:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 23863090:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 20356429:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 2065632:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 20632783:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 6135056:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 6695795:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 165986:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 44057100:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 2908172:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 17753658:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 15436446:>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 95.63 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 25750 :>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 3121524:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 1947021:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 32486014:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 65749 :>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 15445729:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 12493302:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 14759033:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 502624:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 30227464:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 15044932:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 24388519:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 21658871:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 2338197:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 25495271:>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 88.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14489840:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 491457:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 28763127:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 16775733:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 26290125:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 22083897:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 7276038:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 25835329:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 24242 :>0:r1=0; 0:r4=0; 1:r3=0; z=2; 3528543:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 1011530:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 33250778:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 39422 :>0:r1=1; 0:r4=0; 1:r3=1; z=2; 15508843:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 4631096:>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 96.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X11.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X11 "Rfe DpAddrdR Fre SyncdWW Wse LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; lwz r1,0(r2) | li r1,1 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | lwsync ; | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 27,0(11) _litmus_P0_1_: xor 10,27,27 _litmus_P0_2_: lwzx 28,10,9 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X11 Allowed Histogram (8 states) 53812078:>0:r1=0; 0:r4=0; y=1; 19006738:>0:r1=1; 0:r4=0; y=1; 13301835:>0:r1=0; 0:r4=1; y=1; 48499282:>0:r1=1; 0:r4=1; y=1; 15859315:>0:r1=0; 0:r4=0; y=2; 1 :>0:r1=1; 0:r4=0; y=2; 44848559:>0:r1=0; 0:r4=1; y=2; 4672192:>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=2e151daaab42138b8c478ba081d896ed Observation X11 Sometimes 1 199999999 Time X11 74.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 22931192:>0:r1=0; 0:r4=0; y=1; z=1; 19258032:>0:r1=1; 0:r4=0; y=1; z=1; 9965281:>0:r1=0; 0:r4=1; y=1; z=1; 29154929:>0:r1=1; 0:r4=1; y=1; z=1; 8469150:>0:r1=0; 0:r4=0; y=2; z=1; 28275 :>0:r1=1; 0:r4=0; y=2; z=1; 12763271:>0:r1=0; 0:r4=1; y=2; z=1; 6387517:>0:r1=1; 0:r4=1; y=2; z=1; 39254623:>0:r1=0; 0:r4=0; y=1; z=2; 3541324:>0:r1=1; 0:r4=0; y=1; z=2; 15064341:>0:r1=0; 0:r4=1; y=1; z=2; 22969163:>0:r1=1; 0:r4=1; y=1; z=2; 3894390:>0:r1=0; 0:r4=0; y=2; z=2; 6016363:>0:r1=0; 0:r4=1; y=2; z=2; 302149:>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 98.65 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X13.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X13 "Rfe DpAddrdR Fre SyncdWW Wse SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | sync | lwsync ; | li r3,1 | lwz r3,0(r4) | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X13 Allowed Histogram (15 states) 33249774:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 143486:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 19177615:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 9706559:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 25555304:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 21180522:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 11811408:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 31254793:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 21993 :>0:r1=0; 0:r4=0; 2:r3=0; y=2; 3679339:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 1245941:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 13953827:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 513655:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 20032138:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 8473646:>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 95.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 23197736:>0:r1=0; 0:r4=0; y=1; z=1; 20946571:>0:r1=1; 0:r4=0; y=1; z=1; 12248547:>0:r1=0; 0:r4=1; y=1; z=1; 39502333:>0:r1=1; 0:r4=1; y=1; z=1; 13849866:>0:r1=0; 0:r4=0; y=2; z=1; 258550:>0:r1=1; 0:r4=0; y=2; z=1; 19906924:>0:r1=0; 0:r4=1; y=2; z=1; 11802243:>0:r1=1; 0:r4=1; y=2; z=1; 33748425:>0:r1=0; 0:r4=0; y=1; z=2; 62305 :>0:r1=1; 0:r4=0; y=1; z=2; 11419580:>0:r1=0; 0:r4=1; y=1; z=2; 9623428:>0:r1=1; 0:r4=1; y=1; z=2; 21948 :>0:r1=0; 0:r4=0; y=2; z=2; 1863497:>0:r1=0; 0:r4=1; y=2; z=2; 1548047:>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 98.79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X15.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X15 "Rfe DpCtrlIsyncdR Fre LwSyncdWW Rfe DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; beq LC00 | lwsync | beq LC01 | lwsync ; LC00: | li r3,1 | LC01: | li r3,1 ; isync | stw r3,0(r4) | isync | stw r3,0(r4) ; lwz r3,0(r4) | | lwz r3,0(r4) | ; exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: cmpw 30,30 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 31,0(9) _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: cmpw 3,3 _litmus_P2_2_: beq LitLC01 _litmus_P2_3_: LitLC01: _litmus_P2_4_: isync _litmus_P2_5_: lwz 31,0(9) Test X15 Allowed Histogram (16 states) 33994672:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 227026:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 13602629:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 22926127:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 212856:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 17 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=0; 7530406:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 4931938:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 13363463:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 7459355:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 3163209:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 29376264:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 22641432:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 5413787:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 29270594:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 5886225:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 17, Negative: 199999983 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=a488ac47b1a88d9c3f30dcee477424e5 Observation X15 Sometimes 17 199999983 Time X15 83.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 51736015:>0:r1=0; 0:r3=0; y=1; 18236273:>0:r1=1; 0:r3=0; y=1; 3898395:>0:r1=0; 0:r3=1; y=1; 41308235:>0:r1=1; 0:r3=1; y=1; 15939460:>0:r1=0; 0:r3=0; y=2; 1 :>0:r1=1; 0:r3=0; y=2; 59474644:>0:r1=0; 0:r3=1; y=2; 9406977:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=7cfc2b26a1cbcdd15d0fab061a637ce4 Observation X16 Sometimes 1 199999999 Time X16 73.62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14605287:>0:r1=0; 0:r3=0; y=1; z=1; 7578766:>0:r1=1; 0:r3=0; y=1; z=1; 3385003:>0:r1=0; 0:r3=1; y=1; z=1; 27856644:>0:r1=1; 0:r3=1; y=1; z=1; 17681298:>0:r1=0; 0:r3=0; y=2; z=1; 4627756:>0:r1=1; 0:r3=0; y=2; z=1; 23264216:>0:r1=0; 0:r3=1; y=2; z=1; 15738514:>0:r1=1; 0:r3=1; y=2; z=1; 34544243:>0:r1=0; 0:r3=0; y=1; z=2; 418763:>0:r1=1; 0:r3=0; y=1; z=2; 12063816:>0:r1=0; 0:r3=1; y=1; z=2; 19157179:>0:r1=1; 0:r3=1; y=1; z=2; 1429526:>0:r1=0; 0:r3=0; y=2; z=2; 10352454:>0:r1=0; 0:r3=1; y=2; z=2; 7296535:>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 98.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X18.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X18 "Rfe DpCtrlIsyncdR Fre LwSyncdWW Wse SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | lwsync | sync | lwsync ; LC00: | li r3,1 | lwz r3,0(r4) | li r3,1 ; isync | stw r3,0(r4) | | stw r3,0(r4) ; lwz r3,0(r4) | | | ; exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X18 Allowed Histogram (16 states) 32759800:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 98921 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 13647025:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 4444608:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 11401811:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 4622679:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 2958724:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 29106482:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 37697 :>0:r1=0; 0:r3=0; 2:r3=0; y=2; 2 :>0:r1=1; 0:r3=0; 2:r3=0; y=2; 3806907:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 4739200:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 27259346:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 10140448:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 37762701:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 17213649:>0:r1=1; 0:r3=1; 2:r3=1; y=2; Ok Witnesses Positive: 2, Negative: 199999998 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is validated Hash=773f6798f908e0cd810f3e878df07bab Observation X18 Sometimes 2 199999998 Time X18 96.27 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11120085:>0:r1=0; 0:r3=0; y=1; z=1; 5300996:>0:r1=1; 0:r3=0; y=1; z=1; 7366927:>0:r1=0; 0:r3=1; y=1; z=1; 37088692:>0:r1=1; 0:r3=1; y=1; z=1; 25490835:>0:r1=0; 0:r3=0; y=2; z=1; 8555713:>0:r1=1; 0:r3=0; y=2; z=1; 34081887:>0:r1=0; 0:r3=1; y=2; z=1; 26918834:>0:r1=1; 0:r3=1; y=2; z=1; 32750761:>0:r1=0; 0:r3=0; y=1; z=2; 20803 :>0:r1=1; 0:r3=0; y=1; z=2; 4144488:>0:r1=0; 0:r3=1; y=1; z=2; 3329491:>0:r1=1; 0:r3=1; y=1; z=2; 34857 :>0:r1=0; 0:r3=0; y=2; z=2; 2373818:>0:r1=0; 0:r3=1; y=2; z=2; 1421813:>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 98.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (7 states) 17467650:>0:r1=0; 0:r3=0; 1:r3=0; 46896288:>0:r1=0; 0:r3=1; 1:r3=0; 6349661:>0:r1=1; 0:r3=1; 1:r3=0; 52547191:>0:r1=0; 0:r3=0; 1:r3=1; 19609530:>0:r1=1; 0:r3=0; 1:r3=1; 8992295:>0:r1=0; 0:r3=1; 1:r3=1; 48137385:>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=0c99e9e00ef12798cd94e468d7533fcb Observation X20 Never 0 200000000 Time X20 73.74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9959003:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 34818 :>0:r1=1; 0:r3=0; 1:r3=0; z=1; 25330566:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 10321977:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 24015233:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 20631656:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 2132338:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 20786497:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 3508915:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 3507641:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 123054:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 43581811:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 2887517:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 17931268:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 15247706:>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 95.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 25700 :>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 3379624:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 1755774:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 32433776:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 74835 :>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 16409128:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 11546206:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 14840251:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 501147:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 30176961:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 14991421:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 24578690:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 21369961:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 2315798:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 25600728:>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 88.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14455121:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 501606:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 28129032:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 17095392:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 26480570:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 22650589:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 7231758:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 25688108:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 24768 :>0:r1=0; 0:r3=0; 1:r3=0; z=2; 3460350:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 890498:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 32811200:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 43349 :>0:r1=1; 0:r3=0; 1:r3=1; z=2; 15915035:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 4622624:>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 95.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 53677143:>0:r1=0; 0:r3=0; y=1; 19165620:>0:r1=1; 0:r3=0; y=1; 13256104:>0:r1=0; 0:r3=1; y=1; 48578408:>0:r1=1; 0:r3=1; y=1; 16084629:>0:r1=0; 0:r3=0; y=2; 3 :>0:r1=1; 0:r3=0; y=2; 44444144:>0:r1=0; 0:r3=1; y=2; 4793949:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 3, Negative: 199999997 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=1a78bce42911eadebdb22805402de8eb Observation X24 Sometimes 3 199999997 Time X24 74.62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 23568765:>0:r1=0; 0:r3=0; y=1; z=1; 19419763:>0:r1=1; 0:r3=0; y=1; z=1; 10325453:>0:r1=0; 0:r3=1; y=1; z=1; 27295291:>0:r1=1; 0:r3=1; y=1; z=1; 10434711:>0:r1=0; 0:r3=0; y=2; z=1; 30867 :>0:r1=1; 0:r3=0; y=2; z=1; 15505325:>0:r1=0; 0:r3=1; y=2; z=1; 6909714:>0:r1=1; 0:r3=1; y=2; z=1; 39283940:>0:r1=0; 0:r3=0; y=1; z=2; 3486948:>0:r1=1; 0:r3=0; y=1; z=2; 14203888:>0:r1=0; 0:r3=1; y=1; z=2; 22742175:>0:r1=1; 0:r3=1; y=1; z=2; 2278274:>0:r1=0; 0:r3=0; y=2; z=2; 4152340:>0:r1=0; 0:r3=1; y=2; z=2; 362546:>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 97.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33113403:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 138511:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 20186397:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 8463712:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 25692250:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 21678770:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 11693902:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 29731107:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 22419 :>0:r1=0; 0:r3=0; 2:r3=0; y=2; 3939305:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 1124145:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 14206794:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 547181:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 20606681:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 8855423:>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 96.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X27.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X27 "Rfe DpCtrldW Wse LwSyncdWW Rfe DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; beq LC00 | lwsync | beq LC01 | lwsync ; LC00: | li r3,1 | LC01: | li r3,1 ; li r3,1 | stw r3,0(r4) | isync | stw r3,0(r4) ; stw r3,0(r4) | | lwz r3,0(r4) | ; exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 3,0(11) _litmus_P0_1_: cmpw 3,3 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: li 30,1 _litmus_P0_5_: stw 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: lwz 28,0(11) _litmus_P2_1_: cmpw 28,28 _litmus_P2_2_: beq LitLC01 _litmus_P2_3_: LitLC01: _litmus_P2_4_: isync _litmus_P2_5_: lwz 30,0(9) Test X27 Allowed Histogram (16 states) 22399693:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 13746355:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 11663249:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 944852:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 4814297:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 28097367:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 31005330:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 6495660:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 32345485:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 228146:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 270567:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 2 :>0:r1=1; 2:r1=1; 2:r3=0; x=2; 16201665:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 4367114:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 25815466:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 1604752:>0:r1=1; 2:r1=1; 2:r3=1; x=2; Ok Witnesses Positive: 2, Negative: 199999998 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=ffa63368caa391807dee9905d20510c6 Observation X27 Sometimes 2 199999998 Time X27 90.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 10544782:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 18292707:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 6515706:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 6987994:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 1906001:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 25801815:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 19420850:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 31940843:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 36732506:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 886358:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 497451:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 67 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 11685353:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 9541384:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 11383476:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 7862707:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 67, Negative: 199999933 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=4adca431a2784b4aa9df91b1fc3b1666 Observation X28 Sometimes 67 199999933 Time X28 82.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X29.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X29 "Rfe LwSyncdRW Wse LwSyncdWW Rfe DpCtrlIsyncdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | cmpw r1,r1 ; | li r3,1 | lwsync | beq LC00 ; | stw r3,0(r4) | li r3,1 | LC00: ; | | stw r3,0(r4) | isync ; | | | lwz r3,0(r4) ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: lwsync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: lwz 28,0(11) _litmus_P3_1_: cmpw 28,28 _litmus_P3_2_: beq LitLC00 _litmus_P3_3_: LitLC00: _litmus_P3_4_: isync _litmus_P3_5_: lwz 30,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X29 Allowed Histogram (16 states) 10288512:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 18768426:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 6486840:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 7120577:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 1892778:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 26142016:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 19492598:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 32348456:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 36790930:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 611932:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 497581:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 70 :>1:r1=1; 3:r1=1; 3:r3=0; x=2; 11346816:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 8513637:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 11440857:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 8257974:>1:r1=1; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 70, Negative: 199999930 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=cd58719fd03bc8a841de06004867cb05 Observation X29 Sometimes 70 199999930 Time X29 83.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 (16 states) 22079555:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 13712428:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 11842259:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 934849:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 4532530:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 27960073:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 30981703:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 6531578:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 32185465:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 229919:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 281144:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 1 :>0:r1=1; 2:r1=1; 2:r4=0; x=2; 15827456:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 5003029:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 26224172:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 1673839:>0:r1=1; 2:r1=1; 2:r4=1; x=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is validated Hash=a0f55fa2291a072f015a1f0b83d20074 Observation X30 Sometimes 1 199999999 Time X30 91.40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X31.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X31 "Rfe PodRW Wse LwSyncdWW Rfe DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) | li r1,1 ; li r3,1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; stw r3,0(r4) | lwsync | beq LC00 | lwsync ; | li r3,1 | LC00: | li r3,1 ; | stw r3,0(r4) | isync | stw r3,0(r4) ; | | lwz r3,0(r4) | ; exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 3,0(11) _litmus_P0_1_: li 30,1 _litmus_P0_2_: stw 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: lwz 28,0(11) _litmus_P2_1_: cmpw 28,28 _litmus_P2_2_: beq LitLC00 _litmus_P2_3_: LitLC00: _litmus_P2_4_: isync _litmus_P2_5_: lwz 30,0(9) Test X31 Allowed Histogram (16 states) 22283780:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 13628357:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 11817394:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 936856:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 4529446:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 28019645:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 30809371:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 6492502:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 32627318:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 225938:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 270951:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 1 :>0:r1=1; 2:r1=1; 2:r3=0; x=2; 15726345:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 5010325:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 25970608:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 1651163:>0:r1=1; 2:r1=1; 2:r3=1; x=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=ffb6dc3e13fae7c7e7811955e241147b Observation X31 Sometimes 1 199999999 Time X31 91.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33428298:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 87045 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 7753593:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 21787061:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 41123 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 562 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=0; 4783095:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 9615919:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 10332198:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 6957925:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 1987664:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 28748044:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 3670299:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 8135066:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 20957294:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 41714814:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; Ok Witnesses Positive: 562, Negative: 199999438 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=abdf662fb230128532b66df78e4a75f1 Observation X32 Sometimes 562 199999438 Time X32 78.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33171066:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 88141 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 7869749:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 22194342:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 39862 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 581 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; 4840113:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 9657262:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 10385838:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 7004982:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 1971571:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 28655985:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 3557705:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 8121348:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 20885667:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 41555788:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; Ok Witnesses Positive: 581, Negative: 199999419 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=c86889a7cdc1c89457a71c414046d8c0 Observation X33 Sometimes 581 199999419 Time X33 78.23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 10445194:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 19732103:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 6579452:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 7642948:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 1993333:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 28505153:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 21469566:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 40449883:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 34143284:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 77046 :>1:r1=1; 3:r1=0; 3:r4=0; x=2; 80786 :>1:r1=0; 3:r1=1; 3:r4=0; x=2; 656 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 10099740:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 7275854:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 3872051:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 7632951:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 656, Negative: 199999344 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=8db91522dc421fe43a7baf7aff0de837 Observation X34 Sometimes 656 199999344 Time X34 84.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 10658184:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 19917851:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 6524970:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 7828763:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 2045399:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 28270882:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 21405771:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 41271064:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 33754071:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 65390 :>1:r1=1; 3:r1=0; 3:r3=0; x=2; 78761 :>1:r1=0; 3:r1=1; 3:r3=0; x=2; 556 :>1:r1=1; 3:r1=1; 3:r3=0; x=2; 9642683:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 6745679:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 3920246:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 7869730:>1:r1=1; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 556, Negative: 199999444 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=00744a65cf189719eb1309a79c27a2ca Observation X35 Sometimes 556 199999444 Time X35 83.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31175509:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 437233:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 1319866:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 25506570:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 461612:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 800670:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 13074834:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 1352011:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 708960:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 250312:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 20110759:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 25217526:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 13265941:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 19918096:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 46400101:>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 89.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31084020:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 443381:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 1463549:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 26474854:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 492201:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 781828:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 12706219:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 1335366:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 724320:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 248883:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 20471549:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 25301037:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 13129454:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 19872781:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 45470558:>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 88.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7848845:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 7094960:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 1410336:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 42168166:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 19388535:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 7791545:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 18435313:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 36746171:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 30664859:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 628470:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 1043727:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 14957112:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 32211 :>0:r1=0; 0:r4=0; 2:r1=1; z=2; 269848:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 11519902:>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 97.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y03.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y03 "Rf*e DpAddrdR Fre LwSyncdWW Wse LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 27,0,11 _litmus_P0_2_: xor 10,27,27 _litmus_P0_3_: lwzx 28,10,9 _litmus_P0_4_: stwcx. 27,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y03 Allowed Histogram (7 states) 34912195:>0:r1=0; 0:r4=0; y=1; 19743094:>0:r1=1; 0:r4=0; y=1; 1135974:>0:r1=0; 0:r4=1; y=1; 58372240:>0:r1=1; 0:r4=1; y=1; 17448413:>0:r1=0; 0:r4=0; y=2; 25139933:>0:r1=0; 0:r4=1; y=2; 43248151:>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.79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7355956:>0:r1=0; 0:r4=0; y=1; z=1; 9448139:>0:r1=1; 0:r4=0; y=1; z=1; 805244:>0:r1=0; 0:r4=1; y=1; z=1; 35093497:>0:r1=1; 0:r4=1; y=1; z=1; 15848805:>0:r1=0; 0:r4=0; y=2; z=1; 5361619:>0:r1=1; 0:r4=0; y=2; z=1; 11071843:>0:r1=0; 0:r4=1; y=2; z=1; 30678291:>0:r1=1; 0:r4=1; y=2; z=1; 26360452:>0:r1=0; 0:r4=0; y=1; z=2; 218175:>0:r1=1; 0:r4=0; y=1; z=2; 2982206:>0:r1=0; 0:r4=1; y=1; z=2; 36710651:>0:r1=1; 0:r4=1; y=1; z=2; 1099064:>0:r1=0; 0:r4=0; y=2; z=2; 4740316:>0:r1=0; 0:r4=1; y=2; z=2; 12225742:>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 101.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30343983:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 55524 :>0:r1=1; 0:r4=0; 2:r3=0; y=1; 982418:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 20088905:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 6994843:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 4954044:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 867263:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 38924237:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 36033 :>0:r1=0; 0:r4=0; 2:r3=0; y=2; 321714:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 9405879:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 20040779:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 10219892:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 16921934:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 39842552:>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 99.08 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 6940605:>0:r1=0; 0:r4=0; y=1; z=1; 6147065:>0:r1=1; 0:r4=0; y=1; z=1; 833903:>0:r1=0; 0:r4=1; y=1; z=1; 50067397:>0:r1=1; 0:r4=1; y=1; z=1; 19956440:>0:r1=0; 0:r4=0; y=2; z=1; 8671731:>0:r1=1; 0:r4=0; y=2; z=1; 15287341:>0:r1=0; 0:r4=1; y=2; z=1; 47346916:>0:r1=1; 0:r4=1; y=2; z=1; 28593761:>0:r1=0; 0:r4=0; y=1; z=2; 23086 :>0:r1=1; 0:r4=0; y=1; z=2; 985882:>0:r1=0; 0:r4=1; y=1; z=2; 11092703:>0:r1=1; 0:r4=1; y=1; z=2; 34727 :>0:r1=0; 0:r4=0; y=2; z=2; 212534:>0:r1=0; 0:r4=1; y=2; z=2; 3805909:>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 100.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 16167265:>0:r1=0; 0:r4=0; 1:r3=0; 27520721:>0:r1=0; 0:r4=1; 1:r3=0; 28167088:>0:r1=1; 0:r4=1; 1:r3=0; 37072353:>0:r1=0; 0:r4=0; 1:r3=1; 21676204:>0:r1=1; 0:r4=0; 1:r3=1; 985391:>0:r1=0; 0:r4=1; 1:r3=1; 68410978:>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 75.70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y08.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y08 "Rf*e DpAddrdR Fre SyncdWR Fre LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | lwsync | lwsync ; lwzx r4,r3,r5 | lwz r3,0(r4) | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | | ; exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y08 Allowed Histogram (15 states) 11681590:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 28842 :>0:r1=1; 0:r4=0; 1:r3=0; z=1; 16092095:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 21427615:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 11863907:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 22400748:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 148013:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 31150817:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 1425695:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 4133492:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 2133103:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 28288547:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 2766742:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 4315034:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 42143760:>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 98.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 25380 :>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 80932 :>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 5510510:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 29634007:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 62188 :>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 1312731:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 28489131:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 13313191:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 137297:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 22370643:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 24345292:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 15004194:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 21001529:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 1042329:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 37670646:>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 89.95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13680298:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 158479:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 20663168:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 26659819:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 15451045:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 24412890:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 944045:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 42681030:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 24728 :>0:r1=0; 0:r4=0; 1:r3=0; z=2; 73654 :>0:r1=0; 0:r4=1; 1:r3=0; z=2; 3836592:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 27923444:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 36115 :>0:r1=1; 0:r4=0; 1:r3=1; z=2; 1420122:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 22034571:>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 97.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y11.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y11 "Rf*e DpAddrdR Fre SyncdWW Wse LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 27,0,11 _litmus_P0_2_: xor 10,27,27 _litmus_P0_3_: lwzx 28,10,9 _litmus_P0_4_: stwcx. 27,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y11 Allowed Histogram (7 states) 37044697:>0:r1=0; 0:r4=0; y=1; 21347750:>0:r1=1; 0:r4=0; y=1; 1226555:>0:r1=0; 0:r4=1; y=1; 73188384:>0:r1=1; 0:r4=1; y=1; 15486726:>0:r1=0; 0:r4=0; y=2; 26332420:>0:r1=0; 0:r4=1; y=2; 25373468:>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 78.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11489066:>0:r1=0; 0:r4=0; y=1; z=1; 20660768:>0:r1=1; 0:r4=0; y=1; z=1; 1175118:>0:r1=0; 0:r4=1; y=1; z=1; 44891474:>0:r1=1; 0:r4=1; y=1; z=1; 11679750:>0:r1=0; 0:r4=0; y=2; z=1; 24851 :>0:r1=1; 0:r4=0; y=2; z=1; 11927687:>0:r1=0; 0:r4=1; y=2; z=1; 12126195:>0:r1=1; 0:r4=1; y=2; z=1; 27876047:>0:r1=0; 0:r4=0; y=1; z=2; 3141473:>0:r1=1; 0:r4=0; y=1; z=2; 3308322:>0:r1=0; 0:r4=1; y=1; z=2; 43746069:>0:r1=1; 0:r4=1; y=1; z=2; 1196720:>0:r1=0; 0:r4=0; y=2; z=2; 4384141:>0:r1=0; 0:r4=1; y=2; z=2; 2372319:>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 100.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30276297:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 64960 :>0:r1=1; 0:r4=0; 2:r3=0; y=1; 1318386:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 29456627:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 14306511:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 20048018:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 2909815:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 51546852:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 23556 :>0:r1=0; 0:r4=0; 2:r3=0; y=2; 67272 :>0:r1=0; 0:r4=1; 2:r3=0; y=2; 5406920:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 13308657:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 174369:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 17057459:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 14034301:>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 98.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14048743:>0:r1=0; 0:r4=0; y=1; z=1; 21286641:>0:r1=1; 0:r4=0; y=1; z=1; 1554812:>0:r1=0; 0:r4=1; y=1; z=1; 59776600:>0:r1=1; 0:r4=1; y=1; z=1; 13350283:>0:r1=0; 0:r4=0; y=2; z=1; 62458 :>0:r1=1; 0:r4=0; y=2; z=1; 16927000:>0:r1=0; 0:r4=1; y=2; z=1; 16839498:>0:r1=1; 0:r4=1; y=2; z=1; 28381062:>0:r1=0; 0:r4=0; y=1; z=2; 32473 :>0:r1=1; 0:r4=0; y=1; z=2; 1245473:>0:r1=0; 0:r4=1; y=1; z=2; 22740418:>0:r1=1; 0:r4=1; y=1; z=2; 23523 :>0:r1=0; 0:r4=0; y=2; z=2; 63971 :>0:r1=0; 0:r4=1; y=2; z=2; 3667045:>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 101.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y15.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y15 "Rf*e DpCtrlIsyncdR Fre LwSyncdWW Rf*e DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | DIY02: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; cmpw r1,r1 | lwsync | cmpw r1,r1 | lwsync ; beq LC01 | li r3,1 | beq LC03 | li r3,1 ; LC01: | stw r3,0(r4) | LC03: | stw r3,0(r4) ; isync | | isync | ; lwz r3,0(r4) | | lwz r3,0(r4) | ; stwcx. r1,r0,r2 | | stwcx. r1,r0,r2 | ; bne DIY00 | | bne DIY02 | ; exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: cmpw 30,30 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 31,0(9) _litmus_P0_7_: stwcx. 30,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: LitDIY02: _litmus_P2_1_: lwarx 3,0,11 _litmus_P2_2_: cmpw 3,3 _litmus_P2_3_: beq LitLC03 _litmus_P2_4_: LitLC03: _litmus_P2_5_: isync _litmus_P2_6_: lwz 31,0(9) _litmus_P2_7_: stwcx. 3,0,11 _litmus_P2_8_: bne LitDIY02 Test Y15 Allowed Histogram (15 states) 31312850:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 456215:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 1661762:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 26515101:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 645361:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 1013669:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 12773533:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 1476877:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 725265:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 261375:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 20745028:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 26718825:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 12461902:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 20235801:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 42996436:>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 89.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 35954262:>0:r1=0; 0:r3=0; y=1; 19700646:>0:r1=1; 0:r3=0; y=1; 1137437:>0:r1=0; 0:r3=1; y=1; 57460257:>0:r1=1; 0:r3=1; y=1; 17485433:>0:r1=0; 0:r3=0; y=2; 25217743:>0:r1=0; 0:r3=1; y=2; 43044222:>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 76.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8686275:>0:r1=0; 0:r3=0; y=1; z=1; 10353409:>0:r1=1; 0:r3=0; y=1; z=1; 828890:>0:r1=0; 0:r3=1; y=1; z=1; 36161845:>0:r1=1; 0:r3=1; y=1; z=1; 15710962:>0:r1=0; 0:r3=0; y=2; z=1; 4035017:>0:r1=1; 0:r3=0; y=2; z=1; 13024134:>0:r1=0; 0:r3=1; y=2; z=1; 28426062:>0:r1=1; 0:r3=1; y=2; z=1; 26261315:>0:r1=0; 0:r3=0; y=1; z=2; 215238:>0:r1=1; 0:r3=0; y=1; z=2; 3086279:>0:r1=0; 0:r3=1; y=1; z=2; 36481330:>0:r1=1; 0:r3=1; y=1; z=2; 923403:>0:r1=0; 0:r3=0; y=2; z=2; 2872187:>0:r1=0; 0:r3=1; y=2; z=2; 12933654:>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 100.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) 30566980:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 58262 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 929779:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 20211844:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 8481455:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 5689821:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 912931:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 40296837:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 34575 :>0:r1=0; 0:r3=0; 2:r3=0; y=2; 261130:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 9544641:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 19094220:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 9316678:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 16970933:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 37629914:>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 98.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8770708:>0:r1=0; 0:r3=0; y=1; z=1; 8745348:>0:r1=1; 0:r3=0; y=1; z=1; 895149:>0:r1=0; 0:r3=1; y=1; z=1; 50629303:>0:r1=1; 0:r3=1; y=1; z=1; 18636404:>0:r1=0; 0:r3=0; y=2; z=1; 6999103:>0:r1=1; 0:r3=0; y=2; z=1; 15526307:>0:r1=0; 0:r3=1; y=2; z=1; 43961422:>0:r1=1; 0:r3=1; y=2; z=1; 29103665:>0:r1=0; 0:r3=0; y=1; z=2; 23384 :>0:r1=1; 0:r3=0; y=1; z=2; 985904:>0:r1=0; 0:r3=1; y=1; z=2; 11322050:>0:r1=1; 0:r3=1; y=1; z=2; 33564 :>0:r1=0; 0:r3=0; y=2; z=2; 221169:>0:r1=0; 0:r3=1; y=2; z=2; 4146520:>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 100.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y20.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y20 "Rf*e DpCtrlIsyncdR Fre SyncdWR Fre LwSyncdWW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | sync | lwsync ; beq LC01 | lwz r3,0(r4) | li r3,1 ; LC01: | | stw r3,0(r4) ; isync | | ; lwz r3,0(r4) | | ; stwcx. r1,r0,r2 | | ; bne DIY00 | | ; exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 31,1 _litmus_P1_1_: stw 31,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 30,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: cmpw 30,30 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 31,0(9) _litmus_P0_7_: stwcx. 30,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y20 Allowed Histogram (7 states) 16208621:>0:r1=0; 0:r3=0; 1:r3=0; 27849191:>0:r1=0; 0:r3=1; 1:r3=0; 28121041:>0:r1=1; 0:r3=1; 1:r3=0; 38658696:>0:r1=0; 0:r3=0; 1:r3=1; 20378239:>0:r1=1; 0:r3=0; 1:r3=1; 1087592:>0:r1=0; 0:r3=1; 1:r3=1; 67696620:>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.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11688899:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 28634 :>0:r1=1; 0:r3=0; 1:r3=0; z=1; 16362598:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 21169158:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 12581117:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 21969497:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 143509:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 30918648:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 1419072:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 3989744:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 2170165:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 28058505:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 2762491:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 4334425:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 42403538:>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 98.85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 25652 :>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 83490 :>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 5474779:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 29597879:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 60900 :>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 1001214:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 28370329:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 13697801:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 151486:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 22484830:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 24256737:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 15787163:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 21376304:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 1100424:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 36531012:>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 90.43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13722360:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 167243:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 20737845:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 26310905:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 15946101:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 24327168:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 965337:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 42050476:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 24924 :>0:r1=0; 0:r3=0; 1:r3=0; z=2; 78516 :>0:r1=0; 0:r3=1; 1:r3=0; z=2; 3879888:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 28346291:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 39315 :>0:r1=1; 0:r3=0; 1:r3=1; z=2; 1418610:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 21985021:>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 98.12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 38111867:>0:r1=0; 0:r3=0; y=1; 21075017:>0:r1=1; 0:r3=0; y=1; 1415603:>0:r1=0; 0:r3=1; y=1; 72348600:>0:r1=1; 0:r3=1; y=1; 15608968:>0:r1=0; 0:r3=0; y=2; 26086891:>0:r1=0; 0:r3=1; y=2; 25353054:>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.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 12240249:>0:r1=0; 0:r3=0; y=1; z=1; 20867403:>0:r1=1; 0:r3=0; y=1; z=1; 1382457:>0:r1=0; 0:r3=1; y=1; z=1; 45241144:>0:r1=1; 0:r3=1; y=1; z=1; 11807544:>0:r1=0; 0:r3=0; y=2; z=1; 25227 :>0:r1=1; 0:r3=0; y=2; z=1; 13555747:>0:r1=0; 0:r3=1; y=2; z=1; 11069793:>0:r1=1; 0:r3=1; y=2; z=1; 27729066:>0:r1=0; 0:r3=0; y=1; z=2; 3265913:>0:r1=1; 0:r3=0; y=1; z=2; 3435334:>0:r1=0; 0:r3=1; y=1; z=2; 43710399:>0:r1=1; 0:r3=1; y=1; z=2; 972199:>0:r1=0; 0:r3=0; y=2; z=2; 2546668:>0:r1=0; 0:r3=1; y=2; z=2; 2150857:>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 101.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30198349:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 70649 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 1136161:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 29763781:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 15069630:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 20840102:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 3222617:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 50979847:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 23528 :>0:r1=0; 0:r3=0; 2:r3=0; y=2; 68297 :>0:r1=0; 0:r3=1; 2:r3=0; y=2; 5242126:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 13434678:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 175288:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 16929329:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 12845618:>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 98.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7483285:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 21429321:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 5616451:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 7872744:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 1458172:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 18682095:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 41315613:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 36986573:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 31058245:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 36685 :>0:r1=1; 2:r1=0; 2:r3=0; x=2; 643509:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 845205:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 221482:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 14810272:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 11540348:>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 96.89 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7344180:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 12657236:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 6487894:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 6628944:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 170965:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 15919792:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 25427344:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 47816297:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 31941692:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 788919:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 240539:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 1001553:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 1457112:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 25580366:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 16537167:>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.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7703218:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 13262750:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 6153561:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 6660873:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 168397:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 15959578:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 25396253:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 47395725:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 31893130:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 815545:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 251704:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 990098:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 1389167:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 25562134:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 16397867:>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 86.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 6745754:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 20880238:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 6382597:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 8396690:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 1365060:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 18672457:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 41023485:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 37315679:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 30344832:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 35876 :>0:r1=1; 2:r1=0; 2:r4=0; x=2; 594681:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 965209:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 259203:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 15293879:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 11724360:>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 95.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7259348:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 21366448:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 6075341:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 8255808:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 1404944:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 19003422:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 40736380:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 36641407:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 30818577:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 36429 :>0:r1=1; 2:r1=0; 2:r3=0; x=2; 604287:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 853781:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 256966:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 15001183:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 11685679:>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 96.77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33078461:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 63187 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 6473055:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 13266465:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 24312 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 3983484:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 7174503:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 281779:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 755849:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 234224:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 18619183:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 13358131:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 15478390:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 27593971:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 59615006:>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 80.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32882487:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 65163 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 6932444:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 14051603:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 24079 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 3692873:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 7219491:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 265620:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 751285:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 235570:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 18296508:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 13333087:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 15475929:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 27547080:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 59226781:>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 81.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7462180:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 12539817:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 6456018:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 7138942:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 211761:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 18762476:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 28890869:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 56697545:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 32721102:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 38587 :>1:r1=1; 3:r1=0; 3:r4=0; x=2; 22083 :>1:r1=0; 3:r1=1; 3:r4=0; x=2; 356201:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 741854:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 13387352:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 14573213:>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.71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7815666:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 13087723:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 6165898:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 7157492:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 201761:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 18659166:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 28910547:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 56469166:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 32690550:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 37679 :>1:r1=1; 3:r1=0; 3:r3=0; x=2; 23758 :>1:r1=0; 3:r1=1; 3:r3=0; x=2; 330274:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 746891:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 13199321:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 14504108:>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 87.40 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=-s 1000 -r 100k -i 1 Sat Jan 22 21:48:24 CST 2011