mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-01 09:49:27 +03:00
Remove _concNoTest
It's not clear how it can be safely implemented with the possibility for relaxed memory effects to occur.
This commit is contained in:
Michael Walker
parent
10a8c5f559
commit
615535b49b
@ -204,27 +204,6 @@ class ( Applicative m, Monad m
|
||||
uninterruptibleMask :: ((forall a. m a -> m a) -> m b) -> m b
|
||||
uninterruptibleMask = Ca.uninterruptibleMask
|
||||
|
||||
-- | Runs its argument, just as if the @_concNoTest@ weren't there.
|
||||
--
|
||||
-- This function is purely for testing purposes, and indicates that
|
||||
-- it's not worth considering more than one schedule here. This is
|
||||
-- useful if you have some larger computation built up out of
|
||||
-- subcomputations which you have already got tests for: you only
|
||||
-- want to consider what's unique to the large component.
|
||||
--
|
||||
-- The test runner will report a failure if the argument fails.
|
||||
--
|
||||
-- Note that inappropriate use of @_concNoTest@ can actually
|
||||
-- /suppress/ bugs! For this reason it is recommended to use it only
|
||||
-- for things which don't make use of any state from a larger
|
||||
-- scope. As a rule-of-thumb: if you can't define it as a top-level
|
||||
-- function taking no @CVRef@, @CVar@, or @CTVar@ arguments, you
|
||||
-- probably shouldn't @_concNoTest@ it.
|
||||
--
|
||||
-- > _concNoTest x = x
|
||||
_concNoTest :: m a -> m a
|
||||
_concNoTest = id
|
||||
|
||||
-- | Does nothing.
|
||||
--
|
||||
-- This function is purely for testing purposes, and indicates that
|
||||
@ -334,7 +313,6 @@ instance MonadConc m => MonadConc (ReaderT r m) where
|
||||
fork = reader fork
|
||||
forkOn i = reader (forkOn i)
|
||||
forkWithUnmask ma = ReaderT $ \r -> forkWithUnmask (\f -> runReaderT (ma $ reader f) r)
|
||||
_concNoTest = reader _concNoTest
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
@ -367,7 +345,6 @@ instance (MonadConc m, Monoid w) => MonadConc (WL.WriterT w m) where
|
||||
fork = writerlazy fork
|
||||
forkOn i = writerlazy (forkOn i)
|
||||
forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WL.runWriterT (ma $ writerlazy f))
|
||||
_concNoTest = writerlazy _concNoTest
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
@ -400,7 +377,6 @@ instance (MonadConc m, Monoid w) => MonadConc (WS.WriterT w m) where
|
||||
fork = writerstrict fork
|
||||
forkOn i = writerstrict (forkOn i)
|
||||
forkWithUnmask ma = lift $ forkWithUnmask (\f -> fst `liftM` WS.runWriterT (ma $ writerstrict f))
|
||||
_concNoTest = writerstrict _concNoTest
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
@ -433,7 +409,6 @@ instance MonadConc m => MonadConc (SL.StateT s m) where
|
||||
fork = statelazy fork
|
||||
forkOn i = statelazy (forkOn i)
|
||||
forkWithUnmask ma = SL.StateT $ \s -> (\a -> (a,s)) `liftM` forkWithUnmask (\f -> SL.evalStateT (ma $ statelazy f) s)
|
||||
_concNoTest = statelazy _concNoTest
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
@ -466,7 +441,6 @@ instance MonadConc m => MonadConc (SS.StateT s m) where
|
||||
fork = statestrict fork
|
||||
forkOn i = statestrict (forkOn i)
|
||||
forkWithUnmask ma = SS.StateT $ \s -> (\a -> (a,s)) `liftM` forkWithUnmask (\f -> SS.evalStateT (ma $ statestrict f) s)
|
||||
_concNoTest = statestrict _concNoTest
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
@ -499,7 +473,6 @@ instance (MonadConc m, Monoid w) => MonadConc (RL.RWST r w s m) where
|
||||
fork = rwslazy fork
|
||||
forkOn i = rwslazy (forkOn i)
|
||||
forkWithUnmask ma = RL.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkWithUnmask (\f -> fst `liftM` RL.evalRWST (ma $ rwslazy f) r s)
|
||||
_concNoTest = rwslazy _concNoTest
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
@ -532,7 +505,6 @@ instance (MonadConc m, Monoid w) => MonadConc (RS.RWST r w s m) where
|
||||
fork = rwsstrict fork
|
||||
forkOn i = rwsstrict (forkOn i)
|
||||
forkWithUnmask ma = RS.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkWithUnmask (\f -> fst `liftM` RS.evalRWST (ma $ rwsstrict f) r s)
|
||||
_concNoTest = rwsstrict _concNoTest
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
|
||||
@ -423,5 +423,4 @@ showfail :: Failure -> String
|
||||
showfail Deadlock = "[deadlock]"
|
||||
showfail STMDeadlock = "[stm-deadlock]"
|
||||
showfail InternalError = "[internal-error]"
|
||||
showfail FailureInNoTest = "[_concNoTest]"
|
||||
showfail UncaughtException = "[exception]"
|
||||
|
||||
@ -51,7 +51,6 @@ module Test.DejaFu.Deterministic
|
||||
, modifyCRef
|
||||
|
||||
-- * Testing
|
||||
, _concNoTest
|
||||
, _concKnowsAbout
|
||||
, _concForgets
|
||||
, _concAllKnown
|
||||
@ -136,7 +135,6 @@ instance C.MonadConc (Conc t) where
|
||||
atomicWriteCRef = atomicWriteCRef
|
||||
modifyCRef = modifyCRef
|
||||
atomically = atomically
|
||||
_concNoTest = _concNoTest
|
||||
_concKnowsAbout = _concKnowsAbout
|
||||
_concForgets = _concForgets
|
||||
_concAllKnown = _concAllKnown
|
||||
@ -311,11 +309,6 @@ forkOn _ = fork
|
||||
getNumCapabilities :: Conc t Int
|
||||
getNumCapabilities = return 2
|
||||
|
||||
-- | Run the argument in one step. If the argument fails, the whole
|
||||
-- computation will fail.
|
||||
_concNoTest :: Conc t a -> Conc t a
|
||||
_concNoTest ma = C $ cont $ \c -> ANoTest (unC ma) c
|
||||
|
||||
-- | Record that the referenced variable is known by the current thread.
|
||||
_concKnowsAbout :: Either (CVar t a) (CTVar t (STRef t) a) -> Conc t ()
|
||||
_concKnowsAbout (Left (Var (cvarid, _))) = C $ cont $ \c -> AKnowsAbout (Left cvarid) (c ())
|
||||
|
||||
@ -55,7 +55,6 @@ module Test.DejaFu.Deterministic.IO
|
||||
, modifyCRef
|
||||
|
||||
-- * Testing
|
||||
, _concNoTest
|
||||
, _concKnowsAbout
|
||||
, _concForgets
|
||||
, _concAllKnown
|
||||
@ -140,7 +139,6 @@ instance C.MonadConc (ConcIO t) where
|
||||
atomicWriteCRef = atomicWriteCRef
|
||||
modifyCRef = modifyCRef
|
||||
atomically = atomically
|
||||
_concNoTest = _concNoTest
|
||||
_concKnowsAbout = _concKnowsAbout
|
||||
_concForgets = _concForgets
|
||||
_concAllKnown = _concAllKnown
|
||||
@ -313,11 +311,6 @@ forkOn _ = fork
|
||||
getNumCapabilities :: ConcIO t Int
|
||||
getNumCapabilities = return 2
|
||||
|
||||
-- | 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
|
||||
|
||||
-- | Record that the referenced variable is known by the current thread.
|
||||
_concKnowsAbout :: Either (CVar t a) (CTVar t IORef a) -> ConcIO t ()
|
||||
_concKnowsAbout (Left (Var (cvarid, _))) = C $ cont $ \c -> AKnowsAbout (Left cvarid) (c ())
|
||||
|
||||
@ -102,7 +102,7 @@ runThreads fixed runstm sched memtype origg origthreads idsrc ref = go idsrc []
|
||||
| isNonexistant = writeRef fixed ref (Just $ Left InternalError) >> return (g, idSource, sofar)
|
||||
| isBlocked = writeRef fixed ref (Just $ Left InternalError) >> return (g, idSource, sofar)
|
||||
| otherwise = do
|
||||
stepped <- stepThread fixed runconc runstm memtype (_continuation $ fromJust thread) idSource chosen threads wb
|
||||
stepped <- stepThread fixed runstm memtype (_continuation $ fromJust thread) idSource chosen threads wb
|
||||
case stepped of
|
||||
Right (threads', idSource', act, wb') ->
|
||||
let sofar' = (decision, alternatives, act) : sofar
|
||||
@ -132,8 +132,6 @@ runThreads fixed runstm sched memtype origg origthreads idsrc ref = go idsrc []
|
||||
((~= OnMask undefined) <$> M.lookup 0 threads) == Just True)
|
||||
isSTMLocked = isLocked 0 threads && ((~= OnCTVar []) <$> M.lookup 0 threads) == Just True
|
||||
|
||||
runconc ma i = do { (a,_,i',_) <- runFixed' fixed runstm sched SequentialConsistency g i ma; return (a,i') }
|
||||
|
||||
unblockWaitingOn tid = M.map unblock where
|
||||
unblock thrd = case _blocking thrd of
|
||||
Just (OnMask t) | t == tid -> thrd { _blocking = Nothing }
|
||||
@ -171,7 +169,6 @@ runThreads fixed runstm sched memtype origg origthreads idsrc ref = go idsrc []
|
||||
nextActions' (AMasking ms _ _) = [WillSetMasking False ms]
|
||||
nextActions' (AResetMask b1 b2 ms k) = (if b1 then WillSetMasking else WillResetMasking) b2 ms : nextActions' k
|
||||
nextActions' (ALift _) = [WillLift]
|
||||
nextActions' (ANoTest _ _) = [WillNoTest]
|
||||
nextActions' (AKnowsAbout _ k) = WillKnowsAbout : nextActions' k
|
||||
nextActions' (AForgets _ k) = WillForgets : nextActions' k
|
||||
nextActions' (AAllKnown k) = WillAllKnown : nextActions' k
|
||||
@ -183,8 +180,6 @@ runThreads fixed runstm sched memtype origg origthreads idsrc ref = go idsrc []
|
||||
-- | Run a single thread one step, by dispatching on the type of
|
||||
-- 'Action'.
|
||||
stepThread :: forall n r s. (Functor n, Monad n) => Fixed n r s
|
||||
-> (forall x. M n r s x -> IdSource -> n (Either Failure x, IdSource))
|
||||
-- ^ Run a 'MonadConc' computation atomically.
|
||||
-> (forall x. s n r x -> CTVarId -> n (Result x, CTVarId))
|
||||
-- ^ Run a 'MonadSTM' transaction atomically.
|
||||
-> MemType
|
||||
@ -200,7 +195,7 @@ stepThread :: forall n r s. (Functor n, Monad n) => Fixed n r s
|
||||
-> WriteBuffer r
|
||||
-- ^ @CRef@ write buffer
|
||||
-> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r))
|
||||
stepThread fixed runconc runstm memtype action idSource tid threads wb = case action of
|
||||
stepThread fixed runstm memtype action idSource tid threads wb = case action of
|
||||
AFork a b -> stepFork a b
|
||||
AMyTId c -> stepMyTId c
|
||||
APut ref a c -> stepPut ref a c
|
||||
@ -222,7 +217,6 @@ stepThread fixed runconc runstm memtype action idSource tid threads wb = case ac
|
||||
APopCatching a -> stepPopCatching a
|
||||
AMasking m ma c -> stepMasking m ma c
|
||||
AResetMask b1 b2 m c -> stepResetMask b1 b2 m c
|
||||
ANoTest ma a -> stepNoTest ma a
|
||||
AKnowsAbout v c -> stepKnowsAbout v c
|
||||
AForgets v c -> stepForgets v c
|
||||
AAllKnown c -> stepAllKnown c
|
||||
@ -390,14 +384,6 @@ stepThread fixed runconc runstm memtype action idSource tid threads wb = case ac
|
||||
a <- na
|
||||
return $ Right (goto a tid threads, idSource, Lift, wb)
|
||||
|
||||
-- | Run a computation atomically. If this fails, the entire thing fails.
|
||||
stepNoTest ma c = do
|
||||
(a, idSource') <- runconc ma idSource
|
||||
return $
|
||||
case a of
|
||||
Right a' -> Right (goto (c a') tid threads, idSource', NoTest, wb)
|
||||
_ -> Left FailureInNoTest
|
||||
|
||||
-- | Record that a variable is known about.
|
||||
stepKnowsAbout v c = return $ Right (knows [v] tid $ goto c tid threads, idSource, KnowsAbout, wb)
|
||||
|
||||
|
||||
@ -50,7 +50,6 @@ data Action n r s =
|
||||
| forall a. AReadRef (R r a) (a -> Action n r s)
|
||||
| forall a b. AModRef (R r a) (a -> (a, b)) (b -> Action n r s)
|
||||
| forall a. AWriteRef (R r a) a (Action n r s)
|
||||
| forall a. ANoTest (M n r s a) (a -> Action n r s)
|
||||
| forall a. AAtom (s n r a) (a -> Action n r s)
|
||||
| ANew (CVarId -> n (Action n r s))
|
||||
| ANewRef (CRefId -> n (Action n r s))
|
||||
@ -232,9 +231,6 @@ data ThreadAction =
|
||||
-- ^ 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.
|
||||
| NoTest
|
||||
-- ^ A computation annotated with '_concNoTest' was executed in a
|
||||
-- single step.
|
||||
| KnowsAbout
|
||||
-- ^ A '_concKnowsAbout' annotation was processed.
|
||||
| Forgets
|
||||
@ -319,9 +315,6 @@ data Lookahead =
|
||||
-- ^ Will 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.
|
||||
| WillNoTest
|
||||
-- ^ Will execute a computation annotated with '_concNoTest' in a
|
||||
-- single step.
|
||||
| WillKnowsAbout
|
||||
-- ^ Will process a '_concKnowsAbout' annotation.
|
||||
| WillForgets
|
||||
@ -362,9 +355,6 @@ data Failure =
|
||||
-- ^ 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.
|
||||
deriving (Eq, Show)
|
||||
|
||||
instance NFData Failure where
|
||||
|
||||
Loading…
Reference in New Issue
Block a user