Record in SCT trace reasons for decisions.

In particular, this lets us distinguish between switching to a new
thread because the old was blocked, or switching to a new thread
because of a pre-emption.
This commit is contained in:
Michael Walker 2014-12-21 12:42:43 +00:00
parent 8b0f2763d3
commit 96eaf85095

View File

@ -34,8 +34,10 @@
module Control.Monad.Conc.SCT
( -- *Systematic Concurrency Testing
SCTScheduler
, Decision(..)
, runSCT
, sctRandom
, showTrace
) where
import Control.Monad.Conc.Fixed
@ -43,7 +45,20 @@ import System.Random (RandomGen, randomR)
-- | An @SCTScheduler@ is like a regular 'Scheduler', except it builds
-- a log of scheduling decisions made.
type SCTScheduler s = Scheduler (s, [ThreadId])
type SCTScheduler s = Scheduler (s, [Decision])
-- | 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
-- initial thread).
| Continue
-- ^ Continue running the last thread for another step.
| SwitchTo ThreadId
-- ^ Pre-empt the running thread, and switch to another.
deriving (Eq, Show)
-- | Run a concurrent program under a given scheduler a number of
-- times, collecting the results and the scheduling that gave rise to
@ -52,16 +67,30 @@ type SCTScheduler s = Scheduler (s, [ThreadId])
-- The initial state for each run is the final state of the last run,
-- so it is important that the scheduler actually maintain some
-- internal state, or all the results will be identical.
runSCT :: SCTScheduler s -> s -> Int -> (forall t. Conc t a) -> IO [(Maybe a, [ThreadId])]
runSCT :: SCTScheduler s -> s -> Int -> (forall t. Conc t a) -> IO [(Maybe a, [Decision])]
runSCT sched s runs c = runSCT' s runs where
runSCT' _ 0 = return []
runSCT' s n = do
(res, (s', log)) <- runConc' sched (s, [0]) c
(res, (s', log)) <- runConc' sched (s, [Start 0]) c
rest <- runSCT' s' $ n - 1
return $ (res, log) : rest
-- | A simple pre-emptive random scheduler.
sctRandom :: RandomGen g => SCTScheduler g
sctRandom (g, log) _ threads = (tid, (g', log ++ [tid])) where
sctRandom (g, log) last threads = (tid, (g', log ++ [decision])) where
(choice, g') = randomR (0, length threads - 1) g
tid = threads !! choice
decision | tid == last = Continue
| last `elem` threads = SwitchTo tid
| otherwise = Start tid
-- | Pretty-print a scheduler trace.
showTrace :: [Decision] -> String
showTrace = trace "" 0 where
trace log num (Start tid:ds) = thread log num ++ trace ("S" ++ show tid) 1 ds
trace log num (Continue:ds) = trace log (num + 1) ds
trace log num (SwitchTo tid:ds) = thread log num ++ trace ("P" ++ show tid) 1 ds
trace log num [] = thread log num
thread "" _ = ""
thread log num = log ++ replicate num '-'