Add a simple runner which gathers results and schedulings from multiple runs

This commit is contained in:
Michael Walker 2014-12-20 11:01:51 +00:00
parent 86a2617b41
commit 82e9241686
2 changed files with 72 additions and 0 deletions

71
Control/Monad/Conc/SCT.hs Normal file
View File

@ -0,0 +1,71 @@
{-# LANGUAGE RankNTypes #-}
-- | A runner for concurrent monads to systematically detect
-- concurrency errors such as data races and deadlocks.
--
-- As an example, consider this program, which has two locks and a
-- shared variable. Two threads are spawned, which claim the locks,
-- update the shared variable, and release the locks. The main thread
-- waits for them both to terminate, and returns the final result.
--
-- > bad :: Conc t Int
-- > bad = do
-- > a <- new
-- > b <- new
-- >
-- > c <- new
-- > put c 0
-- >
-- > j1 <- spawn $ put a () >> put b () >> take c >>= put c . succ >> take b >> take a
-- > j2 <- spawn $ put b () >> put a () >> take c >>= put c . pred >> take a >> take b
-- >
-- > take j1
-- > take j2
-- >
-- > take c
--
-- The correct result is 0, as it starts out as 0 and is incremented
-- and decremented by threads 1 and 2, respectively. However, note the
-- order of acquisition of the locks in the two threads. If thread 2
-- pre-empts thread 1 between the acquisition of the locks (or if
-- thread 1 pre-empts thread 2), a deadlock situation will arise, as
-- thread 1 will have lock `a` and be waiting on `b`, and thread 2
-- will have `b` and be waiting on `a`.
module Control.Monad.Conc.SCT
( -- *Systematic Concurrency Testing
SCTScheduler
, runSCT
, sctRandom
) where
import Prelude hiding (take)
import Control.Monad.Conc.Fixed
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])
-- | Run a concurrent program under a given scheduler a number of
-- times, collecting the results and the scheduling that gave rise to
-- them.
--
-- 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 sched s runs c = runSCT' s runs where
runSCT' _ 0 = return []
runSCT' s n = do
(res, (s', log)) <- runConc' sched (s, [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
(choice, g') = randomR (0, length threads - 1) g
tid = threads !! choice

View File

@ -19,6 +19,7 @@ cabal-version: >=1.10
library
exposed-modules: Control.Monad.Conc.Class
, Control.Monad.Conc.Fixed
, Control.Monad.Conc.SCT
-- other-modules:
-- other-extensions:
build-depends: base >=4.6 && <5