[Haskell-cafe] STM Finalizers

[Roman Cheplyaka]

Michael,

This looks awesome! Will you try to merge your work into ghc?

I look forward to reading your thesis.

On 30/07/15 14:11, Michael Schröder 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:
> 
>  1. The finalizer is only performed if the STM transaction is guaranteed
>     to commit.
>  2. 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
> 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150730/8d575bff/attachment.sig>