[GHC] #7930: Nested STM Invariants are lost

[GHC]

#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:

 >  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).

 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