[Haskell-cafe] STM Finalizers

[Michael Schröder]

>
> what happens if an exception is thrown?


In normal STM, if an exception occurs during a transaction, the transaction
is gracefully aborted & none of its effects are made visible. Exactly the
same thing is true in the presence of finalizers: if an exception occurs in
the finalizer, the transaction is aborted & its effects discarded (you are
still responsible for cleaning up any side effects that happened as part of
the I/O action, of course).


> what are the retry semantics?


The finalizer is only run once the transaction is guaranteed to commit.

The STM part of the transaction might retry many times, but once the system
determines there are no conflicts, it runs the finalizer. When the
finalizer has finished, the transaction commits & makes its effects
visible. If during the time the finalizer is running another transaction
comes along and makes a conflicting write and tries to commit, the other
transaction has to retry (in reality, the other transaction's thread is put
to sleep and woken up once it actually has a chance to commit, i.e. once
the finalizer of the first transaction has finished).


> is there a at-most-once guarantees for the IO action?


Yes (see above).


A much more detailed description of all of this can be found in Sections
2.4 and 2.5 of my thesis [1], in which I give a complete formal semantics
of STM with finalizers.

[1]: https://github.com/mcschroeder/thesis
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150730/f8ec322e/attachment.html>