dejafu 0.4.0.0 → 0.5.0.0

raw patch · 11 files changed

+1726/−896 lines, 11 filesdep +randomdep −deepseqdep −dpordep ~concurrencyPVP ok

version bump matches the API change (PVP)

Dependencies added: random

Dependencies removed: deepseq, dpor

Dependency ranges changed: concurrency

API changes (from Hackage documentation)

Files

• Test/DejaFu.hs +131/−75
• Test/DejaFu/Common.hs +121/−180
• Test/DejaFu/Conc.hs +35/−45
• Test/DejaFu/Conc/Internal.hs +240/−241
• Test/DejaFu/Conc/Internal/Common.hs +54/−52
• Test/DejaFu/Conc/Internal/Memory.hs +21/−16
• Test/DejaFu/Conc/Internal/Threading.hs +19/−19
• Test/DejaFu/SCT.hs +258/−263
• Test/DejaFu/SCT/Internal.hs +712/−0
• Test/DejaFu/Schedule.hs +129/−0
• dejafu.cabal +6/−5

@@ -93,13 +93,16 @@    -- * Testing with different settings -  , autocheck'-  , autocheckIO'-  , dejafu'-  , dejafus'-  , dejafuIO'-  , dejafusIO'+  , Way(..)+  , defaultWay +  , autocheckWay+  , autocheckWayIO+  , dejafuWay+  , dejafuWayIO+  , dejafusWay+  , dejafusWayIO+   -- ** Memory Models    -- | Threads running under modern multicore processors do not behave@@ -133,7 +136,7 @@   --   -- We can see this by testing with different memory models:   ---  -- > > autocheck' SequentialConsistency example2+  -- > > autocheckWay defaultWay SequentialConsistency example2   -- > [pass] Never Deadlocks (checked: 6)   -- > [pass] No Exceptions (checked: 6)   -- > [fail] Consistent Result (checked: 5)@@ -145,7 +148,7 @@   -- >         ...   -- > False   ---  -- > > autocheck' TotalStoreOrder example2+  -- > > autocheckWay defaultWay TotalStoreOrder example2   -- > [pass] Never Deadlocks (checked: 303)   -- > [pass] No Exceptions (checked: 303)   -- > [fail] Consistent Result (checked: 302)@@ -202,9 +205,9 @@   , Result(..)   , Failure(..)   , runTest-  , runTest'+  , runTestWay   , runTestM-  , runTestM'+  , runTestWayM    -- * Predicates @@ -240,22 +243,22 @@   ) where  import Control.Arrow (first)-import Control.DeepSeq (NFData(..)) import Control.Monad (when, unless) import Control.Monad.Ref (MonadRef) import Control.Monad.ST (runST) import Data.Function (on) import Data.List (intercalate, intersperse, minimumBy) import Data.Ord (comparing)+import System.Random (RandomGen, StdGen)  import Test.DejaFu.Common import Test.DejaFu.Conc import Test.DejaFu.SCT --- | The default memory model: @TotalStoreOrder@-defaultMemType :: MemType-defaultMemType = TotalStoreOrder +-------------------------------------------------------------------------------+-- DejaFu+ -- | Automatically test a computation. In particular, look for -- deadlocks, uncaught exceptions, and multiple return values. --@@ -266,10 +269,10 @@   => (forall t. ConcST t a)   -- ^ The computation to test   -> IO Bool-autocheck = autocheck' defaultMemType defaultBounds+autocheck = autocheckWay defaultWay defaultMemType --- | Variant of 'autocheck' which takes a memor model and schedule--- bounds.+-- | Variant of 'autocheck' which takes a way to run the program and a+-- memory model. -- -- Schedule bounding is used to filter the large number of possible -- schedules, and can be iteratively increased for further coverage@@ -281,26 +284,28 @@ -- -- __Warning:__ Using largers bounds will almost certainly -- significantly increase the time taken to test!-autocheck' :: (Eq a, Show a)-  => MemType+autocheckWay :: (Eq a, Show a, RandomGen g)+  => Way g+  -- ^ How to run the concurrent program.+  -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> Bounds-  -- ^ The schedule bounds   -> (forall t. ConcST t a)   -- ^ The computation to test   -> IO Bool-autocheck' memtype cb conc = dejafus' memtype cb conc autocheckCases+autocheckWay way memtype conc =+  dejafusWay way memtype conc autocheckCases  -- | Variant of 'autocheck' for computations which do 'IO'. autocheckIO :: (Eq a, Show a) => ConcIO a -> IO Bool-autocheckIO = autocheckIO' defaultMemType defaultBounds+autocheckIO = autocheckWayIO defaultWay defaultMemType --- | Variant of 'autocheck'' for computations which do 'IO'.-autocheckIO' :: (Eq a, Show a) => MemType -> Bounds -> ConcIO a -> IO Bool-autocheckIO' memtype cb concio = dejafusIO' memtype cb concio autocheckCases+-- | Variant of 'autocheckWay' for computations which do 'IO'.+autocheckWayIO :: (Eq a, Show a, RandomGen g) => Way g -> MemType -> ConcIO a -> IO Bool+autocheckWayIO way memtype concio =+  dejafusWayIO way memtype concio autocheckCases  -- | Predicates for the various autocheck functions.-autocheckCases :: (Eq a, Show a) => [(String, Predicate a)]+autocheckCases :: Eq a => [(String, Predicate a)] autocheckCases =   [ ("Never Deadlocks",   representative deadlocksNever)   , ("No Exceptions",     representative exceptionsNever)@@ -315,21 +320,21 @@   -> (String, Predicate a)   -- ^ The predicate (with a name) to check   -> IO Bool-dejafu = dejafu' defaultMemType defaultBounds+dejafu = dejafuWay defaultWay defaultMemType --- | Variant of 'dejafu'' which takes a memory model and schedule--- bounds.-dejafu' :: Show a-  => MemType+-- | Variant of 'dejafu' which takes a way to run the program and a+-- memory model.+dejafuWay :: (Show a, RandomGen g)+  => Way g+  -- ^ How to run the concurrent program.+  -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> Bounds-  -- ^ The schedule bounds   -> (forall t. ConcST t a)   -- ^ The computation to test   -> (String, Predicate a)   -- ^ The predicate (with a name) to check   -> IO Bool-dejafu' memtype cb conc test = dejafus' memtype cb conc [test]+dejafuWay way memtype conc test = dejafusWay way memtype conc [test]  -- | Variant of 'dejafu' which takes a collection of predicates to -- test, returning 'True' if all pass.@@ -339,46 +344,49 @@   -> [(String, Predicate a)]   -- ^ The list of predicates (with names) to check   -> IO Bool-dejafus = dejafus' defaultMemType defaultBounds+dejafus = dejafusWay defaultWay defaultMemType --- | Variant of 'dejafus' which takes a memory model and schedule--- bounds.-dejafus' :: Show a-  => MemType+-- | Variant of 'dejafus' which takes a way to run the program and a+-- memory model.+dejafusWay :: (Show a, RandomGen g)+  => Way g+  -- ^ How to run the concurrent program.+  -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> Bounds-  -- ^ The schedule bounds.   -> (forall t. ConcST t a)   -- ^ The computation to test   -> [(String, Predicate a)]   -- ^ The list of predicates (with names) to check   -> IO Bool-dejafus' memtype cb conc tests = do-  let traces = runST (sctBound memtype cb conc)+dejafusWay way memtype conc tests = do+  let traces = runST (runSCT way memtype conc)   results <- mapM (\(name, test) -> doTest name $ test traces) tests   return $ and results  -- | Variant of 'dejafu' for computations which do 'IO'. dejafuIO :: Show a => ConcIO a -> (String, Predicate a) -> IO Bool-dejafuIO = dejafuIO' defaultMemType defaultBounds+dejafuIO = dejafuWayIO defaultWay defaultMemType --- | Variant of 'dejafu'' for computations which do 'IO'.-dejafuIO' :: Show a => MemType -> Bounds -> ConcIO a -> (String, Predicate a) -> IO Bool-dejafuIO' memtype cb concio test = dejafusIO' memtype cb concio [test]+-- | Variant of 'dejafuWay' for computations which do 'IO'.+dejafuWayIO :: (Show a, RandomGen g) => Way g -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool+dejafuWayIO way memtype concio test =+  dejafusWayIO way memtype concio [test]  -- | Variant of 'dejafus' for computations which do 'IO'. dejafusIO :: Show a => ConcIO a -> [(String, Predicate a)] -> IO Bool-dejafusIO = dejafusIO' defaultMemType defaultBounds+dejafusIO = dejafusWayIO defaultWay defaultMemType --- | Variant of 'dejafus'' for computations which do 'IO'.-dejafusIO' :: Show a => MemType -> Bounds -> ConcIO a -> [(String, Predicate a)] -> IO Bool-dejafusIO' memtype cb concio tests = do-  traces  <- sctBound memtype cb concio+-- | Variant of 'dejafusWay' for computations which do 'IO'.+dejafusWayIO :: (Show a, RandomGen g) => Way g -> MemType -> ConcIO a -> [(String, Predicate a)] -> IO Bool+dejafusWayIO way memtype concio tests = do+  traces  <- runSCT way memtype concio   results <- mapM (\(name, test) -> doTest name $ test traces) tests   return $ and results --- * Test cases +-------------------------------------------------------------------------------+-- Test cases+ -- | The results of a test, including the number of cases checked to -- determine the final boolean outcome. data Result a = Result@@ -386,23 +394,20 @@   -- ^ Whether the test passed or not.   , _casesChecked :: Int   -- ^ The number of cases checked.-  , _failures     :: [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]+  , _failures     :: [(Either Failure a, Trace)]   -- ^ The failing cases, if any.   , _failureMsg   :: String   -- ^ A message to display on failure, if nonempty   } deriving Show  -- | A failed result, taking the given list of failures.-defaultFail :: [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> Result a+defaultFail :: [(Either Failure a, Trace)] -> Result a defaultFail failures = Result False 0 failures ""  -- | A passed result. defaultPass :: Result a defaultPass = Result True 0 [] "" -instance NFData a => NFData (Result a) where-  rnf r = rnf (_pass r, _casesChecked r, _failures r, _failureMsg r)- instance Functor Result where   fmap f r = r { _failures = map (first $ fmap f) $ _failures r } @@ -417,38 +422,42 @@   -> (forall t. ConcST t a)   -- ^ The computation to test   -> Result a-runTest test conc = runST (runTestM test conc)+runTest test conc =+  runST (runTestM test conc) --- | Variant of 'runTest' which takes a memory model and schedule--- bounds.-runTest' ::-    MemType+-- | Variant of 'runTest' which takes a way to run the program and a+-- memory model.+runTestWay :: RandomGen g+  => Way g+  -- ^ How to run the concurrent program.+  -> MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> Bounds-  -- ^ The schedule bounds.   -> Predicate a   -- ^ The predicate to check   -> (forall t. ConcST t a)   -- ^ The computation to test   -> Result a-runTest' memtype cb predicate conc =-  runST (runTestM' memtype cb predicate conc)+runTestWay way memtype predicate conc =+  runST (runTestWayM way memtype predicate conc)  -- | Monad-polymorphic variant of 'runTest'. runTestM :: MonadRef r n          => Predicate a -> Conc n r a -> n (Result a)-runTestM = runTestM' defaultMemType defaultBounds+runTestM = runTestWayM defaultWay defaultMemType  -- | Monad-polymorphic variant of 'runTest''.-runTestM' :: MonadRef r n-          => MemType -> Bounds -> Predicate a -> Conc n r a -> n (Result a)-runTestM' memtype cb predicate conc = predicate <$> sctBound memtype cb conc+runTestWayM :: (MonadRef r n, RandomGen g)+            => Way g -> MemType -> Predicate a -> Conc n r a -> n (Result a)+runTestWayM way memtype predicate conc =+  predicate <$> runSCT way memtype conc --- * Predicates +-------------------------------------------------------------------------------+-- Predicates+ -- | A @Predicate@ is a function which collapses a list of results -- into a 'Result'.-type Predicate a = [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> Result a+type Predicate a = [(Either Failure a, Trace)] -> Result a  -- | Reduce the list of failures in a @Predicate@ to one -- representative trace for each unique result.@@ -601,7 +610,54 @@ gives' :: (Eq a, Show a) => [a] -> Predicate a gives' = gives . map Right --- * Internal++-------------------------------------------------------------------------------+-- Defaults++-- | A default way to execute concurrent programs: systematically+-- using 'defaultBounds'.+--+-- The type parameter is constrained to 'StdGen', even though it is+-- unused, to avoid ambiguity errors.+defaultWay :: Way StdGen+defaultWay = Systematically defaultBounds++-- | The default memory model: @TotalStoreOrder@+defaultMemType :: MemType+defaultMemType = TotalStoreOrder++-- | All bounds enabled, using their default values.+defaultBounds :: Bounds+defaultBounds = Bounds+  { boundPreemp = Just defaultPreemptionBound+  , boundFair   = Just defaultFairBound+  , boundLength = Just defaultLengthBound+  }++-- | A sensible default preemption bound: 2.+--+-- See /Concurrency Testing Using Schedule Bounding: an Empirical Study/,+-- P. Thomson, A. F. Donaldson, A. Betts for justification.+defaultPreemptionBound :: PreemptionBound+defaultPreemptionBound = 2++-- | A sensible default fair bound: 5.+--+-- This comes from playing around myself, but there is probably a+-- better default.+defaultFairBound :: FairBound+defaultFairBound = 5++-- | A sensible default length bound: 250.+--+-- Based on the assumption that anything which executes for much+-- longer (or even this long) will take ages to test.+defaultLengthBound :: LengthBound+defaultLengthBound = 250+++-------------------------------------------------------------------------------+-- Utils  -- | Run a test and print to stdout doTest :: Show a => String -> Result a -> IO Bool

@@ -60,14 +60,12 @@   , MemType(..)   ) where -import Control.DeepSeq (NFData(..)) import Control.Exception (MaskingState(..))-import Data.Dynamic (Dynamic) import Data.List (sort, nub, intercalate)+import Data.List.NonEmpty (NonEmpty) import Data.Maybe (fromMaybe, mapMaybe) import Data.Set (Set) import qualified Data.Set as S-import Test.DPOR (Decision(..), Trace)  ------------------------------------------------------------------------------- -- Identifiers@@ -83,9 +81,6 @@   show (ThreadId (Just n) _) = n   show (ThreadId Nothing  i) = show i -instance NFData ThreadId where-  rnf (ThreadId n i) = rnf (n, i)- -- | Every @CRef@ has a unique identifier. data CRefId = CRefId (Maybe String) Int   deriving Eq@@ -97,9 +92,6 @@   show (CRefId (Just n) _) = n   show (CRefId Nothing  i) = show i -instance NFData CRefId where-  rnf (CRefId n i) = rnf (n, i)- -- | Every @MVar@ has a unique identifier. data MVarId = MVarId (Maybe String) Int   deriving Eq@@ -111,9 +103,6 @@   show (MVarId (Just n) _) = n   show (MVarId Nothing  i) = show i -instance NFData MVarId where-  rnf (MVarId n i) = rnf (n, i)- -- | Every @TVar@ has a unique identifier. data TVarId = TVarId (Maybe String) Int   deriving Eq@@ -125,9 +114,6 @@   show (TVarId (Just n) _) = n   show (TVarId Nothing  i) = show i -instance NFData TVarId where-  rnf (TVarId n i) = rnf (n, i)- -- | The ID of the initial thread. initialThread :: ThreadId initialThread = ThreadId (Just "main") 0@@ -202,40 +188,42 @@   -- ^ Set the number of Haskell threads that can run simultaneously.   | Yield   -- ^ Yield the current thread.-  | NewVar MVarId+  | NewMVar MVarId   -- ^ Create a new 'MVar'.-  | PutVar MVarId [ThreadId]+  | PutMVar MVarId [ThreadId]   -- ^ Put into a 'MVar', possibly waking up some threads.-  | BlockedPutVar MVarId+  | BlockedPutMVar MVarId   -- ^ Get blocked on a put.-  | TryPutVar MVarId Bool [ThreadId]+  | TryPutMVar MVarId Bool [ThreadId]   -- ^ Try to put into a 'MVar', possibly waking up some threads.-  | ReadVar MVarId+  | ReadMVar MVarId   -- ^ Read from a 'MVar'.-  | BlockedReadVar MVarId+  | TryReadMVar MVarId Bool+  -- ^ Try to read from a 'MVar'.+  | BlockedReadMVar MVarId   -- ^ Get blocked on a read.-  | TakeVar MVarId [ThreadId]+  | TakeMVar MVarId [ThreadId]   -- ^ Take from a 'MVar', possibly waking up some threads.-  | BlockedTakeVar MVarId+  | BlockedTakeMVar MVarId   -- ^ Get blocked on a take.-  | TryTakeVar MVarId Bool [ThreadId]+  | TryTakeMVar MVarId Bool [ThreadId]   -- ^ Try to take from a 'MVar', possibly waking up some threads.-  | NewRef CRefId+  | NewCRef CRefId   -- ^ Create a new 'CRef'.-  | ReadRef CRefId+  | ReadCRef CRefId   -- ^ Read from a 'CRef'.-  | ReadRefCas CRefId+  | ReadCRefCas CRefId   -- ^ Read from a 'CRef' for a future compare-and-swap.-  | ModRef CRefId+  | ModCRef CRefId   -- ^ Modify a 'CRef'.-  | ModRefCas CRefId+  | ModCRefCas CRefId   -- ^ Modify a 'CRef' using a compare-and-swap.-  | WriteRef CRefId+  | WriteCRef CRefId   -- ^ Write to a 'CRef' without synchronising.-  | CasRef CRefId Bool+  | CasCRef CRefId Bool   -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising   -- it.-  | CommitRef ThreadId CRefId+  | CommitCRef ThreadId CRefId   -- ^ Commit the last write to the given 'CRef' by the given thread,   -- so that all threads can see the updated value.   | STM TTrace [ThreadId]@@ -268,48 +256,18 @@   -- 'ConcIO'.   | Return   -- ^ A 'return' or 'pure' action was executed.-  | Message Dynamic-  -- ^ A '_concMessage' annotation was processed.   | Stop   -- ^ Cease execution and terminate.-  deriving Show--instance NFData ThreadAction where-  rnf (Fork t) = rnf t-  rnf (GetNumCapabilities i) = rnf i-  rnf (SetNumCapabilities i) = rnf i-  rnf (NewVar c) = rnf c-  rnf (PutVar c ts) = rnf (c, ts)-  rnf (BlockedPutVar c) = rnf c-  rnf (TryPutVar c b ts) = rnf (c, b, ts)-  rnf (ReadVar c) = rnf c-  rnf (BlockedReadVar c) = rnf c-  rnf (TakeVar c ts) = rnf (c, ts)-  rnf (BlockedTakeVar c) = rnf c-  rnf (TryTakeVar c b ts) = rnf (c, b, ts)-  rnf (NewRef c) = rnf c-  rnf (ReadRef c) = rnf c-  rnf (ReadRefCas c) = rnf c-  rnf (ModRef c) = rnf c-  rnf (ModRefCas c) = rnf c-  rnf (WriteRef c) = rnf c-  rnf (CasRef c b) = rnf (c, b)-  rnf (CommitRef t c) = rnf (t, c)-  rnf (STM s ts) = rnf (s, ts)-  rnf (BlockedSTM s) = rnf s-  rnf (ThrowTo t) = rnf t-  rnf (BlockedThrowTo t) = rnf t-  rnf (SetMasking b m) = b `seq` m `seq` ()-  rnf (ResetMasking b m) = b `seq` m `seq` ()-  rnf (Message m) = m `seq` ()-  rnf a = a `seq` ()+  | Subconcurrency+  -- ^ Start executing an action with @subconcurrency@.+  deriving (Eq, Show)  -- | Check if a @ThreadAction@ immediately blocks. isBlock :: ThreadAction -> Bool isBlock (BlockedThrowTo  _) = True-isBlock (BlockedTakeVar _) = True-isBlock (BlockedReadVar _) = True-isBlock (BlockedPutVar  _) = True+isBlock (BlockedTakeMVar _) = True+isBlock (BlockedReadMVar _) = True+isBlock (BlockedPutMVar  _) = True isBlock (BlockedSTM _) = True isBlock _ = False @@ -344,34 +302,36 @@   -- simultaneously.   | WillYield   -- ^ Will yield the current thread.-  | WillNewVar+  | WillNewMVar   -- ^ Will create a new 'MVar'.-  | WillPutVar MVarId+  | WillPutMVar MVarId   -- ^ Will put into a 'MVar', possibly waking up some threads.-  | WillTryPutVar MVarId+  | WillTryPutMVar MVarId   -- ^ Will try to put into a 'MVar', possibly waking up some threads.-  | WillReadVar MVarId+  | WillReadMVar MVarId   -- ^ Will read from a 'MVar'.-  | WillTakeVar MVarId+  | WillTryReadMVar MVarId+  -- ^ Will try to read from a 'MVar'.+  | WillTakeMVar MVarId   -- ^ Will take from a 'MVar', possibly waking up some threads.-  | WillTryTakeVar MVarId+  | WillTryTakeMVar MVarId   -- ^ Will try to take from a 'MVar', possibly waking up some threads.-  | WillNewRef+  | WillNewCRef   -- ^ Will create a new 'CRef'.-  | WillReadRef CRefId+  | WillReadCRef CRefId   -- ^ Will read from a 'CRef'.-  | WillReadRefCas CRefId+  | WillReadCRefCas CRefId   -- ^ Will read from a 'CRef' for a future compare-and-swap.-  | WillModRef CRefId+  | WillModCRef CRefId   -- ^ Will modify a 'CRef'.-  | WillModRefCas CRefId-  -- ^ Will nodify a 'CRef' using a compare-and-swap.-  | WillWriteRef CRefId+  | WillModCRefCas CRefId+  -- ^ Will modify a 'CRef' using a compare-and-swap.+  | WillWriteCRef CRefId   -- ^ Will write to a 'CRef' without synchronising.-  | WillCasRef CRefId+  | WillCasCRef CRefId   -- ^ Will attempt to to a 'CRef' using a compare-and-swap,   -- synchronising it.-  | WillCommitRef ThreadId CRefId+  | WillCommitCRef ThreadId CRefId   -- ^ Will commit the last write by the given thread to the 'CRef'.   | WillSTM   -- ^ Will execute an STM transaction, possibly waking up some@@ -397,31 +357,11 @@   -- 'ConcIO'.   | WillReturn   -- ^ Will execute a 'return' or 'pure' action.-  | WillMessage Dynamic-  -- ^ Will process a _concMessage' annotation.   | WillStop   -- ^ Will cease execution and terminate.-  deriving Show--instance NFData Lookahead where-  rnf (WillSetNumCapabilities i) = rnf i-  rnf (WillPutVar c) = rnf c-  rnf (WillTryPutVar c) = rnf c-  rnf (WillReadVar c) = rnf c-  rnf (WillTakeVar c) = rnf c-  rnf (WillTryTakeVar c) = rnf c-  rnf (WillReadRef c) = rnf c-  rnf (WillReadRefCas c) = rnf c-  rnf (WillModRef c) = rnf c-  rnf (WillModRefCas c) = rnf c-  rnf (WillWriteRef c) = rnf c-  rnf (WillCasRef c) = rnf c-  rnf (WillCommitRef t c) = rnf (t, c)-  rnf (WillThrowTo t) = rnf t-  rnf (WillSetMasking b m) = b `seq` m `seq` ()-  rnf (WillResetMasking b m) = b `seq` m `seq` ()-  rnf (WillMessage m) = m `seq` ()-  rnf l = l `seq` ()+  | WillSubconcurrency+  -- ^ Will execute an action with @subconcurrency@.+  deriving (Eq, Show)  -- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has -- happened. 'Killed' has no 'Lookahead' counterpart.@@ -431,23 +371,24 @@ rewind (GetNumCapabilities _) = Just WillGetNumCapabilities rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i) rewind Yield = Just WillYield-rewind (NewVar _) = Just WillNewVar-rewind (PutVar c _) = Just (WillPutVar c)-rewind (BlockedPutVar c) = Just (WillPutVar c)-rewind (TryPutVar c _ _) = Just (WillTryPutVar c)-rewind (ReadVar c) = Just (WillReadVar c)-rewind (BlockedReadVar c) = Just (WillReadVar c)-rewind (TakeVar c _) = Just (WillTakeVar c)-rewind (BlockedTakeVar c) = Just (WillTakeVar c)-rewind (TryTakeVar c _ _) = Just (WillTryTakeVar c)-rewind (NewRef _) = Just WillNewRef-rewind (ReadRef c) = Just (WillReadRef c)-rewind (ReadRefCas c) = Just (WillReadRefCas c)-rewind (ModRef c) = Just (WillModRef c)-rewind (ModRefCas c) = Just (WillModRefCas c)-rewind (WriteRef c) = Just (WillWriteRef c)-rewind (CasRef c _) = Just (WillCasRef c)-rewind (CommitRef t c) = Just (WillCommitRef t c)+rewind (NewMVar _) = Just WillNewMVar+rewind (PutMVar c _) = Just (WillPutMVar c)+rewind (BlockedPutMVar c) = Just (WillPutMVar c)+rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c)+rewind (ReadMVar c) = Just (WillReadMVar c)+rewind (BlockedReadMVar c) = Just (WillReadMVar c)+rewind (TryReadMVar c _) = Just (WillTryReadMVar c)+rewind (TakeMVar c _) = Just (WillTakeMVar c)+rewind (BlockedTakeMVar c) = Just (WillTakeMVar c)+rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c)+rewind (NewCRef _) = Just WillNewCRef+rewind (ReadCRef c) = Just (WillReadCRef c)+rewind (ReadCRefCas c) = Just (WillReadCRefCas c)+rewind (ModCRef c) = Just (WillModCRef c)+rewind (ModCRefCas c) = Just (WillModCRefCas c)+rewind (WriteCRef c) = Just (WillWriteCRef c)+rewind (CasCRef c _) = Just (WillCasCRef c)+rewind (CommitCRef t c) = Just (WillCommitCRef t c) rewind (STM _ _) = Just WillSTM rewind (BlockedSTM _) = Just WillSTM rewind Catching = Just WillCatching@@ -460,18 +401,17 @@ rewind (ResetMasking b m) = Just (WillResetMasking b m) rewind LiftIO = Just WillLiftIO rewind Return = Just WillReturn-rewind (Message m) = Just (WillMessage m) rewind Stop = Just WillStop+rewind Subconcurrency = Just WillSubconcurrency  -- | Check if an operation could enable another thread. willRelease :: Lookahead -> Bool willRelease WillFork = True willRelease WillYield = True-willRelease (WillPutVar _) = True-willRelease (WillTryPutVar _) = True-willRelease (WillReadVar _) = True-willRelease (WillTakeVar _) = True-willRelease (WillTryTakeVar _) = True+willRelease (WillPutMVar _) = True+willRelease (WillTryPutMVar _) = True+willRelease (WillTakeMVar _) = True+willRelease (WillTryTakeMVar _) = True willRelease WillSTM = True willRelease WillThrow = True willRelease (WillSetMasking _ _) = True@@ -508,17 +448,6 @@   -- communication.   deriving (Eq, Show) -instance NFData ActionType where-  rnf (UnsynchronisedRead  r) = rnf r-  rnf (UnsynchronisedWrite r) = rnf r-  rnf (PartiallySynchronisedCommit r) = rnf r-  rnf (PartiallySynchronisedWrite  r) = rnf r-  rnf (PartiallySynchronisedModify  r) = rnf r-  rnf (SynchronisedModify  r) = rnf r-  rnf (SynchronisedRead    c) = rnf c-  rnf (SynchronisedWrite   c) = rnf c-  rnf a = a `seq` ()- -- | Check if an action imposes a write barrier. isBarrier :: ActionType -> Bool isBarrier (SynchronisedModify _) = True@@ -564,18 +493,19 @@  -- | Variant of 'simplifyAction' that takes a 'Lookahead'. simplifyLookahead :: Lookahead -> ActionType-simplifyLookahead (WillPutVar c)     = SynchronisedWrite c-simplifyLookahead (WillTryPutVar c)  = SynchronisedWrite c-simplifyLookahead (WillReadVar c)    = SynchronisedRead c-simplifyLookahead (WillTakeVar c)    = SynchronisedRead c-simplifyLookahead (WillTryTakeVar c) = SynchronisedRead c-simplifyLookahead (WillReadRef r)     = UnsynchronisedRead r-simplifyLookahead (WillReadRefCas r)  = UnsynchronisedRead r-simplifyLookahead (WillModRef r)      = SynchronisedModify r-simplifyLookahead (WillModRefCas r)   = PartiallySynchronisedModify r-simplifyLookahead (WillWriteRef r)    = UnsynchronisedWrite r-simplifyLookahead (WillCasRef r)      = PartiallySynchronisedWrite r-simplifyLookahead (WillCommitRef _ r) = PartiallySynchronisedCommit r+simplifyLookahead (WillPutMVar c)     = SynchronisedWrite c+simplifyLookahead (WillTryPutMVar c)  = SynchronisedWrite c+simplifyLookahead (WillReadMVar c)    = SynchronisedRead c+simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c+simplifyLookahead (WillTakeMVar c)    = SynchronisedRead c+simplifyLookahead (WillTryTakeMVar c)  = SynchronisedRead c+simplifyLookahead (WillReadCRef r)     = UnsynchronisedRead r+simplifyLookahead (WillReadCRefCas r)  = UnsynchronisedRead r+simplifyLookahead (WillModCRef r)      = SynchronisedModify r+simplifyLookahead (WillModCRefCas r)   = PartiallySynchronisedModify r+simplifyLookahead (WillWriteCRef r)    = UnsynchronisedWrite r+simplifyLookahead (WillCasCRef r)      = PartiallySynchronisedWrite r+simplifyLookahead (WillCommitCRef _ r) = PartiallySynchronisedCommit r simplifyLookahead WillSTM         = SynchronisedOther simplifyLookahead (WillThrowTo _) = SynchronisedOther simplifyLookahead _ = UnsynchronisedOther@@ -611,22 +541,34 @@   -- ^ Terminate successfully and commit effects.   deriving (Eq, Show) -instance NFData TAction where-  rnf (TRead  v) = rnf v-  rnf (TWrite v) = rnf v-  rnf (TCatch  s m) = rnf (s, m)-  rnf (TOrElse s m) = rnf (s, m)-  rnf a = a `seq` ()- ------------------------------------------------------------------------------- -- Traces +-- | One of the outputs of the runner is a @Trace@, which is a log of+-- decisions made, all the runnable threads and what they would do,+-- and the action a thread took in its step.+type Trace+  = [(Decision, [(ThreadId, NonEmpty Lookahead)], ThreadAction)]++-- | Scheduling decisions are based on the state of the running+-- program, and so we can capture some of that state in recording what+-- specific decision we made.+data Decision =+    Start ThreadId+  -- ^ Start a new thread, because the last was blocked (or it's the+  -- start of computation).+  | Continue+  -- ^ Continue running the last thread for another step.+  | SwitchTo ThreadId+  -- ^ Pre-empt the running thread, and switch to another.+  deriving (Eq, Show)+ -- | Pretty-print a trace, including a key of the thread IDs (not -- including thread 0). Each line of the key is indented by two -- spaces.-showTrace :: Trace ThreadId ThreadAction Lookahead -> String+showTrace :: Trace -> String showTrace trc = intercalate "\n" $ concatMap go trc : strkey where-  go (_,_,CommitRef _ _) = "C-"+  go (_,_,CommitCRef _ _) = "C-"   go (Start    (ThreadId _ i),_,_) = "S" ++ show i ++ "-"   go (SwitchTo (ThreadId _ i),_,_) = "P" ++ show i ++ "-"   go (Continue,_,_) = "-"@@ -648,18 +590,18 @@ -- SO, we don't count a switch TO a commit thread as a -- preemption. HOWEVER, the switch FROM a commit thread counts as a -- preemption if it is not to the thread that the commit interrupted.-preEmpCount :: [(Decision ThreadId, ThreadAction)]-            -> (Decision ThreadId, Lookahead)+preEmpCount :: [(Decision, ThreadAction)]+            -> (Decision, Lookahead)             -> Int-preEmpCount ts (d, _) = go initialThread Nothing ts where-  go _ (Just Yield) ((SwitchTo t, a):rest) = go t (Just a) rest-  go tid prior ((SwitchTo t, a):rest)+preEmpCount (x:xs) (d, _) = go initialThread x xs where+  go _ (_, Yield) (r@(SwitchTo t, _):rest) = go t r rest+  go tid prior (r@(SwitchTo t, _):rest)     | isCommitThread t = go tid prior (skip rest)-    | otherwise = 1 + go t (Just a) rest-  go _   _ ((Start t,  a):rest) = go t   (Just a) rest-  go tid _ ((Continue, a):rest) = go tid (Just a) rest+    | otherwise = 1 + go t r rest+  go _   _ (r@(Start t,  _):rest) = go t   r rest+  go tid _ (r@(Continue, _):rest) = go tid r rest   go _ prior [] = case (prior, d) of-    (Just Yield, SwitchTo _) -> 0+    ((_, Yield), SwitchTo _) -> 0     (_, SwitchTo _) -> 1     _ -> 0 @@ -670,6 +612,7 @@   skip = dropWhile (not . isContextSwitch . fst)   isContextSwitch Continue = False   isContextSwitch _ = True+preEmpCount [] _ = 0  ------------------------------------------------------------------------------- -- Failures@@ -692,18 +635,19 @@   -- ^ The computation became blocked indefinitely on @TVar@s.   | UncaughtException   -- ^ An uncaught exception bubbled to the top of the computation.+  | IllegalSubconcurrency+  -- ^ Calls to @subconcurrency@ were nested, or attempted when+  -- multiple threads existed.   deriving (Eq, Show, Read, Ord, Enum, Bounded) -instance NFData Failure where-  rnf f = f `seq` ()- -- | Pretty-print a failure showFail :: Failure -> String-showFail Abort             = "[abort]"-showFail Deadlock          = "[deadlock]"-showFail STMDeadlock       = "[stm-deadlock]"-showFail InternalError     = "[internal-error]"+showFail Abort = "[abort]"+showFail Deadlock = "[deadlock]"+showFail STMDeadlock = "[stm-deadlock]"+showFail InternalError = "[internal-error]" showFail UncaughtException = "[exception]"+showFail IllegalSubconcurrency = "[illegal-subconcurrency]"  ------------------------------------------------------------------------------- -- Memory Models@@ -726,9 +670,6 @@   -- are not necessarily committed in the same order that they are   -- created.   deriving (Eq, Show, Read, Ord, Enum, Bounded)--instance NFData MemType where-  rnf m = m `seq` ()  ------------------------------------------------------------------------------- -- Utilities

@@ -28,6 +28,7 @@   , Failure(..)   , MemType(..)   , runConcurrent+  , subconcurrency    -- * Execution traces   , Trace@@ -42,33 +43,30 @@   , showFail    -- * Scheduling-  , module Test.DPOR.Schedule+  , module Test.DejaFu.Schedule   ) where  import Control.Exception (MaskingState(..)) import qualified Control.Monad.Base as Ba import qualified Control.Monad.Catch as Ca import qualified Control.Monad.IO.Class as IO-import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef)+import Control.Monad.Ref (MonadRef,) import Control.Monad.ST (ST)-import Data.Dynamic (toDyn)+import qualified Data.Foldable as F import Data.IORef (IORef)-import qualified Data.Map.Strict as M-import Data.Maybe (fromJust) import Data.STRef (STRef)-import Test.DPOR.Schedule+import Test.DejaFu.Schedule  import qualified Control.Monad.Conc.Class as C import Test.DejaFu.Common import Test.DejaFu.Conc.Internal import Test.DejaFu.Conc.Internal.Common-import Test.DejaFu.Conc.Internal.Threading import Test.DejaFu.STM  {-# ANN module ("HLint: ignore Avoid lambda" :: String) #-} {-# ANN module ("HLint: ignore Use const"    :: String) #-} -newtype Conc n r a = C { unC :: M n r (STMLike n r) a } deriving (Functor, Applicative, Monad)+newtype Conc n r a = C { unC :: M n r a } deriving (Functor, Applicative, Monad)  -- | A 'MonadConc' implementation using @ST@, this should be preferred -- if you do not need 'liftIO'.@@ -77,10 +75,10 @@ -- | A 'MonadConc' implementation using @IO@. type ConcIO = Conc IO IORef -toConc :: ((a -> Action n r (STMLike n r)) -> Action n r (STMLike n r)) -> Conc n r a+toConc :: ((a -> Action n r) -> Action n r) -> Conc n r a toConc = C . cont -wrap :: (M n r (STMLike n r) a -> M n r (STMLike n r) a) -> Conc n r a -> Conc n r a+wrap :: (M n r a -> M n r a) -> Conc n r a -> Conc n r a wrap f = C . f . unC  instance IO.MonadIO ConcIO where@@ -123,29 +121,30 @@    -- ---------- -  newCRefN n a = toConc (\c -> ANewRef n a c)+  newCRefN n a = toConc (\c -> ANewCRef n a c) -  readCRef   ref = toConc (AReadRef    ref)-  readForCAS ref = toConc (AReadRefCas ref)+  readCRef   ref = toConc (AReadCRef    ref)+  readForCAS ref = toConc (AReadCRefCas ref)    peekTicket' _ = _ticketVal -  writeCRef ref      a = toConc (\c -> AWriteRef ref a (c ()))-  casCRef   ref tick a = toConc (ACasRef ref tick a)+  writeCRef ref      a = toConc (\c -> AWriteCRef ref a (c ()))+  casCRef   ref tick a = toConc (ACasCRef ref tick a) -  atomicModifyCRef ref f = toConc (AModRef    ref f)-  modifyCRefCAS    ref f = toConc (AModRefCas ref f)+  atomicModifyCRef ref f = toConc (AModCRef    ref f)+  modifyCRefCAS    ref f = toConc (AModCRefCas ref f)    -- ---------- -  newEmptyMVarN n = toConc (\c -> ANewVar n c)+  newEmptyMVarN n = toConc (\c -> ANewMVar n c) -  putMVar  var a = toConc (\c -> APutVar var a (c ()))-  readMVar var   = toConc (AReadVar var)-  takeMVar var   = toConc (ATakeVar var)+  putMVar  var a = toConc (\c -> APutMVar var a (c ()))+  readMVar var   = toConc (AReadMVar var)+  takeMVar var   = toConc (ATakeMVar var) -  tryPutMVar  var a = toConc (ATryPutVar  var a)-  tryTakeMVar var   = toConc (ATryTakeVar var)+  tryPutMVar  var a = toConc (ATryPutMVar  var a)+  tryReadMVar var   = toConc (ATryReadMVar var)+  tryTakeMVar var   = toConc (ATryTakeMVar var)    -- ---------- @@ -155,10 +154,6 @@    atomically = toConc . AAtom -  -- ------------  _concMessage msg = toConc (\c -> AMessage (toDyn msg) (c ()))- -- | Run a concurrent computation with a given 'Scheduler' and initial -- state, returning a failure reason on error. Also returned is the -- final state of the scheduler, and an execution trace.@@ -176,25 +171,20 @@ -- nonexistent thread. In either of those cases, the computation will -- be halted. runConcurrent :: MonadRef r n-              => Scheduler ThreadId ThreadAction Lookahead s+              => Scheduler s               -> MemType               -> s               -> Conc n r a-              -> n (Either Failure a, s, Trace ThreadId ThreadAction Lookahead)-runConcurrent sched memtype s (C conc) = do-  ref <- newRef Nothing--  let c = runCont conc (AStop . writeRef ref . Just . Right)-  let threads = launch' Unmasked initialThread (const c) M.empty--  (s', trace) <- runThreads runTransaction-                           sched-                           memtype-                           s-                           threads-                           initialIdSource-                           ref--  out <- readRef ref+              -> n (Either Failure a, s, Trace)+runConcurrent sched memtype s ma = do+  (res, s', trace) <- runConcurrency sched memtype s (unC ma)+  pure (res, s', F.toList trace) -  pure (fromJust out, s', reverse trace)+-- | Run a concurrent computation and return its result.+--+-- This can only be called in the main thread, when no other threads+-- exist. Calls to 'subconcurrency' cannot be nested. Violating either+-- of these conditions will result in the computation failing with+-- @IllegalSubconcurrency@.+subconcurrency :: Conc n r a -> Conc n r (Either Failure a)+subconcurrency ma = toConc (ASub (unC ma))

@@ -16,19 +16,23 @@ module Test.DejaFu.Conc.Internal where  import Control.Exception (MaskingState(..), toException)-import Control.Monad.Ref (MonadRef, newRef, writeRef)+import Control.Monad.Ref (MonadRef, newRef, readRef, writeRef)+import qualified Data.Foldable as F import Data.Functor (void) import Data.List (sort) import Data.List.NonEmpty (NonEmpty(..), fromList) import qualified Data.Map.Strict as M-import Data.Maybe (fromJust, isJust, isNothing, listToMaybe)-import Test.DPOR (Scheduler)+import Data.Maybe (fromJust, isJust, isNothing)+import Data.Monoid ((<>))+import Data.Sequence (Seq, (<|))+import qualified Data.Sequence as Seq  import Test.DejaFu.Common import Test.DejaFu.Conc.Internal.Common import Test.DejaFu.Conc.Internal.Memory import Test.DejaFu.Conc.Internal.Threading-import Test.DejaFu.STM (Result(..))+import Test.DejaFu.Schedule+import Test.DejaFu.STM (Result(..), runTransaction)  {-# ANN module ("HLint: ignore Use record patterns" :: String) #-} {-# ANN module ("HLint: ignore Use const"           :: String) #-}@@ -36,40 +40,69 @@ -------------------------------------------------------------------------------- -- * Execution +-- | 'Trace' but as a sequence.+type SeqTrace+  = Seq (Decision, [(ThreadId, NonEmpty Lookahead)], ThreadAction)++-- | Run a concurrent computation with a given 'Scheduler' and initial+-- state, returning a failure reason on error. Also returned is the+-- final state of the scheduler, and an execution trace.+runConcurrency :: MonadRef r n+               => Scheduler g+               -> MemType+               -> g+               -> M n r a+               -> n (Either Failure a, g, SeqTrace)+runConcurrency sched memtype g ma = do+  ref <- newRef Nothing++  let c = runCont ma (AStop . writeRef ref . Just . Right)+  let threads = launch' Unmasked initialThread (const c) M.empty+  let ctx = Context { cSchedState = g, cIdSource = initialIdSource, cThreads = threads, cWriteBuf = emptyBuffer, cCaps = 2 }++  (finalCtx, trace) <- runThreads sched memtype ref ctx+  out <- readRef ref+  pure (fromJust out, cSchedState finalCtx, trace)++-- | The context a collection of threads are running in.+data Context n r g = Context+  { cSchedState :: g+  , cIdSource   :: IdSource+  , cThreads    :: Threads n r+  , cWriteBuf   :: WriteBuffer r+  , cCaps       :: Int+  }+ -- | Run a collection of threads, until there are no threads left.------ Note: this returns the trace in reverse order, because it's more--- efficient to prepend to a list than append. As this function isn't--- exposed to users of the library, this is just an internal gotcha to--- watch out for.-runThreads :: MonadRef r n => (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))-           -> Scheduler ThreadId ThreadAction Lookahead g -> MemType -> g -> Threads n r s -> IdSource -> r (Maybe (Either Failure a)) -> n (g, Trace ThreadId ThreadAction Lookahead)-runThreads runstm sched memtype origg origthreads idsrc ref = go idsrc [] Nothing origg origthreads emptyBuffer 2 where-  go idSource sofar prior g threads wb caps-    | isTerminated  = stop g-    | isDeadlocked  = die g Deadlock-    | isSTMLocked   = die g STMDeadlock-    | isAborted     = die g' Abort-    | isNonexistant = die g' InternalError-    | isBlocked     = die g' InternalError+runThreads :: MonadRef r n+           => Scheduler g -> MemType -> r (Maybe (Either Failure a)) -> Context n r g -> n (Context n r g, SeqTrace)+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' }     | otherwise = do-      stepped <- stepThread runstm memtype (_continuation $ fromJust thread) idSource chosen threads wb caps+      stepped <- stepThread sched memtype chosen (_continuation $ fromJust thread) $ ctx { cSchedState = g' }       case stepped of-        Right (threads', idSource', act, wb', caps') -> loop threads' idSource' act wb' caps'-+        Right (ctx', actOrTrc) -> loop actOrTrc ctx'         Left UncaughtException-          | chosen == initialThread -> die g' UncaughtException-          | otherwise -> loop (kill chosen threads) idSource Killed wb caps--        Left failure -> die g' failure+          | 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' }      where-      (choice, g')  = sched (map (\(d,_,a) -> (d,a)) $ reverse sofar) ((\p (_,_,a) -> (p,a)) <$> prior <*> listToMaybe sofar) (fromList $ map (\(t,l:|_) -> (t,l)) runnable') g+      (choice, g')  = sched sofarSched prior (fromList $ map (\(t,l:|_) -> (t,l)) runnable') (cSchedState ctx)       chosen        = fromJust choice       runnable'     = [(t, nextActions t) | t <- sort $ M.keys runnable]       runnable      = M.filter (isNothing . _blocking) threadsc       thread        = M.lookup chosen threadsc-      threadsc      = addCommitThreads wb threads+      threadsc      = addCommitThreads (cWriteBuf ctx) threads+      threads       = cThreads ctx       isAborted     = isNothing choice       isBlocked     = isJust . _blocking $ fromJust thread       isNonexistant = isNothing thread@@ -87,299 +120,265 @@           _ -> thrd        decision-        | Just chosen == prior = Continue-        | prior `notElem` map (Just . fst) runnable' = Start chosen+        | Just chosen == (fst <$> prior) = Continue+        | (fst <$> prior) `notElem` map (Just . fst) runnable' = Start chosen         | otherwise = SwitchTo chosen        nextActions t = lookahead . _continuation . fromJust $ M.lookup t threadsc -      stop outg = pure (outg, sofar)-      die  outg reason = writeRef ref (Just $ Left reason) >> stop outg+      stop finalCtx = pure (finalCtx, sofar)+      die reason finalCtx = writeRef ref (Just $ Left reason) >> stop finalCtx -      loop threads' idSource' act wb' =-        let sofar' = ((decision, runnable', act) : sofar)-            threads'' = if (interruptible <$> M.lookup chosen threads') /= Just False then unblockWaitingOn chosen threads' else threads'-        in go idSource' sofar' (Just chosen) g' (delCommitThreads threads'') wb'+      loop trcOrAct ctx' =+        let (act, trc) = case trcOrAct of+              Left (a, as) -> (a, (decision, runnable', a) <| as)+              Right a      -> (a, Seq.singleton (decision, runnable', a))+            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' }  -------------------------------------------------------------------------------- -- * Single-step execution  -- | Run a single thread one step, by dispatching on the type of -- 'Action'.-stepThread :: forall n r s. MonadRef r n-  => (forall x. s x -> IdSource -> n (Result x, IdSource, TTrace))-  -- ^ Run a 'MonadSTM' transaction atomically.+stepThread :: forall n r g. MonadRef r n+  => Scheduler g+  -- ^ The scheduler.   -> MemType-  -- ^ The memory model-  -> Action n r s-  -- ^ Action to step-  -> IdSource-  -- ^ Source of fresh IDs+  -- ^ The memory model to use.   -> ThreadId   -- ^ ID of the current thread-  -> Threads n r s-  -- ^ Current state of threads-  -> WriteBuffer r-  -- ^ @CRef@ write buffer-  -> Int-  -- ^ The number of capabilities-  -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))-stepThread runstm memtype action idSource tid threads wb caps = case action of-  AFork    n a b   -> stepFork        n a b-  AMyTId   c       -> stepMyTId       c-  AGetNumCapabilities   c -> stepGetNumCapabilities c-  ASetNumCapabilities i c -> stepSetNumCapabilities i c-  AYield   c       -> stepYield       c-  ANewVar  n c     -> stepNewVar      n c-  APutVar  var a c -> stepPutVar      var a c-  ATryPutVar var a c -> stepTryPutVar var a c-  AReadVar var c   -> stepReadVar     var c-  ATakeVar var c   -> stepTakeVar     var c-  ATryTakeVar var c -> stepTryTakeVar var c-  ANewRef  n a c   -> stepNewRef      n a c-  AReadRef ref c   -> stepReadRef     ref c-  AReadRefCas ref c -> stepReadRefCas ref c-  AModRef  ref f c -> stepModRef      ref f c-  AModRefCas ref f c -> stepModRefCas ref f c-  AWriteRef ref a c -> stepWriteRef   ref a c-  ACasRef ref tick a c -> stepCasRef ref tick a c-  ACommit  t c     -> stepCommit      t c-  AAtom    stm c   -> stepAtom        stm c-  ALift    na      -> stepLift        na-  AThrow   e       -> stepThrow       e-  AThrowTo t e c   -> stepThrowTo     t e c-  ACatching h ma c -> stepCatching    h ma c-  APopCatching a   -> stepPopCatching a-  AMasking m ma c  -> stepMasking     m ma c-  AResetMask b1 b2 m c -> stepResetMask b1 b2 m c-  AReturn     c    -> stepReturn c-  AMessage    m c  -> stepMessage m c-  AStop       na   -> stepStop na+  -> Action n r+  -- ^ Action to step+  -> Context n r g+  -- ^ The execution context.+  -> n (Either Failure (Context n r g, Either (ThreadAction, SeqTrace) ThreadAction))+stepThread sched memtype tid action ctx = case action of+    -- start a new thread, assigning it the next 'ThreadId'+    AFork n a b -> pure . Right $+        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)) -  where-    -- | Start a new thread, assigning it the next 'ThreadId'-    ---    -- Explicit type signature needed for GHC 8. Looks like the-    -- impredicative polymorphism checks got stronger.-    stepFork :: String-             -> ((forall b. M n r s b -> M n r s b) -> Action n r s)-             -> (ThreadId -> Action n r s)-             -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))-    stepFork n a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid, wb, caps) where-      threads' = launch tid newtid a threads-      (idSource', newtid) = nextTId n idSource+    -- get the 'ThreadId' of the current thread+    AMyTId c -> simple (goto (c tid) tid (cThreads ctx)) MyThreadId -    -- | Get the 'ThreadId' of the current thread-    stepMyTId c = simple (goto (c tid) tid threads) MyThreadId+    -- get the number of capabilities+    AGetNumCapabilities c -> simple (goto (c (cCaps ctx)) tid (cThreads ctx)) $ GetNumCapabilities (cCaps ctx) -    -- | Get the number of capabilities-    stepGetNumCapabilities c = simple (goto (c caps) tid threads) $ GetNumCapabilities caps+    -- set the number of capabilities+    ASetNumCapabilities i c -> pure . Right $+      (ctx { cThreads = goto c tid (cThreads ctx), cCaps = i }, Right (SetNumCapabilities i)) -    -- | Set the number of capabilities-    stepSetNumCapabilities i c = return $ Right (goto c tid threads, idSource, SetNumCapabilities i, wb, i)+    -- yield the current thread+    AYield c -> simple (goto c tid (cThreads ctx)) Yield -    -- | Yield the current thread-    stepYield c = simple (goto c tid threads) Yield+    -- create a new @MVar@, using the next 'MVarId'.+    ANewMVar n c -> do+      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)) -    -- | Put a value into a @MVar@, blocking the thread until it's-    -- empty.-    stepPutVar cvar@(MVar cvid _) a c = synchronised $ do-      (success, threads', woken) <- putIntoMVar cvar a c tid threads-      simple threads' $ if success then PutVar cvid woken else BlockedPutVar cvid+    -- put a value into a @MVar@, blocking the thread until it's empty.+    APutMVar cvar@(MVar cvid _) a c -> synchronised $ do+      (success, threads', woken) <- putIntoMVar cvar a c tid (cThreads ctx)+      simple threads' $ if success then PutMVar cvid woken else BlockedPutMVar cvid -    -- | Try to put a value into a @MVar@, without blocking.-    stepTryPutVar cvar@(MVar cvid _) a c = synchronised $ do-      (success, threads', woken) <- tryPutIntoMVar cvar a c tid threads-      simple threads' $ TryPutVar cvid success woken+    -- try to put a value into a @MVar@, without blocking.+    ATryPutMVar cvar@(MVar cvid _) a c -> synchronised $ do+      (success, threads', woken) <- tryPutIntoMVar cvar a c tid (cThreads ctx)+      simple threads' $ TryPutMVar cvid success woken -    -- | Get the value from a @MVar@, without emptying, blocking the+    -- get the value from a @MVar@, without emptying, blocking the     -- thread until it's full.-    stepReadVar cvar@(MVar cvid _) c = synchronised $ do-      (success, threads', _) <- readFromMVar cvar c tid threads-      simple threads' $ if success then ReadVar cvid else BlockedReadVar cvid+    AReadMVar cvar@(MVar cvid _) c -> synchronised $ do+      (success, threads', _) <- readFromMVar cvar c tid (cThreads ctx)+      simple threads' $ if success then ReadMVar cvid else BlockedReadMVar cvid -    -- | Take the value from a @MVar@, blocking the thread until it's+    -- try to get the value from a @MVar@, without emptying, without+    -- blocking.+    ATryReadMVar cvar@(MVar cvid _) c -> synchronised $ do+      (success, threads', _) <- tryReadFromMVar cvar c tid (cThreads ctx)+      simple threads' $ TryReadMVar cvid success++    -- take the value from a @MVar@, blocking the thread until it's     -- full.-    stepTakeVar cvar@(MVar cvid _) c = synchronised $ do-      (success, threads', woken) <- takeFromMVar cvar c tid threads-      simple threads' $ if success then TakeVar cvid woken else BlockedTakeVar cvid+    ATakeMVar cvar@(MVar cvid _) c -> synchronised $ do+      (success, threads', woken) <- takeFromMVar cvar c tid (cThreads ctx)+      simple threads' $ if success then TakeMVar cvid woken else BlockedTakeMVar cvid -    -- | Try to take the value from a @MVar@, without blocking.-    stepTryTakeVar cvar@(MVar cvid _) c = synchronised $ do-      (success, threads', woken) <- tryTakeFromMVar cvar c tid threads-      simple threads' $ TryTakeVar cvid success woken+    -- try to take the value from a @MVar@, without blocking.+    ATryTakeMVar cvar@(MVar cvid _) c -> synchronised $ do+      (success, threads', woken) <- tryTakeFromMVar cvar c tid (cThreads ctx)+      simple threads' $ TryTakeMVar cvid success woken -    -- | Read from a @CRef@.-    stepReadRef cref@(CRef crid _) c = do+    -- create a new @CRef@, using the next 'CRefId'.+    ANewCRef n a c -> do+      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))++    -- read from a @CRef@.+    AReadCRef cref@(CRef crid _) c -> do       val <- readCRef cref tid-      simple (goto (c val) tid threads) $ ReadRef crid+      simple (goto (c val) tid (cThreads ctx)) $ ReadCRef crid -    -- | Read from a @CRef@ for future compare-and-swap operations.-    stepReadRefCas cref@(CRef crid _) c = do+    -- read from a @CRef@ for future compare-and-swap operations.+    AReadCRefCas cref@(CRef crid _) c -> do       tick <- readForTicket cref tid-      simple (goto (c tick) tid threads) $ ReadRefCas crid+      simple (goto (c tick) tid (cThreads ctx)) $ ReadCRefCas crid -    -- | Modify a @CRef@.-    stepModRef cref@(CRef crid _) f c = synchronised $ do+    -- modify a @CRef@.+    AModCRef cref@(CRef crid _) f c -> synchronised $ do       (new, val) <- f <$> readCRef cref tid       writeImmediate cref new-      simple (goto (c val) tid threads) $ ModRef crid+      simple (goto (c val) tid (cThreads ctx)) $ ModCRef crid -    -- | Modify a @CRef@ using a compare-and-swap.-    stepModRefCas cref@(CRef crid _) f c = synchronised $ do+    -- modify a @CRef@ using a compare-and-swap.+    AModCRefCas cref@(CRef crid _) f c -> synchronised $ do       tick@(Ticket _ _ old) <- readForTicket cref tid       let (new, val) = f old       void $ casCRef cref tid tick new-      simple (goto (c val) tid threads) $ ModRefCas crid+      simple (goto (c val) tid (cThreads ctx)) $ ModCRefCas crid -    -- | Write to a @CRef@ without synchronising-    stepWriteRef cref@(CRef crid _) a c = case memtype of-      -- Write immediately.+    -- write to a @CRef@ without synchronising.+    AWriteCRef cref@(CRef crid _) a c -> case memtype of+      -- write immediately.       SequentialConsistency -> do         writeImmediate cref a-        simple (goto c tid threads) $ WriteRef crid--      -- Add to buffer using thread id.+        simple (goto c tid (cThreads ctx)) $ WriteCRef crid+      -- add to buffer using thread id.       TotalStoreOrder -> do-        wb' <- bufferWrite wb (tid, Nothing) cref a-        return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)--      -- Add to buffer using both thread id and cref id+        wb' <- bufferWrite (cWriteBuf ctx) (tid, Nothing) cref a+        pure $ Right (ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Right (WriteCRef crid))+      -- add to buffer using both thread id and cref id       PartialStoreOrder -> do-        wb' <- bufferWrite wb (tid, Just crid) cref a-        return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)+        wb' <- bufferWrite (cWriteBuf ctx) (tid, Just crid) cref a+        pure $ Right (ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Right (WriteCRef crid)) -    -- | Perform a compare-and-swap on a @CRef@.-    stepCasRef cref@(CRef crid _) tick a c = synchronised $ do+    -- perform a compare-and-swap on a @CRef@.+    ACasCRef cref@(CRef crid _) tick a c -> synchronised $ do       (suc, tick') <- casCRef cref tid tick a-      simple (goto (c (suc, tick')) tid threads) $ CasRef crid suc+      simple (goto (c (suc, tick')) tid (cThreads ctx)) $ CasCRef crid suc -    -- | Commit a @CRef@ write-    stepCommit t c = do+    -- commit a @CRef@ write+    ACommit t c -> do       wb' <- case memtype of-        -- Shouldn't ever get here+        -- shouldn't ever get here         SequentialConsistency ->           error "Attempting to commit under SequentialConsistency"--        -- Commit using the thread id.-        TotalStoreOrder -> commitWrite wb (t, Nothing)--        -- Commit using the cref id.-        PartialStoreOrder -> commitWrite wb (t, Just c)--      return $ Right (threads, idSource, CommitRef t c, wb', caps)+        -- commit using the thread id.+        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)) -    -- | Run a STM transaction atomically.-    stepAtom stm c = synchronised $ do-      (res, idSource', trace) <- runstm stm idSource+    -- run a STM transaction atomically.+    AAtom stm c -> synchronised $ do+      (res, idSource', trace) <- runTransaction stm (cIdSource ctx)       case res of         Success _ written val ->-          let (threads', woken) = wake (OnTVar written) threads-          in return $ Right (goto (c val) tid threads', idSource', STM trace woken, wb, caps)+          let (threads', woken) = wake (OnTVar written) (cThreads ctx)+          in pure $ Right (ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }, Right (STM trace woken))         Retry touched ->-          let threads' = block (OnTVar touched) tid threads-          in return $ Right (threads', idSource', BlockedSTM trace, wb, caps)+          let threads' = block (OnTVar touched) tid (cThreads ctx)+          in pure $ Right (ctx { cThreads = threads', cIdSource = idSource'}, Right (BlockedSTM trace))         Exception e -> do           res' <- stepThrow e-          return $ case res' of-            Right (threads', _, _, _, _) -> Right (threads', idSource', Throw, wb, caps)+          pure $ case res' of+            Right (ctx', _) -> Right (ctx' { cIdSource = idSource' }, Right Throw)             Left err -> Left err -    -- | Run a subcomputation in an exception-catching context.-    stepCatching h ma c = simple threads' Catching where-      a     = runCont ma      (APopCatching . c)-      e exc = runCont (h exc) (APopCatching . c)--      threads' = goto a tid (catching e tid threads)--    -- | Pop the top exception handler from the thread's stack.-    stepPopCatching a = simple threads' PopCatching where-      threads' = goto a tid (uncatching tid threads)+    -- lift an action from the underlying monad into the @Conc@+    -- computation.+    ALift na -> do+      a <- na+      simple (goto a tid (cThreads ctx)) LiftIO -    -- | Throw an exception, and propagate it to the appropriate+    -- throw an exception, and propagate it to the appropriate     -- handler.-    stepThrow e =-      case propagate (toException e) tid threads of-        Just threads' -> simple threads' Throw-        Nothing -> return $ Left UncaughtException+    AThrow e -> stepThrow e -    -- | Throw an exception to the target thread, and propagate it to+    -- throw an exception to the target thread, and propagate it to     -- the appropriate handler.-    stepThrowTo t e c = synchronised $-      let threads' = goto c tid threads-          blocked  = block (OnMask t) tid threads-      in case M.lookup t threads of+    AThrowTo t e c -> synchronised $+      let threads' = goto c tid (cThreads ctx)+          blocked  = block (OnMask t) tid (cThreads ctx)+      in case M.lookup t (cThreads ctx) of            Just thread              | interruptible thread -> case propagate (toException e) t threads' of                Just threads'' -> simple threads'' $ ThrowTo t                Nothing-                 | t == initialThread -> return $ Left UncaughtException+                 | t == initialThread -> pure $ Left UncaughtException                  | otherwise -> simple (kill t threads') $ ThrowTo t              | otherwise -> simple blocked $ BlockedThrowTo t            Nothing -> simple threads' $ ThrowTo t -    -- | Execute a subcomputation with a new masking state, and give-    -- it a function to run a computation with the current masking-    -- state.-    ---    -- Explicit type sig necessary for checking in the prescence of-    -- 'umask', sadly.-    stepMasking :: MaskingState-                -> ((forall b. M n r s b -> M n r s b) -> M n r s a)-                -> (a -> Action n r s)-                -> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))-    stepMasking m ma c = simple threads' $ SetMasking False m where-      a = runCont (ma umask) (AResetMask False False m' . c)+    -- run a subcomputation in an exception-catching context.+    ACatching h ma c ->+      let a        = runCont ma      (APopCatching . c)+          e exc    = runCont (h exc) (APopCatching . c)+          threads' = goto a tid (catching e tid (cThreads ctx))+      in simple threads' Catching -      m' = _masking . fromJust $ M.lookup tid threads-      umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> return b-      resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k ()+    -- pop the top exception handler from the thread's stack.+    APopCatching a ->+      let threads' = goto a tid (uncatching tid (cThreads ctx))+      in simple threads' PopCatching -      threads' = goto a tid (mask m tid threads)+    -- execute a subcomputation with a new masking state, and give it+    -- a function to run a computation with the current masking state.+    AMasking m ma c ->+      let a = runCont (ma umask) (AResetMask False False m' . c)+          m' = _masking . fromJust $ M.lookup tid (cThreads ctx)+          umask mb = resetMask True m' >> mb >>= \b -> resetMask False m >> pure b+          resetMask typ ms = cont $ \k -> AResetMask typ True ms $ k ()+          threads' = goto a tid (mask m tid (cThreads ctx))+      in simple threads' $ SetMasking False m -    -- | Reset the masking thread of the state.-    stepResetMask b1 b2 m c = simple threads' act where-      act      = (if b1 then SetMasking else ResetMasking) b2 m-      threads' = goto c tid (mask m tid threads) -    -- | Create a new @MVar@, using the next 'MVarId'.-    stepNewVar n c = do-      let (idSource', newmvid) = nextMVId n idSource-      ref <- newRef Nothing-      let mvar = MVar newmvid ref-      return $ Right (goto (c mvar) tid threads, idSource', NewVar newmvid, wb, caps)--    -- | Create a new @CRef@, using the next 'CRefId'.-    stepNewRef n a c = do-      let (idSource', newcrid) = nextCRId n idSource-      ref <- newRef (M.empty, 0, a)-      let cref = CRef newcrid ref-      return $ Right (goto (c cref) tid threads, idSource', NewRef newcrid, wb, caps)+    -- reset the masking thread of the state.+    AResetMask b1 b2 m c ->+      let act      = (if b1 then SetMasking else ResetMasking) b2 m+          threads' = goto c tid (mask m tid (cThreads ctx))+      in simple threads' act -    -- | Lift an action from the underlying monad into the @Conc@-    -- computation.-    stepLift na = do-      a <- na-      simple (goto a tid threads) LiftIO+    -- execute a 'return' or 'pure'.+    AReturn c -> simple (goto c tid (cThreads ctx)) Return -    -- | Execute a 'return' or 'pure'.-    stepReturn c = simple (goto c tid threads) Return+    -- kill the current thread.+    AStop na -> na >> simple (kill tid (cThreads ctx)) Stop -    -- | Add a message to the trace.-    stepMessage m c = simple (goto c tid threads) (Message m)+    -- run a subconcurrent computation.+    ASub ma c+      | M.size (cThreads ctx) > 1 -> pure (Left IllegalSubconcurrency)+      | otherwise -> do+          (res, g', trace) <- runConcurrency sched memtype (cSchedState ctx) ma+          pure $ Right (ctx { cThreads = goto (c res) tid (cThreads ctx), cSchedState = g' }, Left (Subconcurrency, trace))+  where -    -- | Kill the current thread.-    stepStop na = na >> simple (kill tid threads) Stop+    -- this is not inline in the long @case@ above as it's needed by+    -- @AAtom@, @AThrow@, and @AThrowTo@.+    stepThrow e =+      case propagate (toException e) tid (cThreads ctx) of+        Just threads' -> simple threads' Throw+        Nothing -> pure $ Left UncaughtException -    -- | Helper for actions which don't touch the 'IdSource' or-    -- 'WriteBuffer'-    simple threads' act = return $ Right (threads', idSource, act, wb, caps)+    -- helper for actions which only change the threads.+    simple threads' act = pure $ Right (ctx { cThreads = threads' }, Right act) -    -- | Helper for actions impose a write barrier.+    -- helper for actions impose a write barrier.     synchronised ma = do-      writeBarrier wb+      writeBarrier (cWriteBuf ctx)       res <- ma        return $ case res of-        Right (threads', idSource', act', _, caps') -> Right (threads', idSource', act', emptyBuffer, caps')+        Right (ctx', act) -> Right (ctx' { cWriteBuf = emptyBuffer }, act)         _ -> res

@@ -14,10 +14,10 @@ module Test.DejaFu.Conc.Internal.Common where  import Control.Exception (Exception, MaskingState(..))-import Data.Dynamic (Dynamic) import Data.Map.Strict (Map) import Data.List.NonEmpty (NonEmpty, fromList) import Test.DejaFu.Common+import Test.DejaFu.STM (STMLike)  {-# ANN module ("HLint: ignore Use record patterns" :: String) #-} @@ -32,16 +32,16 @@ -- current expression of threads and exception handlers very difficult -- (perhaps even not possible without significant reworking), so I -- abandoned the attempt.-newtype M n r s a = M { runM :: (a -> Action n r s) -> Action n r s }+newtype M n r a = M { runM :: (a -> Action n r) -> Action n r } -instance Functor (M n r s) where+instance Functor (M n r) where     fmap f m = M $ \ c -> runM m (c . f) -instance Applicative (M n r s) where+instance Applicative (M n r) where     pure x  = M $ \c -> AReturn $ c x     f <*> v = M $ \c -> runM f (\g -> runM v (c . g)) -instance Monad (M n r s) where+instance Monad (M n r) where     return  = pure     m >>= k = M $ \c -> runM m (\x -> runM (k x) c) @@ -82,11 +82,11 @@   }  -- | Construct a continuation-passing operation from a function.-cont :: ((a -> Action n r s) -> Action n r s) -> M n r s a+cont :: ((a -> Action n r) -> Action n r) -> M n r a cont = M  -- | Run a CPS computation with the given final computation.-runCont :: M n r s a -> (a -> Action n r s) -> Action n r s+runCont :: M n r a -> (a -> Action n r) -> Action n r runCont = runM  --------------------------------------------------------------------------------@@ -96,68 +96,70 @@ -- only occur as a result of an action, and they cover (most of) the -- primitives of the concurrency. 'spawn' is absent as it is -- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'.-data Action n r s =-    AFork  String ((forall b. M n r s b -> M n r s b) -> Action n r s) (ThreadId -> Action n r s)-  | AMyTId (ThreadId -> Action n r s)+data Action n r =+    AFork  String ((forall b. M n r b -> M n r b) -> Action n r) (ThreadId -> Action n r)+  | AMyTId (ThreadId -> Action n r) -  | AGetNumCapabilities (Int -> Action n r s)-  | ASetNumCapabilities Int (Action n r s)+  | AGetNumCapabilities (Int -> Action n r)+  | ASetNumCapabilities Int (Action n r) -  | forall a. ANewVar String (MVar r a -> Action n r s)-  | forall a. APutVar     (MVar r a) a (Action n r s)-  | forall a. ATryPutVar  (MVar r a) a (Bool -> Action n r s)-  | forall a. AReadVar    (MVar r a) (a -> Action n r s)-  | forall a. ATakeVar    (MVar r a) (a -> Action n r s)-  | forall a. ATryTakeVar (MVar r a) (Maybe a -> Action n r s)+  | forall a. ANewMVar String (MVar r a -> Action n r)+  | forall a. APutMVar     (MVar r a) a (Action n r)+  | forall a. ATryPutMVar  (MVar r a) a (Bool -> Action n r)+  | forall a. AReadMVar    (MVar r a) (a -> Action n r)+  | forall a. ATryReadMVar (MVar r a) (Maybe a -> Action n r)+  | forall a. ATakeMVar    (MVar r a) (a -> Action n r)+  | forall a. ATryTakeMVar (MVar r a) (Maybe a -> Action n r) -  | forall a.   ANewRef String a (CRef r a -> Action n r s)-  | forall a.   AReadRef    (CRef r a) (a -> Action n r s)-  | forall a.   AReadRefCas (CRef r a) (Ticket a -> Action n r s)-  | forall a b. AModRef     (CRef r a) (a -> (a, b)) (b -> Action n r s)-  | forall a b. AModRefCas  (CRef r a) (a -> (a, b)) (b -> Action n r s)-  | forall a.   AWriteRef   (CRef r a) a (Action n r s)-  | forall a.   ACasRef     (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r s)+  | forall a.   ANewCRef String a (CRef r a -> Action n r)+  | forall a.   AReadCRef    (CRef r a) (a -> Action n r)+  | forall a.   AReadCRefCas (CRef r a) (Ticket a -> Action n r)+  | forall a b. AModCRef     (CRef r a) (a -> (a, b)) (b -> Action n r)+  | forall a b. AModCRefCas  (CRef r a) (a -> (a, b)) (b -> Action n r)+  | forall a.   AWriteCRef   (CRef r a) a (Action n r)+  | forall a.   ACasCRef     (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r)    | forall e.   Exception e => AThrow e-  | forall e.   Exception e => AThrowTo ThreadId e (Action n r s)-  | forall a e. Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s)-  | APopCatching (Action n r s)-  | forall a. AMasking MaskingState ((forall b. M n r s b -> M n r s b) -> M n r s a) (a -> Action n r s)-  | AResetMask Bool Bool MaskingState (Action n r s)--  | AMessage    Dynamic (Action n r s)+  | forall e.   Exception e => AThrowTo ThreadId e (Action n r)+  | forall a e. Exception e => ACatching (e -> M n r a) (M n r a) (a -> Action n r)+  | APopCatching (Action n r)+  | forall a. AMasking MaskingState ((forall b. M n r b -> M n r b) -> M n r a) (a -> Action n r)+  | AResetMask Bool Bool MaskingState (Action n r) -  | forall a. AAtom (s a) (a -> Action n r s)-  | ALift (n (Action n r s))-  | AYield  (Action n r s)-  | AReturn (Action n r s)+  | forall a. AAtom (STMLike n r a) (a -> Action n r)+  | ALift (n (Action n r))+  | AYield  (Action n r)+  | AReturn (Action n r)   | ACommit ThreadId CRefId   | AStop (n ()) +  | forall a. ASub (M n r a) (Either Failure a -> Action n r)+ -------------------------------------------------------------------------------- -- * Scheduling & Traces  -- | Look as far ahead in the given continuation as possible.-lookahead :: Action n r s -> NonEmpty Lookahead+lookahead :: Action n r -> NonEmpty Lookahead lookahead = fromList . lookahead' where   lookahead' (AFork _ _ _)           = [WillFork]   lookahead' (AMyTId _)              = [WillMyThreadId]   lookahead' (AGetNumCapabilities _) = [WillGetNumCapabilities]   lookahead' (ASetNumCapabilities i k) = WillSetNumCapabilities i : lookahead' k-  lookahead' (ANewVar _ _)           = [WillNewVar]-  lookahead' (APutVar (MVar c _) _ k)    = WillPutVar c : lookahead' k-  lookahead' (ATryPutVar (MVar c _) _ _) = [WillTryPutVar c]-  lookahead' (AReadVar (MVar c _) _)     = [WillReadVar c]-  lookahead' (ATakeVar (MVar c _) _)     = [WillTakeVar c]-  lookahead' (ATryTakeVar (MVar c _) _)  = [WillTryTakeVar c]-  lookahead' (ANewRef _ _ _)         = [WillNewRef]-  lookahead' (AReadRef (CRef r _) _)     = [WillReadRef r]-  lookahead' (AReadRefCas (CRef r _) _)  = [WillReadRefCas r]-  lookahead' (AModRef (CRef r _) _ _)    = [WillModRef r]-  lookahead' (AModRefCas (CRef r _) _ _) = [WillModRefCas r]-  lookahead' (AWriteRef (CRef r _) _ k) = WillWriteRef r : lookahead' k-  lookahead' (ACasRef (CRef r _) _ _ _) = [WillCasRef r]-  lookahead' (ACommit t c)           = [WillCommitRef t c]+  lookahead' (ANewMVar _ _)           = [WillNewMVar]+  lookahead' (APutMVar (MVar c _) _ k)    = WillPutMVar c : lookahead' k+  lookahead' (ATryPutMVar (MVar c _) _ _) = [WillTryPutMVar c]+  lookahead' (AReadMVar (MVar c _) _)     = [WillReadMVar c]+  lookahead' (ATryReadMVar (MVar c _) _)  = [WillTryReadMVar c]+  lookahead' (ATakeMVar (MVar c _) _)     = [WillTakeMVar c]+  lookahead' (ATryTakeMVar (MVar c _) _)  = [WillTryTakeMVar c]+  lookahead' (ANewCRef _ _ _)         = [WillNewCRef]+  lookahead' (AReadCRef (CRef r _) _)     = [WillReadCRef r]+  lookahead' (AReadCRefCas (CRef r _) _)  = [WillReadCRefCas r]+  lookahead' (AModCRef (CRef r _) _ _)    = [WillModCRef r]+  lookahead' (AModCRefCas (CRef r _) _ _) = [WillModCRefCas r]+  lookahead' (AWriteCRef (CRef r _) _ k) = WillWriteCRef r : lookahead' k+  lookahead' (ACasCRef (CRef r _) _ _ _) = [WillCasCRef r]+  lookahead' (ACommit t c)           = [WillCommitCRef t c]   lookahead' (AAtom _ _)             = [WillSTM]   lookahead' (AThrow _)              = [WillThrow]   lookahead' (AThrowTo tid _ k)      = WillThrowTo tid : lookahead' k@@ -166,7 +168,7 @@   lookahead' (AMasking ms _ _)       = [WillSetMasking False ms]   lookahead' (AResetMask b1 b2 ms k) = (if b1 then WillSetMasking else WillResetMasking) b2 ms : lookahead' k   lookahead' (ALift _)               = [WillLiftIO]-  lookahead' (AMessage m k)          = WillMessage m : lookahead' k   lookahead' (AYield k)              = WillYield : lookahead' k   lookahead' (AReturn k)             = WillReturn : lookahead' k   lookahead' (AStop _)               = [WillStop]+  lookahead' (ASub _ _)              = [WillSubconcurrency]

@@ -126,7 +126,7 @@   flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate cref a  -- | Add phantom threads to the thread list to commit pending writes.-addCommitThreads :: WriteBuffer r -> Threads n r s -> Threads n r s+addCommitThreads :: WriteBuffer r -> Threads n r -> Threads n r addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where   phantoms = [ (ThreadId Nothing $ negate tid, mkthread $ fromJust c)              | ((k, b), tid) <- zip (M.toList wb) [1..]@@ -136,41 +136,46 @@   go EmptyL = Nothing  -- | Remove phantom threads.-delCommitThreads :: Threads n r s -> Threads n r s+delCommitThreads :: Threads n r -> Threads n r delCommitThreads = M.filterWithKey $ \k _ -> k >= initialThread  -------------------------------------------------------------------------------- -- * Manipulating @MVar@s  -- | Put into a @MVar@, blocking if full.-putIntoMVar :: MonadRef r n => MVar r a -> a -> Action n r s-            -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+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)  -- | Try to put into a @MVar@, not blocking if full.-tryPutIntoMVar :: MonadRef r n => MVar r a -> a -> (Bool -> Action n r s)-               -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+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  -- | Read from a @MVar@, blocking if empty.-readFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r s)-            -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+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) +-- | 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+ -- | Take from a @MVar@, blocking if empty.-takeFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r s)-             -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+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)  -- | Try to take from a @MVar@, not blocking if empty.-tryTakeFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r s)-                -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+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  -- | Mutate a @MVar@, in either a blocking or nonblocking way. mutMVar :: MonadRef r n-        => Bool -> MVar r a -> a -> (Bool -> Action n r s)-        -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+        => Bool -> 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 @@ -191,8 +196,8 @@ -- | Read a @MVar@, in either a blocking or nonblocking -- way. seeMVar :: MonadRef r n-        => Bool -> Bool -> MVar r a -> (Maybe a -> Action n r s)-        -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])+        => Bool -> Bool -> 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 

@@ -27,22 +27,22 @@ -- * Threads  -- | Threads are stored in a map index by 'ThreadId'.-type Threads n r s = Map ThreadId (Thread n r s)+type Threads n r = Map ThreadId (Thread n r)  -- | All the state of a thread.-data Thread n r s = Thread-  { _continuation :: Action n r s+data Thread n r = Thread+  { _continuation :: Action n r   -- ^ The next action to execute.   , _blocking     :: Maybe BlockedOn   -- ^ The state of any blocks.-  , _handlers     :: [Handler n r s]+  , _handlers     :: [Handler n r]   -- ^ Stack of exception handlers   , _masking      :: MaskingState   -- ^ The exception masking state.   }  -- | Construct a thread with just one action-mkthread :: Action n r s -> Thread n r s+mkthread :: Action n r -> Thread n r mkthread c = Thread c Nothing [] Unmasked  --------------------------------------------------------------------------------@@ -53,7 +53,7 @@ data BlockedOn = OnMVarFull MVarId | OnMVarEmpty MVarId | OnTVar [TVarId] | OnMask ThreadId deriving Eq  -- | Determine if a thread is blocked in a certain way.-(~=) :: Thread n r s -> BlockedOn -> Bool+(~=) :: Thread n r -> BlockedOn -> Bool thread ~= theblock = case (_blocking thread, theblock) of   (Just (OnMVarFull  _), OnMVarFull  _) -> True   (Just (OnMVarEmpty _), OnMVarEmpty _) -> True@@ -65,11 +65,11 @@ -- * Exceptions  -- | An exception handler.-data Handler n r s = forall e. Exception e => Handler (e -> Action n r s)+data Handler n r = forall e. Exception e => Handler (e -> Action n r)  -- | Propagate an exception upwards, finding the closest handler -- which can deal with it.-propagate :: SomeException -> ThreadId -> Threads n r s -> Maybe (Threads n r s)+propagate :: SomeException -> ThreadId -> Threads n r -> Maybe (Threads n r) propagate e tid threads = case M.lookup tid threads >>= go . _handlers of   Just (act, hs) -> Just $ except act hs tid threads   Nothing -> Nothing@@ -79,40 +79,40 @@     go (Handler h:hs) = maybe (go hs) (\act -> Just (act, hs)) $ h <$> fromException e  -- | Check if a thread can be interrupted by an exception.-interruptible :: Thread n r s -> Bool+interruptible :: Thread n r -> Bool interruptible thread = _masking thread == Unmasked || (_masking thread == MaskedInterruptible && isJust (_blocking thread))  -- | Register a new exception handler.-catching :: Exception e => (e -> Action n r s) -> ThreadId -> Threads n r s -> Threads n r s+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 }  -- | Remove the most recent exception handler.-uncatching :: ThreadId -> Threads n r s -> Threads n r s+uncatching :: ThreadId -> Threads n r -> Threads n r uncatching = M.alter $ \(Just thread) -> Just $ thread { _handlers = tail $ _handlers thread }  -- | Raise an exception in a thread.-except :: Action n r s -> [Handler n r s] -> ThreadId -> Threads n r s -> Threads n r s+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 }  -- | Set the masking state of a thread.-mask :: MaskingState -> ThreadId -> Threads n r s -> Threads n r s+mask :: MaskingState -> ThreadId -> Threads n r -> Threads n r mask ms = M.alter $ \(Just thread) -> Just $ thread { _masking = ms }  -------------------------------------------------------------------------------- -- * Manipulating threads  -- | Replace the @Action@ of a thread.-goto :: Action n r s -> ThreadId -> Threads n r s -> Threads n r s+goto :: Action n r -> ThreadId -> Threads n r -> Threads n r goto a = M.alter $ \(Just thread) -> Just (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!-launch :: ThreadId -> ThreadId -> ((forall b. M n r s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s+launch :: ThreadId -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r launch parent tid a threads = launch' ms tid a threads where   ms = fromMaybe Unmasked $ _masking <$> M.lookup parent threads  -- | Start a thread with the given ID and masking state. This must not already be in use!-launch' :: MaskingState -> ThreadId -> ((forall b. M n r s b -> M n r s b) -> Action n r s) -> Threads n r s -> Threads n r s+launch' :: MaskingState -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r launch' ms tid a = M.insert tid thread where   thread = Thread { _continuation = a umask, _blocking = Nothing, _handlers = [], _masking = ms } @@ -120,11 +120,11 @@   resetMask typ m = cont $ \k -> AResetMask typ True m $ k ()  -- | Kill a thread.-kill :: ThreadId -> Threads n r s -> Threads n r s+kill :: ThreadId -> Threads n r -> Threads n r kill = M.delete  -- | Block a thread.-block :: BlockedOn -> ThreadId -> Threads n r s -> Threads n r s+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!"@@ -132,7 +132,7 @@ -- | Unblock all threads waiting on the appropriate block. For 'TVar' -- blocks, this will wake all threads waiting on at least one of the -- given 'TVar's.-wake :: BlockedOn -> Threads n r s -> (Threads n r s, [ThreadId])+wake :: BlockedOn -> Threads n r -> (Threads n r, [ThreadId]) wake blockedOn threads = (unblock <$> threads, M.keys $ M.filter isBlocked threads) where   unblock thread     | isBlocked thread = thread { _blocking = Nothing }

@@ -1,4 +1,4 @@-{-# LANGUAGE CPP #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}  -- | -- Module      : Test.DejaFu.SCT@@ -6,12 +6,17 @@ -- License     : MIT -- Maintainer  : Michael Walker <mike@barrucadu.co.uk> -- Stability   : experimental--- Portability : CPP+-- Portability : GeneralizedNewtypeDeriving -- -- Systematic testing for concurrent computations. module Test.DejaFu.SCT-  ( -- * Bounded Partial-order Reduction+  ( -- * Running Concurrent Programs+    Way(..)+  , runSCT+  , resultsSet +  -- * Bounded Partial-order Reduction+   -- | We can characterise the state of a concurrent computation by   -- considering the ordering of dependent events. This is a partial   -- order: independent events can be performed in any order without@@ -23,35 +28,23 @@   -- significantly. /Bounded/ partial-order reduction is a further   -- optimisation, which only considers schedules within some bound.   ---  -- This module provides both a generic function for BPOR, and also a-  -- pre-emption bounding BPOR runner, which is used by the-  -- "Test.DejaFu" module.-  ---  -- See /Bounded partial-order reduction/, K. Coons, M. Musuvathi,-  -- K. McKinley for more details.--    sctBounded--  -- * Combination Bounds--  -- | Combination schedule bounding, where individual bounds are-  -- enabled if they are set.+  -- This module provides a combination pre-emption, fair, and length+  -- bounding runner:   --   -- * Pre-emption + fair bounding is useful for programs which use   --   loop/yield control flows but are otherwise terminating.   --   -- * Pre-emption, fair + length bounding is useful for-  -- non-terminating programs, and used by the testing functionality-  -- in @Test.DejaFu@.+  --   non-terminating programs, and used by the testing functionality+  --   in @Test.DejaFu@.+  --+  -- See /Bounded partial-order reduction/, K. Coons, M. Musuvathi,+  -- K. McKinley for more details.    , Bounds(..)-  , defaultBounds   , noBounds-   , sctBound -  -- * Individual Bounds-   -- ** Pre-emption Bounding    -- | BPOR using pre-emption bounding. This adds conservative@@ -62,10 +55,7 @@   -- See the BPOR paper for more details.    , PreemptionBound(..)-  , defaultPreemptionBound   , sctPreBound-  , pBacktrack-  , pBound    -- ** Fair Bounding @@ -76,10 +66,7 @@   -- See the BPOR paper for more details.    , FairBound(..)-  , defaultFairBound   , sctFairBound-  , fBacktrack-  , fBound    -- ** Length Bounding @@ -87,52 +74,84 @@   -- terms of primitive actions) of an execution.    , LengthBound(..)-  , defaultLengthBound   , sctLengthBound -  -- * Backtracking+  -- * Random Scheduling -  , BacktrackStep(..)-  , BacktrackFunc+  -- | By greatly sacrificing completeness, testing of a large+  -- concurrent system can be greatly sped-up. Counter-intuitively,+  -- random scheduling has better bug-finding behaviour than just+  -- executing a program \"for real\" many times. This is perhaps+  -- because a random scheduler is more chaotic than the real+  -- scheduler.++  , sctRandom   ) where -import Control.DeepSeq (NFData(..)) import Control.Monad.Ref (MonadRef)-import Data.Map.Strict (Map)+import Data.List (foldl') import qualified Data.Map.Strict as M import Data.Maybe (isJust, fromJust)+import Data.Set (Set) import qualified Data.Set as S-import Test.DPOR ( DPOR(..), dpor-                 , BacktrackFunc, BacktrackStep(..), backtrackAt-                 , BoundFunc, (&+&), trueBound-                 , PreemptionBound(..), defaultPreemptionBound, preempBacktrack-                 , FairBound(..), defaultFairBound, fairBound, fairBacktrack-                 , LengthBound(..), defaultLengthBound, lenBound, lenBacktrack-                 )+import System.Random (RandomGen)  import Test.DejaFu.Common import Test.DejaFu.Conc+import Test.DejaFu.SCT.Internal  -------------------------------------------------------------------------------+-- Running Concurrent Programs++-- | How to explore the possible executions of a concurrent program.+data Way g+  = Systematically Bounds+  -- ^ Systematically explore all executions within the bounds.+  | Randomly g Int+  -- ^ Explore a fixed number of random executions, with the given+  -- PRNG.+  deriving (Eq, Ord, Read, Show)++-- | Explore possible executions of a concurrent program.+--+-- * If the 'Way' is @Systematically@, 'sctBound' is used.+--+-- * If the 'Way' is @Randomly@, 'sctRandom' is used.+runSCT :: (MonadRef r n, RandomGen g)+  => Way g+  -- ^ How to run the concurrent program.+  -> MemType+  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -> Conc n r a+  -- ^ The computation to run many times.+  -> n [(Either Failure a, Trace)]+runSCT (Systematically cb) memtype = sctBound memtype cb+runSCT (Randomly g lim)    memtype = sctRandom memtype g lim++-- | Return the set of results of a concurrent program.+resultsSet :: (MonadRef r n, RandomGen g, Ord a)+  => Way g+  -- ^ How to run the concurrent program.+  -> MemType+  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -> Conc n r a+  -- ^ The computation to run many times.+  -> n (Set (Either Failure a))+resultsSet way memtype conc =+  S.fromList . map fst <$> runSCT way memtype conc++------------------------------------------------------------------------------- -- Combined Bounds  data Bounds = Bounds   { boundPreemp :: Maybe PreemptionBound   , boundFair   :: Maybe FairBound   , boundLength :: Maybe LengthBound-  }---- | All bounds enabled, using their default values.-defaultBounds :: Bounds-defaultBounds = Bounds-  { boundPreemp = Just defaultPreemptionBound-  , boundFair   = Just defaultFairBound-  , boundLength = Just defaultLengthBound-  }+  } deriving (Eq, Ord, Read, Show)  -- | No bounds enabled. This forces the scheduler to just use -- partial-order reduction and sleep sets to prune the search--- space. This will /ONLY/ work if your computation always terminated!+-- space. This will /ONLY/ work if your computation always terminates! noBounds :: Bounds noBounds = Bounds   { boundPreemp = Nothing@@ -140,35 +159,29 @@   , boundLength = Nothing   } --- | An SCT runner using a bounded scheduler-sctBound :: MonadRef r n-  => MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> Bounds-  -- ^ The combined bounds.-  -> Conc n r a-  -- ^ The computation to run many times-  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]-sctBound memtype cb = sctBounded memtype (cBound cb) (cBacktrack cb)- -- | Combination bound function-cBound :: Bounds -> BoundFunc ThreadId ThreadAction Lookahead-cBound (Bounds pb fb lb) = maybe trueBound pBound pb &+& maybe trueBound fBound fb &+& maybe trueBound lenBound lb+cBound :: Bounds -> BoundFunc+cBound (Bounds pb fb lb) =+  maybe trueBound pBound pb &+&+  maybe trueBound fBound fb &+&+  maybe trueBound lBound lb  -- | Combination backtracking function. Add all backtracking points -- corresponding to enabled bound functions. -- -- If no bounds are enabled, just backtrack to the given point.-cBacktrack :: Bounds -> BacktrackFunc ThreadId ThreadAction Lookahead s-cBacktrack (Bounds Nothing Nothing Nothing) bs i t = backtrackAt (const False) False bs i t-cBacktrack (Bounds pb fb lb) bs i t = lBack . fBack $ pBack bs where-  pBack backs = if isJust pb then pBacktrack   backs i t else backs-  fBack backs = if isJust fb then fBacktrack   backs i t else backs-  lBack backs = if isJust lb then lenBacktrack backs i t else backs+cBacktrack :: Bounds -> BacktrackFunc+cBacktrack (Bounds (Just _) _ _) = pBacktrack+cBacktrack (Bounds _ (Just _) _) = fBacktrack+cBacktrack (Bounds _ _ (Just _)) = lBacktrack+cBacktrack _ = backtrackAt (\_ _ -> False)  ------------------------------------------------------------------------------- -- Pre-emption bounding +newtype PreemptionBound = PreemptionBound Int+  deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)+ -- | An SCT runner using a pre-emption bounding scheduler. sctPreBound :: MonadRef r n   => MemType@@ -178,25 +191,40 @@   -- execution   -> Conc n r a   -- ^ The computation to run many times-  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]-sctPreBound memtype pb = sctBounded memtype (pBound pb) pBacktrack+  -> n [(Either Failure a, Trace)]+sctPreBound memtype pb = sctBound memtype $ Bounds (Just pb) Nothing Nothing +-- | Pre-emption bound function. This does not count pre-emptive+-- context switches to a commit thread.+pBound :: PreemptionBound -> BoundFunc+pBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb+ -- | Add a backtrack point, and also conservatively add one prior to -- the most recent transition before that point. This may result in -- the same state being reached multiple times, but is needed because -- of the artificial dependency imposed by the bound.-pBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s-pBacktrack = preempBacktrack isCommitRef+pBacktrack :: BacktrackFunc+pBacktrack bs = backtrackAt (\_ _ -> False) bs . concatMap addConservative where+  addConservative o@(i, _, tid) = o : case conservative i of+    Just j  -> [(j, True, tid)]+    Nothing -> [] --- | Pre-emption bound function. This is different to @preempBound@ in--- that it does not count pre-emptive context switches to a commit--- thread.-pBound :: PreemptionBound -> BoundFunc ThreadId ThreadAction Lookahead-pBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb+  -- index of conservative point+  conservative i = go (reverse (take (i-1) bs)) (i-1) where+    go _ (-1) = Nothing+    go (b1:rest@(b2:_)) j+      | bcktThreadid b1 /= bcktThreadid b2+        && not (isCommitRef $ bcktAction b1)+        && not (isCommitRef $ bcktAction b2) = Just j+      | otherwise = go rest (j-1)+    go _ _ = Nothing  ------------------------------------------------------------------------------- -- Fair bounding +newtype FairBound = FairBound Int+  deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)+ -- | An SCT runner using a fair bounding scheduler. sctFairBound :: MonadRef r n   => MemType@@ -206,21 +234,26 @@   -- performed by different threads.   -> Conc n r a   -- ^ The computation to run many times-  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]-sctFairBound memtype fb = sctBounded memtype (fBound fb) fBacktrack+  -> n [(Either Failure a, Trace)]+sctFairBound memtype fb = sctBound memtype $ Bounds Nothing (Just fb) Nothing  -- | Fair bound function-fBound :: FairBound -> BoundFunc ThreadId ThreadAction Lookahead-fBound = fairBound didYield willYield (\act -> case act of Fork t -> [t]; _ -> [])+fBound :: FairBound -> BoundFunc+fBound (FairBound fb) ts (_, l) = maxYieldCountDiff ts l <= fb  -- | Add a backtrack point. If the thread isn't runnable, or performs -- a release operation, add all runnable threads.-fBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s-fBacktrack = fairBacktrack willRelease+fBacktrack :: BacktrackFunc+fBacktrack = backtrackAt check where+  -- True if a release operation is performed.+  check t b = Just True == (willRelease <$> M.lookup t (bcktRunnable b))  ------------------------------------------------------------------------------- -- Length bounding +newtype LengthBound = LengthBound Int+  deriving (Enum, Eq, Ord, Num, Real, Integral, Read, Show)+ -- | An SCT runner using a length bounding scheduler. sctLengthBound :: MonadRef r n   => MemType@@ -230,80 +263,105 @@   -- actions.   -> Conc n r a   -- ^ The computation to run many times-  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]-sctLengthBound memtype lb = sctBounded memtype (lenBound lb) lenBacktrack+  -> n [(Either Failure a, Trace)]+sctLengthBound memtype lb = sctBound memtype $ Bounds Nothing Nothing (Just lb) +-- | Length bound function+lBound :: LengthBound -> BoundFunc+lBound (LengthBound lb) ts _ = length ts < lb++-- | Add a backtrack point. If the thread isn't runnable, add all+-- runnable threads.+lBacktrack :: BacktrackFunc+lBacktrack = backtrackAt (\_ _ -> False)+ ---------------------------------------------------------------------------------- DPOR+-- Systematic concurrency testing  -- | SCT via BPOR. -- -- Schedules are generated by running the computation with a--- deterministic scheduler with some initial list of decisions, after--- which the supplied function is called. At each step of execution,--- possible-conflicting actions are looked for, if any are found,--- \"backtracking points\" are added, to cause the events to happen in--- a different order in a future execution.+-- deterministic scheduler with some initial list of decisions. At+-- each step of execution, possible-conflicting actions are looked+-- for, if any are found, \"backtracking points\" are added, to cause+-- the events to happen in a different order in a future execution. -- -- Note that unlike with non-bounded partial-order reduction, this may -- do some redundant work as the introduction of a bound can make -- previously non-interfering events interfere with each other.-sctBounded :: MonadRef r n+sctBound :: MonadRef r n   => MemType   -- ^ The memory model to use for non-synchronised @CRef@ operations.-  -> BoundFunc ThreadId ThreadAction Lookahead-  -- ^ Check if a prefix trace is within the bound-  -> BacktrackFunc ThreadId ThreadAction Lookahead DepState-  -- ^ Add a new backtrack point, this takes the history of the-  -- execution so far, the index to insert the backtracking point, and-  -- the thread to backtrack to. This may insert more than one-  -- backtracking point.+  -> Bounds+  -- ^ The combined bounds.   -> Conc n r a-  -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]-sctBounded memtype bf backtrack conc =-  dpor didYield-       willYield-       initialDepState-       updateDepState-       (dependent  memtype)-       (dependent' memtype)-#if MIN_VERSION_dpor(0,2,0)-       -- dpor-0.2 knows about daemon threads.-       (\_ (t, l) _ -> t == initialThread && case l of WillStop -> True; _ -> False)-#endif-       initialThread-       (>=initialThread)-       bf-       backtrack-       pruneCommits-       (\sched s -> runConcurrent sched memtype s conc)+  -- ^ The computation to run many times+  -> n [(Either Failure a, Trace)]+sctBound 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 nextPrefix dp of+    Just (prefix, conservative, sleep) -> do+      (res, s, trace) <- runConcurrent scheduler+                                       memtype+                                       (initialDPORSchedState sleep prefix)+                                       conc ----------------------------------------------------------------------------------- Post-processing+      let bpoints = findBacktracks (schedBoundKill s) (schedBPoints s) trace+      let newDPOR = addTrace conservative trace dp --- | Remove commits from the todo sets where every other action will--- result in a write barrier (and so a commit) occurring.------ To get the benefit from this, do not execute commit actions from--- the todo set until there are no other choises.-pruneCommits :: DPOR ThreadId ThreadAction -> DPOR ThreadId ThreadAction-pruneCommits bpor-  | not onlycommits || not alldonesync = go bpor-  | otherwise = go bpor { dporTodo = M.empty }+      if schedIgnore s+      then go newDPOR+      else ((res, trace):) <$> go (addBacktracks bpoints newDPOR) -  where-    go b = b { dporDone = pruneCommits <$> dporDone bpor }+    Nothing -> pure [] -    onlycommits = all (<initialThread) . M.keys $ dporTodo bpor-    alldonesync = all barrier . M.elems $ dporDone bpor+  -- Find the next schedule prefix.+  nextPrefix = findSchedulePrefix (>=initialThread) -    barrier = isBarrier . simplifyAction . fromJust . dporAction+  -- The DPOR scheduler.+  scheduler = dporSched (dependent memtype) (cBound cb) +  -- Find the new backtracking steps.+  findBacktracks = findBacktrackSteps (dependent' memtype) (cBacktrack cb)++  -- Incorporate a trace into the DPOR tree.+  addTrace = incorporateTrace (dependent memtype)++  -- Incorporate the new backtracking steps into the DPOR tree.+  addBacktracks = incorporateBacktrackSteps (cBound cb)++-- | SCT via random scheduling.+--+-- Schedules are generated by assigning to each new thread a random+-- weight. Threads are then scheduled by a weighted random selection.+--+-- This is not guaranteed to find all distinct results.+sctRandom :: (MonadRef r n, RandomGen g)+  => MemType+  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -> g+  -- ^ The random number generator.+  -> Int+  -- ^ The number of executions to perform.+  -> Conc n r a+  -- ^ The computation to run many times.+  -> n [(Either Failure a, Trace)]+sctRandom memtype g0 lim0 conc = go g0 lim0 where+  go _ 0 = pure []+  go g n = do+    (res, s, trace) <- runConcurrent randSched+                                     memtype+                                     (initialRandSchedState g)+                                     conc++    ((res, trace):) <$> go (schedGen s) (n-1)+ ------------------------------------------------------------------------------- -- Dependency function  -- | Check if an action is dependent on another.-dependent :: MemType -> DepState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool+dependent :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool -- This is basically the same as 'dependent'', but can make use of the -- additional information in a 'ThreadAction' to make different -- decisions in a few cases:@@ -327,14 +385,14 @@ --  - Dependency of STM transactions can be /greatly/ improved here, --    as the 'Lookahead' does not know which @TVar@s will be touched, --    and so has to assume all transactions are dependent.-dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b-dependent _ ds (_, ThrowTo t) (t2, a) = t == t2 && canInterrupt ds t2 a-dependent memtype ds (t1, a1) (t2, a2) = case rewind a2 of+dependent _ _ _ (SetNumCapabilities a) _ (GetNumCapabilities b) = a /= b+dependent _ ds _ (ThrowTo t) t2 a = t == t2 && canInterrupt ds t2 a+dependent memtype ds t1 a1 t2 a2 = case rewind a2 of   Just l2     | isSTM a1 && isSTM a2       -> not . S.null $ tvarsOf a1 `S.intersection` tvarsOf a2     | not (isBlock a1 && isBarrier (simplifyLookahead l2)) ->-      dependent' memtype ds (t1, a1) (t2, l2)+      dependent' memtype ds t1 a1 t2 l2   _ -> dependentActions memtype ds (simplifyAction a1) (simplifyAction a2)    where@@ -343,17 +401,11 @@     isSTM _ = False  -- | Variant of 'dependent' to handle 'Lookahead'.-dependent' :: MemType -> DepState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool-dependent' memtype ds (t1, a1) (t2, l2) = case (a1, l2) of-#if MIN_VERSION_dpor(0,2,0)-  -- dpor-0.2 handles this case, woo.-#else-  -- Because Haskell threads are daemonised, when the initial thread-  -- stops all child threads do too, this imposes a dependency.-  (Stop, _)     | t1 == initialThread -> True-  (_, WillStop) | t2 == initialThread -> True-#endif-+--+-- Termination of the initial thread is handled specially in the DPOR+-- implementation.+dependent' :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool+dependent' memtype ds t1 a1 t2 l2 = case (a1, l2) of   -- Worst-case assumption: all IO is dependent.   (LiftIO, WillLiftIO) -> True @@ -392,9 +444,11 @@   -- Unsynchronised reads and writes are always dependent, even under   -- a relaxed memory model, as an unsynchronised write gives rise to   -- a commit, which synchronises.-  (UnsynchronisedRead  r1, UnsynchronisedWrite r2) -> r1 == r2-  (UnsynchronisedWrite r1, UnsynchronisedRead  r2) -> r1 == r2-  (UnsynchronisedWrite r1, UnsynchronisedWrite r2) -> r1 == r2+  (UnsynchronisedRead          r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> a2 /= UnsynchronisedRead r1+  (UnsynchronisedWrite         r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True+  (PartiallySynchronisedWrite  r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True+  (PartiallySynchronisedModify r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True+  (SynchronisedModify          r1, _) | same crefOf && a2 /= PartiallySynchronisedCommit r1 -> True    -- Unsynchronised writes and synchronisation where the buffer is not   -- empty.@@ -420,121 +474,62 @@     same f = isJust (f a1) && f a1 == f a2  ---------------------------------------------------------------------------------- Dependency function state--data DepState = DepState-  { depCRState :: Map CRefId Bool-  -- ^ Keep track of which @CRef@s have buffered writes.-  , depMaskState :: Map ThreadId MaskingState-  -- ^ Keep track of thread masking states. If a thread isn't present,-  -- the masking state is assumed to be @Unmasked@. This nicely-  -- provides compatibility with dpor-0.1, where the thread IDs are-  -- not available.-  }--instance NFData DepState where-  -- Cheats: 'MaskingState' has no 'NFData' instance.-  rnf ds = rnf (depCRState ds, M.keys (depMaskState ds))---- | Initial dependency state.-initialDepState :: DepState-initialDepState = DepState M.empty M.empty---- | Update the 'CRef' buffer state with the action that has just--- happened.-#if MIN_VERSION_dpor(0,2,0)-updateDepState :: DepState -> (ThreadId, ThreadAction) -> DepState-updateDepState depstate (tid, act) = DepState-  { depCRState   = updateCRState       act $ depCRState   depstate-  , depMaskState = updateMaskState tid act $ depMaskState depstate-  }-#else-updateDepState :: DepState -> ThreadAction -> DepState-updateDepState depstate act = depstate-  { depCRState = updateCRState act $ depCRState depstate }-#endif---- | Update the 'CRef' buffer state with the action that has just--- happened.-updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool-updateCRState (CommitRef _ r) = M.delete r-updateCRState (WriteRef    r) = M.insert r True-updateCRState ta-  | isBarrier $ simplifyAction ta = const M.empty-  | otherwise = id---- | Update the thread masking state with the action that has just--- happened.-updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState-updateMaskState tid (Fork tid2) = \masks -> case M.lookup tid masks of-  -- A thread inherits the masking state of its parent.-  Just ms -> M.insert tid2 ms masks-  Nothing -> masks-updateMaskState tid (SetMasking   _ ms) = M.insert tid ms-updateMaskState tid (ResetMasking _ ms) = M.insert tid ms-updateMaskState _ _ = id+-- Utilities --- | Check if a 'CRef' has a buffered write pending.-isBuffered :: DepState -> CRefId -> Bool-isBuffered depstate r = M.findWithDefault False r (depCRState depstate)+-- | Determine if an action is a commit or not.+isCommitRef :: ThreadAction -> Bool+isCommitRef (CommitCRef _ _) = True+isCommitRef _ = False --- | Check if an exception can interrupt a thread (action).-canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool-canInterrupt depstate tid act-  -- If masked interruptible, blocked actions can be interrupted.-  | isMaskedInterruptible depstate tid = case act of-    BlockedPutVar  _ -> True-    BlockedReadVar _ -> True-    BlockedTakeVar _ -> True-    BlockedSTM     _ -> True-    BlockedThrowTo _ -> True-    _ -> False-  -- If masked uninterruptible, nothing can be.-  | isMaskedUninterruptible depstate tid = False-  -- If no mask, anything can be.-  | otherwise = True+-- | Extra threads created in a fork.+forkTids :: ThreadAction -> [ThreadId]+forkTids (Fork t) = [t]+forkTids _ = [] --- | Check if an exception can interrupt a thread (lookahead).-canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool-canInterruptL depstate tid lh-  -- If masked interruptible, actions which can block may be-  -- interrupted.-  | isMaskedInterruptible depstate tid = case lh of-    WillPutVar  _ -> True-    WillReadVar _ -> True-    WillTakeVar _ -> True-    WillSTM       -> True-    WillThrowTo _ -> True-    _ -> False-  -- If masked uninterruptible, nothing can be.-  | isMaskedUninterruptible depstate tid = False-  -- If no mask, anything can be.-  | otherwise = True+-- | Count the number of yields by a thread in a schedule prefix.+yieldCount :: ThreadId+  -- ^ The thread to count yields for.+  -> [(Decision, ThreadAction)]+  -> Lookahead+  -> Int+yieldCount tid ts l = go initialThread ts where+  go t ((Start    t', act):rest) = go' t t' act rest+  go t ((SwitchTo t', act):rest) = go' t t' act rest+  go t ((Continue,    act):rest) = go' t t  act rest+  go t []+    | t == tid && willYield l = 1+    | otherwise = 0 --- | Check if a thread is masked interruptible.-isMaskedInterruptible :: DepState -> ThreadId -> Bool-isMaskedInterruptible depstate tid =-  M.lookup tid (depMaskState depstate) == Just MaskedInterruptible+  {-# INLINE go' #-}+  go' t t' act rest+    | t == tid && didYield act = 1 + go t' rest+    | otherwise = go t' rest --- | Check if a thread is masked uninterruptible.-isMaskedUninterruptible :: DepState -> ThreadId -> Bool-isMaskedUninterruptible depstate tid =-  M.lookup tid (depMaskState depstate) == Just MaskedUninterruptible+-- | Get the maximum difference between the yield counts of all+-- threads in this schedule prefix.+maxYieldCountDiff :: [(Decision, ThreadAction)]+  -> Lookahead+  -> Int+maxYieldCountDiff ts l = go 0 yieldCounts where+  go m (yc:ycs) =+    let m' = m `max` foldl' (go' yc) 0 ycs+    in go m' ycs+  go m [] = m+  go' yc0 m yc = m `max` abs (yc0 - yc) ----------------------------------------------------------------------------------- Utilities+  yieldCounts = [yieldCount t ts l | t <- allTids ts] --- | Determine if an action is a commit or not.-isCommitRef :: ThreadAction -> Bool-isCommitRef (CommitRef _ _) = True-isCommitRef _ = False+  -- All the threads created during the lifetime of the system.+  allTids ((_, act):rest) =+    let tids' = forkTids act+    in if null tids' then allTids rest else tids' ++ allTids rest+  allTids [] = [initialThread] --- | Check if a thread yielded.-didYield :: ThreadAction -> Bool-didYield Yield = True-didYield _ = False+-- | The \"true\" bound, which allows everything.+trueBound :: BoundFunc+trueBound _ _ = True --- | Check if a thread will yield.-willYield :: Lookahead -> Bool-willYield WillYield = True-willYield _ = False+-- | Combine two bounds into a larger bound, where both must be+-- satisfied.+(&+&) :: BoundFunc -> BoundFunc -> BoundFunc+(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl

@@ -0,0 +1,712 @@+-- |+-- Module      : Test.DejaFu.SCT.Internal+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : portable+--+-- Internal types and functions for dynamic partial-order+-- reduction. This module is NOT considered to form part of the public+-- interface of this library.+module Test.DejaFu.SCT.Internal where++import Control.Exception (MaskingState(..))+import Data.Char (ord)+import Data.Function (on)+import qualified Data.Foldable as F+import Data.List (intercalate, nubBy, partition, sortOn)+import Data.List.NonEmpty (NonEmpty(..), toList)+import Data.Map.Strict (Map)+import Data.Maybe (catMaybes, fromJust, isNothing, listToMaybe)+import qualified Data.Map.Strict as M+import Data.Set (Set)+import qualified Data.Set as S+import Data.Sequence (Seq, (|>))+import qualified Data.Sequence as Sq+import System.Random (RandomGen, randomR)++import Test.DejaFu.Common+import Test.DejaFu.Schedule (Decision(..), Scheduler, decisionOf, tidOf)++-------------------------------------------------------------------------------+-- * Dynamic partial-order reduction++-- | DPOR execution is represented as a tree of states, characterised+-- by the decisions that lead to that state.+data DPOR = DPOR+  { dporRunnable :: Set ThreadId+  -- ^ What threads are runnable at this step.+  , 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.+  , dporSleep    :: Map ThreadId ThreadAction+  -- ^ Transitions to ignore (in this node and children) until a+  -- dependent transition happens.+  , dporTaken    :: Map ThreadId ThreadAction+  -- ^ 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 Show++-- | One step of the execution, including information for backtracking+-- purposes. This backtracking information is used to generate new+-- schedules.+data BacktrackStep = BacktrackStep+  { bcktThreadid   :: ThreadId+  -- ^ The thread running at this step+  , bcktDecision   :: Decision+  -- ^ What was decided at this step.+  , bcktAction     :: ThreadAction+  -- ^ What happened at this step.+  , bcktRunnable   :: Map ThreadId Lookahead+  -- ^ The threads runnable at this step+  , bcktBacktracks :: Map ThreadId Bool+  -- ^ The list of alternative threads to run, and whether those+  -- alternatives were added conservatively due to the bound.+  , bcktState      :: DepState+  -- ^ Some domain-specific state at this point.+  } deriving Show++-- | Initial DPOR state, given an initial thread ID. This initial+-- thread should exist and be runnable at the start of execution.+initialState :: DPOR+initialState = DPOR+  { dporRunnable = S.singleton initialThread+  , dporTodo     = M.singleton initialThread False+  , dporDone     = M.empty+  , dporSleep    = M.empty+  , dporTaken    = M.empty+  , dporAction   = Nothing+  }++-- | Produce a new schedule prefix from a @DPOR@ tree. If there are no new+-- prefixes remaining, return 'Nothing'. Also returns whether the+-- decision was added conservatively, and the sleep set at the point+-- where divergence happens.+--+-- A schedule prefix is a possibly empty sequence of decisions that+-- have already been made, terminated by a single decision from the+-- to-do set. The intent is to put the system into a new state when+-- executed with this initial sequence of scheduling decisions.+findSchedulePrefix+  :: (ThreadId -> Bool)+  -- ^ Some partitioning function, applied to the to-do decisions. If+  -- there is an identifier which passes the test, it will be used,+  -- rather than any which fail it. This allows a very basic way of+  -- domain-specific prioritisation between otherwise equal choices,+  -- which may be useful in some cases.+  -> DPOR+  -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)+findSchedulePrefix predicate = listToMaybe . go where+  go dpor =+    let prefixes = here dpor : map go' (M.toList $ dporDone dpor)+    in case concatPartition (\(t:_,_,_) -> predicate t) prefixes of+         ([], choices) -> choices+         (choices, _)  -> choices++  go' (tid, dpor) = (\(ts,c,slp) -> (tid:ts,c,slp)) <$> go dpor++  -- Prefix traces terminating with a to-do decision at this point.+  here dpor = [([t], c, sleeps dpor) | (t, c) <- M.toList $ dporTodo 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 dpor = 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.+incorporateTrace+  :: (DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool)+  -- ^ Dependency function+  -> Bool+  -- ^ Whether the \"to-do\" point which was used to create this new+  -- execution was conservative or not.+  -> Trace+  -- ^ The execution trace: the decision made, the runnable threads,+  -- and the action performed.+  -> DPOR+  -> DPOR+incorporateTrace dependency conservative trace dpor0 = grow initialDepState (initialDPORThread dpor0) trace dpor0 where+  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 ->+           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+                   }+  grow _ _ [] dpor = dpor++  -- Construct a new subtree corresponding to a trace suffix.+  subtree state tid sleep ((_, _, a):rest) =+    let state' = updateDepState state tid a+        sleep' = M.filterWithKey (\t a' -> not $ dependency state' tid a t a') sleep+    in DPOR+        { dporRunnable = S.fromList $ case rest of+            ((_, runnable, _):_) -> map fst runnable+            [] -> []+        , dporTodo     = M.empty+        , dporDone     = M.fromList $ case rest of+          ((d', _, _):_) ->+            let tid' = tidOf tid d'+            in  [(tid', subtree state' tid' sleep' rest)]+          [] -> []+        , 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!"++-- | Produce a list of new backtracking points from an execution+-- trace. These are then used to inform new \"to-do\" points in the+-- @DPOR@ tree.+--+-- Two traces are passed in to this function: the first is generated+-- from the special DPOR scheduler, the other from the execution of+-- the concurrent program.+--+-- If the trace ends with any threads other than the initial one still+-- runnable, a dependency is imposed between this final action and+-- everything else.+findBacktrackSteps+  :: (DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool)+  -- ^ Dependency function.+  -> BacktrackFunc+  -- ^ Backtracking function. Given a list of backtracking points, and+  -- a thread to backtrack to at a specific point in that list, add+  -- the new backtracking points. There will be at least one: this+  -- chosen one, but the function may add others.+  -> Bool+  -- ^ Whether the computation was aborted due to no decisions being+  -- in-bounds.+  -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])+  -- ^ A sequence of threads at each step: the nonempty list of+  -- runnable threads (with lookahead values), and the list of threads+  -- still to try. The reason for the two separate lists is because+  -- the threads chosen to try will be dependent on the specific+  -- domain.+  -> Trace+  -- ^ The execution trace.+  -> [BacktrackStep]+findBacktrackSteps dependency backtrack boundKill = go initialDepState S.empty initialThread [] . F.toList where+  -- Walk through the traces one step at a time, building up a list of+  -- new backtracking points.+  go state allThreads tid bs ((e,i):is) ((d,_,a):ts) =+    let tid' = tidOf tid d+        state' = updateDepState state tid' a+        this = BacktrackStep+          { bcktThreadid   = tid'+          , bcktDecision   = d+          , bcktAction     = a+          , bcktRunnable   = M.fromList . toList $ e+          , bcktBacktracks = M.fromList $ map (\i' -> (i', False)) i+          , bcktState      = state'+          }+        bs' = doBacktrack killsEarly allThreads' (toList e) (bs++[this])+        runnable = S.fromList (M.keys $ bcktRunnable this)+        allThreads' = allThreads `S.union` runnable+        killsEarly = null ts && boundKill+    in go state' allThreads' tid' bs' is ts+  go _ _ _ bs _ _ = bs++  -- Find the prior actions dependent with this one and add+  -- backtracking points.+  doBacktrack killsEarly allThreads enabledThreads bs =+    let tagged = reverse $ zip [0..] bs+        idxs   = [ (head is, False, u)+                 | (u, n) <- enabledThreads+                 , v <- S.toList allThreads+                 , u /= v+                 , let is = idxs' u n v tagged+                 , not $ null is]++        idxs' u n v = catMaybes . go' True where+          {-# INLINE go' #-}+          go' final ((i,b):rest)+            -- Don't cross subconcurrency boundaries+            | isSubC final b = []+            -- If this is the final action in the trace and the+            -- execution was killed due to nothing being within bounds+            -- (@killsEarly == True@) assume worst-case dependency.+            | bcktThreadid b == v && (killsEarly || isDependent b) = Just i : go' False rest+            | otherwise = go' False rest+          go' _ [] = []++          {-# INLINE isSubC #-}+          isSubC final b = case bcktAction b of+            Stop -> not final && bcktThreadid b == initialThread+            Subconcurrency -> bcktThreadid b == initialThread+            _ -> False++          {-# INLINE isDependent #-}+          isDependent b = dependency (bcktState b) (bcktThreadid b) (bcktAction b) u n+    in backtrack bs idxs++-- | Add new backtracking points, if they have not already been+-- visited, fit into the bound, and aren't in the sleep set.+incorporateBacktrackSteps+  :: ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool)+  -- ^ Bound function: returns true if that schedule prefix terminated+  -- with the lookahead decision fits within the bound.+  -> [BacktrackStep]+  -- ^ Backtracking steps identified by 'findBacktrackSteps'.+  -> DPOR+  -> DPOR+incorporateBacktrackSteps bv = go Nothing [] where+  go priorTid pref (b:bs) bpor =+    let bpor' = doBacktrack priorTid pref b bpor+        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++  doBacktrack priorTid pref b bpor =+    let todo' = [ x+                | x@(t,c) <- M.toList $ bcktBacktracks b+                , let decision  = decisionOf priorTid (dporRunnable bpor) 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)+                ]+    in bpor { dporTodo = dporTodo bpor `M.union` M.fromList todo' }++-------------------------------------------------------------------------------+-- * DPOR scheduler++-- | The scheduler state+data DPORSchedState = DPORSchedState+  { schedSleep     :: Map ThreadId ThreadAction+  -- ^ The sleep set: decisions not to make until something dependent+  -- with them happens.+  , schedPrefix    :: [ThreadId]+  -- ^ Decisions still to make+  , schedBPoints   :: Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])+  -- ^ Which threads are runnable at each step, and the alternative+  -- decisions still to make.+  , schedIgnore    :: Bool+  -- ^ Whether to ignore this execution or not: @True@ if the+  -- execution is aborted due to all possible decisions being in the+  -- sleep set, as then everything in this execution is covered by+  -- another.+  , schedBoundKill :: Bool+  -- ^ Whether the execution was terminated due to all decisions being+  -- out of bounds.+  , schedDepState  :: DepState+  -- ^ State used by the dependency function to determine when to+  -- remove decisions from the sleep set.+  } deriving Show++-- | Initial DPOR scheduler state for a given prefix+initialDPORSchedState :: Map ThreadId ThreadAction+  -- ^ The initial sleep set.+  -> [ThreadId]+  -- ^ The schedule prefix.+  -> DPORSchedState+initialDPORSchedState sleep prefix = DPORSchedState+  { schedSleep     = sleep+  , schedPrefix    = prefix+  , schedBPoints   = Sq.empty+  , schedIgnore    = False+  , schedBoundKill = False+  , schedDepState  = initialDepState+  }++-- | A bounding function takes the scheduling decisions so far and a+-- decision chosen to come next, and returns if that decision is+-- within the bound.+type BoundFunc+  = [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool++-- | A backtracking step is a point in the execution where another+-- decision needs to be made, in order to explore interesting new+-- schedules. A backtracking /function/ takes the steps identified so+-- far and a list of points and thread at that point to backtrack+-- to. More points be added to compensate for the effects of the+-- bounding function. For example, under pre-emption bounding a+-- conservative backtracking point is added at the prior context+-- switch. The bool is whether the point is conservative. Conservative+-- points are always explored, whereas non-conservative ones might be+-- skipped based on future information.+--+-- In general, a backtracking function should identify one or more+-- backtracking points, and then use @backtrackAt@ to do the actual+-- work.+type BacktrackFunc+  = [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep]++-- | Add a backtracking point. If the thread isn't runnable, add all+-- runnable threads. If the backtracking point is already present,+-- don't re-add it UNLESS this would make it conservative.+backtrackAt+  :: (ThreadId -> BacktrackStep -> Bool)+  -- ^ If this returns @True@, backtrack to all runnable threads,+  -- rather than just the given thread.+  -> BacktrackFunc+backtrackAt toAll bs0 = backtrackAt' . nubBy ((==) `on` fst') . sortOn fst' where+  fst' (x,_,_) = x++  backtrackAt' ((i,c,t):is) = go i bs0 i c t is+  backtrackAt' [] = bs0++  go i0 (b:bs) 0 c tid is+    -- If the backtracking point is already present, don't re-add it,+    -- UNLESS this would force it to backtrack (it's conservative)+    -- where before it might not.+    | not (toAll tid b) && tid `M.member` bcktRunnable b =+      let val = M.lookup tid $ bcktBacktracks b+          b' = if isNothing val || (val == Just False && c)+            then b { bcktBacktracks = backtrackTo tid c b }+            else b+      in b' : case is of+        ((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is'+        [] -> bs+    -- Otherwise just backtrack to everything runnable.+    | otherwise =+      let b' = b { bcktBacktracks = backtrackAll c b }+      in b' : case is of+        ((i',c',t'):is') -> go i' bs (i'-i0-1) c' t' is'+        [] -> bs+  go i0 (b:bs) i c tid is = b : go i0 bs (i-1) c tid is+  go _ [] _ _ _ _ = err "backtrackAt" "ran out of schedule whilst backtracking!"++  -- Backtrack to a single thread+  backtrackTo tid c = M.insert tid c . bcktBacktracks++  -- Backtrack to all runnable threads+  backtrackAll c = M.map (const c) . bcktRunnable++-- | DPOR scheduler: takes a list of decisions, and maintains a trace+-- including the runnable threads, and the alternative choices allowed+-- by the bound-specific initialise function.+--+-- After the initial decisions are exhausted, this prefers choosing+-- the prior thread if it's (1) still runnable and (2) hasn't just+-- yielded. Furthermore, threads which /will/ yield are ignored in+-- preference of those which will not.+dporSched+  :: (DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool)+  -- ^ Dependency function.+  -> BoundFunc+  -- ^ Bound function: returns true if that schedule prefix terminated+  -- with the lookahead decision fits within the bound.+  -> Scheduler DPORSchedState+dporSched dependency inBound trc prior threads s = schedule where+  -- Pick a thread to run.+  schedule = case schedPrefix s of+    -- If there is a decision available, make it+    (d:ds) -> (Just d, (nextState []) { schedPrefix = ds })++    -- Otherwise query the initialise function for a list of possible+    -- choices, filter out anything in the sleep set, and make one of+    -- them arbitrarily (recording the others).+    [] ->+      let choices  = restrictToBound initialise+          checkDep t a = case prior of+            Just (tid, act) -> dependency (schedDepState s) tid act t a+            Nothing -> False+          ssleep'  = M.filterWithKey (\t a -> not $ checkDep t a) $ schedSleep s+          choices' = filter (`notElem` M.keys ssleep') choices+          signore' = not (null choices) && all (`elem` M.keys ssleep') choices+          sbkill'  = not (null initialise) && null choices+      in case choices' of+            (nextTid:rest) -> (Just nextTid, (nextState rest) { schedSleep = ssleep' })+            [] -> (Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill' })++  -- The next scheduler state+  nextState rest = s+    { schedBPoints  = schedBPoints s |> (threads, rest)+    , schedDepState = nextDepState+    }+  nextDepState = let ds = schedDepState s in maybe ds (uncurry $ updateDepState ds) prior++  -- Pick a new thread to run, not considering bounds. Choose the+  -- current thread if available and it hasn't just yielded, otherwise+  -- add all runnable threads.+  initialise = tryDaemons . yieldsToEnd $ case prior of+    Just (tid, act)+      | not (didYield act) && tid `elem` tids -> [tid]+    _ -> tids'++  -- If one of the chosen actions will kill the computation, and there+  -- are daemon threads, try them instead.+  --+  -- This is necessary if the killing action is NOT dependent with+  -- every other action, according to the dependency function. This+  -- is, strictly speaking, wrong; an action that kills another thread+  -- is definitely dependent with everything in that thread. HOWEVER,+  -- implementing it that way leads to an explosion of schedules+  -- tried. Really, all that needs to happen is for the+  -- thread-that-would-be-killed to be executed fully ONCE, and then+  -- the normal dependency mechanism will identify any other+  -- backtracking points that should be tried. This is achieved by+  -- adding every thread that would be killed to the to-do list.+  -- Furthermore, these threads MUST be ahead of the killing thread,+  -- or the killing thread will end up in the sleep set and so the+  -- killing action not performed. This is, again, because of the lack+  -- of the dependency messing things up in the name of performance.+  --+  -- See commits a056f54 and 8554ce9, and my 4th June comment in issue+  -- #52.+  tryDaemons ts+    | any doesKill ts = case partition doesKill tids' of+        (kills, nokills) -> nokills ++ kills+    | otherwise = ts+  doesKill t = killsDaemons t (action t)++  -- Restrict the possible decisions to those in the bound.+  restrictToBound = filter (\t -> inBound trc (decision t, action t))++  -- Move the threads which will immediately yield to the end of the list+  yieldsToEnd ts = case partition (willYield . action) ts of+    (yields, noyields) -> noyields ++ yields++  -- Get the decision that will lead to a thread being scheduled.+  decision = decisionOf (fst <$> prior) (S.fromList tids')++  -- Get the action of a thread+  action t = fromJust $ lookup t threads'++  -- The runnable thread IDs+  tids = fst <$> threads++  -- The runnable threads as a normal list.+  threads' = toList threads+  tids'    = toList tids++-------------------------------------------------------------------------------+-- Weighted random scheduler++-- | The scheduler state+data RandSchedState g = RandSchedState+  { schedWeights :: Map ThreadId Int+  -- ^ The thread weights: used in determining which to run.+  , schedGen     :: g+  -- ^ The random number generator.+  }++-- | Initial weighted random scheduler state.+initialRandSchedState :: g -> RandSchedState g+initialRandSchedState = RandSchedState M.empty++-- | Weighted random scheduler: assigns to each new thread a weight,+-- and makes a weighted random choice out of the runnable threads at+-- every step.+randSched :: RandomGen g => Scheduler (RandSchedState g)+randSched _ _ threads s = (pick choice enabled, RandSchedState weights' g'') where+  -- Select a thread+  pick idx ((x, f):xs)+    | idx < f = Just x+    | otherwise = pick (idx - f) xs+  pick _ [] = Nothing+  (choice, g'') = randomR (0, sum (map snd enabled) - 1) g'+  enabled = M.toList $ M.filterWithKey (\tid _ -> tid `elem` tids) weights'++  -- The weights, with any new threads added.+  weights' = schedWeights s `M.union` M.fromList newWeights+  (newWeights, g') = foldr assignWeight ([], schedGen s) $ filter (`M.notMember` schedWeights s) tids+  assignWeight tid ~(ws, g0) =+    let (w, g) = randomR (1, 50) g0+    in ((tid, w):ws, g)++  -- The runnable threads.+  tids = map fst (toList threads)++-------------------------------------------------------------------------------+-- Dependency function state++data DepState = DepState+  { depCRState :: Map CRefId Bool+  -- ^ Keep track of which @CRef@s have buffered writes.+  , depMaskState :: Map ThreadId MaskingState+  -- ^ Keep track of thread masking states. If a thread isn't present,+  -- the masking state is assumed to be @Unmasked@. This nicely+  -- provides compatibility with dpor-0.1, where the thread IDs are+  -- not available.+  } deriving (Eq, Show)++-- | Initial dependency state.+initialDepState :: DepState+initialDepState = DepState M.empty M.empty++-- | Update the 'CRef' buffer state with the action that has just+-- happened.+updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState+updateDepState depstate tid act = DepState+  { depCRState   = updateCRState       act $ depCRState   depstate+  , depMaskState = updateMaskState tid act $ depMaskState depstate+  }++-- | Update the 'CRef' buffer state with the action that has just+-- happened.+updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool+updateCRState (CommitCRef _ r) = M.delete r+updateCRState (WriteCRef    r) = M.insert r True+updateCRState ta+  | isBarrier $ simplifyAction ta = const M.empty+  | otherwise = id++-- | Update the thread masking state with the action that has just+-- happened.+updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState+updateMaskState tid (Fork tid2) = \masks -> case M.lookup tid masks of+  -- A thread inherits the masking state of its parent.+  Just ms -> M.insert tid2 ms masks+  Nothing -> masks+updateMaskState tid (SetMasking   _ ms) = M.insert tid ms+updateMaskState tid (ResetMasking _ ms) = M.insert tid ms+updateMaskState _ _ = id++-- | Check if a 'CRef' has a buffered write pending.+isBuffered :: DepState -> CRefId -> Bool+isBuffered depstate r = M.findWithDefault False r (depCRState depstate)++-- | Check if an exception can interrupt a thread (action).+canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool+canInterrupt depstate tid act+  -- If masked interruptible, blocked actions can be interrupted.+  | isMaskedInterruptible depstate tid = case act of+    BlockedPutMVar  _ -> True+    BlockedReadMVar _ -> True+    BlockedTakeMVar _ -> True+    BlockedSTM      _ -> True+    BlockedThrowTo  _ -> True+    _ -> False+  -- If masked uninterruptible, nothing can be.+  | isMaskedUninterruptible depstate tid = False+  -- If no mask, anything can be.+  | otherwise = True++-- | Check if an exception can interrupt a thread (lookahead).+canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool+canInterruptL depstate tid lh+  -- If masked interruptible, actions which can block may be+  -- interrupted.+  | isMaskedInterruptible depstate tid = case lh of+    WillPutMVar  _ -> True+    WillReadMVar _ -> True+    WillTakeMVar _ -> True+    WillSTM        -> True+    WillThrowTo  _ -> True+    _ -> False+  -- If masked uninterruptible, nothing can be.+  | isMaskedUninterruptible depstate tid = False+  -- If no mask, anything can be.+  | otherwise = True++-- | Check if a thread is masked interruptible.+isMaskedInterruptible :: DepState -> ThreadId -> Bool+isMaskedInterruptible depstate tid =+  M.lookup tid (depMaskState depstate) == Just MaskedInterruptible++-- | Check if a thread is masked uninterruptible.+isMaskedUninterruptible :: DepState -> ThreadId -> Bool+isMaskedUninterruptible depstate tid =+  M.lookup tid (depMaskState depstate) == Just MaskedUninterruptible++-------------------------------------------------------------------------------+-- * Utilities++-- The initial thread of a DPOR tree.+initialDPORThread :: DPOR -> ThreadId+initialDPORThread = S.elemAt 0 . dporRunnable++-- | Check if a thread yielded.+didYield :: ThreadAction -> Bool+didYield Yield = True+didYield _ = False++-- | Check if a thread will yield.+willYield :: Lookahead -> Bool+willYield WillYield = True+willYield _ = False++-- | Check if an action will kill daemon threads.+killsDaemons :: ThreadId -> Lookahead -> Bool+killsDaemons t WillStop = t == initialThread+killsDaemons _ _ = False++-- | Render a 'DPOR' value as a graph in GraphViz \"dot\" format.+toDot :: (ThreadId -> String)+  -- ^ Show a @tid@ - this should produce a string suitable for+  -- use as a node identifier.+  -> (ThreadAction -> String)+  -- ^ Show a @action@.+  -> DPOR+  -> String+toDot = toDotFiltered (\_ _ -> True)++-- | Render a 'DPOR' value as a graph in GraphViz \"dot\" format, with+-- a function to determine if a subtree should be included or not.+toDotFiltered :: (ThreadId -> DPOR -> Bool)+  -- ^ Subtree predicate.+  -> (ThreadId -> String)+  -> (ThreadAction -> String)+  -> DPOR+  -> String+toDotFiltered check showTid showAct = digraph . go "L" where+  digraph str = "digraph {\n" ++ str ++ "\n}"++  go l b = unlines $ node l b : edges l b++  -- Display a labelled node.+  node n b = n ++ " [label=\"" ++ label b ++ "\"]"++  -- Display the edges.+  edges l b = [ edge l l' i ++ go l' b'+              | (i, b') <- M.toList (dporDone b)+              , check i b'+              , let l' = l ++ tidId i+              ]++  -- A node label, summary of the DPOR state at that node.+  label b = showLst id+    [ maybe "Nothing" (("Just " ++) . showAct) $ dporAction b+    , "Run:" ++ showLst showTid (S.toList $ dporRunnable b)+    , "Tod:" ++ showLst showTid (M.keys   $ dporTodo     b)+    , "Slp:" ++ showLst (\(t,a) -> "(" ++ showTid t ++ ", " ++ showAct a ++ ")")+        (M.toList $ dporSleep b)+    ]++  -- Display a labelled edge+  edge n1 n2 l = n1 ++ " -> " ++ n2 ++ " [label=\"" ++ showTid l ++ "\"]\n"++  -- Show a list of values+  showLst showf xs = "[" ++ intercalate ", " (map showf xs) ++ "]"++  -- Generate a graphviz-friendly identifier from a tid.+  tidId = concatMap (show . ord) . showTid++-- | 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)

@@ -0,0 +1,129 @@+-- |+-- Module      : Test.DejaFu.Schedule+-- Copyright   : (c) 2016 Michael Walker+-- License     : MIT+-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>+-- Stability   : experimental+-- Portability : portable+--+-- Scheduling for concurrent computations.+module Test.DejaFu.Schedule+  ( -- * Scheduling+    Scheduler++  , Decision(..)+  , tidOf+  , decisionOf++  , NonEmpty(..)++  -- ** Preemptive+  , randomSched+  , roundRobinSched++  -- ** Non-preemptive+  , randomSchedNP+  , roundRobinSchedNP++  -- * Utilities+  , makeNonPreemptive+  ) where++import Data.List.NonEmpty (NonEmpty(..), toList)+import System.Random (RandomGen, randomR)++import Test.DejaFu.Common++-- | A @Scheduler@ drives the execution of a concurrent program. The+-- parameters it takes are:+--+-- 1. The trace so far.+--+-- 2. The last thread executed (if this is the first invocation, this+--    is @Nothing@).+--+-- 3. The runnable threads at this point.+--+-- 4. The state.+--+-- It returns a thread to execute, or @Nothing@ if execution should+-- abort here, and also a new state.+type Scheduler state+  = [(Decision, ThreadAction)]+  -> Maybe (ThreadId, ThreadAction)+  -> NonEmpty (ThreadId, Lookahead)+  -> state+  -> (Maybe ThreadId, state)++-------------------------------------------------------------------------------+-- Scheduling decisions++-- | Get the resultant thread identifier of a 'Decision', with a default case+-- for 'Continue'.+tidOf :: ThreadId -> Decision -> ThreadId+tidOf _ (Start t)    = t+tidOf _ (SwitchTo t) = t+tidOf tid _          = tid++-- | Get the 'Decision' that would have resulted in this thread identifier,+-- given a prior thread (if any) and list of runnable threads.+decisionOf :: Foldable f+  => Maybe ThreadId+  -- ^ The prior thread.+  -> f ThreadId+  -- ^ The runnable threads.+  -> ThreadId+  -- ^ The current thread.+  -> Decision+decisionOf Nothing _ chosen = Start chosen+decisionOf (Just prior) runnable chosen+  | prior == chosen = Continue+  | prior `elem` runnable = SwitchTo chosen+  | otherwise = Start chosen++-------------------------------------------------------------------------------+-- Preemptive++-- | A simple random scheduler which, at every step, picks a random+-- thread to run.+randomSched :: RandomGen g => Scheduler g+randomSched _ _ threads g = (Just $ threads' !! choice, g') where+  (choice, g') = randomR (0, length threads' - 1) g+  threads' = map fst $ toList threads++-- | A round-robin scheduler which, at every step, schedules the+-- thread with the next 'ThreadId'.+roundRobinSched :: Scheduler ()+roundRobinSched _ Nothing ((tid,_):|_) _ = (Just tid, ())+roundRobinSched _ (Just (prior, _)) threads _+  | prior >= maximum threads' = (Just $ minimum threads', ())+  | otherwise = (Just . minimum $ filter (>prior) threads', ())++  where+    threads' = map fst $ toList threads++-------------------------------------------------------------------------------+-- Non-preemptive++-- | A random scheduler which doesn't preempt the running+-- thread. That is, if the last thread scheduled is still runnable,+-- run that, otherwise schedule randomly.+randomSchedNP :: RandomGen g => Scheduler g+randomSchedNP = makeNonPreemptive randomSched++-- | A round-robin scheduler which doesn't preempt the running+-- thread.+roundRobinSchedNP :: Scheduler ()+roundRobinSchedNP = makeNonPreemptive roundRobinSched++-------------------------------------------------------------------------------+-- Utilities++-- | Turn a potentially preemptive scheduler into a non-preemptive+-- one.+makeNonPreemptive :: Scheduler s -> Scheduler s+makeNonPreemptive sched = newsched where+  newsched trc p@(Just (prior, _)) threads s+    | prior `elem` map fst (toList threads) = (Just prior, s)+    | otherwise = sched trc p threads s+  newsched trc Nothing threads s = sched trc Nothing threads s

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             0.4.0.0+version:             0.5.0.0 synopsis:            Systematic testing for Haskell concurrency.  description:@@ -74,12 +74,13 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-0.4.0.0+  tag:      dejafu-0.5.0.0  library   exposed-modules:     Test.DejaFu                      , Test.DejaFu.Conc                      , Test.DejaFu.Common+                     , Test.DejaFu.Schedule                      , Test.DejaFu.SCT                      , Test.DejaFu.STM @@ -87,18 +88,18 @@                      , Test.DejaFu.Conc.Internal.Common                      , Test.DejaFu.Conc.Internal.Memory                      , Test.DejaFu.Conc.Internal.Threading+                     , Test.DejaFu.SCT.Internal                      , Test.DejaFu.STM.Internal    -- other-modules:          -- other-extensions:       build-depends:       base              >=4.8  && <5-                     , concurrency       >=1.0  && <1.1+                     , concurrency       ==1.1.0.*                      , containers        >=0.5  && <0.6-                     , deepseq           >=1.3  && <1.5-                     , dpor              >=0.1  && <0.3                      , exceptions        >=0.7  && <0.9                      , monad-loops       >=0.4  && <0.5                      , mtl               >=2.2  && <2.3+                     , random            >=1.0  && <1.2                      , ref-fd            >=0.4  && <0.5                      , semigroups        >=0.16 && <0.19                      , transformers      >=0.4  && <0.6