Too much RAM and CPU usage when printing semi-large goals

[mtzguido]

Hey Clément, documenting the issue we spoke about on slack.

This file

module Slow

open FStar.Tactics

assume val f : (i:int) -> PURE int (fun p -> i > 0 /\ (forall i. i > 0 ==> p i))

#set-options "--debug Slow --debug_level TCDeclTime --admit_smt_queries true"

let tau () =
  dump "1";
  dump "2";
  dump "3";
  dump "4";
  dump "5";
  dump "6";
  dump "7";
  dump "8";
  dump "9";
  dump "10";
  ()

let test () : Tot int by (tau ()) =
  let f (x:pos) = f (f x) in
  let f (x:pos) = f (f x) in
  let f (x:pos) = f (f x) in
  let f (x:pos) = f (f x) in
  let f (x:pos) = f (f x) in
  let f (x:pos) = f (f x) in
  let f (x:pos) = f (f x) in
  //let f (x:pos) = f (f x) in
  //let f (x:pos) = f (f x) in
  //let f (x:pos) = f (f x) in
  let v = f (f (f 1)) in
  let v = f (f (f 1)) in
  v

verifies in the command line pretty quickly:

$ runlim fstar.exe Slow.fst
[... bunch of output ..]
Checked let test : _ in 2170 milliseconds
Verified module: Slow (2256 milliseconds)
All verification conditions discharged successfully
[runlim] end:			Wed Aug 15 16:46:17 2018
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		103
[runlim] real:			11.55 seconds
[runlim] time:			10.18 seconds
[runlim] space:			557.2 MB
[runlim] samples:		109

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:

[F*] Checked let test : _ in 27748 milliseconds

It in fact takes much longer than F* itself takes for the whole run, as top shows. 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 checking test:

---

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.

[cpitclaudel]

😍 this example is so small, thanks a lot :)

[cpitclaudel]

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.out

Having 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]

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]

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.