#12742 was reviewed by @gadmm who mentioned that the assertion could also be hit when using statmemprof (which changes the young limit). How does that factor into the current reasoning?

Ah yes - I meant to mention statmemprof. I'm not sure what the situation is here - @NickBarnes should be able to advise.

@damiendoligez your thoughts would be welcomed!

#12879 also relates to the hook mentioned here, fwiw.

This looks right to me - certainly we should reset the young_limit before we call the hook, and plausibly either version of the assertion could fail if we don't.

I am less clear that we should rule out equality in the assertion, but I think that we only reset the limit at times when we know what young_trigger is (e.g. because we have just set it). Clearly we'd benefit overall from more documentation and checking of the invariants here. When in Caml, and no actions are pending, young_ptr >= young_limit (*). That is, you can allocate down to and including the word pointed to by the trigger, without triggering GC - equality is permitted. It's only when young_ptr becomes less than young_limit that we enter the runtime.

(*) More exactly, alloc_ptr >= trigger, where alloc_ptr is either young_ptr or the copy of it in a register in register-rich architectures, and trigger is young_trigger or memprof_young_trigger, copied into young_limit. When actions are pending, young_limit gets set to UINTNAT_MAX to force the next allocation test to enter the runtime.

My interpretation of this issue and the one at #12879 is that one should definitely not call caml_thread_yield inside caml_poll_gc_work. I propose instead to move the code responsible for calling caml_thread_yield into caml_do_pending_actions_exn, in order to treat it as a delayable pending action (which is meant to run OCaml code). This should fix both bugs at once. I opened the PR #12882 to explore this approach.

Note that in OCaml 4, systhread preemption used to be implemented with signals, and thus delayed to a safe point, as in #12882. This also ensured some property for reasoning in FFI code about concurrent mutations.

Thanks for the digging up these issues.

Clearly we'd benefit overall from more documentation and checking of the invariants here.

OK, the invariant for calling caml_reset_young_limit could be tightened, as currently it is meant to be callable anytime, while I am not sure we make use of this freedom. What is not clear to me is, how can we specify it in a way that it is clear that young_ptr != young_limit holds (with memprof in mind)?

Also, I am all for adding assertions that helped catch bugs in practice, but the bug is that caml_reset_young_limit was not called when it should have been, whereas checking young_ptr != young_limit seems to ensure the opposite, that caml_reset_young_limit is not called when it should not be. Is this the right assertion for this bug or could another assertion be more relevant?

I agree with everyone that moving the call to caml_reset_young_limit is a bug-fix. Instead of moving it up a few lines, I would even move it all the way up to right after the assignement to young_trigger because it's morally part of this assignment.

As for the assertion, I don't think you can tighten it safely. As hinted by @NickBarnes and @gadmm, I think that would interfere with statmemprof because an assignment to young_trigger is not the only possible reason for calling caml_reset_young_limit.

Consider the following scenario:

• young_ptr is close to young_trigger and memprof_young_trigger is between the two. You have young_limit == memprof_young_trigger
• an allocation of exactly the right size occurs and sets young_ptr == young_trigger. This allocation triggers caml_memprof_renew_minor_sample, which calls caml_reset_young_limit without changing young_trigger, so you still have young_ptr == young_trigger at the start of caml_reset_young_limit.

While I haven't looked at the new statmemprof code, the invariant here is really that young_ptr >= young_trigger and you shouldn't count too much on the calling context of caml_reset_young_limit for extra conditions.

I think @damiendoligez's analysis is right.