[Haskell-cafe] STM Finalizers
roma at ro-che.info
Thu Jul 30 11:20:25 UTC 2015
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
> . 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:
> 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: 
> 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 , which also includes a formal operational
> semantics of the whole thing.
> I have implemented finalizers in my fork of GHC , if any of you want
> to play around with them yourself. The atomicallyWithIO function is
> exported from the GHC.Conc.Sync module.
>  https://github.com/mcschroeder/thesis
>  https://github.com/mcschroeder/social-example
>  https://github.com/mcschroeder/ghc
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the Haskell-Cafe