mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-01 09:49:27 +03:00
Add setNumCapabilities. Closes #23.
This commit is contained in:
Michael Walker
parent
42f0132ff4
commit
efa65859b1
@ -112,6 +112,9 @@ class ( Applicative m, Monad m
|
||||
-- | Get the number of Haskell threads that can run simultaneously.
|
||||
getNumCapabilities :: m Int
|
||||
|
||||
-- | Set the number of Haskell threads that can run simultaneously.
|
||||
setNumCapabilities :: Int -> m ()
|
||||
|
||||
-- | Get the @ThreadId@ of the current thread.
|
||||
myThreadId :: m (ThreadId m)
|
||||
|
||||
@ -315,6 +318,7 @@ instance MonadConc IO where
|
||||
forkOn = C.forkOn
|
||||
forkOnWithUnmask = C.forkOnWithUnmask
|
||||
getNumCapabilities = C.getNumCapabilities
|
||||
setNumCapabilities = C.setNumCapabilities
|
||||
myThreadId = C.myThreadId
|
||||
yield = C.yield
|
||||
throwTo = C.throwTo
|
||||
@ -393,6 +397,7 @@ instance MonadConc m => MonadConc (ReaderT r m) where
|
||||
forkOnWithUnmask i ma = ReaderT $ \r -> forkOnWithUnmask i (\f -> runReaderT (ma $ reader f) r)
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
setNumCapabilities = lift . setNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
yield = lift yield
|
||||
throwTo t = lift . throwTo t
|
||||
@ -432,6 +437,7 @@ instance (MonadConc m, Monoid w) => MonadConc (WL.WriterT w m) where
|
||||
forkOnWithUnmask i ma = lift $ forkOnWithUnmask i (\f -> fst `liftM` WL.runWriterT (ma $ writerlazy f))
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
setNumCapabilities = lift . setNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
yield = lift yield
|
||||
throwTo t = lift . throwTo t
|
||||
@ -471,6 +477,7 @@ instance (MonadConc m, Monoid w) => MonadConc (WS.WriterT w m) where
|
||||
forkOnWithUnmask i ma = lift $ forkOnWithUnmask i (\f -> fst `liftM` WS.runWriterT (ma $ writerstrict f))
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
setNumCapabilities = lift . setNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
yield = lift yield
|
||||
throwTo t = lift . throwTo t
|
||||
@ -510,6 +517,7 @@ instance MonadConc m => MonadConc (SL.StateT s m) where
|
||||
forkOnWithUnmask i ma = SL.StateT $ \s -> (\a -> (a,s)) `liftM` forkOnWithUnmask i (\f -> SL.evalStateT (ma $ statelazy f) s)
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
setNumCapabilities = lift . setNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
yield = lift yield
|
||||
throwTo t = lift . throwTo t
|
||||
@ -549,6 +557,7 @@ instance MonadConc m => MonadConc (SS.StateT s m) where
|
||||
forkOnWithUnmask i ma = SS.StateT $ \s -> (\a -> (a,s)) `liftM` forkOnWithUnmask i (\f -> SS.evalStateT (ma $ statestrict f) s)
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
setNumCapabilities = lift . setNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
yield = lift yield
|
||||
throwTo t = lift . throwTo t
|
||||
@ -588,6 +597,7 @@ instance (MonadConc m, Monoid w) => MonadConc (RL.RWST r w s m) where
|
||||
forkOnWithUnmask i ma = RL.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkOnWithUnmask i (\f -> fst `liftM` RL.evalRWST (ma $ rwslazy f) r s)
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
setNumCapabilities = lift . setNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
yield = lift yield
|
||||
throwTo t = lift . throwTo t
|
||||
@ -627,6 +637,7 @@ instance (MonadConc m, Monoid w) => MonadConc (RS.RWST r w s m) where
|
||||
forkOnWithUnmask i ma = RS.RWST $ \r s -> (\a -> (a,s,mempty)) `liftM` forkOnWithUnmask i (\f -> fst `liftM` RS.evalRWST (ma $ rwsstrict f) r s)
|
||||
|
||||
getNumCapabilities = lift getNumCapabilities
|
||||
setNumCapabilities = lift . setNumCapabilities
|
||||
myThreadId = lift myThreadId
|
||||
yield = lift yield
|
||||
throwTo t = lift . throwTo t
|
||||
|
||||
@ -102,11 +102,11 @@ instance Monad n => C.MonadConc (Conc n r (STMLike n r)) where
|
||||
forkWithUnmask ma = toConc (AFork (\umask -> runCont (unC $ ma $ wrap umask) (\_ -> AStop)))
|
||||
forkOnWithUnmask _ = C.forkWithUnmask
|
||||
|
||||
-- This implementation lies and always returns 2. There is no way to
|
||||
-- verify in the computation that this is a lie, and will
|
||||
-- potentially avoid special-case behaviour for 1 capability, so it
|
||||
-- seems a sane choice.
|
||||
getNumCapabilities = return 2
|
||||
-- This implementation lies and returns 2 until a value is set. This
|
||||
-- will potentially avoid special-case behaviour for 1 capability,
|
||||
-- so it seems a sane choice.
|
||||
getNumCapabilities = toConc AGetNumCapabilities
|
||||
setNumCapabilities caps = toConc (\c -> ASetNumCapabilities caps (c ()))
|
||||
|
||||
myThreadId = toConc AMyTId
|
||||
|
||||
|
||||
@ -109,8 +109,8 @@ runFixed' fixed runstm sched memtype s idSource ma = do
|
||||
-- watch out for.
|
||||
runThreads :: (Functor n, Monad n) => Fixed n r s -> (forall x. s x -> CTVarId -> n (Result x, CTVarId))
|
||||
-> Scheduler g -> MemType -> g -> Threads n r s -> IdSource -> r (Maybe (Either Failure a)) -> n (g, IdSource, Trace')
|
||||
runThreads fixed runstm sched memtype origg origthreads idsrc ref = go idsrc [] Nothing origg origthreads emptyBuffer where
|
||||
go idSource sofar prior g threads wb
|
||||
runThreads fixed runstm sched memtype origg origthreads idsrc ref = go idsrc [] Nothing origg origthreads emptyBuffer 2 where
|
||||
go idSource sofar prior g threads wb caps
|
||||
| isTerminated = stop g
|
||||
| isDeadlocked = die g Deadlock
|
||||
| isSTMLocked = die g STMDeadlock
|
||||
@ -118,13 +118,13 @@ runThreads fixed runstm sched memtype origg origthreads idsrc ref = go idsrc []
|
||||
| isNonexistant = die g' InternalError
|
||||
| isBlocked = die g' InternalError
|
||||
| otherwise = do
|
||||
stepped <- stepThread fixed runstm memtype (_continuation $ fromJust thread) idSource chosen threads wb
|
||||
stepped <- stepThread fixed runstm memtype (_continuation $ fromJust thread) idSource chosen threads wb caps
|
||||
case stepped of
|
||||
Right (threads', idSource', act, wb') -> loop threads' idSource' act wb'
|
||||
Right (threads', idSource', act, wb', caps') -> loop threads' idSource' act wb' caps'
|
||||
|
||||
Left UncaughtException
|
||||
| chosen == 0 -> die g' UncaughtException
|
||||
| otherwise -> loop (kill chosen threads) idSource Killed wb
|
||||
| otherwise -> loop (kill chosen threads) idSource Killed wb caps
|
||||
|
||||
Left failure -> die g' failure
|
||||
|
||||
@ -189,10 +189,14 @@ stepThread :: forall n r s. (Functor n, Monad n) => Fixed n r s
|
||||
-- ^ Current state of threads
|
||||
-> WriteBuffer r
|
||||
-- ^ @CRef@ write buffer
|
||||
-> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r))
|
||||
stepThread fixed runstm memtype action idSource tid threads wb = case action of
|
||||
-> Int
|
||||
-- ^ The number of capabilities
|
||||
-> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))
|
||||
stepThread fixed runstm memtype action idSource tid threads wb caps = case action of
|
||||
AFork a b -> stepFork a b
|
||||
AMyTId c -> stepMyTId c
|
||||
AGetNumCapabilities c -> stepGetNumCapabilities c
|
||||
ASetNumCapabilities i c -> stepSetNumCapabilities i c
|
||||
AYield c -> stepYield c
|
||||
ANewVar c -> stepNewVar c
|
||||
APutVar var a c -> stepPutVar var a c
|
||||
@ -225,13 +229,19 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of
|
||||
|
||||
where
|
||||
-- | Start a new thread, assigning it the next 'ThreadId'
|
||||
stepFork a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid, wb) where
|
||||
stepFork a b = return $ Right (goto (b newtid) tid threads', idSource', Fork newtid, wb, caps) where
|
||||
threads' = launch tid newtid a threads
|
||||
(idSource', newtid) = nextTId idSource
|
||||
|
||||
-- | Get the 'ThreadId' of the current thread
|
||||
stepMyTId c = simple (goto (c tid) tid threads) MyThreadId
|
||||
|
||||
-- | Get the number of capabilities
|
||||
stepGetNumCapabilities c = simple (goto (c caps) tid threads) $ GetNumCapabilities caps
|
||||
|
||||
-- | Set the number of capabilities
|
||||
stepSetNumCapabilities i c = return $ Right (goto c tid threads, idSource, SetNumCapabilities i, wb, i)
|
||||
|
||||
-- | Yield the current thread
|
||||
stepYield c = simple (goto c tid threads) Yield
|
||||
|
||||
@ -300,13 +310,13 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of
|
||||
TotalStoreOrder -> do
|
||||
let (ThreadId tid') = tid
|
||||
wb' <- bufferWrite fixed wb tid' cref a tid
|
||||
return $ Right (goto c tid threads, idSource, WriteRef crid, wb')
|
||||
return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)
|
||||
|
||||
-- Add to buffer using cref id
|
||||
PartialStoreOrder -> do
|
||||
let (CRefId crid') = crid
|
||||
wb' <- bufferWrite fixed wb crid' cref a tid
|
||||
return $ Right (goto c tid threads, idSource, WriteRef crid, wb')
|
||||
return $ Right (goto c tid threads, idSource, WriteRef crid, wb', caps)
|
||||
|
||||
-- | Perform a compare-and-swap on a @CRef@.
|
||||
stepCasRef cref@(CRef (crid, _)) tick a c = synchronised $ do
|
||||
@ -326,7 +336,7 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of
|
||||
-- Commit using the cref id.
|
||||
PartialStoreOrder -> commitWrite fixed wb c'
|
||||
|
||||
return $ Right (threads, idSource, CommitRef t c, wb')
|
||||
return $ Right (threads, idSource, CommitRef t c, wb', caps)
|
||||
|
||||
-- | Run a STM transaction atomically.
|
||||
stepAtom stm c = synchronised $ do
|
||||
@ -336,12 +346,12 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of
|
||||
Success readen written val
|
||||
| any (<oldctvid) readen || any (<oldctvid) written ->
|
||||
let (threads', woken) = wake (OnCTVar written) threads
|
||||
in return $ Right (knows (map Right written) tid $ goto (c val) tid threads', idSource { _nextCTVId = newctvid }, STM woken, wb)
|
||||
in return $ Right (knows (map Right written) tid $ goto (c val) tid threads', idSource { _nextCTVId = newctvid }, STM woken, wb, caps)
|
||||
| otherwise ->
|
||||
return $ Right (knows (map Right written) tid $ goto (c val) tid threads, idSource { _nextCTVId = newctvid }, FreshSTM, wb)
|
||||
return $ Right (knows (map Right written) tid $ goto (c val) tid threads, idSource { _nextCTVId = newctvid }, FreshSTM, wb, caps)
|
||||
Retry touched ->
|
||||
let threads' = block (OnCTVar touched) tid threads
|
||||
in return $ Right (threads', idSource { _nextCTVId = newctvid }, BlockedSTM, wb)
|
||||
in return $ Right (threads', idSource { _nextCTVId = newctvid }, BlockedSTM, wb, caps)
|
||||
Exception e -> stepThrow e
|
||||
|
||||
-- | Run a subcomputation in an exception-catching context.
|
||||
@ -386,7 +396,7 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of
|
||||
stepMasking :: MaskingState
|
||||
-> ((forall b. M n r s b -> M n r s b) -> M n r s a)
|
||||
-> (a -> Action n r s)
|
||||
-> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r))
|
||||
-> n (Either Failure (Threads n r s, IdSource, ThreadAction, WriteBuffer r, Int))
|
||||
stepMasking m ma c = simple threads' $ SetMasking False m where
|
||||
a = runCont (ma umask) (AResetMask False False m' . c)
|
||||
|
||||
@ -406,14 +416,14 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of
|
||||
let (idSource', newcvid) = nextCVId idSource
|
||||
ref <- newRef fixed Nothing
|
||||
let cvar = CVar (newcvid, ref)
|
||||
return $ Right (knows [Left newcvid] tid $ goto (c cvar) tid threads, idSource', NewVar newcvid, wb)
|
||||
return $ Right (knows [Left newcvid] tid $ goto (c cvar) tid threads, idSource', NewVar newcvid, wb, caps)
|
||||
|
||||
-- | Create a new @CRef@, using the next 'CRefId'.
|
||||
stepNewRef a c = do
|
||||
let (idSource', newcrid) = nextCRId idSource
|
||||
ref <- newRef fixed (M.empty, 0, a)
|
||||
let cref = CRef (newcrid, ref)
|
||||
return $ Right (goto (c cref) tid threads, idSource', NewRef newcrid, wb)
|
||||
return $ Right (goto (c cref) tid threads, idSource', NewRef newcrid, wb, caps)
|
||||
|
||||
-- | Lift an action from the underlying monad into the @Conc@
|
||||
-- computation.
|
||||
@ -438,7 +448,7 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of
|
||||
|
||||
-- | Helper for actions which don't touch the 'IdSource' or
|
||||
-- 'WriteBuffer'
|
||||
simple threads' act = return $ Right (threads', idSource, act, wb)
|
||||
simple threads' act = return $ Right (threads', idSource, act, wb, caps)
|
||||
|
||||
-- | Helper for actions impose a write barrier.
|
||||
synchronised ma = do
|
||||
@ -446,7 +456,7 @@ stepThread fixed runstm memtype action idSource tid threads wb = case action of
|
||||
res <- ma
|
||||
|
||||
return $ case res of
|
||||
Right (threads', idSource', act', _) -> Right (threads', idSource', act', emptyBuffer)
|
||||
Right (threads', idSource', act', _, caps') -> Right (threads', idSource', act', emptyBuffer, caps')
|
||||
_ -> res
|
||||
|
||||
-- | Helper function for wrapping up exceptions.
|
||||
|
||||
@ -86,6 +86,9 @@ data Action n r s =
|
||||
AFork ((forall b. M n r s b -> M n r s b) -> Action n r s) (ThreadId -> Action n r s)
|
||||
| AMyTId (ThreadId -> Action n r s)
|
||||
|
||||
| AGetNumCapabilities (Int -> Action n r s)
|
||||
| ASetNumCapabilities Int (Action n r s)
|
||||
|
||||
| forall a. ANewVar (CVar r a -> Action n r s)
|
||||
| forall a. APutVar (CVar r a) a (Action n r s)
|
||||
| forall a. ATryPutVar (CVar r a) a (Bool -> Action n r s)
|
||||
@ -242,6 +245,10 @@ data ThreadAction =
|
||||
-- ^ Start a new thread.
|
||||
| MyThreadId
|
||||
-- ^ Get the 'ThreadId' of the current thread.
|
||||
| GetNumCapabilities Int
|
||||
-- ^ Get the number of Haskell threads that can run simultaneously.
|
||||
| SetNumCapabilities Int
|
||||
-- ^ Set the number of Haskell threads that can run simultaneously.
|
||||
| Yield
|
||||
-- ^ Yield the current thread.
|
||||
| NewVar CVarId
|
||||
@ -328,6 +335,8 @@ data ThreadAction =
|
||||
|
||||
instance NFData ThreadAction where
|
||||
rnf (Fork t) = rnf t
|
||||
rnf (GetNumCapabilities i) = rnf i
|
||||
rnf (SetNumCapabilities i) = rnf i
|
||||
rnf (NewVar c) = rnf c
|
||||
rnf (PutVar c ts) = rnf (c, ts)
|
||||
rnf (BlockedPutVar c) = rnf c
|
||||
@ -359,6 +368,12 @@ data Lookahead =
|
||||
-- ^ Will start a new thread.
|
||||
| WillMyThreadId
|
||||
-- ^ Will get the 'ThreadId'.
|
||||
| WillGetNumCapabilities
|
||||
-- ^ Will get the number of Haskell threads that can run
|
||||
-- simultaneously.
|
||||
| WillSetNumCapabilities Int
|
||||
-- ^ Will set the number of Haskell threads that can run
|
||||
-- simultaneously.
|
||||
| WillYield
|
||||
-- ^ Will yield the current thread.
|
||||
| WillNewVar
|
||||
@ -428,6 +443,7 @@ data Lookahead =
|
||||
deriving (Eq, Show)
|
||||
|
||||
instance NFData Lookahead where
|
||||
rnf (WillSetNumCapabilities i) = rnf i
|
||||
rnf (WillPutVar c) = rnf c
|
||||
rnf (WillTryPutVar c) = rnf c
|
||||
rnf (WillReadVar c) = rnf c
|
||||
@ -451,6 +467,8 @@ lookahead :: Action n r s -> NonEmpty Lookahead
|
||||
lookahead = unsafeToNonEmpty . lookahead' where
|
||||
lookahead' (AFork _ _) = [WillFork]
|
||||
lookahead' (AMyTId _) = [WillMyThreadId]
|
||||
lookahead' (AGetNumCapabilities _) = [WillGetNumCapabilities]
|
||||
lookahead' (ASetNumCapabilities i k) = WillSetNumCapabilities i : lookahead' k
|
||||
lookahead' (ANewVar _) = [WillNewVar]
|
||||
lookahead' (APutVar (CVar (c, _)) _ k) = WillPutVar c : lookahead' k
|
||||
lookahead' (ATryPutVar (CVar (c, _)) _ _) = [WillTryPutVar c]
|
||||
|
||||
@ -304,6 +304,9 @@ dependent _ _ (_, Lift) (_, Lift) = True
|
||||
dependent _ _ (_, ThrowTo t) (t2, a) = t == t2 && a /= Stop
|
||||
dependent _ _ (t2, a) (_, ThrowTo t) = t == t2 && a /= Stop
|
||||
dependent _ _ (_, STM _) (_, STM _) = True
|
||||
dependent _ _ (_, GetNumCapabilities a) (_, SetNumCapabilities b) = a /= b
|
||||
dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b
|
||||
dependent _ _ (_, SetNumCapabilities a) (_, SetNumCapabilities b) = a /= b
|
||||
dependent memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify d2)
|
||||
|
||||
-- | Variant of 'dependent' to handle 'ThreadAction''s
|
||||
@ -312,6 +315,9 @@ dependent' _ _ (_, Lift) (_, WillLift) = True
|
||||
dependent' _ _ (_, ThrowTo t) (t2, a) = t == t2 && a /= WillStop
|
||||
dependent' _ _ (t2, a) (_, WillThrowTo t) = t == t2 && a /= Stop
|
||||
dependent' _ _ (_, STM _) (_, WillSTM) = True
|
||||
dependent' _ _ (_, GetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b
|
||||
dependent' _ _ (_, SetNumCapabilities a) (_, WillGetNumCapabilities) = True
|
||||
dependent' _ _ (_, SetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b
|
||||
dependent' memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify' d2)
|
||||
|
||||
-- | Check if two 'ActionType's are dependent. Note that this is not
|
||||
|
||||
@ -39,6 +39,8 @@ tests = test
|
||||
, testDejafu excCatchAll "excCatchAll" $ gives' [(True, True)]
|
||||
, testDejafu excSTM "excSTM" $ gives' [True]
|
||||
|
||||
, testDejafu capsGet "capsGet" $ gives' [True]
|
||||
, testDejafu capsSet "capsSet" $ gives' [True]
|
||||
]
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -219,3 +221,17 @@ excSTM :: MonadConc m => m Bool
|
||||
excSTM = catchArithException
|
||||
(atomically $ throwSTM Overflow)
|
||||
(\_ -> return True)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Capabilities
|
||||
|
||||
-- | Check that the capabilities are consistent when retrieved.
|
||||
capsGet :: MonadConc m => m Bool
|
||||
capsGet = (==) <$> getNumCapabilities <*> getNumCapabilities
|
||||
|
||||
-- | Check that the capabilities can be set.
|
||||
capsSet :: MonadConc m => m Bool
|
||||
capsSet = do
|
||||
caps <- getNumCapabilities
|
||||
setNumCapabilities $ caps + 1
|
||||
(== caps + 1) <$> getNumCapabilities
|
||||
|
||||
Loading…
Reference in New Issue
Block a user