Sat Jan 22 10:58:53 CST 2011 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X00.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X00 "Rfe DpAddrdR Fre LwSyncdWW Rfe DpAddrdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r5 | lwsync ; | li r3,1 | | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: lwz 30,0(11) _litmus_P2_1_: xor 10,30,30 _litmus_P2_2_: lwzx 31,10,9 Test X00 Allowed Histogram (16 states) 34187875:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 376748:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 13390956:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 22123390:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 372954:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 19 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=0; 7675515:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 4838602:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 13113867:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 7574797:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 2824807:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 29398305:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 21966138:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 5300820:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 29262718:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 7592489:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; Ok Witnesses Positive: 19, Negative: 199999981 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is validated Hash=6559e19d9e37619f3f8bf433a5805105 Observation X00 Sometimes 19 199999981 Time X00 434.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X01.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X01 "Rfe DpAddrdR Fre LwSyncdWW Rfe DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | beq LC00 | lwsync ; | li r3,1 | LC00: | li r3,1 ; | stw r3,0(r4) | isync | stw r3,0(r4) ; | | lwz r3,0(r4) | ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: cmpw 3,3 _litmus_P2_2_: beq LitLC00 _litmus_P2_3_: LitLC00: _litmus_P2_4_: isync _litmus_P2_5_: lwz 31,0(9) Test X01 Allowed Histogram (16 states) 33929106:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 367731:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 13407937:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 22407875:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 378524:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 14 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=0; 7724407:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 4905074:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 13303178:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 7619928:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 2820728:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 29461109:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 21869841:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 5271689:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 29144647:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 7388212:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 14, Negative: 199999986 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=2dd158f1ef0b66595a56ff21c6e00a13 Observation X01 Sometimes 14 199999986 Time X01 423.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 19068584:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 10270566:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 3858625:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 30313129:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 16180095:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 2400733:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 27546347:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 8505059:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 32617488:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 508019:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 16089684:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 22869213:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 501972:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 7017257:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 2253229:>0:r1=1; 0:r4=1; 2:r1=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is NOT validated Hash=ddaab862216f1c9eafeceba074a24928 Observation X02 Never 0 200000000 Time X02 487.98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 50661096:>0:r1=0; 0:r4=0; y=1; 17773501:>0:r1=1; 0:r4=0; y=1; 3805171:>0:r1=0; 0:r4=1; y=1; 43447028:>0:r1=1; 0:r4=1; y=1; 16477254:>0:r1=0; 0:r4=0; y=2; 1 :>0:r1=1; 0:r4=0; y=2; 56593679:>0:r1=0; 0:r4=1; y=2; 11242270:>0:r1=1; 0:r4=1; y=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=979eb45568765c8b5bb24cb8beb2a694 Observation X03 Sometimes 1 199999999 Time X03 258.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X04.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X04 "Rfe DpAddrdR Fre LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | lwsync | lwsync ; | li r3,1 | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X04 Allowed Histogram (16 states) 17801798:>0:r1=0; 0:r4=0; y=1; z=1; 9172951:>0:r1=1; 0:r4=0; y=1; z=1; 2629766:>0:r1=0; 0:r4=1; y=1; z=1; 30513666:>0:r1=1; 0:r4=1; y=1; z=1; 11660055:>0:r1=0; 0:r4=0; y=2; z=1; 2280608:>0:r1=1; 0:r4=0; y=2; z=1; 20727271:>0:r1=0; 0:r4=1; y=2; z=1; 15525311:>0:r1=1; 0:r4=1; y=2; z=1; 34219294:>0:r1=0; 0:r4=0; y=1; z=2; 657523:>0:r1=1; 0:r4=0; y=1; z=2; 12942692:>0:r1=0; 0:r4=1; y=1; z=2; 19605014:>0:r1=1; 0:r4=1; y=1; z=2; 3065509:>0:r1=0; 0:r4=0; y=2; z=2; 1 :>0:r1=1; 0:r4=0; y=2; z=2; 11736716:>0:r1=0; 0:r4=1; y=2; z=2; 7461825:>0:r1=1; 0:r4=1; y=2; z=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=bbe86be3ef3c2131f0d4681c0ccd31a8 Observation X04 Sometimes 1 199999999 Time X04 521.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X05.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X05 "Rfe DpAddrdR Fre LwSyncdWW Wse SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | sync | lwsync ; | li r3,1 | lwz r3,0(r4) | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X05 Allowed Histogram (16 states) 33022391:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 151498:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 12670703:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 5997686:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 12735144:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 6232200:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 2308804:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 31016125:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 203630:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 2 :>0:r1=1; 0:r4=0; 2:r3=0; y=2; 4985539:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 4523170:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 24268388:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 8146563:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 35503005:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 18235152:>0:r1=1; 0:r4=1; 2:r3=1; y=2; Ok Witnesses Positive: 2, Negative: 199999998 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is validated Hash=2f45a04baa1582caaf7bebb0f6429fad Observation X05 Sometimes 2 199999998 Time X05 518.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15021361:>0:r1=0; 0:r4=0; y=1; z=1; 8310421:>0:r1=1; 0:r4=0; y=1; z=1; 5977590:>0:r1=0; 0:r4=1; y=1; z=1; 38340540:>0:r1=1; 0:r4=1; y=1; z=1; 20783931:>0:r1=0; 0:r4=0; y=2; z=1; 5207165:>0:r1=1; 0:r4=0; y=2; z=1; 31962283:>0:r1=0; 0:r4=1; y=2; z=1; 26267450:>0:r1=1; 0:r4=1; y=2; z=1; 33311999:>0:r1=0; 0:r4=0; y=1; z=2; 118164:>0:r1=1; 0:r4=0; y=1; z=2; 4901844:>0:r1=0; 0:r4=1; y=1; z=2; 4488864:>0:r1=1; 0:r4=1; y=1; z=2; 200352:>0:r1=0; 0:r4=0; y=2; z=2; 3405277:>0:r1=0; 0:r4=1; y=2; z=2; 1702759:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=2f7e7e797a32b772dba41a2c989f624e Observation X06 Never 0 200000000 Time X06 540.66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X07.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X07 "Rfe DpAddrdR Fre SyncdWR Fre LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; lwz r1,0(r2) | li r1,1 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | lwsync ; | lwz r3,0(r4) | li r3,1 ; | | stw r3,0(r4) ; exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 31,1 _litmus_P1_1_: stw 31,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 30,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X07 Allowed Histogram (7 states) 18133600:>0:r1=0; 0:r4=0; 1:r3=0; 45314073:>0:r1=0; 0:r4=1; 1:r3=0; 6839042:>0:r1=1; 0:r4=1; 1:r3=0; 51392479:>0:r1=0; 0:r4=0; 1:r3=1; 20159235:>0:r1=1; 0:r4=0; 1:r3=1; 6842354:>0:r1=0; 0:r4=1; 1:r3=1; 51319217:>0:r1=1; 0:r4=1; 1:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=27f80466ebe5b987c02fd5b2375e9014 Observation X07 Never 0 200000000 Time X07 237.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8049858:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 195870:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 22374555:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 12161179:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 22854724:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 19977138:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 1358238:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 20812847:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 5125741:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 6963620:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 223242:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 42411875:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 2703705:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 18281772:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 16505636:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=c693aeac120b5ebe47aca8096f1cefc4 Observation X08 Never 0 200000000 Time X08 512.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 88375 :>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 2721921:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 1867223:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 32600089:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 97646 :>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 14665774:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 14201805:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 14512931:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 489774:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 30240205:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 15587279:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 23058135:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 20134123:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 1766261:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 27968459:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=25130932b014cac34245d116a5f68876 Observation X09 Never 0 200000000 Time X09 446.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14496484:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 607130:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 28645310:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 17748758:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 25032882:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 21447655:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 5955981:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 27790730:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 138321:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 3104176:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 1015079:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 33303459:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 103605:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 14909736:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 5700694:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=6da0ade67698eb3fe55496c10e533d9d Observation X10 Never 0 200000000 Time X10 505.23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X11.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X11 "Rfe DpAddrdR Fre SyncdWW Wse LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; lwz r1,0(r2) | li r1,1 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | lwsync ; | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 27,0(11) _litmus_P0_1_: xor 10,27,27 _litmus_P0_2_: lwzx 28,10,9 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X11 Allowed Histogram (7 states) 53608073:>0:r1=0; 0:r4=0; y=1; 19836782:>0:r1=1; 0:r4=0; y=1; 9498474:>0:r1=0; 0:r4=1; y=1; 50791690:>0:r1=1; 0:r4=1; y=1; 15433676:>0:r1=0; 0:r4=0; y=2; 44555105:>0:r1=0; 0:r4=1; y=2; 6276200:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=2e151daaab42138b8c478ba081d896ed Observation X11 Never 0 200000000 Time X11 263.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 22289549:>0:r1=0; 0:r4=0; y=1; z=1; 17893872:>0:r1=1; 0:r4=0; y=1; z=1; 8407282:>0:r1=0; 0:r4=1; y=1; z=1; 30193455:>0:r1=1; 0:r4=1; y=1; z=1; 8720421:>0:r1=0; 0:r4=0; y=2; z=1; 150110:>0:r1=1; 0:r4=0; y=2; z=1; 13698959:>0:r1=0; 0:r4=1; y=2; z=1; 8409157:>0:r1=1; 0:r4=1; y=2; z=1; 37749760:>0:r1=0; 0:r4=0; y=1; z=2; 3124704:>0:r1=1; 0:r4=0; y=1; z=2; 15779471:>0:r1=0; 0:r4=1; y=1; z=2; 23906581:>0:r1=1; 0:r4=1; y=1; z=2; 3437718:>0:r1=0; 0:r4=0; y=2; z=2; 5776099:>0:r1=0; 0:r4=1; y=2; z=2; 462862:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=449f3e0ad9111a8f4431787ea3e14c01 Observation X12 Never 0 200000000 Time X12 498.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33456616:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 167934:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 18941195:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 10800835:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 23988496:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 20354957:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 10239231:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 32059595:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 128636:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 3301498:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 1199318:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 13938544:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 601057:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 20785718:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 10036370:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=e039602c16d523ecfdb1a0b4937a34a6 Observation X13 Never 0 200000000 Time X13 493.66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 23191254:>0:r1=0; 0:r4=0; y=1; z=1; 19421737:>0:r1=1; 0:r4=0; y=1; z=1; 10379741:>0:r1=0; 0:r4=1; y=1; z=1; 40910610:>0:r1=1; 0:r4=1; y=1; z=1; 13663749:>0:r1=0; 0:r4=0; y=2; z=1; 395616:>0:r1=1; 0:r4=0; y=2; z=1; 20358264:>0:r1=0; 0:r4=1; y=2; z=1; 13096053:>0:r1=1; 0:r4=1; y=2; z=1; 33267621:>0:r1=0; 0:r4=0; y=1; z=2; 164205:>0:r1=1; 0:r4=0; y=1; z=2; 11182633:>0:r1=0; 0:r4=1; y=1; z=2; 10300630:>0:r1=1; 0:r4=1; y=1; z=2; 157712:>0:r1=0; 0:r4=0; y=2; z=2; 2193906:>0:r1=0; 0:r4=1; y=2; z=2; 1316269:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=74664d9800a1cc765c71acb315cf55f7 Observation X14 Never 0 200000000 Time X14 522.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X15.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X15 "Rfe DpCtrlIsyncdR Fre LwSyncdWW Rfe DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | cmpw r1,r1 | stw r1,0(r2) ; beq LC00 | lwsync | beq LC01 | lwsync ; LC00: | li r3,1 | LC01: | li r3,1 ; isync | stw r3,0(r4) | isync | stw r3,0(r4) ; lwz r3,0(r4) | | lwz r3,0(r4) | ; exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: cmpw 30,30 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 31,0(9) _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: lwz 3,0(11) _litmus_P2_1_: cmpw 3,3 _litmus_P2_2_: beq LitLC01 _litmus_P2_3_: LitLC01: _litmus_P2_4_: isync _litmus_P2_5_: lwz 31,0(9) Test X15 Allowed Histogram (16 states) 34194357:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 386366:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 13590508:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 22087890:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 378450:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 13 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=0; 7807337:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 4844296:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 13364884:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 7696671:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 2804628:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 29238842:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 21876861:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 5251849:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 29072782:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 7404266:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 13, Negative: 199999987 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=a488ac47b1a88d9c3f30dcee477424e5 Observation X15 Sometimes 13 199999987 Time X15 428.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 50576008:>0:r1=0; 0:r3=0; y=1; 17900421:>0:r1=1; 0:r3=0; y=1; 3685594:>0:r1=0; 0:r3=1; y=1; 43506442:>0:r1=1; 0:r3=1; y=1; 16545830:>0:r1=0; 0:r3=0; y=2; 2 :>0:r1=1; 0:r3=0; y=2; 56345253:>0:r1=0; 0:r3=1; y=2; 11440450:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 2, Negative: 199999998 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=7cfc2b26a1cbcdd15d0fab061a637ce4 Observation X16 Sometimes 2 199999998 Time X16 276.03 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14610250:>0:r1=0; 0:r3=0; y=1; z=1; 7770142:>0:r1=1; 0:r3=0; y=1; z=1; 3064686:>0:r1=0; 0:r3=1; y=1; z=1; 27968919:>0:r1=1; 0:r3=1; y=1; z=1; 17289495:>0:r1=0; 0:r3=0; y=2; z=1; 3865621:>0:r1=1; 0:r3=0; y=2; z=1; 23635021:>0:r1=0; 0:r3=1; y=2; z=1; 17647876:>0:r1=1; 0:r3=1; y=2; z=1; 34431701:>0:r1=0; 0:r3=0; y=1; z=2; 649536:>0:r1=1; 0:r3=0; y=1; z=2; 11925819:>0:r1=0; 0:r3=1; y=1; z=2; 19078081:>0:r1=1; 0:r3=1; y=1; z=2; 1365636:>0:r1=0; 0:r3=0; y=2; z=2; 9621747:>0:r1=0; 0:r3=1; y=2; z=2; 7075470:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=8ece2ae907eaa93a2cebf24dcb08cf79 Observation X17 Never 0 200000000 Time X17 502.28 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33105604:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 158386:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 13710886:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 5009192:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 11508794:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 5621366:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 2298326:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 29781962:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 233188:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 5126757:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 4117937:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 25815062:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 9100858:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 36149932:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 18261750:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=773f6798f908e0cd810f3e878df07bab Observation X18 Never 0 200000000 Time X18 524.11 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 12249309:>0:r1=0; 0:r3=0; y=1; z=1; 6536492:>0:r1=1; 0:r3=0; y=1; z=1; 6265165:>0:r1=0; 0:r3=1; y=1; z=1; 36147937:>0:r1=1; 0:r3=1; y=1; z=1; 24248821:>0:r1=0; 0:r3=0; y=2; z=1; 6939186:>0:r1=1; 0:r3=0; y=2; z=1; 32629500:>0:r1=0; 0:r3=1; y=2; z=1; 28004325:>0:r1=1; 0:r3=1; y=2; z=1; 32818600:>0:r1=0; 0:r3=0; y=1; z=2; 119650:>0:r1=1; 0:r3=0; y=1; z=2; 4987936:>0:r1=0; 0:r3=1; y=1; z=2; 4183880:>0:r1=1; 0:r3=1; y=1; z=2; 260175:>0:r1=0; 0:r3=0; y=2; z=2; 3177206:>0:r1=0; 0:r3=1; y=2; z=2; 1431818:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=811f0a85dc5f811c7436b53d2ca9c449 Observation X19 Never 0 200000000 Time X19 557.18 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X20.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X20 "Rfe DpCtrlIsyncdR Fre SyncdWR Fre LwSyncdWW" {0:r2=z; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; lwz r1,0(r2) | li r1,1 | li r1,1 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | sync | lwsync ; LC00: | lwz r3,0(r4) | li r3,1 ; isync | | stw r3,0(r4) ; lwz r3,0(r4) | | ; exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 31,1 _litmus_P1_1_: stw 31,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 30,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: cmpw 30,30 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 31,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X20 Allowed Histogram (7 states) 18029510:>0:r1=0; 0:r3=0; 1:r3=0; 45166972:>0:r1=0; 0:r3=1; 1:r3=0; 6830529:>0:r1=1; 0:r3=1; 1:r3=0; 51866984:>0:r1=0; 0:r3=0; 1:r3=1; 20578077:>0:r1=1; 0:r3=0; 1:r3=1; 7118374:>0:r1=0; 0:r3=1; 1:r3=1; 50409554:>0:r1=1; 0:r3=1; 1:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=0c99e9e00ef12798cd94e468d7533fcb Observation X20 Never 0 200000000 Time X20 237.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 10395371:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 183809:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 25327119:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 12158480:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 22973539:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 20583433:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 1415353:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 20977720:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 2795856:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 3662166:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 169040:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 42268600:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 2766563:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 18030219:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 16292732:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=10b56f844965b778138fc256080a6cb2 Observation X21 Never 0 200000000 Time X21 502.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 61118 :>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 2861235:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 1585203:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 32610605:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 89198 :>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 15927074:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 12979390:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 14492320:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 467498:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 30182576:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 15506221:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 23060546:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 20442088:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 1788835:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 27946093:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=e7fc832a2e4b347328216cfab07885d9 Observation X22 Never 0 200000000 Time X22 427.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14402667:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 610447:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 28036279:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 17812359:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 25071175:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 22245095:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 5722201:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 27936684:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 131567:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 3015013:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 929683:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 33194692:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 107551:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 14992370:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 5792217:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=86fcf34749ab0aa370ea66e6893791a0 Observation X23 Never 0 200000000 Time X23 493.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 53760601:>0:r1=0; 0:r3=0; y=1; 19957715:>0:r1=1; 0:r3=0; y=1; 9950191:>0:r1=0; 0:r3=1; y=1; 50054051:>0:r1=1; 0:r3=1; y=1; 15699459:>0:r1=0; 0:r3=0; y=2; 1 :>0:r1=1; 0:r3=0; y=2; 44349019:>0:r1=0; 0:r3=1; y=2; 6228963:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=1a78bce42911eadebdb22805402de8eb Observation X24 Sometimes 1 199999999 Time X24 268.50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 22710203:>0:r1=0; 0:r3=0; y=1; z=1; 18186357:>0:r1=1; 0:r3=0; y=1; z=1; 8675798:>0:r1=0; 0:r3=1; y=1; z=1; 27824427:>0:r1=1; 0:r3=1; y=1; z=1; 10614255:>0:r1=0; 0:r3=0; y=2; z=1; 166467:>0:r1=1; 0:r3=0; y=2; z=1; 16707683:>0:r1=0; 0:r3=1; y=2; z=1; 9298270:>0:r1=1; 0:r3=1; y=2; z=1; 38154257:>0:r1=0; 0:r3=0; y=1; z=2; 3016559:>0:r1=1; 0:r3=0; y=1; z=2; 14804547:>0:r1=0; 0:r3=1; y=1; z=2; 23410561:>0:r1=1; 0:r3=1; y=1; z=2; 1884941:>0:r1=0; 0:r3=0; y=2; z=2; 4019833:>0:r1=0; 0:r3=1; y=2; z=2; 525842:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=629e26a0c6f613b14043edf57727b702 Observation X25 Never 0 200000000 Time X25 507.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33521292:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 186647:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 20552195:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 9023013:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 24163950:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 20373897:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 10085124:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 30748035:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 154684:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 3710924:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 1003711:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 14031165:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 649454:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 21256139:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 10539770:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=54da285ce144acabc337e28ea8958874 Observation X26 Never 0 200000000 Time X26 511.40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 20764760:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 14408158:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 11631055:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 1419934:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 4059857:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 27455420:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 30511621:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 8354731:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 32429044:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 426265:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 547819:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 15942180:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 6278883:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 23415093:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 2355180:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ffa63368caa391807dee9905d20510c6 Observation X27 Never 0 200000000 Time X27 510.50 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X28.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X28 "Rfe LwSyncdRW Wse LwSyncdWW Rfe DpAddrdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r5=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | xor r3,r1,r1 ; | li r3,1 | lwsync | lwzx r4,r3,r5 ; | stw r3,0(r4) | li r3,1 | ; | | stw r3,0(r4) | ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: lwsync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: lwz 28,0(11) _litmus_P3_1_: xor 10,28,28 _litmus_P3_2_: lwzx 30,10,9 _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X28 Allowed Histogram (16 states) 10501936:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 17647146:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 6765315:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 6664026:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 1964131:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 24580423:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 18821064:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 34168000:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 36543017:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 1279326:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 541557:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 62 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 11190176:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 10934423:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 11301282:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 7098116:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 62, Negative: 199999938 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=4adca431a2784b4aa9df91b1fc3b1666 Observation X28 Sometimes 62 199999938 Time X28 447.13 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X29.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X29 "Rfe LwSyncdRW Wse LwSyncdWW Rfe DpCtrlIsyncdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | cmpw r1,r1 ; | li r3,1 | lwsync | beq LC00 ; | stw r3,0(r4) | li r3,1 | LC00: ; | | stw r3,0(r4) | isync ; | | | lwz r3,0(r4) ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: lwsync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: lwz 28,0(11) _litmus_P3_1_: cmpw 28,28 _litmus_P3_2_: beq LitLC00 _litmus_P3_3_: LitLC00: _litmus_P3_4_: isync _litmus_P3_5_: lwz 30,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X29 Allowed Histogram (16 states) 10540882:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 18091222:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 6748384:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 6818254:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 2015131:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 24872359:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 18738790:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 34733463:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 36621465:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 903827:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 551960:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 55 :>1:r1=1; 3:r1=1; 3:r3=0; x=2; 10433927:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 9290195:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 11945473:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 7694613:>1:r1=1; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 55, Negative: 199999945 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=cd58719fd03bc8a841de06004867cb05 Observation X29 Sometimes 55 199999945 Time X29 427.16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 20399862:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 14381109:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 11637834:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 1410490:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 3758802:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 27306354:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 30438730:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 8271741:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 32492045:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 425122:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 523218:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 15687581:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 6647641:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 24079697:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 2539774:>0:r1=1; 2:r1=1; 2:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=a0f55fa2291a072f015a1f0b83d20074 Observation X30 Never 0 200000000 Time X30 493.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 20510065:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 14421709:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 11682947:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 1433179:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 3789205:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 27368349:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 30294564:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 8206105:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 32774775:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 435767:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 520776:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 15640275:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 6628050:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 23780770:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 2513464:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ffb6dc3e13fae7c7e7811955e241147b Observation X31 Never 0 200000000 Time X31 493.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X32.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X32 "Rfe SyncdRR Fre LwSyncdWW Rfe DpAddrdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r5=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | xor r3,r1,r1 ; | lwz r3,0(r4) | lwsync | lwzx r4,r3,r5 ; | | li r3,1 | ; | | stw r3,0(r4) | ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 31,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P3_0_: lwz 30,0(11) _litmus_P3_1_: xor 10,30,30 _litmus_P3_2_: lwzx 31,10,9 _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X32 Allowed Histogram (16 states) 33466434:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 261117:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 7700568:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 21269166:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 51408 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 492 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=0; 5068082:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 8864420:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 9620653:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 7689522:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 1635089:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 28224136:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 4355311:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 7464175:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 21265000:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 43064427:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; Ok Witnesses Positive: 492, Negative: 199999508 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=abdf662fb230128532b66df78e4a75f1 Observation X32 Sometimes 492 199999508 Time X32 440.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X33.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X33 "Rfe SyncdRR Fre LwSyncdWW Rfe DpCtrlIsyncdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | cmpw r1,r1 ; | lwz r3,0(r4) | lwsync | beq LC00 ; | | li r3,1 | LC00: ; | | stw r3,0(r4) | isync ; | | | lwz r3,0(r4) ; exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: lwz 31,0(9) _litmus_P0_0_: li 7,1 _litmus_P0_1_: stw 7,0(9) _litmus_P3_0_: lwz 3,0(11) _litmus_P3_1_: cmpw 3,3 _litmus_P3_2_: beq LitLC00 _litmus_P3_3_: LitLC00: _litmus_P3_4_: isync _litmus_P3_5_: lwz 31,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X33 Allowed Histogram (16 states) 33074967:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 199182:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 7723685:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 21679205:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 41329 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 575 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; 4982465:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 9147910:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 9623694:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 7628756:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 1612009:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 28264547:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 4286515:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 7488677:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 21353705:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 42892779:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; Ok Witnesses Positive: 575, Negative: 199999425 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=c86889a7cdc1c89457a71c414046d8c0 Observation X33 Sometimes 575 199999425 Time X33 414.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X34.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X34 "Rfe SyncdRW Wse LwSyncdWW Rfe DpAddrdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r5=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | xor r3,r1,r1 ; | li r3,1 | lwsync | lwzx r4,r3,r5 ; | stw r3,0(r4) | li r3,1 | ; | | stw r3,0(r4) | ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: lwz 28,0(11) _litmus_P3_1_: xor 10,28,28 _litmus_P3_2_: lwzx 30,10,9 _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X34 Allowed Histogram (16 states) 10758523:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 19015080:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 7084639:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 7158346:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 1759755:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 28078914:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 21898187:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 41462886:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 33896658:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 203752:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 74907 :>1:r1=0; 3:r1=1; 3:r4=0; x=2; 564 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 9752421:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 8250340:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 3972441:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 6632587:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 564, Negative: 199999436 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=8db91522dc421fe43a7baf7aff0de837 Observation X34 Sometimes 564 199999436 Time X34 447.82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X35.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X35 "Rfe SyncdRW Wse LwSyncdWW Rfe DpCtrlIsyncdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | sync | stw r1,0(r2) | cmpw r1,r1 ; | li r3,1 | lwsync | beq LC00 ; | stw r3,0(r4) | li r3,1 | LC00: ; | | stw r3,0(r4) | isync ; | | | lwz r3,0(r4) ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: lwz 28,0(11) _litmus_P3_1_: cmpw 28,28 _litmus_P3_2_: beq LitLC00 _litmus_P3_3_: LitLC00: _litmus_P3_4_: isync _litmus_P3_5_: lwz 30,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X35 Allowed Histogram (16 states) 11162136:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 19828943:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 6894696:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 6764627:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 1759119:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 27884502:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 21842987:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 42190543:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 33707884:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 169807:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 75061 :>1:r1=0; 3:r1=1; 3:r3=0; x=2; 475 :>1:r1=1; 3:r1=1; 3:r3=0; x=2; 9043479:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 7411707:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 4289227:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 6974807:>1:r1=1; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 475, Negative: 199999525 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=00744a65cf189719eb1309a79c27a2ca Observation X35 Sometimes 475 199999525 Time X35 437.79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31274919:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 546169:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 1147070:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 24951983:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 557365:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 1117951:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 13203284:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 1172695:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 1035677:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 197977:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 19159633:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 24710095:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 13376990:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 18875894:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 48672298:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=08b576a9816ca91b136efc84cb8198fe Observation Y00 Never 0 200000000 Time Y00 432.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y01.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y01 "Rf*e DpAddrdR Fre LwSyncdWW Rf*e DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | DIY01: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | cmpw r1,r1 | lwsync ; lwzx r4,r3,r5 | li r3,1 | beq LC02 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | LC02: | stw r3,0(r4) ; bne DIY00 | | isync | ; | | lwz r3,0(r4) | ; | | stwcx. r1,r0,r2 | ; | | bne DIY01 | ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 30,0,11 _litmus_P0_2_: xor 10,30,30 _litmus_P0_3_: lwzx 31,10,9 _litmus_P0_4_: stwcx. 30,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: LitDIY01: _litmus_P2_1_: lwarx 3,0,11 _litmus_P2_2_: cmpw 3,3 _litmus_P2_3_: beq LitLC02 _litmus_P2_4_: LitLC02: _litmus_P2_5_: isync _litmus_P2_6_: lwz 31,0(9) _litmus_P2_7_: stwcx. 3,0,11 _litmus_P2_8_: bne LitDIY01 Test Y01 Allowed Histogram (15 states) 31218317:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 586884:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 1331257:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 25809306:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 630641:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 1277216:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 12743524:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 1197245:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 1130568:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 195757:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 19405373:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 24665632:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 13297474:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 18733886:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 47776920:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=27be645f8ce747a8241695ecd5d12775 Observation Y01 Never 0 200000000 Time Y01 445.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8008576:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 8289767:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 1008369:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 40799668:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 18950997:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 7174525:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 17434012:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 38412910:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 30585714:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 1000009:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 1299207:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 14867622:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 202491:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 892945:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 11073188:>0:r1=1; 0:r4=1; 2:r1=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r1=1) is NOT validated Hash=e299ccd513ee6b40ffc1479736b6d80f Observation Y02 Never 0 200000000 Time Y02 527.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y03.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y03 "Rf*e DpAddrdR Fre LwSyncdWW Wse LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; DIY00: | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | lwsync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 27,0,11 _litmus_P0_2_: xor 10,27,27 _litmus_P0_3_: lwzx 28,10,9 _litmus_P0_4_: stwcx. 27,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y03 Allowed Histogram (7 states) 35788453:>0:r1=0; 0:r4=0; y=1; 20767768:>0:r1=1; 0:r4=0; y=1; 821837:>0:r1=0; 0:r4=1; y=1; 56842523:>0:r1=1; 0:r4=1; y=1; 17522321:>0:r1=0; 0:r4=0; y=2; 25881564:>0:r1=0; 0:r4=1; y=2; 42375534:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=fbc1c062cf6f3291c2ce205045bcf85e Observation Y03 Never 0 200000000 Time Y03 285.93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7897352:>0:r1=0; 0:r4=0; y=1; z=1; 9885973:>0:r1=1; 0:r4=0; y=1; z=1; 647779:>0:r1=0; 0:r4=1; y=1; z=1; 34274368:>0:r1=1; 0:r4=1; y=1; z=1; 15315420:>0:r1=0; 0:r4=0; y=2; z=1; 4626058:>0:r1=1; 0:r4=0; y=2; z=1; 11389732:>0:r1=0; 0:r4=1; y=2; z=1; 32319700:>0:r1=1; 0:r4=1; y=2; z=1; 26474733:>0:r1=0; 0:r4=0; y=1; z=2; 696710:>0:r1=1; 0:r4=0; y=1; z=2; 3267737:>0:r1=0; 0:r4=1; y=1; z=2; 35758389:>0:r1=1; 0:r4=1; y=1; z=2; 1223072:>0:r1=0; 0:r4=0; y=2; z=2; 4355866:>0:r1=0; 0:r4=1; y=2; z=2; 11867111:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=00bb906e6b50e3e5b6bc490a41e163e4 Observation Y04 Never 0 200000000 Time Y04 541.85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30880005:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 293415:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 1497943:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 19728991:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 7012748:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 6131608:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 616566:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 37957887:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 263478:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 1116080:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 8899399:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 19178208:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 9479873:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 16095286:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 40848513:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=2d110167698039bf55def82743b120ef Observation Y05 Never 0 200000000 Time Y05 524.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7339164:>0:r1=0; 0:r4=0; y=1; z=1; 7815431:>0:r1=1; 0:r4=0; y=1; z=1; 681512:>0:r1=0; 0:r4=1; y=1; z=1; 47644483:>0:r1=1; 0:r4=1; y=1; z=1; 19025496:>0:r1=0; 0:r4=0; y=2; z=1; 7516558:>0:r1=1; 0:r4=0; y=2; z=1; 14206147:>0:r1=0; 0:r4=1; y=2; z=1; 48614014:>0:r1=1; 0:r4=1; y=2; z=1; 28832746:>0:r1=0; 0:r4=0; y=1; z=2; 297010:>0:r1=1; 0:r4=0; y=1; z=2; 1444145:>0:r1=0; 0:r4=1; y=1; z=2; 11649401:>0:r1=1; 0:r4=1; y=1; z=2; 250221:>0:r1=0; 0:r4=0; y=2; z=2; 1004781:>0:r1=0; 0:r4=1; y=2; z=2; 3678891:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5519b7e18d61900b26b6e20148fd6e5b Observation Y06 Never 0 200000000 Time Y06 543.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15350176:>0:r1=0; 0:r4=0; 1:r3=0; 28023647:>0:r1=0; 0:r4=1; 1:r3=0; 27155627:>0:r1=1; 0:r4=1; 1:r3=0; 39181843:>0:r1=0; 0:r4=0; 1:r3=1; 23203022:>0:r1=1; 0:r4=0; 1:r3=1; 1765326:>0:r1=0; 0:r4=1; 1:r3=1; 65320359:>0:r1=1; 0:r4=1; 1:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=75dc62611c83cbf21aa9273aa6a41b23 Observation Y07 Never 0 200000000 Time Y07 249.83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11705113:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 164494:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 16633714:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 22585346:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 11380342:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 22561226:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 102389:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 30179710:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 1341997:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 3648153:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 1950500:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 28452838:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 2752315:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 4245129:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 42296734:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=6f98559c8174fdcd1fe2a621ad7dc8d2 Observation Y08 Never 0 200000000 Time Y08 495.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 144723:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 539811:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 4509979:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 30082960:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 264564:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 1619018:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 29181471:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 13202935:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 243064:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 21783311:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 25376720:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 14042922:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 20311210:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 734913:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 37962399:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r4=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=f9c57151a878a2fb7ca88a7241079b1d Observation Y09 Never 0 200000000 Time Y09 478.12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13470914:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 285169:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 20122313:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 27569956:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 14458923:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 24383778:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 671599:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 42700188:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 145006:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 556182:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 3113681:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 28682478:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 284999:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 1824879:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 21729935:>0:r1=1; 0:r4=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r4=0 /\ 1:r3=0) is NOT validated Hash=d987b1dfa9ff6dbc9cfc5646bda90ed3 Observation Y10 Never 0 200000000 Time Y10 509.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 39040507:>0:r1=0; 0:r4=0; y=1; 23413497:>0:r1=1; 0:r4=0; y=1; 1936883:>0:r1=0; 0:r4=1; y=1; 67593258:>0:r1=1; 0:r4=1; y=1; 14791154:>0:r1=0; 0:r4=0; y=2; 24976912:>0:r1=0; 0:r4=1; y=2; 28247789:>0:r1=1; 0:r4=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=5506d17360dcb64cbec742d67fe4340e Observation Y11 Never 0 200000000 Time Y11 276.57 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11277473:>0:r1=0; 0:r4=0; y=1; z=1; 20212967:>0:r1=1; 0:r4=0; y=1; z=1; 939833:>0:r1=0; 0:r4=1; y=1; z=1; 42834559:>0:r1=1; 0:r4=1; y=1; z=1; 11699894:>0:r1=0; 0:r4=0; y=2; z=1; 162543:>0:r1=1; 0:r4=0; y=2; z=1; 11874955:>0:r1=0; 0:r4=1; y=2; z=1; 15348861:>0:r1=1; 0:r4=1; y=2; z=1; 28152004:>0:r1=0; 0:r4=0; y=1; z=2; 2786473:>0:r1=1; 0:r4=0; y=1; z=2; 3831106:>0:r1=0; 0:r4=1; y=1; z=2; 43721987:>0:r1=1; 0:r4=1; y=1; z=2; 1213078:>0:r1=0; 0:r4=0; y=2; z=2; 3777194:>0:r1=0; 0:r4=1; y=2; z=2; 2167073:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=e74570fa8cc4ed49e2bc7eb3e6efaadc Observation Y12 Never 0 200000000 Time Y12 504.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30860938:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 341779:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 1987913:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 29692648:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 13490309:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 19666187:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 2399944:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 49249452:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 194932:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 684898:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 4429788:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 13116864:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 301754:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 16333071:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 17249523:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=d514c17376c3fe56c7da249e5154e952 Observation Y13 Never 0 200000000 Time Y13 535.80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13441498:>0:r1=0; 0:r4=0; y=1; z=1; 21166882:>0:r1=1; 0:r4=0; y=1; z=1; 1121423:>0:r1=0; 0:r4=1; y=1; z=1; 57559595:>0:r1=1; 0:r4=1; y=1; z=1; 13282685:>0:r1=0; 0:r4=0; y=2; z=1; 242718:>0:r1=1; 0:r4=0; y=2; z=1; 15903161:>0:r1=0; 0:r4=1; y=2; z=1; 20547740:>0:r1=1; 0:r4=1; y=2; z=1; 28955882:>0:r1=0; 0:r4=0; y=1; z=2; 308721:>0:r1=1; 0:r4=0; y=1; z=2; 1819966:>0:r1=0; 0:r4=1; y=1; z=2; 21884757:>0:r1=1; 0:r4=1; y=1; z=2; 162368:>0:r1=0; 0:r4=0; y=2; z=2; 614137:>0:r1=0; 0:r4=1; y=2; z=2; 2988467:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=db5bc36ebd8ef1745e795c6bdf75e423 Observation Y14 Never 0 200000000 Time Y14 527.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31253874:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 540768:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 1443516:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 26010954:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 751576:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 1465284:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 12885077:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 1263167:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 1061029:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 210033:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 20005376:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 26252514:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 12692489:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 19329921:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 44834422:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=11eec175e5c988e350ebfc54fd0e2c1c Observation Y15 Never 0 200000000 Time Y15 418.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 36845990:>0:r1=0; 0:r3=0; y=1; 20984039:>0:r1=1; 0:r3=0; y=1; 831502:>0:r1=0; 0:r3=1; y=1; 55581666:>0:r1=1; 0:r3=1; y=1; 17654560:>0:r1=0; 0:r3=0; y=2; 25813618:>0:r1=0; 0:r3=1; y=2; 42288625:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=8e9853ba7646212616eafb737d8e71e4 Observation Y16 Never 0 200000000 Time Y16 291.04 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8873902:>0:r1=0; 0:r3=0; y=1; z=1; 10390383:>0:r1=1; 0:r3=0; y=1; z=1; 701696:>0:r1=0; 0:r3=1; y=1; z=1; 35962616:>0:r1=1; 0:r3=1; y=1; z=1; 15444556:>0:r1=0; 0:r3=0; y=2; z=1; 3595888:>0:r1=1; 0:r3=0; y=2; z=1; 12706443:>0:r1=0; 0:r3=1; y=2; z=1; 29356890:>0:r1=1; 0:r3=1; y=2; z=1; 25866443:>0:r1=0; 0:r3=0; y=1; z=2; 658502:>0:r1=1; 0:r3=0; y=1; z=2; 3423737:>0:r1=0; 0:r3=1; y=1; z=2; 36011609:>0:r1=1; 0:r3=1; y=1; z=2; 1038785:>0:r1=0; 0:r3=0; y=2; z=2; 3133425:>0:r1=0; 0:r3=1; y=2; z=2; 12835125:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=5dde3da66b8fd3eb942a6c2fb7e9050b Observation Y17 Never 0 200000000 Time Y17 528.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) 30872461:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 337091:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 1418407:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 19978238:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 8516552:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 6836782:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 635506:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 39289111:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 271815:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 1069395:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 9614196:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 18324352:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 8231641:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 15969936:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 38634517:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=abfe8f96fb73d61f24cd4ed25c4cbe36 Observation Y18 Never 0 200000000 Time Y18 536.76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8876760:>0:r1=0; 0:r3=0; y=1; z=1; 9476494:>0:r1=1; 0:r3=0; y=1; z=1; 755682:>0:r1=0; 0:r3=1; y=1; z=1; 49113734:>0:r1=1; 0:r3=1; y=1; z=1; 18024991:>0:r1=0; 0:r3=0; y=2; z=1; 6157287:>0:r1=1; 0:r3=0; y=2; z=1; 14421244:>0:r1=0; 0:r3=1; y=2; z=1; 44749763:>0:r1=1; 0:r3=1; y=2; z=1; 29225023:>0:r1=0; 0:r3=0; y=1; z=2; 318953:>0:r1=1; 0:r3=0; y=1; z=2; 1463345:>0:r1=0; 0:r3=1; y=1; z=2; 11863345:>0:r1=1; 0:r3=1; y=1; z=2; 279431:>0:r1=0; 0:r3=0; y=2; z=2; 1051091:>0:r1=0; 0:r3=1; y=2; z=2; 4222857:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=a4ab8a1891a2982f2576f75c35f64825 Observation Y19 Never 0 200000000 Time Y19 548.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15681052:>0:r1=0; 0:r3=0; 1:r3=0; 28526091:>0:r1=0; 0:r3=1; 1:r3=0; 27203232:>0:r1=1; 0:r3=1; 1:r3=0; 40630427:>0:r1=0; 0:r3=0; 1:r3=1; 22359374:>0:r1=1; 0:r3=0; 1:r3=1; 1937449:>0:r1=0; 0:r3=1; 1:r3=1; 63662375:>0:r1=1; 0:r3=1; 1:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=310ba9b87ba9c8abbb2cb09115abba03 Observation Y20 Never 0 200000000 Time Y20 252.21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y21.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y21 "Rf*e DpCtrlIsyncdR Fre SyncdWR Fre LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,1 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; cmpw r1,r1 | sync | lwsync | lwsync ; beq LC01 | lwz r3,0(r4) | li r3,1 | li r3,1 ; LC01: | | stw r3,0(r4) | stw r3,0(r4) ; isync | | | ; lwz r3,0(r4) | | | ; stwcx. r1,r0,r2 | | | ; bne DIY00 | | | ; exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: cmpw 28,28 _litmus_P0_3_: beq LitLC01 _litmus_P0_4_: LitLC01: _litmus_P0_5_: isync _litmus_P0_6_: lwz 30,0(9) _litmus_P0_7_: stwcx. 28,0,11 _litmus_P0_8_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y21 Allowed Histogram (15 states) 11705951:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 167465:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 16856733:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 22456713:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 12124757:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 22140745:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 104745:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 29844249:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 1328557:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 3519062:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 1961270:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 28440069:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 2814716:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 4288200:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 42246768:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=63a4ff1b2a8c61b6b9352662bce3e8c9 Observation Y21 Never 0 200000000 Time Y21 492.80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 114635:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 424488:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 4449178:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 30519525:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 236938:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 1181183:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 29139334:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 13482523:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 231905:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 21825738:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 25467027:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 14715412:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 20541597:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 766305:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 36904212:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (0:r1=1 /\ 0:r3=0 /\ 1:r3=0 /\ 2:r3=0) is NOT validated Hash=8a2b1f87ebce2fea7bdd4e78ab49e198 Observation Y22 Never 0 200000000 Time Y22 460.97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13547485:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 279181:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 20325328:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 27261663:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 14889120:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 24494403:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 701647:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 42066782:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 125856:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 475896:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 3131311:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 29123419:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 261099:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 1598054:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 21718756:>0:r1=1; 0:r3=1; 1:r3=1; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) is NOT validated Hash=34f72841a6635924e4f6e89a17ea5886 Observation Y23 Never 0 200000000 Time Y23 492.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 40233058:>0:r1=0; 0:r3=0; y=1; 23392793:>0:r1=1; 0:r3=0; y=1; 2497563:>0:r1=0; 0:r3=1; y=1; 65899758:>0:r1=1; 0:r3=1; y=1; 14961960:>0:r1=0; 0:r3=0; y=2; 25159443:>0:r1=0; 0:r3=1; y=2; 27855425:>0:r1=1; 0:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=967cc1d43171137af345c68503a9bda3 Observation Y24 Never 0 200000000 Time Y24 281.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11804972:>0:r1=0; 0:r3=0; y=1; z=1; 20486788:>0:r1=1; 0:r3=0; y=1; z=1; 1125317:>0:r1=0; 0:r3=1; y=1; z=1; 43978567:>0:r1=1; 0:r3=1; y=1; z=1; 11895570:>0:r1=0; 0:r3=0; y=2; z=1; 144471:>0:r1=1; 0:r3=0; y=2; z=1; 12838464:>0:r1=0; 0:r3=1; y=2; z=1; 13685274:>0:r1=1; 0:r3=1; y=2; z=1; 27676582:>0:r1=0; 0:r3=0; y=1; z=2; 2882944:>0:r1=1; 0:r3=0; y=1; z=2; 3913175:>0:r1=0; 0:r3=1; y=1; z=2; 43770474:>0:r1=1; 0:r3=1; y=1; z=2; 1048985:>0:r1=0; 0:r3=0; y=2; z=2; 2668402:>0:r1=0; 0:r3=1; y=2; z=2; 2080015:>0:r1=1; 0:r3=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r3=0) is NOT validated Hash=67d202536303d5d116d23867165f4ed6 Observation Y25 Never 0 200000000 Time Y25 494.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30930081:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 333204:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 1596405:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 30112541:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 14215201:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 20324521:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 2643155:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 49083527:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 165823:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 588612:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 4352595:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 13185503:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 290443:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 16240134:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 15938255:>0:r1=1; 0:r3=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0 /\ 2:r3=0) is NOT validated Hash=44ca19804af93c9cee9c0f6acff5a2b0 Observation Y26 Never 0 200000000 Time Y26 516.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7346783:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 21085021:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 6656674:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 7393011:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 1043819:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 17380953:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 39694690:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 39342925:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 30571088:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 239446:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 1059254:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 1183458:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 853658:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 15026134:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 11123086:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=ad65804aeb1597ba714e2328512d7995 Observation Y27 Never 0 200000000 Time Y27 532.16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7040625:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 12468622:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 7318813:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 6878011:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 160000:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 15518905:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 24609567:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 48886767:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 31344457:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 1073373:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 444837:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 1114839:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 2447365:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 25417447:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 15276372:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=ce1b4a24ee0901b9de433860bfb46080 Observation Y28 Never 0 200000000 Time Y28 470.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7454718:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 13057656:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 7048877:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 6867322:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 160187:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 15312312:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 24362883:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 48641965:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 31462474:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 1101598:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 473256:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 1130295:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 2398336:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 25308989:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 15219132:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=8bc55273b7032305e0142605023bce2d Observation Y29 Never 0 200000000 Time Y29 478.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 6575628:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 20542672:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 7305940:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 8033990:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 979093:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 17658117:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 39402657:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 39225945:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 30331169:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 241630:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 1000186:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 1250607:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 875848:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 15249333:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 11327185:>0:r1=1; 2:r1=1; 2:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r4=0) is NOT validated Hash=3e1573bf73b4fdef87461b3565d66b20 Observation Y30 Never 0 200000000 Time Y30 532.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7004036:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 21093038:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 7027900:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 7923610:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 1032788:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 18117879:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 39225186:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 38463616:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 30760937:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 195910:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 987083:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 1093917:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 754473:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 14879827:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 11439800:>0:r1=1; 2:r1=1; 2:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) is NOT validated Hash=e6774eda20819c8f372129af64bca016 Observation Y31 Never 0 200000000 Time Y31 512.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32914232:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 171353:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 6061403:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 13166080:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 90063 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 4482408:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 7510657:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 520689:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 1180913:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 168031:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 18301180:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 13028442:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 14888938:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 27180275:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 60335336:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=a577eb9c8f1d583ecead3fdf77525a1e Observation Y32 Never 0 200000000 Time Y32 405.10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33055400:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 161343:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 6461337:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 13903884:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 89834 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 4209376:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 7527105:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 482375:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 1127441:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 169159:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 17845873:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 12998160:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 14857758:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 26905033:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 60205922:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; No Witnesses Positive: 0, Negative: 200000000 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=eea22bd3e2446126dd9b287b5df5faca Observation Y33 Never 0 200000000 Time Y33 399.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7149357:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 12474262:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 7521089:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 7073163:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 140417:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 18364261:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 28594796:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 57468949:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 32486980:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 157278:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 119731:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 679381:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 1326835:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 12999178:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 13444323:>1:r1=1; 3:r1=1; 3:r4=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is NOT validated Hash=49482953dd91da1bcee183b3b0b006b8 Observation Y34 Never 0 200000000 Time Y34 468.62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7490747:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 13032673:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 7313406:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 7045000:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 151761:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 18145898:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 28204577:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 57352152:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 32490953:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 194625:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 148643:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 745564:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 1458583:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 12895735:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 13329683:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=1ab190404386bf69014d12d891f99e7c Observation Y35 Never 0 200000000 Time Y35 487.08 Revision 6782, version 3.00+1 Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 100000 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 1000 #endif #ifndef AVAIL #define AVAIL 0 #endif /* gcc options: -D_GNU_SOURCE -Wall -std=gnu99 -O -m32 -pthread */ /* barrier: user */ /* launch: changing */ /* cache: false */ /* call: false */ /* affinity: incr0 */ /* randomise_affinity: false */ /* prealloc: false */ /* memory: indirect */ /* safer: true */ /* preload: true */ /* para: self */ /* speedcheck: false */ /* proc used: 0 */ GCCOPTS="-D_GNU_SOURCE -Wall -std=gnu99 -O -m32 -pthread" LITMUSOPTS=-s 1000 -r 100k Sat Jan 22 20:00:22 CST 2011