Stream: Coq devs & plugin devs

Topic: Deactivating `par:` process spawning

Pierre-Marie Pédrot (Nov 17 2022 at 13:47):

Trying to fix the fiat-crypto CI, I realized in https://github.com/coq/coq/pull/16801 that neither -async-proofs off nor -async-proofs-j 1 deactivate the coqworker process spawning when evaluating par: blocks.

Pierre-Marie Pédrot (Nov 17 2022 at 13:48):

This is bad because we use too much memory because of the two processes.

Pierre-Marie Pédrot (Nov 17 2022 at 13:48):

Reading the code, I've only found a very hackish way to deactivate par: altogether and make it behave like a no-op.

Pierre-Marie Pédrot (Nov 17 2022 at 13:48):

Namely, you have to pass the option -worker-id $SOMEDUMMYNAME.

Pierre-Marie Pédrot (Nov 17 2022 at 13:49):

Is there a more principled way to do this? I've found nothing in the doc, and only the above trick reading the code.

Enrico Tassi (Nov 17 2022 at 14:36):

No. I think the right place is today vernac/comTactic which contains a non-parallel version of par and has an API to override it. IMO there you could check for a Goption. (and hence disable via a flag to coqc).

Enrico Tassi (Nov 17 2022 at 14:37):

(there is also -async-proofs-tac-j, but passing 1 would still spawn one extra worker). If you need a quicker patch, pass that and in the STM don't call Partac.enable_blabla if nworkers is 1 (even if it was intentional to allow 1 worker but still use the machinery, to test it)

Gaëtan Gilbert (Nov 17 2022 at 14:46):

which contains a non-parallel version of par

that nobody has ever tested AFAIK

Enrico Tassi (Nov 17 2022 at 14:49):

Maybe it is the right time? I think I tested it on the test suite (not on the whole CI).

Enrico Tassi (Nov 17 2022 at 14:49):

In any case, I don't see any other way of reducing the resources used by par if not by using that code.

Pierre-Marie Pédrot (Nov 17 2022 at 14:58):

The -worker-id trick makes Coq take this path, and on the examples I've tried it seems to work

Enrico Tassi (Nov 17 2022 at 15:09):

Can you run a full CI with your hack implementation?

Pierre-Marie Pédrot (Nov 17 2022 at 15:12):

I have no implementation, I just added the -worker-id flag and it worked, weirdly enough

Pierre-Marie Pédrot (Nov 17 2022 at 15:13):

(without spawning a coqworkmgr process, that is)

Pierre-Marie Pédrot (Nov 17 2022 at 15:13):

do you want me to try hacking the fiat-crypto CI by passing this flag?

Enrico Tassi (Nov 17 2022 at 15:14):

that is the thing, then refine the PR with an actual flag for making par non-parallel

Enrico Tassi (Nov 17 2022 at 15:14):

if it does not fix the issue, then I think the priority is zero (for this extra flag)

Pierre-Marie Pédrot (Nov 17 2022 at 15:16):

dunno, that means that if you use par: you should be ready to use twice as much as memory as needed for the equivalent non-par code

Enrico Tassi (Nov 17 2022 at 15:24):

This has always been the case. I don't get what you want to say

Enrico Tassi (Nov 17 2022 at 15:24):

(actually more than double, it depends on the -blabla-j you pass, people use ~ 10 there as far as I know)

Enrico Tassi (Nov 17 2022 at 15:26):

I think @Michael Soegtrop uses it, other reached me privately, not sure they told me how many workers they used, but for sure not 2 given their speedup

Enrico Tassi (Nov 17 2022 at 15:29):

Our CI is very limited, my smartphone is 4 years old and has more ram than our workers... my new laptop comes with 64GB (and the price in the public market is about 1K).

Théo Zimmermann (Nov 17 2022 at 17:24):

par: had 17 users in the survey respondents: https://coq.discourse.group/t/coq-community-survey-2022-results-part-iii/1777

Michael Soegtrop (Nov 17 2022 at 18:21):

I like to use par in interactive mode for proofs with many cases (I have some which have around 100 to a few 100). I default to 6 when I start an IDE. For me this is quite essential. A side note: I switched from CoqIDE to VSCoq only after par: did work there.

If I use par in batch builds depends on the machine I am on.

Enrico Tassi (Nov 17 2022 at 19:15):

I guess you sed it to all:

Pierre-Marie Pédrot (Nov 17 2022 at 19:18):

I'm not advocating for changing the default behaviour of par:, I'm just saying that for memory reasons (and probably some reproducibility) we should be able to run par: in a single process with a specific flag.

Paolo Giarrusso (Nov 17 2022 at 21:10):

Could -async-proofs-j get to know 0 and accept -async-proofs-j 0 for this?

Paolo Giarrusso (Nov 17 2022 at 21:11):

Then Coq devs (and user) might be able to guess the right option more easily

Pierre-Marie Pédrot (Nov 24 2022 at 11:19):

I've implemented this solution in https://github.com/coq/coq/pull/16837, but it turns out that all these async options are just pure Potemkin configuration. Except for a tiny subset of them, coqc and coqtop plainly ignores them.

Pierre-Marie Pédrot (Nov 24 2022 at 11:20):

They are parsed but never set.

Pierre-Marie Pédrot (Nov 24 2022 at 11:20):

Reading the initialization code of the various toplevels is giving me a primal fear.

Pierre-Marie Pédrot (Nov 24 2022 at 11:21):

We're gladly mixing global variable mutation with state threading, with various places of the code messing with some hardcoded flags. I have literally no idea how and where to fix it.

Pierre-Marie Pédrot (Nov 24 2022 at 11:21):

Calling @Enrico Tassi for help.

Pierre-Marie Pédrot (Nov 24 2022 at 11:23):

Stm.init_core seems like the most reasonable solution but I'm still wary I might break other parts. (Notably new_doc just a few lines below overwrites the config imperatively with whatever it's passed.)

Enrico Tassi (Nov 24 2022 at 12:11):

Hum, I don't have much time but let me check why coqc ignores the flag

Enrico Tassi (Nov 24 2022 at 12:14):

Hum coqc.ml calls Stmargs.parse_args, and that one does

    |"-async-proofs-tac-j" ->
      let j = Coqargs.get_int ~opt (next ()) in
      if j <= 0 then begin
        Coqargs.error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1")
      end;
      { oval with
        Stm.AsyncOpts.async_proofs_n_tacworkers = j
      }

Enrico Tassi (Nov 24 2022 at 12:14):

So I guess I reviewed your code too quickly, this is the flag which should be set to 0

Enrico Tassi (Nov 24 2022 at 12:15):

wait, the PR is ok, so why didn't git pull give me the right code

Enrico Tassi (Nov 24 2022 at 12:20):

ah ah ah, this is really funny, I did pull, but not recompile. So jump to definition in coqc.ml opened an outdated file in _build/blabla

Enrico Tassi (Nov 24 2022 at 12:20):

thank you so much for duplicating sources

Pierre-Marie Pédrot (Nov 24 2022 at 12:21):

The PR is OK, assuming that options are correctly set. The real issue is that Coq just drops the set of options.

Pierre-Marie Pédrot (Nov 24 2022 at 12:22):

So all of this stuff that is neatly documented, including all the -async-* variants, are just no-ops.

Pierre-Marie Pédrot (Nov 24 2022 at 12:22):

(as such, it's not specific to this particular option)

Enrico Tassi (Nov 24 2022 at 12:29):

No it is not that simple, the options are passed to the STM, but are passed too late, at new_doc time. It makes no sense, I'll try a fix

Gaëtan Gilbert (Nov 24 2022 at 12:32):

I tried at https://github.com/coq/coq/pull/16896
didn't test much though

Enrico Tassi (Nov 24 2022 at 12:43):

I don't think it is right, I'll open another PR

Enrico Tassi (Nov 24 2022 at 12:48):

here, tested locally: https://github.com/coq/coq/pull/16897

Enrico Tassi (Nov 24 2022 at 12:51):

the problem is that the stm options (which are not per doc but global) were also passed to Stm.init_process (don't call my why it was named like that) but that function did not store the value, and the call to Stm.init_core which happens immediately after did not see the flags.

Pierre-Marie Pédrot (Nov 24 2022 at 12:51):

that's a reasonable hotfix, but shouldn't we at some point get rid of the global flags? in this sense the fix is going the wrong way.

Enrico Tassi (Nov 24 2022 at 12:52):

Then the options were also passed to new_doc which would save them in a (single) global place, not document specific

Enrico Tassi (Nov 24 2022 at 12:52):

NO we should remove the STM

Enrico Tassi (Nov 24 2022 at 12:52):

(from coqc)

Pierre-Marie Pédrot (Nov 24 2022 at 12:52):

(oh, yeah, that's even better)

Pierre-Marie Pédrot (Nov 24 2022 at 12:54):

when is that going to happen btw? we're wasting loads of memory because of the STM

Pierre-Marie Pédrot (Nov 24 2022 at 12:55):

this should be another high-priority topic on our merely existent roadmap

Gaëtan Gilbert (Nov 24 2022 at 12:56):

"loads of memory" = ?

Pierre-Marie Pédrot (Nov 24 2022 at 13:02):

we keep pointers to irrelevant summaries, so nothing good

Gaëtan Gilbert (Nov 24 2022 at 13:02):

that's not very specific

Pierre-Marie Pédrot (Nov 24 2022 at 13:03):

it's hard to tell exactly how much we would save but there was this issue exploring live data after a GC and we kept random pointers to evarmaps

Pierre-Marie Pédrot (Nov 24 2022 at 13:03):

given that evarmaps can be big...

Enrico Tassi (Nov 24 2022 at 13:07):

IMO it not large at all, but it is true it keeps a summary for each lemma

Enrico Tassi (Nov 24 2022 at 13:08):

The patch I was trying to write about side effects (and the simple compiler) should get rid of it. But after december 12, now I'm busy

Enrico Tassi (Nov 24 2022 at 15:00):

@Pierre-Marie Pédrot @Gaëtan Gilbert would you mind giving https://github.com/coq/coq/pull/16897 a shot and merging?

Pierre-Marie Pédrot (Nov 24 2022 at 15:08):

this works for me on the trivial examples but this is the kind of code I won't ever trust

Pierre-Marie Pédrot (Nov 24 2022 at 15:08):

@Gaëtan Gilbert don't you want to take the responsibility for this one?

Gaëtan Gilbert (Nov 24 2022 at 15:13):

did https://github.com/coq/coq/pull/16801 make fiat pass? if so then just change it in the new PR to the new mechanism and see how it goes

Pierre-Marie Pédrot (Nov 24 2022 at 15:14):

it used to at some point, but we have had the time to break it 50 times in the meantime

Last updated: Apr 19 2024 at 18:01 UTC