Add a pre-emption bounding runner, and use it for tests

Control/Monad/Conc/Fixed/Internal.hs

@@ -94,7 +94,9 @@ data ThreadAction =
   -- ^ Try to take from a 'CVar', possibly waking up some threads.
   | Lift
   -- ^ Lift an action from the underlying monad.
-  deriving (Eq, Show)
+  | Stop
+  -- ^ Cease execution and terminate.
+  deriving (Eq, Ord, Show)
 
 -- | Run a concurrent computation with a given 'Scheduler' and initial
 -- state, returning `Just result` if it terminates, and `Nothing` if a
@@ -144,7 +146,7 @@ runThreads fixed sofar prior sched s threads ref
   | isNonexistant = writeRef fixed ref Nothing >> return (s, sofar)
   | otherwise = do
     (threads', act) <- stepThread (fst $ fromJust thread) fixed chosen threads
-    let sofar' = maybe sofar (\a -> (chosen, a) : sofar) act
+    let sofar' = (chosen, act) : sofar
     runThreads fixed sofar' chosen sched s' threads' ref
 
   where
@@ -160,7 +162,7 @@ runThreads fixed sofar prior sched s threads ref
 -- 'Action'.
 stepThread :: (Monad (c t), Monad n)
            => Action n r
-           -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, Maybe ThreadAction)
+           -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction)
 stepThread (AFork    a b)     = stepFork    a b
 stepThread (APut     ref a c) = stepPut     ref a c
 stepThread (ATryPut  ref a c) = stepTryPut  ref a c
@@ -168,99 +170,99 @@ stepThread (AGet     ref c)   = stepGet     ref c
 stepThread (ATake    ref c)   = stepTake    ref c
 stepThread (ATryTake ref c)   = stepTryTake ref c
 stepThread (ALift    na)      = stepLift    na
-stepThread AStop             = stepStop
+stepThread  AStop             = stepStop
 
 -- | Start a new thread, assigning it a unique 'ThreadId'
 stepFork :: (Monad (c t), Monad n)
          => Action n r -> Action n r
-         -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, Maybe ThreadAction)
+         -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction)
 stepFork a b _ i threads =
   let (threads', newid) = launch a threads
-  in return (goto b i threads', Just $ Fork newid)
+  in return (goto b i threads', Fork newid)
 
 -- | Put a value into a @CVar@, blocking the thread until it's empty.
 stepPut :: (Monad (c t), Monad n)
         => R r a -> a -> Action n r
-        -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, Maybe ThreadAction)
+        -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction)
 stepPut ref a c fixed i threads = do
   (val, blocks) <- readRef fixed ref
   case val of
     Just _  -> do
       threads' <- block fixed ref WaitEmpty i threads
-      return (threads', Just BlockedPut)
+      return (threads', BlockedPut)
     Nothing -> do
       writeRef fixed ref (Just a, blocks)
       (threads', woken) <- wake fixed ref WaitFull threads
-      return (goto c i threads', Just $ Put woken)
+      return (goto c i threads', Put woken)
 
 -- | Try to put a value into a @CVar@, without blocking.
 stepTryPut :: (Monad (c t), Monad n)
            => R r a -> a -> (Bool -> Action n r)
-           -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, Maybe ThreadAction)
+           -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction)
 stepTryPut ref a c fixed i threads = do
   (val, blocks) <- readRef fixed ref
   case val of
-    Just _  -> return (goto (c False) i threads, Just $ TryPut False [])
+    Just _  -> return (goto (c False) i threads, TryPut False [])
     Nothing -> do
       writeRef fixed ref (Just a, blocks)
       (threads', woken) <- wake fixed ref WaitFull threads
-      return (goto (c True) i threads', Just $ TryPut True woken)
+      return (goto (c True) i threads', TryPut True woken)
 
 -- | Get the value from a @CVar@, without emptying, blocking the
 -- thread until it's full.
 stepGet :: (Monad (c t), Monad n)
         => R r a -> (a -> Action n r)
-        -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, Maybe ThreadAction)
+        -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction)
 stepGet ref c fixed i threads = do
   (val, _) <- readRef fixed ref
   case val of
-    Just val' -> return (goto (c val') i threads, Just Read)
+    Just val' -> return (goto (c val') i threads, Read)
     Nothing   -> do
       threads' <- block fixed ref WaitFull i threads
-      return (threads', Just BlockedRead)
+      return (threads', BlockedRead)
 
 -- | Take the value from a @CVar@, blocking the thread until it's
 -- full.
 stepTake :: (Monad (c t), Monad n)
          => R r a -> (a -> Action n r)
-         -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, Maybe ThreadAction)
+         -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction)
 stepTake ref c fixed i threads = do
   (val, blocks) <- readRef fixed ref
   case val of
     Just val' -> do
       writeRef fixed ref (Nothing, blocks)
       (threads', woken) <- wake fixed ref WaitEmpty threads
-      return (goto (c val') i threads', Just $ Take woken)
+      return (goto (c val') i threads', Take woken)
     Nothing   -> do
       threads' <- block fixed ref WaitFull i threads
-      return (threads', Just BlockedTake)
+      return (threads', BlockedTake)
 
 -- | Try to take the value from a @CVar@, without blocking.
 stepTryTake :: (Monad (c t), Monad n)
             => R r a -> (Maybe a -> Action n r)
-            -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, Maybe ThreadAction)
+            -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction)
 stepTryTake ref c fixed i threads = do
   (val, blocks) <- readRef fixed ref
   case val of
     Just _ -> do
       writeRef fixed ref (Nothing, blocks)
       (threads', woken) <- wake fixed ref WaitEmpty threads
-      return (goto (c val) i threads', Just $ TryTake True woken)
+      return (goto (c val) i threads', TryTake True woken)
-    Nothing   -> return (goto (c Nothing) i threads, Just $ TryTake False [])
+    Nothing   -> return (goto (c Nothing) i threads, TryTake False [])
 
 -- | Lift an action from the underlying monad into the @Conc@
 -- computation.
 stepLift :: (Monad (c t), Monad n)
          => n (Action n r)
-         -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, Maybe ThreadAction)
+         -> Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction)
 stepLift na _ i threads = do
   a <- na
-  return (goto a i threads, Just Lift)
+  return (goto a i threads, Lift)
 
 -- | Kill the current thread.
 stepStop :: (Monad (c t), Monad n)
-         => Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, Maybe ThreadAction)
+         => Fixed c n r t -> ThreadId -> Threads n r -> n (Threads n r, ThreadAction)
-stepStop _ i threads = return (kill i threads, Nothing)
+stepStop _ i threads = return (kill i threads, Stop)
 
 -- * Manipulating threads
 

Control/Monad/Conc/SCT.hs

@@ -32,29 +32,41 @@
 -- will have `b` and be waiting on `a`.
 
 module Control.Monad.Conc.SCT
- ( -- *Systematic Concurrency Testing
+ ( -- * Types
    SCTScheduler
  , SchedTrace
  , SCTTrace
  , Decision(..)
+
+-- * SCT Runners
  , runSCT
  , runSCTIO
  , runSCT'
  , runSCTIO'
 
- -- * Schedulers
+ -- * Random Schedulers
  , sctRandom
  , sctRandomNP
 
+ -- * Pre-emption Bounding
+ , sctPreBound
+ , sctPreBoundIO
+ , preEmpCount
+
  -- * Utilities
  , toSCT
  , showTrace
+ , ordNub
+ , (~=)
  ) where
 
 import Control.Monad.Conc.Fixed
 import System.Random (RandomGen)
 
 import qualified Control.Monad.Conc.Fixed.IO as CIO
+import qualified Data.Set as Set
+
+-- * Types
 
 -- | An @SCTScheduler@ is like a regular 'Scheduler', except it builds
 -- a trace of scheduling decisions made.
@@ -79,7 +91,9 @@ data Decision =
   -- ^ Continue running the last thread for another step.
   | SwitchTo ThreadId
   -- ^ Pre-empt the running thread, and switch to another.
-  deriving (Eq, Show)
+  deriving (Eq, Ord, Show)
+
+-- * SCT Runners
 
 -- | Run a concurrent program under a given scheduler a number of
 -- times, collecting the results and the scheduling that gave rise to
@@ -90,8 +104,8 @@ data Decision =
 -- internal state, or all the results will be identical.
 runSCT :: SCTScheduler s -> s -> Int -> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
 runSCT sched s n = runSCT' sched s n term step where
-  term (_, g) = g == 0
+  term _  g = g == 0
-  step (s, g) = (s, g - 1)
+  step s' g _ = (s', g - 1)
 
 -- | A varant of 'runSCT' for concurrent programs that do 'IO'.
 --
@@ -101,8 +115,8 @@ runSCT sched s n = runSCT' sched s n term step where
 -- function!
 runSCTIO :: SCTScheduler s -> s -> Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
 runSCTIO sched s n = runSCTIO' sched s n term step where
-  term (_, g) = g == 0
+  term _  g = g == 0
-  step (s, g) = (s, g - 1)
+  step s' g _ = (s', g - 1)
 
 -- | Run a concurrent program under a given scheduler, where the SCT
 -- runner itself maintains some internal state, and has a function to
@@ -114,17 +128,19 @@ runSCTIO sched s n = runSCTIO' sched s n term step where
 runSCT' :: SCTScheduler s -- ^ The scheduler
         -> s -- ^ The scheduler's initial satte
         -> g -- ^ The runner's initial state
-        -> ((s, g) -> Bool) -- ^ Termination decider
+        -> (s -> g -> Bool) -- ^ Termination decider
-        -> ((s, g) -> (s, g)) -- ^ State step function
+        -> (s -> g -> SCTTrace -> (s, g)) -- ^ State step function
         -> (forall t. Conc t a) -- ^ Conc program
         -> [(Maybe a, SCTTrace)]
 runSCT' sched s g term step c
-  | term (s, g) = []
+  | term s g = []
-  | otherwise = (res, scttrace strace ttrace) : rest where
+  | otherwise = (res, trace) : rest where
 
   (res, (s', strace), ttrace) = runConc' sched (s, [(Start 0, [])]) c
 
-  (s'', g') = step (s', g)
+  trace = scttrace strace ttrace
+
+  (s'', g') = step s' g trace
 
   rest = runSCT' sched s'' g' term step c
 
@@ -134,22 +150,20 @@ runSCT' sched s g term step c
 -- interleavings! Be very confident that nothing in a 'liftIO' can
 -- block on the action of another thread, or you risk deadlocking this
 -- function!
-runSCTIO' :: SCTScheduler s -> s -> g -> ((s, g) -> Bool) -> ((s, g) -> (s, g)) -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
+runSCTIO' :: SCTScheduler s -> s -> g -> (s -> g -> Bool) -> (s -> g -> SCTTrace -> (s, g)) -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
 runSCTIO' sched s g term step c
-  | term (s, g) = return []
+  | term s g = return []
   | otherwise = do
     (res, (s', strace), ttrace) <- CIO.runConc' sched (s, [(Start 0, [])]) c
 
-    let (s'', g') = step (s', g)
+    let trace = scttrace strace ttrace
+    let (s'', g') = step s' g trace
 
     rest <- runSCTIO' sched s'' g' term step c
 
-    return $ (res, scttrace strace ttrace) : rest
+    return $ (res, trace) : rest
 
--- | Zip a list of 'SchedTrace's and a 'Trace' together into an
+-- * Random Schedulers
--- 'SCTTrace'.
-scttrace :: SchedTrace -> Trace -> SCTTrace
-scttrace = zipWith $ \(d, alts) (_, act) -> (d, alts, act)
 
 -- | A simple pre-emptive random scheduler.
 sctRandom :: RandomGen g => SCTScheduler g
@@ -159,6 +173,119 @@ sctRandom = toSCT randomSched
 sctRandomNP :: RandomGen g => SCTScheduler g
 sctRandomNP = toSCT randomSchedNP
 
+-- * Pre-emption bounding
+
+data PreBoundState = P
+  { _pc :: Int
+  -- ^ Current pre-emption count.
+  , _next :: [[Decision]]
+  -- ^ Schedules to try in this pc.
+  , _done :: [SCTTrace]
+  -- ^ Schedules completed in this pc.
+  , _halt :: Bool
+  -- ^ Indicates more schedules couldn't be found, and to halt
+  -- immediately.
+  }
+
+-- | An SCT runner using a pre-emption bounding scheduler. Schedules
+-- will be explored systematically, starting with all
+-- pre-emption-count zero schedules, and gradually adding more
+-- pre-emptions.
+sctPreBound :: Int -- ^ The pre-emption bound. Anything < 0 will be
+                  -- interpreted as 0.
+            -> (forall t. Conc t a) -> [(Maybe a, SCTTrace)]
+sctPreBound pb = runSCT' pbSched s g (pbTerm pb') (pbStep pb') where
+  s = []
+  g = P { _pc = 0, _next = [], _done = [], _halt = False }
+  pb' = if pb < 0 then 0 else pb
+
+-- | Variant of 'sctPreBound' using 'IO'. See usual caveats about IO.
+sctPreBoundIO :: Int -> (forall t. CIO.Conc t a) -> IO [(Maybe a, SCTTrace)]
+sctPreBoundIO pb = runSCTIO' pbSched s g (pbTerm pb') (pbStep pb') where
+  s = []
+  g = P { _pc = 0, _next = [], _done = [], _halt = False }
+  pb' = if pb < 0 then 0 else pb
+
+-- | Pre-emption bounding scheduler, which uses a queue of scheduling
+-- decisions to drive the initial trace.
+pbSched :: SCTScheduler [Decision]
+pbSched = toSCT sched where
+  -- If we have a decision queued, make it.
+  sched (Start t:ds)    _ _ = (t, ds)
+  sched (Continue:ds)     t _ = (t, ds)
+  sched (SwitchTo t:ds) _ _ = (t, ds)
+
+  -- Otherwise just use a non-pre-emptive scheduler.
+  sched [] t1 ts@(t2:_)
+    | t1 `elem` ts = (t1, [])
+    | otherwise    = (t2, [])
+
+  -- Error, should never happen, so just deadlock it.
+  sched [] _ [] = (-1, [])
+
+-- | Pre-emption bounding termination function: terminates on attempt
+-- to start a PB above the limit.
+pbTerm :: Int -> a -> PreBoundState -> Bool
+pbTerm pb _ g = (_pc g == pb + 1) || _halt g
+
+-- | Pre-emption bounding state step function: computes remaining
+-- schedules to try and chooses one.
+pbStep :: Int -> a -> PreBoundState -> SCTTrace -> ([Decision], PreBoundState)
+pbStep pb _ g t = case _next g of
+  -- We have schedules remaining in this PB, so run the next
+  (x:xs) -> (tail x, g { _next = xs, _done = done' })
+
+  -- We have no schedules remaining, try to generate some more.
+  --
+  -- If there are no more schedules in this PB, and this isn't the
+  -- last PB, advance to the next.
+  --
+  -- If there are no schedules in the next PB, halt.
+  [] ->
+    let thisPB = [y | y <- concatMap others done', preEmpCount y == _pc g, not $ any (y ~=) done']
+        nextPB = ordNub [y | y <- concatMap next done', preEmpCount y == pc']
+    in case thisPB of
+         (x:xs) -> (tail x, g { _next = xs, _done = done' })
+         [] -> if _pc g == pb
+              then halt
+              else case nextPB of
+                     (x:xs) -> (tail x, g { _pc = pc', _next = xs, _done = [] })
+                     [] -> halt
+
+  where
+    halt  = ([], g { _halt = True })
+    done' = t : _done g
+    pc'   = _pc g + 1
+
+    -- | Return all modifications to this schedule which do not
+    -- introduce extra pre-emptions.
+    others ((Start i,    alts, _):ds) = [[a] | a <- alts] ++ [Start    i : o | o <- others ds]
+    others ((SwitchTo i, alts, _):ds) = [[a] | a <- alts] ++ [SwitchTo i : o | o <- others ds]
+    others ((d, _, _):ds) = [d : o | o <- others ds]
+    others [] = []
+
+    -- | Return all modifications to this schedule which do introduce
+    -- an extra pre-emption. Only introduce pre-emptions around CVar
+    -- actions.
+    next ((Continue, alts, Put _):ds)       = [[n] | n <- alts] ++ [Continue : n | n <- next ds]
+    next ((Continue, alts, BlockedPut):ds)  = [[n] | n <- alts] ++ [Continue : n | n <- next ds]
+    next ((Continue, alts, TryPut _ _):ds)  = [[n] | n <- alts] ++ [Continue : n | n <- next ds]
+    next ((Continue, alts, Read):ds)        = [[n] | n <- alts] ++ [Continue : n | n <- next ds]
+    next ((Continue, alts, BlockedRead):ds) = [[n] | n <- alts] ++ [Continue : n | n <- next ds]
+    next ((Continue, alts, Take _):ds)      = [[n] | n <- alts] ++ [Continue : n | n <- next ds]
+    next ((Continue, alts, BlockedTake):ds) = [[n] | n <- alts] ++ [Continue : n | n <- next ds]
+    next ((Continue, alts, TryTake _ _):ds) = [[n] | n <- alts] ++ [Continue : n | n <- next ds]
+    next ((d, _, _):ds) = [d : n | n <- next ds]
+    next [] = []
+
+-- | Check the pre-emption count of some scheduling decisions.
+preEmpCount :: [Decision] -> Int
+preEmpCount (SwitchTo _:ss) = 1 + preEmpCount ss
+preEmpCount (_:ss) = preEmpCount ss
+preEmpCount [] = 0
+
+-- * Utils
+
 -- | Convert a 'Scheduler' to an 'SCTScheduler' by recording the
 -- trace.
 toSCT :: Scheduler s -> SCTScheduler s
@@ -182,3 +309,22 @@ showTrace = trace "" 0 . map fst where
     trace prefix num []                = thread prefix num
 
     thread prefix num = prefix ++ replicate num '-'
+
+-- | Zip a list of 'SchedTrace's and a 'Trace' together into an
+-- 'SCTTrace'.
+scttrace :: SchedTrace -> Trace -> SCTTrace
+scttrace = zipWith $ \(d, alts) (_, act) -> (d, alts, act)
+
+-- | O(nlogn) nub, <https://github.com/nh2/haskell-ordnub>
+ordNub :: Ord a => [a] -> [a]
+ordNub = go Set.empty where
+  go _ [] = []
+  go s (x:xs)
+    | x `Set.member` s = go s xs
+    | otherwise = x : go (Set.insert x s) xs
+
+-- | Check if a list of decisions matches an initial portion of a trace.
+(~=) :: [Decision] -> SCTTrace -> Bool
+(d:ds) ~= ((t,_,_):ts) = d == t && ds ~= ts
+[] ~= _  = True
+_  ~= [] = False

Tests/Cases.hs

@@ -9,18 +9,16 @@ import Tests.Utils
 -- | List of all tests
 testCases :: [Test]
 testCases =
-  [ Test "Simple 2-Deadlock" $ testNot "No deadlocks found!" $ testDeadlockFree 100   simple2Deadlock
+  [ Test "Simple 2-Deadlock" $ testNot "No deadlocks found!" $ testDeadlockFree 1   simple2Deadlock
-  , Test "2 Philosophers"    $ testNot "No deadlocks found!" $ testDeadlockFree 100 $ philosophers 2
+  , Test "2 Philosophers"    $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 2
-  , Test "3 Philosophers"    $ testNot "No deadlocks found!" $ testDeadlockFree 100 $ philosophers 3
+  , Test "3 Philosophers"    $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 3
-  --Random scheduling isn't good enough for these, without increasing
+  , Test "4 Philosophers"    $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 4
-  --the runs.
+  , Test "5 Philosophers"    $ testNot "No deadlocks found!" $ testDeadlockFree 1 $ philosophers 5
-  --, Test "4 Philosophers"    $ testNot "No deadlocks found!" $ testDeadlockFree 100 $ philosophers 4
+  --, Test "100 Philosophers"  $ testNot "No deadlocks found!" $ testDeadlockFree 0 $ philosophers 100
-  --, Test "5 Philosophers"    $ testNot "No deadlocks found!" $ testDeadlockFree 100 $ philosophers 5
+  , Test "Threshold Value"   $ testNot "All values equal!"   $ testAlwaysSame   1   thresholdValue
-  --, Test "100 Philosophers"  $ testNot "No deadlocks found!" $ testDeadlockFree 100 $ philosophers 100
+  , Test "Forgotten Unlock"  $                                 testDeadlocks    1   forgottenUnlock
-  , Test "Threshold Value"   $ testNot "All values equal!"   $ testAlwaysSame   100   thresholdValue
+  , Test "Simple 2-Race"     $ testNot "All values equal!"   $ testAlwaysSame   1   simple2Race
-  , Test "Forgotten Unlock"  $                                 testDeadlocks    100   forgottenUnlock
+  , Test "Racey Stack"       $ testNot "All values equal!"   $ testAlwaysSame   1   raceyStack
-  , Test "Simple 2-Race"     $ testNot "All values equal!"   $ testAlwaysSame   100   simple2Race
-  , Test "Racey Stack"       $ testNot "All values equal!"   $ testAlwaysSame   100   raceyStack
   ]
 
 -- | Should deadlock on a minority of schedules.

Tests/Utils.hs

@@ -2,7 +2,7 @@
 module Tests.Utils where
 
 import Control.Monad.Conc.Fixed (Conc)
-import Control.Monad.Conc.SCT (runSCT, sctRandom)
+import Control.Monad.Conc.SCT (sctPreBound)
 import Data.List (group, sort)
 import Data.Maybe (isJust, isNothing)
 import System.Random (mkStdGen)
@@ -14,7 +14,7 @@ data Result = Pass | Fail String | Error String
 -- | Test that a predicate holds over the results of a concurrent
 -- computation.
 testPred :: ([Maybe a] -> Result) -> Int -> (forall t. Conc t a) -> Result
-testPred predicate num conc = predicate . map fst $ runSCT sctRandom (mkStdGen 0) num conc
+testPred predicate num conc = predicate . map fst $ sctPreBound num conc
 
 -- | Test that a concurrent computation is free of deadlocks.
 testDeadlockFree :: Int -> (forall t. Conc t a) -> Result