#7930: Nested STM Invariants are lost ----------------------------------------+----------------------------------- Reporter: fryguybob | Owner: fryguybob Type: bug | Status: new Priority: normal | Component: Runtime System Version: 7.6.3 | Keywords: STM Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: Incorrect result at runtime | Blockedby: Blocking: | Related: ----------------------------------------+----------------------------------- Comment(by fryguybob): Luite Stegeman and I have been investigating this further and while the fix for this issue should be straight forward (merging the {{{invariants_to_check}}} field when committing a nested transaction) we have found some additional issues with invariants. In the original paper [1] the text makes it mostly clear how invariants and {{{retry}}} interact: [D7] If an invariant evaluates to retry then the user transaction is aborted and re-executed (potentially after blocking until it is worth re-executing it). And [D8] If an invariant executes a check statement, then the new invariant is checked at that point, but is not retained by the system. The {{{check}}} mentioned in the paper is the {{{alwaysSucceeds}}} in {{{GHC.Conc.Sync}}} which is currently defined as: {{{ -- | Low-level primitive on which always and alwaysSucceeds are built. -- checkInv differs form these in that (i) the invariant is not -- checked when checkInv is called, only at the end of this and -- subsequent transactions, (ii) the invariant failure is indicated -- by raising an exception. checkInv :: STM a -> STM () checkInv (STM m) = STM (\s -> (check# m) s) -- | alwaysSucceeds adds a new invariant that must be true when passed -- to alwaysSucceeds, at the end of the current transaction, and at -- the end of every subsequent transaction. If it fails at any -- of those points then the transaction violating it is aborted -- and the exception raised by the invariant is propagated. alwaysSucceeds :: STM a -> STM () alwaysSucceeds i = do ( i >> retry ) `orElse` ( return () ) checkInv i -- | always is a variant of alwaysSucceeds in which the invariant is -- expressed as an STM Bool action that must return True. Returning -- False or raising an exception are both treated as invariant failures. always :: STM Bool -> STM () always i = alwaysSucceeds ( do v <- i if (v) then return () else ( error "Transactional invariant violation" ) ) }}} This definition attempts to reuse the {{{retry}}} mechanism to handle the rollback of the initial run of the invariant. Lets consider when {{{i}}} evaluates to {{{retry}}}. According to [D7] this {{{i}}} should cause a {{{retry}}} at the level of {{{alwaysSucceeds}}}. But as we see with the code above it will be caught by the {{{orElse}}} as if the invariant succeeded. All is not lost as the invariant is added to the {{{invariants_to_check}}} queue by {{{check#}}} and eventually the {{{retry}}} happens at top-level. Not so fast! There are several problems with this delay. 1. The way [D7] is worded implies that any {{{retry}}} in an invariant is really a top-level {{{retry}}}. I don't know if this is accidental or not, but if so, delay makes some sense. If not the wrong thing happens when you have {{{alwaysSucceeds i `orElse` ...}}}. 2. The delay does not make sense because there are other effects that can intervene before the transaction is committed! Indeed, it could be that it will not hit the retry later on. Or an exception could happen due to the very invariant property being checked (See example below). 3. How does [D8] interact with [D7]? If I have an {{{alwaysSucceeds}}} nested inside another and it does a {{{retry}}} this should be a top-level retry by [D7]. But it should not be retained, so it will never be seen by [D8]. Its parent will, however, be run which will have the effect of running the child again. Its {{{retry}}} will be delayed to commit, but there is no commit. We are checking an invariant! Such a nested {{{retry}}} will never be seen (See other example below). An example that exhibits (2) is the following. The exception should never happen as it is guarded by the {{{retry}}} in the first invariant check. {{{ import Control.Concurrent import Control.Concurrent.STM import Control.Exception.Base test c = do y <- atomically $ do always $ do x <- readTVar c if x then return True else retry z <- readTVar c if z then return z else throwSTM (AssertionFailed "Fail") -- Should never happen print y main = do c <- newTVarIO False forkIO (test c) threadDelay 100000 atomically (writeTVar c True) threadDelay 100000 putStrLn "Done." }}} Running we get the output: {{{ *Main> :main <interactive>: Fail Done. }}} While we would hope to get the output: {{{ *Main> :main True Done. }}} We can exhibit problem (3) with the following program. The idea here is to show an invariant nested within an invariant has different semantics then a single level. {{{ import Control.Concurrent import Control.Concurrent.STM test c = do y <- atomically $ do always $ do always $ do x <- readTVar c if x then return True else retry -- Always retry when c is false. return True readTVar c -- Should always be True. print y main = do c <- newTVarIO False forkIO (test c) threadDelay 100000 atomically (writeTVar c True) threadDelay 100000 putStrLn "Done." }}} Here we get: {{{ *Main> :main False (immediately) Done. }}} When we would expect: {{{ *Main> :main True (after slight delay) Done. }}} I only bring all this up in this ticket as I believe the oversight of the issue in this ticket may have been due to attempts to get [D8] right. I will see if I can address this ticket directly without resolving these other issue with a fix that will work with an eventual resolution of these additional issues. The new issues are harder to fix as it will require a change to `alwaysSucceeds` as we need to distinguish between a {{{retry}}} to rollback the effects and a {{{retry}}} with semantic meaning for the invariant. Additionally it will require some clarification to the semantics. I'm no expert in reading semantics but it appears to me that there should be a CHECK3 that specifies what happens when the term transitions to a {{{retry}}} in the context of a {{{check}}}. My reading of the paper is that the intent was for {{{check retry ==> retry}}}. This I think clarifies all three points above with {{{retry}}} in check catchable it its initial run, but not at commit time, and no delay in seeing a {{{retry}}}. [1]: Harris, Tim, and Simon Peyton Jones. "Transactional memory with data invariants." First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT’06), Ottowa. 2006. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7930#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#7930: Nested STM Invariants are lost ---------------------------------+------------------------------------------ Reporter: fryguybob | Owner: fryguybob Type: bug | Status: new Priority: normal | Milestone: Component: Runtime System | Version: 7.6.3 Keywords: STM | Os: Unknown/Multiple Architecture: Unknown/Multiple | Failure: Incorrect result at runtime Difficulty: Unknown | Testcase: Blockedby: | Blocking: Related: | ---------------------------------+------------------------------------------ Comment(by timharris): Hi -- here are some comments I sent Simon earlier. I do not usually use Trac, but feel free to contact me on e-mail, tim.harris@gmail.com --Tim The initial comment re invariants_to_check sounds correct. I think we added nested transactions after adding invariants. I don't remember thinking about the interaction before, but retaining the invariants from within a nested transactions sounds correct (since, in the absence of exceptions in X, I would expect catch X Y to behave like X). The other cases are more complex. I don't think the descriptions I wrote for the functions are very clear. e.g., for alwaysSucceeds, exactly what it means for an invariant to be true (Returns true? Does not throw? Does not retry? What if it loops?) I think the bug report's authors understand all these problems. I'd probably go back to the semantics in Fig 4 of http://timharris.co.uk/papers/2006-transact.pdf and write the functions descriptions again based on that, and then fix up the code as necessary. "check X" in the semantics is intended to be "always X" in the code. "check X" will throw if X throws, and retry if X retries. It tests X in this way immediately, and then again on the commit of each transaction (including the current one). I don't think the current code implements this correctly. With "always X" fixed, I'd then define "alwaysSucceeds X" in terms of "always" rather than vice-versa. (I think it should just be always ( X >> return true).) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7930#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler