OPEN ARENA MULTITHREADING CODE

It seems clear to me that supporting pthread_kill is not easy in the context of OCaml, it is known how hard it was for Isabelle to get their Thread.kill right, however as of today it works fine, so Isabelle can just indeed submit its proof checking tasks to its thread pool and cancel them happily if the document has changed. I will open an issue upstream to continue the discussion.

OPEN ARENA MULTITHREADING CODE

Thanks for the all the feedback, unfortunately this means that OCaml 5.0 will still be unfit for a large variety of uses, mostly related to applications that would like to use domains to perform search, where it is indeed impractical to have for example a thread in a chess search engine for example to do poll, that assuming the developers of such existing code would agree to retrofitting that.įor example, for Coq, it is just either very costly or very brittle to add such checking points. I would suggest organising your code such that the speculative domains poll for the termination condition and voluntarily terminate. Hence, we do not provide or plan to provide such a mechanism for domains. I gave a bibliography of important resources on this topic at the end of the guide to program with interrupts and during my presentation at the Ocaml workshop 2021 ( video).ĭomain.kill and similar asynchronous exceptions are hard to use correctly in the presence of resources. There is a non-negligible delta between this paper and the practice of asynchronous exceptions in Haskell, and it omits the experience of other languages that have introduced key exception-safety concepts. The Asynchronous Exceptions in Haskell paper is a nice work but I would not recommend it as a first read nor as a sole reference.

Once Memprof is available for OCaml 5, my library memprof-limits will provide ways and guidance to interrupt a domain on an arbitrary trigger, including in the presence of resources that need cleaning-up. There are already lots of programs using asynchronous exceptions in OCaml, and it is sometimes not realistic to rewrite them to poll explicitly (as knows well). You might be thinking about making arbitrary programs ready for asynchronous exceptions, which of course is not realistic and is not a question that we are asking in general. Current programs not using asynchronous exceptions would continue running just fine because they would not use asynchronous exceptions, and in addition only the part of the program that needs to be interrupted needs to be made exception-safe.

I do not think it is true that adding asynchronous exception-safety features would be a problem for backwards-compatibility.

Open arena multithreading