Merge pull request #867 from GaloisInc/issue856

Fix race conditions in thunk evaluation

cryptol.cabal

@@ -66,6 +66,7 @@ library
                        random            >= 1.0.1,
                        sbv               >= 8.6,
                        simple-smt        >= 0.7.1,
+                       stm               >= 2.4,
                        strict,
                        text              >= 1.1,
                        tf-random         >= 0.5,

src/Cryptol/Eval/Concrete.hs

@@ -20,7 +20,7 @@
 {-# LANGUAGE ViewPatterns #-}
 module Cryptol.Eval.Concrete
   ( module Cryptol.Eval.Concrete.Value
-  , evalPrim
+  , primTable
   , toExpr
   ) where
 
@@ -131,11 +131,8 @@ floatToExpr prims eT pT f =
 
 -- Primitives ------------------------------------------------------------------
 
-evalPrim :: PrimIdent -> Maybe Value
-evalPrim prim = Map.lookup prim primTable
-
-primTable :: Map.Map PrimIdent Value
-primTable = let sym = Concrete in
+primTable :: EvalOpts -> Map.Map PrimIdent Value
+primTable eOpts = let sym = Concrete in
   Map.union (floatPrims sym) $
   Map.fromList $ map (\(n, v) -> (prelPrim n, v))
 
@@ -324,7 +321,7 @@ primTable = let sym = Concrete in
                       lam $ \x -> return $
                       lam $ \y -> do
                          msg <- valueToString sym =<< s
-                         EvalOpts { evalPPOpts, evalLogger } <- getEvalOpts
+                         let EvalOpts { evalPPOpts, evalLogger } = eOpts
                          doc <- ppValue sym evalPPOpts =<< x
                          yv <- y
                          io $ logPrint evalLogger

src/Cryptol/Eval/Monad.hs

@@ -9,14 +9,14 @@
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 
 module Cryptol.Eval.Monad
 ( -- * Evaluation monad
   Eval(..)
 , runEval
 , EvalOpts(..)
-, getEvalOpts
 , PPOpts(..)
 , PPFloatFormat(..)
 , PPFloatExp(..)
@@ -26,6 +26,7 @@ module Cryptol.Eval.Monad
 , ready
 , blackhole
 , evalSpark
+, maybeReady
   -- * Error reporting
 , Unsupported(..)
 , EvalError(..)
@@ -34,13 +35,13 @@ module Cryptol.Eval.Monad
 , typeCannotBeDemoted
 ) where
 
-import           Control.Concurrent.Async
-import           Control.DeepSeq
+import           Control.Concurrent
+import           Control.Concurrent.STM
+
 import           Control.Monad
 import qualified Control.Monad.Fail as Fail
 import           Control.Monad.Fix
 import           Control.Monad.IO.Class
-import           Data.IORef
 import           Data.Typeable (Typeable)
 import qualified Control.Exception as X
 
@@ -85,23 +86,69 @@ data EvalOpts = EvalOpts
   , evalPPOpts :: PPOpts    -- ^ How to pretty print things.
   }
 
-
 -- | The monad for Cryptol evaluation.
+--   A computation is either "ready", which means it represents
+--   only trivial computation, or is an "eval" action which must
+--   be computed to get the answer, or it is a "thunk", which
+--   represents a delayed, shared computation.
 data Eval a
    = Ready !a
-   | Thunk !(EvalOpts -> IO a)
-
+   | Eval !(IO a)
+   | Thunk !(TVar (ThunkState a))
+
+-- | This datastructure tracks the lifecycle of a thunk.
+--
+--   Thunks are used for basically three use cases.  First,
+--   we use thunks to preserve sharing.  Basically every
+--   cryptol expression that is bound to a name, and is not
+--   already obviously a value (and in a few other places as
+--   well) will get turned into a thunk in order to avoid
+--   recomputations.  These thunks will start in the `Unforced`
+--   state, and have a backup computation that just raises
+--   the `LoopError` exception.
+--
+--   Secondly, thunks are used to cut cycles when evaluating
+--   recursive definition groups.  Every named clause in a
+--   recursive definition is thunked so that the value can appear
+--   in its definition.  Such thunks start in the `Void` state,
+--   as they must exist before we have a definition to assign them.
+--   Forcing a thunk in the `Void` state is a programmer error (panic).
+--   Once the body of a definition is ready, we replace the
+--   thunk with the relevant computation, going to the `Unforced` state.
+--
+--   In the third case, we are using thunks to provide an optimistic
+--   shortcut for evaluation.  In these cases we first try to run a
+--   computation that is stricter than the semantics actually allows.
+--   If it succeeds, all is well an we continue.  However, if it tight
+--   loops, we fall back on a lazier (and generally more expensive)
+--   version, which is the "backup" computation referred to above.
 data ThunkState a
-  = Unforced        -- ^ This thunk has not yet been forced
-  | BlackHole       -- ^ This thunk is currently being evaluated
-  | Forced !(Either EvalError a)
-    -- ^ This thunk has previously been forced,
-    -- and has the given value, or evaluation resulted in an error.
-
-
--- | Access the evaluation options.
-getEvalOpts :: Eval EvalOpts
-getEvalOpts = Thunk pure
+  = Void !String
+       -- ^ This thunk has not yet been initialized
+  | Unforced !(IO a) !(IO a)
+       -- ^ This thunk has not yet been forced.  We keep track of the "main"
+       --   computation to run and a "backup" computation to run if we
+       --   detect a tight loop when evaluating the first one.
+  | UnderEvaluation !ThreadId !(IO a)
+       -- ^ This thunk is currently being evaluated by the thread with the given
+       --   thread ID.  We track the "backup" computation to run if we detect
+       --   a tight loop evaluating this thunk.  If the thunk is being evaluated
+       --   by some other thread, the current thread will await it's completion.
+  | ForcedErr !EvalError
+       -- ^ This thunk has been forced, and it's evaluation results in an exception
+  | Forced !a
+       -- ^ This thunk has been forced to the given value
+
+
+-- | Test if a value is "ready", which means that
+--   it requires no computation to return.
+maybeReady :: Eval a -> Eval (Maybe a)
+maybeReady (Ready a) = pure (Just a)
+maybeReady (Thunk tv) = Eval $
+  readTVarIO tv >>= \case
+     Forced a -> pure (Just a)
+     _ -> pure Nothing
+maybeReady (Eval _) = pure Nothing
 
 
 {-# INLINE delayFill #-}
@@ -114,22 +161,64 @@ delayFill ::
   Eval a {- ^ Computation to delay -} ->
   Eval a {- ^ Backup computation to run if a tight loop is detected -} ->
   Eval (Eval a)
-delayFill (Ready x) _ = Ready (Ready x)
-delayFill (Thunk x) retry = Thunk $ \opts -> do
-  r <- newIORef Unforced
-  return $ unDelay retry r (x opts)
-
+delayFill e@(Ready _) _  = return e
+delayFill e@(Thunk _) _  = return e
+delayFill (Eval x) backup = Eval (Thunk <$> newTVarIO (Unforced x (runEval backup)))
 
 -- | Begin executing the given operation in a separate thread,
 --   returning a thunk which will await the completion of
 --   the computation when forced.
 evalSpark ::
   Eval a ->
   Eval (Eval a)
-evalSpark (Ready x) = Ready (Ready x)
-evalSpark (Thunk x) = Thunk $ \opts ->
-  do a <- async (x opts)
-     return (Thunk $ \_ -> wait a)
+
+-- Ready computations need no additional evaluation.
+evalSpark e@(Ready _) = return e
+
+-- A thunked computation might already have
+-- been forced.  If so, return the result.  Otherwise,
+-- fork a thread to force this computation and return
+-- the thunk.
+evalSpark (Thunk tv)  = Eval $
+  readTVarIO tv >>= \case
+    Forced x     -> return (Ready x)
+    ForcedErr ex -> return (Eval (X.throwIO ex))
+    _ ->
+       do _ <- forkIO (sparkThunk tv)
+          return (Thunk tv)
+
+-- If the computation is nontrivial but not already a thunk,
+-- create a thunk and fork a thread to force it.
+evalSpark (Eval x) = Eval $
+  do tv <- newTVarIO (Unforced x (X.throwIO (LoopError "")))
+     _ <- forkIO (sparkThunk tv)
+     return (Thunk tv)
+
+
+-- | To the work of forcing a thunk. This is the worker computation
+--   that is foked off via @evalSpark@.
+sparkThunk :: TVar (ThunkState a) -> IO ()
+sparkThunk tv =
+  do tid <- myThreadId
+     -- Try to claim the thunk.  If it is still in the @Void@ state, wait
+     -- until it is in some other state.  If it is @Unforced@ claim the thunk.
+     -- Otherwise, it is already evaluated or under evaluation by another thread,
+     -- and we have no work to do.
+     st <- atomically $
+              do st <- readTVar tv
+                 case st of
+                   Void _ -> retry
+                   Unforced _ backup -> writeTVar tv (UnderEvaluation tid backup)
+                   _ -> return ()
+                 return st
+     -- If we successfully claimed the thunk to work on, run the computation and
+     -- update the thunk state with the result.
+     case st of
+       Unforced work _ ->
+         X.try work >>= \case
+           Left err -> atomically (writeTVar tv (ForcedErr err))
+           Right a  -> atomically (writeTVar tv (Forced a))
+       _ -> return ()
 
 
 -- | Produce a thunk value which can be filled with its associated computation
@@ -139,43 +228,76 @@ evalSpark (Thunk x) = Thunk $ \opts ->
 blackhole ::
   String {- ^ A name to associate with this thunk. -} ->
   Eval (Eval a, Eval a -> Eval ())
-blackhole msg = do
-  r <- io $ newIORef (fail msg)
-  let get = join (io $ readIORef r)
-  let set = io . writeIORef r
-  return (get, set)
-
-unDelay :: Eval a -> IORef (ThunkState a) -> IO a -> Eval a
-unDelay retry r x = do
-  rval <- io $ readIORef r
-  case rval of
-    Forced val -> io (toVal val)
-    BlackHole  ->
-      retry
-    Unforced -> io $ do
-      writeIORef r BlackHole
-      val <- X.try x
-      writeIORef r (Forced val)
-      toVal val
-
-  where
-  toVal mbV = case mbV of
-                Right a -> pure a
-                Left e  -> X.throwIO e
+blackhole msg = Eval $
+  do tv <- newTVarIO (Void msg)
+     let set (Ready x)  = io $ atomically (writeTVar tv (Forced x))
+         set m          = io $ atomically (writeTVar tv (Unforced (runEval m) (X.throwIO (LoopError msg))))
+     return (Thunk tv, set)
+
+-- | Force a thunk to get the result.
+unDelay :: TVar (ThunkState a) -> IO a
+unDelay tv =
+  -- First, check if the thunk is in an evaluated state,
+  -- and return the value if so.
+  readTVarIO tv >>= \case
+    Forced x -> pure x
+    ForcedErr e -> X.throwIO e
+    _ ->
+      -- Otherwise, try to claim the thunk to work on.
+      do tid <- myThreadId
+         res <- atomically $ do
+                  res <- readTVar tv
+                  case res of
+                    -- In this case, we claim the thunk.  Update the state to indicate
+                    -- that we are working on it.
+                    Unforced nm backup -> writeTVar tv (UnderEvaluation tid backup)
+
+                    -- In this case, the thunk is already being evaluated.  If it is
+                    -- under evaluation by this thread, we have to run the backup computation,
+                    -- and "consume" it by updating the backup computation to one that throws
+                    -- a loop error.  If some other thread is evaluating, reset the
+                    -- transaction to await completion of the thunk.
+                    UnderEvaluation t _
+                      | tid == t  -> writeTVar tv (UnderEvaluation tid (X.throwIO (LoopError "")))
+                      | otherwise -> retry -- wait, if some other thread is evaualting
+                    _ -> return ()
+
+                  -- Return the original thunk state so we can decide what work to do
+                  -- after the transaction completes.
+                  return res
+
+         -- helper for actually doing the work
+         let doWork work =
+               X.try work >>= \case
+                 Left ex -> do atomically (writeTVar tv (ForcedErr ex))
+                               X.throwIO ex
+                 Right a -> do atomically (writeTVar tv (Forced a))
+                               return a
+
+         -- Now, examine the thunk state and decide what to do.
+         case res of
+           Void msg -> evalPanic "unDelay" ["Thunk forced before it was initialized", msg]
+           Forced x -> pure x
+           ForcedErr e -> X.throwIO e
+           UnderEvaluation _ backup -> doWork backup -- this thread was already evaluating this thunk
+           Unforced work _ -> doWork work
 
 -- | Execute the given evaluation action.
-runEval :: EvalOpts -> Eval a -> IO a
-runEval _ (Ready a) = return a
-runEval opts (Thunk x) = x opts
+runEval :: Eval a -> IO a
+runEval (Ready a)  = return a
+runEval (Eval x)   = x
+runEval (Thunk tv) = unDelay tv
 
 {-# INLINE evalBind #-}
 evalBind :: Eval a -> (a -> Eval b) -> Eval b
 evalBind (Ready a) f  = f a
-evalBind (Thunk x) f  = Thunk $ \opts -> x opts >>= runEval opts . f
+evalBind (Eval x) f   = Eval (x >>= runEval . f)
+evalBind (Thunk x) f  = Eval (unDelay x >>= runEval . f)
 
 instance Functor Eval where
-  fmap f (Ready x) = Ready (f x)
-  fmap f (Thunk m) = Thunk $ \opts -> f <$> m opts
+  fmap f (Ready x)   = Ready (f x)
+  fmap f (Eval m)    = Eval (f <$> m)
+  fmap f (Thunk tv)  = Eval (f <$> unDelay tv)
   {-# INLINE fmap #-}
 
 instance Applicative Eval where
@@ -191,21 +313,17 @@ instance Monad Eval where
   {-# INLINE (>>=) #-}
 
 instance Fail.MonadFail Eval where
-  fail x = Thunk (\_ -> fail x)
+  fail x = Eval (fail x)
 
 instance MonadIO Eval where
   liftIO = io
 
-instance NFData a => NFData (Eval a) where
-  rnf (Ready a) = rnf a
-  rnf (Thunk _) = ()
-
 instance MonadFix Eval where
-  mfix f = Thunk $ \opts -> mfix (\x -> runEval opts (f x))
+  mfix f = Eval $ mfix (\x -> runEval (f x))
 
 -- | Lift an 'IO' computation into the 'Eval' monad.
 io :: IO a -> Eval a
-io m = Thunk (\_ -> m)
+io m = Eval m
 {-# INLINE io #-}
 
 

src/Cryptol/Eval/SBV.hs

@@ -18,7 +18,7 @@
 module Cryptol.Eval.SBV
   ( SBV(..), Value
   , SBVEval(..), SBVResult(..)
-  , evalPrim
+  , primTable
   , forallBV_, existsBV_
   , forallSBool_, existsSBool_
   , forallSInteger_, existsSInteger_
@@ -356,9 +356,6 @@ evalPanic cxt = panic ("[Symbolic]" ++ cxt)
 
 -- Primitives ------------------------------------------------------------------
 
-evalPrim :: PrimIdent -> Maybe Value
-evalPrim prim = Map.lookup prim primTable
-
 -- See also Cryptol.Eval.Concrete.primTable
 primTable :: Map.Map PrimIdent Value
 primTable  = let sym = SBV in