mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-20 12:01:33 +03:00
Tidy up code a bit, also drop monad-st
This commit is contained in:
parent
03a61057b5
commit
cc40353001
@ -1,8 +1,127 @@
|
|||||||
|
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||||
|
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||||
|
{-# LANGUAGE Rank2Types #-}
|
||||||
|
|
||||||
-- | Concurrent monads with a fixed scheduler.
|
-- | Concurrent monads with a fixed scheduler.
|
||||||
module Control.Monad.Conc.Fixed
|
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
|
, module Control.Monad.Conc.Fixed.Schedulers
|
||||||
) where
|
) 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.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 <https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html>
|
||||||
|
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
|
||||||
|
@ -29,10 +29,14 @@ module Control.Monad.Conc.Fixed.IO
|
|||||||
, readCVar
|
, readCVar
|
||||||
, takeCVar
|
, takeCVar
|
||||||
, tryTakeCVar
|
, tryTakeCVar
|
||||||
|
|
||||||
|
-- * Schedulers
|
||||||
|
, module Control.Monad.Conc.Fixed.Schedulers
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import Control.Applicative (Applicative(..), (<$>))
|
import Control.Applicative (Applicative(..), (<$>))
|
||||||
import Control.Monad.Conc.Fixed.Internal
|
import Control.Monad.Conc.Fixed.Internal
|
||||||
|
import Control.Monad.Conc.Fixed.Schedulers
|
||||||
import Control.Monad.Cont (cont, runCont)
|
import Control.Monad.Cont (cont, runCont)
|
||||||
import Data.IORef (IORef, newIORef, readIORef, writeIORef)
|
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
|
-- Note how the @t@ in 'Conc' is universally quantified, what this
|
||||||
-- means in practice is that you can't do something like 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
|
-- So 'CVar's cannot leak out of the 'Conc' computation. If this is
|
||||||
-- making your head hurt, check out the \"How @runST@ works\" section
|
-- making your head hurt, check out the \"How @runST@ works\" section
|
||||||
|
@ -13,7 +13,7 @@ import Data.Maybe (catMaybes, fromJust, isNothing)
|
|||||||
|
|
||||||
import qualified Data.Map as M
|
import qualified Data.Map as M
|
||||||
|
|
||||||
-- * Types
|
-- * The @Conc@ Monad
|
||||||
|
|
||||||
-- | The underlying monad is based on continuations over Actions.
|
-- | The underlying monad is based on continuations over Actions.
|
||||||
type M n r a = Cont (Action n r) a
|
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.
|
-- and a list of things blocked on it.
|
||||||
type R r a = r (Maybe a, [Block])
|
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 concrete implementations to override.
|
||||||
-- dict of methods for different implementations to override!
|
|
||||||
data Fixed c n r t = F
|
data Fixed c n r t = F
|
||||||
{ newRef :: forall a. a -> n (r a)
|
{ newRef :: forall a. a -> n (r a)
|
||||||
-- ^ Create a new reference
|
-- ^ Create a new reference
|
||||||
@ -38,6 +37,8 @@ data Fixed c n r t = F
|
|||||||
-- type.
|
-- type.
|
||||||
}
|
}
|
||||||
|
|
||||||
|
-- * Non-Empty Lists
|
||||||
|
|
||||||
-- | The type of non-empty lists.
|
-- | The type of non-empty lists.
|
||||||
data NonEmpty a = a :| [a] deriving (Eq, Ord, Read, Show)
|
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 :: NonEmpty a -> [a]
|
||||||
toList (a :| as) = a : as
|
toList (a :| as) = a : as
|
||||||
|
|
||||||
-- * Running @Conc@ monads
|
-- * Running @Conc@ Computations
|
||||||
|
|
||||||
-- | Scheduling is done in terms of a trace of 'Action's. Blocking can
|
-- | 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
|
-- 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
|
-- primitives of the concurrency. 'spawn' is absent as it is
|
||||||
-- derived from 'new', 'fork' and 'put'.
|
-- implemented in terms of 'newEmptyCVar', 'fork', and 'putCVar'.
|
||||||
data Action n r =
|
data Action n r =
|
||||||
AFork (Action n r) (Action n r)
|
AFork (Action n r) (Action n r)
|
||||||
| forall a. APut (R r a) a (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
|
-- 'ThreadId' of the last thread scheduled, and the list of runnable
|
||||||
-- threads. It produces a 'ThreadId' to schedule, and a new state.
|
-- threads. It produces a 'ThreadId' to schedule, and a new state.
|
||||||
--
|
--
|
||||||
-- Note: In order to prevent deadlock, the 'Conc' runtime will assume
|
-- Note: In order to prevent computation from hanging, the 'Conc'
|
||||||
-- that a deadlock situation has arisen if the scheduler attempts to
|
-- runtime will assume that a deadlock situation has arisen if the
|
||||||
-- (a) schedule a blocked thread, or (b) schedule a nonexistant
|
-- scheduler attempts to (a) schedule a blocked thread, or (b)
|
||||||
-- thread. In either of those cases, the computation will be halted.
|
-- schedule a nonexistent thread. In either of those cases, the
|
||||||
|
-- computation will be halted.
|
||||||
type Scheduler s = s -> ThreadId -> NonEmpty ThreadId -> (ThreadId, s)
|
type Scheduler s = s -> ThreadId -> NonEmpty ThreadId -> (ThreadId, s)
|
||||||
|
|
||||||
-- | One of the outputs of the runner is a @Trace@, which is just a
|
-- | One of the outputs of the runner is a @Trace@, which is just a
|
||||||
@ -110,7 +112,9 @@ data ThreadAction =
|
|||||||
| TryTake Bool [ThreadId]
|
| TryTake Bool [ThreadId]
|
||||||
-- ^ Try to take from a 'CVar', possibly waking up some threads.
|
-- ^ Try to take from a 'CVar', possibly waking up some threads.
|
||||||
| Lift
|
| 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
|
| Stop
|
||||||
-- ^ Cease execution and terminate.
|
-- ^ Cease execution and terminate.
|
||||||
deriving (Eq, Show)
|
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)
|
-> Scheduler s -> s -> c t a -> n (Maybe a)
|
||||||
runFixed fixed sched s ma = liftM (\(a,_,_) -> a) $ runFixed' fixed sched s ma
|
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.
|
-- scheduler and an execution trace.
|
||||||
runFixed' :: (Monad (c t), Monad n) => Fixed c n r t
|
runFixed' :: (Monad (c t), Monad n) => Fixed c n r t
|
||||||
-> Scheduler s -> s -> c t a -> n (Maybe a, s, Trace)
|
-> Scheduler s -> s -> c t a -> n (Maybe a, s, Trace)
|
||||||
|
@ -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 <https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html>
|
|
||||||
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
|
|
@ -79,11 +79,13 @@ makeSCT :: Scheduler s -> SCTScheduler s
|
|||||||
makeSCT sched (s, trace) prior threads = (tid, (s', (decision, alters) : trace)) where
|
makeSCT sched (s, trace) prior threads = (tid, (s', (decision, alters) : trace)) where
|
||||||
(tid, s') = sched s prior threads
|
(tid, s') = sched s prior threads
|
||||||
|
|
||||||
decision | tid == prior = Continue
|
decision
|
||||||
|
| tid == prior = Continue
|
||||||
| prior `elem` threads' = SwitchTo tid
|
| prior `elem` threads' = SwitchTo tid
|
||||||
| otherwise = Start tid
|
| otherwise = Start tid
|
||||||
|
|
||||||
alters | tid == prior = map SwitchTo $ filter (/=prior) threads'
|
alters
|
||||||
|
| tid == prior = map SwitchTo $ filter (/=prior) threads'
|
||||||
| prior `elem` threads' = Continue : map SwitchTo (filter (\t -> t /= prior && t /= tid) threads')
|
| prior `elem` threads' = Continue : map SwitchTo (filter (\t -> t /= prior && t /= tid) threads')
|
||||||
| otherwise = map Start $ filter (/=tid) threads'
|
| otherwise = map Start $ filter (/=tid) threads'
|
||||||
|
|
||||||
|
@ -45,8 +45,8 @@ data Decision =
|
|||||||
|
|
||||||
instance NFData Decision where
|
instance NFData Decision where
|
||||||
rnf (Start tid) = rnf tid
|
rnf (Start tid) = rnf tid
|
||||||
rnf Continue = ()
|
|
||||||
rnf (SwitchTo tid) = rnf tid
|
rnf (SwitchTo tid) = rnf tid
|
||||||
|
rnf Continue = ()
|
||||||
|
|
||||||
-- * SCT Runners
|
-- * SCT Runners
|
||||||
|
|
||||||
|
@ -132,16 +132,21 @@ pbStep pb lifts (s, g) t = case _next g of
|
|||||||
--
|
--
|
||||||
-- If there are no more schedules, halt.
|
-- If there are no more schedules, halt.
|
||||||
Empty ->
|
Empty ->
|
||||||
case thisPB of
|
case (thisPB, nextPB) of
|
||||||
(x:xs)
|
-- 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 })
|
| pb /= pc -> (s' x, g { _next = nextPB +| xs +| Empty })
|
||||||
| otherwise -> (s' x, g { _next = xs +| Empty })
|
| otherwise -> (s' x, g { _next = xs +| Empty })
|
||||||
[]
|
|
||||||
| pb /= pc ->
|
-- No schedules left in this PB, but if we have some more from
|
||||||
case nextPB of
|
-- the next PB (and we're not at the limit) add those.
|
||||||
(x:xs) -> (s' x, g { _next = xs +| Empty })
|
([], x:xs)
|
||||||
[] -> (s' [], g { _halt = True })
|
| pb /= pc -> (s' x, g { _next = xs +| Empty })
|
||||||
| otherwise -> (s' [], g { _halt = True })
|
|
||||||
|
-- No schedules left at all, so halt.
|
||||||
|
_ -> halt
|
||||||
|
|
||||||
where
|
where
|
||||||
-- The prefix and suffix are in reverse order, fix those.
|
-- 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.
|
-- | New scheduler state, with a given list of initial decisions.
|
||||||
s' ds = pbInitialS { _decisions = ds }
|
s' ds = pbInitialS { _decisions = ds }
|
||||||
|
|
||||||
|
-- | The halt state
|
||||||
|
halt = (pbInitialS, g { _halt = True })
|
||||||
|
|
||||||
-- | All schedules we get from the current one WITHOUT introducing
|
-- | All schedules we get from the current one WITHOUT introducing
|
||||||
-- any pre-emptions.
|
-- any pre-emptions.
|
||||||
thisPB = [ pref' y | y <- siblings suff]
|
thisPB = [ pref' y | y <- siblings suff]
|
||||||
|
@ -3,8 +3,7 @@
|
|||||||
-- | Useful functions for writing SCT test cases for @Conc@
|
-- | Useful functions for writing SCT test cases for @Conc@
|
||||||
-- computations.
|
-- computations.
|
||||||
module Control.Monad.Conc.SCT.Tests
|
module Control.Monad.Conc.SCT.Tests
|
||||||
(
|
( doTests
|
||||||
doTests
|
|
||||||
-- * Test cases
|
-- * Test cases
|
||||||
, Result(..)
|
, Result(..)
|
||||||
, runTest
|
, runTest
|
||||||
|
@ -47,7 +47,6 @@ library
|
|||||||
exposed-modules: Control.Monad.Conc.Class
|
exposed-modules: Control.Monad.Conc.Class
|
||||||
, Control.Monad.Conc.CVar
|
, Control.Monad.Conc.CVar
|
||||||
, Control.Monad.Conc.Fixed
|
, Control.Monad.Conc.Fixed
|
||||||
, Control.Monad.Conc.Fixed.ST
|
|
||||||
, Control.Monad.Conc.Fixed.IO
|
, Control.Monad.Conc.Fixed.IO
|
||||||
, Control.Monad.Conc.Fixed.Schedulers
|
, Control.Monad.Conc.Fixed.Schedulers
|
||||||
, Control.Monad.Conc.SCT
|
, Control.Monad.Conc.SCT
|
||||||
@ -60,7 +59,6 @@ library
|
|||||||
, containers
|
, containers
|
||||||
, deepseq
|
, deepseq
|
||||||
, monad-loops
|
, monad-loops
|
||||||
, monad-st
|
|
||||||
, mtl
|
, mtl
|
||||||
, random
|
, random
|
||||||
, transformers
|
, transformers
|
||||||
|
@ -1,6 +1,7 @@
|
|||||||
-- | Tests sourced from <https://github.com/sctbenchmarks>.
|
-- | Tests sourced from <https://github.com/sctbenchmarks>.
|
||||||
module Tests.Cases where
|
module Tests.Cases where
|
||||||
|
|
||||||
|
import Control.Applicative ((<$>))
|
||||||
import Control.Monad (replicateM)
|
import Control.Monad (replicateM)
|
||||||
import Control.Monad.Conc.Class
|
import Control.Monad.Conc.Class
|
||||||
import Control.Monad.Conc.CVar
|
import Control.Monad.Conc.CVar
|
||||||
@ -11,17 +12,17 @@ import qualified Tests.Logger as L
|
|||||||
-- | List of all tests
|
-- | List of all tests
|
||||||
testCases :: [(String, Result String)]
|
testCases :: [(String, Result String)]
|
||||||
testCases =
|
testCases =
|
||||||
[ ("Simple 2-Deadlock" , fmap show $ runTest deadlocksSometimes simple2Deadlock)
|
[ ("Simple 2-Deadlock" , show <$> runTest deadlocksSometimes simple2Deadlock)
|
||||||
, ("2 Philosophers" , fmap show $ runTest deadlocksSometimes $ philosophers 2)
|
, ("2 Philosophers" , show <$> runTest deadlocksSometimes (philosophers 2))
|
||||||
, ("3 Philosophers" , fmap show $ runTest deadlocksSometimes $ philosophers 3)
|
, ("3 Philosophers" , show <$> runTest deadlocksSometimes (philosophers 3))
|
||||||
, ("4 Philosophers" , fmap show $ runTest deadlocksSometimes $ philosophers 4)
|
, ("4 Philosophers" , show <$> runTest deadlocksSometimes (philosophers 4))
|
||||||
, ("Threshold Value" , fmap show $ runTest (pNot alwaysSame) thresholdValue)
|
, ("Threshold Value" , show <$> runTest (pNot alwaysSame) thresholdValue)
|
||||||
, ("Forgotten Unlock" , fmap show $ runTest deadlocksAlways forgottenUnlock)
|
, ("Forgotten Unlock" , show <$> runTest deadlocksAlways forgottenUnlock)
|
||||||
, ("Simple 2-Race" , fmap show $ runTest (pNot alwaysSame) simple2Race)
|
, ("Simple 2-Race" , show <$> runTest (pNot alwaysSame) simple2Race)
|
||||||
, ("Racey Stack" , fmap show $ runTest (pNot alwaysSame) raceyStack)
|
, ("Racey Stack" , show <$> runTest (pNot alwaysSame) raceyStack)
|
||||||
, ("Logger (LA)" , fmap show $ L.testLA)
|
, ("Logger (LA)" , show <$> L.testLA)
|
||||||
, ("Logger (LP)" , fmap show $ L.testLP)
|
, ("Logger (LP)" , show <$> L.testLP)
|
||||||
, ("Logger (LE)" , fmap show $ L.testLE)
|
, ("Logger (LE)" , show <$> L.testLE)
|
||||||
]
|
]
|
||||||
|
|
||||||
-- | Should deadlock on a minority of schedules.
|
-- | Should deadlock on a minority of schedules.
|
||||||
|
Loading…
Reference in New Issue
Block a user