[GHC] #7930: Nested STM Invariants are lost

[GHC]

#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