webworkers for runZ3WebJS never gets killed about z3guide HOT 5 CLOSED

@NikolajBjorner Is my understanding of this line correct that Z3.Context in the high-level API deletes the context itself, so that we don't have to call Z3.del_context(ctx) externally?

from z3guide.

I asked because we always called Z3.del_context(ctx) when handling web-based executions for the SMITLIB format (see this line in runZ3Web.ts), but not in runZ3JSWeb.ts, where we call evalZ3JS() from eval-z3.ts that @bakkot provided. The evalZ3JS() call does not delete the context after calling eval(), so I doubt whether this is causing the dangling webworkers for JS examples.

from z3guide.

To replicate in Chrome (which lets you see the number of dedicated workers in Task Manager):

1. Go to Playground, where a SMTLIB example is hosted. Click "Run" twice (to get the web-computed output instead of the pre-computed output). You see one webworker.
2. Go to some other SMTLIB code snippet and click "Run" twice to get the web-computed output, you still see one webworker, no matter how many more times you click.
3. Now go to some JS example in the "Programming Z3" section. Click "Run" twice to get the web-computed output, you see TWO webworkers, where the new one was added for the JS example.
4. Go to another JS example, click "Run" twice, and you see THREE webworkers, where the last two dedicated for executions of the two JS snippets, respectively.

I would expect for one or maybe two webworkers at most for the web-based executions, one handling the SMTLIB examples and the other handling the JS examples. It looks like we are creating a new webworker every time we run one new JS snippet, which is problematic.

from z3guide.

The webworkers actually never get killed by anything, but there's a bounded number. Normally they'd go away when you navigate to a new page, but the docusaurus site appears to not be doing a "soft" navigation, where it just loads the content for the new page and changes the URL without doing an actual navigation (which would kill the existing webworkers).

Given that, you shouldn't be able to make more than 3 workers, I think - 1 for the SMTLIB examples, 2 for the JS examples (though I don't know why it's 2 rather than 1). In particular, I am pretty sure it's not making a new one every time you evaluate a JS snippet, at least in my testing.

from z3guide.

Thanks for the quick response. It is indeed capped at 3 for JS examples. In that case I think we should be fine...? I mean people can always refresh the page to clear out the queue of webworkers.

from z3guide.