2014-12-27 15:20:45 +03:00
|
|
|
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
2015-02-13 20:47:04 +03:00
|
|
|
{-# LANGUAGE RankNTypes #-}
|
2015-01-28 15:10:19 +03:00
|
|
|
{-# LANGUAGE TypeFamilies #-}
|
2014-12-27 15:20:45 +03:00
|
|
|
|
2015-02-01 04:21:42 +03:00
|
|
|
-- | Deterministic traced execution of concurrent computations which
|
|
|
|
-- may do @IO@.
|
2014-12-27 15:20:45 +03:00
|
|
|
--
|
2015-02-01 04:21:42 +03:00
|
|
|
-- __Caution!__ Blocking on the action of another thread in 'liftIO'
|
2014-12-27 15:20:45 +03:00
|
|
|
-- cannot be detected! So if you perform some potentially blocking
|
|
|
|
-- action in a 'liftIO' the entire collection of threads may deadlock!
|
2015-02-01 04:21:42 +03:00
|
|
|
-- You should therefore keep @IO@ blocks small, and only perform
|
2014-12-27 15:20:45 +03:00
|
|
|
-- blocking operations with the supplied primitives, insofar as
|
|
|
|
-- possible.
|
2015-01-31 18:50:54 +03:00
|
|
|
module Test.DejaFu.Deterministic.IO
|
2015-02-01 04:21:42 +03:00
|
|
|
( -- * The @ConcIO@ Monad
|
|
|
|
ConcIO
|
2015-02-06 18:24:47 +03:00
|
|
|
, Failure(..)
|
2015-02-01 04:21:42 +03:00
|
|
|
, runConcIO
|
2014-12-27 15:20:45 +03:00
|
|
|
, liftIO
|
|
|
|
, fork
|
2015-02-13 20:47:04 +03:00
|
|
|
, forkFinally
|
|
|
|
, forkWithUnmask
|
2015-02-13 03:39:27 +03:00
|
|
|
, myThreadId
|
2015-01-28 15:10:19 +03:00
|
|
|
, spawn
|
2015-02-10 01:31:05 +03:00
|
|
|
, atomically
|
2015-02-12 16:42:32 +03:00
|
|
|
, throw
|
2015-02-13 20:13:00 +03:00
|
|
|
, throwTo
|
|
|
|
, killThread
|
2015-02-12 22:15:07 +03:00
|
|
|
, catch
|
2015-02-13 20:47:04 +03:00
|
|
|
, mask
|
|
|
|
, uninterruptibleMask
|
2014-12-27 15:20:45 +03:00
|
|
|
|
|
|
|
-- * Communication: CVars
|
|
|
|
, CVar
|
|
|
|
, newEmptyCVar
|
|
|
|
, putCVar
|
|
|
|
, tryPutCVar
|
|
|
|
, readCVar
|
|
|
|
, takeCVar
|
|
|
|
, tryTakeCVar
|
2015-01-25 19:15:23 +03:00
|
|
|
|
2015-02-06 19:11:20 +03:00
|
|
|
-- * Testing
|
|
|
|
, _concNoTest
|
|
|
|
|
2015-02-01 04:21:42 +03:00
|
|
|
-- * Execution traces
|
|
|
|
, Trace
|
2015-02-06 18:24:47 +03:00
|
|
|
, Decision(..)
|
|
|
|
, ThreadAction(..)
|
2015-02-03 17:14:36 +03:00
|
|
|
, CVarId
|
2015-02-01 04:21:42 +03:00
|
|
|
, showTrace
|
|
|
|
|
|
|
|
-- * Scheduling
|
|
|
|
, module Test.DejaFu.Deterministic.Schedule
|
2014-12-27 15:20:45 +03:00
|
|
|
) where
|
|
|
|
|
|
|
|
import Control.Applicative (Applicative(..), (<$>))
|
2015-02-12 16:42:32 +03:00
|
|
|
import Control.Exception (Exception, SomeException(..))
|
2014-12-27 15:20:45 +03:00
|
|
|
import Control.Monad.Cont (cont, runCont)
|
2015-02-10 01:04:28 +03:00
|
|
|
import Control.State (Wrapper(..), refIO)
|
|
|
|
import Data.IORef (IORef, newIORef)
|
2015-01-31 18:50:54 +03:00
|
|
|
import Test.DejaFu.Deterministic.Internal
|
2015-02-01 04:21:42 +03:00
|
|
|
import Test.DejaFu.Deterministic.Schedule
|
2015-02-10 01:31:05 +03:00
|
|
|
import Test.DejaFu.STM (STMLike, runTransactionIO)
|
2014-12-27 15:20:45 +03:00
|
|
|
|
2015-02-12 22:15:07 +03:00
|
|
|
import qualified Control.Monad.Catch as Ca
|
2014-12-27 15:20:45 +03:00
|
|
|
import qualified Control.Monad.Conc.Class as C
|
|
|
|
import qualified Control.Monad.IO.Class as IO
|
|
|
|
|
2015-02-01 04:21:42 +03:00
|
|
|
-- | The 'IO' variant of Test.DejaFu.Deterministic's @Conc@ monad.
|
2015-02-10 01:31:05 +03:00
|
|
|
newtype ConcIO t a = C { unC :: M IO IORef (STMLike t) a } deriving (Functor, Applicative, Monad)
|
2014-12-27 15:20:45 +03:00
|
|
|
|
2015-02-12 22:15:07 +03:00
|
|
|
instance Ca.MonadCatch (ConcIO t) where
|
|
|
|
catch = catch
|
2015-02-12 16:31:48 +03:00
|
|
|
|
2015-02-12 22:15:07 +03:00
|
|
|
instance Ca.MonadThrow (ConcIO t) where
|
2015-02-12 16:42:32 +03:00
|
|
|
throwM = throw
|
2015-02-12 16:31:48 +03:00
|
|
|
|
2015-02-13 20:47:04 +03:00
|
|
|
instance Ca.MonadMask (ConcIO t) where
|
|
|
|
mask = mask
|
|
|
|
uninterruptibleMask = uninterruptibleMask
|
|
|
|
|
2015-02-01 04:21:42 +03:00
|
|
|
instance IO.MonadIO (ConcIO t) where
|
2014-12-27 15:20:45 +03:00
|
|
|
liftIO = liftIO
|
|
|
|
|
2015-02-01 04:21:42 +03:00
|
|
|
instance C.MonadConc (ConcIO t) where
|
2015-02-13 03:39:27 +03:00
|
|
|
type CVar (ConcIO t) = CVar t
|
|
|
|
type STMLike (ConcIO t) = STMLike t IO IORef
|
|
|
|
type ThreadId (ConcIO t) = Int
|
2014-12-27 15:20:45 +03:00
|
|
|
|
2015-02-13 20:47:04 +03:00
|
|
|
fork = fork
|
|
|
|
forkWithUnmask = forkWithUnmask
|
|
|
|
myThreadId = myThreadId
|
|
|
|
throwTo = throwTo
|
|
|
|
newEmptyCVar = newEmptyCVar
|
|
|
|
putCVar = putCVar
|
|
|
|
tryPutCVar = tryPutCVar
|
|
|
|
readCVar = readCVar
|
|
|
|
takeCVar = takeCVar
|
|
|
|
tryTakeCVar = tryTakeCVar
|
|
|
|
atomically = atomically
|
|
|
|
_concNoTest = _concNoTest
|
2014-12-27 15:20:45 +03:00
|
|
|
|
2015-02-10 01:31:05 +03:00
|
|
|
fixed :: Fixed IO IORef (STMLike t)
|
2015-02-10 01:04:28 +03:00
|
|
|
fixed = Wrapper refIO $ unC . liftIO
|
2014-12-27 15:20:45 +03:00
|
|
|
|
2015-02-01 04:21:42 +03:00
|
|
|
-- | The concurrent variable type used with the 'ConcIO' monad. These
|
|
|
|
-- behave the same as @Conc@'s @CVar@s
|
2014-12-28 01:03:37 +03:00
|
|
|
newtype CVar t a = V { unV :: R IORef a } deriving Eq
|
2014-12-27 15:20:45 +03:00
|
|
|
|
2015-02-01 04:21:42 +03:00
|
|
|
-- | Lift an 'IO' action into the 'ConcIO' monad.
|
|
|
|
liftIO :: IO a -> ConcIO t a
|
2014-12-27 15:20:45 +03:00
|
|
|
liftIO ma = C $ cont lifted where
|
|
|
|
lifted c = ALift $ c <$> ma
|
|
|
|
|
|
|
|
-- | Run the provided computation concurrently, returning the result.
|
2015-02-01 04:21:42 +03:00
|
|
|
spawn :: ConcIO t a -> ConcIO t (CVar t a)
|
2015-01-28 15:10:19 +03:00
|
|
|
spawn = C.spawn
|
2014-12-27 15:20:45 +03:00
|
|
|
|
|
|
|
-- | Block on a 'CVar' until it is full, then read from it (without
|
|
|
|
-- emptying).
|
2015-02-01 04:21:42 +03:00
|
|
|
readCVar :: CVar t a -> ConcIO t a
|
2014-12-28 01:03:37 +03:00
|
|
|
readCVar cvar = C $ cont $ AGet $ unV cvar
|
2014-12-27 15:20:45 +03:00
|
|
|
|
|
|
|
-- | Run the provided computation concurrently.
|
2015-02-13 03:39:27 +03:00
|
|
|
fork :: ConcIO t () -> ConcIO t ThreadId
|
|
|
|
fork (C ma) = C $ cont $ AFork (runCont ma $ const AStop)
|
|
|
|
|
|
|
|
-- | Get the 'ThreadId' of the current thread.
|
|
|
|
myThreadId :: ConcIO t ThreadId
|
|
|
|
myThreadId = C $ cont AMyTId
|
2014-12-27 15:20:45 +03:00
|
|
|
|
2015-02-10 01:31:05 +03:00
|
|
|
-- | Run the provided 'MonadSTM' transaction atomically. If 'retry' is
|
|
|
|
-- called, it will be blocked until any of the touched 'CTVar's have
|
|
|
|
-- been written to.
|
|
|
|
atomically :: STMLike t IO IORef a -> ConcIO t a
|
|
|
|
atomically stm = C $ cont $ AAtom stm
|
|
|
|
|
2014-12-27 15:20:45 +03:00
|
|
|
-- | Create a new empty 'CVar'.
|
2015-02-01 04:21:42 +03:00
|
|
|
newEmptyCVar :: ConcIO t (CVar t a)
|
2015-01-12 03:08:53 +03:00
|
|
|
newEmptyCVar = C $ cont lifted where
|
2015-02-03 17:14:36 +03:00
|
|
|
lifted c = ANew $ \cvid -> c <$> newEmptyCVar' cvid
|
2015-02-10 04:20:04 +03:00
|
|
|
newEmptyCVar' cvid = (\ref -> V (cvid, ref)) <$> newIORef Nothing
|
2014-12-27 15:20:45 +03:00
|
|
|
|
|
|
|
-- | Block on a 'CVar' until it is empty, then write to it.
|
2015-02-01 04:21:42 +03:00
|
|
|
putCVar :: CVar t a -> a -> ConcIO t ()
|
2014-12-28 01:03:37 +03:00
|
|
|
putCVar cvar a = C $ cont $ \c -> APut (unV cvar) a $ c ()
|
2014-12-27 15:20:45 +03:00
|
|
|
|
|
|
|
-- | Put a value into a 'CVar' if there isn't one, without blocking.
|
2015-02-01 04:21:42 +03:00
|
|
|
tryPutCVar :: CVar t a -> a -> ConcIO t Bool
|
2014-12-28 01:03:37 +03:00
|
|
|
tryPutCVar cvar a = C $ cont $ ATryPut (unV cvar) a
|
2014-12-27 15:20:45 +03:00
|
|
|
|
|
|
|
-- | Block on a 'CVar' until it is full, then read from it (with
|
|
|
|
-- emptying).
|
2015-02-01 04:21:42 +03:00
|
|
|
takeCVar :: CVar t a -> ConcIO t a
|
2014-12-28 01:03:37 +03:00
|
|
|
takeCVar cvar = C $ cont $ ATake $ unV cvar
|
2014-12-27 15:20:45 +03:00
|
|
|
|
|
|
|
-- | Read a value from a 'CVar' if there is one, without blocking.
|
2015-02-01 04:21:42 +03:00
|
|
|
tryTakeCVar :: CVar t a -> ConcIO t (Maybe a)
|
2014-12-28 01:03:37 +03:00
|
|
|
tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar
|
2014-12-27 15:20:45 +03:00
|
|
|
|
2015-02-12 16:42:32 +03:00
|
|
|
-- | Raise an exception in the 'ConcIO' monad. The exception is raised
|
|
|
|
-- when the action is run, not when it is applied. It short-citcuits
|
|
|
|
-- the rest of the computation:
|
|
|
|
--
|
|
|
|
-- > throw e >> x == throw e
|
|
|
|
throw :: Exception e => e -> ConcIO t a
|
|
|
|
throw e = C $ cont $ \_ -> AThrow (SomeException e)
|
|
|
|
|
2015-02-13 20:13:00 +03:00
|
|
|
-- | Throw an exception to the target thread. This blocks until the
|
|
|
|
-- exception is delivered, and it is just as if the target thread had
|
|
|
|
-- raised it with 'throw'. This can interrupt a blocked action.
|
|
|
|
throwTo :: Exception e => ThreadId -> e -> ConcIO t ()
|
|
|
|
throwTo tid e = C $ cont $ \c -> AThrowTo tid (SomeException e) $ c ()
|
|
|
|
|
|
|
|
-- | Raise the 'ThreadKilled' exception in the target thread. Note
|
|
|
|
-- that if the thread is prepared to catch this exception, it won't
|
|
|
|
-- actually kill it.
|
|
|
|
killThread :: ThreadId => ConcIO t ()
|
|
|
|
killThread = C.killThread
|
|
|
|
|
2015-02-12 22:15:07 +03:00
|
|
|
-- | Catch an exception raised by 'throw'. This __cannot__ catch
|
|
|
|
-- errors, such as evaluating 'undefined', or division by zero. If you
|
|
|
|
-- need that, use Control.Exception.catch and 'liftIO'.
|
|
|
|
catch :: Exception e => ConcIO t a -> (e -> ConcIO t a) -> ConcIO t a
|
2015-02-13 03:56:45 +03:00
|
|
|
catch ma h = C $ cont $ ACatching (unC . h) (unC ma)
|
2015-02-12 22:15:07 +03:00
|
|
|
|
2015-02-13 20:47:04 +03:00
|
|
|
-- | Fork a thread and call the supplied function when the thread is
|
|
|
|
-- about to terminate, with an exception or a returned value. The
|
|
|
|
-- function is called with asynchronous exceptions masked.
|
|
|
|
--
|
|
|
|
-- This function is useful for informing the parent when a child
|
|
|
|
-- terminates, for example.
|
|
|
|
forkFinally :: ConcIO t a -> (Either SomeException a -> ConcIO t ()) -> ConcIO t ThreadId
|
|
|
|
forkFinally action and_then =
|
|
|
|
mask $ \restore ->
|
|
|
|
fork $ Ca.try (restore action) >>= and_then
|
|
|
|
|
|
|
|
-- | Like 'fork', but the child thread is passed a function that can
|
|
|
|
-- be used to unmask asynchronous exceptions.
|
|
|
|
forkWithUnmask :: ((forall a. ConcIO t a -> ConcIO t a) -> ConcIO t ()) -> ConcIO t ThreadId
|
|
|
|
forkWithUnmask = error "'forkWithUnmask' not yet implemented for 'ConcIO'"
|
|
|
|
|
|
|
|
-- | Executes a computation with asynchronous exceptions
|
|
|
|
-- /masked/. That is, any thread which attempts to raise an exception
|
|
|
|
-- in the current thread with 'throwTo' will be blocked until
|
|
|
|
-- asynchronous exceptions are unmasked again.
|
|
|
|
--
|
|
|
|
-- The argument passed to mask is a function that takes as its
|
|
|
|
-- argument another function, which can be used to restore the
|
|
|
|
-- prevailing masking state within the context of the masked
|
|
|
|
-- computation.
|
|
|
|
mask :: ((forall a. ConcIO t a -> ConcIO t a) -> ConcIO t b) -> ConcIO t b
|
|
|
|
mask = error "'mask' not yet implemented for 'ConcIO'"
|
|
|
|
|
|
|
|
-- | Like 'mask', but the masked computation is not
|
|
|
|
-- interruptible. THIS SHOULD BE USED WITH GREAT CARE, because if a
|
|
|
|
-- thread executing in 'uninterruptibleMask' blocks for any reason,
|
|
|
|
-- then the thread (and possibly the program, if this is the main
|
|
|
|
-- thread) will be unresponsive and unkillable. This function should
|
|
|
|
-- only be necessary if you need to mask exceptions around an
|
|
|
|
-- interruptible operation, and you can guarantee that the
|
|
|
|
-- interruptible operation will only block for a short period of time.
|
|
|
|
uninterruptibleMask :: ((forall a. ConcIO t a -> ConcIO t a) -> ConcIO t b) -> ConcIO t b
|
|
|
|
uninterruptibleMask = error "'uninterruptibleMask' not yet implemented for 'ConcIO'"
|
|
|
|
|
2015-02-06 19:11:20 +03:00
|
|
|
-- | Run the argument in one step. If the argument fails, the whole
|
|
|
|
-- computation will fail.
|
|
|
|
_concNoTest :: ConcIO t a -> ConcIO t a
|
|
|
|
_concNoTest ma = C $ cont $ \c -> ANoTest (unC ma) c
|
|
|
|
|
2014-12-27 15:20:45 +03:00
|
|
|
-- | Run a concurrent computation with a given 'Scheduler' and initial
|
2015-02-06 18:24:47 +03:00
|
|
|
-- state, returning an failure reason on error. Also returned is the
|
|
|
|
-- final state of the scheduler, and an execution trace.
|
|
|
|
runConcIO :: Scheduler s -> s -> (forall t. ConcIO t a) -> IO (Either Failure a, s, Trace)
|
2015-02-10 01:31:05 +03:00
|
|
|
runConcIO sched s ma = runFixed fixed runTransactionIO sched s $ unC ma
|