diff --git a/Control/Monad/Conc/Fixed.hs b/Control/Monad/Conc/Fixed.hs index 144947c..fdb21f0 100755 --- a/Control/Monad/Conc/Fixed.hs +++ b/Control/Monad/Conc/Fixed.hs @@ -1,8 +1,127 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Rank2Types #-} + -- | Concurrent monads with a fixed scheduler. module Control.Monad.Conc.Fixed - ( module Control.Monad.Conc.Fixed.ST + ( -- * The Conc Monad + Conc + , Trace + , ThreadAction(..) + , runConc + , runConc' + , spawn + , fork + + -- * Communication: CVars + , CVar + , newEmptyCVar + , putCVar + , tryPutCVar + , readCVar + , takeCVar + , tryTakeCVar + + -- * Schedulers , module Control.Monad.Conc.Fixed.Schedulers ) where -import Control.Monad.Conc.Fixed.ST +import Control.Applicative (Applicative(..), (<$>)) +import Control.Monad.Conc.Fixed.Internal import Control.Monad.Conc.Fixed.Schedulers +import Control.Monad.Cont (cont, runCont) +import Control.Monad.ST (ST, runST) +import Data.STRef (STRef, newSTRef, readSTRef, writeSTRef) + +import qualified Control.Monad.Conc.Class as C + +-- | The @Conc@ monad itself. This uses the same +-- universally-quantified indexing state trick as used by 'ST' and +-- 'STRef's to prevent mutable references from leaking out of the +-- monad. See 'runConc' for an example of what this means. +newtype Conc t a = C { unC :: M (ST t) (STRef t) a } deriving (Functor, Applicative, Monad) + +instance C.ConcFuture (CVar t) (Conc t) where + spawn = spawn + readCVar = readCVar + +instance C.ConcCVar (CVar t) (Conc t) where + fork = fork + newEmptyCVar = newEmptyCVar + putCVar = putCVar + tryPutCVar = tryPutCVar + takeCVar = takeCVar + tryTakeCVar = tryTakeCVar + +fixed :: Fixed Conc (ST t) (STRef t) t +fixed = F + { newRef = newSTRef + , readRef = readSTRef + , writeRef = writeSTRef + , liftN = \ma -> C $ cont (\c -> ALift $ c <$> ma) + , getCont = unC + } + +-- | The concurrent variable type used with the 'Conc' monad. One +-- notable difference between these and 'MVar's is that 'MVar's are +-- single-wakeup, and wake up in a FIFO order. Writing to a @CVar@ +-- wakes up all threads blocked on reading it, and it is up to the +-- scheduler which one runs next. Taking from a @CVar@ behaves +-- analogously. +newtype CVar t a = V { unV :: R (STRef t) a } deriving Eq + +-- | Run the provided computation concurrently, returning the result. +spawn :: Conc t a -> Conc t (CVar t a) +spawn = C.defaultSpawn + +-- | Block on a 'CVar' until it is full, then read from it (without +-- emptying). +readCVar :: CVar t a -> Conc t a +readCVar cvar = C $ cont $ AGet $ unV cvar + +-- | Run the provided computation concurrently. +fork :: Conc t () -> Conc t () +fork (C ma) = C $ cont $ \c -> AFork (runCont ma $ const AStop) $ c () + +-- | Create a new empty 'CVar'. +newEmptyCVar :: Conc t (CVar t a) +newEmptyCVar = C $ cont lifted where + lifted c = ANew $ c <$> newEmptyCVar' + newEmptyCVar' = V <$> newSTRef (Nothing, []) + +-- | Block on a 'CVar' until it is empty, then write to it. +putCVar :: CVar t a -> a -> Conc t () +putCVar cvar a = C $ cont $ \c -> APut (unV cvar) a $ c () + +-- | Put a value into a 'CVar' if there isn't one, without blocking. +tryPutCVar :: CVar t a -> a -> Conc t Bool +tryPutCVar cvar a = C $ cont $ ATryPut (unV cvar) a + +-- | Block on a 'CVar' until it is full, then read from it (with +-- emptying). +takeCVar :: CVar t a -> Conc t a +takeCVar cvar = C $ cont $ ATake $ unV cvar + +-- | Read a value from a 'CVar' if there is one, without blocking. +tryTakeCVar :: CVar t a -> Conc t (Maybe a) +tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar + +-- | Run a concurrent computation with a given 'Scheduler' and initial +-- state, returning a 'Just' if it terminates, and 'Nothing' if a +-- deadlock is detected. +-- +-- Note how the @t@ in 'Conc' is universally quantified, what this +-- means in practice is that you can't do something like this: +-- +-- > runConc (\s _ (x:_) -> (x, s)) () $ new >>= return +-- +-- So 'CVar's cannot leak out of the 'Conc' computation. If this is +-- making your head hurt, check out the \"How @runST@ works\" section +-- of +runConc :: Scheduler s -> s -> (forall t. Conc t a) -> Maybe a +runConc sched s ma = let (a,_,_) = runConc' sched s ma in a + +-- | Variant of 'runConc' which returns the final state of the +-- scheduler and an execution trace. +runConc' :: Scheduler s -> s -> (forall t. Conc t a) -> (Maybe a, s, Trace) +runConc' sched s ma = runST $ runFixed' fixed sched s ma diff --git a/Control/Monad/Conc/Fixed/IO.hs b/Control/Monad/Conc/Fixed/IO.hs index d367a00..b563284 100644 --- a/Control/Monad/Conc/Fixed/IO.hs +++ b/Control/Monad/Conc/Fixed/IO.hs @@ -29,10 +29,14 @@ module Control.Monad.Conc.Fixed.IO , readCVar , takeCVar , tryTakeCVar + + -- * Schedulers + , module Control.Monad.Conc.Fixed.Schedulers ) where import Control.Applicative (Applicative(..), (<$>)) import Control.Monad.Conc.Fixed.Internal +import Control.Monad.Conc.Fixed.Schedulers import Control.Monad.Cont (cont, runCont) import Data.IORef (IORef, newIORef, readIORef, writeIORef) @@ -126,7 +130,7 @@ tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar -- Note how the @t@ in 'Conc' is universally quantified, what this -- means in practice is that you can't do something like this: -- --- > runConc (\s _ (x:_) -> (x, s)) () $ new >>= return +-- > runConc (\s _ (x:_) -> (x, s)) () newEmptyCVar -- -- So 'CVar's cannot leak out of the 'Conc' computation. If this is -- making your head hurt, check out the \"How @runST@ works\" section diff --git a/Control/Monad/Conc/Fixed/Internal.hs b/Control/Monad/Conc/Fixed/Internal.hs index 5bf5a68..82e0bc8 100644 --- a/Control/Monad/Conc/Fixed/Internal.hs +++ b/Control/Monad/Conc/Fixed/Internal.hs @@ -13,7 +13,7 @@ import Data.Maybe (catMaybes, fromJust, isNothing) import qualified Data.Map as M --- * Types +-- * The @Conc@ Monad -- | The underlying monad is based on continuations over Actions. type M n r a = Cont (Action n r) a @@ -22,8 +22,7 @@ type M n r a = Cont (Action n r) a -- and a list of things blocked on it. type R r a = r (Maybe a, [Block]) --- | Doing this with a typeclass proved to be really hard, so here's a --- dict of methods for different implementations to override! +-- | Dict of methods for concrete implementations to override. data Fixed c n r t = F { newRef :: forall a. a -> n (r a) -- ^ Create a new reference @@ -38,6 +37,8 @@ data Fixed c n r t = F -- type. } +-- * Non-Empty Lists + -- | The type of non-empty lists. data NonEmpty a = a :| [a] deriving (Eq, Ord, Read, Show) @@ -51,12 +52,12 @@ instance NFData a => NFData (NonEmpty a) where toList :: NonEmpty a -> [a] toList (a :| as) = a : as --- * Running @Conc@ monads +-- * Running @Conc@ Computations -- | Scheduling is done in terms of a trace of 'Action's. Blocking can -- only occur as a result of an action, and they cover (most of) the --- primitives of the concurrency. 'spawn' is absent as it can be --- derived from 'new', 'fork' and 'put'. +-- primitives of the concurrency. 'spawn' is absent as it is +-- implemented in terms of 'newEmptyCVar', 'fork', and 'putCVar'. data Action n r = AFork (Action n r) (Action n r) | forall a. APut (R r a) a (Action n r) @@ -77,10 +78,11 @@ type ThreadId = Int -- 'ThreadId' of the last thread scheduled, and the list of runnable -- threads. It produces a 'ThreadId' to schedule, and a new state. -- --- Note: In order to prevent deadlock, the 'Conc' runtime will assume --- that a deadlock situation has arisen if the scheduler attempts to --- (a) schedule a blocked thread, or (b) schedule a nonexistant --- thread. In either of those cases, the computation will be halted. +-- Note: In order to prevent computation from hanging, the 'Conc' +-- runtime will assume that a deadlock situation has arisen if the +-- scheduler attempts to (a) schedule a blocked thread, or (b) +-- schedule a nonexistent thread. In either of those cases, the +-- computation will be halted. type Scheduler s = s -> ThreadId -> NonEmpty ThreadId -> (ThreadId, s) -- | One of the outputs of the runner is a @Trace@, which is just a @@ -110,7 +112,9 @@ data ThreadAction = | TryTake Bool [ThreadId] -- ^ Try to take from a 'CVar', possibly waking up some threads. | Lift - -- ^ Lift an action from the underlying monad. + -- ^ Lift an action from the underlying monad. Note that the + -- penultimate action in a trace will always be a @Lift@, this is an + -- artefact of how the runner works. | Stop -- ^ Cease execution and terminate. deriving (Eq, Show) @@ -136,7 +140,7 @@ runFixed :: (Monad (c t), Monad n) => Fixed c n r t -> Scheduler s -> s -> c t a -> n (Maybe a) runFixed fixed sched s ma = liftM (\(a,_,_) -> a) $ runFixed' fixed sched s ma --- | Variant of 'runConc' which returns the final state of the +-- | Variant of 'runFixed' which returns the final state of the -- scheduler and an execution trace. runFixed' :: (Monad (c t), Monad n) => Fixed c n r t -> Scheduler s -> s -> c t a -> n (Maybe a, s, Trace) @@ -281,7 +285,7 @@ stepTryTake ref c fixed i threads = do writeRef fixed ref (Nothing, blocks) (threads', woken) <- wake fixed ref WaitEmpty threads return (goto (c val) i threads', TryTake True woken) - Nothing -> return (goto (c Nothing) i threads, TryTake False []) + Nothing -> return (goto (c Nothing) i threads, TryTake False []) -- | Create a new @CVar@. This is exactly the same as lifting a value, -- except by separating the two we can (a) produce a more useful diff --git a/Control/Monad/Conc/Fixed/ST.hs b/Control/Monad/Conc/Fixed/ST.hs deleted file mode 100644 index 67f5aea..0000000 --- a/Control/Monad/Conc/Fixed/ST.hs +++ /dev/null @@ -1,141 +0,0 @@ -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE TypeFamilies #-} - --- | Concurrent monads with a fixed scheduler which can do ST. -module Control.Monad.Conc.Fixed.ST - ( -- * The Conc Monad - Conc - , Trace - , ThreadAction(..) - , runConc - , runConc' - , runConcST - , liftST - , spawn - , fork - - -- * Communication: CVars - , CVar - , newEmptyCVar - , putCVar - , tryPutCVar - , readCVar - , takeCVar - , tryTakeCVar - ) where - -import Control.Applicative (Applicative(..), (<$>)) -import Control.Monad.Conc.Fixed.Internal -import Control.Monad.Cont (cont, runCont) -import Control.Monad.ST (ST, runST) -import Data.STRef (STRef, newSTRef, readSTRef, writeSTRef) - -import qualified Control.Monad.Conc.Class as C -import qualified Control.Monad.ST.Class as ST - --- | The @Conc@ monad itself. This uses the same --- universally-quantified indexing state trick as used by 'ST' and --- 'STRef's to prevent mutable references from leaking out of the --- monad. See 'runConc' for an example of what this means. -newtype Conc t a = C { unC :: M (ST t) (STRef t) a } deriving (Functor, Applicative, Monad) - -instance ST.MonadST (Conc t) where - type World (Conc t) = t - liftST = liftST - -instance C.ConcFuture (CVar t) (Conc t) where - spawn = spawn - readCVar = readCVar - -instance C.ConcCVar (CVar t) (Conc t) where - fork = fork - newEmptyCVar = newEmptyCVar - putCVar = putCVar - tryPutCVar = tryPutCVar - takeCVar = takeCVar - tryTakeCVar = tryTakeCVar - -fixed :: Fixed Conc (ST t) (STRef t) t -fixed = F - { newRef = newSTRef - , readRef = readSTRef - , writeRef = writeSTRef - , liftN = liftST - , getCont = unC - } - --- | The concurrent variable type used with the 'Conc' monad. One --- notable difference between these and 'MVar's is that 'MVar's are --- single-wakeup, and wake up in a FIFO order. Writing to a @CVar@ --- wakes up all threads blocked on reading it, and it is up to the --- scheduler which one runs next. Taking from a @CVar@ behaves --- analogously. -newtype CVar t a = V { unV :: R (STRef t) a } deriving Eq - --- | Lift an 'ST' action into the 'Conc' monad. -liftST :: ST t a -> Conc t a -liftST ma = C $ cont lifted where - lifted c = ALift $ c <$> ma - --- | Run the provided computation concurrently, returning the result. -spawn :: Conc t a -> Conc t (CVar t a) -spawn = C.defaultSpawn - --- | Block on a 'CVar' until it is full, then read from it (without --- emptying). -readCVar :: CVar t a -> Conc t a -readCVar cvar = C $ cont $ AGet $ unV cvar - --- | Run the provided computation concurrently. -fork :: Conc t () -> Conc t () -fork (C ma) = C $ cont $ \c -> AFork (runCont ma $ const AStop) $ c () - --- | Create a new empty 'CVar'. -newEmptyCVar :: Conc t (CVar t a) -newEmptyCVar = C $ cont lifted where - lifted c = ANew $ c <$> newEmptyCVar' - newEmptyCVar' = V <$> newSTRef (Nothing, []) - --- | Block on a 'CVar' until it is empty, then write to it. -putCVar :: CVar t a -> a -> Conc t () -putCVar cvar a = C $ cont $ \c -> APut (unV cvar) a $ c () - --- | Put a value into a 'CVar' if there isn't one, without blocking. -tryPutCVar :: CVar t a -> a -> Conc t Bool -tryPutCVar cvar a = C $ cont $ ATryPut (unV cvar) a - --- | Block on a 'CVar' until it is full, then read from it (with --- emptying). -takeCVar :: CVar t a -> Conc t a -takeCVar cvar = C $ cont $ ATake $ unV cvar - --- | Read a value from a 'CVar' if there is one, without blocking. -tryTakeCVar :: CVar t a -> Conc t (Maybe a) -tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar - --- | Run a concurrent computation with a given 'Scheduler' and initial --- state, returning a 'Just' if it terminates, and 'Nothing' if a --- deadlock is detected. --- --- Note how the @t@ in 'Conc' is universally quantified, what this --- means in practice is that you can't do something like this: --- --- > runConc (\s _ (x:_) -> (x, s)) () $ new >>= return --- --- So 'CVar's cannot leak out of the 'Conc' computation. If this is --- making your head hurt, check out the \"How @runST@ works\" section --- of -runConc :: Scheduler s -> s -> (forall t. Conc t a) -> Maybe a -runConc sched s ma = let (a,_,_) = runConc' sched s ma in a - --- | Variant of 'runConc' which returns the final state of the --- scheduler and an execution trace. -runConc' :: Scheduler s -> s -> (forall t. Conc t a) -> (Maybe a, s, Trace) -runConc' sched s ma = runST $ runConcST sched s ma - --- | Variant of 'runConc' keeping the result in ST, allowing for --- further processing. -runConcST :: Scheduler s -> s -> Conc t a -> ST t (Maybe a, s, Trace) -runConcST = runFixed' fixed diff --git a/Control/Monad/Conc/SCT.hs b/Control/Monad/Conc/SCT.hs index 261a106..5acecd8 100644 --- a/Control/Monad/Conc/SCT.hs +++ b/Control/Monad/Conc/SCT.hs @@ -79,22 +79,24 @@ makeSCT :: Scheduler s -> SCTScheduler s makeSCT sched (s, trace) prior threads = (tid, (s', (decision, alters) : trace)) where (tid, s') = sched s prior threads - decision | tid == prior = Continue - | prior `elem` threads' = SwitchTo tid - | otherwise = Start tid + decision + | tid == prior = Continue + | prior `elem` threads' = SwitchTo tid + | otherwise = Start tid - alters | tid == prior = map SwitchTo $ filter (/=prior) threads' - | prior `elem` threads' = Continue : map SwitchTo (filter (\t -> t /= prior && t /= tid) threads') - | otherwise = map Start $ filter (/=tid) threads' + alters + | tid == prior = map SwitchTo $ filter (/=prior) threads' + | prior `elem` threads' = Continue : map SwitchTo (filter (\t -> t /= prior && t /= tid) threads') + | otherwise = map Start $ filter (/=tid) threads' threads' = toList threads -- | Pretty-print a scheduler trace. showTrace :: SchedTrace -> String showTrace = trace "" 0 . map fst where - trace prefix num (Start tid:ds) = thread prefix num ++ trace ("S" ++ show tid) 1 ds - trace prefix num (SwitchTo tid:ds) = thread prefix num ++ trace ("P" ++ show tid) 1 ds - trace prefix num (Continue:ds) = trace prefix (num + 1) ds - trace prefix num [] = thread prefix num + trace prefix num (Start tid:ds) = thread prefix num ++ trace ("S" ++ show tid) 1 ds + trace prefix num (SwitchTo tid:ds) = thread prefix num ++ trace ("P" ++ show tid) 1 ds + trace prefix num (Continue:ds) = trace prefix (num + 1) ds + trace prefix num [] = thread prefix num - thread prefix num = prefix ++ replicate num '-' + thread prefix num = prefix ++ replicate num '-' diff --git a/Control/Monad/Conc/SCT/Internal.hs b/Control/Monad/Conc/SCT/Internal.hs index 115b4dc..cef1b76 100755 --- a/Control/Monad/Conc/SCT/Internal.hs +++ b/Control/Monad/Conc/SCT/Internal.hs @@ -44,9 +44,9 @@ data Decision = deriving (Eq, Show) instance NFData Decision where - rnf (Start tid) = rnf tid - rnf Continue = () + rnf (Start tid) = rnf tid rnf (SwitchTo tid) = rnf tid + rnf Continue = () -- * SCT Runners diff --git a/Control/Monad/Conc/SCT/PreBound.hs b/Control/Monad/Conc/SCT/PreBound.hs index d27e281..e5b0475 100755 --- a/Control/Monad/Conc/SCT/PreBound.hs +++ b/Control/Monad/Conc/SCT/PreBound.hs @@ -132,16 +132,21 @@ pbStep pb lifts (s, g) t = case _next g of -- -- If there are no more schedules, halt. Empty -> - case thisPB of - (x:xs) + case (thisPB, nextPB) of + -- We still have schedules in the current PB, so add those to + -- the queue (and any schedules from the next PB if we're not at + -- the limit) + (x:xs, _) | pb /= pc -> (s' x, g { _next = nextPB +| xs +| Empty }) | otherwise -> (s' x, g { _next = xs +| Empty }) - [] - | pb /= pc -> - case nextPB of - (x:xs) -> (s' x, g { _next = xs +| Empty }) - [] -> (s' [], g { _halt = True }) - | otherwise -> (s' [], g { _halt = True }) + + -- No schedules left in this PB, but if we have some more from + -- the next PB (and we're not at the limit) add those. + ([], x:xs) + | pb /= pc -> (s' x, g { _next = xs +| Empty }) + + -- No schedules left at all, so halt. + _ -> halt where -- The prefix and suffix are in reverse order, fix those. @@ -156,6 +161,9 @@ pbStep pb lifts (s, g) t = case _next g of -- | New scheduler state, with a given list of initial decisions. s' ds = pbInitialS { _decisions = ds } + -- | The halt state + halt = (pbInitialS, g { _halt = True }) + -- | All schedules we get from the current one WITHOUT introducing -- any pre-emptions. thisPB = [ pref' y | y <- siblings suff] diff --git a/Control/Monad/Conc/SCT/Tests.hs b/Control/Monad/Conc/SCT/Tests.hs index 12811a1..3ab3d75 100644 --- a/Control/Monad/Conc/SCT/Tests.hs +++ b/Control/Monad/Conc/SCT/Tests.hs @@ -3,8 +3,7 @@ -- | Useful functions for writing SCT test cases for @Conc@ -- computations. module Control.Monad.Conc.SCT.Tests - ( - doTests + ( doTests -- * Test cases , Result(..) , runTest diff --git a/monad-conc.cabal b/monad-conc.cabal index 136d200..9c52cca 100755 --- a/monad-conc.cabal +++ b/monad-conc.cabal @@ -47,7 +47,6 @@ library exposed-modules: Control.Monad.Conc.Class , Control.Monad.Conc.CVar , Control.Monad.Conc.Fixed - , Control.Monad.Conc.Fixed.ST , Control.Monad.Conc.Fixed.IO , Control.Monad.Conc.Fixed.Schedulers , Control.Monad.Conc.SCT @@ -60,7 +59,6 @@ library , containers , deepseq , monad-loops - , monad-st , mtl , random , transformers diff --git a/tests/Tests/Cases.hs b/tests/Tests/Cases.hs index 102ad9f..5c5898c 100644 --- a/tests/Tests/Cases.hs +++ b/tests/Tests/Cases.hs @@ -1,6 +1,7 @@ -- | Tests sourced from . module Tests.Cases where +import Control.Applicative ((<$>)) import Control.Monad (replicateM) import Control.Monad.Conc.Class import Control.Monad.Conc.CVar @@ -11,17 +12,17 @@ import qualified Tests.Logger as L -- | List of all tests testCases :: [(String, Result String)] testCases = - [ ("Simple 2-Deadlock" , fmap show $ runTest deadlocksSometimes simple2Deadlock) - , ("2 Philosophers" , fmap show $ runTest deadlocksSometimes $ philosophers 2) - , ("3 Philosophers" , fmap show $ runTest deadlocksSometimes $ philosophers 3) - , ("4 Philosophers" , fmap show $ runTest deadlocksSometimes $ philosophers 4) - , ("Threshold Value" , fmap show $ runTest (pNot alwaysSame) thresholdValue) - , ("Forgotten Unlock" , fmap show $ runTest deadlocksAlways forgottenUnlock) - , ("Simple 2-Race" , fmap show $ runTest (pNot alwaysSame) simple2Race) - , ("Racey Stack" , fmap show $ runTest (pNot alwaysSame) raceyStack) - , ("Logger (LA)" , fmap show $ L.testLA) - , ("Logger (LP)" , fmap show $ L.testLP) - , ("Logger (LE)" , fmap show $ L.testLE) + [ ("Simple 2-Deadlock" , show <$> runTest deadlocksSometimes simple2Deadlock) + , ("2 Philosophers" , show <$> runTest deadlocksSometimes (philosophers 2)) + , ("3 Philosophers" , show <$> runTest deadlocksSometimes (philosophers 3)) + , ("4 Philosophers" , show <$> runTest deadlocksSometimes (philosophers 4)) + , ("Threshold Value" , show <$> runTest (pNot alwaysSame) thresholdValue) + , ("Forgotten Unlock" , show <$> runTest deadlocksAlways forgottenUnlock) + , ("Simple 2-Race" , show <$> runTest (pNot alwaysSame) simple2Race) + , ("Racey Stack" , show <$> runTest (pNot alwaysSame) raceyStack) + , ("Logger (LA)" , show <$> L.testLA) + , ("Logger (LP)" , show <$> L.testLP) + , ("Logger (LE)" , show <$> L.testLE) ] -- | Should deadlock on a minority of schedules.