2. The delay does not make sense because there are other effects that can intervene before the transaction is committed! Indeed, it could be
#7930: Nested STM Invariants are lost -------------------------------------+------------------------------------- Reporter: fryguybob | Owner: fryguybob Type: bug | Status: new Priority: normal | Milestone: Component: Runtime System | Version: 7.6.3 Resolution: | Keywords: STM Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result | Unknown/Multiple at runtime | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by int-e): Replying to [comment:1 fryguybob]: I believe the analysis is excellent. I only have some minor additional comments: 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).
In fact, the effect does not even have to be external to the transaction, as demonstrated by the following single threaded example, which completes successfully instead of getting stuck retrying the transaction: {{{ import Control.Concurrent.STM main = do atomically $ do t <- newTVar True alwaysSucceeds $ do b <- readTVar t if b then retry else return () writeTVar t False putStrLn "Success" }}} Interestingly, there is no CHECK rule for the `retry` case in the operational semantics (Figure 4 of [1]), which could well explain this oversight.
This definition attempts to reuse the `retry` mechanism to handle the rollback of the initial run of the invariant.
The rollback is (also?) necessary to ensure [D6]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/7930#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler