dejafu 0.7.1.0 → 0.7.1.1

raw patch · 7 files changed

+115/−93 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +20/−0
• Test/DejaFu/Conc/Internal.hs +1/−1
• Test/DejaFu/Conc/Internal/Memory.hs +22/−18
• Test/DejaFu/Conc/Internal/Threading.hs +6/−8
• Test/DejaFu/SCT.hs +6/−5
• Test/DejaFu/SCT/Internal.hs +58/−59
• dejafu.cabal +2/−2

@@ -6,6 +6,26 @@ This project is versioned according to the [Package Versioning Policy](https://pvp.haskell.org), the *de facto* standard Haskell versioning scheme. ++0.7.1.1 [2017-08-16] (git tag: [dejafu-0.7.1.1][])+-------++https://hackage.haskell.org/package/dejafu-0.7.1.1++### Miscellaneous++- Significantly reduced memory usage in systematic testing when discarding traces.++    Previously this was `O(max trace length * number of executions)`++    Now it's `O(max trace length + total size of traces kept)`++[dejafu-0.7.1.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.1.1+++---------------------------------------------------------------------------------------------------++ 0.7.1.0 [2017-08-10] (git tag: [dejafu-0.7.1.0][]) ------- 

@@ -8,7 +8,7 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : RankNTypes, ScopedTypeVariables+-- Portability : MultiParamTypeClasses, RankNTypes, ScopedTypeVariables -- -- Concurrent monads with a fixed scheduler: internal types and -- functions. This module is NOT considered to form part of the public

@@ -8,7 +8,7 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : BangPatterns, GADTs+-- Portability : BangPatterns, GADTs, MultiParamTypeClasses -- -- Operations over @CRef@s and @MVar@s. This module is NOT considered -- to form part of the public interface of this library.@@ -144,50 +144,53 @@ -------------------------------------------------------------------------------- -- * Manipulating @MVar@s +-- these are a bit clearer than a Bool+data Blocking = Blocking | NonBlocking+data Emptying = Emptying | NonEmptying+ -- | Put into a @MVar@, blocking if full. putIntoMVar :: MonadRef r n => MVar r a -> a -> Action n r             -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])-putIntoMVar cvar a c = mutMVar True cvar a (const c)+putIntoMVar cvar a c = mutMVar Blocking cvar a (const c)  -- | Try to put into a @MVar@, not blocking if full. tryPutIntoMVar :: MonadRef r n => MVar r a -> a -> (Bool -> Action n r)                -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])-tryPutIntoMVar = mutMVar False+tryPutIntoMVar = mutMVar NonBlocking  -- | Read from a @MVar@, blocking if empty. readFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r)             -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])-readFromMVar cvar c = seeMVar False True cvar (c . fromJust)+readFromMVar cvar c = seeMVar NonEmptying Blocking cvar (c . fromJust)  -- | Try to read from a @MVar@, not blocking if empty. tryReadFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r)                 -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])-tryReadFromMVar = seeMVar False False+tryReadFromMVar = seeMVar NonEmptying NonBlocking  -- | Take from a @MVar@, blocking if empty. takeFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r)              -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])-takeFromMVar cvar c = seeMVar True True cvar (c . fromJust)+takeFromMVar cvar c = seeMVar Emptying Blocking cvar (c . fromJust)  -- | Try to take from a @MVar@, not blocking if empty. tryTakeFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r)                 -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])-tryTakeFromMVar = seeMVar True False+tryTakeFromMVar = seeMVar Emptying NonBlocking  -- | Mutate a @MVar@, in either a blocking or nonblocking way. mutMVar :: MonadRef r n-        => Bool -> MVar r a -> a -> (Bool -> Action n r)+        => Blocking -> MVar r a -> a -> (Bool -> Action n r)         -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId]) mutMVar blocking (MVar cvid ref) a c threadid threads = do   val <- readRef ref    case val of-    Just _-      | blocking ->+    Just _ -> case blocking of+      Blocking ->         let threads' = block (OnMVarEmpty cvid) threadid threads         in pure (False, threads', [])--      | otherwise ->+      NonBlocking ->         pure (False, goto (c False) threadid threads, [])      Nothing -> do@@ -198,21 +201,22 @@ -- | Read a @MVar@, in either a blocking or nonblocking -- way. seeMVar :: MonadRef r n-        => Bool -> Bool -> MVar r a -> (Maybe a -> Action n r)+        => Emptying -> Blocking -> MVar r a -> (Maybe a -> Action n r)         -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId]) seeMVar emptying blocking (MVar cvid ref) c threadid threads = do   val <- readRef ref    case val of     Just _ -> do-      when emptying $ writeRef ref Nothing+      case emptying of+        Emptying    -> writeRef ref Nothing+        NonEmptying -> pure ()       let (threads', woken) = wake (OnMVarEmpty cvid) threads       pure (True, goto (c val) threadid threads', woken) -    Nothing-      | blocking ->+    Nothing -> case blocking of+      Blocking ->         let threads' = block (OnMVarFull cvid) threadid threads         in pure (False, threads', [])--      | otherwise ->+      NonBlocking ->         pure (False, goto (c Nothing) threadid threads, [])

@@ -85,26 +85,26 @@  -- | Register a new exception handler. catching :: Exception e => (e -> Action n r) -> ThreadId -> Threads n r -> Threads n r-catching h = M.alter $ \(Just thread) -> Just $ thread { _handlers = Handler h : _handlers thread }+catching h = M.adjust $ \thread -> thread { _handlers = Handler h : _handlers thread }  -- | Remove the most recent exception handler. uncatching :: ThreadId -> Threads n r -> Threads n r-uncatching = M.alter $ \(Just thread) -> Just $ thread { _handlers = tail $ _handlers thread }+uncatching = M.adjust $ \thread -> thread { _handlers = tail $ _handlers thread }  -- | Raise an exception in a thread. except :: Action n r -> [Handler n r] -> ThreadId -> Threads n r -> Threads n r-except act hs = M.alter $ \(Just thread) -> Just $ thread { _continuation = act, _handlers = hs, _blocking = Nothing }+except act hs = M.adjust $ \thread -> thread { _continuation = act, _handlers = hs, _blocking = Nothing }  -- | Set the masking state of a thread. mask :: MaskingState -> ThreadId -> Threads n r -> Threads n r-mask ms = M.alter $ \(Just thread) -> Just $ thread { _masking = ms }+mask ms = M.adjust $ \thread -> thread { _masking = ms }  -------------------------------------------------------------------------------- -- * Manipulating threads  -- | Replace the @Action@ of a thread. goto :: Action n r -> ThreadId -> Threads n r -> Threads n r-goto a = M.alter $ \(Just thread) -> Just (thread { _continuation = a })+goto a = M.adjust $ \thread -> thread { _continuation = a }  -- | Start a thread with the given ID, inheriting the masking state -- from the parent thread. This ID must not already be in use!@@ -126,9 +126,7 @@  -- | Block a thread. block :: BlockedOn -> ThreadId -> Threads n r -> Threads n r-block blockedOn = M.alter doBlock where-  doBlock (Just thread) = Just $ thread { _blocking = Just blockedOn }-  doBlock _ = error "Invariant failure in 'block': thread does NOT exist!"+block blockedOn = M.adjust $ \thread -> thread { _blocking = Just blockedOn }  -- | Unblock all threads waiting on the appropriate block. For 'TVar' -- blocks, this will wake all threads waiting on at least one of the

@@ -1,3 +1,4 @@+{-# LANGUAGE BangPatterns #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} @@ -7,7 +8,7 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : GADTs, GeneralizedNewtypeDeriving+-- Portability : BangPatterns, GADTs, GeneralizedNewtypeDeriving -- -- Systematic testing for concurrent computations. module Test.DejaFu.SCT@@ -106,7 +107,7 @@   ) where  import           Control.Applicative      ((<|>))-import           Control.DeepSeq          (NFData(..))+import           Control.DeepSeq          (NFData(..), force) import           Control.Monad.Ref        (MonadRef) import           Data.List                (foldl') import qualified Data.Map.Strict          as M@@ -492,7 +493,7 @@ sctBoundDiscard discard memtype cb conc = go initialState where   -- Repeatedly run the computation gathering all the results and   -- traces into a list until there are no schedules remaining to try.-  go dp = case findSchedulePrefix dp of+  go !dp = case findSchedulePrefix dp of     Just (prefix, conservative, sleep) -> do       (res, s, trace) <- runConcurrent scheduler                                        memtype@@ -503,8 +504,8 @@       let newDPOR = addTrace conservative trace dp        if schedIgnore s-        then go newDPOR-        else checkDiscard discard res trace $ go (addBacktracks bpoints newDPOR)+        then go (force newDPOR)+        else checkDiscard discard res trace $ go (force (addBacktracks bpoints newDPOR))      Nothing -> pure [] 

@@ -11,6 +11,7 @@ -- interface of this library. module Test.DejaFu.SCT.Internal where +import           Control.Applicative  ((<|>)) import           Control.DeepSeq      (NFData(..)) import           Control.Exception    (MaskingState(..)) import qualified Data.Foldable        as F@@ -42,8 +43,13 @@   , dporTodo     :: Map ThreadId Bool   -- ^ Follow-on decisions still to make, and whether that decision   -- was added conservatively due to the bound.-  , dporDone     :: Map ThreadId DPOR-  -- ^ Follow-on decisions that have been made.+  , dporNext     :: Maybe (ThreadId, DPOR)+  -- ^ The next decision made. Executions are explored in a+  -- depth-first fashion, so this changes as old subtrees are+  -- exhausted and new ones explored.+  , dporDone     :: Set ThreadId+  -- ^ All transitions which have been taken from this point,+  -- including conservatively-added ones.   , dporSleep    :: Map ThreadId ThreadAction   -- ^ Transitions to ignore (in this node and children) until a   -- dependent transition happens.@@ -51,18 +57,15 @@   -- ^ Transitions which have been taken, excluding   -- conservatively-added ones. This is used in implementing sleep   -- sets.-  , dporAction   :: Maybe ThreadAction-  -- ^ What happened at this step. This will be 'Nothing' at the root,-  -- 'Just' everywhere else.   } deriving (Eq, Show)  instance NFData DPOR where   rnf dpor = rnf ( dporRunnable dpor                  , dporTodo     dpor+                 , dporNext     dpor                  , dporDone     dpor                  , dporSleep    dpor                  , dporTaken    dpor-                 , dporAction   dpor                  )  -- | One step of the execution, including information for backtracking@@ -99,10 +102,10 @@ initialState = DPOR   { dporRunnable = S.singleton initialThread   , dporTodo     = M.singleton initialThread False-  , dporDone     = M.empty+  , dporNext     = Nothing+  , dporDone     = S.empty   , dporSleep    = M.empty   , dporTaken    = M.empty-  , dporAction   = Nothing   }  -- | Produce a new schedule prefix from a @DPOR@ tree. If there are no new@@ -117,24 +120,24 @@ findSchedulePrefix   :: DPOR   -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)-findSchedulePrefix = listToMaybe . go where-  go dpor =-    let prefixes = here dpor : map go' (M.toList $ dporDone dpor)-    in case concatPartition (\(t:_,_,_) -> t >= initialThread) prefixes of-         ([], choices) -> choices-         (choices, _)  -> choices--  go' (tid, dpor) = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> go dpor+findSchedulePrefix dpor = case dporNext dpor of+    Just (tid, child) -> go tid child <|> here+    Nothing -> here+  where+    go tid child = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> findSchedulePrefix child -  -- Prefix traces terminating with a to-do decision at this point.-  here dpor = [([t], c, sleeps dpor) | (t, c) <- M.toList $ dporTodo dpor]+    -- Prefix traces terminating with a to-do decision at this point.+    here =+      let todos = [([t], c, sleeps) | (t, c) <- M.toList $ dporTodo dpor]+          (best, worst) = partition (\([t],_,_) -> t >= initialThread) todos+      in listToMaybe best <|> listToMaybe worst -  -- The new sleep set is the union of the sleep set of the node we're-  -- branching from, plus all the decisions we've already explored.-  sleeps dpor = dporSleep dpor `M.union` dporTaken dpor+    -- The new sleep set is the union of the sleep set of the node+    -- we're branching from, plus all the decisions we've already+    -- explored.+    sleeps = dporSleep dpor `M.union` dporTaken dpor --- | Add a new trace to the tree, creating a new subtree branching off--- at the point where the \"to-do\" decision was made.+-- | Add a new trace to the stack.  This won't work if to-dos aren't explored depth-first. incorporateTrace   :: MemType   -- ^ Memory model@@ -150,20 +153,23 @@   grow state tid trc@((d, _, a):rest) dpor =     let tid'   = tidOf tid d         state' = updateDepState state tid' a-    in case M.lookup tid' (dporDone dpor) of-         Just dpor' ->-           let done = M.insert tid' (grow state' tid' rest dpor') (dporDone dpor)-           in dpor { dporDone = done }-         Nothing ->+    in case dporNext dpor of+         Just (t, child)+           | t == tid'      -> dpor { dporNext = Just (tid', grow state' tid' rest child) }+           | hasTodos child -> err "incorporateTrace" "replacing child with todos!"+         _ ->            let taken = M.insert tid' a (dporTaken dpor)                sleep = dporSleep dpor `M.union` dporTaken dpor-               done  = M.insert tid' (subtree state' tid' sleep trc) (dporDone dpor)            in dpor { dporTaken = if conservative then dporTaken dpor else taken                    , dporTodo  = M.delete tid' (dporTodo dpor)-                   , dporDone  = done+                   , dporNext  = Just (tid', subtree state' tid' sleep trc)+                   , dporDone  = S.insert tid' (dporDone dpor)                    }   grow _ _ [] _ = err "incorporateTrace" "trace exhausted without reading a to-do point!" +  -- check if there are to-do points in a tree+  hasTodos dpor = not (M.null (dporTodo dpor)) || (case dporNext dpor of Just (_, dpor') -> hasTodos dpor'; _ -> False)+   -- Construct a new subtree corresponding to a trace suffix.   subtree state tid sleep ((_, _, a):rest) =     let state' = updateDepState state tid a@@ -172,17 +178,19 @@         { dporRunnable = S.fromList $ case rest of             ((_, runnable, _):_) -> map fst runnable             [] -> []-        , dporTodo     = M.empty-        , dporDone     = M.fromList $ case rest of+        , dporTodo = M.empty+        , dporNext = case rest of           ((d', _, _):_) ->             let tid' = tidOf tid d'-            in  [(tid', subtree state' tid' sleep' rest)]-          [] -> []+            in  Just (tid', subtree state' tid' sleep' rest)+          [] -> Nothing+        , dporDone = case rest of+            ((d', _, _):_) -> S.singleton (tidOf tid d')+            [] -> S.empty         , dporSleep = sleep'         , dporTaken = case rest of           ((d', _, a'):_) -> M.singleton (tidOf tid d') a'           [] -> M.empty-        , dporAction = Just a         }   subtree _ _ _ [] = err "incorporateTrace" "subtree suffix empty!" @@ -282,24 +290,29 @@   -> DPOR   -> DPOR incorporateBacktrackSteps bv = go Nothing [] where-  go priorTid pref (b:bs) bpor =-    let bpor' = doBacktrack priorTid pref b bpor+  go priorTid pref (b:bs) dpor =+    let dpor' = doBacktrack priorTid pref b dpor         tid   = bcktThreadid b         pref' = pref ++ [(bcktDecision b, bcktAction b)]-        child = go (Just tid) pref' bs . fromJust $ M.lookup tid (dporDone bpor)-    in bpor' { dporDone = M.insert tid child $ dporDone bpor' }-  go _ _ [] bpor = bpor+        child = case dporNext dpor of+                  Just (t, d)+                    | t /= tid -> err "incorporateBacktrackSteps" "incorporating wrong trace!"+                    | otherwise -> go (Just t) pref' bs d+                  Nothing -> err "incorporateBacktrackSteps" "child is missing!"+    in dpor' { dporNext = Just (tid, child) }+  go _ _ [] dpor = dpor -  doBacktrack priorTid pref b bpor =+  doBacktrack priorTid pref b dpor =     let todo' = [ x                 | x@(t,c) <- M.toList $ bcktBacktracks b-                , let decision  = decisionOf priorTid (dporRunnable bpor) t+                , let decision  = decisionOf priorTid (dporRunnable dpor) t                 , let lahead = fromJust . M.lookup t $ bcktRunnable b                 , bv pref (decision, lahead)-                , t `notElem` M.keys (dporDone bpor)-                , c || M.notMember t (dporSleep bpor)+                , Just t /= (fst <$> dporNext dpor)+                , S.notMember t (dporDone dpor)+                , c || M.notMember t (dporSleep dpor)                 ]-    in bpor { dporTodo = dporTodo bpor `M.union` M.fromList todo' }+    in dpor { dporTodo = dporTodo dpor `M.union` M.fromList todo' }  ------------------------------------------------------------------------------- -- * DPOR scheduler@@ -795,17 +808,3 @@ -- | Internal errors. err :: String -> String -> a err func msg = error (func ++ ": (internal error) " ++ msg)---- | A combination of 'partition' and 'concat'.-concatPartition :: (a -> Bool) -> [[a]] -> ([a], [a])-{-# INLINE concatPartition #-}--- note: `foldr (flip (foldr select))` is slow, as is `foldl (foldl--- select))`, and `foldl'` variants. The sweet spot seems to be `foldl--- (foldr select)` for some reason I don't really understand.-concatPartition p = foldl (foldr select) ([], []) where-  -- Lazy pattern matching, got this trick from the 'partition'-  -- implementation. This reduces allocation fairly significantly; I-  -- do not know why.-  select a ~(ts, fs)-    | p a       = (a:ts, fs)-    | otherwise = (ts, a:fs)

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