Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Make sure a function registered with `at_exit` is executed only once #1790
As shown in MPR#7253 and MPR#7796, there are several cases where
referenced this pull request
May 21, 2018
This seems to be a robust solution to the "double execution" problem. I see no issues with it.
Since you're fixing
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.
@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
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
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
If you have several
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