Start moving generic DPOR to separate module

dejafu/Test/DejaFu/DPOR.hs

@@ -0,0 +1,61 @@
+-- | Dynamic partial-order reduction.
+module Test.DejaFu.DPOR where
+
+import Control.DeepSeq (NFData(..))
+import Data.List (foldl')
+
+-- | 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 thread_id =
+    Start thread_id
+  -- ^ 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 thread_id
+  -- ^ Pre-empt the running thread, and switch to another.
+  deriving (Eq, Show)
+
+instance NFData thread_id => NFData (Decision thread_id) where
+  rnf (Start    tid) = rnf tid
+  rnf (SwitchTo tid) = rnf tid
+  rnf d = d `seq` ()
+
+-- | Get the resultant thread identifier of a 'Decision', with a default case
+-- for 'Continue'.
+tidOf ::
+    t
+  -- ^ The @Continue@ case.
+  -> Decision t
+  -- ^ The decision.
+  -> t
+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 :: (Eq thread_id, Foldable f)
+  => Maybe thread_id
+  -- ^ The prior thread.
+  -> f thread_id
+  -- ^ The runnable threads.
+  -> thread_id
+  -- ^ The current thread.
+  -> Decision thread_id
+decisionOf Nothing _ chosen = Start chosen
+decisionOf (Just prior) runnable chosen
+  | prior == chosen = Continue
+  | prior `elem` runnable = SwitchTo chosen
+  | otherwise = Start chosen
+
+-- | Get the tid of the currently active thread after executing a
+-- series of decisions. The list MUST begin with a 'Start', if it
+-- doesn't an error will be thrown.
+activeTid ::
+    [Decision thread_id]
+  -- ^ The sequence of decisions that have been made.
+  -> thread_id
+activeTid (Start tid:ds) = foldl' tidOf tid ds
+activeTid _ = error "activeTid: first decision MUST be a 'Start'."

dejafu/Test/DejaFu/Deterministic/Internal.hs

@@ -62,6 +62,7 @@ import Data.Functor (void)
 import Data.List (sort)
 import Data.List.Extra
 import Data.Maybe (fromJust, isJust, isNothing, listToMaybe)
+import Test.DejaFu.DPOR (Decision(..))
 import Test.DejaFu.STM (Result(..))
 import Test.DejaFu.Internal
 import Test.DejaFu.Deterministic.Internal.Common

dejafu/Test/DejaFu/Deterministic/Internal/Common.hs

@@ -12,6 +12,7 @@ import Data.Map.Strict (Map)
 import Data.Maybe (mapMaybe)
 import Data.List (sort, nub, intercalate)
 import Data.List.Extra
+import Test.DejaFu.DPOR (Decision(..))
 import Test.DejaFu.Internal
 
 {-# ANN module ("HLint: ignore Use record patterns" :: String) #-}
@@ -282,17 +283,17 @@ initialIdSource = Id 0 0 0 0 [] [] [] []
 -- attempts to (a) schedule a blocked thread, or (b) schedule a
 -- nonexistent thread. In either of those cases, the computation will
 -- be halted.
-type Scheduler s = s -> [(Decision, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, NonEmpty Lookahead) -> (Maybe ThreadId, s)
+type Scheduler s = s -> [(Decision ThreadId, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, NonEmpty Lookahead) -> (Maybe ThreadId, s)
 
 -- | One of the outputs of the runner is a @Trace@, which is a log of
 -- decisions made, alternative decisions (including what action would
 -- have been performed had that decision been taken), and the action a
 -- thread took in its step.
-type Trace = [(Decision, [(Decision, Lookahead)], ThreadAction)]
+type Trace = [(Decision ThreadId, [(Decision ThreadId, Lookahead)], ThreadAction)]
 
 -- | Like a 'Trace', but gives more lookahead (where possible) for
 -- alternative decisions.
-type Trace' = [(Decision, [(Decision, NonEmpty Lookahead)], ThreadAction)]
+type Trace' = [(Decision ThreadId, [(Decision ThreadId, NonEmpty Lookahead)], ThreadAction)]
 
 -- | Throw away information from a 'Trace'' to get just a 'Trace'.
 toTrace :: Trace' -> Trace
@@ -317,24 +318,6 @@ showTrace trc = intercalate "\n" $ trace "" 0 trc : (map ("  "++) . sort . nub $
   toKey (Start (ThreadId (Just name) i), _, _) = Just $ show i ++ ": " ++ name
   toKey _ = Nothing
 
--- | 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)
-
-instance NFData Decision where
-  rnf (Start    tid) = rnf tid
-  rnf (SwitchTo tid) = rnf tid
-  rnf d = d `seq` ()
-
 -- | All the actions that a thread can perform.
 data ThreadAction =
     Fork ThreadId

dejafu/Test/DejaFu/SCT.hs

@@ -92,9 +92,6 @@ module Test.DejaFu.SCT
   , (&+&)
   , trueBound
   , backtrackAt
-  , tidOf
-  , decisionOf
-  , activeTid
   , preEmpCount
   , preEmpCount'
   , yieldCount
@@ -108,8 +105,9 @@ import Data.List (nub, partition)
 import Data.Sequence (Seq, (|>))
 import Data.Map (Map)
 import Data.Maybe (isNothing, isJust, fromJust)
-import Test.DejaFu.Deterministic
+import Test.DejaFu.Deterministic hiding (Decision(..))
 import Test.DejaFu.Deterministic.Internal (initialThread, willRelease)
+import Test.DejaFu.DPOR (Decision(..), decisionOf)
 import Test.DejaFu.SCT.Internal
 
 import qualified Data.Map.Strict as M
@@ -119,7 +117,7 @@ import qualified Data.Set as S
 -- | 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
+type BoundFunc = [(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Bool
 
 -- | Combine two bounds into a larger bound, where both must be
 -- satisfied.
@@ -251,7 +249,7 @@ pbBound :: PreemptionBound -> BoundFunc
 pbBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb
 
 -- | Count the number of pre-emptions in a schedule prefix.
-preEmpCount :: [(Decision, ThreadAction)] -> (Decision, a) -> Int
+preEmpCount :: [(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, a) -> Int
 preEmpCount ts (d, _) = go Nothing ts where
   go p ((d', a):rest) = preEmpC p d' + go (Just a) rest
   go p [] = preEmpC p d
@@ -315,7 +313,7 @@ fBound :: FairBound -> BoundFunc
 fBound (FairBound fb) ts dl = maxYieldCountDiff ts dl <= fb
 
 -- | Count the number of yields by a thread in a schedule prefix.
-yieldCount :: ThreadId -> [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int
+yieldCount :: ThreadId -> [(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Int
 yieldCount tid ts (_, l) = go initialThread ts where
   go t ((Start    t', Yield):rest) = (if t == tid then 1 else 0) + go t' rest
   go t ((SwitchTo t', Yield):rest) = (if t == tid then 1 else 0) + go t' rest
@@ -323,12 +321,11 @@ yieldCount tid ts (_, l) = go initialThread ts where
   go _ ((Start    t', _):rest) = go t' rest
   go _ ((SwitchTo t', _):rest) = go t' rest
   go t ((Continue,    _):rest) = go t  rest
-  go t (_:rest) = go t rest
   go t [] = case l of WillYield | t == tid -> 1; _ -> 0
 
 -- | Get the maximum difference between the yield counts of all
 -- threads in this schedule prefix.
-maxYieldCountDiff :: [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int
+maxYieldCountDiff :: [(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Int
 maxYieldCountDiff ts dl = maximum yieldCountDiffs where
   yieldCounts = [yieldCount tid ts dl | tid <- nub $ allTids ts]
   yieldCountDiffs = [y1 - y2 | y1 <- yieldCounts, y2 <- yieldCounts]
@@ -414,7 +411,7 @@ sctBoundedIO memtype bf backtrack c = sctBoundedM memtype bf backtrack run where
 -- | Generic SCT runner.
 sctBoundedM :: (Functor m, Monad m)
   => MemType
-  -> ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool)
+  -> ([(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Bool)
   -> ([BacktrackStep] -> Int -> ThreadId -> [BacktrackStep])
   -> (MemType -> Scheduler SchedState -> SchedState -> m (Either Failure a, SchedState, Trace'))
   -- ^ Monadic runner, with computation fixed.
@@ -465,7 +462,7 @@ initialSchedState sleep prefix = SchedState
 -- including the runnable threads, and the alternative choices allowed
 -- by the bound-specific initialise function.
 bporSched :: MemType
-  -> ([(Decision, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> [ThreadId])
+  -> ([(Decision ThreadId, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> [ThreadId])
   -> Scheduler SchedState
 bporSched memtype initials = force $ \s trc prior threads -> case _sprefix s of
   -- If there is a decision available, make it
@@ -493,7 +490,7 @@ bporSched memtype initials = force $ \s trc prior threads -> case _sprefix s of
 -- the current thread if available and it hasn't just yielded,
 -- otherwise add all runnable threads.
 initialise :: BoundFunc
-  -> [(Decision, ThreadAction)]
+  -> [(Decision ThreadId, ThreadAction)]
   -> Maybe (ThreadId, ThreadAction)
   -> NonEmpty (ThreadId, Lookahead)
   -> [ThreadId]

dejafu/Test/DejaFu/SCT/Internal.hs

@@ -8,8 +8,9 @@ import Data.Maybe (mapMaybe, isJust, fromJust, listToMaybe)
 import Data.Ord (Down(..), comparing)
 import Data.Sequence (Seq, ViewL(..))
 import Data.Set (Set)
-import Test.DejaFu.Deterministic.Internal
+import Test.DejaFu.Deterministic.Internal hiding (Decision(..))
 import Test.DejaFu.Deterministic.Schedule
+import Test.DejaFu.DPOR (Decision(..), decisionOf, tidOf)
 
 import qualified Data.Map.Strict as M
 import qualified Data.Sequence as Sq
@@ -23,7 +24,7 @@ import qualified Data.Set as S
 data BacktrackStep = BacktrackStep
   { _threadid  :: ThreadId
   -- ^ The thread running at this step
-  , _decision  :: (Decision, ThreadAction)
+  , _decision  :: (Decision ThreadId, ThreadAction)
   -- ^ What happened at this step.
   , _runnable  :: Map ThreadId Lookahead
   -- ^ The threads runnable at this step
@@ -235,7 +236,7 @@ grow dependency conservative = grow' initialCRState initialThread where
 
 -- | Add new backtracking points, if they have not already been
 -- visited, fit into the bound, and aren't in the sleep set.
-todo :: ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool) -> [BacktrackStep] -> BPOR -> BPOR
+todo :: ([(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Bool) -> [BacktrackStep] -> BPOR -> BPOR
 todo bv = go Nothing [] where
   go priorTid pref (b:bs) bpor =
     let bpor' = backtrack priorTid pref b bpor
@@ -277,26 +278,6 @@ pruneCommits bpor
 
 -- * Utilities
 
--- | Get the resultant 'ThreadId' 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 'ThreadId',
--- given a prior 'ThreadId' (if any) and list of runnable threads.
-decisionOf :: Maybe ThreadId -> Set ThreadId -> ThreadId -> Decision
-decisionOf prior runnable chosen
-  | prior == Just chosen = Continue
-  | prior `S.member` S.map Just runnable = SwitchTo chosen
-  | otherwise = Start chosen
-
--- | Get the tid of the currently active thread after executing a
--- series of decisions. The list MUST begin with a 'Start'.
-activeTid :: [Decision] -> ThreadId
-activeTid = foldl' tidOf initialThread
-
 -- | Check if an action is dependent on another.
 dependent :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool
 dependent _ _ (_, Lift) (_, Lift) = True

dejafu/dejafu.cabal

@@ -98,6 +98,7 @@ library
                      , Test.DejaFu
                      , Test.DejaFu.Deterministic
                      , Test.DejaFu.Deterministic.Schedule
+                     , Test.DejaFu.DPOR
                      , Test.DejaFu.SCT
                      , Test.DejaFu.STM