aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/profiling.txt
blob: 434b0bfd11871f56904567c340f6eb2c3d3ebba9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
Notes on Profiling Proof General in XEmacs  [da]
------------------------------------------------

M-x clear-profiling-info
Eval: (profile (proof-toolbar-next) (proof-shell-wait))
M-x profile-results

NB: Must ignore calls to accept-process-output and sit-for, these
 are from proof-shell-wait (only).


Testing by processing first line of src/HOL/Real/ROOT.ML (i.e. loading
RealDef)

Best case scenarios:

 * Running Isabelle in ordinary shell buffer in Emacs, PIII:
             ~8% Emacs (PIII), ~90% SML   if shell hidden
            ~15% X, ~25% xemacs, ~60% SML if shell displayed!

 * Running Isabelle in xterm:
	    ~3% xterm, ~2% X, 95% SML   if xterm hidden
            ~4% xterm, ~16% X, 90% SML  if xterm revealed


Before optimization:

 * CPU time split about 70%/30% (Cel 366) or 65%/35% (PIII 500) SML/xemacs



   
    



Sample Runs. Tue Oct  5
-----------------------

[On Cel 366 64M]


Function Name                          Ticks    %/Total   Call Count
===================================    =====    =======   ==========
(in redisplay)                         1183     44.947    
re-search-forward                      901      34.233    8061
sit-for                                159      6.041     11919
comint-output-filter                   93       3.533     3596
accept-process-output                  43       1.634     11919
string-match                           34       1.292     7300
font-lock-pre-idle-hook                30       1.140     25261
insert-before-markers                  28       1.064     3597
let                                    14       0.532     10853
map-extents                            13       0.494     539
(in garbage collection)                10       0.380     
byte-code                              9        0.342     25376
while                                  8        0.304     3648
setq                                   7        0.266     8299
comint-postoutput-scroll-to-bottom     7        0.266     3597
next-window                            6        0.228     7194
put-nonduplicable-text-property        5        0.190     1166
marker-position                        5        0.190     14389
goto-char                              5        0.190     14097
walk-windows                           4        0.152     3597
window-minibuffer-p                    4        0.152     3597
proof-toolbar-refresh                  4        0.152     3686
and                                    4        0.152     11162
selected-window                        3        0.114     14390
window-start                           3        0.114     3596
proof-shell-filter                     3        0.114     3597
itimer-time-difference                 3        0.114     546
#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4>    3        0.114     7194
#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442>    3        0.114     1298
process-buffer                         3        0.114     3596
point                                  3        0.114     7382
or                                     3        0.114     7256
comint-watch-for-password-prompt       3        0.114     3597
save-excursion                         2        0.076     3655
proof-shell-process-urgent-messages    2        0.076     3597
marker-buffer                          2        0.076     3596
font-lock-fontify-keywords-region      2        0.076     45
process-mark                           2        0.076     7208
redisplay-echo-area                    2        0.076     23
if                                     2        0.076     18901
buffer-name                            1        0.038     3650
erase-buffer                           1        0.038     26
pos-visible-in-window-p                1        0.038     1
window-buffer                          1        0.038     7195
self-insert-command                    1        0.038     14
<                                      1        0.038     4300
itimer-timer-driver                    1        0.038     182
font-lock-fontify-glumped-region       1        0.038     31
get-buffer-process                     1        0.038     3633
char-to-string                         1        0.038     3597
save-current-buffer                    1        0.038     17
insert-string                          1        0.038     23
--------------------------------------------------------------------
Total                                  2632     100.00


One tick = 1 ms


[On PIII 256M]  top shows roughly 65% SML / 35% xemacs.

Function Name                             Ticks    %/Total   Call Count
======================================    =====    =======   ==========
(in redisplay)                            3529     55.166    
re-search-forward                         1520     23.761    31627
sit-for                                   356      5.565     33870
comint-output-filter                      265      4.143     12980
accept-process-output                     125      1.954     33870
font-lock-pre-idle-hook                   67       1.047     73094
insert-before-markers                     51       0.797     12981
(in garbage collection)                   46       0.719     
string-match                              44       0.688     27686
byte-code                                 27       0.422     74822
let                                       23       0.360     39724
#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4>    21       0.328     25962
selected-window                           20       0.313     51951
comint-postoutput-scroll-to-bottom        19       0.297     12981
setq                                      15       0.234     39971
if                                        15       0.234     72709
walk-windows                              13       0.203     12981
proof-toolbar-refresh                     13       0.203     14429
marker-position                           12       0.188     51925
proof-shell-filter                        12       0.188     12981
goto-char                                 12       0.188     53685
run-hook-with-args                        12       0.188     13219
next-window                               11       0.172     25962
and                                       9        0.141     40761
save-excursion                            8        0.125     13756
buffer-name                               7        0.109     13783
window-buffer                             7        0.109     26077
log-message                               7        0.109     237
process-mark                              7        0.109     26208
point                                     7        0.109     27554
while                                     7        0.109     13727
#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442>    6        0.094     11268
char-to-string                            6        0.094     12981
force-mode-line-update                    6        0.094     12980
<                                         5        0.078     19216
itimer-run-expired-timers                 4        0.063     415
aref                                      4        0.063     11953
get-buffer-process                        4        0.063     13290
proof-shell-process-urgent-messages       4        0.063     12981
redisplay-echo-area                       4        0.063     238
insert-string                             4        0.063     238
font-lock-fontify-keywords-region         4        0.063     740
window-minibuffer-p                       3        0.047     12981
window-start                              3        0.047     12980
marker-buffer                             3        0.047     12980
process-buffer                            3        0.047     12980
featurep                                  3        0.047     2120
comint-watch-for-password-prompt          3        0.047     12981
set-buffer                                2        0.031     259
or                                        2        0.031     26285
font-lock-after-change-function-1         2        0.031     494
font-lock-default-fontify-region          2        0.031     740
event-over-toolbar-p                      1        0.016     107
get-buffer                                1        0.016     433
extent-object                             1        0.016     988
itimerp                                   1        0.016     9136
itimer-is-idle                            1        0.016     3735
set-extent-property                       1        0.016     1024
make-string                               1        0.016     247
next-single-property-change               1        0.016     246
expand-file-name                          1        0.016     96
incf                                      1        0.016     11268
center-to-window-line                     1        0.016     9
proof-done-advancing                      1        0.016     2
itimer-time-difference                    1        0.016     1660
itimer-timer-driver                       1        0.016     415
1+                                        1        0.016     11268
length                                    1        0.016     249
append-message                            1        0.016     238
concat                                    1        0.016     246
proof-shell-strip-special-annotations     1        0.016     246
proof-shell-process-urgent-message        1        0.016     246
buffer-substring                          1        0.016     493
save-current-buffer                       1        0.016     248
newline                                   1        0.016     246
insert                                    1        0.016     249
current-time                              1        0.016     831
match-beginning                           1        0.016     247
font-lock-append-text-property            1        0.016     246
progn                                     1        0.016     1034
proof-response-buffer-display             1        0.016     246
font-lock-fontify-syntactically-region    1        0.016     740
font-lock-fontify-glumped-region          1        0.016     494
#<compiled-function (buffer &rest body) "...(8)" [save-current-buffer set-buffer buffer body] 3 540150>    1        0.016     248
font-lock-after-change-function           1        0.016     494
-----------------------------------------------------------------------
Total                                     6397     100.00


One tick = 1 ms


*** After some optimization attempt in proof-shell-process-urgent-messages,
    to remove re-search-forward hog:

[Cel 366]

Function Name                          Ticks    %/Total   Call Count
===================================    =====    =======   ==========
accept-process-output                  3279     62.374    1047436
(in redisplay)                         919      17.481    
sit-for                                547      10.405    1047435
re-search-forward                      134      2.549     8950
while                                  110      2.092     3648
comint-output-filter                   65       1.236     3347
(in garbage collection)                24       0.457     
font-lock-pre-idle-hook                18       0.342     14166
insert-before-markers                  15       0.285     3348
string-match                           10       0.190     7376
let                                    9        0.171     7010
#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4>    9        0.171     6696
setq                                   6        0.114     12598
byte-code                              5        0.095     14879
#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442>    5        0.095     4762
and                                    5        0.095     10936
comint-postoutput-scroll-to-bottom     5        0.095     3348
log-message                            4        0.076     98
save-excursion                         3        0.057     3655
itimerp                                3        0.057     14128
selected-window                        3        0.057     13403
next-window                            3        0.057     6696
point                                  3        0.057     10722
proof-toolbar-refresh                  3        0.057     3942
if                                     3        0.057     23233
font-lock-default-unfontify-region     3        0.057     295
walk-windows                           2        0.038     3348
event-window                           2        0.038     658
buffer-name                            2        0.038     3670
erase-buffer                           2        0.038     105
put-nonduplicable-text-property        2        0.038     590
window-start                           2        0.038     3347
null                                   2        0.038     3352
marker-position                        2        0.038     13393
marker-buffer                          2        0.038     3347
itimer-time-difference                 2        0.038     2223
-                                      2        0.038     3350
font-lock-fontify-keywords-region      2        0.038     295
goto-char                              2        0.038     14092
buffer-substring                       2        0.038     196
redisplay-echo-area                    2        0.038     104
run-hook-with-args                     2        0.038     3447
comint-watch-for-password-prompt       2        0.038     3348
event-over-vertical-divider-p          1        0.019     254
event-glyph-extent                     1        0.019     329
get-buffer                             1        0.019     255
pointer-image-instance-p               1        0.019     985
barf-if-buffer-read-only               1        0.019     98
extent-at                              1        0.019     87
itimer-value                           1        0.019     6175
pos-visible-in-window-p                1        0.019     4
expand-file-name                       1        0.019     192
file-truename                          1        0.019     104
center-to-window-line                  1        0.019     4
proof-shell-process-urgent-messages    1        0.019     3348
proof-shell-filter                     1        0.019     3348
set-marker                             1        0.019     3429
itimer-run-expired-timers              1        0.019     247
<                                      1        0.019     5950
min                                    1        0.019     3428
1-                                     1        0.019     3428
display-message                        1        0.019     99
font-lock-fontify-glumped-region       1        0.019     197
get-buffer-process                     1        0.019     6791
process-mark                           1        0.019     10124
default-mouse-motion-handler           1        0.019     329
char-to-string                         1        0.019     3348
save-current-buffer                    1        0.019     99
newline                                1        0.019     98
or                                     1        0.019     3490
#<compiled-function (buffer &rest body) "...(8)" [save-current-buffer set-buffer buffer body] 3 540150>    1        0.019     99
font-lock-unfontify-region             1        0.019     295
specifier-instance                     1        0.019     329
--------------------------------------------------------------------
Total                                  5257     100.00


One tick = 1 ms


[PIII]  split now about 70%/30%

Function Name                             Ticks    %/Total   Call Count
======================================    =====    =======   ==========
(in redisplay)                            3638     72.082    
sit-for                                   358      7.093     34176
comint-output-filter                      247      4.894     12963
accept-process-output                     132      2.615     34176
font-lock-pre-idle-hook                   70       1.387     74389
insert-before-markers                     67       1.328     12964
string-match                              50       0.991     27655
(in garbage collection)                   43       0.852     
#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4>    29       0.575     25928
re-search-forward                         25       0.495     18630
comint-postoutput-scroll-to-bottom        24       0.476     12964
byte-code                                 22       0.436     76129
selected-window                           20       0.396     51883
walk-windows                              19       0.376     12964
let                                       18       0.357     13746
next-window                               16       0.317     25928
proof-toolbar-refresh                     13       0.258     14445
while                                     13       0.258     13710
proof-shell-filter                        11       0.218     12964
process-mark                              11       0.218     39137
save-excursion                            10       0.198     13741
setq                                      10       0.198     27010
and                                       9        0.178     27701
goto-char                                 8        0.159     27695
run-hook-with-args                        8        0.159     13211
if                                        7        0.139     33491
font-lock-fontify-keywords-region         6        0.119     740
#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442>    6        0.119     11268
get-buffer-process                        6        0.119     26242
char-to-string                            6        0.119     12964
redisplay-echo-area                       6        0.119     253
specifier-instance                        6        0.119     656
itimerp                                   5        0.099     5713
1-                                        5        0.099     13209
point                                     5        0.099     27523
buffer-name                               4        0.079     13766
current-buffer                            4        0.079     13210
window-start                              4        0.079     12963
<                                         4        0.079     6236
itimer-timer-driver                       4        0.079     380
default-mouse-motion-handler              4        0.079     656
featurep                                  4        0.079     2693
force-mode-line-update                    4        0.079     12963
comint-watch-for-password-prompt          4        0.079     12964
proof-shell-process-urgent-messages       3        0.059     12964
font-lock-fontify-syntactically-region    3        0.059     740
incf                                      3        0.059     11268
marker-position                           3        0.059     12968
set-marker                                3        0.059     13210
itimer-time-difference                    3        0.059     1140
process-buffer                            3        0.059     12963
event-window                              2        0.040     1312
window-minibuffer-p                       2        0.040     12964
window-buffer                             2        0.040     26524
-                                         2        0.040     12967
move-to-left-margin                       2        0.040     246
remove-message                            2        0.040     253
event-buffer                              2        0.040     656
font-lock-default-unfontify-region        2        0.040     740
font-lock-after-change-function           2        0.040     494
buffer-substring                          2        0.040     493
insert-string                             2        0.040     253
event-over-modeline-p                     1        0.020     537
event-glyph-extent                        1        0.020     656
set-syntax-table                          1        0.020     740
pointer-image-instance-p                  1        0.020     1913
extent-start-position                     1        0.020     494
make-extent                               1        0.020     527
detach-extent                             1        0.020     495
extent-at                                 1        0.020     363
itimer-value                              1        0.020     2660
itimer-is-idle                            1        0.020     2280
set-extent-property                       1        0.020     1024
highlight-extent                          1        0.020     656
pos-visible-in-window-p                   1        0.020     9
glyph-property-instance                   1        0.020     656
get-text-property                         1        0.020     492
put-nonduplicable-text-property           1        0.020     1480
next-single-property-change               1        0.020     246
quote                                     1        0.020     13798
marker-buffer                             1        0.020     12963
itimer-run-expired-timers                 1        0.020     380
aset                                      1        0.020     5280
log-message                               1        0.020     246
min                                       1        0.020     13209
current-left-margin                       1        0.020     246
display-message                           1        0.020     246
fw-frame                                  1        0.020     656
font-lock-fontify-region                  1        0.020     740
font-lock-append-text-property            1        0.020     246
substring                                 1        0.020     247
proof-response-buffer-display             1        0.020     246
delq                                      1        0.020     246
syntactically-sectionize                  1        0.020     740
format                                    1        0.020     238
proof-file-truename                       1        0.020     88
newline                                   1        0.020     246
store-match-data                          1        0.020     742
proof-zap-commas-region                   1        0.020     494
specifierp                                1        0.020     656
log-message-filter                        1        0.020     246
-----------------------------------------------------------------------
Total                                     5047     100.00


One tick = 1 ms