Stack overflows

[cpitclaudel]

Hi there,

I 'm compiling a fairly large set of mutually recursive functions (~1k lines). The resulting javascript is a large (~3k lines) function. I'm running into stack overflows, although the same bytecode requires very little stack (it starts overflowing when I reduce the stack size to 25kB, but it works fine at e.g. 50kB).

Is there anything I should look into, specifically? Any optimizations I should disable, or enable? The problem happens both with the default settings and with --opt 3

Thanks.

[ejgallego]

Browser / node information is crucial here as SO behavior is very sensible to a particular JS optimizer.

One trick you can try in Dev Chrome is to "warm" the optimizer up. That is to say, try to execute such function a few times, after 2/3 stack overflows the browser may re-optimize and the problem may be disappear.

[A gross hack, I know]

[cpitclaudel]

I'm on Chromium, Version 64.0.3282.167 (Official Build) Built on Ubuntu , running on LinuxMint 18.1 (64-bit). I think the main issue is the frame size: the call stacks are not deep:

fstar.core.js:157336 rebuild$0
fstar.core.js:157336 console.trace
rebuild$0 @ fstar.core.js:157336
norm$6 @ fstar.core.js:155839
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155826
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155826
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
norm$2 @ fstar.core.js:160162
norm$6 @ fstar.core.js:156536
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155826
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155826
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155826
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155839
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155826
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
caml_trampoline @ fstar.core.js:2365
rebuild @ fstar.core.js:160165
norm_and_rebuild_match @ fstar.core.js:159505
rebuild$0 @ fstar.core.js:159647
norm$6 @ fstar.core.js:155839
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155826
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155986
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
caml_trampoline @ fstar.core.js:2365
rebuild @ fstar.core.js:160165
norm_and_rebuild_match @ fstar.core.js:159505
rebuild$0 @ fstar.core.js:159647
norm$6 @ fstar.core.js:155839
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155839
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
do_unfold_fv @ fstar.core.js:157256
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
do_unfold_fv @ fstar.core.js:157275
norm$6 @ fstar.core.js:155980
do_unfold_fv @ fstar.core.js:157256
norm$6 @ fstar.core.js:155980
do_unfold_fv @ fstar.core.js:157256
norm$6 @ fstar.core.js:155980
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
rebuild$0 @ fstar.core.js:159324
norm$6 @ fstar.core.js:155848
norm$2 @ fstar.core.js:160162
normalize_with_primitive_steps @ fstar.core.js:160370
normalize$0 @ fstar.core.js:160373
simplify_guard @ fstar.core.js:167737
with_guard @ fstar.core.js:167767
(anonymous) @ fstar.core.js:167829
caml_call1 @ fstar.core.js:3732
pipe_left @ fstar.core.js:101858
sub_comp @ fstar.core.js:167828
check_expected_effect @ fstar.core.js:179584
tc_value @ fstar.core.js:180671
tc_maybe_toplevel_term$0 @ fstar.core.js:180978
tc_maybe_toplevel_term @ fstar.core.js:183338
tc_tot_or_gtot_term @ fstar.core.js:183342
_cFG_ @ fstar.core.js:184522
caml_call1 @ fstar.core.js:3732
map$18 @ fstar.core.js:99502
(anonymous) @ fstar.core.js:184535
caml_call1 @ fstar.core.js:3732
pipe_right @ fstar.core.js:101857
check_let_recs @ fstar.core.js:184535
check_top_level_let_rec @ fstar.core.js:179660
tc_maybe_toplevel_term$0 @ fstar.core.js:183121
tc_maybe_toplevel_term @ fstar.core.js:183338
(anonymous) @ fstar.core.js:188216
caml_call1 @ fstar.core.js:3732
record_time @ fstar.core.js:100748
tc_decls @ fstar.core.js:185775
tc_partial_modul @ fstar.core.js:191403
tc_modul @ fstar.core.js:191454
(anonymous) @ fstar.core.js:198472
caml_call1 @ fstar.core.js:3732
record_time @ fstar.core.js:100748
check_mod @ fstar.core.js:198423
tc_one_file @ fstar.core.js:198543
go$1 @ fstar.core.js:211032
caml_call1 @ fstar.core.js:3732
record_time @ fstar.core.js:100748
(anonymous) @ fstar.core.js:211254
caml_call_gen @ fstar.core.js:181
(anonymous) @ fstar.core.js:1500
Driver.CLI.verify @ fstar.driver.js:130
Instance.verify @ fstar.cli.worker.js:43
Instance.processMessage @ fstar.cli.worker.js:52
(anonymous) @ fstar.cli.worker.js:62
Instance.processMessages @ fstar.cli.worker.js:62
Instance.onMessage @ fstar.cli.worker.js:69
Instance.self.onmessage @ fstar.cli.worker.js:27

[ejgallego]

In that browser you may try enabling chrome://flags/#enable-javascript-harmony then add to the command line --js-flags="--harmony-tailcalls" --js-flags="--stack-size=65536" even tho I'm not sure these last two have an effect anymore. [Remember to close all browser instances and reboot]

I don't follow V8 dev closely anymore so I dunno what chrome://flags/#enable-future-v8-vm-features does.

[cpitclaudel]

Thanks. I just tried in Firefox, and the problem exists there too. :/

[ejgallego]

In the end, the only way I've managed to get around these problems in a reliable way is to run the code in the main thread.

Even if V8 developers told me otherwise, the main thread gets a way better stack treatment than workers. But at some point, using the above flags, I could run using workers pretty well.

[cpitclaudel]

Hmm, I see. I'm not excited about running the code in the main thread :/ How do you retrieve .vos from the main thread? Asynchronously? Do you suspend Coq while waiting for them?

[cpitclaudel]

Your point about re-running is correct, though: I only get a stack overflow the first time...

[ejgallego]

Hmm, I see. I'm not excited about running the code in the main thread :/

Neither I am.

How do you retrieve .vos from the main thread? Asynchronously? Do you suspend Coq while waiting for them?

Yup, I don't start Coq until all the required files have been downloaded.

Your point about re-running is correct, though: I only get a stack overflow the first time...

Glad to hear it doesn't only happen to me. So I have been tracking browser performance since Chrome 40 and indeed it is very hard, a fast-moving target.

It doesn't help that plans for tail-call optimization in JS are so messed up [with Google advocating to optimize only if annotated]. I dunno what more it can be done, it would be great to know how to improve the warm up routine, but I didn't get something that I like.

Maybe you may have some luck asking in SO about SO, people such as Andreas Rossberg used to be there!!

https://stackoverflow.com/questions/38272392/why-does-enable-javascript-harmony-prevent-stackoverflows-in-web-workers

[cpitclaudel]

Yup, I don't start Coq until all the required files have been downloaded.

I see :/

It doesn't help that plans for tail-call optimization in JS are so messed up [with Google advocating to only optimized on-demand]. I dunno what more it can be done, it would be great to know how to improve the warm up routine.

Thing is, I really don't think it's a tail call issue: the calls aren't actually tail-recursive, but that shouldn't be too bad, since there's fairly few of them.. The problem seems to be large stack frames more than many calls.

[ejgallego]

Maybe, last time I investigated a bit more problems like this tail-call had some effect, [Andrew also thought like that] but yeah, who knows, my understanding is that stack size in workers was static so difference in behavior has to be due to JIT.

[cpitclaudel]

Yuck, yuck, yuck.

[ejgallego]

This seems a dead-end, yuck yuck, however, how would https://github.com/sebmarkbage/ocamlrun-wasm fare ?

[cpitclaudel]

Not sure. I don't think that there was much effort there in integrating with system libraries, so I don't know how that would work (files in particular)

Js_of_OCaml is still pretty unique.

[cpitclaudel]

Another relevant source: https://mozakai.blogspot.com/2013/08/outlining-workaround-for-jits-and-big.html

[hhugo]

I 'm compiling a fairly large set of mutually recursive functions (~1k lines). The resulting javascript is a large (~3k lines) function. I'm running into stack overflows, although the same bytecode requires very little stack (it starts overflowing when I reduce the stack size to 25kB, but it works fine at e.g. 50kB).

@cpitclaudel, can you point to code you're compiling and its generated code ?

[cpitclaudel]

Absolutely :)

I'm working on compiling the F* proof assistant. The setup to compile it is here: https://github.com/cpitclaudel/fstar.js

The actual OCaml code that gets compiled (and the problematic function) is here https://github.com/FStarLang/FStar/blob/d678ab35b751adeb843264cbc3da8b30851cb22b/src/ocaml-output/FStar_TypeChecker_Normalize.ml#L3709 and here https://github.com/FStarLang/FStar/blob/d678ab35b751adeb843264cbc3da8b30851cb22b/src/ocaml-output/FStar_TypeChecker_Normalize.ml#L7133

I've uploaded a copy of the generated code here https://gist.github.com/cpitclaudel/2da7d62be9242d3099b129ba23cbb84a. The interesting function are this:

                 norm$6=
                  function(counter,cfg,env,stack,t)
                   {var cfg$0=cfg,env$0=env,stack$0=stack,t$0=t;
                    for(;;)

and that:

                 rebuild$0=
                  function(counter,cfg,env,stack,t$7)
                   {var cfg$0=cfg,env$0=env,stack$0=stack,t$8=t$7;
                    a:

The OCaml code is already the result of extracting F* code, so a more readable version is at https://github.com/FStarLang/FStar/blob/d678ab35b751adeb843264cbc3da8b30851cb22b/src/typechecker/FStar.TypeChecker.Normalize.fs#L1012 and https://github.com/FStarLang/FStar/blob/d678ab35b751adeb843264cbc3da8b30851cb22b/src/typechecker/FStar.TypeChecker.Normalize.fs#L2056

Let me know if I can help diagnose this (for example, I could share the bytecode files — this is all very much work in progress… sorry if things aren't the simplest to run / compile). One experience I've had with compiling CVC4 with emscripten is that Chrome and FF are both very sensitive to excessive function size, making Emscripten's outlining optimization extremely useful.

[hhugo]

just curious, have you tried disabling inlining ? (with --disable=inline)

[cpitclaudel]

I think so, once (IIRC, I disabled all optimizations); let me try it again :)

[ejgallego]

By the way @cpitclaudel what method are you using to get call stacks in the StackOverflow handler? Myself I am not having much luck with the usual tricks.

[hhugo]

what "usual trick" are you talking about ?

[ejgallego]

Setting a breakpoint inside caml_wrap_exception is one of them for example. [Having more luck with this one right now BTW].

Before I tried https://github.com/ocsigen/js_of_ocaml/issues/410 but may I did not understand well.

[cpitclaudel]

I disable all error catching in my program, and then I inspect the error in chrome's debugger. In bad cases, I put console.trace in the function that I suspect is causing issues.

[ejgallego]

I see, thanks. I have started to use a very similar method [adding debugger to caml_wrap_exception] and so far it has been working well now, for some reason last time I tried I didn't manage to get proper backtraces.

Anyways, stack traces for Coq don't look very interesting, lots of very simple calls mixed with a couple of large closures. In 8.9 these large closures will go away so we will see if that has an effect.

[hhugo]

There is a way to attach js stacktraces to ocaml exceptions. It would not work for stackoverflow yet though. I'll try to come back with an example soon.

[cpitclaudel]

just curious, have you tried disabling inlining ? (with --disable=inline)

It doesn't seem to make a difference — I get stack overflows in the same places.

[hhugo]

The new cps compilation mode used for ocaml 5.0 effects might help. (--enable effects)

[hhugo]

reopen if you still have issues