I've started reading through and I can finish the review of by mid-week.

One thing I am not sure about is whether it's the right thing to reintroduce caml_process_pending_actions_exn. While the reimplementation complies with the _exn bit, it doesn't actually process pending actions - only signals. If there is code that has long-running C code that relies on that as a poll, it will compile but may perform terribly if there are multiple domains running.

I would tend to agree with you regarding caml_process_pending_action_exn and reintroduce it in the API only commented-out. But polling for signals is barely just what is needed to avoid a big temporary rework of the Coq VM. (The other regression that affects the Coq VM is allocation calling finalisers right away, but they seem to avoid it by not using finalisers at all.) Right @silene?

However I will document the limitation.

The 6th and 7th commit are best reviewed by comparing to pre-multicore trunk. It mainly reintroduces what was already there. Only for runtime/weak.c in the 7th I had to get creative, so you might want to proofread it twice.

I would tend to agree with you regarding caml_process_pending_action_exn and reintroduce it in the API only commented-out. But polling for signals is barely just what is needed to avoid a big temporary rework of the Coq VM.

So my understanding from rocq-prover/rocq#15464 (comment) and the discussion afterward is that switching to caml_process_pending_signals_exn (which is effectively what actions would now do) is sufficient.

Right, there are no meaningful finalizers in Coq.

Basically, what Coq needs is an extremely cheap way of testing that a signal (namely sigint) is pending. By extremely cheap, I mean that, ideally, it should be nothing more than reading a single word in memory. If the test is positive, then we ask the runtime to trigger the resolution of the signal. The only thing we need is that, whatever the runtime performs at this point, if an exception is raised (and for sigint, it is), we have a way to intercept the exception to cleanup after ourselves before reraising the exception.

Whether we detect only pending signals or other pending events, we do not care, as long as the test is cheap and has no false positive. And if the runtime decides to perform a lot more work than just resolving the pending signal, that is also fine with us.

And just to be complete, handling signals is just one of the issues. The other is what to do with Alloc_small. Indeed, we pass as the last macro argument some C code that calls caml_process_pending_actions. Again, we do not care what the runtime performs at this point and how long it takes. We just need some way to catch any exception that might be raised.

Right. One point is that caml_process_pending_signals_exn is internal (but Coq VM already uses internals) and we can avoid having one more preprocessor switch in the Coq VM. It's as you prefer.

Coq VM will indeed need to be changed to call Alloc_small with { caml_handle_gc_interrupt(); } as last parameter. It might be forward-compatible for OCaml 5. (caml_handle_gc_interrupt_no_async_exc is renamed into caml_handle_gc_interupt in this PR, although it currently calls finalisers in both versions; later it should not).

So there's maybe the option of not requiring more changes to the CoqVM later.

It's worth testing the performance impact of polling in the new version. caml_check_pending_actions is broken currently, do not use it. caml_process_pending_*_exn are already guarded by caml_check_for_pending_signals which is much more efficient than it used to be. caml_process_pending_actions_* is always meant to be fast when no actions are pending.

caml_check_for_pending_signals is much more efficient than it used to be

Perhaps, but it is still incredibly slower than the approach available in OCaml 4. In the old world, we could just check the value of caml_something_to_do. Now we have to execute the following function:

  atomic_thread_fence(memory_order_acquire);
  for (i = 0; i < NSIG_WORDS; i++) {
    if (atomic_load_explicit(&caml_pending_signals[i], memory_order_relaxed))
      return 1;
  }

By the way, was the performance of OCaml bytecode interpreter tested? The old one was checking caml_something_to_do several million times per second. Now that caml_check_for_pending_signals is called instead, I expect performance to be disastrous. I just tried on a simple loop computing Fibonacci. With OCaml trunk, the bytecode interpreter is 600% slower than OCaml 4.13. In fact, 75% of the time is actually wasted inside caml_check_for_pending_signals, according to perf.

Believe it or not, this function amounts to a test of a single machine word and is compiled as such! See #10880. How recent is your benchmark?

I am interested in feeback regarding the perf of caml_pending_actions*, later. (OCaml ≥ 4.10 has the same issue.) If needed we can declare it as inline in some way.

I just tried on a simple loop computing Fibonacci. With OCaml trunk, the bytecode interpreter is 600% slower than OCaml 4.13. In fact, 75% of the time is actually wasted inside caml_check_for_pending_signals, according to perf.

That was the case a while ago, before #10880 was merged. Performance should be much better now, but can probably be improved some more by just testing young_ptr against young_limit.

just testing young_ptr against young_limit

This would not work currently.

This would not work currently.

Couldn't we make it work? It's good enough for native code, so it should be doable in bytecode too.

I might have misread your comment. For @silene it is probably not enough to test young_limit because it is reset by allocations. Eventually for OCaml's bytecode interpreter the goal is to just have this test, yes. But if the issue mentioned at #10880 (comment) has the same origin then this is fixed on the way to solving #10915 (edit: looking at it again I do not see an indication that the failing test depends on #10915; I do not mean to discourage looking at the issue independently).

How recent is your benchmark?

Indeed, my mistake. After recompiling OCaml trunk, it is not as slow, but it is still 70% slower than OCaml 4.08 and 4.13. That said, it does not seem to be due to caml_check_for_pending_signals, which is now down to 4% of the total time.

For the record, in the loop version of Fibonacci, time is spent inside caml_modify, while in the recursive version, time is spent inside caml_ensure_stack_capacity. But, while the time spent there is significant, it does not entirely explain the slowdown.

I have to leave your remaining remark for another time.

• I have removed the commit about documenting caml_modify. Stephen is preparing us a much better explanation.
• I have somehow fixed the implementation of caml_check_pending_actions, which happens to fix a bug in io.c (edit: hasty conclusion).
• I have removed caml_process_pending_actions_exn for now. I have left it commented-out in the API for documentation purposes. @silene, please use the internal caml_process_pending_signals_exn in the meanwhile if OCaml 5.0 is released without this function.

Please review the last three commits (the others have not changed) and then I'll clean up the history.

It is clean now, thanks.

Brilliant, thanks for your work on this @gadmm