One could also guard against repeated execution of the individual at-exit functions, as in:

diff --git a/stdlib/stdlib.ml b/stdlib/stdlib.ml
index f87787b9d4..d59bb8b170 100644
--- a/stdlib/stdlib.ml
+++ b/stdlib/stdlib.ml
@@ -538,6 +538,8 @@ let exit_function = ref flush_all
 
 let at_exit f =
   let g = !exit_function in
+  let already_ran = ref false in
+  let f () = if !already_ran then () else (already_ran := true; f ()) in
   exit_function := (fun () -> f(); g())
 
 let do_at_exit () = (!exit_function) ()

I think this should also fix the cases of repeated execution reported in MPR#7253.

Wow. A very good catch!

The PR is a clear improvement as it is, but @gasche's version (with erasing exit_function before calling it) is even better. This should also fix a few other buggy cases.

I don't think @gasche's scenario should happen in practice, but his alternate implementation is nicer, so I just commited it to this GPR.

Doesn't this second version create a race condition, if the change
is propagated to otherlibs/threads/stdlib.ml?

There are also race conditions in @xavierleroy's and @nojb's version, right?

I think the first version is not worse than what we had before w.r.t to
race condition: the registered function can be run more than once.
The second version seems to introduce a race condition causing a
registered function to be never called.

Replicating a few lines from Mutex (in order to avoid a compilation dependency) should help with the race conditions. By the way, wasn't there always a race condition in at_exit, if two threads happen to call it simultaneously?

Could a context switch happen when a closure is allocated?

let at_exit f =
  let g = !exit_function in
  exit_function := (fun () -> f(); g())

Yes.

Thank you @xclerc for having obliquely reminded me to update the otherlibs/threads stdlib.

otherlibs/threads is the VM threads, where preemption occurs only at function calls and loops. So, reading a reference then assigning the reference is actually atomic, making the do_at_exit function thread-safe. (This is how mutexes are implemented in VM threads, actually.)

For system threads do_at_exit is not atomic and not thread safe, for reasons given by others above, but please please do keep in mind that the standard library is not thread safe to begin with. E.g. hash tables are not thread safe, and have never been, and that's a lot more serious than a race between exit and at_exit.

otherlibs/threads is the VM threads, where preemption occurs only at function calls and loops. So, reading a reference then assigning the reference is actually atomic, making the do_at_exit function thread-safe. (This is how mutexes are implemented in VM threads, actually.)

But, precisely, preemption could occur after reading and setting
exit_function when f is called. A second thread would then see
an empty exit_function and could terminate the program by calling
sys_exit. The registered function(s) would never be called in such
a scenario.

For system threads do_at_exit is not atomic and not thread safe, for reasons given by others above, but please please do keep in mind that the standard library is not thread safe to begin with. E.g. hash tables are not thread safe, and have never been, and that's a lot more serious than a race between exit and at_exit.

Sure; I guess my concern was with the composition of libraries.
When dealing with data structures, you can most of the time
shield yourself from a ill-behaved third-party library; it seems much
more difficult (if only possible) with features such as at_exit.
However, I reckon this is a corner case.

OK, I thought you were concerned about the (non-) atomicity of swapping the contents of the reference. Your scenario for a race condition can occur both with VM threads and system threads, I believe.

All this being said, I'd like to improve the sequential case (which this PR does) before worrying about thread safety. Can I please have permission to merge?

The potential for at_exit functions not to run at all in a threaded program I feel should at least be documented.

I agree with @xclerc that it does feel strange to introduce a thread safety issue in a feature where it's very difficult (indeed, impossible in the general case) to work around it in user code.

(It occurred to me that an alternative would be to only change
the documentation in order to require the functions registered
through the at_exit mechanism to be idempotent.)

Having only idempotent functions registered through at_exit is not that convenient, since one common usage is to print out information when the program exits. If this solution (improving the documentation) ends up being chosen, it would be worth mentioning it is only required for concurrent code.

Well, the idea is just to put the burden on the user of at_exit.
If you have no threads and want to print something, just protect
the printing by a bool ref or use laziness.

Cent fois sur le métier... I'll be back with a different implementation.

I am back! See #1790. @nojb's suggestion above (#1783 (comment)) works great.