(For the record, I mentioned lazyness for use on client code
in the case the API required the registered functions to be
idempotent.)

Well, lazyness could have been used in the implementation of at_exit as well, with possibly stronger atomicity guarantees in Multicore OCaml, but dependencies dictated otherwise.

This seems to be a robust solution to the "double execution" problem. I see no issues with it.

Since you're fixing at_exit, then perhaps it's a good moment to get rid of a different kind of a race condition -- the one in at_exit itself, which happens because of VM thread preemption during the allocation of a closure?

One possible approach:

let at_exit f =
  let g = ref (fun () -> ()) in
  let f_already_ran = ref false in
  let f () =
    if not !f_already_ran then (f_already_ran := true; f ());
    !g ()
  in
  g := !exit_function;
  exit_function := f

This is the silliest piece of code I wrote today, but it illustrates the idea.

Also, an at_exit function that raises could prevent other at_exit functions from being run.

This problem is not fixed by this PR right ?

@murmour, rour code can also be made more readable:

let once f =
  let has_run = ref false in
  fun () ->
    if !has_run then ()
    else (has_run := true; f ())

let add_before f gref =
  (* using (gref := fun () -> f (); !gref ()) would introduce
     an infinite loop; instead we define old_g to be
     the value of !gref before the assignment *)
  let old_g = ref !gref in
  let seq () = f (); !old_g () in
  (* gref may be mutated concurrently during the allocation of seq,
     so we made old_g a reference and update it afterwards. *)
  old_g := !gref;
  gref := seq

let at_exit f =
  add_before (once f) exit_function

@gasche

your code can also be made more readable:

Yes, totally. The change to avoid a race condition is unobvious. On the other hand, I find the original code (of this PR) very readable, with no need for improvements.

Perhaps it'd suffice just to add a couple of comments?

let at_exit f =
  let g = ref (fun () -> ()) in (* a placeholder for !exit_function *)
  let f_ran = ref false in
  let f () =
    if not !f_ran then (f_ran := true; f ());
    !g ()
  in
  (* The following is thread-safe
     (indirection in g was added to avoid a race condition) *)
  g := !exit_function;
  exit_function := f

@dbuenzli asks:

This problem [an at_exit function that raises could prevent other at_exit functions from being run] is not fixed by this PR right ?

Amusingly, the example you gave in MPR#7253 actually works, and is reproduced by the test I added. An exception is raised, then the Printexc code that reports this uncaught exception calls do_at_exit again. The at_exit functions already executed are skipped, including the one that raises the exception, and the remaining at_exit functions are run.

If you have several at_exit functions that raise, some other at_exit functions may still be skipped.

I intend to merge the code in its present state very soon, based on @murmour's positive review. Holler if you're not happy.

As to making at_exit atomic, the implementation above is probably correct with both thread libraries, but could we do this in a different GPR?

As to making at_exit atomic, the implementation above is probably correct with both thread libraries, but could we do this in a different GPR?

It won't hurt to be more atomic, yes.

Cherry-pick to 4.07: 6ce1e6d

Even better: this pull request fixes MPR#7178 as well.