From 82e92416867845330145db24444d37cbac00c951 Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Sat, 20 Dec 2014 11:01:51 +0000 Subject: [PATCH] Add a simple runner which gathers results and schedulings from multiple runs --- Control/Monad/Conc/SCT.hs | 71 +++++++++++++++++++++++++++++++++++++++ monad-conc.cabal | 1 + 2 files changed, 72 insertions(+) create mode 100644 Control/Monad/Conc/SCT.hs diff --git a/Control/Monad/Conc/SCT.hs b/Control/Monad/Conc/SCT.hs new file mode 100644 index 0000000..9a7f265 --- /dev/null +++ b/Control/Monad/Conc/SCT.hs @@ -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 + diff --git a/monad-conc.cabal b/monad-conc.cabal index 3989b23..2d32e51 100755 --- a/monad-conc.cabal +++ b/monad-conc.cabal @@ -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