[Haskell-cafe] STM Finalizers

[Michael Schröder]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150730/69719d06/attachment.html>