[Haskell-cafe] STM Finalizers

Ben midfield at gmail.com
Thu Jul 30 16:24:55 UTC 2015


what happens if an exception is thrown?  what are the retry semantics?  is there a at-most-once guarantees for the IO action?

best regards, b

> On Jul 30, 2015, at 4:11 AM, Michael Schröder <mc.schroeder at gmail.com> wrote:
> 
> Hi everyone,
> 
> I want to finally announce some work I did as part of my master's thesis [1]. It's an extension to GHC's STM implementation. The main idea is to introduce a new primitive function
> 
>     atomicallyWithIO :: STM a -> (a -> IO b) -> IO b
> 
> Like the existing atomically operation, atomicallyWithIO performs an STM computation. Additionally, it takes a finalizer, which is an arbitrary I/O action that can depend on the result of the STM computation, and combines it with the transaction in such a way that:
> 	• The finalizer is only performed if the STM transaction is guaranteed to commit.
> 	• The STM transaction only commits if the finalizer finishes without raising an exception.
> 
> 
> A motivation of why this is useful: 
> 
> Say we want to save the results of some STM transaction, i.e. persist them to disk. Currently, this is not possible in a transactionally safe way. The naive approach would be to first atomically perform some STM computation and then independently serialise its result:
> 
>     do 
>         x <- atomically m
>         serialize x
> 
> There are two issues with this. First, another thread could perform a second transaction and serialise it before we have finished serialising ours, which could result in an inconsistent state between the memory of our program and what is stored on disk. Secondly, the function serialize might not terminate at all; it could throw an exception or its thread could die. Again we would end up with an inconsistent state and possibly data loss.
> 
> We might try to simply move serialisation into the atomic block, but to do this we have to circumvent the types, which should already be a huge red flag:
> 
>     atomically $ do
>         x <- m
>         unsafeIOToSTM (serialize x)
> 
> The problem here is of course that an STM transaction can retry many times, which will also result in serialize being executed many times, which is probably not something we want. Furthermore, if the thread receives an asynchronous exception, the transaction will abort in an orderly fashion, while serialize, with its irrevocable side effects, cannot be undone.
> 
> But with finalizers, the solution is easy:
> 
>     atomicallyWithIO m serialize
> 
> 
> I've written a small example application that uses finalizers and other stuff from my thesis to build a lightweight STM database framework: [2]
> 
> There are more possible uses cases besides serialisation (such as interactive transactions) and some interesting issues surrounding finalizers (like nesting of transactions) which are discussed in greater detail in my thesis [1], which also includes a formal operational semantics of the whole thing.
> 
> I have implemented finalizers in my fork of GHC [3], if any of you want to play around with them yourself. The atomicallyWithIO function is exported from the GHC.Conc.Sync module.
> 
> 
> Cheers,
> Michael
> 
> 
> [1] https://github.com/mcschroeder/thesis
> [2] https://github.com/mcschroeder/social-example
> [3] https://github.com/mcschroeder/ghc
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe



More information about the Haskell-Cafe mailing list