{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
module Test.DejaFu.Conc.Internal.Threading where
import Control.Exception (Exception, MaskingState(..),
SomeException, fromException)
import Data.List (intersect)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Maybe (isJust)
import GHC.Stack (HasCallStack)
import Test.DejaFu.Conc.Internal.Common
import Test.DejaFu.Internal
import Test.DejaFu.Types
type Threads n = Map ThreadId (Thread n)
data Thread n = Thread
{ Thread n -> Action n
_continuation :: Action n
, Thread n -> Maybe BlockedOn
_blocking :: Maybe BlockedOn
, Thread n -> [Handler n]
_handlers :: [Handler n]
, Thread n -> MaskingState
_masking :: MaskingState
, Thread n -> Maybe (BoundThread n (Action n))
_bound :: Maybe (BoundThread n (Action n))
}
mkthread :: Action n -> Thread n
mkthread :: Action n -> Thread n
mkthread Action n
c = Action n
-> Maybe BlockedOn
-> [Handler n]
-> MaskingState
-> Maybe (BoundThread n (Action n))
-> Thread n
forall (n :: * -> *).
Action n
-> Maybe BlockedOn
-> [Handler n]
-> MaskingState
-> Maybe (BoundThread n (Action n))
-> Thread n
Thread Action n
c Maybe BlockedOn
forall a. Maybe a
Nothing [] MaskingState
Unmasked Maybe (BoundThread n (Action n))
forall a. Maybe a
Nothing
data BlockedOn = OnMVarFull MVarId | OnMVarEmpty MVarId | OnTVar [TVarId] | OnMask ThreadId deriving BlockedOn -> BlockedOn -> Bool
(BlockedOn -> BlockedOn -> Bool)
-> (BlockedOn -> BlockedOn -> Bool) -> Eq BlockedOn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BlockedOn -> BlockedOn -> Bool
$c/= :: BlockedOn -> BlockedOn -> Bool
== :: BlockedOn -> BlockedOn -> Bool
$c== :: BlockedOn -> BlockedOn -> Bool
Eq
(~=) :: Thread n -> BlockedOn -> Bool
Thread n
thread ~= :: Thread n -> BlockedOn -> Bool
~= BlockedOn
theblock = case (Thread n -> Maybe BlockedOn
forall (n :: * -> *). Thread n -> Maybe BlockedOn
_blocking Thread n
thread, BlockedOn
theblock) of
(Just (OnMVarFull MVarId
_), OnMVarFull MVarId
_) -> Bool
True
(Just (OnMVarEmpty MVarId
_), OnMVarEmpty MVarId
_) -> Bool
True
(Just (OnTVar [TVarId]
_), OnTVar [TVarId]
_) -> Bool
True
(Just (OnMask ThreadId
_), OnMask ThreadId
_) -> Bool
True
(Maybe BlockedOn, BlockedOn)
_ -> Bool
False
data Handler n = forall e. Exception e => Handler MaskingState (e -> Action n)
propagate :: HasCallStack => SomeException -> ThreadId -> Threads n -> Maybe (Threads n)
propagate :: SomeException -> ThreadId -> Threads n -> Maybe (Threads n)
propagate SomeException
e ThreadId
tid Threads n
threads = (MaskingState, Action n, [Handler n]) -> Threads n
raise ((MaskingState, Action n, [Handler n]) -> Threads n)
-> Maybe (MaskingState, Action n, [Handler n]) -> Maybe (Threads n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Handler n] -> Maybe (MaskingState, Action n, [Handler n])
forall (n :: * -> *).
[Handler n] -> Maybe (MaskingState, Action n, [Handler n])
propagate' [Handler n]
handlers where
handlers :: [Handler n]
handlers = Thread n -> [Handler n]
forall (n :: * -> *). Thread n -> [Handler n]
_handlers (ThreadId -> Threads n -> Thread n
forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
tid Threads n
threads)
raise :: (MaskingState, Action n, [Handler n]) -> Threads n
raise (MaskingState
ms, Action n
act, [Handler n]
hs) = MaskingState
-> Action n -> [Handler n] -> ThreadId -> Threads n -> Threads n
forall (n :: * -> *).
HasCallStack =>
MaskingState
-> Action n -> [Handler n] -> ThreadId -> Threads n -> Threads n
except MaskingState
ms Action n
act [Handler n]
hs ThreadId
tid Threads n
threads
propagate' :: [Handler n] -> Maybe (MaskingState, Action n, [Handler n])
propagate' [] = Maybe (MaskingState, Action n, [Handler n])
forall a. Maybe a
Nothing
propagate' (Handler MaskingState
ms e -> Action n
h:[Handler n]
hs) = Maybe (MaskingState, Action n, [Handler n])
-> (Action n -> Maybe (MaskingState, Action n, [Handler n]))
-> Maybe (Action n)
-> Maybe (MaskingState, Action n, [Handler n])
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Handler n] -> Maybe (MaskingState, Action n, [Handler n])
propagate' [Handler n]
hs) (\Action n
act -> (MaskingState, Action n, [Handler n])
-> Maybe (MaskingState, Action n, [Handler n])
forall a. a -> Maybe a
Just (MaskingState
ms, Action n
act, [Handler n]
hs)) (Maybe (Action n) -> Maybe (MaskingState, Action n, [Handler n]))
-> Maybe (Action n) -> Maybe (MaskingState, Action n, [Handler n])
forall a b. (a -> b) -> a -> b
$ e -> Action n
h (e -> Action n) -> Maybe e -> Maybe (Action n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeException -> Maybe e
forall e. Exception e => SomeException -> Maybe e
fromException SomeException
e
interruptible :: Thread n -> Bool
interruptible :: Thread n -> Bool
interruptible Thread n
thread =
Thread n -> MaskingState
forall (n :: * -> *). Thread n -> MaskingState
_masking Thread n
thread MaskingState -> MaskingState -> Bool
forall a. Eq a => a -> a -> Bool
== MaskingState
Unmasked Bool -> Bool -> Bool
||
(Thread n -> MaskingState
forall (n :: * -> *). Thread n -> MaskingState
_masking Thread n
thread MaskingState -> MaskingState -> Bool
forall a. Eq a => a -> a -> Bool
== MaskingState
MaskedInterruptible Bool -> Bool -> Bool
&& Maybe BlockedOn -> Bool
forall a. Maybe a -> Bool
isJust (Thread n -> Maybe BlockedOn
forall (n :: * -> *). Thread n -> Maybe BlockedOn
_blocking Thread n
thread))
catching :: (Exception e, HasCallStack) => (e -> Action n) -> ThreadId -> Threads n -> Threads n
catching :: (e -> Action n) -> ThreadId -> Threads n -> Threads n
catching e -> Action n
h = (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall k v.
(Ord k, Show k, HasCallStack) =>
(v -> v) -> k -> Map k v -> Map k v
eadjust ((Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n)
-> (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall a b. (a -> b) -> a -> b
$ \Thread n
thread ->
let ms0 :: MaskingState
ms0 = Thread n -> MaskingState
forall (n :: * -> *). Thread n -> MaskingState
_masking Thread n
thread
h' :: Handler n
h' = MaskingState -> (e -> Action n) -> Handler n
forall (n :: * -> *) e.
Exception e =>
MaskingState -> (e -> Action n) -> Handler n
Handler MaskingState
ms0 e -> Action n
h
in Thread n
thread { _handlers :: [Handler n]
_handlers = Handler n
h' Handler n -> [Handler n] -> [Handler n]
forall a. a -> [a] -> [a]
: Thread n -> [Handler n]
forall (n :: * -> *). Thread n -> [Handler n]
_handlers Thread n
thread }
uncatching :: HasCallStack => ThreadId -> Threads n -> Threads n
uncatching :: ThreadId -> Threads n -> Threads n
uncatching = (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall k v.
(Ord k, Show k, HasCallStack) =>
(v -> v) -> k -> Map k v -> Map k v
eadjust ((Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n)
-> (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall a b. (a -> b) -> a -> b
$ \Thread n
thread ->
Thread n
thread { _handlers :: [Handler n]
_handlers = [Handler n] -> [Handler n]
forall a. HasCallStack => [a] -> [a]
etail (Thread n -> [Handler n]
forall (n :: * -> *). Thread n -> [Handler n]
_handlers Thread n
thread) }
except :: HasCallStack => MaskingState -> Action n -> [Handler n] -> ThreadId -> Threads n -> Threads n
except :: MaskingState
-> Action n -> [Handler n] -> ThreadId -> Threads n -> Threads n
except MaskingState
ms Action n
act [Handler n]
hs = (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall k v.
(Ord k, Show k, HasCallStack) =>
(v -> v) -> k -> Map k v -> Map k v
eadjust ((Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n)
-> (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall a b. (a -> b) -> a -> b
$ \Thread n
thread -> Thread n
thread
{ _continuation :: Action n
_continuation = Action n
act
, _masking :: MaskingState
_masking = MaskingState
ms
, _handlers :: [Handler n]
_handlers = [Handler n]
hs
, _blocking :: Maybe BlockedOn
_blocking = Maybe BlockedOn
forall a. Maybe a
Nothing
}
mask :: HasCallStack => MaskingState -> ThreadId -> Threads n -> Threads n
mask :: MaskingState -> ThreadId -> Threads n -> Threads n
mask MaskingState
ms = (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall k v.
(Ord k, Show k, HasCallStack) =>
(v -> v) -> k -> Map k v -> Map k v
eadjust ((Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n)
-> (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall a b. (a -> b) -> a -> b
$ \Thread n
thread -> Thread n
thread { _masking :: MaskingState
_masking = MaskingState
ms }
goto :: HasCallStack => Action n -> ThreadId -> Threads n -> Threads n
goto :: Action n -> ThreadId -> Threads n -> Threads n
goto Action n
a = (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall k v.
(Ord k, Show k, HasCallStack) =>
(v -> v) -> k -> Map k v -> Map k v
eadjust ((Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n)
-> (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall a b. (a -> b) -> a -> b
$ \Thread n
thread -> Thread n
thread { _continuation :: Action n
_continuation = Action n
a }
launch :: HasCallStack => ThreadId -> ThreadId -> ((forall b. ModelConc n b -> ModelConc n b) -> Action n) -> Threads n -> Threads n
launch :: ThreadId
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
launch ThreadId
parent ThreadId
tid (forall b. ModelConc n b -> ModelConc n b) -> Action n
a Threads n
threads = MaskingState
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
forall (n :: * -> *).
HasCallStack =>
MaskingState
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
launch' MaskingState
ms ThreadId
tid (forall b. ModelConc n b -> ModelConc n b) -> Action n
a Threads n
threads where
ms :: MaskingState
ms = Thread n -> MaskingState
forall (n :: * -> *). Thread n -> MaskingState
_masking (ThreadId -> Threads n -> Thread n
forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
parent Threads n
threads)
launch' :: HasCallStack => MaskingState -> ThreadId -> ((forall b. ModelConc n b -> ModelConc n b) -> Action n) -> Threads n -> Threads n
launch' :: MaskingState
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
launch' MaskingState
ms ThreadId
tid (forall b. ModelConc n b -> ModelConc n b) -> Action n
a = ThreadId -> Thread n -> Threads n -> Threads n
forall k v.
(Ord k, Show k, HasCallStack) =>
k -> v -> Map k v -> Map k v
einsert ThreadId
tid Thread n
thread where
thread :: Thread n
thread = Action n
-> Maybe BlockedOn
-> [Handler n]
-> MaskingState
-> Maybe (BoundThread n (Action n))
-> Thread n
forall (n :: * -> *).
Action n
-> Maybe BlockedOn
-> [Handler n]
-> MaskingState
-> Maybe (BoundThread n (Action n))
-> Thread n
Thread ((forall b. ModelConc n b -> ModelConc n b) -> Action n
a forall b. ModelConc n b -> ModelConc n b
forall (n :: * -> *) b. Program Basic n b -> Program Basic n b
umask) Maybe BlockedOn
forall a. Maybe a
Nothing [] MaskingState
ms Maybe (BoundThread n (Action n))
forall a. Maybe a
Nothing
umask :: Program Basic n b -> Program Basic n b
umask Program Basic n b
mb = Bool -> MaskingState -> Program Basic n ()
forall (n :: * -> *). Bool -> MaskingState -> Program Basic n ()
resetMask Bool
True MaskingState
Unmasked Program Basic n () -> Program Basic n b -> Program Basic n b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Program Basic n b
mb Program Basic n b -> (b -> Program Basic n b) -> Program Basic n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b
b -> Bool -> MaskingState -> Program Basic n ()
forall (n :: * -> *). Bool -> MaskingState -> Program Basic n ()
resetMask Bool
False MaskingState
ms Program Basic n () -> Program Basic n b -> Program Basic n b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> b -> Program Basic n b
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
b
resetMask :: Bool -> MaskingState -> Program Basic n ()
resetMask Bool
typ MaskingState
m = ((() -> Action n) -> Action n) -> Program Basic n ()
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (((() -> Action n) -> Action n) -> Program Basic n ())
-> ((() -> Action n) -> Action n) -> Program Basic n ()
forall a b. (a -> b) -> a -> b
$ \() -> Action n
k -> Bool -> Bool -> MaskingState -> Action n -> Action n
forall (n :: * -> *).
Bool -> Bool -> MaskingState -> Action n -> Action n
AResetMask Bool
typ Bool
True MaskingState
m (Action n -> Action n) -> Action n -> Action n
forall a b. (a -> b) -> a -> b
$ () -> Action n
k ()
block :: HasCallStack => BlockedOn -> ThreadId -> Threads n -> Threads n
block :: BlockedOn -> ThreadId -> Threads n -> Threads n
block BlockedOn
blockedOn = (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall k v.
(Ord k, Show k, HasCallStack) =>
(v -> v) -> k -> Map k v -> Map k v
eadjust ((Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n)
-> (Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall a b. (a -> b) -> a -> b
$ \Thread n
thread -> Thread n
thread { _blocking :: Maybe BlockedOn
_blocking = BlockedOn -> Maybe BlockedOn
forall a. a -> Maybe a
Just BlockedOn
blockedOn }
wake :: BlockedOn -> Threads n -> (Threads n, [ThreadId])
wake :: BlockedOn -> Threads n -> (Threads n, [ThreadId])
wake BlockedOn
blockedOn Threads n
threads = (Thread n -> Thread n
forall (n :: * -> *). Thread n -> Thread n
unblock (Thread n -> Thread n) -> Threads n -> Threads n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Threads n
threads, Threads n -> [ThreadId]
forall k a. Map k a -> [k]
M.keys (Threads n -> [ThreadId]) -> Threads n -> [ThreadId]
forall a b. (a -> b) -> a -> b
$ (Thread n -> Bool) -> Threads n -> Threads n
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter Thread n -> Bool
forall (n :: * -> *). Thread n -> Bool
isBlocked Threads n
threads) where
unblock :: Thread n -> Thread n
unblock Thread n
thread
| Thread n -> Bool
forall (n :: * -> *). Thread n -> Bool
isBlocked Thread n
thread = Thread n
thread { _blocking :: Maybe BlockedOn
_blocking = Maybe BlockedOn
forall a. Maybe a
Nothing }
| Bool
otherwise = Thread n
thread
isBlocked :: Thread n -> Bool
isBlocked Thread n
thread = case (Thread n -> Maybe BlockedOn
forall (n :: * -> *). Thread n -> Maybe BlockedOn
_blocking Thread n
thread, BlockedOn
blockedOn) of
(Just (OnTVar [TVarId]
tvids), OnTVar [TVarId]
blockedOn') -> [TVarId]
tvids [TVarId] -> [TVarId] -> [TVarId]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [TVarId]
blockedOn' [TVarId] -> [TVarId] -> Bool
forall a. Eq a => a -> a -> Bool
/= []
(Maybe BlockedOn
theblock, BlockedOn
_) -> Maybe BlockedOn
theblock Maybe BlockedOn -> Maybe BlockedOn -> Bool
forall a. Eq a => a -> a -> Bool
== BlockedOn -> Maybe BlockedOn
forall a. a -> Maybe a
Just BlockedOn
blockedOn
makeBound :: (MonadDejaFu n, HasCallStack)
=> n (BoundThread n (Action n)) -> ThreadId -> Threads n -> n (Threads n)
makeBound :: n (BoundThread n (Action n))
-> ThreadId -> Threads n -> n (Threads n)
makeBound n (BoundThread n (Action n))
fbt ThreadId
tid Threads n
threads = do
BoundThread n (Action n)
bt <- n (BoundThread n (Action n))
fbt
Threads n -> n (Threads n)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Thread n -> Thread n) -> ThreadId -> Threads n -> Threads n
forall k v.
(Ord k, Show k, HasCallStack) =>
(v -> v) -> k -> Map k v -> Map k v
eadjust (\Thread n
t -> Thread n
t { _bound :: Maybe (BoundThread n (Action n))
_bound = BoundThread n (Action n) -> Maybe (BoundThread n (Action n))
forall a. a -> Maybe a
Just BoundThread n (Action n)
bt }) ThreadId
tid Threads n
threads)
kill :: (MonadDejaFu n, HasCallStack) => ThreadId -> Threads n -> n (Threads n)
kill :: ThreadId -> Threads n -> n (Threads n)
kill ThreadId
tid Threads n
threads = do
let thread :: Thread n
thread = ThreadId -> Threads n -> Thread n
forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
tid Threads n
threads
n ()
-> (BoundThread n (Action n) -> n ())
-> Maybe (BoundThread n (Action n))
-> n ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> n ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) BoundThread n (Action n) -> n ()
forall (m :: * -> *) a. MonadDejaFu m => BoundThread m a -> m ()
killBoundThread (Thread n -> Maybe (BoundThread n (Action n))
forall (n :: * -> *). Thread n -> Maybe (BoundThread n (Action n))
_bound Thread n
thread)
Threads n -> n (Threads n)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ThreadId -> Threads n -> Threads n
forall k a. Ord k => k -> Map k a -> Map k a
M.delete ThreadId
tid Threads n
threads)
runLiftedAct :: MonadDejaFu n => ThreadId -> Threads n -> n (Action n) -> n (Action n)
runLiftedAct :: ThreadId -> Threads n -> n (Action n) -> n (Action n)
runLiftedAct ThreadId
tid Threads n
threads n (Action n)
ma = case Thread n -> Maybe (BoundThread n (Action n))
forall (n :: * -> *). Thread n -> Maybe (BoundThread n (Action n))
_bound (Thread n -> Maybe (BoundThread n (Action n)))
-> Maybe (Thread n) -> Maybe (BoundThread n (Action n))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ThreadId -> Threads n -> Maybe (Thread n)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ThreadId
tid Threads n
threads of
Just BoundThread n (Action n)
bt -> BoundThread n (Action n) -> n (Action n) -> n (Action n)
forall (m :: * -> *) a.
MonadDejaFu m =>
BoundThread m a -> m a -> m a
runInBoundThread BoundThread n (Action n)
bt n (Action n)
ma
Maybe (BoundThread n (Action n))
Nothing -> n (Action n)
ma