mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-11-29 11:23:43 +03:00
Implement supportsBoundThreads in terms of supportsBoundThreads
This commit is contained in:
parent
959dafbdc1
commit
a34bfbb666
@ -83,7 +83,8 @@ runConcurrency invariants forSnapshot sched memtype g idsrc caps ma = do
|
||||
}
|
||||
(c, ref) <- runRefCont AStop (Just . Right) (runModelConc ma)
|
||||
let threads0 = launch' Unmasked initialThread (const c) (cThreads ctx)
|
||||
threads <- (if C.rtsSupportsBoundThreads then makeBound initialThread else pure) threads0
|
||||
sbt <- C.supportsBoundThreads
|
||||
threads <- (if sbt then makeBound initialThread else pure) threads0
|
||||
res <- runThreads forSnapshot sched memtype ref ctx { cThreads = threads }
|
||||
killAllThreads (finalContext res)
|
||||
pure res
|
||||
@ -101,7 +102,8 @@ runConcurrencyWithSnapshot sched memtype ctx restore ma = do
|
||||
let threads0 = M.delete initialThread (cThreads ctx)
|
||||
let threads1 = launch' Unmasked initialThread (const c) threads0
|
||||
let boundThreads = M.filter (isJust . _bound) threads1
|
||||
threads2 <- (if C.rtsSupportsBoundThreads then makeBound initialThread else pure) threads1
|
||||
sbt <- C.supportsBoundThreads
|
||||
threads2 <- (if sbt then makeBound initialThread else pure) threads1
|
||||
threads3 <- foldrM makeBound threads2 (M.keys boundThreads)
|
||||
restore threads3
|
||||
res <- runThreads False sched memtype ref ctx { cThreads = threads3 }
|
||||
@ -291,6 +293,14 @@ stepThread _ _ _ _ tid (AForkOS n a b) = \ctx@Context{..} -> do
|
||||
, const (pure ())
|
||||
)
|
||||
|
||||
-- check if we support bound threads
|
||||
stepThread _ _ _ _ tid (ASupportsBoundThreads c) = \ctx@Context{..} -> do
|
||||
sbt <- C.supportsBoundThreads
|
||||
pure ( Succeeded ctx { cThreads = goto (c sbt) tid cThreads }
|
||||
, SupportsBoundThreads sbt
|
||||
, const (pure ())
|
||||
)
|
||||
|
||||
-- check if the current thread is bound
|
||||
stepThread _ _ _ _ tid (AIsBound c) = \ctx@Context{..} -> do
|
||||
let isBound = isJust . _bound $ elookup tid cThreads
|
||||
|
@ -136,6 +136,8 @@ data ModelTicket a = ModelTicket
|
||||
data Action n =
|
||||
AFork String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)
|
||||
| AForkOS String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)
|
||||
|
||||
| ASupportsBoundThreads (Bool -> Action n)
|
||||
| AIsBound (Bool -> Action n)
|
||||
| AMyTId (ThreadId -> Action n)
|
||||
|
||||
@ -182,6 +184,7 @@ data Action n =
|
||||
lookahead :: Action n -> Lookahead
|
||||
lookahead (AFork _ _ _) = WillFork
|
||||
lookahead (AForkOS _ _ _) = WillForkOS
|
||||
lookahead (ASupportsBoundThreads _) = WillSupportsBoundThreads
|
||||
lookahead (AIsBound _) = WillIsCurrentThreadBound
|
||||
lookahead (AMyTId _) = WillMyThreadId
|
||||
lookahead (AGetNumCapabilities _) = WillGetNumCapabilities
|
||||
|
@ -92,10 +92,14 @@ instance (pty ~ Basic, Monad n) => C.MonadConc (Program pty n) where
|
||||
|
||||
forkWithUnmaskN n ma = ModelConc (AFork n (\umask -> runModelConc (ma umask) (\_ -> AStop (pure ()))))
|
||||
forkOnWithUnmaskN n _ = C.forkWithUnmaskN n
|
||||
forkOSWithUnmaskN n ma
|
||||
| C.rtsSupportsBoundThreads =
|
||||
|
||||
supportsBoundThreads = ModelConc ASupportsBoundThreads
|
||||
|
||||
forkOSWithUnmaskN n ma = C.supportsBoundThreads >>= \case
|
||||
True ->
|
||||
ModelConc (AForkOS n (\umask -> runModelConc (ma umask) (\_ -> AStop (pure ()))))
|
||||
| otherwise = fail "RTS doesn't support multiple OS threads (use ghc -threaded when linking)"
|
||||
False ->
|
||||
fail "RTS doesn't support multiple OS threads (use ghc -threaded when linking)"
|
||||
|
||||
isCurrentThreadBound = ModelConc AIsBound
|
||||
|
||||
|
@ -165,6 +165,7 @@ tvarsRead act = S.fromList $ case act of
|
||||
rewind :: ThreadAction -> Lookahead
|
||||
rewind (Fork _) = WillFork
|
||||
rewind (ForkOS _) = WillForkOS
|
||||
rewind (SupportsBoundThreads _) = WillSupportsBoundThreads
|
||||
rewind (IsCurrentThreadBound _) = WillIsCurrentThreadBound
|
||||
rewind MyThreadId = WillMyThreadId
|
||||
rewind (GetNumCapabilities _) = WillGetNumCapabilities
|
||||
|
@ -116,6 +116,8 @@ data ThreadAction =
|
||||
-- ^ Start a new thread.
|
||||
| ForkOS ThreadId
|
||||
-- ^ Start a new bound thread.
|
||||
| SupportsBoundThreads Bool
|
||||
-- ^ Check if bound threads are supported.
|
||||
| IsCurrentThreadBound Bool
|
||||
-- ^ Check if the current thread is bound.
|
||||
| MyThreadId
|
||||
@ -206,6 +208,7 @@ data ThreadAction =
|
||||
instance NFData ThreadAction where
|
||||
rnf (Fork t) = rnf t
|
||||
rnf (ForkOS t) = rnf t
|
||||
rnf (SupportsBoundThreads b) = rnf b
|
||||
rnf (IsCurrentThreadBound b) = rnf b
|
||||
rnf MyThreadId = ()
|
||||
rnf (GetNumCapabilities i) = rnf i
|
||||
@ -252,6 +255,8 @@ data Lookahead =
|
||||
-- ^ Will start a new thread.
|
||||
| WillForkOS
|
||||
-- ^ Will start a new bound thread.
|
||||
| WillSupportsBoundThreads
|
||||
-- ^ Will check if bound threads are supported.
|
||||
| WillIsCurrentThreadBound
|
||||
-- ^ Will check if the current thread is bound.
|
||||
| WillMyThreadId
|
||||
@ -331,6 +336,7 @@ data Lookahead =
|
||||
instance NFData Lookahead where
|
||||
rnf WillFork = ()
|
||||
rnf WillForkOS = ()
|
||||
rnf WillSupportsBoundThreads = ()
|
||||
rnf WillIsCurrentThreadBound = ()
|
||||
rnf WillMyThreadId = ()
|
||||
rnf WillGetNumCapabilities = ()
|
||||
|
Loading…
Reference in New Issue
Block a user