Treat daemon threads specially.

dporSched now schedules all daemon threads if any of the initial
decisions willl terminate the computation. Closes #40.

dejafu/Test/DejaFu/SCT.hs

@@ -317,6 +317,10 @@ sctBoundedM memtype bf backtrack run =
        updateCRState
        (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

dpor/Test/DPOR.hs

@@ -104,6 +104,7 @@ module Test.DPOR
 
 import Control.DeepSeq (NFData)
 import Data.List (nub)
+import Data.List.NonEmpty (NonEmpty)
 import qualified Data.Map.Strict as M
 
 import Test.DPOR.Internal
@@ -129,6 +130,14 @@ import Test.DPOR.Schedule
 -- the most specific and (2) will be more pessimistic (due to,
 -- typically, less information being available when merely looking
 -- ahead).
+--
+-- The daemon-termination predicate returns @True@ if the action being
+-- looked at will cause the entire computation to terminate,
+-- regardless of the other runnable threads (which are passed in the
+-- 'NonEmpty' list). Such actions will then be put off for as long as
+-- possible. This allows supporting concurrency models with daemon
+-- threads without doing something as drastic as imposing a dependency
+-- between the program-terminating action and /everything/ else.
 dpor :: ( Ord    tid
        , NFData tid
        , NFData action
@@ -148,6 +157,8 @@ dpor :: ( Ord    tid
   -- ^ The dependency (1) function.
   -> (s -> (tid, action) -> (tid, lookahead) -> Bool)
   -- ^ The dependency (2) function.
+  -> (s -> (tid, lookahead) -> NonEmpty tid -> Bool)
+  -- ^ The daemon-termination predicate.
   -> tid
   -- ^ The initial thread.
   -> (tid -> Bool)
@@ -173,6 +184,7 @@ dpor didYield
      ststep
      dependency1
      dependency2
+     killsDaemons
      initialTid
      predicate
      inBound
@@ -203,7 +215,7 @@ dpor didYield
     nextPrefix = findSchedulePrefix predicate (const (0, ()))
 
     -- The DPOR scheduler.
-    scheduler = dporSched didYield willYield dependency1 ststep inBound
+    scheduler = dporSched didYield willYield dependency1 killsDaemons ststep inBound
 
     -- Find the new backtracking steps.
     findBacktracks = findBacktrackSteps stinit ststep dependency2 backtrack .
@@ -231,6 +243,8 @@ simpleDPOR :: ( Ord    tid
   -- ^ The dependency (1) function.
   -> ((tid, action) -> (tid, lookahead) -> Bool)
   -- ^ The dependency (2) function.
+  -> ((tid, lookahead) -> NonEmpty tid -> Bool)
+  -- ^ The daemon-termination predicate.
   -> tid
   -- ^ The initial thread.
   -> BoundFunc tid action lookahead
@@ -249,6 +263,7 @@ simpleDPOR didYield
            willYield
            dependency1
            dependency2
+           killsDaemons
            initialTid
            inBound
            backtrack
@@ -258,6 +273,7 @@ simpleDPOR didYield
          (\_ _ -> ())
          (const dependency1)
          (const dependency2)
+         (const killsDaemons)
          initialTid
          (const True)
          inBound

dpor/Test/DPOR/Internal.hs

@@ -468,13 +468,15 @@ dporSched :: (Ord tid, NFData tid, NFData action, NFData lookahead, NFData s)
   -- ^ Determine if a thread will yield.
   -> (s -> (tid, action) -> (tid, action) -> Bool)
   -- ^ Dependency function.
+  -> (s -> (tid, lookahead) -> NonEmpty tid -> Bool)
+  -- ^ Daemon-termination predicate.
   -> (s -> (tid, action) -> s)
   -- ^ Dependency function's state step function.
   -> BoundFunc tid action lookahead
   -- ^ Bound function: returns true if that schedule prefix terminated
   -- with the lookahead decision fits within the bound.
   -> DPORScheduler tid action lookahead s
-dporSched didYield willYield dependency ststep inBound trc prior threads s = force schedule where
+dporSched didYield willYield dependency killsDaemons ststep inBound trc prior threads s = force schedule where
   -- Pick a thread to run.
   schedule = case schedPrefix s of
     -- If there is a decision available, make it
@@ -498,33 +500,44 @@ dporSched didYield willYield dependency ststep inBound trc prior threads s = for
   -- The next scheduler state
   nextState rest = s
     { schedBPoints  = schedBPoints s |> (threads, rest)
-    , schedDepState = let ds = schedDepState s in maybe ds (ststep ds) prior
+    , schedDepState = nextDepState
     }
+  nextDepState = let ds = schedDepState s in maybe ds (ststep ds) prior
 
   -- Pick a new thread to run, which does not exceed the bound. Choose
   -- the current thread if available and it hasn't just yielded,
   -- otherwise add all runnable threads.
-  initialise = restrictToBound . yieldsToEnd $ case prior of
+  initialise = restrictToBound . tryDaemons . yieldsToEnd $ case prior of
     Just (tid, act)
-      | didYield act -> map fst (toList threads)
-      | any (\(t, _) -> t == tid) threads -> [tid]
-    _ -> map fst (toList threads)
+      | 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.
+  tryDaemons ts
+    | any doesKill ts = filter (not . doesKill) tids' ++ filter doesKill ts
+    | otherwise       = ts
+  doesKill t = killsDaemons nextDepState (t, action t) tids
 
   -- Restrict the possible decisions to those in the bound.
-  restrictToBound = fst . partition (\t -> inBound trc (decision t, action t))
+  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 $ map fst threads')
+  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
 
 -------------------------------------------------------------------------------
 -- * Utilities

dpor/Test/DPOR/Random.hs

@@ -23,6 +23,7 @@ module Test.DPOR.Random
   ) where
 
 import Control.DeepSeq (NFData)
+import Data.List.NonEmpty (NonEmpty)
 import Data.Maybe (fromMaybe)
 import System.Random (RandomGen, randomR)
 
@@ -65,6 +66,8 @@ randomDPOR :: ( Ord       tid
   -- ^ The dependency (1) function.
   -> (s -> (tid, action) -> (tid, lookahead) -> Bool)
   -- ^ The dependency (2) function.
+  -> (s -> (tid, lookahead) -> NonEmpty tid -> Bool)
+  -- ^ The daemon-termination predicate.
   -> tid
   -- ^ The initial thread.
   -> (tid -> Bool)
@@ -96,6 +99,7 @@ randomDPOR didYield
            ststep
            dependency1
            dependency2
+           killsDaemons
            initialTid
            predicate
            inBound
@@ -131,7 +135,7 @@ randomDPOR didYield
     nextPrefix = findSchedulePrefix predicate . gen
 
     -- The DPOR scheduler.
-    scheduler = dporSched didYield willYield dependency1 ststep inBound
+    scheduler = dporSched didYield willYield dependency1 killsDaemons ststep inBound
 
     -- Find the new backtracking steps.
     findBacktracks = findBacktrackSteps stinit ststep dependency2 backtrack .
@@ -183,6 +187,7 @@ boundedRandom didYield willYield initialTid inBoundm
                ststep
                dependency1
                dependency2
+               killsDaemons
                initialTid
                predicate
                inBound
@@ -193,6 +198,7 @@ boundedRandom didYield willYield initialTid inBoundm
     ststep _ _ = ()
     dependency1 _ _ _ = True
     dependency2 _ _ _ = True
+    killsDaemons _ _ _ = True
     predicate _ = True
     inBound = fromMaybe trueBound inBoundm
     backtrack = backtrackAt (const False) False