Implement a weighted random scheduler.

dejafu/Test/DejaFu/SCT.hs

@@ -42,8 +42,6 @@ module Test.DejaFu.SCT
 
   , sctBound
 
-  -- * Individual Bounds
-
   -- ** Pre-emption Bounding
 
   -- | BPOR using pre-emption bounding. This adds conservative
@@ -77,6 +75,17 @@ module Test.DejaFu.SCT
   , LengthBound(..)
   , defaultLengthBound
   , sctLengthBound
+
+  -- * Random Scheduling
+
+  -- | 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.Monad.Ref (MonadRef)
@@ -84,6 +93,7 @@ import Data.List (foldl')
 import qualified Data.Map.Strict as M
 import Data.Maybe (isJust, fromJust)
 import qualified Data.Set as S
+import System.Random (RandomGen)
 
 import Test.DejaFu.Common
 import Test.DejaFu.Conc
@@ -254,7 +264,7 @@ lBacktrack :: BacktrackFunc
 lBacktrack = backtrackAt (\_ _ -> False)
 
 -------------------------------------------------------------------------------
--- DPOR
+-- Systematic concurrency testing
 
 -- | SCT via BPOR.
 --
@@ -282,7 +292,7 @@ sctBound memtype cb conc = go initialState where
     Just (prefix, conservative, sleep, ()) -> do
       (res, s, trace) <- runConcurrent scheduler
                                        memtype
-                                       (initialSchedState sleep prefix)
+                                       (initialDPORSchedState sleep prefix)
                                        conc
 
       let bpoints = findBacktracks (schedBoundKill s) (schedBPoints s) trace
@@ -309,6 +319,32 @@ sctBound memtype cb conc = go initialState where
   -- 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
 

dejafu/Test/DejaFu/SCT/Internal.hs

@@ -24,6 +24,7 @@ import Data.Set (Set)
 import qualified Data.Set as S
 import Data.Sequence (Seq, ViewL(..), (|>))
 import qualified Data.Sequence as Sq
+import System.Random (RandomGen, randomR)
 
 import Test.DejaFu.Common
 import Test.DejaFu.Schedule (Decision(..), Scheduler, decisionOf, tidOf)
@@ -304,7 +305,7 @@ incorporateBacktrackSteps bv = go Nothing [] where
 -- * DPOR scheduler
 
 -- | The scheduler state
-data SchedState = SchedState
+data DPORSchedState = DPORSchedState
   { schedSleep     :: Map ThreadId ThreadAction
   -- ^ The sleep set: decisions not to make until something dependent
   -- with them happens.
@@ -326,13 +327,13 @@ data SchedState = SchedState
   -- remove decisions from the sleep set.
   } deriving Show
 
--- | Initial scheduler state for a given prefix
-initialSchedState :: Map ThreadId ThreadAction
+-- | Initial DPOR scheduler state for a given prefix
+initialDPORSchedState :: Map ThreadId ThreadAction
   -- ^ The initial sleep set.
   -> [ThreadId]
   -- ^ The schedule prefix.
-  -> SchedState
-initialSchedState sleep prefix = SchedState
+  -> DPORSchedState
+initialDPORSchedState sleep prefix = DPORSchedState
   { schedSleep     = sleep
   , schedPrefix    = prefix
   , schedBPoints   = Sq.empty
@@ -419,7 +420,7 @@ dporSched
   -> BoundFunc
   -- ^ Bound function: returns true if that schedule prefix terminated
   -- with the lookahead decision fits within the bound.
-  -> Scheduler SchedState
+  -> Scheduler DPORSchedState
 dporSched dependency inBound trc prior threads s = schedule where
   -- Pick a thread to run.
   schedule = case schedPrefix s of
@@ -503,6 +504,44 @@ dporSched dependency inBound trc prior threads s = schedule where
   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