Context: I’ve been experimenting with adding persistence on top of STM in Haskell. There’s an existing library called TCache to do this, but I’m not happy with some of the design choices there: there’s a lot of global mutable state, playing fast and loose with notions of safety, etc., on top of it not building with modern GHC versions. So I set out to implement an alternative, which I’ve published as persistent-stm, which features a more limited set of possible states and a more explicit API, along with a more detailed argument for its correctness.
However, I’m not happy with the argument for correctness. In the end, the restriction on unsafeIOToSTM that’s most difficult to justify is the one that says the thread may be aborted at any time without throwing an exception or otherwise allowing for any cleanup. This means that code run by unsafeIOToSTM must have the property that if the thread vanishes at any moment, the behavior will still be correct.
That seems to me a very difficult demand to satisfy. In particular, pretty much any effectful code might internally use an implementation that needs some kind of cleanup, and this isn’t typically documented at all. In combing through implementations, I’ve found that seemingly innocuous actions like generating a random number often involve some kind of locking that could stall the whole process if a thread holding the lock were to abort in the middle. There is a trick to work around this, by creating an empty MVar, forking a new thread that writes its result into the MVar, and then taking the result from the MVar… but I also cannot satisfy myself that this isn’t itself unsafe. Can you really fork a new thread without there being even a single moment where you hold a lock on something like the list of threads in the Haskell runtime? Even if you can today, will this remain true in the future?
I guess all this is building up to asking: is it actually just impossible to use unsafeIOToSTM and be confident that the resulting code is guaranteed to be correct? If not, where does the guarantee of correctness come from?
In my case, my use of unsafeIOToSTM is limited to calls to
deRefWeak. There’s no exception handling in my own code, but in order to be safe, I must additionally be sure that no exception handling is needed in the implementations of these functions, either now or in the future. I cannot see how it’s possible to be sure of that for anything.