[Haskell-cafe] STM Finalizers

[Ben]

looks very nice.  thanks for the pointers.

best, ben

> On Jul 30, 2015, at 2:19 PM, Michael Schröder <mc.schroeder at gmail.com> wrote:
> 
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe