sam jan 22 16:10:26 CET 2011 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X00.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X00 "Rfe DpAddrdR Fre LwSyncdWW Rfe DpAddrdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r5 | lwsync ; | li r3,1 | | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: lwz 30,0(11) _litmus_P2_1_: xor 10,30,30 _litmus_P2_2_: lwzx 31,10,9 Test X00 Allowed Histogram (15 states) 22511794:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 257415:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 91848989:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 51559856:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 219429:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 2779151:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 329605:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 91813084:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 2594622:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 126207190:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 188234644:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 35220350:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 328159:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 88607967:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 97487745:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=6559e19d9e37619f3f8bf433a5805105 Observation X00 Never 0 800000000 Time X00 32.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X01.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X01 "Rfe DpAddrdR Fre LwSyncdWW Rfe DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | beq LC00 | lwsync ; | li r3,1 | LC00: | li r3,1 ; | stw r3,0(r4) | isync | stw r3,0(r4) ; | | lwz r3,0(r4) | ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: cmpw 3,3 _litmus_P2_2_: beq LitLC00 _litmus_P2_3_: LitLC00: _litmus_P2_4_: isync _litmus_P2_5_: lwz 31,0(9) Test X01 Allowed Histogram (15 states) 10544755:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 66011 :>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 68206946:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 25504457:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 93949 :>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 1462427:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 167520:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 95174600:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 2679132:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 134172086:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 188622153:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 41252189:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 629267:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 94765643:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 136658865:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=2dd158f1ef0b66595a56ff21c6e00a13 Observation X01 Never 0 800000000 Time X01 33.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 64771574:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 3756197:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 165505112:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 185122988:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 20698167:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 472293:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 81584113:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 91475021:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 30662247:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 339746:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 92808682:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 59896863:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 328214:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 2373980:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 204803:>0:r1=1; 0:r4=1; 2:r1=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is NOT validated Hash=ddaab862216f1c9eafeceba074a24928 Observation X02 Never 0 800000000 Time X02 37.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X03.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X03 "Rfe DpAddrdR Fre LwSyncdWW Wse LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; lwz r1,0(r2) | li r1,1 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | lwsync ; | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 27,0(11) _litmus_P0_1_: xor 10,27,27 _litmus_P0_2_: lwzx 28,10,9 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X03 Allowed Histogram (8 states) 232482031:>0:r1=0; 0:r4=0; y=1; 32193496:>0:r1=1; 0:r4=0; y=1; 197583269:>0:r1=0; 0:r4=1; y=1; 333939628:>0:r1=1; 0:r4=1; y=1; 25714754:>0:r1=0; 0:r4=0; y=2; 10179 :>0:r1=1; 0:r4=0; y=2; 153963098:>0:r1=0; 0:r4=1; y=2; 24113545:>0:r1=1; 0:r4=1; y=2; Ok Witnesses Positive: 10179, Negative: 999989821 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=979eb45568765c8b5bb24cb8beb2a694 Observation X03 Sometimes 10179 999989821 Time X03 79.55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 85845033:>0:r1=0; 0:r4=0; y=1; z=1; 1219437:>0:r1=1; 0:r4=0; y=1; z=1; 236163835:>0:r1=0; 0:r4=1; y=1; z=1; 389510464:>0:r1=1; 0:r4=1; y=1; z=1; 2931470:>0:r1=0; 0:r4=0; y=2; z=1; 145175:>0:r1=1; 0:r4=0; y=2; z=1; 13185795:>0:r1=0; 0:r4=1; y=2; z=1; 24905994:>0:r1=1; 0:r4=1; y=2; z=1; 3214390:>0:r1=0; 0:r4=0; y=1; z=2; 86968 :>0:r1=1; 0:r4=0; y=1; z=2; 17897635:>0:r1=0; 0:r4=1; y=1; z=2; 21937816:>0:r1=1; 0:r4=1; y=1; z=2; 144102:>0:r1=0; 0:r4=0; y=2; z=2; 2145410:>0:r1=0; 0:r4=1; y=2; z=2; 666476:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=bbe86be3ef3c2131f0d4681c0ccd31a8 Observation X04 Never 0 800000000 Time X04 50.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X05.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X05 "Rfe DpAddrdR Fre LwSyncdWW Wse SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | sync | lwsync ; | li r3,1 | lwz r3,0(r4) | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X05 Allowed Histogram (15 states) 1250733:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 97457 :>0:r1=1; 0:r4=0; 2:r3=0; y=1; 4799171:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 1582205:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 66981049:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 1161138:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 160527639:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 112665181:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 26157 :>0:r1=0; 0:r4=0; 2:r3=0; y=2; 1336525:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 148881:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 37420479:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 464706:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 140776922:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 270761757:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=2f45a04baa1582caaf7bebb0f6429fad Observation X05 Never 0 800000000 Time X05 39.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 70193455:>0:r1=0; 0:r4=0; y=1; z=1; 1172502:>0:r1=1; 0:r4=0; y=1; z=1; 278571415:>0:r1=0; 0:r4=1; y=1; z=1; 79016970:>0:r1=1; 0:r4=1; y=1; z=1; 30049747:>0:r1=0; 0:r4=0; y=2; z=1; 250287:>0:r1=1; 0:r4=0; y=2; z=1; 132288340:>0:r1=0; 0:r4=1; y=2; z=1; 199539704:>0:r1=1; 0:r4=1; y=2; z=1; 1012145:>0:r1=0; 0:r4=0; y=1; z=2; 28105 :>0:r1=1; 0:r4=0; y=1; z=2; 4738342:>0:r1=0; 0:r4=1; y=1; z=2; 1686377:>0:r1=1; 0:r4=1; y=1; z=2; 10870 :>0:r1=0; 0:r4=0; y=2; z=2; 1221123:>0:r1=0; 0:r4=1; y=2; z=2; 220618:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=2f7e7e797a32b772dba41a2c989f624e Observation X06 Never 0 800000000 Time X06 52.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32511889:>0:r1=0; 0:r4=0; 1:r3=0; 9326 :>0:r1=1; 0:r4=0; 1:r3=0; 125719987:>0:r1=0; 0:r4=1; 1:r3=0; 6976504:>0:r1=1; 0:r4=1; 1:r3=0; 355240205:>0:r1=0; 0:r4=0; 1:r3=1; 53370086:>0:r1=1; 0:r4=0; 1:r3=1; 248512396:>0:r1=0; 0:r4=1; 1:r3=1; 177659607:>0:r1=1; 0:r4=1; 1:r3=1; Ok Witnesses Positive: 9326, Negative: 999990674 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is validated Hash=27f80466ebe5b987c02fd5b2375e9014 Observation X07 Sometimes 9326 999990674 Time X07 73.87 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1760423:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 21192 :>0:r1=1; 0:r4=0; 1:r3=0; z=1; 4644163:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 469273:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 262316980:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 41524975:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 248460347:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 185777658:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 83088 :>0:r1=0; 0:r4=0; 1:r3=0; z=2; 1591681:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 177714:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 20826578:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 1359130:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 16884199:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 14102599:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=c693aeac120b5ebe47aca8096f1cefc4 Observation X08 Never 0 800000000 Time X08 38.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 44348 :>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 712185:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 36374 :>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 5101188:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 44957 :>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 21007775:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 3052493:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 13433462:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 557533:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 31193847:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 8239712:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 202588282:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 10361637:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 399153242:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 104472965:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=25130932b014cac34245d116a5f68876 Observation X09 Never 0 800000000 Time X09 33.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 6376977:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 228241:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 11903286:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 3184211:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 259165642:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 22043614:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 369140933:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 115668794:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 30005 :>0:r1=0; 0:r4=0; 1:r3=0; z=2; 1113752:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 50047 :>0:r1=1; 0:r4=1; 1:r3=0; z=2; 3352426:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 60937 :>0:r1=1; 0:r4=0; 1:r3=1; z=2; 6549550:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 1131585:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=6da0ade67698eb3fe55496c10e533d9d Observation X10 Never 0 800000000 Time X10 38.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 317387409:>0:r1=0; 0:r4=0; y=1; 48568660:>0:r1=1; 0:r4=0; y=1; 272106012:>0:r1=0; 0:r4=1; y=1; 220197970:>0:r1=1; 0:r4=1; y=1; 21913293:>0:r1=0; 0:r4=0; y=2; 5006 :>0:r1=1; 0:r4=0; y=2; 112911683:>0:r1=0; 0:r4=1; y=2; 6909967:>0:r1=1; 0:r4=1; y=2; Ok Witnesses Positive: 5006, Negative: 999994994 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=2e151daaab42138b8c478ba081d896ed Observation X11 Sometimes 5006 999994994 Time X11 80.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 198501525:>0:r1=0; 0:r4=0; y=1; z=1; 31186283:>0:r1=1; 0:r4=0; y=1; z=1; 290690628:>0:r1=0; 0:r4=1; y=1; z=1; 227197880:>0:r1=1; 0:r4=1; y=1; z=1; 559979:>0:r1=0; 0:r4=0; y=2; z=1; 8381 :>0:r1=1; 0:r4=0; y=2; z=1; 2468825:>0:r1=0; 0:r4=1; y=2; z=1; 511414:>0:r1=1; 0:r4=1; y=2; z=1; 11741754:>0:r1=0; 0:r4=0; y=1; z=2; 825112:>0:r1=1; 0:r4=0; y=1; z=2; 20647052:>0:r1=0; 0:r4=1; y=1; z=2; 14872481:>0:r1=1; 0:r4=1; y=1; z=2; 25989 :>0:r1=0; 0:r4=0; y=2; z=2; 644036:>0:r1=0; 0:r4=1; y=2; z=2; 118661:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=449f3e0ad9111a8f4431787ea3e14c01 Observation X12 Never 0 800000000 Time X12 52.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1315953:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 97476 :>0:r1=1; 0:r4=0; 2:r3=0; y=1; 6957819:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 1391550:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 146061941:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 7434276:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 341561861:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 203539533:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 8683 :>0:r1=0; 0:r4=0; 2:r3=0; y=2; 1269616:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 95838 :>0:r1=1; 0:r4=1; 2:r3=0; y=2; 9964004:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 161021:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 53302792:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 26837637:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=e039602c16d523ecfdb1a0b4937a34a6 Observation X13 Never 0 800000000 Time X13 38.97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 141024206:>0:r1=0; 0:r4=0; y=1; z=1; 9961809:>0:r1=1; 0:r4=0; y=1; z=1; 438507052:>0:r1=0; 0:r4=1; y=1; z=1; 157787349:>0:r1=1; 0:r4=1; y=1; z=1; 3328594:>0:r1=0; 0:r4=0; y=2; z=1; 35921 :>0:r1=1; 0:r4=0; y=2; z=1; 28894131:>0:r1=0; 0:r4=1; y=2; z=1; 10851644:>0:r1=1; 0:r4=1; y=2; z=1; 1042355:>0:r1=0; 0:r4=0; y=1; z=2; 39957 :>0:r1=1; 0:r4=0; y=1; z=2; 6294517:>0:r1=0; 0:r4=1; y=1; z=2; 1758145:>0:r1=1; 0:r4=1; y=1; z=2; 2539 :>0:r1=0; 0:r4=0; y=2; z=2; 416041:>0:r1=0; 0:r4=1; y=2; z=2; 55740 :>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=74664d9800a1cc765c71acb315cf55f7 Observation X14 Never 0 800000000 Time X14 53.73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X15.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X15 "Rfe DpCtrlIsyncdR Fre LwSyncdWW Rfe DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; beq LC00 | lwsync | beq LC01 | lwsync ; LC00: | li r3,1 | LC01: | li r3,1 ; isync | stw r3,0(r4) | isync | stw r3,0(r4) ; lwz r3,0(r4) | | lwz r3,0(r4) | ; exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: cmpw 30,30 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 31,0(9) _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: cmpw 3,3 _litmus_P2_2_: beq LitLC01 _litmus_P2_3_: LitLC01: _litmus_P2_4_: isync _litmus_P2_5_: lwz 31,0(9) Test X15 Allowed Histogram (15 states) 5305865:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 37911 :>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 58029596:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 15566127:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 35899 :>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 1286536:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 194437:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 70501729:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 1609045:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 268537027:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 125596747:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 26160116:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 334259:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 117487867:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 109316839:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=a488ac47b1a88d9c3f30dcee477424e5 Observation X15 Never 0 800000000 Time X15 33.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 161514551:>0:r1=0; 0:r3=0; y=1; 19652918:>0:r1=1; 0:r3=0; y=1; 324124531:>0:r1=0; 0:r3=1; y=1; 286620271:>0:r1=1; 0:r3=1; y=1; 11456136:>0:r1=0; 0:r3=0; y=2; 10598 :>0:r1=1; 0:r3=0; y=2; 171348144:>0:r1=0; 0:r3=1; y=2; 25272851:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 10598, Negative: 999989402 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=7cfc2b26a1cbcdd15d0fab061a637ce4 Observation X16 Sometimes 10598 999989402 Time X16 79.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 12133648:>0:r1=0; 0:r3=0; y=1; z=1; 905165:>0:r1=1; 0:r3=0; y=1; z=1; 288321784:>0:r1=0; 0:r3=1; y=1; z=1; 407925025:>0:r1=1; 0:r3=1; y=1; z=1; 1364340:>0:r1=0; 0:r3=0; y=2; z=1; 81030 :>0:r1=1; 0:r3=0; y=2; z=1; 15343910:>0:r1=0; 0:r3=1; y=2; z=1; 29948535:>0:r1=1; 0:r3=1; y=2; z=1; 1677596:>0:r1=0; 0:r3=0; y=1; z=2; 37331 :>0:r1=1; 0:r3=0; y=1; z=2; 17478881:>0:r1=0; 0:r3=1; y=1; z=2; 21369431:>0:r1=1; 0:r3=1; y=1; z=2; 71907 :>0:r1=0; 0:r3=0; y=2; z=2; 2435645:>0:r1=0; 0:r3=1; y=2; z=2; 905772:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=8ece2ae907eaa93a2cebf24dcb08cf79 Observation X17 Never 0 800000000 Time X17 52.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X18.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X18 "Rfe DpCtrlIsyncdR Fre LwSyncdWW Wse SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | lwsync | sync | lwsync ; LC00: | li r3,1 | lwz r3,0(r4) | li r3,1 ; isync | stw r3,0(r4) | | stw r3,0(r4) ; lwz r3,0(r4) | | | ; exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X18 Allowed Histogram (15 states) 268257:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 5822 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 4538275:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 1505871:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 14386659:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 467806:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 323515695:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 49200571:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 10806 :>0:r1=0; 0:r3=0; 2:r3=0; y=2; 1295823:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 311630:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 7799617:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 257112:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 173341570:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 223094486:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=773f6798f908e0cd810f3e878df07bab Observation X18 Never 0 800000000 Time X18 39.45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11215685:>0:r1=0; 0:r3=0; y=1; z=1; 588224:>0:r1=1; 0:r3=0; y=1; z=1; 343047386:>0:r1=0; 0:r3=1; y=1; z=1; 62609094:>0:r1=1; 0:r3=1; y=1; z=1; 4549861:>0:r1=0; 0:r3=0; y=2; z=1; 156353:>0:r1=1; 0:r3=0; y=2; z=1; 142734943:>0:r1=0; 0:r3=1; y=2; z=1; 227558183:>0:r1=1; 0:r3=1; y=2; z=1; 166927:>0:r1=0; 0:r3=0; y=1; z=2; 5167 :>0:r1=1; 0:r3=0; y=1; z=2; 4181978:>0:r1=0; 0:r3=1; y=1; z=2; 1804868:>0:r1=1; 0:r3=1; y=1; z=2; 3739 :>0:r1=0; 0:r3=0; y=2; z=2; 911764:>0:r1=0; 0:r3=1; y=2; z=2; 465828:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=811f0a85dc5f811c7436b53d2ca9c449 Observation X19 Never 0 800000000 Time X19 52.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X20.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X20 "Rfe DpCtrlIsyncdR Fre SyncdWR Fre LwSyncdWW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; lwz r1,0(r2) | li r1,1 | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | sync | lwsync ; LC00: | lwz r3,0(r4) | li r3,1 ; isync | | stw r3,0(r4) ; lwz r3,0(r4) | | ; exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 31,1 _litmus_P1_1_: stw 31,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 30,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: cmpw 30,30 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 31,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X20 Allowed Histogram (8 states) 24658121:>0:r1=0; 0:r3=0; 1:r3=0; 15796 :>0:r1=1; 0:r3=0; 1:r3=0; 137145768:>0:r1=0; 0:r3=1; 1:r3=0; 7995820:>0:r1=1; 0:r3=1; 1:r3=0; 280287194:>0:r1=0; 0:r3=0; 1:r3=1; 36749836:>0:r1=1; 0:r3=0; 1:r3=1; 310122693:>0:r1=0; 0:r3=1; 1:r3=1; 203024772:>0:r1=1; 0:r3=1; 1:r3=1; Ok Witnesses Positive: 15796, Negative: 999984204 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is validated Hash=0c99e9e00ef12798cd94e468d7533fcb Observation X20 Sometimes 15796 999984204 Time X20 72.55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1440580:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 14398 :>0:r1=1; 0:r3=0; 1:r3=0; z=1; 6930883:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 1295952:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 184388752:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 24863781:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 304343983:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 203668808:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 74533 :>0:r1=0; 0:r3=0; 1:r3=0; z=2; 1988887:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 299823:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 22170397:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 1311814:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 24821919:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 22385490:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=10b56f844965b778138fc256080a6cb2 Observation X21 Never 0 800000000 Time X21 38.70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 25884 :>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 766222:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 60411 :>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 3284306:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 21795 :>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 21375258:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 4373606:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 6172616:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 265916:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 30799550:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 9278207:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 145577536:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 6622498:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 415726828:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 155649367:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=e7fc832a2e4b347328216cfab07885d9 Observation X22 Never 0 800000000 Time X22 35.16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 5177616:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 166448:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 14539471:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 3889798:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 142386091:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 10347498:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 483961281:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 126785429:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 10153 :>0:r1=0; 0:r3=0; 1:r3=0; z=2; 1082540:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 160749:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 1966393:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 43220 :>0:r1=1; 0:r3=0; 1:r3=1; z=2; 7365105:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 2118208:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=86fcf34749ab0aa370ea66e6893791a0 Observation X23 Never 0 800000000 Time X23 38.71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 263261744:>0:r1=0; 0:r3=0; y=1; 32318362:>0:r1=1; 0:r3=0; y=1; 376670154:>0:r1=0; 0:r3=1; y=1; 186427431:>0:r1=1; 0:r3=1; y=1; 13400659:>0:r1=0; 0:r3=0; y=2; 10662 :>0:r1=1; 0:r3=0; y=2; 120624275:>0:r1=0; 0:r3=1; y=2; 7286713:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 10662, Negative: 999989338 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=1a78bce42911eadebdb22805402de8eb Observation X24 Sometimes 10662 999989338 Time X24 81.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 116859320:>0:r1=0; 0:r3=0; y=1; z=1; 12788458:>0:r1=1; 0:r3=0; y=1; z=1; 396792774:>0:r1=0; 0:r3=1; y=1; z=1; 226459344:>0:r1=1; 0:r3=1; y=1; z=1; 370601:>0:r1=0; 0:r3=0; y=2; z=1; 4129 :>0:r1=1; 0:r3=0; y=2; z=1; 3157137:>0:r1=0; 0:r3=1; y=2; z=1; 640816:>0:r1=1; 0:r3=1; y=2; z=1; 6654201:>0:r1=0; 0:r3=0; y=1; z=2; 354316:>0:r1=1; 0:r3=0; y=1; z=2; 19961003:>0:r1=0; 0:r3=1; y=1; z=2; 15128729:>0:r1=1; 0:r3=1; y=1; z=2; 17571 :>0:r1=0; 0:r3=0; y=2; z=2; 639785:>0:r1=0; 0:r3=1; y=2; z=2; 171816:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=629e26a0c6f613b14043edf57727b702 Observation X25 Never 0 800000000 Time X25 52.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1010477:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 11873 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 8597846:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 1803826:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 44700311:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 2645727:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 572568804:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 109038179:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 8467 :>0:r1=0; 0:r3=0; 2:r3=0; y=2; 938920:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 169093:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 2591044:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 81824 :>0:r1=1; 0:r3=0; 2:r3=1; y=2; 46422479:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 9411130:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=54da285ce144acabc337e28ea8958874 Observation X26 Never 0 800000000 Time X26 39.71 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X27.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X27 "Rfe DpCtrldW Wse LwSyncdWW Rfe DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; beq LC00 | lwsync | beq LC01 | lwsync ; LC00: | li r3,1 | LC01: | li r3,1 ; li r3,1 | stw r3,0(r4) | isync | stw r3,0(r4) ; stw r3,0(r4) | | lwz r3,0(r4) | ; exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 3,0(11) _litmus_P0_1_: cmpw 3,3 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: li 30,1 _litmus_P0_5_: stw 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: lwz 28,0(11) _litmus_P2_1_: cmpw 28,28 _litmus_P2_2_: beq LitLC01 _litmus_P2_3_: LitLC01: _litmus_P2_4_: isync _litmus_P2_5_: lwz 30,0(9) Test X27 Allowed Histogram (15 states) 27018127:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 5143981:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 1424796:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 187523:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 204831840:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 60621881:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 219244551:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 122489832:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 12159675:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 109221:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 118915:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 77551729:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 3521454:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 64776663:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 799812:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ffa63368caa391807dee9905d20510c6 Observation X27 Never 0 800000000 Time X27 38.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 147999478:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 27831187:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 245731:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 64039 :>1:r1=1; 3:r1=1; 3:r4=0; x=1; 129815832:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 215037337:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 85396566:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 181580068:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 1968439:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 139187:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 1694 :>1:r1=0; 3:r1=1; 3:r4=0; x=2; 4807590:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 2996161:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 1413618:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 703073:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=4adca431a2784b4aa9df91b1fc3b1666 Observation X28 Never 0 800000000 Time X28 32.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X29.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X29 "Rfe LwSyncdRW Wse LwSyncdWW Rfe DpCtrlIsyncdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | cmpw r1,r1 ; | li r3,1 | lwsync | beq LC00 ; | stw r3,0(r4) | li r3,1 | LC00: ; | | stw r3,0(r4) | isync ; | | | lwz r3,0(r4) ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: lwsync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: lwz 28,0(11) _litmus_P3_1_: cmpw 28,28 _litmus_P3_2_: beq LitLC00 _litmus_P3_3_: LitLC00: _litmus_P3_4_: isync _litmus_P3_5_: lwz 30,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X29 Allowed Histogram (15 states) 34908597:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 6262089:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 119330:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 30331 :>1:r1=1; 3:r1=1; 3:r3=0; x=1; 236914407:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 262236264:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 89383497:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 156142077:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 647676:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 24959 :>1:r1=1; 3:r1=0; 3:r3=0; x=2; 1315 :>1:r1=0; 3:r1=1; 3:r3=0; x=2; 7422923:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 2587299:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 2280814:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 1038422:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=cd58719fd03bc8a841de06004867cb05 Observation X29 Never 0 800000000 Time X29 31.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X30.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X30 "Rfe PodRW Wse LwSyncdWW Rfe DpAddrdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) | li r1,1 ; li r3,1 | stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) ; stw r3,0(r4) | lwsync | lwzx r4,r3,r5 | lwsync ; | li r3,1 | | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) Generated assembler _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 3,0(11) _litmus_P0_1_: li 30,1 _litmus_P0_2_: stw 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: lwz 28,0(11) _litmus_P2_1_: xor 10,28,28 _litmus_P2_2_: lwzx 30,10,9 Test X30 Allowed Histogram (15 states) 79467791:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 14262722:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 1487765:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 218744:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 114982433:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 52125756:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 249211058:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 119900764:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 24720906:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 190075:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 165818:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 64165555:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 1286968:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 77608936:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 204709:>0:r1=1; 2:r1=1; 2:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=a0f55fa2291a072f015a1f0b83d20074 Observation X30 Never 0 800000000 Time X30 37.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X31.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X31 "Rfe PodRW Wse LwSyncdWW Rfe DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) | li r1,1 ; li r3,1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; stw r3,0(r4) | lwsync | beq LC00 | lwsync ; | li r3,1 | LC00: | li r3,1 ; | stw r3,0(r4) | isync | stw r3,0(r4) ; | | lwz r3,0(r4) | ; exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 3,0(11) _litmus_P0_1_: li 30,1 _litmus_P0_2_: stw 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: lwz 28,0(11) _litmus_P2_1_: cmpw 28,28 _litmus_P2_2_: beq LitLC00 _litmus_P2_3_: LitLC00: _litmus_P2_4_: isync _litmus_P2_5_: lwz 30,0(9) Test X31 Allowed Histogram (15 states) 19798252:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 5090340:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 1467387:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 237772:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 216661456:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 65399073:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 199952370:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 128496288:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 7795795:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 100403:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 91591 :>0:r1=0; 2:r1=1; 2:r3=0; x=2; 90674799:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 2310986:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 61497229:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 426259:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ffb6dc3e13fae7c7e7811955e241147b Observation X31 Never 0 800000000 Time X31 38.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 515122:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 33341 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 101568099:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 63607539:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 2107 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 263218:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 180203:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 3895688:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 1922627:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 122693106:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 211905815:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 487959:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 168582:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 54773246:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 237983348:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=abdf662fb230128532b66df78e4a75f1 Observation X32 Never 0 800000000 Time X32 28.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 2426443:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 45603 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 37468446:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 13346308:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 5900 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 1459165:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 144755:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 7220110:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 1353775:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 226506225:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 312895997:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 1100124:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 232226:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 40061157:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 155733766:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=c86889a7cdc1c89457a71c414046d8c0 Observation X33 Never 0 800000000 Time X33 29.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 102307908:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 69617267:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 147866:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 90238 :>1:r1=1; 3:r1=1; 3:r4=0; x=1; 114508612:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 272489924:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 56676813:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 179429237:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 162328:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 9380 :>1:r1=1; 3:r1=0; 3:r4=0; x=2; 671 :>1:r1=0; 3:r1=1; 3:r4=0; x=2; 1908097:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 2174646:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 251902:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 225111:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=8db91522dc421fe43a7baf7aff0de837 Observation X34 Never 0 800000000 Time X34 32.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (15 states) 21758326:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 14355715:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 74676 :>1:r1=0; 3:r1=1; 3:r3=0; x=1; 37964 :>1:r1=1; 3:r1=1; 3:r3=0; x=1; 201295759:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 323126927:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 58389533:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 175988910:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 97492 :>1:r1=0; 3:r1=0; 3:r3=0; x=2; 2466 :>1:r1=1; 3:r1=0; 3:r3=0; x=2; 641 :>1:r1=0; 3:r1=1; 3:r3=0; x=2; 2019400:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 1963486:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 451011:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 437694:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=00744a65cf189719eb1309a79c27a2ca Observation X35 Never 0 800000000 Time X35 31.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 4606617:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 101378:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 7665613:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 67684021:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 95381 :>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 858876:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 703983:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 7643160:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 922162:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 1172095:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 56054968:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 59513953:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 755220:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 49340436:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 542882137:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=08b576a9816ca91b136efc84cb8198fe Observation Y00 Never 0 800000000 Time Y00 38.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1645252:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 41098 :>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 1791216:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 14713964:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 52492 :>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 522411:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 549518:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 2251820:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 519312:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 141174:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 26466823:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 55917776:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 1446806:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 30644741:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 663295597:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=27be645f8ce747a8241695ecd5d12775 Observation Y01 Never 0 800000000 Time Y01 37.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33751492:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 1435506:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 3745253:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 312259320:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 31914996:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 776857:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 12304513:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 372589063:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 2047104:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 50446 :>0:r1=1; 0:r4=0; 2:r1=0; z=2; 3202785:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 24633861:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 17566 :>0:r1=0; 0:r4=0; 2:r1=1; z=2; 452636:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 818602:>0:r1=1; 0:r4=1; 2:r1=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is NOT validated Hash=e299ccd513ee6b40ffc1479736b6d80f Observation Y02 Never 0 800000000 Time Y02 41.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 166212307:>0:r1=0; 0:r4=0; y=1; 41692715:>0:r1=1; 0:r4=0; y=1; 16683108:>0:r1=0; 0:r4=1; y=1; 552872854:>0:r1=1; 0:r4=1; y=1; 27964205:>0:r1=0; 0:r4=0; y=2; 76148937:>0:r1=0; 0:r4=1; y=2; 118425874:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=fbc1c062cf6f3291c2ce205045bcf85e Observation Y03 Never 0 1000000000 Time Y03 82.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 53953626:>0:r1=0; 0:r4=0; y=1; z=1; 1067312:>0:r1=1; 0:r4=0; y=1; z=1; 1636619:>0:r1=0; 0:r4=1; y=1; z=1; 653125102:>0:r1=1; 0:r4=1; y=1; z=1; 2908497:>0:r1=0; 0:r4=0; y=2; z=1; 72204 :>0:r1=1; 0:r4=0; y=2; z=1; 2047984:>0:r1=0; 0:r4=1; y=2; z=1; 44530397:>0:r1=1; 0:r4=1; y=2; z=1; 1525045:>0:r1=0; 0:r4=0; y=1; z=2; 55185 :>0:r1=1; 0:r4=0; y=1; z=2; 1435726:>0:r1=0; 0:r4=1; y=1; z=2; 35560191:>0:r1=1; 0:r4=1; y=1; z=2; 44731 :>0:r1=0; 0:r4=0; y=2; z=2; 585263:>0:r1=0; 0:r4=1; y=2; z=2; 1452118:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=00bb906e6b50e3e5b6bc490a41e163e4 Observation Y04 Never 0 800000000 Time Y04 54.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 359003:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 18835 :>0:r1=1; 0:r4=0; 2:r3=0; y=1; 1492635:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 6027225:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 65310541:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 1566280:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 6515697:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 439352112:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 15611 :>0:r1=0; 0:r4=0; 2:r3=0; y=2; 560199:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 649935:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 6185014:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 279372:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 7351512:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 264316029:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=2d110167698039bf55def82743b120ef Observation Y05 Never 0 800000000 Time Y05 41.70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 61266923:>0:r1=0; 0:r4=0; y=1; z=1; 1859677:>0:r1=1; 0:r4=0; y=1; z=1; 5135623:>0:r1=0; 0:r4=1; y=1; z=1; 444662147:>0:r1=1; 0:r4=1; y=1; z=1; 5906248:>0:r1=0; 0:r4=0; y=2; z=1; 187887:>0:r1=1; 0:r4=0; y=2; z=1; 8495974:>0:r1=0; 0:r4=1; y=2; z=1; 253568038:>0:r1=1; 0:r4=1; y=2; z=1; 1491271:>0:r1=0; 0:r4=0; y=1; z=2; 52281 :>0:r1=1; 0:r4=0; y=1; z=2; 2783324:>0:r1=0; 0:r4=1; y=1; z=2; 13108984:>0:r1=1; 0:r4=1; y=1; z=2; 23392 :>0:r1=0; 0:r4=0; y=2; z=2; 722960:>0:r1=0; 0:r4=1; y=2; z=2; 735271:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5519b7e18d61900b26b6e20148fd6e5b Observation Y06 Never 0 800000000 Time Y06 55.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 27914881:>0:r1=0; 0:r4=0; 1:r3=0; 74379594:>0:r1=0; 0:r4=1; 1:r3=0; 69825985:>0:r1=1; 0:r4=1; 1:r3=0; 185332061:>0:r1=0; 0:r4=0; 1:r3=1; 59629661:>0:r1=1; 0:r4=0; 1:r3=1; 40211408:>0:r1=0; 0:r4=1; 1:r3=1; 542706410:>0:r1=1; 0:r4=1; 1:r3=1; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=75dc62611c83cbf21aa9273aa6a41b23 Observation Y07 Never 0 1000000000 Time Y07 76.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1870261:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 20908 :>0:r1=1; 0:r4=0; 1:r3=0; z=1; 4494016:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 6204401:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 69565834:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 8523069:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 8713303:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 627183268:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 49023 :>0:r1=0; 0:r4=0; 1:r3=0; z=2; 847906:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 684925:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 4500350:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 414473:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 4157544:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 62770719:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=6f98559c8174fdcd1fe2a621ad7dc8d2 Observation Y08 Never 0 800000000 Time Y08 42.40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31649 :>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 381437:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 219910:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 2253133:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 45570 :>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 8167315:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 16796893:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 4020663:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 82761 :>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 13183345:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 22261505:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 64425190:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 6229038:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 98335058:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 563566533:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=f9c57151a878a2fb7ca88a7241079b1d Observation Y09 Never 0 800000000 Time Y09 37.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 2304098:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 92993 :>0:r1=1; 0:r4=0; 1:r3=0; z=1; 5829123:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 16503273:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 78265614:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 10562123:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 29709540:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 643145384:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 9712 :>0:r1=0; 0:r4=0; 1:r3=0; z=2; 391189:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 385199:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 1064648:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 67494 :>0:r1=1; 0:r4=0; 1:r3=1; z=2; 2976378:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 8693232:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=d987b1dfa9ff6dbc9cfc5646bda90ed3 Observation Y10 Never 0 800000000 Time Y10 41.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 179021592:>0:r1=0; 0:r4=0; y=1; 51501715:>0:r1=1; 0:r4=0; y=1; 47163428:>0:r1=0; 0:r4=1; y=1; 570331662:>0:r1=1; 0:r4=1; y=1; 20313528:>0:r1=0; 0:r4=0; y=2; 67820327:>0:r1=0; 0:r4=1; y=2; 63847748:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5506d17360dcb64cbec742d67fe4340e Observation Y11 Never 0 1000000000 Time Y11 83.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y12.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y12 "Rf*e DpAddrdR Fre SyncdWW Wse LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,2 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | lwsync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | | ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y12 Allowed Histogram (15 states) 60804964:>0:r1=0; 0:r4=0; y=1; z=1; 3363432:>0:r1=1; 0:r4=0; y=1; z=1; 7310335:>0:r1=0; 0:r4=1; y=1; z=1; 669103996:>0:r1=1; 0:r4=1; y=1; z=1; 349953:>0:r1=0; 0:r4=0; y=2; z=1; 8866 :>0:r1=1; 0:r4=0; y=2; z=1; 2491834:>0:r1=0; 0:r4=1; y=2; z=1; 3888542:>0:r1=1; 0:r4=1; y=2; z=1; 2004245:>0:r1=0; 0:r4=0; y=1; z=2; 121901:>0:r1=1; 0:r4=0; y=1; z=2; 3598635:>0:r1=0; 0:r4=1; y=1; z=2; 46206080:>0:r1=1; 0:r4=1; y=1; z=2; 13267 :>0:r1=0; 0:r4=0; y=2; z=2; 396718:>0:r1=0; 0:r4=1; y=2; z=2; 337232:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=e74570fa8cc4ed49e2bc7eb3e6efaadc Observation Y12 Never 0 800000000 Time Y12 54.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 879609:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 28477 :>0:r1=1; 0:r4=0; 2:r3=0; y=1; 2677685:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 7742026:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 69245997:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 5036986:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 35057235:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 634672186:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 10389 :>0:r1=0; 0:r4=0; 2:r3=0; y=2; 393306:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 504858:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 2548180:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 51159 :>0:r1=1; 0:r4=0; 2:r3=1; y=2; 7424816:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 33727091:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=d514c17376c3fe56c7da249e5154e952 Observation Y13 Never 0 800000000 Time Y13 42.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 60093990:>0:r1=0; 0:r4=0; y=1; z=1; 4011786:>0:r1=1; 0:r4=0; y=1; z=1; 21137207:>0:r1=0; 0:r4=1; y=1; z=1; 655772590:>0:r1=1; 0:r4=1; y=1; z=1; 590677:>0:r1=0; 0:r4=0; y=2; z=1; 10404 :>0:r1=1; 0:r4=0; y=2; z=1; 3714569:>0:r1=0; 0:r4=1; y=2; z=1; 45695290:>0:r1=1; 0:r4=1; y=2; z=1; 221889:>0:r1=0; 0:r4=0; y=1; z=2; 41128 :>0:r1=1; 0:r4=0; y=1; z=2; 2291668:>0:r1=0; 0:r4=1; y=1; z=2; 5986133:>0:r1=1; 0:r4=1; y=1; z=2; 1183 :>0:r1=0; 0:r4=0; y=2; z=2; 225677:>0:r1=0; 0:r4=1; y=2; z=2; 205809:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=db5bc36ebd8ef1745e795c6bdf75e423 Observation Y14 Never 0 800000000 Time Y14 54.16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 622447:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 20688 :>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 559332:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 13809165:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 19193 :>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 292352:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 993052:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 575094:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 372055:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 7518 :>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 19472212:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 13628767:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 949790:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 15879687:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 732798648:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=11eec175e5c988e350ebfc54fd0e2c1c Observation Y15 Never 0 800000000 Time Y15 37.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 80039724:>0:r1=0; 0:r3=0; y=1; 38800566:>0:r1=1; 0:r3=0; y=1; 17274633:>0:r1=0; 0:r3=1; y=1; 650333557:>0:r1=1; 0:r3=1; y=1; 10154811:>0:r1=0; 0:r3=0; y=2; 79379594:>0:r1=0; 0:r3=1; y=2; 124017115:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=8e9853ba7646212616eafb737d8e71e4 Observation Y16 Never 0 1000000000 Time Y16 84.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 3993993:>0:r1=0; 0:r3=0; y=1; z=1; 685103:>0:r1=1; 0:r3=0; y=1; z=1; 6433297:>0:r1=0; 0:r3=1; y=1; z=1; 701896839:>0:r1=1; 0:r3=1; y=1; z=1; 484203:>0:r1=0; 0:r3=0; y=2; z=1; 30517 :>0:r1=1; 0:r3=0; y=2; z=1; 1550340:>0:r1=0; 0:r3=1; y=2; z=1; 35121064:>0:r1=1; 0:r3=1; y=2; z=1; 379526:>0:r1=0; 0:r3=0; y=1; z=2; 29921 :>0:r1=1; 0:r3=0; y=1; z=2; 458894:>0:r1=0; 0:r3=1; y=1; z=2; 45477489:>0:r1=1; 0:r3=1; y=1; z=2; 21401 :>0:r1=0; 0:r3=0; y=2; z=2; 283751:>0:r1=0; 0:r3=1; y=2; z=2; 3153662:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=5dde3da66b8fd3eb942a6c2fb7e9050b Observation Y17 Never 0 800000000 Time Y17 53.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 284069:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 9729 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 503032:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 9425245:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 6335569:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 1416887:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 3476136:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 420878530:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 10215 :>0:r1=0; 0:r3=0; 2:r3=0; y=2; 275370:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 2006854:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 2147113:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 261594:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 4545178:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 348424479:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=abfe8f96fb73d61f24cd4ed25c4cbe36 Observation Y18 Never 0 800000000 Time Y18 42.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 2373891:>0:r1=0; 0:r3=0; y=1; z=1; 730920:>0:r1=1; 0:r3=0; y=1; z=1; 7020930:>0:r1=0; 0:r3=1; y=1; z=1; 479454864:>0:r1=1; 0:r3=1; y=1; z=1; 624522:>0:r1=0; 0:r3=0; y=2; z=1; 60394 :>0:r1=1; 0:r3=0; y=2; z=1; 1711691:>0:r1=0; 0:r3=1; y=2; z=1; 299562158:>0:r1=1; 0:r3=1; y=2; z=1; 33070 :>0:r1=0; 0:r3=0; y=1; z=2; 5325 :>0:r1=1; 0:r3=0; y=1; z=2; 212906:>0:r1=0; 0:r3=1; y=1; z=2; 6753977:>0:r1=1; 0:r3=1; y=1; z=2; 1437 :>0:r1=0; 0:r3=0; y=2; z=2; 66449 :>0:r1=0; 0:r3=1; y=2; z=2; 1387466:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=a4ab8a1891a2982f2576f75c35f64825 Observation Y19 Never 0 800000000 Time Y19 54.62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 18300085:>0:r1=0; 0:r3=0; 1:r3=0; 74870283:>0:r1=0; 0:r3=1; 1:r3=0; 73655104:>0:r1=1; 0:r3=1; 1:r3=0; 89278888:>0:r1=0; 0:r3=0; 1:r3=1; 51150083:>0:r1=1; 0:r3=0; 1:r3=1; 20432302:>0:r1=0; 0:r3=1; 1:r3=1; 672313255:>0:r1=1; 0:r3=1; 1:r3=1; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=310ba9b87ba9c8abbb2cb09115abba03 Observation Y20 Never 0 1000000000 Time Y20 78.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1118409:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 8873 :>0:r1=1; 0:r3=0; 1:r3=0; z=1; 3214196:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 4682261:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 6235426:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 4222149:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 4882984:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 708488886:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 30560 :>0:r1=0; 0:r3=0; 1:r3=0; z=2; 305667:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 1713961:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 769969:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 208105:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 1815894:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 62302660:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=63a4ff1b2a8c61b6b9352662bce3e8c9 Observation Y21 Never 0 800000000 Time Y21 41.22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 17251 :>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 220031:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 469532:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 970310:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 29119 :>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 2921527:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 21299730:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 1307790:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 44918 :>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 8653490:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 36524744:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 14466312:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 4941744:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 21677279:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 686456223:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=8a2b1f87ebce2fea7bdd4e78ab49e198 Observation Y22 Never 0 800000000 Time Y22 36.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 1064138:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 26308 :>0:r1=1; 0:r3=0; 1:r3=0; z=1; 3308100:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 12505554:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 6210399:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 5223538:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 10384570:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 748663293:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 3301 :>0:r1=0; 0:r3=0; 1:r3=0; z=2; 58959 :>0:r1=0; 0:r3=1; 1:r3=0; z=2; 1126507:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 117494:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 16648 :>0:r1=1; 0:r3=0; 1:r3=1; z=2; 811129:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 10480062:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=34f72841a6635924e4f6e89a17ea5886 Observation Y23 Never 0 800000000 Time Y23 42.53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 87448734:>0:r1=0; 0:r3=0; y=1; 42197017:>0:r1=1; 0:r3=0; y=1; 33550755:>0:r1=0; 0:r3=1; y=1; 689191290:>0:r1=1; 0:r3=1; y=1; 9434630:>0:r1=0; 0:r3=0; y=2; 70784885:>0:r1=0; 0:r3=1; y=2; 67392689:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 1000000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=967cc1d43171137af345c68503a9bda3 Observation Y24 Never 0 1000000000 Time Y24 84.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 4444568:>0:r1=0; 0:r3=0; y=1; z=1; 1660357:>0:r1=1; 0:r3=0; y=1; z=1; 7077247:>0:r1=0; 0:r3=1; y=1; z=1; 718825108:>0:r1=1; 0:r3=1; y=1; z=1; 147700:>0:r1=0; 0:r3=0; y=2; z=1; 3794 :>0:r1=1; 0:r3=0; y=2; z=1; 1291870:>0:r1=0; 0:r3=1; y=2; z=1; 3251825:>0:r1=1; 0:r3=1; y=2; z=1; 789390:>0:r1=0; 0:r3=0; y=1; z=2; 91137 :>0:r1=1; 0:r3=0; y=1; z=2; 1525971:>0:r1=0; 0:r3=1; y=1; z=2; 60020838:>0:r1=1; 0:r3=1; y=1; z=2; 9805 :>0:r1=0; 0:r3=0; y=2; z=2; 210778:>0:r1=0; 0:r3=1; y=2; z=2; 649612:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=67d202536303d5d116d23867165f4ed6 Observation Y25 Never 0 800000000 Time Y25 55.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 339193:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 8678 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 1061383:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 11365017:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 6864935:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 2402919:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 9171406:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 713325781:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 4361 :>0:r1=0; 0:r3=0; 2:r3=0; y=2; 173110:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 1155579:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 1131452:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 27150 :>0:r1=1; 0:r3=0; 2:r3=1; y=2; 4451503:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 48517533:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=44ca19804af93c9cee9c0f6acff5a2b0 Observation Y26 Never 0 800000000 Time Y26 42.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 4464493:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 3318696:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 879378:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 859901:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 2564054:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 5078541:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 346160814:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 415649784:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 137468:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 3098 :>0:r1=1; 2:r1=0; 2:r3=0; x=2; 10553 :>0:r1=0; 2:r1=1; 2:r3=0; x=2; 846996:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 114275:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 18199042:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 1712907:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ad65804aeb1597ba714e2328512d7995 Observation Y27 Never 0 800000000 Time Y27 40.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 84993822:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 23350866:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 442049:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 44534 :>1:r1=1; 3:r1=1; 3:r4=0; x=1; 12391585:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 8343100:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 238925363:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 414750329:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 4690174:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 36399 :>1:r1=1; 3:r1=0; 3:r4=0; x=2; 1826 :>1:r1=0; 3:r1=1; 3:r4=0; x=2; 2050439:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 873888:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 6367683:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 2737943:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=ce1b4a24ee0901b9de433860bfb46080 Observation Y28 Never 0 800000000 Time Y28 33.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 22702001:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 733248:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 95212 :>1:r1=0; 3:r1=1; 3:r3=0; x=1; 3888 :>1:r1=1; 3:r1=1; 3:r3=0; x=1; 40617055:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 6315688:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 273811279:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 442034771:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 271632:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 6792 :>1:r1=1; 3:r1=0; 3:r3=0; x=2; 1698 :>1:r1=0; 3:r1=1; 3:r3=0; x=2; 1213618:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 442940:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 7965427:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 3784751:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=8bc55273b7032305e0142605023bce2d Observation Y29 Never 0 800000000 Time Y29 33.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 46027546:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 28589216:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 1350632:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 605576:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 3830649:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 13747243:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 329517684:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 334966111:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 2785098:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 21165 :>0:r1=1; 2:r1=0; 2:r4=0; x=2; 60448 :>0:r1=0; 2:r1=1; 2:r4=0; x=2; 4364195:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 580811:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 32609349:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 944277:>0:r1=1; 2:r1=1; 2:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=3e1573bf73b4fdef87461b3565d66b20 Observation Y30 Never 0 800000000 Time Y30 40.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 6446382:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 4375973:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 839483:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 676323:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 2938665:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 6598632:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 340625044:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 405795816:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 705254:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 7264 :>0:r1=1; 2:r1=0; 2:r3=0; x=2; 16524 :>0:r1=0; 2:r1=1; 2:r3=0; x=2; 1431282:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 200649:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 27116040:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 2226669:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=e6774eda20819c8f372129af64bca016 Observation Y31 Never 0 800000000 Time Y31 40.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 504710:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 21653 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 91438891:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 25593997:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 1652 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 337954:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 22054 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 1972756:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 996146:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 32322258:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 12272016:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 2736666:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 1680849:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 214563412:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 415534986:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=a577eb9c8f1d583ecead3fdf77525a1e Observation Y32 Never 0 800000000 Time Y32 30.75 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 144610:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 5347 :>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 8857903:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 525769:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 1731 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 125847:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 4527 :>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 691442:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 139988:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 35744678:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 4810530:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 4760284:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 1280050:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 298541778:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 444365516:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 800000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=eea22bd3e2446126dd9b287b5df5faca Observation Y33 Never 0 800000000 Time Y33 29.81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 93079525:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 26309677:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 422196:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 47483 :>1:r1=1; 3:r1=1; 3:r4=0; x=1; 28153405:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 13263938:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 200061231:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 433751994:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 132249:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 7132 :>1:r1=1; 3:r1=0; 3:r4=0; x=2; 784 :>1:r1=0; 3:r1=1; 3:r4=0; x=2; 800357:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 732599:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 1324943:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 1912487:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=49482953dd91da1bcee183b3b0b006b8 Observation Y34 Never 0 800000000 Time Y34 33.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 24119028:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 911632:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 78395 :>1:r1=0; 3:r1=1; 3:r3=0; x=1; 3452 :>1:r1=1; 3:r1=1; 3:r3=0; x=1; 47955924:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 8570822:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 245110975:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 467843360:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 54648 :>1:r1=0; 3:r1=0; 3:r3=0; x=2; 1645 :>1:r1=1; 3:r1=0; 3:r3=0; x=2; 687 :>1:r1=0; 3:r1=1; 3:r3=0; x=2; 347491:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 169808:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 2063220:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 2768913:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 800000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=1ab190404386bf69014d12d891f99e7c Observation Y35 Never 0 800000000 Time Y35 34.75 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=-i 1 sam jan 22 17:07:09 CET 2011