mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-18 19:11:37 +03:00
Implement catching exceptions
This commit is contained in:
parent
9bd781c697
commit
97611ff5b5
@ -347,7 +347,8 @@ findFailures2 p xs = findFailures xs 0 [] where
|
||||
|
||||
-- | Pretty-print a failure
|
||||
showfail :: Failure -> String
|
||||
showfail Deadlock = "[deadlock]"
|
||||
showfail STMDeadlock = "[stm-deadlock]"
|
||||
showfail InternalError = "[internal-error]"
|
||||
showfail FailureInNoTest = "[_concNoTest]"
|
||||
showfail Deadlock = "[deadlock]"
|
||||
showfail STMDeadlock = "[stm-deadlock]"
|
||||
showfail InternalError = "[internal-error]"
|
||||
showfail FailureInNoTest = "[_concNoTest]"
|
||||
showfail UncaughtException = "[exception]"
|
||||
|
@ -17,6 +17,7 @@ module Test.DejaFu.Deterministic
|
||||
, spawn
|
||||
, atomically
|
||||
, throw
|
||||
, catch
|
||||
|
||||
-- * Communication: CVars
|
||||
, CVar
|
||||
@ -43,7 +44,6 @@ module Test.DejaFu.Deterministic
|
||||
|
||||
import Control.Applicative (Applicative(..), (<$>))
|
||||
import Control.Exception (Exception, SomeException(..))
|
||||
import Control.Monad.Catch (MonadCatch(..), MonadThrow(..))
|
||||
import Control.Monad.Cont (cont, runCont)
|
||||
import Control.Monad.ST (ST, runST)
|
||||
import Control.State (Wrapper(..), refST)
|
||||
@ -52,6 +52,7 @@ import Test.DejaFu.Deterministic.Internal
|
||||
import Test.DejaFu.Deterministic.Schedule
|
||||
import Test.DejaFu.STM (STMLike, runTransactionST)
|
||||
|
||||
import qualified Control.Monad.Catch as Ca
|
||||
import qualified Control.Monad.Conc.Class as C
|
||||
|
||||
-- | The @Conc@ monad itself. This uses the same
|
||||
@ -60,10 +61,10 @@ import qualified Control.Monad.Conc.Class as C
|
||||
-- monad.
|
||||
newtype Conc t a = C { unC :: M (ST t) (STRef t) (STMLike t) a } deriving (Functor, Applicative, Monad)
|
||||
|
||||
instance MonadCatch (Conc t) where
|
||||
catch = error "Exceptions not yet handled in Conc."
|
||||
instance Ca.MonadCatch (Conc t) where
|
||||
catch = catch
|
||||
|
||||
instance MonadThrow (Conc t) where
|
||||
instance Ca.MonadThrow (Conc t) where
|
||||
throwM = throw
|
||||
|
||||
instance C.MonadConc (Conc t) where
|
||||
@ -141,6 +142,12 @@ tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar
|
||||
throw :: Exception e => e -> Conc t a
|
||||
throw e = C $ cont $ \_ -> AThrow (SomeException e)
|
||||
|
||||
-- | 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 'ConcIO'.
|
||||
catch :: Exception e => Conc t a -> (e -> Conc t a) -> Conc t a
|
||||
catch ma h = C $ cont $ ACatching (\e -> unC $ h e) (unC ma)
|
||||
|
||||
-- | Run the argument in one step. If the argument fails, the whole
|
||||
-- computation will fail.
|
||||
_concNoTest :: Conc t a -> Conc t a
|
||||
|
@ -21,6 +21,7 @@ module Test.DejaFu.Deterministic.IO
|
||||
, spawn
|
||||
, atomically
|
||||
, throw
|
||||
, catch
|
||||
|
||||
-- * Communication: CVars
|
||||
, CVar
|
||||
@ -47,7 +48,6 @@ module Test.DejaFu.Deterministic.IO
|
||||
|
||||
import Control.Applicative (Applicative(..), (<$>))
|
||||
import Control.Exception (Exception, SomeException(..))
|
||||
import Control.Monad.Catch (MonadCatch(..), MonadThrow(..))
|
||||
import Control.Monad.Cont (cont, runCont)
|
||||
import Control.State (Wrapper(..), refIO)
|
||||
import Data.IORef (IORef, newIORef)
|
||||
@ -55,16 +55,17 @@ import Test.DejaFu.Deterministic.Internal
|
||||
import Test.DejaFu.Deterministic.Schedule
|
||||
import Test.DejaFu.STM (STMLike, runTransactionIO)
|
||||
|
||||
import qualified Control.Monad.Catch as Ca
|
||||
import qualified Control.Monad.Conc.Class as C
|
||||
import qualified Control.Monad.IO.Class as IO
|
||||
|
||||
-- | The 'IO' variant of Test.DejaFu.Deterministic's @Conc@ monad.
|
||||
newtype ConcIO t a = C { unC :: M IO IORef (STMLike t) a } deriving (Functor, Applicative, Monad)
|
||||
|
||||
instance MonadCatch (ConcIO t) where
|
||||
catch = error "Exceptions not yet handled in ConcIO."
|
||||
instance Ca.MonadCatch (ConcIO t) where
|
||||
catch = catch
|
||||
|
||||
instance MonadThrow (ConcIO t) where
|
||||
instance Ca.MonadThrow (ConcIO t) where
|
||||
throwM = throw
|
||||
|
||||
instance IO.MonadIO (ConcIO t) where
|
||||
@ -146,6 +147,12 @@ tryTakeCVar cvar = C $ cont $ ATryTake $ unV cvar
|
||||
throw :: Exception e => e -> ConcIO t a
|
||||
throw e = C $ cont $ \_ -> AThrow (SomeException e)
|
||||
|
||||
-- | 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
|
||||
catch ma h = C $ cont $ ACatching (\e -> unC $ h e) (unC ma)
|
||||
|
||||
-- | Run the argument in one step. If the argument fails, the whole
|
||||
-- computation will fail.
|
||||
_concNoTest :: ConcIO t a -> ConcIO t a
|
||||
|
@ -6,8 +6,8 @@
|
||||
module Test.DejaFu.Deterministic.Internal where
|
||||
|
||||
import Control.DeepSeq (NFData(..))
|
||||
import Control.Exception (Exception, SomeException(..), fromException)
|
||||
import Control.Monad (liftM, when)
|
||||
import Control.Exception (SomeException)
|
||||
import Control.Monad.Cont (Cont, runCont)
|
||||
import Control.State
|
||||
import Data.List (intersect)
|
||||
@ -48,6 +48,7 @@ data Action n r s =
|
||||
| ANew (CVarId -> n (Action n r s))
|
||||
| ALift (n (Action n r s))
|
||||
| AThrow SomeException
|
||||
| forall a e. Exception e => ACatching (e -> M n r s a) (M n r s a) (a -> Action n r s)
|
||||
| AStop
|
||||
|
||||
-- | Every live thread has a unique identitifer.
|
||||
@ -130,12 +131,12 @@ data ThreadAction =
|
||||
| NoTest
|
||||
-- ^ A computation annotated with '_concNoTest' was executed in a
|
||||
-- single step.
|
||||
| PushHandler
|
||||
-- ^ Add a new exception handler.
|
||||
| PopHandler
|
||||
-- ^ Remove the most recent exception handler.
|
||||
| Catching
|
||||
-- ^ Register a new exception handler
|
||||
| Throw
|
||||
-- ^ Throw an exception.
|
||||
| Killed
|
||||
-- ^ Killed by an uncaught exception.
|
||||
| Lift
|
||||
-- ^ Lift an action from the underlying monad. Note that the
|
||||
-- penultimate action in a trace will always be a @Lift@, this is an
|
||||
@ -168,6 +169,8 @@ data Failure =
|
||||
-- ^ The computation became blocked indefinitely on @CVar@s.
|
||||
| STMDeadlock
|
||||
-- ^ The computation became blocked indefinitely on @CTVar@s.
|
||||
| UncaughtException
|
||||
-- ^ An uncaught exception bubbled to the top of the computation.
|
||||
| FailureInNoTest
|
||||
-- ^ A computation annotated with '_concNoTest' produced a failure,
|
||||
-- rather than a result.
|
||||
@ -191,7 +194,7 @@ runFixed' fixed runstm sched s idSource ma = do
|
||||
ref <- newRef (wref fixed) Nothing
|
||||
|
||||
let c = ma >>= liftN fixed . writeRef (wref fixed) ref . Just . Right
|
||||
let threads = M.fromList [(0, (runCont c $ const AStop, Nothing))]
|
||||
let threads = M.fromList [(0, (runCont c $ const AStop, Nothing, []))]
|
||||
|
||||
(s', idSource', trace) <- runThreads fixed runstm sched s threads idSource ref
|
||||
out <- readRef (wref fixed) ref
|
||||
@ -205,14 +208,24 @@ runFixed' fixed runstm sched s idSource ma = do
|
||||
data BlockedOn = OnCVarFull CVarId | OnCVarEmpty CVarId | OnCTVar [CTVarId] deriving Eq
|
||||
|
||||
-- | Determine if a thread is blocked in a certainw ay.
|
||||
(~=) :: (a, Maybe BlockedOn) -> BlockedOn -> Bool
|
||||
(_, Just (OnCVarFull _)) ~= (OnCVarFull _) = True
|
||||
(_, Just (OnCVarEmpty _)) ~= (OnCVarEmpty _) = True
|
||||
(_, Just (OnCTVar _)) ~= (OnCTVar _) = True
|
||||
(~=) :: (a, Maybe BlockedOn, b) -> BlockedOn -> Bool
|
||||
(_, Just (OnCVarFull _), _) ~= (OnCVarFull _) = True
|
||||
(_, Just (OnCVarEmpty _), _) ~= (OnCVarEmpty _) = True
|
||||
(_, Just (OnCTVar _), _) ~= (OnCTVar _) = True
|
||||
_ ~= _ = False
|
||||
|
||||
-- | Threads are represented as a tuple of (next action, is blocked).
|
||||
type Threads n r s = Map ThreadId (Action n r s, Maybe BlockedOn)
|
||||
-- | Threads are represented as a tuple of (next action, is blocked, handler stack).
|
||||
type Threads n r s = Map ThreadId (Action n r s, Maybe BlockedOn, [Handler n r s])
|
||||
|
||||
-- | An exception handler.
|
||||
data Handler n r s = forall e. Exception e => Handler (e -> Action n r s)
|
||||
|
||||
-- | Propagate an exception upwards, finding the closest handler
|
||||
-- which can deal with it.
|
||||
propagate :: SomeException -> [Handler n r s] -> Maybe (Action n r s, [Handler n r s])
|
||||
propagate _ [] = Nothing
|
||||
propagate e (Handler h:hs) = maybe (propagate e hs) (\act -> Just (act, hs)) $ fmap h e' where
|
||||
e' = fromException e
|
||||
|
||||
-- | The number of ID parameters was getting a bit unwieldy, so this
|
||||
-- hides them all away.
|
||||
@ -252,20 +265,27 @@ runThreads fixed runstm sched origg origthreads idsrc ref = go idsrc [] (-1) ori
|
||||
| isNonexistant = writeRef (wref fixed) ref (Just $ Left InternalError) >> return (g, idSource, sofar)
|
||||
| isBlocked = writeRef (wref fixed) ref (Just $ Left InternalError) >> return (g, idSource, sofar)
|
||||
| otherwise = do
|
||||
stepped <- stepThread fixed runconc runstm (fst $ fromJust thread) idSource chosen threads
|
||||
stepped <- stepThread fixed runconc runstm ((\(a,_,_) -> a) $ fromJust thread) idSource chosen threads
|
||||
case stepped of
|
||||
Right (threads', idSource', act) ->
|
||||
let sofar' = (decision, alternatives, act) : sofar
|
||||
in go idSource' sofar' chosen g' threads'
|
||||
|
||||
Left UncaughtException
|
||||
| chosen == 0 -> writeRef (wref fixed) ref (Just $ Left UncaughtException) >> return (g, idSource, sofar)
|
||||
| otherwise ->
|
||||
let sofar' = (decision, alternatives, Killed) : sofar
|
||||
threads' = kill chosen threads
|
||||
in go idSource sofar' chosen g' threads'
|
||||
|
||||
Left failure -> writeRef (wref fixed) ref (Just $ Left failure) >> return (g, idSource, sofar)
|
||||
|
||||
where
|
||||
(chosen, g') = if prior == -1 then (0, g) else sched g prior $ head runnable' :| tail runnable'
|
||||
runnable' = M.keys runnable
|
||||
runnable = M.filter (isNothing . snd) threads
|
||||
runnable = M.filter (isNothing . (\(_,b,_) -> b)) threads
|
||||
thread = M.lookup chosen threads
|
||||
isBlocked = isJust . snd $ fromJust thread
|
||||
isBlocked = isJust . (\(_,b,_) -> b) $ fromJust thread
|
||||
isNonexistant = isNothing thread
|
||||
isTerminated = 0 `notElem` M.keys threads
|
||||
isDeadlocked = M.null runnable && (((~= OnCVarFull undefined) `fmap` M.lookup 0 threads) == Just True ||
|
||||
@ -311,6 +331,7 @@ stepThread fixed runconc runstm action idSource tid threads = case action of
|
||||
ANew na -> stepNew na
|
||||
ALift na -> stepLift na
|
||||
AThrow e -> stepThrow e
|
||||
ACatching h ma c -> stepCatching h ma c
|
||||
ANoTest ma a -> stepNoTest ma a
|
||||
AStop -> stepStop
|
||||
|
||||
@ -351,20 +372,32 @@ stepThread fixed runconc runstm action idSource tid threads = case action of
|
||||
-- | Run a STM transaction atomically.
|
||||
stepAtom stm c = do
|
||||
(res, newctvid) <- runstm stm (_nextCTVId idSource)
|
||||
return . Right $
|
||||
case res of
|
||||
Success touched val ->
|
||||
let (threads', woken) = wake (OnCTVar touched) threads
|
||||
in (goto (c val) tid threads', idSource { _nextCTVId = newctvid }, STM woken)
|
||||
Retry touched ->
|
||||
let threads' = block (OnCTVar touched) tid threads
|
||||
in (threads', idSource { _nextCTVId = newctvid }, BlockedSTM)
|
||||
in (threads', lastcvid, newctvid, lasttid, BlockedSTM)
|
||||
Exception e -> stepThrow e
|
||||
case res of
|
||||
Success touched val ->
|
||||
let (threads', woken) = wake (OnCTVar touched) threads
|
||||
in return $ Right (goto (c val) tid threads', idSource { _nextCTVId = newctvid }, STM woken)
|
||||
Retry touched ->
|
||||
let threads' = block (OnCTVar touched) tid threads
|
||||
in return $ Right (threads', idSource { _nextCTVId = newctvid }, BlockedSTM)
|
||||
Exception e -> stepThrow e
|
||||
|
||||
-- | Run a subcomputation in an exception-catching context.
|
||||
stepCatching h ma c = do
|
||||
let a = runCont ma $ c
|
||||
let e = \exc -> runCont (h exc) c
|
||||
|
||||
let threads' = M.alter (\(Just (_, Nothing, hs)) -> Just (a, Nothing, Handler e:hs)) tid threads
|
||||
|
||||
return $ Right (threads', idSource, Catching)
|
||||
|
||||
-- | Throw an exception, and propagate it to the appropriate
|
||||
-- handler.
|
||||
stepThrow _ = error "Exceptions not yet handled in stepThread"
|
||||
stepThrow e = return $
|
||||
case propagate e . (\(_,_,c) -> c) . fromJust $ M.lookup tid threads of
|
||||
Just (act, hs) ->
|
||||
let threads' = M.alter (\(Just (_, Nothing, _)) -> Just (act, Nothing, hs)) tid threads
|
||||
in Right (threads', idSource, Throw)
|
||||
Nothing -> Left UncaughtException
|
||||
|
||||
-- | Create a new @CVar@, using the next 'CVarId'.
|
||||
stepNew na = do
|
||||
@ -439,11 +472,11 @@ readFromCVar emptying blocking (cvid, ref) c fixed threadid threads = do
|
||||
|
||||
-- | Replace the @Action@ of a thread.
|
||||
goto :: Action n r s -> ThreadId -> Threads n r s -> Threads n r s
|
||||
goto a = M.alter $ \(Just (_, b)) -> Just (a, b)
|
||||
goto a = M.alter $ \(Just (_, b, hs)) -> Just (a, b, hs)
|
||||
|
||||
-- | Start a thread with the given ID. This must not already be in use!
|
||||
launch :: ThreadId -> Action n r s -> Threads n r s -> Threads n r s
|
||||
launch tid a = M.insert tid (a, Nothing)
|
||||
launch tid a = M.insert tid (a, Nothing, [])
|
||||
|
||||
-- | Kill a thread.
|
||||
kill :: ThreadId -> Threads n r s -> Threads n r s
|
||||
@ -452,17 +485,17 @@ kill = M.delete
|
||||
-- | Block a thread.
|
||||
block :: BlockedOn -> ThreadId -> Threads n r s -> Threads n r s
|
||||
block blockedOn = M.alter doBlock where
|
||||
doBlock (Just (a, _)) = Just (a, Just blockedOn)
|
||||
doBlock (Just (a, _, hs)) = Just (a, Just blockedOn, hs)
|
||||
|
||||
-- | Unblock all threads waiting on the appropriate block. For 'CTVar'
|
||||
-- blocks, this will wake all threads waiting on at least one of the
|
||||
-- given 'CTVar's.
|
||||
wake :: BlockedOn -> Threads n r s -> (Threads n r s, [ThreadId])
|
||||
wake blockedOn threads = (M.map unblock threads, M.keys $ M.filter isBlocked threads) where
|
||||
unblock thread@(a, _)
|
||||
| isBlocked thread = (a, Nothing)
|
||||
unblock thread@(a, _, hs)
|
||||
| isBlocked thread = (a, Nothing, hs)
|
||||
| otherwise = thread
|
||||
|
||||
isBlocked (_, theblock) = case (theblock, blockedOn) of
|
||||
isBlocked (_, theblock, _) = case (theblock, blockedOn) of
|
||||
(Just (OnCTVar ctvids), OnCTVar blockedOn') -> ctvids `intersect` blockedOn' /= []
|
||||
_ -> theblock == Just blockedOn
|
||||
|
Loading…
Reference in New Issue
Block a user