Sun Jan 23 10:50:00 CST 2011 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X00.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X00 "Rfe DpAddrdR Fre LwSyncdWW Rfe DpAddrdR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r5=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | lwz r1,0(r2) | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | xor r3,r1,r1 | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | lwzx r4,r3,r5 | lwsync ; | li r3,1 | | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 30,0(11) _litmus_P0_1_: xor 10,30,30 _litmus_P0_2_: lwzx 31,10,9 _litmus_P3_0_: li 5,1 _litmus_P3_1_: stw 5,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 4,1 _litmus_P3_4_: stw 4,0(9) _litmus_P2_0_: lwz 30,0(11) _litmus_P2_1_: xor 10,30,30 _litmus_P2_2_: lwzx 31,10,9 Test X00 Allowed Histogram (16 states) 33363290:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 3688434:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 11748145:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 22791178:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 3027984:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 1179 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=0; 9921494:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 5009892:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 13937602:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 7717039:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 722764:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 15086827:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 23894595:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 3073373:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 15615532:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 30400672:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=1; Ok Witnesses Positive: 1179, Negative: 199998821 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r4=0) is validated Hash=6559e19d9e37619f3f8bf433a5805105 Observation X00 Sometimes 1179 199998821 Time X00 404.27 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33525276:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 3642998:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 11937455:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 22674019:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 3093258:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 638 :>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=0; 10137617:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 5111220:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 14064205:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 7737666:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 667741:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 14964741:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 23684360:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 3059113:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 15336043:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 30363650:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 638, Negative: 199999362 Condition exists (0:r1=1 /\ 0:r4=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=2dd158f1ef0b66595a56ff21c6e00a13 Observation X01 Sometimes 638 199999362 Time X01 404.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 18105272:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 11451923:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 548332:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 16176484:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 17158698:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 2252728:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 15223902:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 29672936:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 33175026:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 2798303:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 15920747:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 23371428:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 3623137:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 8458376:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 2062708:>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 419.04 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 52525333:>0:r1=0; 0:r4=0; y=1; 19205996:>0:r1=1; 0:r4=0; y=1; 996238:>0:r1=0; 0:r4=1; y=1; 40987871:>0:r1=1; 0:r4=1; y=1; 19943498:>0:r1=0; 0:r4=0; y=2; 13 :>0:r1=1; 0:r4=0; y=2; 45248853:>0:r1=0; 0:r4=1; y=2; 21092198:>0:r1=1; 0:r4=1; y=2; Ok Witnesses Positive: 13, Negative: 199999987 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=979eb45568765c8b5bb24cb8beb2a694 Observation X03 Sometimes 13 199999987 Time X03 192.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X04.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X04 "Rfe DpAddrdR Fre LwSyncdWW Wse LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | lwsync | lwsync ; | li r3,1 | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X04 Allowed Histogram (15 states) 18068561:>0:r1=0; 0:r4=0; y=1; z=1; 9424480:>0:r1=1; 0:r4=0; y=1; z=1; 375553:>0:r1=0; 0:r4=1; y=1; z=1; 19698776:>0:r1=1; 0:r4=1; y=1; z=1; 15169605:>0:r1=0; 0:r4=0; y=2; z=1; 1762368:>0:r1=1; 0:r4=0; y=2; z=1; 14018867:>0:r1=0; 0:r4=1; y=2; z=1; 29072803:>0:r1=1; 0:r4=1; y=2; z=1; 33536658:>0:r1=0; 0:r4=0; y=1; z=2; 1809494:>0:r1=1; 0:r4=0; y=1; z=2; 10265467:>0:r1=0; 0:r4=1; y=1; z=2; 20893464:>0:r1=1; 0:r4=1; y=1; z=2; 4629339:>0:r1=0; 0:r4=0; y=2; z=2; 12105486:>0:r1=0; 0:r4=1; y=2; z=2; 9169079:>0:r1=1; 0:r4=1; y=2; z=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) is NOT validated Hash=bbe86be3ef3c2131f0d4681c0ccd31a8 Observation X04 Never 0 200000000 Time X04 453.66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X05.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X05 "Rfe DpAddrdR Fre LwSyncdWW Wse SyncdWR Fre LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,2 | li r1,1 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | lwsync | sync | lwsync ; | li r3,1 | lwz r3,0(r4) | li r3,1 ; | stw r3,0(r4) | | stw r3,0(r4) ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: xor 10,28,28 _litmus_P0_2_: lwzx 30,10,9 _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: sync _litmus_P2_3_: lwz 3,0(9) Test X05 Allowed Histogram (15 states) 33253388:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 87111 :>0:r1=1; 0:r4=0; 2:r3=0; y=1; 12816424:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 6149996:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 10417709:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 8791664:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 378446:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 23504337:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 325793:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 7326978:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 5970398:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 28565353:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 7615331:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 21998237:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 32798835:>0:r1=1; 0:r4=1; 2:r3=1; y=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0 /\ 2:r3=0) is NOT validated Hash=2f45a04baa1582caaf7bebb0f6429fad Observation X05 Never 0 200000000 Time X05 477.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14786585:>0:r1=0; 0:r4=0; y=1; z=1; 9429321:>0:r1=1; 0:r4=0; y=1; z=1; 2654714:>0:r1=0; 0:r4=1; y=1; z=1; 28425173:>0:r1=1; 0:r4=1; y=1; z=1; 24623289:>0:r1=0; 0:r4=0; y=2; z=1; 4949277:>0:r1=1; 0:r4=0; y=2; z=1; 21631378:>0:r1=0; 0:r4=1; y=2; z=1; 34116195:>0:r1=1; 0:r4=1; y=2; z=1; 33618252:>0:r1=0; 0:r4=0; y=1; z=2; 72323 :>0:r1=1; 0:r4=0; y=1; z=2; 6654153:>0:r1=0; 0:r4=1; y=1; z=2; 6220724:>0:r1=1; 0:r4=1; y=1; z=2; 235415:>0:r1=0; 0:r4=0; y=2; z=2; 5252265:>0:r1=0; 0:r4=1; y=2; z=2; 7330936:>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 466.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 21158439:>0:r1=0; 0:r4=0; 1:r3=0; 39044250:>0:r1=0; 0:r4=1; 1:r3=0; 6625585:>0:r1=1; 0:r4=1; 1:r3=0; 50364793:>0:r1=0; 0:r4=0; 1:r3=1; 26249003:>0:r1=1; 0:r4=0; 1:r3=1; 7582392:>0:r1=0; 0:r4=1; 1:r3=1; 48975538:>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 218.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 10099094:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 238227:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 16982434:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 22962556:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 22800153:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 17003381:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 288243:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 15894467:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 5992100:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 9035776:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 922979:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 36074287:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 5112129:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 18533170:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 18061004:>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 474.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 65327 :>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 1998660:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 1339274:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 33155159:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 69720 :>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 14762438:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 17061066:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 20697021:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 1291188:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 24027882:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 23857013:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 20417242:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 16952049:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 299523:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 24006438:>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 412.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 16190014:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 727635:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 24000826:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 23687346:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 24057868:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 22540320:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 2821543:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 22211718:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 220582:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 2023754:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 245594:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 33457001:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 129060:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 18627417:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 9059322:>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 494.55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X11.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X11 "Rfe DpAddrdR Fre SyncdWW Wse LwSyncdWW" {0:r2=z; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z;} P0 | P1 | P2 ; lwz r1,0(r2) | li r1,1 | li r1,2 ; xor r3,r1,r1 | stw r1,0(r2) | stw r1,0(r2) ; lwzx r4,r3,r5 | sync | lwsync ; | li r3,1 | li r3,1 ; | stw r3,0(r4) | stw r3,0(r4) ; exists (y=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: lwz 27,0(11) _litmus_P0_1_: xor 10,27,27 _litmus_P0_2_: lwzx 28,10,9 _litmus_P2_0_: li 30,2 _litmus_P2_1_: stw 30,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X11 Allowed Histogram (8 states) 55054525:>0:r1=0; 0:r4=0; y=1; 24320694:>0:r1=1; 0:r4=0; y=1; 8811060:>0:r1=0; 0:r4=1; y=1; 47935296:>0:r1=1; 0:r4=1; y=1; 18398414:>0:r1=0; 0:r4=0; y=2; 1 :>0:r1=1; 0:r4=0; y=2; 41297699:>0:r1=0; 0:r4=1; y=2; 4182311:>0:r1=1; 0:r4=1; y=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (y=2 /\ 0:r1=1 /\ 0:r4=0) is validated Hash=2e151daaab42138b8c478ba081d896ed Observation X11 Sometimes 1 199999999 Time X11 206.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 22911442:>0:r1=0; 0:r4=0; y=1; z=1; 18042329:>0:r1=1; 0:r4=0; y=1; z=1; 3462894:>0:r1=0; 0:r4=1; y=1; z=1; 20990410:>0:r1=1; 0:r4=1; y=1; z=1; 10650559:>0:r1=0; 0:r4=0; y=2; z=1; 168119:>0:r1=1; 0:r4=0; y=2; z=1; 14823946:>0:r1=0; 0:r4=1; y=2; z=1; 17683597:>0:r1=1; 0:r4=1; y=2; z=1; 35214962:>0:r1=0; 0:r4=0; y=1; z=2; 3230666:>0:r1=1; 0:r4=0; y=1; z=2; 15022049:>0:r1=0; 0:r4=1; y=1; z=2; 24881643:>0:r1=1; 0:r4=1; y=1; z=2; 4462564:>0:r1=0; 0:r4=0; y=2; z=2; 7316159:>0:r1=0; 0:r4=1; y=2; z=2; 1138661:>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 474.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33291771:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 105618:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 18543807:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 12123200:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 20467692:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 22176176:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 3643954:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 23628212:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 241156:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 2995180:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 957528:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 19434272:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 1987555:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 21288168:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 19115711:>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 479.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 23135667:>0:r1=0; 0:r4=0; y=1; z=1; 22464715:>0:r1=1; 0:r4=0; y=1; z=1; 6560835:>0:r1=0; 0:r4=1; y=1; z=1; 29560913:>0:r1=1; 0:r4=1; y=1; z=1; 15846405:>0:r1=0; 0:r4=0; y=2; z=1; 539312:>0:r1=1; 0:r4=0; y=2; z=1; 20273344:>0:r1=0; 0:r4=1; y=2; z=1; 18833312:>0:r1=1; 0:r4=1; y=2; z=1; 33375177:>0:r1=0; 0:r4=0; y=1; z=2; 116579:>0:r1=1; 0:r4=0; y=1; z=2; 13895885:>0:r1=0; 0:r4=1; y=1; z=2; 13745975:>0:r1=1; 0:r4=1; y=1; z=2; 153554:>0:r1=0; 0:r4=0; y=2; z=2; 1253565:>0:r1=0; 0:r4=1; y=2; z=2; 244762:>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 465.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33547139:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 4017557:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 11931720:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 22419065:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 3105001:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 4 :>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=0; 10225456:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 4996755:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 14222782:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 8045829:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 567810:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 14462747:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 23910758:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 3014473:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 15345125:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 30187779:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=1; Ok Witnesses Positive: 4, Negative: 199999996 Condition exists (0:r1=1 /\ 0:r3=0 /\ 2:r1=1 /\ 2:r3=0) is validated Hash=a488ac47b1a88d9c3f30dcee477424e5 Observation X15 Sometimes 4 199999996 Time X15 405.22 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 52882831:>0:r1=0; 0:r3=0; y=1; 19270353:>0:r1=1; 0:r3=0; y=1; 1060154:>0:r1=0; 0:r3=1; y=1; 40838739:>0:r1=1; 0:r3=1; y=1; 19730912:>0:r1=0; 0:r3=0; y=2; 17 :>0:r1=1; 0:r3=0; y=2; 44971130:>0:r1=0; 0:r3=1; y=2; 21245864:>0:r1=1; 0:r3=1; y=2; Ok Witnesses Positive: 17, Negative: 199999983 Condition exists (y=2 /\ 0:r1=1 /\ 0:r3=0) is validated Hash=7cfc2b26a1cbcdd15d0fab061a637ce4 Observation X16 Sometimes 17 199999983 Time X16 194.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 14301920:>0:r1=0; 0:r3=0; y=1; z=1; 7700663:>0:r1=1; 0:r3=0; y=1; z=1; 392452:>0:r1=0; 0:r3=1; y=1; z=1; 18477592:>0:r1=1; 0:r3=1; y=1; z=1; 21243546:>0:r1=0; 0:r3=0; y=2; z=1; 3580443:>0:r1=1; 0:r3=0; y=2; z=1; 16036412:>0:r1=0; 0:r3=1; y=2; z=1; 30321367:>0:r1=1; 0:r3=1; y=2; z=1; 33407976:>0:r1=0; 0:r3=0; y=1; z=2; 1826729:>0:r1=1; 0:r3=0; y=1; z=2; 10649929:>0:r1=0; 0:r3=1; y=1; z=2; 20435350:>0:r1=1; 0:r3=1; y=1; z=2; 2473918:>0:r1=0; 0:r3=0; y=2; z=2; 10040828:>0:r1=0; 0:r3=1; y=2; z=2; 9110875:>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 449.73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33123533:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 77230 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 13407110:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 5337964:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 9250849:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 8063933:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 360619:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 22875643:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 336640:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 7815705:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 5256891:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 30462057:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 8678923:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 22766855:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 32186048:>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 464.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11468379:>0:r1=0; 0:r3=0; y=1; z=1; 7377655:>0:r1=1; 0:r3=0; y=1; z=1; 2680212:>0:r1=0; 0:r3=1; y=1; z=1; 27124273:>0:r1=1; 0:r3=1; y=1; z=1; 28625547:>0:r1=0; 0:r3=0; y=2; z=1; 6890839:>0:r1=1; 0:r3=0; y=2; z=1; 22013691:>0:r1=0; 0:r3=1; y=2; z=1; 35980348:>0:r1=1; 0:r3=1; y=2; z=1; 33130223:>0:r1=0; 0:r3=0; y=1; z=2; 53040 :>0:r1=1; 0:r3=0; y=1; z=2; 6688719:>0:r1=0; 0:r3=1; y=1; z=2; 6095196:>0:r1=1; 0:r3=1; y=1; z=2; 188111:>0:r1=0; 0:r3=0; y=2; z=2; 4524524:>0:r1=0; 0:r3=1; y=2; z=2; 7159243:>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 439.12 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 21271953:>0:r1=0; 0:r3=0; 1:r3=0; 39053289:>0:r1=0; 0:r3=1; 1:r3=0; 6589935:>0:r1=1; 0:r3=1; 1:r3=0; 50372605:>0:r1=0; 0:r3=0; 1:r3=1; 26658274:>0:r1=1; 0:r3=0; 1:r3=1; 7528861:>0:r1=0; 0:r3=1; 1:r3=1; 48525083:>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 228.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X21.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X21 "Rfe DpCtrlIsyncdR Fre SyncdWR Fre LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; lwz r1,0(r2) | li r1,1 | li r1,1 | li r1,2 ; cmpw r1,r1 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; beq LC00 | sync | lwsync | lwsync ; LC00: | lwz r3,0(r4) | li r3,1 | li r3,1 ; isync | | stw r3,0(r4) | stw r3,0(r4) ; lwz r3,0(r4) | | | ; exists (z=2 /\ 0:r1=1 /\ 0:r3=0 /\ 1:r3=0) Generated assembler _litmus_P1_0_: li 30,1 _litmus_P1_1_: stw 30,0(11) _litmus_P1_2_: sync _litmus_P1_3_: lwz 3,0(9) _litmus_P0_0_: lwz 28,0(11) _litmus_P0_1_: cmpw 28,28 _litmus_P0_2_: beq LitLC00 _litmus_P0_3_: LitLC00: _litmus_P0_4_: isync _litmus_P0_5_: lwz 30,0(9) _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,1 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X21 Allowed Histogram (15 states) 12983026:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 249837:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 19889719:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 22668003:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 22535921:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 17561458:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 258619:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 15809011:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 3169815:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 6247714:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 812013:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 36235371:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 5288189:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 18583762:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 17707542:>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 484.06 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 65929 :>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 2229616:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 1135067:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 33478687:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 67345 :>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 15899328:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 15574982:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 20915869:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 1248613:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 23994731:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 24211721:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 20149163:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 16730403:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 299294:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 23999252:>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 413.24 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 16007015:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 678381:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 23896142:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 23037250:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 24615561:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 23366819:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 2710179:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 22290420:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 202037:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 1900299:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 245518:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 33402341:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 124258:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 18365825:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 9157955:>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 478.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 (7 states) 55187396:>0:r1=0; 0:r3=0; y=1; 24577056:>0:r1=1; 0:r3=0; y=1; 9173690:>0:r1=0; 0:r3=1; y=1; 47306916:>0:r1=1; 0:r3=1; y=1; 18459150:>0:r1=0; 0:r3=0; y=2; 41263328:>0:r1=0; 0:r3=1; y=2; 4032464:>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=1a78bce42911eadebdb22805402de8eb Observation X24 Never 0 200000000 Time X24 196.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 22849443:>0:r1=0; 0:r3=0; y=1; z=1; 18678479:>0:r1=1; 0:r3=0; y=1; z=1; 3133465:>0:r1=0; 0:r3=1; y=1; z=1; 19591950:>0:r1=1; 0:r3=1; y=1; z=1; 12584869:>0:r1=0; 0:r3=0; y=2; z=1; 199664:>0:r1=1; 0:r3=0; y=2; z=1; 17432404:>0:r1=0; 0:r3=1; y=2; z=1; 18142869:>0:r1=1; 0:r3=1; y=2; z=1; 34948489:>0:r1=0; 0:r3=0; y=1; z=2; 3046582:>0:r1=1; 0:r3=0; y=1; z=2; 15247449:>0:r1=0; 0:r3=1; y=1; z=2; 24966572:>0:r1=1; 0:r3=1; y=1; z=2; 2773366:>0:r1=0; 0:r3=0; y=2; z=2; 5166551:>0:r1=0; 0:r3=1; y=2; z=2; 1237848:>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 470.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33048555:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 93748 :>0:r1=1; 0:r3=0; 2:r3=0; y=1; 20041198:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 9926805:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 19542847:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 22362783:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 3211186:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 22231980:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 198709:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 3698007:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 904455:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 20677362:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 2451937:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 21944607:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 19665821:>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 463.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 20631406:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 17085220:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 10990562:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 1198647:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 611905:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 15818201:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 16763773:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 29665293:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 32651114:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 2510805:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 2944898:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 15822668:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 7313955:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 23442332:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 2549221:>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 423.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 10035513:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 26366981:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 4307336:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 6476620:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 211428:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 12860866:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 16325646:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 38114741:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 34928427:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 3127198:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 287159:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 5 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 13157768:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 9697577:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 18358033:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 5744702:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 5, Negative: 199999995 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=4adca431a2784b4aa9df91b1fc3b1666 Observation X28 Sometimes 5 199999995 Time X28 417.84 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/X29.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC X29 "Rfe LwSyncdRW Wse LwSyncdWW Rfe DpCtrlIsyncdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | lwz r1,0(r2) ; stw r1,0(r2) | lwsync | stw r1,0(r2) | cmpw r1,r1 ; | li r3,1 | lwsync | beq LC00 ; | stw r3,0(r4) | li r3,1 | LC00: ; | | stw r3,0(r4) | isync ; | | | lwz r3,0(r4) ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: lwsync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: lwz 28,0(11) _litmus_P3_1_: cmpw 28,28 _litmus_P3_2_: beq LitLC00 _litmus_P3_3_: LitLC00: _litmus_P3_4_: isync _litmus_P3_5_: lwz 30,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test X29 Allowed Histogram (15 states) 9831986:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 27146341:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 4327273:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 6656195:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 220486:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 13377803:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 16385023:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 38874207:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 34982948:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 2137716:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 304260:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 12220072:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 8119898:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 19195613:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 6220179:>1:r1=1; 3:r1=1; 3:r3=1; x=2; No Witnesses Positive: 0, Negative: 200000000 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is NOT validated Hash=cd58719fd03bc8a841de06004867cb05 Observation X29 Never 0 200000000 Time X29 415.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 20500584:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 16852516:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 10779299:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 1168249:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 614091:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 15566335:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 16952051:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 29853385:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 32808300:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 2608682:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 2807806:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 15481100:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 7467572:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 23989823:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 2550207:>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 410.00 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 20578402:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 16971460:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 10881917:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 1162666:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 568510:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 15539898:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 16791517:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 29730649:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 32852767:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 2598307:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 2923615:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 15576550:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 7563756:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 23737096:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 2522890:>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 418.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 33010281:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 344499:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 5500215:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 30499906:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 32358 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 2 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=0; 3093986:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 8819052:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 12273211:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 5473416:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 1646297:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 17756836:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 6303525:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 6947164:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 25116700:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 43182552:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=1; Ok Witnesses Positive: 2, Negative: 199999998 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=abdf662fb230128532b66df78e4a75f1 Observation X32 Sometimes 2 199999998 Time X32 406.51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32959803:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 306843:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 5512611:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 30545833:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 29104 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 2 :>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=0; 3103089:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 8807799:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 12221461:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 5572275:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 1617692:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 17978986:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 6298382:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 6821470:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 25325272:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 42899378:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=1; Ok Witnesses Positive: 2, Negative: 199999998 Condition exists (1:r1=1 /\ 1:r3=0 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=c86889a7cdc1c89457a71c414046d8c0 Observation X33 Sometimes 2 199999998 Time X33 404.55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7877787:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 30124712:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 4499846:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 7131266:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 1572607:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 17213279:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 25016061:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 41539811:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 33868138:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 404204:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 106545:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 2 :>1:r1=1; 3:r1=1; 3:r4=0; x=2; 13107076:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 6846209:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 5062907:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 5629550:>1:r1=1; 3:r1=1; 3:r4=1; x=2; Ok Witnesses Positive: 2, Negative: 199999998 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r4=0) is validated Hash=8db91522dc421fe43a7baf7aff0de837 Observation X34 Sometimes 2 199999998 Time X34 416.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 7861419:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 30290794:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 4509544:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 7268946:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 1624427:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 16879481:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 25343313:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 42356781:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 33677723:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 303724:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 122129:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 1 :>1:r1=1; 3:r1=1; 3:r3=0; x=2; 12163336:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 6107344:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 5375019:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 6116019:>1:r1=1; 3:r1=1; 3:r3=1; x=2; Ok Witnesses Positive: 1, Negative: 199999999 Condition exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) is validated Hash=00744a65cf189719eb1309a79c27a2ca Observation X35 Sometimes 1 199999999 Time X35 410.46 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 31989489:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=0; 1590871:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=0; 1124720:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=0; 28607402:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=0; 1608553:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=0; 2144631:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=0; 9447006:>0:r1=1; 0:r4=1; 2:r1=1; 2:r4=0; 1094098:>0:r1=0; 0:r4=0; 2:r1=0; 2:r4=1; 2079811:>0:r1=1; 0:r4=0; 2:r1=0; 2:r4=1; 399156:>0:r1=0; 0:r4=1; 2:r1=0; 2:r4=1; 14668306:>0:r1=1; 0:r4=1; 2:r1=0; 2:r4=1; 28460612:>0:r1=0; 0:r4=0; 2:r1=1; 2:r4=1; 9482480:>0:r1=1; 0:r4=0; 2:r1=1; 2:r4=1; 14218887:>0:r1=0; 0:r4=1; 2:r1=1; 2:r4=1; 53083978:>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 409.18 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32178950:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=0; 1690910:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=0; 1289925:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=0; 28855924:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=0; 1818022:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=0; 2427278:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=0; 9679927:>0:r1=1; 0:r4=1; 2:r1=1; 2:r3=0; 947611:>0:r1=0; 0:r4=0; 2:r1=0; 2:r3=1; 2118877:>0:r1=1; 0:r4=0; 2:r1=0; 2:r3=1; 356553:>0:r1=0; 0:r4=1; 2:r1=0; 2:r3=1; 14749938:>0:r1=1; 0:r4=1; 2:r1=0; 2:r3=1; 28247281:>0:r1=0; 0:r4=0; 2:r1=1; 2:r3=1; 9396613:>0:r1=1; 0:r4=0; 2:r1=1; 2:r3=1; 13837298:>0:r1=0; 0:r4=1; 2:r1=1; 2:r3=1; 52404893:>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 415.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9861107:>0:r1=0; 0:r4=0; 2:r1=0; z=1; 6786613:>0:r1=1; 0:r4=0; 2:r1=0; z=1; 623651:>0:r1=0; 0:r4=1; 2:r1=0; z=1; 30351733:>0:r1=1; 0:r4=1; 2:r1=0; z=1; 22014525:>0:r1=0; 0:r4=0; 2:r1=1; z=1; 6005543:>0:r1=1; 0:r4=0; 2:r1=1; z=1; 15722794:>0:r1=0; 0:r4=1; 2:r1=1; z=1; 47624967:>0:r1=1; 0:r4=1; 2:r1=1; z=1; 31787376:>0:r1=0; 0:r4=0; 2:r1=0; z=2; 278852:>0:r1=1; 0:r4=0; 2:r1=0; z=2; 1169301:>0:r1=0; 0:r4=1; 2:r1=0; z=2; 16260922:>0:r1=1; 0:r4=1; 2:r1=0; z=2; 227994:>0:r1=0; 0:r4=0; 2:r1=1; z=2; 805878:>0:r1=0; 0:r4=1; 2:r1=1; z=2; 10478744:>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 471.66 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 41281385:>0:r1=0; 0:r4=0; y=1; 18227067:>0:r1=1; 0:r4=0; y=1; 365361:>0:r1=0; 0:r4=1; y=1; 50835571:>0:r1=1; 0:r4=1; y=1; 20217394:>0:r1=0; 0:r4=0; y=2; 24650426:>0:r1=0; 0:r4=1; y=2; 44422796:>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 253.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 12188992:>0:r1=0; 0:r4=0; y=1; z=1; 7297669:>0:r1=1; 0:r4=0; y=1; z=1; 962920:>0:r1=0; 0:r4=1; y=1; z=1; 23442615:>0:r1=1; 0:r4=1; y=1; z=1; 18602674:>0:r1=0; 0:r4=0; y=2; z=1; 3879619:>0:r1=1; 0:r4=0; y=2; z=1; 12294102:>0:r1=0; 0:r4=1; y=2; z=1; 36226121:>0:r1=1; 0:r4=1; y=2; z=1; 26772765:>0:r1=0; 0:r4=0; y=1; z=2; 1658285:>0:r1=1; 0:r4=0; y=1; z=2; 3435794:>0:r1=0; 0:r4=1; y=1; z=2; 32602216:>0:r1=1; 0:r4=1; y=1; z=2; 1580338:>0:r1=0; 0:r4=0; y=2; z=2; 4361253:>0:r1=0; 0:r4=1; y=2; z=2; 14694637:>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 477.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30133588:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 165343:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 1604224:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 19405171:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 8572170:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 6416175:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 619347:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 28659728:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 233416:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 796829:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 11390668:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 23313330:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 7813365:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 16248397:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 44628249:>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 464.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9466047:>0:r1=0; 0:r4=0; y=1; z=1; 6412076:>0:r1=1; 0:r4=0; y=1; z=1; 708010:>0:r1=0; 0:r4=1; y=1; z=1; 37315136:>0:r1=1; 0:r4=1; y=1; z=1; 23265122:>0:r1=0; 0:r4=0; y=2; z=1; 6332436:>0:r1=1; 0:r4=0; y=2; z=1; 15542706:>0:r1=0; 0:r4=1; y=2; z=1; 44037113:>0:r1=1; 0:r4=1; y=2; z=1; 28680397:>0:r1=0; 0:r4=0; y=1; z=2; 162816:>0:r1=1; 0:r4=0; y=1; z=2; 1742701:>0:r1=0; 0:r4=1; y=1; z=2; 13725876:>0:r1=1; 0:r4=1; y=1; z=2; 179484:>0:r1=0; 0:r4=0; y=2; z=2; 699311:>0:r1=0; 0:r4=1; y=2; z=2; 11730769:>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 474.17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 18268250:>0:r1=0; 0:r4=0; 1:r3=0; 24120131:>0:r1=0; 0:r4=1; 1:r3=0; 23776024:>0:r1=1; 0:r4=1; 1:r3=0; 44982478:>0:r1=0; 0:r4=0; 1:r3=1; 23046230:>0:r1=1; 0:r4=0; 1:r3=1; 914169:>0:r1=0; 0:r4=1; 1:r3=1; 64892718:>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 191.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 12931807:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 174706:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 14908435:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 27014436:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 17655568:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 17352997:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 883942:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 23514872:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 1941715:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 3970404:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 2608510:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 28276468:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 4962070:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 3797839:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 40006231:>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 505.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 139440:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=0; 410027:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=0; 2515825:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=0; 29805185:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=0; 231384:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=0; 1528581:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=0; 32194182:>0:r1=1; 0:r4=1; 1:r3=1; 2:r3=0; 15366365:>0:r1=0; 0:r4=0; 1:r3=0; 2:r3=1; 2875583:>0:r1=1; 0:r4=0; 1:r3=0; 2:r3=1; 18702598:>0:r1=0; 0:r4=1; 1:r3=0; 2:r3=1; 29769614:>0:r1=1; 0:r4=1; 1:r3=0; 2:r3=1; 17640985:>0:r1=0; 0:r4=0; 1:r3=1; 2:r3=1; 16487558:>0:r1=1; 0:r4=0; 1:r3=1; 2:r3=1; 719680:>0:r1=0; 0:r4=1; 1:r3=1; 2:r3=1; 31612993:>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 420.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15130828:>0:r1=0; 0:r4=0; 1:r3=0; z=1; 231317:>0:r1=1; 0:r4=0; 1:r3=0; z=1; 18376142:>0:r1=0; 0:r4=1; 1:r3=0; z=1; 29185114:>0:r1=1; 0:r4=1; 1:r3=0; z=1; 18846209:>0:r1=0; 0:r4=0; 1:r3=1; z=1; 22185661:>0:r1=1; 0:r4=0; 1:r3=1; z=1; 561970:>0:r1=0; 0:r4=1; 1:r3=1; z=1; 35040066:>0:r1=1; 0:r4=1; 1:r3=1; z=1; 146320:>0:r1=0; 0:r4=0; 1:r3=0; z=2; 412994:>0:r1=0; 0:r4=1; 1:r3=0; z=2; 1302440:>0:r1=1; 0:r4=1; 1:r3=0; z=2; 28879230:>0:r1=0; 0:r4=0; 1:r3=1; z=2; 351743:>0:r1=1; 0:r4=0; 1:r3=1; z=2; 1622415:>0:r1=0; 0:r4=1; 1:r3=1; z=2; 27727551:>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 463.24 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 43926836:>0:r1=0; 0:r4=0; y=1; 21446755:>0:r1=1; 0:r4=0; y=1; 891699:>0:r1=0; 0:r4=1; y=1; 67577953:>0:r1=1; 0:r4=1; y=1; 18226429:>0:r1=0; 0:r4=0; y=2; 21849011:>0:r1=0; 0:r4=1; y=2; 26081317:>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 255.94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y12.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y12 "Rf*e DpAddrdR Fre SyncdWW Wse LwSyncdWW Wse LwSyncdWW" {0:r2=a; 0:r5=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,1 | li r1,2 | li r1,2 ; lwarx r1,r0,r2 | stw r1,0(r2) | stw r1,0(r2) | stw r1,0(r2) ; xor r3,r1,r1 | sync | lwsync | lwsync ; lwzx r4,r3,r5 | li r3,1 | li r3,1 | li r3,1 ; stwcx. r1,r0,r2 | stw r3,0(r4) | stw r3,0(r4) | stw r3,0(r4) ; bne DIY00 | | | ; exists (y=2 /\ z=2 /\ 0:r1=1 /\ 0:r4=0) Generated assembler _litmus_P1_0_: li 4,1 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: sync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 28,0,11 _litmus_P0_2_: xor 10,28,28 _litmus_P0_3_: lwzx 30,10,9 _litmus_P0_4_: stwcx. 28,0,11 _litmus_P0_5_: bne LitDIY00 _litmus_P3_0_: li 4,2 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y12 Allowed Histogram (15 states) 17643340:>0:r1=0; 0:r4=0; y=1; z=1; 16912721:>0:r1=1; 0:r4=0; y=1; z=1; 2051643:>0:r1=0; 0:r4=1; y=1; z=1; 28781881:>0:r1=1; 0:r4=1; y=1; z=1; 12671488:>0:r1=0; 0:r4=0; y=2; z=1; 119716:>0:r1=1; 0:r4=0; y=2; z=1; 12549785:>0:r1=0; 0:r4=1; y=2; z=1; 23833094:>0:r1=1; 0:r4=1; y=2; z=1; 28346509:>0:r1=0; 0:r4=0; y=1; z=2; 3225926:>0:r1=1; 0:r4=0; y=1; z=2; 3908549:>0:r1=0; 0:r4=1; y=1; z=2; 42311062:>0:r1=1; 0:r4=1; y=1; z=2; 1588949:>0:r1=0; 0:r4=0; y=2; z=2; 3890491:>0:r1=0; 0:r4=1; y=2; z=2; 2164846:>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 479.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30441352:>0:r1=0; 0:r4=0; 2:r3=0; y=1; 209440:>0:r1=1; 0:r4=0; 2:r3=0; y=1; 1654796:>0:r1=0; 0:r4=1; 2:r3=0; y=1; 31326720:>0:r1=1; 0:r4=1; 2:r3=0; y=1; 17714129:>0:r1=0; 0:r4=0; 2:r3=1; y=1; 18178095:>0:r1=1; 0:r4=0; 2:r3=1; y=1; 2391079:>0:r1=0; 0:r4=1; 2:r3=1; y=1; 33088673:>0:r1=1; 0:r4=1; 2:r3=1; y=1; 151474:>0:r1=0; 0:r4=0; 2:r3=0; y=2; 421722:>0:r1=0; 0:r4=1; 2:r3=0; y=2; 2929387:>0:r1=1; 0:r4=1; 2:r3=0; y=2; 14771906:>0:r1=0; 0:r4=0; 2:r3=1; y=2; 3510648:>0:r1=1; 0:r4=0; 2:r3=1; y=2; 16549160:>0:r1=0; 0:r4=1; 2:r3=1; y=2; 26661419:>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 459.14 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 17734802:>0:r1=0; 0:r4=0; y=1; z=1; 19348416:>0:r1=1; 0:r4=0; y=1; z=1; 2069799:>0:r1=0; 0:r4=1; y=1; z=1; 41080157:>0:r1=1; 0:r4=1; y=1; z=1; 15088210:>0:r1=0; 0:r4=0; y=2; z=1; 201795:>0:r1=1; 0:r4=0; y=2; z=1; 15440950:>0:r1=0; 0:r4=1; y=2; z=1; 27576267:>0:r1=1; 0:r4=1; y=2; z=1; 29206571:>0:r1=0; 0:r4=0; y=1; z=2; 330122:>0:r1=1; 0:r4=0; y=1; z=2; 1893292:>0:r1=0; 0:r4=1; y=1; z=2; 28550695:>0:r1=1; 0:r4=1; y=1; z=2; 151209:>0:r1=0; 0:r4=0; y=2; z=2; 413185:>0:r1=0; 0:r4=1; y=2; z=2; 914530:>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 485.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 32368261:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=0; 1866284:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=0; 1361407:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=0; 28564071:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=0; 2563336:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=0; 2944342:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=0; 9634082:>0:r1=1; 0:r3=1; 2:r1=1; 2:r3=0; 1076877:>0:r1=0; 0:r3=0; 2:r1=0; 2:r3=1; 2463539:>0:r1=1; 0:r3=0; 2:r1=0; 2:r3=1; 338569:>0:r1=0; 0:r3=1; 2:r1=0; 2:r3=1; 14823669:>0:r1=1; 0:r3=1; 2:r1=0; 2:r3=1; 28182643:>0:r1=0; 0:r3=0; 2:r1=1; 2:r3=1; 9815691:>0:r1=1; 0:r3=0; 2:r1=1; 2:r3=1; 13759142:>0:r1=0; 0:r3=1; 2:r1=1; 2:r3=1; 50238087:>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 410.15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 41688903:>0:r1=0; 0:r3=0; y=1; 18625358:>0:r1=1; 0:r3=0; y=1; 629936:>0:r1=0; 0:r3=1; y=1; 49673679:>0:r1=1; 0:r3=1; y=1; 20765733:>0:r1=0; 0:r3=0; y=2; 25531787:>0:r1=0; 0:r3=1; y=2; 43084604:>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 258.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13656416:>0:r1=0; 0:r3=0; y=1; z=1; 8400511:>0:r1=1; 0:r3=0; y=1; z=1; 931463:>0:r1=0; 0:r3=1; y=1; z=1; 24415773:>0:r1=1; 0:r3=1; y=1; z=1; 17904847:>0:r1=0; 0:r3=0; y=2; z=1; 2878663:>0:r1=1; 0:r3=0; y=2; z=1; 13679841:>0:r1=0; 0:r3=1; y=2; z=1; 34418950:>0:r1=1; 0:r3=1; y=2; z=1; 26326424:>0:r1=0; 0:r3=0; y=1; z=2; 1652698:>0:r1=1; 0:r3=0; y=1; z=2; 3689941:>0:r1=0; 0:r3=1; y=1; z=2; 32687507:>0:r1=1; 0:r3=1; y=1; z=2; 1373809:>0:r1=0; 0:r3=0; y=2; z=2; 3138325:>0:r1=0; 0:r3=1; y=2; z=2; 14844832:>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 494.70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30537397:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 182621:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 1414710:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 19357351:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 10377645:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 6740813:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 531506:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 29411106:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 235303:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 734417:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 12040603:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 21949082:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 7525880:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 15962826:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 42998740:>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 465.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 11304821:>0:r1=0; 0:r3=0; y=1; z=1; 8123444:>0:r1=1; 0:r3=0; y=1; z=1; 692369:>0:r1=0; 0:r3=1; y=1; z=1; 38590558:>0:r1=1; 0:r3=1; y=1; z=1; 21488020:>0:r1=0; 0:r3=0; y=2; z=1; 5166811:>0:r1=1; 0:r3=0; y=2; z=1; 15641516:>0:r1=0; 0:r3=1; y=2; z=1; 41305546:>0:r1=1; 0:r3=1; y=2; z=1; 29252230:>0:r1=0; 0:r3=0; y=1; z=2; 155671:>0:r1=1; 0:r3=0; y=1; z=2; 1641560:>0:r1=0; 0:r3=1; y=1; z=2; 13292242:>0:r1=1; 0:r3=1; y=1; z=2; 181956:>0:r1=0; 0:r3=0; y=2; z=2; 726841:>0:r1=0; 0:r3=1; y=2; z=2; 12436415:>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 469.69 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 18699681:>0:r1=0; 0:r3=0; 1:r3=0; 24520653:>0:r1=0; 0:r3=1; 1:r3=0; 22914790:>0:r1=1; 0:r3=1; 1:r3=0; 45548285:>0:r1=0; 0:r3=0; 1:r3=1; 21878074:>0:r1=1; 0:r3=0; 1:r3=1; 1347955:>0:r1=0; 0:r3=1; 1:r3=1; 65090562:>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 193.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 13058289:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 168048:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 15492794:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 26346302:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 18012539:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 17537875:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 930851:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 22907765:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 1962669:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 3902531:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 2542997:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 28138134:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 5115597:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 4143199:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 39740410:>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 487.62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 121909:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=0; 392541:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=0; 2397303:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=0; 30074939:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=0; 242326:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=0; 1238956:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=0; 32274629:>0:r1=1; 0:r3=1; 1:r3=1; 2:r3=0; 15945897:>0:r1=0; 0:r3=0; 1:r3=0; 2:r3=1; 2911066:>0:r1=1; 0:r3=0; 1:r3=0; 2:r3=1; 19283378:>0:r1=0; 0:r3=1; 1:r3=0; 2:r3=1; 28933949:>0:r1=1; 0:r3=1; 1:r3=0; 2:r3=1; 17688165:>0:r1=0; 0:r3=0; 1:r3=1; 2:r3=1; 16967224:>0:r1=1; 0:r3=0; 1:r3=1; 2:r3=1; 715800:>0:r1=0; 0:r3=1; 1:r3=1; 2:r3=1; 30811918:>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 416.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 15365216:>0:r1=0; 0:r3=0; 1:r3=0; z=1; 256857:>0:r1=1; 0:r3=0; 1:r3=0; z=1; 18424175:>0:r1=0; 0:r3=1; 1:r3=0; z=1; 29129991:>0:r1=1; 0:r3=1; 1:r3=0; z=1; 18688571:>0:r1=0; 0:r3=0; 1:r3=1; z=1; 22536142:>0:r1=1; 0:r3=0; 1:r3=1; z=1; 567967:>0:r1=0; 0:r3=1; 1:r3=1; z=1; 34048989:>0:r1=1; 0:r3=1; 1:r3=1; z=1; 140364:>0:r1=0; 0:r3=0; 1:r3=0; z=2; 424557:>0:r1=0; 0:r3=1; 1:r3=0; z=2; 1252149:>0:r1=1; 0:r3=1; 1:r3=0; z=2; 29235251:>0:r1=0; 0:r3=0; 1:r3=1; z=2; 387490:>0:r1=1; 0:r3=0; 1:r3=1; z=2; 1666931:>0:r1=0; 0:r3=1; 1:r3=1; z=2; 27875350:>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 459.77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 44299531:>0:r1=0; 0:r3=0; y=1; 21887378:>0:r1=1; 0:r3=0; y=1; 1394021:>0:r1=0; 0:r3=1; y=1; 66366303:>0:r1=1; 0:r3=1; y=1; 19059446:>0:r1=0; 0:r3=0; y=2; 21633222:>0:r1=0; 0:r3=1; y=2; 25360099:>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 254.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 18079927:>0:r1=0; 0:r3=0; y=1; z=1; 17374187:>0:r1=1; 0:r3=0; y=1; z=1; 2530840:>0:r1=0; 0:r3=1; y=1; z=1; 28648100:>0:r1=1; 0:r3=1; y=1; z=1; 12879822:>0:r1=0; 0:r3=0; y=2; z=1; 117815:>0:r1=1; 0:r3=0; y=2; z=1; 13459820:>0:r1=0; 0:r3=1; y=2; z=1; 22733176:>0:r1=1; 0:r3=1; y=2; z=1; 27826494:>0:r1=0; 0:r3=0; y=1; z=2; 3620030:>0:r1=1; 0:r3=0; y=1; z=2; 4475019:>0:r1=0; 0:r3=1; y=1; z=2; 41985491:>0:r1=1; 0:r3=1; y=1; z=2; 1331002:>0:r1=0; 0:r3=0; y=2; z=2; 2847190:>0:r1=0; 0:r3=1; y=2; z=2; 2091087:>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 477.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30570016:>0:r1=0; 0:r3=0; 2:r3=0; y=1; 306057:>0:r1=1; 0:r3=0; 2:r3=0; y=1; 1682078:>0:r1=0; 0:r3=1; 2:r3=0; y=1; 31558870:>0:r1=1; 0:r3=1; 2:r3=0; y=1; 17820336:>0:r1=0; 0:r3=0; 2:r3=1; y=1; 19589996:>0:r1=1; 0:r3=0; 2:r3=1; y=1; 2429039:>0:r1=0; 0:r3=1; 2:r3=1; y=1; 32660694:>0:r1=1; 0:r3=1; 2:r3=1; y=1; 197702:>0:r1=0; 0:r3=0; 2:r3=0; y=2; 542990:>0:r1=0; 0:r3=1; 2:r3=0; y=2; 2514460:>0:r1=1; 0:r3=1; 2:r3=0; y=2; 15310228:>0:r1=0; 0:r3=0; 2:r3=1; y=2; 2839608:>0:r1=1; 0:r3=0; 2:r3=1; y=2; 16171025:>0:r1=0; 0:r3=1; 2:r3=1; y=2; 25806901:>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 481.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 9217812:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 23638992:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 5508655:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 6834568:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 638750:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 14967140:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 29954818:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 47889773:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 31383077:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 327157:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 334085:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 1256653:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 949380:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 17239535:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 9859605:>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 493.49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8274536:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 23053914:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 4391504:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 7211372:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 378977:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 9033132:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 19689745:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 47221471:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 28068837:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 2119181:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 368789:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 1789374:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 2128768:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 34121223:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 12149177:>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 418.32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8561081:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 23415773:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 4275224:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 7337614:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 507199:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 9272505:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 19299439:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 46859078:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 28129708:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 2180928:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 394750:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 1779465:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 2007853:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 33677189:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 12302194:>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 417.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8766365:>0:r1=0; 2:r1=0; 2:r4=0; x=1; 23434551:>0:r1=1; 2:r1=0; 2:r4=0; x=1; 6088517:>0:r1=0; 2:r1=1; 2:r4=0; x=1; 6774341:>0:r1=1; 2:r1=1; 2:r4=0; x=1; 715800:>0:r1=0; 2:r1=0; 2:r4=1; x=1; 15358610:>0:r1=1; 2:r1=0; 2:r4=1; x=1; 29645046:>0:r1=0; 2:r1=1; 2:r4=1; x=1; 47833861:>0:r1=1; 2:r1=1; 2:r4=1; x=1; 31572831:>0:r1=0; 2:r1=0; 2:r4=0; x=2; 279801:>0:r1=1; 2:r1=0; 2:r4=0; x=2; 290362:>0:r1=0; 2:r1=1; 2:r4=0; x=2; 1392760:>0:r1=0; 2:r1=0; 2:r4=1; x=2; 903551:>0:r1=1; 2:r1=0; 2:r4=1; x=2; 17047043:>0:r1=0; 2:r1=1; 2:r4=1; x=2; 9896561:>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 479.92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y31.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y31 "Rf*e PodRW Wse LwSyncdWW Rf*e DpCtrlIsyncdR Fre LwSyncdWW" {0:r2=a; 0:r4=x; 1:r2=x; 1:r4=y; 2:r2=y; 2:r4=z; 3:r2=z; 3:r4=a;} P0 | P1 | P2 | P3 ; DIY00: | li r1,2 | DIY01: | li r1,1 ; lwarx r1,r0,r2 | stw r1,0(r2) | lwarx r1,r0,r2 | stw r1,0(r2) ; stwcx. r1,r0,r2 | lwsync | cmpw r1,r1 | lwsync ; bne DIY00 | li r3,1 | beq LC02 | li r3,1 ; li r3,1 | stw r3,0(r4) | LC02: | stw r3,0(r4) ; stw r3,0(r4) | | isync | ; | | lwz r3,0(r4) | ; | | stwcx. r1,r0,r2 | ; | | bne DIY01 | ; exists (x=2 /\ 0:r1=1 /\ 2:r1=1 /\ 2:r3=0) Generated assembler _litmus_P1_0_: li 4,2 _litmus_P1_1_: stw 4,0(11) _litmus_P1_2_: lwsync _litmus_P1_3_: li 3,1 _litmus_P1_4_: stw 3,0(9) _litmus_P0_0_: LitDIY00: _litmus_P0_1_: lwarx 3,0,11 _litmus_P0_2_: stwcx. 3,0,11 _litmus_P0_3_: bne LitDIY00 _litmus_P0_4_: li 30,1 _litmus_P0_5_: stw 30,0(9) _litmus_P3_0_: li 4,1 _litmus_P3_1_: stw 4,0(11) _litmus_P3_2_: lwsync _litmus_P3_3_: li 3,1 _litmus_P3_4_: stw 3,0(9) _litmus_P2_0_: LitDIY01: _litmus_P2_1_: lwarx 28,0,11 _litmus_P2_2_: cmpw 28,28 _litmus_P2_3_: beq LitLC02 _litmus_P2_4_: LitLC02: _litmus_P2_5_: isync _litmus_P2_6_: lwz 30,0(9) _litmus_P2_7_: stwcx. 28,0,11 _litmus_P2_8_: bne LitDIY01 Test Y31 Allowed Histogram (15 states) 9013031:>0:r1=0; 2:r1=0; 2:r3=0; x=1; 23694855:>0:r1=1; 2:r1=0; 2:r3=0; x=1; 6217313:>0:r1=0; 2:r1=1; 2:r3=0; x=1; 6997667:>0:r1=1; 2:r1=1; 2:r3=0; x=1; 672219:>0:r1=0; 2:r1=0; 2:r3=1; x=1; 15510855:>0:r1=1; 2:r1=0; 2:r3=1; x=1; 29158334:>0:r1=0; 2:r1=1; 2:r3=1; x=1; 47382291:>0:r1=1; 2:r1=1; 2:r3=1; x=1; 31795606:>0:r1=0; 2:r1=0; 2:r3=0; x=2; 225536:>0:r1=1; 2:r1=0; 2:r3=0; x=2; 252321:>0:r1=0; 2:r1=1; 2:r3=0; x=2; 1146388:>0:r1=0; 2:r1=0; 2:r3=1; x=2; 748469:>0:r1=1; 2:r1=0; 2:r3=1; x=2; 17118810:>0:r1=0; 2:r1=1; 2:r3=1; x=2; 10066305:>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 459.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30563754:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=0; 230336:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=0; 7305314:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=0; 24127522:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=0; 55217 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=0; 1804304:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=0; 9102887:>1:r1=1; 1:r3=1; 3:r1=1; 3:r4=0; 919404:>1:r1=0; 1:r3=0; 3:r1=0; 3:r4=1; 708754:>1:r1=1; 1:r3=0; 3:r1=0; 3:r4=1; 171048:>1:r1=0; 1:r3=1; 3:r1=0; 3:r4=1; 11299870:>1:r1=1; 1:r3=1; 3:r1=0; 3:r4=1; 18352506:>1:r1=0; 1:r3=0; 3:r1=1; 3:r4=1; 11477590:>1:r1=1; 1:r3=0; 3:r1=1; 3:r4=1; 29792548:>1:r1=0; 1:r3=1; 3:r1=1; 3:r4=1; 54088946:>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 412.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 30864679:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=0; 204975:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=0; 7440644:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=0; 24473270:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=0; 48984 :>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=0; 1692449:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=0; 9184631:>1:r1=1; 1:r3=1; 3:r1=1; 3:r3=0; 748431:>1:r1=0; 1:r3=0; 3:r1=0; 3:r3=1; 674528:>1:r1=1; 1:r3=0; 3:r1=0; 3:r3=1; 220895:>1:r1=0; 1:r3=1; 3:r1=0; 3:r3=1; 11192748:>1:r1=1; 1:r3=1; 3:r1=0; 3:r3=1; 18395391:>1:r1=0; 1:r3=0; 3:r1=1; 3:r3=1; 11585973:>1:r1=1; 1:r3=0; 3:r1=1; 3:r3=1; 29660040:>1:r1=0; 1:r3=1; 3:r1=1; 3:r3=1; 53612362:>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 408.25 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) 8828997:>1:r1=0; 3:r1=0; 3:r4=0; x=1; 23792501:>1:r1=1; 3:r1=0; 3:r4=0; x=1; 3311499:>1:r1=0; 3:r1=1; 3:r4=0; x=1; 8620051:>1:r1=1; 3:r1=1; 3:r4=0; x=1; 237395:>1:r1=0; 3:r1=0; 3:r4=1; x=1; 11388622:>1:r1=1; 3:r1=0; 3:r4=1; x=1; 30032814:>1:r1=0; 3:r1=1; 3:r4=1; x=1; 52000862:>1:r1=1; 3:r1=1; 3:r4=1; x=1; 29506017:>1:r1=0; 3:r1=0; 3:r4=0; x=2; 252754:>1:r1=1; 3:r1=0; 3:r4=0; x=2; 161130:>1:r1=0; 3:r1=1; 3:r4=0; x=2; 1206650:>1:r1=0; 3:r1=0; 3:r4=1; x=2; 1061614:>1:r1=1; 3:r1=0; 3:r4=1; x=2; 18270263:>1:r1=0; 3:r1=1; 3:r4=1; x=2; 11328831:>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 429.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for src/Y35.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PPC Y35 "Rfe SyncdRW Wse LwSyncdWW Rf*e DpCtrlIsyncdR Fre" {0:r2=z; 1:r2=z; 1:r4=x; 2:r2=x; 2:r4=y; 3:r2=y; 3:r4=z;} P0 | P1 | P2 | P3 ; li r1,1 | lwz r1,0(r2) | li r1,2 | DIY00: ; stw r1,0(r2) | sync | stw r1,0(r2) | lwarx r1,r0,r2 ; | li r3,1 | lwsync | cmpw r1,r1 ; | stw r3,0(r4) | li r3,1 | beq LC01 ; | | stw r3,0(r4) | LC01: ; | | | isync ; | | | lwz r3,0(r4) ; | | | stwcx. r1,r0,r2 ; | | | bne DIY00 ; exists (x=2 /\ 1:r1=1 /\ 3:r1=1 /\ 3:r3=0) Generated assembler _litmus_P1_0_: lwz 3,0(11) _litmus_P1_1_: sync _litmus_P1_2_: li 30,1 _litmus_P1_3_: stw 30,0(9) _litmus_P0_0_: li 6,1 _litmus_P0_1_: stw 6,0(9) _litmus_P3_0_: LitDIY00: _litmus_P3_1_: lwarx 28,0,11 _litmus_P3_2_: cmpw 28,28 _litmus_P3_3_: beq LitLC01 _litmus_P3_4_: LitLC01: _litmus_P3_5_: isync _litmus_P3_6_: lwz 30,0(9) _litmus_P3_7_: stwcx. 28,0,11 _litmus_P3_8_: bne LitDIY00 _litmus_P2_0_: li 4,2 _litmus_P2_1_: stw 4,0(11) _litmus_P2_2_: lwsync _litmus_P2_3_: li 3,1 _litmus_P2_4_: stw 3,0(9) Test Y35 Allowed Histogram (15 states) 9012721:>1:r1=0; 3:r1=0; 3:r3=0; x=1; 24062777:>1:r1=1; 3:r1=0; 3:r3=0; x=1; 3089455:>1:r1=0; 3:r1=1; 3:r3=0; x=1; 8907715:>1:r1=1; 3:r1=1; 3:r3=0; x=1; 294909:>1:r1=0; 3:r1=0; 3:r3=1; x=1; 11319279:>1:r1=1; 3:r1=0; 3:r3=1; x=1; 29779478:>1:r1=0; 3:r1=1; 3:r3=1; x=1; 51541654:>1:r1=1; 3:r1=1; 3:r3=1; x=1; 29901622:>1:r1=0; 3:r1=0; 3:r3=0; x=2; 239846:>1:r1=1; 3:r1=0; 3:r3=0; x=2; 149356:>1:r1=0; 3:r1=1; 3:r3=0; x=2; 1077830:>1:r1=0; 3:r1=0; 3:r3=1; x=2; 1031713:>1:r1=1; 3:r1=0; 3:r3=1; x=2; 18270380:>1:r1=0; 3:r1=1; 3:r3=1; x=2; 11321265:>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 426.34 Revision 6782, version 3.00+1 Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 100000 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 1000 #endif #ifndef AVAIL #define AVAIL 0 #endif /* gcc options: -D_GNU_SOURCE -Wall -std=gnu99 -O -m32 -pthread */ /* barrier: user */ /* launch: changing */ /* cache: false */ /* call: false */ /* affinity: incr0 */ /* randomise_affinity: false */ /* prealloc: false */ /* memory: indirect */ /* safer: true */ /* preload: true */ /* para: self */ /* speedcheck: false */ /* proc used: 0 */ GCCOPTS="-D_GNU_SOURCE -Wall -std=gnu99 -O -m32 -pthread" LITMUSOPTS=-rm -s 1000 -r 100k Sun Jan 23 19:01:37 CST 2011