cpitclaudel
commented
6 years ago :heart_eyes: this example is so small, thanks a lot :)
Open mtzguido opened 6 years ago
cpitclaudel
commented
6 years ago :heart_eyes: this example is so small, thanks a lot :)
cpitclaudel
commented
6 years ago Some quick notes:
The CPU profile looks like this:
- fstar-subp-filter 21762 52%
- if 21758 52%
- progn 21756 52%
- let 21742 52%
- if 21738 52%
- let 21735 52%
- if 21731 52%
- let 21727 52%
- if 21725 52%
- let 21717 52%
- if 21713 52%
- progn 21713 52%
- save-current-buffer 21609 52%
- fstar-subp-find-response 14084 33%
- if 14080 33%
- fstar-subp-json--find-response 14063 33%
- while 14061 33%
- let* 13691 32%
- and 13685 32%
+ fstar-subp-json--read-response 13685 32%
+ if 6 0%
+ fstar--has-feature 7 0%
- cond 7389 17%
- fstar-subp--process-message 7383 17%
- cond 7383 17%
- fstar-tactics--display-proof-state 7383 17%
- let 7383 17%
- save-current-buffer 7379 17%
- let 7379 17%
- save-excursion 7292 17%
- fstar-tactics--insert-proof-state 7292 17%
- fstar-tactics--insert-goals 7292 17%
- let 7292 17%
- let 7292 17%
- while 7292 17%
- let 7292 17%
- fstar-tactics--insert-goal 7292 17%
- let 7292 17%
- let 7292 17%
- fstar--insert-ln-with-face 7268 17%
- fstar-highlight-string 7216 17%
+ save-current-buffer 7216 17%
+ apply 52 0%
+ let 12 0%
+ help-window-setup 51 0%
+ temp-buffer-window-show 28 0%
+ let 8 0%
+ fstar-subp-json--parse-proof-state 4 0%
+ let 6 0%
+ save-excursion 87 0%
+ set-buffer 4 0%
+ fstar-subp--query 19 0%+ ~10% in GC time. Newer Emacsen can use a native JSON parser, and we can disable syntax highlighting for large goals; so we could improve here.
The memory profile looks like this:
- fstar-subp-filter 9,523,485,957 68%
- if 9,479,150,372 68%
- progn 9,479,150,372 68%
- let 9,478,620,260 68%
- if 9,478,620,260 68%
- let 9,478,029,956 68%
- if 9,478,029,956 68%
- let 9,477,287,588 68%
- if 9,477,287,588 68%
- let 9,476,274,884 68%
- if 9,476,274,884 68%
- progn 9,476,274,884 68%
- save-current-buffer 9,476,274,884 68%
- save-excursion 5,910,175,612 42%
insert 750,816 0%
- fstar-subp-find-response 3,565,531,144 25%
- if 3,565,531,144 25%
- fstar-subp-json--find-response 3,563,830,984 25%
- while 3,563,830,984 25%
- let* 3,563,821,896 25%
- and 1,860,173,247 13%
+ fstar-subp-json--read-response 1,860,166,911 13%
- if 1,703,644,425 12%
- progn 1,703,644,425 12%
- let 1,703,642,313 12%
- let 1,703,627,529 12%
- let 1,703,624,361 12%
- if 1,703,624,361 12%
- let 1,703,616,969 12%
- if 1,703,616,969 12%
- let 1,703,614,857 12%
- if 1,703,614,857 12%
- progn 1,703,614,857 12%
- save-current-buffer 1,703,614,857 12%
- cond 1,703,608,323 12%
- fstar-subp--process-message 1,703,516,581 12%
- cond 1,703,516,581 12%
- fstar-tactics--display-proof-state 1,703,487,661 12%
- let 1,703,486,605 12%
+ save-current-buffer 1,703,467,597 12%
- fstar-subp-json--parse-proof-state 19,008 0%
+ let 17,952 0%
- let 14,396 0%
+ message 12,348 0%
+ fstar-subp--display-progress 12,412 0%
+ let 85,406 0%
+ if 6,534 0%
delete-region 4,224 0%This one is trickier: we might save memory on JSON, but these allocations are strings actually printed by F*.
Now comes the part where I blame F* :) The problem is the pretty-printer, AFAICT:
(forall (return_val: pos).
return_val ==
f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f
(
f
(
f
(
f
(
f
(
f
(
f
(
f
(
f
(
f
(
f
(
f
(
f
(This printing strategy is quadratic in the number of calls to f, because of the indentation. This can we worked around either by fixing the pretty printer or by giving it a maximum depth or by giving it a maximum width.
And indeed:
$ time "/build/fstar/master/bin/fstar.exe" --ide slow.fst < slow.in > slow.out
real 0m10.805s
user 0m9.768s
sys 0m1.571s
$ ls -alh slow.out
-rw-r--r-- 1 clement clement 53M Aug 15 22:36 slow.outHaving 53MB of JSON to parse slows Emacs down quite a bit, and it slows F correspondingly because F waits for Emacs to read the output before resuming. Running on the CLI is about twice as fast as running under Emacs, and I suspect that's because F block while waiting for Emacs to empty the shared pipe. We could consider a queue design in which F doesn't block while writing to Emacs.
Of course, all of this doesn't say why Emacs ends up consuming so much memory :) I'll investigate this when I'm back from vacation.
cpitclaudel
commented
6 years ago Another thing: Emacs is bad at long lines. Like, really bad. So these long lines will tend to slow the display to a crawl. I suspect that's the 100% CPU use you were seeing
cpitclaudel
commented
6 years ago Regarding RAM usage: are you running with fstar-debug set? With it I observe linearly growing ram as I replay the snippet over and over, which is expected (the full history of input and output is kept), but without it every time I kill the goals buffer memory usage reverts to what it was before running the snippet. Each run of the snippet allocated an extra 50MB, but that's roughly expected given the size of the output.
Hey Clément, documenting the issue we spoke about on slack.
This file
verifies in the command line pretty quickly:
However, in the interactive mode, emacs (not F* for once!) seems to take a huge amount of time to print each goal, about 3 seconds each! This is the (wall clock) time it takes to check the last definition:
It in fact takes much longer than F* itself takes for the whole run, as
topshows. Also, emacs memory consumption doubles after the run, and killing the buffers (plus GC'ing) doesn't seem to help. Here's a before and after of checkingtest:Of course it can be made worse by making the VC larger, for instance by uncommenting the lines above. This was seen while running the separation logic tactics, and it's much worse there. I think it reaches about 10 seconds per dump, and I've seen emacs take over 40GB of RAM+swap in a clean run. Hopefully this small example is enough to diagnose, but I can provide a repro for the bigger example if not.