dejafu 0.5.1.0 → 0.5.1.1

raw patch · 4 files changed

+74/−52 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Test/DejaFu/Conc.hs +1/−1
• Test/DejaFu/Conc/Internal.hs +70/−48
• Test/DejaFu/SCT/Internal.hs +1/−1
• dejafu.cabal +2/−2

@@ -177,7 +177,7 @@               -> Conc n r a               -> n (Either Failure a, s, Trace) runConcurrent sched memtype s ma = do-  (res, s', trace) <- runConcurrency sched memtype s 2 (unC ma)+  (res, s', trace, _) <- runConcurrency sched memtype s 2 (unC ma)   pure (res, s', F.toList trace)  -- | Run a concurrent computation and return its result.

@@ -53,7 +53,7 @@                -> g                -> Int                -> M n r a-               -> n (Either Failure a, g, SeqTrace)+               -> n (Either Failure a, g, SeqTrace, Maybe (ThreadId, ThreadAction)) runConcurrency sched memtype g caps ma = do   ref <- newRef Nothing @@ -61,9 +61,9 @@   let threads = launch' Unmasked initialThread (const c) M.empty   let ctx = Context { cSchedState = g, cIdSource = initialIdSource, cThreads = threads, cWriteBuf = emptyBuffer, cCaps = caps } -  (finalCtx, trace) <- runThreads sched memtype ref ctx+  (finalCtx, trace, finalAction) <- runThreads sched memtype ref ctx   out <- readRef ref-  pure (fromJust out, cSchedState finalCtx, trace)+  pure (fromJust out, cSchedState finalCtx, trace, finalAction)  -- | The context a collection of threads are running in. data Context n r g = Context@@ -76,25 +76,36 @@  -- | Run a collection of threads, until there are no threads left. runThreads :: MonadRef r n-           => Scheduler g -> MemType -> r (Maybe (Either Failure a)) -> Context n r g -> n (Context n r g, SeqTrace)+           => Scheduler g -> MemType -> r (Maybe (Either Failure a)) -> Context n r g -> n (Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction)) runThreads sched memtype ref = go Seq.empty [] Nothing where   -- sofar is the 'SeqTrace', sofarSched is the @[(Decision,   -- ThreadAction)]@ trace the scheduler needs.   go sofar sofarSched prior ctx-    | isTerminated  = stop ctx-    | isDeadlocked  = die Deadlock ctx-    | isSTMLocked   = die STMDeadlock ctx-    | isAborted     = die Abort $ ctx { cSchedState = g' }-    | isNonexistant = die InternalError $ ctx { cSchedState = g' }-    | isBlocked     = die InternalError $ ctx { cSchedState = g' }+    | isTerminated  = stop prior ctx+    | isDeadlocked  = die prior Deadlock ctx+    | isSTMLocked   = die prior STMDeadlock ctx+    | isAborted     = die prior Abort $ ctx { cSchedState = g' }+    | isNonexistant = die prior InternalError $ ctx { cSchedState = g' }+    | isBlocked     = die prior InternalError $ ctx { cSchedState = g' }     | otherwise = do       stepped <- stepThread sched memtype chosen (_continuation $ fromJust thread) $ ctx { cSchedState = g' }       case stepped of-        Right (ctx', actOrTrc) -> loop actOrTrc ctx'-        Left UncaughtException-          | chosen == initialThread -> die UncaughtException $ ctx { cSchedState = g' }-          | otherwise -> loop (Right Killed) $ ctx { cThreads = kill chosen threadsc, cSchedState = g' }-        Left failure -> die failure $ ctx { cSchedState = g' }+        (Right ctx', actOrTrc) ->+          let (sofar', sofarSched', prior', ctx'') = setupNext actOrTrc ctx'+          in go sofar' sofarSched' prior' ctx''+        (Left UncaughtException, actOrTrc)+          | chosen == initialThread ->+              let ctx' = ctx { cSchedState = g' }+                  (_, _, prior', ctx'') = setupNext actOrTrc ctx'+              in die prior' UncaughtException ctx''+          | otherwise ->+              let ctx' = ctx { cThreads = kill chosen threadsc, cSchedState = g' }+                  (sofar', sofarSched', prior', ctx'') = setupNext actOrTrc ctx'+              in go sofar' sofarSched' prior' ctx''+        (Left failure, actOrTrc) ->+          let ctx' = ctx { cSchedState = g' }+              (_, _, prior', ctx'') = setupNext actOrTrc ctx'+          in die prior' failure ctx''      where       (choice, g')  = sched sofarSched prior (fromList $ map (\(t,l:|_) -> (t,l)) runnable') (cSchedState ctx)@@ -127,24 +138,34 @@        nextActions t = lookahead . _continuation . fromJust $ M.lookup t threadsc -      stop finalCtx = pure (finalCtx, sofar)-      die reason finalCtx = writeRef ref (Just $ Left reason) >> stop finalCtx+      stop finalDecision finalCtx = pure (finalCtx, sofar, finalDecision)+      die finalDecision reason finalCtx = writeRef ref (Just $ Left reason) >> stop finalDecision finalCtx -      loop trcOrAct ctx' =+      setupNext trcOrAct ctx' =         let (act, trc) = case trcOrAct of-              Left (a, as) -> (a, (decision, runnable', a) <| as)-              Right a      -> (a, Seq.singleton (decision, runnable', a))+              Single a    -> (a, Seq.singleton (decision, runnable', a))+              SubC   as _ -> (Subconcurrency, (decision, runnable', Subconcurrency) <| as)             threads' = if (interruptible <$> M.lookup chosen (cThreads ctx')) /= Just False                        then unblockWaitingOn chosen (cThreads ctx')                        else cThreads ctx'             sofar' = sofar <> trc             sofarSched' = sofarSched <> map (\(d,_,a) -> (d,a)) (F.toList trc)-            prior' = Just (chosen, act)-        in go sofar' sofarSched' prior' $ ctx' { cThreads = delCommitThreads threads' }+            prior' = case trcOrAct of+              Single _ -> Just (chosen, act)+              SubC _ finalD -> finalD+        in (sofar', sofarSched', prior', ctx' { cThreads = delCommitThreads threads' })  -------------------------------------------------------------------------------- -- * Single-step execution +-- | What a thread did.+data Act+  = Single ThreadAction+  -- ^ Just one action.+  | SubC SeqTrace (Maybe (ThreadId, ThreadAction))+  -- ^ Subconcurrency, with the given trace and final action.+  deriving (Eq, Show)+ -- | Run a single thread one step, by dispatching on the type of -- 'Action'. stepThread :: forall n r g. MonadRef r n@@ -158,13 +179,13 @@   -- ^ Action to step   -> Context n r g   -- ^ The execution context.-  -> n (Either Failure (Context n r g, Either (ThreadAction, SeqTrace) ThreadAction))+  -> n (Either Failure (Context n r g), Act) stepThread sched memtype tid action ctx = case action of     -- start a new thread, assigning it the next 'ThreadId'-    AFork n a b -> pure . Right $+    AFork n a b -> pure $         let threads' = launch tid newtid a (cThreads ctx)             (idSource', newtid) = nextTId n (cIdSource ctx)-        in (ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Right (Fork newtid))+        in (Right ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }, Single (Fork newtid))      -- get the 'ThreadId' of the current thread     AMyTId c -> simple (goto (c tid) tid (cThreads ctx)) MyThreadId@@ -173,8 +194,8 @@     AGetNumCapabilities c -> simple (goto (c (cCaps ctx)) tid (cThreads ctx)) $ GetNumCapabilities (cCaps ctx)      -- set the number of capabilities-    ASetNumCapabilities i c -> pure . Right $-      (ctx { cThreads = goto c tid (cThreads ctx), cCaps = i }, Right (SetNumCapabilities i))+    ASetNumCapabilities i c -> pure+      (Right ctx { cThreads = goto c tid (cThreads ctx), cCaps = i }, Single (SetNumCapabilities i))      -- yield the current thread     AYield c -> simple (goto c tid (cThreads ctx)) Yield@@ -184,7 +205,7 @@       let (idSource', newmvid) = nextMVId n (cIdSource ctx)       ref <- newRef Nothing       let mvar = MVar newmvid ref-      pure $ Right (ctx { cThreads = goto (c mvar) tid (cThreads ctx), cIdSource = idSource' }, Right (NewMVar newmvid))+      pure (Right ctx { cThreads = goto (c mvar) tid (cThreads ctx), cIdSource = idSource' }, Single (NewMVar newmvid))      -- put a value into a @MVar@, blocking the thread until it's empty.     APutMVar cvar@(MVar cvid _) a c -> synchronised $ do@@ -224,7 +245,7 @@       let (idSource', newcrid) = nextCRId n (cIdSource ctx)       ref <- newRef (M.empty, 0, a)       let cref = CRef newcrid ref-      pure $ Right (ctx { cThreads = goto (c cref) tid (cThreads ctx), cIdSource = idSource' }, Right (NewCRef newcrid))+      pure (Right ctx { cThreads = goto (c cref) tid (cThreads ctx), cIdSource = idSource' }, Single (NewCRef newcrid))      -- read from a @CRef@.     AReadCRef cref@(CRef crid _) c -> do@@ -258,11 +279,11 @@       -- add to buffer using thread id.       TotalStoreOrder -> do         wb' <- bufferWrite (cWriteBuf ctx) (tid, Nothing) cref a-        pure $ Right (ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Right (WriteCRef crid))+        pure (Right ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Single (WriteCRef crid))       -- add to buffer using both thread id and cref id       PartialStoreOrder -> do         wb' <- bufferWrite (cWriteBuf ctx) (tid, Just crid) cref a-        pure $ Right (ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Right (WriteCRef crid))+        pure (Right ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Single (WriteCRef crid))      -- perform a compare-and-swap on a @CRef@.     ACasCRef cref@(CRef crid _) tick a c -> synchronised $ do@@ -279,7 +300,7 @@         TotalStoreOrder -> commitWrite (cWriteBuf ctx) (t, Nothing)         -- commit using the cref id.         PartialStoreOrder -> commitWrite (cWriteBuf ctx) (t, Just c)-      pure $ Right (ctx { cWriteBuf = wb' }, Right (CommitCRef t c))+      pure (Right ctx { cWriteBuf = wb' }, Single (CommitCRef t c))      -- run a STM transaction atomically.     AAtom stm c -> synchronised $ do@@ -287,15 +308,16 @@       case res of         Success _ written val ->           let (threads', woken) = wake (OnTVar written) (cThreads ctx)-          in pure $ Right (ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }, Right (STM trace woken))+          in pure (Right ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }, Single (STM trace woken))         Retry touched ->           let threads' = block (OnTVar touched) tid (cThreads ctx)-          in pure $ Right (ctx { cThreads = threads', cIdSource = idSource'}, Right (BlockedSTM trace))+          in pure (Right ctx { cThreads = threads', cIdSource = idSource'}, Single (BlockedSTM trace))         Exception e -> do-          res' <- stepThrow e+          let act = STM trace []+          res' <- stepThrow act e           pure $ case res' of-            Right (ctx', _) -> Right (ctx' { cIdSource = idSource' }, Right Throw)-            Left err -> Left err+            (Right ctx', _) -> (Right ctx' { cIdSource = idSource' }, Single act)+            (Left err, _) -> (Left err, Single act)      -- lift an action from the underlying monad into the @Conc@     -- computation.@@ -305,7 +327,7 @@      -- throw an exception, and propagate it to the appropriate     -- handler.-    AThrow e -> stepThrow e+    AThrow e -> stepThrow Throw e      -- throw an exception to the target thread, and propagate it to     -- the appropriate handler.@@ -317,7 +339,7 @@              | interruptible thread -> case propagate (toException e) t threads' of                Just threads'' -> simple threads'' $ ThrowTo t                Nothing-                 | t == initialThread -> pure $ Left UncaughtException+                 | t == initialThread -> pure (Left UncaughtException, Single (ThrowTo t))                  | otherwise -> simple (kill t threads') $ ThrowTo t              | otherwise -> simple blocked $ BlockedThrowTo t            Nothing -> simple threads' $ ThrowTo t@@ -359,10 +381,10 @@      -- run a subconcurrent computation.     ASub ma c-      | M.size (cThreads ctx) > 1 -> pure (Left IllegalSubconcurrency)+      | M.size (cThreads ctx) > 1 -> pure (Left IllegalSubconcurrency, Single Subconcurrency)       | otherwise -> do-          (res, g', trace) <- runConcurrency sched memtype (cSchedState ctx) (cCaps ctx) ma-          pure $ Right (ctx { cThreads = goto (AStopSub (c res)) tid (cThreads ctx), cSchedState = g' }, Left (Subconcurrency, trace))+          (res, g', trace, finalDecision) <- runConcurrency sched memtype (cSchedState ctx) (cCaps ctx) ma+          pure (Right ctx { cThreads = goto (AStopSub (c res)) tid (cThreads ctx), cSchedState = g' }, SubC trace finalDecision)      -- after the end of a subconcurrent computation. does nothing,     -- only exists so that: there is an entry in the trace for@@ -373,19 +395,19 @@      -- this is not inline in the long @case@ above as it's needed by     -- @AAtom@, @AThrow@, and @AThrowTo@.-    stepThrow e =+    stepThrow act e =       case propagate (toException e) tid (cThreads ctx) of-        Just threads' -> simple threads' Throw-        Nothing -> pure $ Left UncaughtException+        Just threads' -> simple threads' act+        Nothing -> pure (Left UncaughtException, Single act)      -- helper for actions which only change the threads.-    simple threads' act = pure $ Right (ctx { cThreads = threads' }, Right act)+    simple threads' act = pure (Right ctx { cThreads = threads' }, Single act)      -- helper for actions impose a write barrier.     synchronised ma = do       writeBarrier (cWriteBuf ctx)       res <- ma -      return $ case res of-        Right (ctx', act) -> Right (ctx' { cWriteBuf = emptyBuffer }, act)+      pure $ case res of+        (Right ctx', act) -> (Right ctx' { cWriteBuf = emptyBuffer }, act)         _ -> res

@@ -167,7 +167,7 @@                    , dporTodo  = M.delete tid' (dporTodo dpor)                    , dporDone  = done                    }-  grow _ _ [] dpor = dpor+  grow _ _ [] _ = err "incorporateTrace" "trace exhausted without reading a to-do point!"    -- Construct a new subtree corresponding to a trace suffix.   subtree state tid sleep ((_, _, a):rest) =

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             0.5.1.0+version:             0.5.1.1 synopsis:            Systematic testing for Haskell concurrency.  description:@@ -74,7 +74,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-0.5.1.0+  tag:      dejafu-0.5.1.1  library   exposed-modules:     Test.DejaFu