[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                      
    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 at 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