{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
#if __GLASGOW_HASKELL__ >= 908
{-# OPTIONS_GHC -Wno-x-partial #-}
#endif
module Control.Monad.IOSim.Internal
( IOSim (..)
, runIOSim
, runSimTraceST
, traceM
, traceSTM
, STM
, STMSim
, setCurrentTime
, unshareClock
, TimeoutException (..)
, EventlogEvent (..)
, EventlogMarker (..)
, IOSimThreadId
, ThreadLabel
, Labelled (..)
, SimTrace
, Trace.Trace (SimTrace, TraceMainReturn, TraceMainException, TraceDeadlock)
, SimEvent (..)
, SimResult (..)
, SimEventType (..)
, ppTrace
, ppTrace_
, ppSimEvent
, liftST
, execReadTVar
) where
import Prelude hiding (read)
import Data.Deque.Strict (Deque)
import Data.Deque.Strict qualified as Deque
import Data.Dynamic
import Data.Foldable (foldlM, toList, traverse_)
import Data.List qualified as List
import Data.List.Trace qualified as Trace
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe (mapMaybe)
import Data.OrdPSQ (OrdPSQ)
import Data.OrdPSQ qualified as PSQ
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Time (UTCTime (..), fromGregorian)
import Control.Exception (NonTermination (..), assert, throw)
import Control.Monad (join, when)
import Control.Monad.ST.Lazy
import Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST)
import Data.STRef.Lazy
import Control.Concurrent.Class.MonadSTM.TMVar
import Control.Concurrent.Class.MonadSTM.TVar hiding (TVar)
import Control.Monad.Class.MonadFork (killThread, myThreadId, throwTo)
import Control.Monad.Class.MonadSTM hiding (STM)
import Control.Monad.Class.MonadSTM.Internal (TMVarDefault (TMVar))
import Control.Monad.Class.MonadThrow hiding (getMaskingState)
import Control.Monad.Class.MonadTime
import Control.Monad.Class.MonadTimer.SI (TimeoutState (..))
import Control.Monad.IOSim.InternalTypes
import Control.Monad.IOSim.Types hiding (SimEvent (SimPOREvent),
Trace (SimPORTrace))
import Control.Monad.IOSim.Types (SimEvent)
data Thread s a = Thread {
forall s a. Thread s a -> IOSimThreadId
threadId :: !IOSimThreadId,
forall s a. Thread s a -> ThreadControl s a
threadControl :: !(ThreadControl s a),
forall s a. Thread s a -> ThreadStatus
threadStatus :: !ThreadStatus,
forall s a. Thread s a -> MaskingState
threadMasking :: !MaskingState,
forall s a. Thread s a -> [(SomeException, Labelled IOSimThreadId)]
threadThrowTo :: ![(SomeException, Labelled IOSimThreadId)],
forall s a. Thread s a -> ClockId
threadClockId :: !ClockId,
forall s a. Thread s a -> Maybe ThreadLabel
threadLabel :: Maybe ThreadLabel,
forall s a. Thread s a -> Int
threadNextTId :: !Int
}
isThreadBlocked :: Thread s a -> Bool
isThreadBlocked :: forall s a. Thread s a -> Bool
isThreadBlocked Thread s a
t = case Thread s a -> ThreadStatus
forall s a. Thread s a -> ThreadStatus
threadStatus Thread s a
t of
ThreadBlocked {} -> Bool
True
ThreadStatus
_ -> Bool
False
labelledTVarId :: TVar s a -> ST s (Labelled TVarId)
labelledTVarId :: forall s a. TVar s a -> ST s (Labelled TVarId)
labelledTVarId TVar { TVarId
tvarId :: TVarId
tvarId :: forall s a. TVar s a -> TVarId
tvarId, STRef s (Maybe ThreadLabel)
tvarLabel :: STRef s (Maybe ThreadLabel)
tvarLabel :: forall s a. TVar s a -> STRef s (Maybe ThreadLabel)
tvarLabel } = TVarId -> Maybe ThreadLabel -> Labelled TVarId
forall a. a -> Maybe ThreadLabel -> Labelled a
Labelled TVarId
tvarId (Maybe ThreadLabel -> Labelled TVarId)
-> ST s (Maybe ThreadLabel) -> ST s (Labelled TVarId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef s (Maybe ThreadLabel) -> ST s (Maybe ThreadLabel)
forall s a. STRef s a -> ST s a
readSTRef STRef s (Maybe ThreadLabel)
tvarLabel
labelledThreads :: Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
labelledThreads :: forall s a.
Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
labelledThreads Map IOSimThreadId (Thread s a)
threadMap =
(Thread s a
-> [Labelled IOSimThreadId] -> [Labelled IOSimThreadId])
-> [Labelled IOSimThreadId]
-> Map IOSimThreadId (Thread s a)
-> [Labelled IOSimThreadId]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr'
(\Thread { IOSimThreadId
threadId :: forall s a. Thread s a -> IOSimThreadId
threadId :: IOSimThreadId
threadId, Maybe ThreadLabel
threadLabel :: forall s a. Thread s a -> Maybe ThreadLabel
threadLabel :: Maybe ThreadLabel
threadLabel } ![Labelled IOSimThreadId]
acc -> IOSimThreadId -> Maybe ThreadLabel -> Labelled IOSimThreadId
forall a. a -> Maybe ThreadLabel -> Labelled a
Labelled IOSimThreadId
threadId Maybe ThreadLabel
threadLabel Labelled IOSimThreadId
-> [Labelled IOSimThreadId] -> [Labelled IOSimThreadId]
forall a. a -> [a] -> [a]
: [Labelled IOSimThreadId]
acc)
[] Map IOSimThreadId (Thread s a)
threadMap
data TimerCompletionInfo s =
Timer !(TVar s TimeoutState)
| TimerRegisterDelay !(TVar s Bool)
| TimerThreadDelay !IOSimThreadId !TimeoutId
| TimerTimeout !IOSimThreadId !TimeoutId !(TMVar (IOSim s) IOSimThreadId)
type Timeouts s = OrdPSQ TimeoutId Time (TimerCompletionInfo s)
data SimState s a = SimState {
forall s a. SimState s a -> Deque IOSimThreadId
runqueue :: !(Deque IOSimThreadId),
forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: !(Map IOSimThreadId (Thread s a)),
forall s a. SimState s a -> Time
curTime :: !Time,
forall s a. SimState s a -> Timeouts s
timers :: !(Timeouts s),
forall s a. SimState s a -> Map ClockId UTCTime
clocks :: !(Map ClockId UTCTime),
forall s a. SimState s a -> TVarId
nextVid :: !TVarId,
forall s a. SimState s a -> TimeoutId
nextTmid :: !TimeoutId
}
initialState :: SimState s a
initialState :: forall s a. SimState s a
initialState =
SimState {
runqueue :: Deque IOSimThreadId
runqueue = Deque IOSimThreadId
forall a. Monoid a => a
mempty,
threads :: Map IOSimThreadId (Thread s a)
threads = Map IOSimThreadId (Thread s a)
forall k a. Map k a
Map.empty,
curTime :: Time
curTime = DiffTime -> Time
Time DiffTime
0,
timers :: Timeouts s
timers = Timeouts s
forall k p v. OrdPSQ k p v
PSQ.empty,
clocks :: Map ClockId UTCTime
clocks = ClockId -> UTCTime -> Map ClockId UTCTime
forall k a. k -> a -> Map k a
Map.singleton ([Int] -> ClockId
ClockId []) UTCTime
epoch1970,
nextVid :: TVarId
nextVid = Int -> TVarId
TVarId Int
0,
nextTmid :: TimeoutId
nextTmid = Int -> TimeoutId
TimeoutId Int
0
}
where
epoch1970 :: UTCTime
epoch1970 = Day -> DiffTime -> UTCTime
UTCTime (Year -> Int -> Int -> Day
fromGregorian Year
1970 Int
1 Int
1) DiffTime
0
invariant :: Maybe (Thread s a) -> SimState s a -> x -> x
invariant :: forall s a x. Maybe (Thread s a) -> SimState s a -> x -> x
invariant (Just Thread s a
running) simstate :: SimState s a
simstate@SimState{Deque IOSimThreadId
runqueue :: forall s a. SimState s a -> Deque IOSimThreadId
runqueue :: Deque IOSimThreadId
runqueue,Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads,Map ClockId UTCTime
clocks :: forall s a. SimState s a -> Map ClockId UTCTime
clocks :: Map ClockId UTCTime
clocks} =
Bool -> x -> x
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not (Thread s a -> Bool
forall s a. Thread s a -> Bool
isThreadBlocked Thread s a
running))
(x -> x) -> (x -> x) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> x -> x
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
running IOSimThreadId -> Map IOSimThreadId (Thread s a) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map IOSimThreadId (Thread s a)
threads)
(x -> x) -> (x -> x) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> x -> x
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
running IOSimThreadId -> Deque IOSimThreadId -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`List.notElem` Deque IOSimThreadId
runqueue)
(x -> x) -> (x -> x) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> x -> x
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Thread s a -> ClockId
forall s a. Thread s a -> ClockId
threadClockId Thread s a
running ClockId -> Map ClockId UTCTime -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map ClockId UTCTime
clocks)
(x -> x) -> (x -> x) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Thread s a) -> SimState s a -> x -> x
forall s a x. Maybe (Thread s a) -> SimState s a -> x -> x
invariant Maybe (Thread s a)
forall a. Maybe a
Nothing SimState s a
simstate
invariant Maybe (Thread s a)
Nothing SimState{Deque IOSimThreadId
runqueue :: forall s a. SimState s a -> Deque IOSimThreadId
runqueue :: Deque IOSimThreadId
runqueue,Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads,Map ClockId UTCTime
clocks :: forall s a. SimState s a -> Map ClockId UTCTime
clocks :: Map ClockId UTCTime
clocks} =
Bool -> x -> x
forall a. (?callStack::CallStack) => Bool -> a -> a
assert ((IOSimThreadId -> Bool) -> Deque IOSimThreadId -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (IOSimThreadId -> Map IOSimThreadId (Thread s a) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map IOSimThreadId (Thread s a)
threads) Deque IOSimThreadId
runqueue)
(x -> x) -> (x -> x) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> x -> x
forall a. (?callStack::CallStack) => Bool -> a -> a
assert ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ Thread s a -> Bool
forall s a. Thread s a -> Bool
isThreadBlocked Thread s a
t Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
t IOSimThreadId -> Deque IOSimThreadId -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Deque IOSimThreadId
runqueue)
| Thread s a
t <- Map IOSimThreadId (Thread s a) -> [Thread s a]
forall k a. Map k a -> [a]
Map.elems Map IOSimThreadId (Thread s a)
threads ])
(x -> x) -> (x -> x) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> x -> x
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Deque IOSimThreadId -> [IOSimThreadId]
forall a. Deque a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Deque IOSimThreadId
runqueue [IOSimThreadId] -> [IOSimThreadId] -> Bool
forall a. Eq a => a -> a -> Bool
== [IOSimThreadId] -> [IOSimThreadId]
forall a. Eq a => [a] -> [a]
List.nub (Deque IOSimThreadId -> [IOSimThreadId]
forall a. Deque a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Deque IOSimThreadId
runqueue))
(x -> x) -> (x -> x) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> x -> x
forall a. (?callStack::CallStack) => Bool -> a -> a
assert ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ Thread s a -> ClockId
forall s a. Thread s a -> ClockId
threadClockId Thread s a
t ClockId -> Map ClockId UTCTime -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map ClockId UTCTime
clocks
| Thread s a
t <- Map IOSimThreadId (Thread s a) -> [Thread s a]
forall k a. Map k a -> [a]
Map.elems Map IOSimThreadId (Thread s a)
threads ])
timeSinceEpoch :: Time -> NominalDiffTime
timeSinceEpoch :: Time -> NominalDiffTime
timeSinceEpoch (Time DiffTime
t) = Rational -> NominalDiffTime
forall a. Fractional a => Rational -> a
fromRational (DiffTime -> Rational
forall a. Real a => a -> Rational
toRational DiffTime
t)
schedule :: forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule :: forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule !thread :: Thread s a
thread@Thread{
threadId :: forall s a. Thread s a -> IOSimThreadId
threadId = IOSimThreadId
tid,
threadControl :: forall s a. Thread s a -> ThreadControl s a
threadControl = ThreadControl SimA s b
action ControlStack s b a
ctl,
threadMasking :: forall s a. Thread s a -> MaskingState
threadMasking = MaskingState
maskst,
threadLabel :: forall s a. Thread s a -> Maybe ThreadLabel
threadLabel = Maybe ThreadLabel
tlbl
}
!simstate :: SimState s a
simstate@SimState {
Deque IOSimThreadId
runqueue :: forall s a. SimState s a -> Deque IOSimThreadId
runqueue :: Deque IOSimThreadId
runqueue,
Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads,
Timeouts s
timers :: forall s a. SimState s a -> Timeouts s
timers :: Timeouts s
timers,
Map ClockId UTCTime
clocks :: forall s a. SimState s a -> Map ClockId UTCTime
clocks :: Map ClockId UTCTime
clocks,
TVarId
nextVid :: forall s a. SimState s a -> TVarId
nextVid :: TVarId
nextVid, TimeoutId
nextTmid :: forall s a. SimState s a -> TimeoutId
nextTmid :: TimeoutId
nextTmid,
curTime :: forall s a. SimState s a -> Time
curTime = Time
time
} =
Maybe (Thread s a)
-> SimState s a -> ST s (SimTrace a) -> ST s (SimTrace a)
forall s a x. Maybe (Thread s a) -> SimState s a -> x -> x
invariant (Thread s a -> Maybe (Thread s a)
forall a. a -> Maybe a
Just Thread s a
thread) SimState s a
simstate (ST s (SimTrace a) -> ST s (SimTrace a))
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$
case SimA s b
action of
Return b
x -> case ControlStack s b a
ctl of
ControlStack s b a
MainFrame ->
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl SimEventType
EventThreadFinished
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> Labelled IOSimThreadId
-> a
-> [Labelled IOSimThreadId]
-> SimTrace a
forall a.
Time
-> Labelled IOSimThreadId
-> a
-> [Labelled IOSimThreadId]
-> SimTrace a
TraceMainReturn Time
time (IOSimThreadId -> Maybe ThreadLabel -> Labelled IOSimThreadId
forall a. a -> Maybe ThreadLabel -> Labelled a
Labelled IOSimThreadId
tid Maybe ThreadLabel
tlbl) a
b
x (Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
forall s a.
Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
labelledThreads Map IOSimThreadId (Thread s a)
threads)
ControlStack s b a
ForkFrame -> do
!SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Terminated Thread s a
thread SimState s a
simstate
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl SimEventType
EventThreadFinished
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Terminated)
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace
MaskFrame b -> SimA s c
k MaskingState
maskst' ControlStack s c a
ctl' -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k x) ctl'
, threadMasking = maskst' }
!SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Interruptable Thread s a
thread' SimState s a
simstate
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (MaskingState -> SimEventType
EventMask MaskingState
maskst')
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Interruptable)
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace
CatchFrame e -> SimA s b
_handler b -> SimA s c
k ControlStack s c a
ctl' -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k x) ctl' }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
TimeoutFrame TimeoutId
tmid TMVar (IOSim s) IOSimThreadId
lock Maybe b -> SimA s c
k ControlStack s c a
ctl' -> do
Bool
v <- TMVar (IOSim s) IOSimThreadId -> IOSimThreadId -> ST s Bool
forall s a. TMVar (IOSim s) a -> a -> ST s Bool
execTryPutTMVar TMVar (IOSim s) IOSimThreadId
lock IOSimThreadId
forall a. (?callStack::CallStack) => a
undefined
let
threadAction :: IOSim s ()
threadAction :: IOSim s ()
threadAction =
if Bool
v then TimeoutId -> IOSim s ()
forall s. TimeoutId -> IOSim s ()
unsafeUnregisterTimeout TimeoutId
tmid
else STM (IOSim s) IOSimThreadId -> IOSim s IOSimThreadId
forall a. (?callStack::CallStack) => STM (IOSim s) a -> IOSim s a
forall (m :: * -> *) a.
(MonadSTM m, ?callStack::CallStack) =>
STM m a -> m a
atomically (TMVar (IOSim s) IOSimThreadId -> STM (IOSim s) IOSimThreadId
forall a. TMVar (IOSim s) a -> STM (IOSim s) a
forall (m :: * -> *) a. MonadSTM m => TMVar m a -> STM m a
takeTMVar TMVar (IOSim s) IOSimThreadId
lock) IOSim s IOSimThreadId
-> (IOSimThreadId -> IOSim s ()) -> IOSim s ()
forall a b. IOSim s a -> (a -> IOSim s b) -> IOSim s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ThreadId (IOSim s) -> IOSim s ()
IOSimThreadId -> IOSim s ()
forall (m :: * -> *). MonadFork m => ThreadId m -> m ()
killThread
thread' :: Thread s a
thread' =
Thread s a
thread { threadControl =
ThreadControl (case threadAction of
IOSim forall r. (() -> SimA s r) -> SimA s r
k' -> (() -> SimA s c) -> SimA s c
forall r. (() -> SimA s r) -> SimA s r
k' (\() -> Maybe b -> SimA s c
k (b -> Maybe b
forall a. a -> Maybe a
Just b
x)))
ctl'
}
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
DelayFrame TimeoutId
tmid SimA s c
k ControlStack s c a
ctl' -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl' }
timers' :: Timeouts s
timers' = TimeoutId -> Timeouts s -> Timeouts s
forall k p v. (Ord k, Ord p) => k -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.delete TimeoutId
tmid Timeouts s
timers
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { timers = timers' }
Throw SomeException
e -> case SomeException
-> Thread s a
-> Timeouts s
-> (Either Bool (Thread s a), Timeouts s)
forall s a.
SomeException
-> Thread s a
-> Timeouts s
-> (Either Bool (Thread s a), Timeouts s)
unwindControlStack SomeException
e Thread s a
thread Timeouts s
timers of
(Right thread' :: Thread s a
thread'@Thread { threadMasking :: forall s a. Thread s a -> MaskingState
threadMasking = MaskingState
maskst' }, Timeouts s
timers'') -> do
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { timers = timers'' }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (SomeException -> SimEventType
EventThrow SomeException
e) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (MaskingState -> SimEventType
EventMask MaskingState
maskst') SimTrace a
trace)
(Left Bool
isMain, Timeouts s
timers'')
| Bool
isMain ->
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (SomeException -> SimEventType
EventThrow SomeException
e) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (SomeException -> SimEventType
EventThreadUnhandled SomeException
e) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
Time
-> Labelled IOSimThreadId
-> SomeException
-> [Labelled IOSimThreadId]
-> SimTrace a
forall a.
Time
-> Labelled IOSimThreadId
-> SomeException
-> [Labelled IOSimThreadId]
-> SimTrace a
TraceMainException Time
time (IOSimThreadId -> Maybe ThreadLabel -> Labelled IOSimThreadId
forall a. a -> Maybe ThreadLabel -> Labelled a
Labelled IOSimThreadId
tid Maybe ThreadLabel
tlbl) SomeException
e (Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
forall s a.
Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
labelledThreads Map IOSimThreadId (Thread s a)
threads))
| Bool
otherwise -> do
!SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Terminated Thread s a
thread SimState s a
simstate { timers = timers'' }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (SomeException -> SimEventType
EventThrow SomeException
e)
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (SomeException -> SimEventType
EventThreadUnhandled SomeException
e)
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Terminated)
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace
Catch SimA s a1
action' e -> SimA s a1
handler a1 -> SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl action'
(CatchFrame handler k ctl) }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
Evaluate a1
expr a1 -> SimA s b
k -> do
Either SomeException a1
mbWHNF <- IO (Either SomeException a1) -> ST s (Either SomeException a1)
forall a s. IO a -> ST s a
unsafeIOToST (IO (Either SomeException a1) -> ST s (Either SomeException a1))
-> IO (Either SomeException a1) -> ST s (Either SomeException a1)
forall a b. (a -> b) -> a -> b
$ IO a1 -> IO (Either SomeException a1)
forall e a. Exception e => IO a -> IO (Either e a)
forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> m (Either e a)
try (IO a1 -> IO (Either SomeException a1))
-> IO a1 -> IO (Either SomeException a1)
forall a b. (a -> b) -> a -> b
$ a1 -> IO a1
forall a. a -> IO a
forall (m :: * -> *) a. MonadEvaluate m => a -> m a
evaluate a1
expr
case Either SomeException a1
mbWHNF of
Left SomeException
e -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Throw e) ctl }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
Right a1
whnf -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k whnf) ctl }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
Say ThreadLabel
msg SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (ThreadLabel -> SimEventType
EventSay ThreadLabel
msg) SimTrace a
trace)
Output Dynamic
x SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Dynamic -> SimEventType
EventLog Dynamic
x) SimTrace a
trace)
LiftST ST s a1
st a1 -> SimA s b
k -> do
a1
x <- ST s a1 -> ST s a1
forall s a. ST s a -> ST s a
strictToLazyST ST s a1
st
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k x) ctl }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
GetMonoTime Time -> SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k time) ctl }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
GetWallTime UTCTime -> SimA s b
k -> do
let !clockid :: ClockId
clockid = Thread s a -> ClockId
forall s a. Thread s a -> ClockId
threadClockId Thread s a
thread
!clockoff :: UTCTime
clockoff = Map ClockId UTCTime
clocks Map ClockId UTCTime -> ClockId -> UTCTime
forall k a. Ord k => Map k a -> k -> a
Map.! ClockId
clockid
!walltime :: UTCTime
walltime = Time -> NominalDiffTime
timeSinceEpoch Time
time NominalDiffTime -> UTCTime -> UTCTime
`addUTCTime` UTCTime
clockoff
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k walltime) ctl }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
SetWallTime UTCTime
walltime' SimA s b
k -> do
let !clockid :: ClockId
clockid = Thread s a -> ClockId
forall s a. Thread s a -> ClockId
threadClockId Thread s a
thread
!clockoff :: UTCTime
clockoff = Map ClockId UTCTime
clocks Map ClockId UTCTime -> ClockId -> UTCTime
forall k a. Ord k => Map k a -> k -> a
Map.! ClockId
clockid
!walltime :: UTCTime
walltime = Time -> NominalDiffTime
timeSinceEpoch Time
time NominalDiffTime -> UTCTime -> UTCTime
`addUTCTime` UTCTime
clockoff
!clockoff' :: UTCTime
clockoff' = NominalDiffTime -> UTCTime -> UTCTime
addUTCTime (UTCTime -> UTCTime -> NominalDiffTime
diffUTCTime UTCTime
walltime' UTCTime
walltime) UTCTime
clockoff
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
!simstate' :: SimState s a
simstate' = SimState s a
simstate { clocks = Map.insert clockid clockoff' clocks }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate'
UnshareClock SimA s b
k -> do
let !clockid :: ClockId
clockid = Thread s a -> ClockId
forall s a. Thread s a -> ClockId
threadClockId Thread s a
thread
!clockoff :: UTCTime
clockoff = Map ClockId UTCTime
clocks Map ClockId UTCTime -> ClockId -> UTCTime
forall k a. Ord k => Map k a -> k -> a
Map.! ClockId
clockid
!clockid' :: ClockId
clockid' = let ThreadId [Int]
i = IOSimThreadId
tid in [Int] -> ClockId
ClockId [Int]
i
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl
, threadClockId = clockid' }
!simstate' :: SimState s a
simstate' = SimState s a
simstate { clocks = Map.insert clockid' clockoff clocks }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate'
StartTimeout DiffTime
d SimA s a1
_ Maybe a1 -> SimA s b
_ | DiffTime
d DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
0 ->
ThreadLabel -> ST s (SimTrace a)
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"schedule: StartTimeout: Impossible happened"
StartTimeout DiffTime
d SimA s a1
action' Maybe a1 -> SimA s b
k -> do
!TMVarDefault (IOSim s) IOSimThreadId
lock <- TVar (IOSim s) (Maybe IOSimThreadId)
-> TMVarDefault (IOSim s) IOSimThreadId
TVar s (Maybe IOSimThreadId)
-> TMVarDefault (IOSim s) IOSimThreadId
forall (m :: * -> *) a. TVar m (Maybe a) -> TMVarDefault m a
TMVar (TVar s (Maybe IOSimThreadId)
-> TMVarDefault (IOSim s) IOSimThreadId)
-> ST s (TVar s (Maybe IOSimThreadId))
-> ST s (TMVarDefault (IOSim s) IOSimThreadId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVarId
-> Maybe ThreadLabel
-> Maybe IOSimThreadId
-> ST s (TVar s (Maybe IOSimThreadId))
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar TVarId
nextVid (ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just (ThreadLabel -> Maybe ThreadLabel)
-> ThreadLabel -> Maybe ThreadLabel
forall a b. (a -> b) -> a -> b
$! ThreadLabel
"lock-" ThreadLabel -> ThreadLabel -> ThreadLabel
forall a. [a] -> [a] -> [a]
++ TimeoutId -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show TimeoutId
nextTmid) Maybe IOSimThreadId
forall a. Maybe a
Nothing
let !expiry :: Time
expiry = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
!timers' :: Timeouts s
timers' = TimeoutId
-> Time -> TimerCompletionInfo s -> Timeouts s -> Timeouts s
forall k p v.
(Ord k, Ord p) =>
k -> p -> v -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.insert TimeoutId
nextTmid Time
expiry (IOSimThreadId
-> TimeoutId
-> TMVar (IOSim s) IOSimThreadId
-> TimerCompletionInfo s
forall s.
IOSimThreadId
-> TimeoutId
-> TMVar (IOSim s) IOSimThreadId
-> TimerCompletionInfo s
TimerTimeout IOSimThreadId
tid TimeoutId
nextTmid TMVarDefault (IOSim s) IOSimThreadId
TMVar (IOSim s) IOSimThreadId
lock) Timeouts s
timers
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl =
ThreadControl action'
(TimeoutFrame nextTmid lock k ctl)
}
!SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Yield Thread s a
thread' SimState s a
simstate { timers = timers'
, nextTmid = succ nextTmid
, nextVid = succ nextVid
}
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (TimeoutId -> IOSimThreadId -> Time -> SimEventType
EventTimeoutCreated TimeoutId
nextTmid IOSimThreadId
tid Time
expiry) SimTrace a
trace)
UnregisterTimeout TimeoutId
tmid SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { timers = PSQ.delete tmid timers }
RegisterDelay DiffTime
d TVar s Bool -> SimA s b
k | DiffTime
d DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
< DiffTime
0 -> do
!TVar s Bool
tvar <- TVarId -> Maybe ThreadLabel -> Bool -> ST s (TVar s Bool)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar TVarId
nextVid
(ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just (ThreadLabel -> Maybe ThreadLabel)
-> ThreadLabel -> Maybe ThreadLabel
forall a b. (a -> b) -> a -> b
$! ThreadLabel
"<<timeout " ThreadLabel -> ThreadLabel -> ThreadLabel
forall a. [a] -> [a] -> [a]
++ Int -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show (TimeoutId -> Int
unTimeoutId TimeoutId
nextTmid) ThreadLabel -> ThreadLabel -> ThreadLabel
forall a. [a] -> [a] -> [a]
++ ThreadLabel
">>")
Bool
True
let !expiry :: Time
expiry = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k tvar) ctl }
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { nextVid = succ nextVid }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (TimeoutId -> TVarId -> Time -> SimEventType
EventRegisterDelayCreated TimeoutId
nextTmid TVarId
nextVid Time
expiry) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (TimeoutId -> SimEventType
EventRegisterDelayFired TimeoutId
nextTmid) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
SimTrace a
trace)
RegisterDelay DiffTime
d TVar s Bool -> SimA s b
k -> do
!TVar s Bool
tvar <- TVarId -> Maybe ThreadLabel -> Bool -> ST s (TVar s Bool)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar TVarId
nextVid
(ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just (ThreadLabel -> Maybe ThreadLabel)
-> ThreadLabel -> Maybe ThreadLabel
forall a b. (a -> b) -> a -> b
$! ThreadLabel
"<<timeout " ThreadLabel -> ThreadLabel -> ThreadLabel
forall a. [a] -> [a] -> [a]
++ Int -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show (TimeoutId -> Int
unTimeoutId TimeoutId
nextTmid) ThreadLabel -> ThreadLabel -> ThreadLabel
forall a. [a] -> [a] -> [a]
++ ThreadLabel
">>")
Bool
False
let !expiry :: Time
expiry = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
!timers' :: Timeouts s
timers' = TimeoutId
-> Time -> TimerCompletionInfo s -> Timeouts s -> Timeouts s
forall k p v.
(Ord k, Ord p) =>
k -> p -> v -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.insert TimeoutId
nextTmid Time
expiry (TVar s Bool -> TimerCompletionInfo s
forall s. TVar s Bool -> TimerCompletionInfo s
TimerRegisterDelay TVar s Bool
tvar) Timeouts s
timers
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k tvar) ctl }
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { timers = timers'
, nextVid = succ nextVid
, nextTmid = succ nextTmid }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl
(TimeoutId -> TVarId -> Time -> SimEventType
EventRegisterDelayCreated TimeoutId
nextTmid TVarId
nextVid Time
expiry) SimTrace a
trace)
ThreadDelay DiffTime
d SimA s b
k | DiffTime
d DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
< DiffTime
0 -> do
let !expiry :: Time
expiry = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Return ()) (DelayFrame nextTmid k ctl) }
!simstate' :: SimState s a
simstate' = SimState s a
simstate { nextTmid = succ nextTmid }
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate'
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (TimeoutId -> Time -> SimEventType
EventThreadDelay TimeoutId
nextTmid Time
expiry) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (TimeoutId -> SimEventType
EventThreadDelayFired TimeoutId
nextTmid) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
SimTrace a
trace)
ThreadDelay DiffTime
d SimA s b
k -> do
let !expiry :: Time
expiry = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
!timers' :: Timeouts s
timers' = TimeoutId
-> Time -> TimerCompletionInfo s -> Timeouts s -> Timeouts s
forall k p v.
(Ord k, Ord p) =>
k -> p -> v -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.insert TimeoutId
nextTmid Time
expiry (IOSimThreadId -> TimeoutId -> TimerCompletionInfo s
forall s. IOSimThreadId -> TimeoutId -> TimerCompletionInfo s
TimerThreadDelay IOSimThreadId
tid TimeoutId
nextTmid) Timeouts s
timers
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Return ()) (DelayFrame nextTmid k ctl) }
!SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule (BlockedReason -> Deschedule
Blocked BlockedReason
BlockedOnDelay) Thread s a
thread' SimState s a
simstate { timers = timers'
, nextTmid = succ nextTmid }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (TimeoutId -> Time -> SimEventType
EventThreadDelay TimeoutId
nextTmid Time
expiry) SimTrace a
trace)
NewTimeout DiffTime
d Timeout s -> SimA s b
k | DiffTime
d DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
< DiffTime
0 -> do
let !t :: Timeout s
t = TimeoutId -> Timeout s
forall s. TimeoutId -> Timeout s
NegativeTimeout TimeoutId
nextTmid
!expiry :: Time
expiry = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k t) ctl }
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { nextTmid = succ nextTmid }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (TimeoutId -> TVarId -> Time -> SimEventType
EventTimerCreated TimeoutId
nextTmid TVarId
nextVid Time
expiry) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (TimeoutId -> SimEventType
EventTimerCancelled TimeoutId
nextTmid) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
SimTrace a
trace)
NewTimeout DiffTime
d Timeout s -> SimA s b
k -> do
!TVar s TimeoutState
tvar <- TVarId
-> Maybe ThreadLabel -> TimeoutState -> ST s (TVar s TimeoutState)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar TVarId
nextVid
(ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just (ThreadLabel -> Maybe ThreadLabel)
-> ThreadLabel -> Maybe ThreadLabel
forall a b. (a -> b) -> a -> b
$! ThreadLabel
"<<timeout-state " ThreadLabel -> ThreadLabel -> ThreadLabel
forall a. [a] -> [a] -> [a]
++ Int -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show (TimeoutId -> Int
unTimeoutId TimeoutId
nextTmid) ThreadLabel -> ThreadLabel -> ThreadLabel
forall a. [a] -> [a] -> [a]
++ ThreadLabel
">>")
TimeoutState
TimeoutPending
let !expiry :: Time
expiry = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
!t :: Timeout s
t = TVar s TimeoutState -> TimeoutId -> Timeout s
forall s. TVar s TimeoutState -> TimeoutId -> Timeout s
Timeout TVar s TimeoutState
tvar TimeoutId
nextTmid
!timers' :: Timeouts s
timers' = TimeoutId
-> Time -> TimerCompletionInfo s -> Timeouts s -> Timeouts s
forall k p v.
(Ord k, Ord p) =>
k -> p -> v -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.insert TimeoutId
nextTmid Time
expiry (TVar s TimeoutState -> TimerCompletionInfo s
forall s. TVar s TimeoutState -> TimerCompletionInfo s
Timer TVar s TimeoutState
tvar) Timeouts s
timers
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k t) ctl }
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { timers = timers'
, nextVid = succ nextVid
, nextTmid = succ nextTmid }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (TimeoutId -> TVarId -> Time -> SimEventType
EventTimerCreated TimeoutId
nextTmid TVarId
nextVid Time
expiry) SimTrace a
trace)
CancelTimeout (Timeout TVar s TimeoutState
tvar TimeoutId
tmid) SimA s b
k -> do
let !timers' :: Timeouts s
timers' = TimeoutId -> Timeouts s -> Timeouts s
forall k p v. (Ord k, Ord p) => k -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.delete TimeoutId
tmid Timeouts s
timers
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
![SomeTVar s]
written <- StmA s () -> ST s [SomeTVar s]
forall s. StmA s () -> ST s [SomeTVar s]
execAtomically' (STM s () -> StmA s ()
forall s a. STM s a -> StmA s a
runSTM (STM s () -> StmA s ()) -> STM s () -> StmA s ()
forall a b. (a -> b) -> a -> b
$ TVar (IOSim s) TimeoutState -> TimeoutState -> STM (IOSim s) ()
forall a. TVar (IOSim s) a -> a -> STM (IOSim s) ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar TVar (IOSim s) TimeoutState
TVar s TimeoutState
tvar TimeoutState
TimeoutCancelled)
!()
_ <- (SomeTVar s -> ST s ()) -> [SomeTVar s] -> ST s ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (\(SomeTVar TVar s a
tvar') -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
commitTVar TVar s a
tvar') [SomeTVar s]
written
([IOSimThreadId]
wakeup, Map IOSimThreadId (Set (Labelled TVarId))
wokeby) <- [SomeTVar s]
-> ST
s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))
forall s.
[SomeTVar s]
-> ST
s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))
threadsUnblockedByWrites [SomeTVar s]
written
(SomeTVar s -> ST s ()) -> [SomeTVar s] -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(SomeTVar TVar s a
var) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar s a
var) [SomeTVar s]
written
let ([IOSimThreadId]
unblocked,
SimState s a
simstate') = Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
True [IOSimThreadId]
wakeup SimState s a
simstate
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate' { timers = timers' }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (TimeoutId -> SimEventType
EventTimerCancelled TimeoutId
tmid)
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany
[ (Time
time, IOSimThreadId
tid', Maybe ThreadLabel
tlbl', [Labelled TVarId] -> SimEventType
EventTxWakeup [Labelled TVarId]
vids)
| IOSimThreadId
tid' <- [IOSimThreadId]
unblocked
, let tlbl' :: Maybe ThreadLabel
tlbl' = IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
forall s a.
IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel IOSimThreadId
tid' Map IOSimThreadId (Thread s a)
threads
, let Just [Labelled TVarId]
vids = Set (Labelled TVarId) -> [Labelled TVarId]
forall a. Set a -> [a]
Set.toList (Set (Labelled TVarId) -> [Labelled TVarId])
-> Maybe (Set (Labelled TVarId)) -> Maybe [Labelled TVarId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOSimThreadId
-> Map IOSimThreadId (Set (Labelled TVarId))
-> Maybe (Set (Labelled TVarId))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IOSimThreadId
tid' Map IOSimThreadId (Set (Labelled TVarId))
wokeby ]
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace
CancelTimeout (NegativeTimeout TimeoutId
_tmid) SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
Fork IOSim s ()
a IOSimThreadId -> SimA s b
k -> do
let !nextId :: Int
nextId = Thread s a -> Int
forall s a. Thread s a -> Int
threadNextTId Thread s a
thread
!tid' :: IOSimThreadId
tid' = IOSimThreadId -> Int -> IOSimThreadId
childThreadId IOSimThreadId
tid Int
nextId
!thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k tid') ctl
, threadNextTId = succ nextId }
!thread'' :: Thread s a
thread'' = Thread { threadId :: IOSimThreadId
threadId = IOSimThreadId
tid'
, threadControl :: ThreadControl s a
threadControl = SimA s () -> ControlStack s () a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (IOSim s () -> SimA s ()
forall s a. IOSim s a -> SimA s a
runIOSim IOSim s ()
a)
ControlStack s () a
forall s a. ControlStack s () a
ForkFrame
, threadStatus :: ThreadStatus
threadStatus = ThreadStatus
ThreadRunning
, threadMasking :: MaskingState
threadMasking = Thread s a -> MaskingState
forall s a. Thread s a -> MaskingState
threadMasking Thread s a
thread
, threadThrowTo :: [(SomeException, Labelled IOSimThreadId)]
threadThrowTo = []
, threadClockId :: ClockId
threadClockId = Thread s a -> ClockId
forall s a. Thread s a -> ClockId
threadClockId Thread s a
thread
, threadLabel :: Maybe ThreadLabel
threadLabel = Maybe ThreadLabel
forall a. Maybe a
Nothing
, threadNextTId :: Int
threadNextTId = Int
1
}
!threads' :: Map IOSimThreadId (Thread s a)
threads' = IOSimThreadId
-> Thread s a
-> Map IOSimThreadId (Thread s a)
-> Map IOSimThreadId (Thread s a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IOSimThreadId
tid' Thread s a
thread'' Map IOSimThreadId (Thread s a)
threads
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { runqueue = Deque.snoc tid' runqueue
, threads = threads' }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (IOSimThreadId -> SimEventType
EventThreadForked IOSimThreadId
tid') SimTrace a
trace)
Atomically STM s a1
a a1 -> SimA s b
k ->
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> TVarId
-> StmA s a1
-> (StmTxResult s a1 -> ST s (SimTrace a))
-> ST s (SimTrace a)
forall s a c.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> TVarId
-> StmA s a
-> (StmTxResult s a -> ST s (SimTrace c))
-> ST s (SimTrace c)
execAtomically Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl TVarId
nextVid (STM s a1 -> StmA s a1
forall s a. STM s a -> StmA s a
runSTM STM s a1
a) ((StmTxResult s a1 -> ST s (SimTrace a)) -> ST s (SimTrace a))
-> (StmTxResult s a1 -> ST s (SimTrace a)) -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ \StmTxResult s a1
res ->
case StmTxResult s a1
res of
StmTxCommitted a1
x [SomeTVar s]
written [SomeTVar s]
_read [SomeTVar s]
created
[Dynamic]
tvarDynamicTraces [ThreadLabel]
tvarStringTraces TVarId
nextVid' -> do
(![IOSimThreadId]
wakeup, Map IOSimThreadId (Set (Labelled TVarId))
wokeby) <- [SomeTVar s]
-> ST
s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))
forall s.
[SomeTVar s]
-> ST
s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))
threadsUnblockedByWrites [SomeTVar s]
written
!()
_ <- (SomeTVar s -> ST s ()) -> [SomeTVar s] -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar s a
tvar) [SomeTVar s]
written
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k x) ctl }
([IOSimThreadId]
unblocked,
SimState s a
simstate') = Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
True [IOSimThreadId]
wakeup SimState s a
simstate
[Labelled TVarId]
written' <- (SomeTVar s -> ST s (Labelled TVarId))
-> [SomeTVar s] -> ST s [Labelled TVarId]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s (Labelled TVarId)
forall s a. TVar s a -> ST s (Labelled TVarId)
labelledTVarId TVar s a
tvar) [SomeTVar s]
written
[Labelled TVarId]
created' <- (SomeTVar s -> ST s (Labelled TVarId))
-> [SomeTVar s] -> ST s [Labelled TVarId]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s (Labelled TVarId)
forall s a. TVar s a -> ST s (Labelled TVarId)
labelledTVarId TVar s a
tvar) [SomeTVar s]
created
!SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Yield Thread s a
thread' SimState s a
simstate' { nextVid = nextVid' }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl ([Labelled TVarId]
-> [Labelled TVarId] -> Maybe Effect -> SimEventType
EventTxCommitted
[Labelled TVarId]
written' [Labelled TVarId]
created' Maybe Effect
forall a. Maybe a
Nothing)
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany
[ (Time
time, IOSimThreadId
tid', Maybe ThreadLabel
tlbl', [Labelled TVarId] -> SimEventType
EventTxWakeup [Labelled TVarId]
vids')
| IOSimThreadId
tid' <- [IOSimThreadId]
unblocked
, let tlbl' :: Maybe ThreadLabel
tlbl' = IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
forall s a.
IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel IOSimThreadId
tid' Map IOSimThreadId (Thread s a)
threads
, let Just [Labelled TVarId]
vids' = Set (Labelled TVarId) -> [Labelled TVarId]
forall a. Set a -> [a]
Set.toList (Set (Labelled TVarId) -> [Labelled TVarId])
-> Maybe (Set (Labelled TVarId)) -> Maybe [Labelled TVarId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOSimThreadId
-> Map IOSimThreadId (Set (Labelled TVarId))
-> Maybe (Set (Labelled TVarId))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IOSimThreadId
tid' Map IOSimThreadId (Set (Labelled TVarId))
wokeby ]
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany
[ (Time
time, IOSimThreadId
tid, Maybe ThreadLabel
tlbl, Dynamic -> SimEventType
EventLog Dynamic
tr)
| Dynamic
tr <- [Dynamic]
tvarDynamicTraces ]
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany
[ (Time
time, IOSimThreadId
tid, Maybe ThreadLabel
tlbl, ThreadLabel -> SimEventType
EventSay ThreadLabel
str)
| ThreadLabel
str <- [ThreadLabel]
tvarStringTraces ]
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl ([IOSimThreadId] -> SimEventType
EventUnblocked [IOSimThreadId]
unblocked)
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Yield)
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace
StmTxAborted [SomeTVar s]
_read SomeException
e -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Throw e) ctl }
!SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Maybe Effect -> SimEventType
EventTxAborted Maybe Effect
forall a. Maybe a
Nothing) SimTrace a
trace
StmTxBlocked [SomeTVar s]
read -> do
!()
_ <- (SomeTVar s -> ST s ()) -> [SomeTVar s] -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(SomeTVar TVar s a
tvar) -> IOSimThreadId -> TVar s a -> ST s ()
forall s a. IOSimThreadId -> TVar s a -> ST s ()
blockThreadOnTVar IOSimThreadId
tid TVar s a
tvar) [SomeTVar s]
read
[Labelled TVarId]
vids <- (SomeTVar s -> ST s (Labelled TVarId))
-> [SomeTVar s] -> ST s [Labelled TVarId]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s (Labelled TVarId)
forall s a. TVar s a -> ST s (Labelled TVarId)
labelledTVarId TVar s a
tvar) [SomeTVar s]
read
!SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule (BlockedReason -> Deschedule
Blocked BlockedReason
BlockedOnSTM) Thread s a
thread SimState s a
simstate
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl ([Labelled TVarId] -> Maybe Effect -> SimEventType
EventTxBlocked [Labelled TVarId]
vids Maybe Effect
forall a. Maybe a
Nothing)
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule (BlockedReason -> Deschedule
Blocked BlockedReason
BlockedOnSTM))
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace
GetThreadId IOSimThreadId -> SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k tid) ctl }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
LabelThread IOSimThreadId
tid' ThreadLabel
l SimA s b
k | IOSimThreadId
tid' IOSimThreadId -> IOSimThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== IOSimThreadId
tid -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl
, threadLabel = Just l }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
LabelThread IOSimThreadId
tid' ThreadLabel
l SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
threads' :: Map IOSimThreadId (Thread s a)
threads' = (Thread s a -> Thread s a)
-> IOSimThreadId
-> Map IOSimThreadId (Thread s a)
-> Map IOSimThreadId (Thread s a)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (\Thread s a
t -> Thread s a
t { threadLabel = Just l }) IOSimThreadId
tid' Map IOSimThreadId (Thread s a)
threads
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { threads = threads' }
GetMaskState MaskingState -> SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k maskst) ctl }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
SetMaskState MaskingState
maskst' IOSim s a1
action' a1 -> SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl
(runIOSim action')
(MaskFrame k maskst ctl)
, threadMasking = maskst' }
SimTrace a
trace <-
case MaskingState
maskst' of
MaskingState
Unmasked -> Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Interruptable)
(SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Interruptable Thread s a
thread' SimState s a
simstate
MaskingState
_ -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (MaskingState -> SimEventType
EventMask MaskingState
maskst')
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace
ThrowTo SomeException
e IOSimThreadId
tid' SimA s b
_ | IOSimThreadId
tid' IOSimThreadId -> IOSimThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== IOSimThreadId
tid -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Throw e) ctl }
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (SomeException -> IOSimThreadId -> SimEventType
EventThrowTo SomeException
e IOSimThreadId
tid) SimTrace a
trace)
ThrowTo SomeException
e IOSimThreadId
tid' SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
willBlock :: Bool
willBlock = case IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe (Thread s a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IOSimThreadId
tid' Map IOSimThreadId (Thread s a)
threads of
Just Thread s a
t -> Bool -> Bool
not (Thread s a -> Bool
forall s a. Thread s a -> Bool
threadInterruptible Thread s a
t)
Maybe (Thread s a)
_ -> Bool
False
if Bool
willBlock
then do
let adjustTarget :: Thread s a -> Thread s a
adjustTarget Thread s a
t = Thread s a
t { threadThrowTo = (e, Labelled tid tlbl) : threadThrowTo t }
threads' :: Map IOSimThreadId (Thread s a)
threads' = (Thread s a -> Thread s a)
-> IOSimThreadId
-> Map IOSimThreadId (Thread s a)
-> Map IOSimThreadId (Thread s a)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust Thread s a -> Thread s a
adjustTarget IOSimThreadId
tid' Map IOSimThreadId (Thread s a)
threads
!SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule (BlockedReason -> Deschedule
Blocked BlockedReason
BlockedOnThrowTo) Thread s a
thread' SimState s a
simstate { threads = threads' }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (SomeException -> IOSimThreadId -> SimEventType
EventThrowTo SomeException
e IOSimThreadId
tid')
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl SimEventType
EventThrowToBlocked
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule (BlockedReason -> Deschedule
Blocked BlockedReason
BlockedOnThrowTo))
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace
else do
let adjustTarget :: Thread s a -> Thread s a
adjustTarget t :: Thread s a
t@Thread{ threadControl :: forall s a. Thread s a -> ThreadControl s a
threadControl = ThreadControl SimA s b
_ ControlStack s b a
ctl' } =
Thread s a
t { threadControl = ThreadControl (Throw e) ctl'
, threadStatus = ThreadRunning
}
simstate' :: SimState s a
simstate'@SimState { threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads = Map IOSimThreadId (Thread s a)
threads' }
= ([IOSimThreadId], SimState s a) -> SimState s a
forall a b. (a, b) -> b
snd (Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
False [IOSimThreadId
tid'] SimState s a
simstate)
threads'' :: Map IOSimThreadId (Thread s a)
threads'' = (Thread s a -> Thread s a)
-> IOSimThreadId
-> Map IOSimThreadId (Thread s a)
-> Map IOSimThreadId (Thread s a)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust Thread s a -> Thread s a
adjustTarget IOSimThreadId
tid' Map IOSimThreadId (Thread s a)
threads'
simstate'' :: SimState s a
simstate'' = SimState s a
simstate' { threads = threads'' }
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate''
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (SomeException -> IOSimThreadId -> SimEventType
EventThrowTo SomeException
e IOSimThreadId
tid')
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace
YieldSim SimA s b
k -> do
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Yield Thread s a
thread' SimState s a
simstate
ExploreRaces SimA s b
k ->
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread{ threadControl = ThreadControl k ctl } SimState s a
simstate
Fix x -> IOSim s x
f x -> SimA s b
k -> do
STRef s x
r <- x -> ST s (STRef s x)
forall a s. a -> ST s (STRef s a)
newSTRef (NonTermination -> x
forall a e. Exception e => e -> a
throw NonTermination
NonTermination)
x
x <- ST s x -> ST s x
forall s a. ST s a -> ST s a
unsafeInterleaveST (ST s x -> ST s x) -> ST s x -> ST s x
forall a b. (a -> b) -> a -> b
$ STRef s x -> ST s x
forall s a. STRef s a -> ST s a
readSTRef STRef s x
r
let k' :: SimA s b
k' = IOSim s x -> forall r. (x -> SimA s r) -> SimA s r
forall s a. IOSim s a -> forall r. (a -> SimA s r) -> SimA s r
unIOSim (x -> IOSim s x
f x
x) ((x -> SimA s b) -> SimA s b) -> (x -> SimA s b) -> SimA s b
forall a b. (a -> b) -> a -> b
$ \x
x' ->
ST s () -> (() -> SimA s b) -> SimA s b
forall s a1 a. ST s a1 -> (a1 -> SimA s a) -> SimA s a
LiftST (ST s () -> ST s ()
forall s a. ST s a -> ST s a
lazyToStrictST (STRef s x -> x -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s x
r x
x')) (\() -> x -> SimA s b
k x
x')
thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k' ctl }
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
threadInterruptible :: Thread s a -> Bool
threadInterruptible :: forall s a. Thread s a -> Bool
threadInterruptible Thread s a
thread =
case Thread s a -> MaskingState
forall s a. Thread s a -> MaskingState
threadMasking Thread s a
thread of
MaskingState
Unmasked -> Bool
True
MaskingState
MaskedInterruptible
| Thread s a -> Bool
forall s a. Thread s a -> Bool
isThreadBlocked Thread s a
thread -> Bool
True
| Bool
otherwise -> Bool
False
MaskingState
MaskedUninterruptible -> Bool
False
deschedule :: Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule :: forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Yield !Thread s a
thread !simstate :: SimState s a
simstate@SimState{Deque IOSimThreadId
runqueue :: forall s a. SimState s a -> Deque IOSimThreadId
runqueue :: Deque IOSimThreadId
runqueue, Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads} =
let runqueue' :: Deque IOSimThreadId
runqueue' = IOSimThreadId -> Deque IOSimThreadId -> Deque IOSimThreadId
forall a. a -> Deque a -> Deque a
Deque.snoc (Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
thread) Deque IOSimThreadId
runqueue
threads' :: Map IOSimThreadId (Thread s a)
threads' = IOSimThreadId
-> Thread s a
-> Map IOSimThreadId (Thread s a)
-> Map IOSimThreadId (Thread s a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
thread) Thread s a
thread Map IOSimThreadId (Thread s a)
threads in
SimState s a -> ST s (SimTrace a)
forall s a. SimState s a -> ST s (SimTrace a)
reschedule SimState s a
simstate { runqueue = runqueue', threads = threads' }
deschedule Deschedule
Interruptable !thread :: Thread s a
thread@Thread {
threadId :: forall s a. Thread s a -> IOSimThreadId
threadId = IOSimThreadId
tid,
threadControl :: forall s a. Thread s a -> ThreadControl s a
threadControl = ThreadControl SimA s b
_ ControlStack s b a
ctl,
threadMasking :: forall s a. Thread s a -> MaskingState
threadMasking = MaskingState
Unmasked,
threadThrowTo :: forall s a. Thread s a -> [(SomeException, Labelled IOSimThreadId)]
threadThrowTo = (SomeException
e, Labelled IOSimThreadId
tid') : [(SomeException, Labelled IOSimThreadId)]
etids,
threadLabel :: forall s a. Thread s a -> Maybe ThreadLabel
threadLabel = Maybe ThreadLabel
tlbl
}
!simstate :: SimState s a
simstate@SimState{ curTime :: forall s a. SimState s a -> Time
curTime = Time
time, Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads } =
let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Throw e) ctl
, threadMasking = MaskedInterruptible
, threadThrowTo = etids }
([IOSimThreadId]
unblocked,
SimState s a
simstate') = Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
False [Labelled IOSimThreadId -> IOSimThreadId
forall a. Labelled a -> a
l_labelled Labelled IOSimThreadId
tid'] SimState s a
simstate
in do
SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate'
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Labelled IOSimThreadId -> SimEventType
EventThrowToUnmasked Labelled IOSimThreadId
tid')
(SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany [ (Time
time, IOSimThreadId
tid'', Maybe ThreadLabel
tlbl'', SimEventType
EventThrowToWakeup)
| IOSimThreadId
tid'' <- [IOSimThreadId]
unblocked
, let tlbl'' :: Maybe ThreadLabel
tlbl'' = IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
forall s a.
IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel IOSimThreadId
tid'' Map IOSimThreadId (Thread s a)
threads ]
SimTrace a
trace
deschedule Deschedule
Interruptable !Thread s a
thread !SimState s a
simstate =
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread SimState s a
simstate
deschedule (Blocked BlockedReason
_blockedReason) !thread :: Thread s a
thread@Thread { threadThrowTo :: forall s a. Thread s a -> [(SomeException, Labelled IOSimThreadId)]
threadThrowTo = (SomeException, Labelled IOSimThreadId)
_ : [(SomeException, Labelled IOSimThreadId)]
_
, threadMasking :: forall s a. Thread s a -> MaskingState
threadMasking = MaskingState
maskst } !SimState s a
simstate
| MaskingState
maskst MaskingState -> MaskingState -> Bool
forall a. Eq a => a -> a -> Bool
/= MaskingState
MaskedUninterruptible =
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Interruptable Thread s a
thread { threadMasking = Unmasked } SimState s a
simstate
deschedule (Blocked BlockedReason
blockedReason) !Thread s a
thread !simstate :: SimState s a
simstate@SimState{Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads} =
let thread' :: Thread s a
thread' = Thread s a
thread { threadStatus = ThreadBlocked blockedReason }
threads' :: Map IOSimThreadId (Thread s a)
threads' = IOSimThreadId
-> Thread s a
-> Map IOSimThreadId (Thread s a)
-> Map IOSimThreadId (Thread s a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
thread') Thread s a
thread' Map IOSimThreadId (Thread s a)
threads in
SimState s a -> ST s (SimTrace a)
forall s a. SimState s a -> ST s (SimTrace a)
reschedule SimState s a
simstate { threads = threads' }
deschedule Deschedule
Terminated !Thread s a
thread !simstate :: SimState s a
simstate@SimState{ curTime :: forall s a. SimState s a -> Time
curTime = Time
time, Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads } =
let !wakeup :: [IOSimThreadId]
wakeup = ((SomeException, Labelled IOSimThreadId) -> IOSimThreadId)
-> [(SomeException, Labelled IOSimThreadId)] -> [IOSimThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (Labelled IOSimThreadId -> IOSimThreadId
forall a. Labelled a -> a
l_labelled (Labelled IOSimThreadId -> IOSimThreadId)
-> ((SomeException, Labelled IOSimThreadId)
-> Labelled IOSimThreadId)
-> (SomeException, Labelled IOSimThreadId)
-> IOSimThreadId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SomeException, Labelled IOSimThreadId) -> Labelled IOSimThreadId
forall a b. (a, b) -> b
snd) ([(SomeException, Labelled IOSimThreadId)]
-> [(SomeException, Labelled IOSimThreadId)]
forall a. [a] -> [a]
reverse (Thread s a -> [(SomeException, Labelled IOSimThreadId)]
forall s a. Thread s a -> [(SomeException, Labelled IOSimThreadId)]
threadThrowTo Thread s a
thread))
([IOSimThreadId]
unblocked,
!SimState s a
simstate') = Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
False [IOSimThreadId]
wakeup SimState s a
simstate
in do
!SimTrace a
trace <- SimState s a -> ST s (SimTrace a)
forall s a. SimState s a -> ST s (SimTrace a)
reschedule SimState s a
simstate'
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany
[ (Time
time, IOSimThreadId
tid', Maybe ThreadLabel
tlbl', SimEventType
EventThrowToWakeup)
| IOSimThreadId
tid' <- [IOSimThreadId]
unblocked
, let tlbl' :: Maybe ThreadLabel
tlbl' = IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
forall s a.
IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel IOSimThreadId
tid' Map IOSimThreadId (Thread s a)
threads ]
SimTrace a
trace
deschedule Deschedule
Sleep Thread s a
_thread SimState s a
_simstate =
ThreadLabel -> ST s (SimTrace a)
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"IOSim: impossible happend"
reschedule :: SimState s a -> ST s (SimTrace a)
reschedule :: forall s a. SimState s a -> ST s (SimTrace a)
reschedule !simstate :: SimState s a
simstate@SimState{ Deque IOSimThreadId
runqueue :: forall s a. SimState s a -> Deque IOSimThreadId
runqueue :: Deque IOSimThreadId
runqueue, Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads }
| Just (!IOSimThreadId
tid, Deque IOSimThreadId
runqueue') <- Deque IOSimThreadId -> Maybe (IOSimThreadId, Deque IOSimThreadId)
forall a. Deque a -> Maybe (a, Deque a)
Deque.uncons Deque IOSimThreadId
runqueue =
let thread :: Thread s a
thread = Map IOSimThreadId (Thread s a)
threads Map IOSimThreadId (Thread s a) -> IOSimThreadId -> Thread s a
forall k a. Ord k => Map k a -> k -> a
Map.! IOSimThreadId
tid in
Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread SimState s a
simstate { runqueue = runqueue'
, threads = Map.delete tid threads }
reschedule !simstate :: SimState s a
simstate@SimState{ Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads, Timeouts s
timers :: forall s a. SimState s a -> Timeouts s
timers :: Timeouts s
timers, curTime :: forall s a. SimState s a -> Time
curTime = Time
time } =
case Timeouts s
-> Maybe ([TimeoutId], Time, [TimerCompletionInfo s], Timeouts s)
forall k p a.
(Ord k, Ord p) =>
OrdPSQ k p a -> Maybe ([k], p, [a], OrdPSQ k p a)
removeMinimums Timeouts s
timers of
Maybe ([TimeoutId], Time, [TimerCompletionInfo s], Timeouts s)
Nothing -> SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time -> [Labelled IOSimThreadId] -> SimTrace a
forall a. Time -> [Labelled IOSimThreadId] -> SimTrace a
TraceDeadlock Time
time (Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
forall s a.
Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
labelledThreads Map IOSimThreadId (Thread s a)
threads))
Just ([TimeoutId]
tmids, !Time
time', ![TimerCompletionInfo s]
fired, !Timeouts s
timers') -> Bool -> ST s (SimTrace a) -> ST s (SimTrace a)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Time
time' Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
>= Time
time) (ST s (SimTrace a) -> ST s (SimTrace a))
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ do
![SomeTVar s]
written <- StmA s () -> ST s [SomeTVar s]
forall s. StmA s () -> ST s [SomeTVar s]
execAtomically' (STM s () -> StmA s ()
forall s a. STM s a -> StmA s a
runSTM (STM s () -> StmA s ()) -> STM s () -> StmA s ()
forall a b. (a -> b) -> a -> b
$ (TimerCompletionInfo s -> STM s ())
-> [TimerCompletionInfo s] -> STM s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TimerCompletionInfo s -> STM s ()
forall s. TimerCompletionInfo s -> STM s ()
timeoutSTMAction [TimerCompletionInfo s]
fired)
![TraceValue]
ds <- (SomeTVar s -> ST s TraceValue)
-> [SomeTVar s] -> ST s [TraceValue]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(SomeTVar TVar s a
tvar) -> do
TraceValue
tr <- TVar s a -> Bool -> ST s TraceValue
forall s a. TVar s a -> Bool -> ST s TraceValue
traceTVarST TVar s a
tvar Bool
False
!()
_ <- TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
commitTVar TVar s a
tvar
TraceValue -> ST s TraceValue
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return TraceValue
tr) [SomeTVar s]
written
([IOSimThreadId]
wakeupSTM, Map IOSimThreadId (Set (Labelled TVarId))
wokeby) <- [SomeTVar s]
-> ST
s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))
forall s.
[SomeTVar s]
-> ST
s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))
threadsUnblockedByWrites [SomeTVar s]
written
!()
_ <- (SomeTVar s -> ST s ()) -> [SomeTVar s] -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar s a
tvar) [SomeTVar s]
written
let wakeupThreadDelay :: [(IOSimThreadId, TimeoutId)]
wakeupThreadDelay = [ (IOSimThreadId
tid, TimeoutId
tmid) | TimerThreadDelay IOSimThreadId
tid TimeoutId
tmid <- [TimerCompletionInfo s]
fired ]
wakeup :: [IOSimThreadId]
wakeup = (IOSimThreadId, TimeoutId) -> IOSimThreadId
forall a b. (a, b) -> a
fst ((IOSimThreadId, TimeoutId) -> IOSimThreadId)
-> [(IOSimThreadId, TimeoutId)] -> [IOSimThreadId]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [(IOSimThreadId, TimeoutId)]
wakeupThreadDelay [IOSimThreadId] -> [IOSimThreadId] -> [IOSimThreadId]
forall a. [a] -> [a] -> [a]
++ [IOSimThreadId]
wakeupSTM
([IOSimThreadId]
_, !SimState s a
simstate') = Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
False [IOSimThreadId]
wakeup SimState s a
simstate
!timeoutExpired :: [(IOSimThreadId, TimeoutId, TMVarDefault (IOSim s) IOSimThreadId)]
timeoutExpired = [ (IOSimThreadId
tid, TimeoutId
tmid, TMVarDefault (IOSim s) IOSimThreadId
TMVar (IOSim s) IOSimThreadId
lock)
| TimerTimeout IOSimThreadId
tid TimeoutId
tmid TMVar (IOSim s) IOSimThreadId
lock <- [TimerCompletionInfo s]
fired ]
!SimState s a
simstate'' <- [(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)]
-> SimState s a -> ST s (SimState s a)
forall s a.
[(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)]
-> SimState s a -> ST s (SimState s a)
forkTimeoutInterruptThreads [(IOSimThreadId, TimeoutId, TMVarDefault (IOSim s) IOSimThreadId)]
[(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)]
timeoutExpired SimState s a
simstate'
!SimTrace a
trace <- SimState s a -> ST s (SimTrace a)
forall s a. SimState s a -> ST s (SimTrace a)
reschedule SimState s a
simstate'' { curTime = time'
, timers = timers' }
SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> ST s (SimTrace a))
-> SimTrace a -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany ([ ( Time
time', [Int] -> IOSimThreadId
ThreadId [-Int
1], ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"timer"
, TimeoutId -> SimEventType
EventTimerFired TimeoutId
tmid)
| (TimeoutId
tmid, Timer TVar s TimeoutState
_) <- [TimeoutId]
-> [TimerCompletionInfo s] -> [(TimeoutId, TimerCompletionInfo s)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TimeoutId]
tmids [TimerCompletionInfo s]
fired ]
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ ( Time
time', [Int] -> IOSimThreadId
ThreadId [-Int
1], ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"register delay timer"
, TimeoutId -> SimEventType
EventRegisterDelayFired TimeoutId
tmid)
| (TimeoutId
tmid, TimerRegisterDelay TVar s Bool
_) <- [TimeoutId]
-> [TimerCompletionInfo s] -> [(TimeoutId, TimerCompletionInfo s)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TimeoutId]
tmids [TimerCompletionInfo s]
fired ]
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ (Time
time', [Int] -> IOSimThreadId
ThreadId [-Int
1], ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"register delay timer", Dynamic -> SimEventType
EventLog (tr -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn tr
a))
| TraceValue { traceDynamic :: ()
traceDynamic = Just tr
a } <- [TraceValue]
ds ]
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ (Time
time', [Int] -> IOSimThreadId
ThreadId [-Int
1], ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"register delay timer", ThreadLabel -> SimEventType
EventSay ThreadLabel
a)
| TraceValue { traceString :: TraceValue -> Maybe ThreadLabel
traceString = Just ThreadLabel
a } <- [TraceValue]
ds ]
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ (Time
time', IOSimThreadId
tid', Maybe ThreadLabel
tlbl', [Labelled TVarId] -> SimEventType
EventTxWakeup [Labelled TVarId]
vids)
| IOSimThreadId
tid' <- [IOSimThreadId]
wakeupSTM
, let tlbl' :: Maybe ThreadLabel
tlbl' = IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
forall s a.
IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel IOSimThreadId
tid' Map IOSimThreadId (Thread s a)
threads
, let Just [Labelled TVarId]
vids = Set (Labelled TVarId) -> [Labelled TVarId]
forall a. Set a -> [a]
Set.toList (Set (Labelled TVarId) -> [Labelled TVarId])
-> Maybe (Set (Labelled TVarId)) -> Maybe [Labelled TVarId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOSimThreadId
-> Map IOSimThreadId (Set (Labelled TVarId))
-> Maybe (Set (Labelled TVarId))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IOSimThreadId
tid' Map IOSimThreadId (Set (Labelled TVarId))
wokeby ]
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ ( Time
time', IOSimThreadId
tid, ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"thread delay timer"
, TimeoutId -> SimEventType
EventThreadDelayFired TimeoutId
tmid)
| (IOSimThreadId
tid, TimeoutId
tmid) <- [(IOSimThreadId, TimeoutId)]
wakeupThreadDelay ]
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ ( Time
time', IOSimThreadId
tid, ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"timeout timer"
, TimeoutId -> SimEventType
EventTimeoutFired TimeoutId
tmid)
| (IOSimThreadId
tid, TimeoutId
tmid, TMVarDefault (IOSim s) IOSimThreadId
_) <- [(IOSimThreadId, TimeoutId, TMVarDefault (IOSim s) IOSimThreadId)]
timeoutExpired ]
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ ( Time
time', IOSimThreadId
tid, ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"thread forked"
, IOSimThreadId -> SimEventType
EventThreadForked IOSimThreadId
tid)
| (IOSimThreadId
tid, TimeoutId
_, TMVarDefault (IOSim s) IOSimThreadId
_) <- [(IOSimThreadId, TimeoutId, TMVarDefault (IOSim s) IOSimThreadId)]
timeoutExpired ])
SimTrace a
trace
where
timeoutSTMAction :: TimerCompletionInfo s -> STM s ()
timeoutSTMAction :: forall s. TimerCompletionInfo s -> STM s ()
timeoutSTMAction (Timer TVar s TimeoutState
var) = do
TimeoutState
x <- TVar (IOSim s) TimeoutState -> STM (IOSim s) TimeoutState
forall a. TVar (IOSim s) a -> STM (IOSim s) a
forall (m :: * -> *) a. MonadSTM m => TVar m a -> STM m a
readTVar TVar (IOSim s) TimeoutState
TVar s TimeoutState
var
case TimeoutState
x of
TimeoutState
TimeoutPending -> TVar (IOSim s) TimeoutState -> TimeoutState -> STM (IOSim s) ()
forall a. TVar (IOSim s) a -> a -> STM (IOSim s) ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar TVar (IOSim s) TimeoutState
TVar s TimeoutState
var TimeoutState
TimeoutFired
TimeoutState
TimeoutFired -> ThreadLabel -> STM s ()
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"MonadTimer(Sim): invariant violation"
TimeoutState
TimeoutCancelled -> () -> STM s ()
forall a. a -> STM s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
timeoutSTMAction (TimerRegisterDelay TVar s Bool
var) = TVar (IOSim s) Bool -> Bool -> STM (IOSim s) ()
forall a. TVar (IOSim s) a -> a -> STM (IOSim s) ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar TVar (IOSim s) Bool
TVar s Bool
var Bool
True
timeoutSTMAction TimerThreadDelay{} = () -> STM s ()
forall a. a -> STM s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
timeoutSTMAction TimerTimeout{} = () -> STM s ()
forall a. a -> STM s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
unblockThreads :: Bool -> [IOSimThreadId] -> SimState s a -> ([IOSimThreadId], SimState s a)
unblockThreads :: forall s a.
Bool
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads !Bool
onlySTM ![IOSimThreadId]
wakeup !simstate :: SimState s a
simstate@SimState {Deque IOSimThreadId
runqueue :: forall s a. SimState s a -> Deque IOSimThreadId
runqueue :: Deque IOSimThreadId
runqueue, Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads} =
([IOSimThreadId]
unblocked, SimState s a
simstate {
runqueue = runqueue <> Deque.fromList unblocked,
threads = threads'
})
where
!unblocked :: [IOSimThreadId]
unblocked = [ IOSimThreadId
tid
| IOSimThreadId
tid <- [IOSimThreadId]
wakeup
, case IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe (Thread s a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IOSimThreadId
tid Map IOSimThreadId (Thread s a)
threads of
Just Thread { threadStatus :: forall s a. Thread s a -> ThreadStatus
threadStatus = ThreadBlocked BlockedReason
BlockedOnSTM }
-> Bool
True
Just Thread { threadStatus :: forall s a. Thread s a -> ThreadStatus
threadStatus = ThreadBlocked BlockedReason
_ }
-> Bool -> Bool
not Bool
onlySTM
Maybe (Thread s a)
_ -> Bool
False
]
!threads' :: Map IOSimThreadId (Thread s a)
threads' = (Map IOSimThreadId (Thread s a)
-> IOSimThreadId -> Map IOSimThreadId (Thread s a))
-> Map IOSimThreadId (Thread s a)
-> [IOSimThreadId]
-> Map IOSimThreadId (Thread s a)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl'
((IOSimThreadId
-> Map IOSimThreadId (Thread s a)
-> Map IOSimThreadId (Thread s a))
-> Map IOSimThreadId (Thread s a)
-> IOSimThreadId
-> Map IOSimThreadId (Thread s a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Thread s a -> Thread s a)
-> IOSimThreadId
-> Map IOSimThreadId (Thread s a)
-> Map IOSimThreadId (Thread s a)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (\Thread s a
t -> Thread s a
t { threadStatus = ThreadRunning })))
Map IOSimThreadId (Thread s a)
threads
[IOSimThreadId]
unblocked
forkTimeoutInterruptThreads :: forall s a.
[(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)]
-> SimState s a
-> ST s (SimState s a)
forkTimeoutInterruptThreads :: forall s a.
[(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)]
-> SimState s a -> ST s (SimState s a)
forkTimeoutInterruptThreads [(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)]
timeoutExpired SimState s a
simState =
(SimState s a
-> (Thread s a, TMVarDefault (IOSim s) IOSimThreadId)
-> ST s (SimState s a))
-> SimState s a
-> [(Thread s a, TMVarDefault (IOSim s) IOSimThreadId)]
-> ST s (SimState s a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (\st :: SimState s a
st@SimState{ Deque IOSimThreadId
runqueue :: forall s a. SimState s a -> Deque IOSimThreadId
runqueue :: Deque IOSimThreadId
runqueue, Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads }
(Thread s a
t, TMVar TVar (IOSim s) (Maybe IOSimThreadId)
lock)
-> do
Maybe IOSimThreadId
v <- TVar s (Maybe IOSimThreadId) -> ST s (Maybe IOSimThreadId)
forall s a. TVar s a -> ST s a
execReadTVar TVar (IOSim s) (Maybe IOSimThreadId)
TVar s (Maybe IOSimThreadId)
lock
SimState s a -> ST s (SimState s a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimState s a -> ST s (SimState s a))
-> SimState s a -> ST s (SimState s a)
forall a b. (a -> b) -> a -> b
$ case Maybe IOSimThreadId
v of
Maybe IOSimThreadId
Nothing -> SimState s a
st { runqueue = Deque.snoc (threadId t) runqueue,
threads = Map.insert (threadId t) t threads
}
Just IOSimThreadId
_ -> SimState s a
st
)
SimState s a
simState'
[(Thread s a, TMVarDefault (IOSim s) IOSimThreadId)]
[(Thread s a, TMVar (IOSim s) IOSimThreadId)]
throwToThread
where
throwToThread :: [(Thread s a, TMVar (IOSim s) IOSimThreadId)]
(SimState s a
simState', [(Thread s a, TMVarDefault (IOSim s) IOSimThreadId)]
[(Thread s a, TMVar (IOSim s) IOSimThreadId)]
throwToThread) = (SimState s a
-> (IOSimThreadId, TimeoutId, TMVarDefault (IOSim s) IOSimThreadId)
-> (SimState s a,
(Thread s a, TMVarDefault (IOSim s) IOSimThreadId)))
-> SimState s a
-> [(IOSimThreadId, TimeoutId,
TMVarDefault (IOSim s) IOSimThreadId)]
-> (SimState s a,
[(Thread s a, TMVarDefault (IOSim s) IOSimThreadId)])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
List.mapAccumR SimState s a
-> (IOSimThreadId, TimeoutId, TMVarDefault (IOSim s) IOSimThreadId)
-> (SimState s a,
(Thread s a, TMVarDefault (IOSim s) IOSimThreadId))
SimState s a
-> (IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)
-> (SimState s a, (Thread s a, TMVar (IOSim s) IOSimThreadId))
fn SimState s a
simState [(IOSimThreadId, TimeoutId, TMVarDefault (IOSim s) IOSimThreadId)]
[(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)]
timeoutExpired
where
fn :: SimState s a
-> (IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)
-> (SimState s a, (Thread s a, TMVar (IOSim s) IOSimThreadId))
fn :: SimState s a
-> (IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)
-> (SimState s a, (Thread s a, TMVar (IOSim s) IOSimThreadId))
fn state :: SimState s a
state@SimState { Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads } (IOSimThreadId
tid, TimeoutId
tmid, TMVar (IOSim s) IOSimThreadId
lock) =
let t :: Thread s a
t = case IOSimThreadId
tid IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe (Thread s a)
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map IOSimThreadId (Thread s a)
threads of
Just Thread s a
t' -> Thread s a
t'
Maybe (Thread s a)
Nothing -> ThreadLabel -> Thread s a
forall a. (?callStack::CallStack) => ThreadLabel -> a
error (ThreadLabel
"IOSim: internal error: unknown thread " ThreadLabel -> ThreadLabel -> ThreadLabel
forall a. [a] -> [a] -> [a]
++ IOSimThreadId -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show IOSimThreadId
tid)
nextId :: Int
nextId = Thread s a -> Int
forall s a. Thread s a -> Int
threadNextTId Thread s a
t
in ( SimState s a
state { threads = Map.insert tid t { threadNextTId = succ nextId } threads }
, ( Thread { threadId :: IOSimThreadId
threadId = IOSimThreadId -> Int -> IOSimThreadId
childThreadId IOSimThreadId
tid Int
nextId,
threadControl :: ThreadControl s a
threadControl =
SimA s () -> ControlStack s () a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl
(IOSim s () -> SimA s ()
forall s a. IOSim s a -> SimA s a
runIOSim (IOSim s () -> SimA s ()) -> IOSim s () -> SimA s ()
forall a b. (a -> b) -> a -> b
$ do
IOSimThreadId
mtid <- IOSim s (ThreadId (IOSim s))
IOSim s IOSimThreadId
forall (m :: * -> *). MonadThread m => m (ThreadId m)
myThreadId
Bool
v2 <- STM (IOSim s) Bool -> IOSim s Bool
forall a. (?callStack::CallStack) => STM (IOSim s) a -> IOSim s a
forall (m :: * -> *) a.
(MonadSTM m, ?callStack::CallStack) =>
STM m a -> m a
atomically (STM (IOSim s) Bool -> IOSim s Bool)
-> STM (IOSim s) Bool -> IOSim s Bool
forall a b. (a -> b) -> a -> b
$ TMVar (IOSim s) IOSimThreadId
-> IOSimThreadId -> STM (IOSim s) Bool
forall a. TMVar (IOSim s) a -> a -> STM (IOSim s) Bool
forall (m :: * -> *) a. MonadSTM m => TMVar m a -> a -> STM m Bool
tryPutTMVar TMVar (IOSim s) IOSimThreadId
lock IOSimThreadId
mtid
Bool -> IOSim s () -> IOSim s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
v2 (IOSim s () -> IOSim s ()) -> IOSim s () -> IOSim s ()
forall a b. (a -> b) -> a -> b
$
ThreadId (IOSim s) -> SomeException -> IOSim s ()
forall e. Exception e => ThreadId (IOSim s) -> e -> IOSim s ()
forall (m :: * -> *) e.
(MonadFork m, Exception e) =>
ThreadId m -> e -> m ()
throwTo ThreadId (IOSim s)
IOSimThreadId
tid (TimeoutException -> SomeException
forall e. Exception e => e -> SomeException
toException (TimeoutId -> TimeoutException
TimeoutException TimeoutId
tmid)))
ControlStack s () a
forall s a. ControlStack s () a
ForkFrame,
threadStatus :: ThreadStatus
threadStatus = ThreadStatus
ThreadRunning,
threadMasking :: MaskingState
threadMasking = MaskingState
Unmasked,
threadThrowTo :: [(SomeException, Labelled IOSimThreadId)]
threadThrowTo = [],
threadClockId :: ClockId
threadClockId = Thread s a -> ClockId
forall s a. Thread s a -> ClockId
threadClockId Thread s a
t,
threadLabel :: Maybe ThreadLabel
threadLabel = ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"timeout-forked-thread",
threadNextTId :: Int
threadNextTId = Int
1
}
, TMVar (IOSim s) IOSimThreadId
lock
)
)
unwindControlStack :: forall s a.
SomeException
-> Thread s a
-> Timeouts s
-> ( Either Bool (Thread s a)
, Timeouts s
)
unwindControlStack :: forall s a.
SomeException
-> Thread s a
-> Timeouts s
-> (Either Bool (Thread s a), Timeouts s)
unwindControlStack SomeException
e Thread s a
thread = \Timeouts s
timers ->
case Thread s a -> ThreadControl s a
forall s a. Thread s a -> ThreadControl s a
threadControl Thread s a
thread of
ThreadControl SimA s b
_ ControlStack s b a
ctl ->
MaskingState
-> ControlStack s b a
-> Timeouts s
-> (Either Bool (Thread s a), Timeouts s)
forall s' c.
MaskingState
-> ControlStack s' c a
-> Timeouts s
-> (Either Bool (Thread s' a), Timeouts s)
unwind (Thread s a -> MaskingState
forall s a. Thread s a -> MaskingState
threadMasking Thread s a
thread) ControlStack s b a
ctl Timeouts s
timers
where
unwind :: forall s' c. MaskingState
-> ControlStack s' c a
-> OrdPSQ TimeoutId Time (TimerCompletionInfo s)
-> (Either Bool (Thread s' a), OrdPSQ TimeoutId Time (TimerCompletionInfo s))
unwind :: forall s' c.
MaskingState
-> ControlStack s' c a
-> Timeouts s
-> (Either Bool (Thread s' a), Timeouts s)
unwind MaskingState
_ ControlStack s' c a
MainFrame Timeouts s
timers = (Bool -> Either Bool (Thread s' a)
forall a b. a -> Either a b
Left Bool
True, Timeouts s
timers)
unwind MaskingState
_ ControlStack s' c a
ForkFrame Timeouts s
timers = (Bool -> Either Bool (Thread s' a)
forall a b. a -> Either a b
Left Bool
False, Timeouts s
timers)
unwind MaskingState
_ (MaskFrame c -> SimA s' c
_k MaskingState
maskst' ControlStack s' c a
ctl) Timeouts s
timers = MaskingState
-> ControlStack s' c a
-> Timeouts s
-> (Either Bool (Thread s' a), Timeouts s)
forall s' c.
MaskingState
-> ControlStack s' c a
-> Timeouts s
-> (Either Bool (Thread s' a), Timeouts s)
unwind MaskingState
maskst' ControlStack s' c a
ctl Timeouts s
timers
unwind MaskingState
maskst (CatchFrame e -> SimA s' c
handler c -> SimA s' c
k ControlStack s' c a
ctl) Timeouts s
timers =
case SomeException -> Maybe e
forall e. Exception e => SomeException -> Maybe e
fromException SomeException
e of
Maybe e
Nothing -> MaskingState
-> ControlStack s' c a
-> Timeouts s
-> (Either Bool (Thread s' a), Timeouts s)
forall s' c.
MaskingState
-> ControlStack s' c a
-> Timeouts s
-> (Either Bool (Thread s' a), Timeouts s)
unwind MaskingState
maskst ControlStack s' c a
ctl Timeouts s
timers
Just e
e' -> ( Thread s' a -> Either Bool (Thread s' a)
forall a b. b -> Either a b
Right Thread s a
thread {
threadControl = ThreadControl (handler e')
(MaskFrame k maskst ctl),
threadMasking = atLeastInterruptibleMask maskst
}
, Timeouts s
timers
)
unwind MaskingState
maskst (TimeoutFrame TimeoutId
tmid TMVar (IOSim s') IOSimThreadId
_ Maybe c -> SimA s' c
k ControlStack s' c a
ctl) Timeouts s
timers =
case SomeException -> Maybe TimeoutException
forall e. Exception e => SomeException -> Maybe e
fromException SomeException
e of
Just (TimeoutException TimeoutId
tmid') | TimeoutId
tmid TimeoutId -> TimeoutId -> Bool
forall a. Eq a => a -> a -> Bool
== TimeoutId
tmid' ->
(Thread s' a -> Either Bool (Thread s' a)
forall a b. b -> Either a b
Right Thread s a
thread { threadControl = ThreadControl (k Nothing) ctl }, Timeouts s
timers')
Maybe TimeoutException
_ -> MaskingState
-> ControlStack s' c a
-> Timeouts s
-> (Either Bool (Thread s' a), Timeouts s)
forall s' c.
MaskingState
-> ControlStack s' c a
-> Timeouts s
-> (Either Bool (Thread s' a), Timeouts s)
unwind MaskingState
maskst ControlStack s' c a
ctl Timeouts s
timers'
where
timers' :: Timeouts s
timers' = TimeoutId -> Timeouts s -> Timeouts s
forall k p v. (Ord k, Ord p) => k -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.delete TimeoutId
tmid Timeouts s
timers
unwind MaskingState
maskst (DelayFrame TimeoutId
tmid SimA s' c
_k ControlStack s' c a
ctl) Timeouts s
timers =
MaskingState
-> ControlStack s' c a
-> Timeouts s
-> (Either Bool (Thread s' a), Timeouts s)
forall s' c.
MaskingState
-> ControlStack s' c a
-> Timeouts s
-> (Either Bool (Thread s' a), Timeouts s)
unwind MaskingState
maskst ControlStack s' c a
ctl Timeouts s
timers'
where
timers' :: Timeouts s
timers' = TimeoutId -> Timeouts s -> Timeouts s
forall k p v. (Ord k, Ord p) => k -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.delete TimeoutId
tmid Timeouts s
timers
atLeastInterruptibleMask :: MaskingState -> MaskingState
atLeastInterruptibleMask :: MaskingState -> MaskingState
atLeastInterruptibleMask MaskingState
Unmasked = MaskingState
MaskedInterruptible
atLeastInterruptibleMask MaskingState
ms = MaskingState
ms
removeMinimums :: (Ord k, Ord p)
=> OrdPSQ k p a
-> Maybe ([k], p, [a], OrdPSQ k p a)
removeMinimums :: forall k p a.
(Ord k, Ord p) =>
OrdPSQ k p a -> Maybe ([k], p, [a], OrdPSQ k p a)
removeMinimums = \OrdPSQ k p a
psq ->
case OrdPSQ k p a -> Maybe (k, p, a, OrdPSQ k p a)
forall k p v.
(Ord k, Ord p) =>
OrdPSQ k p v -> Maybe (k, p, v, OrdPSQ k p v)
PSQ.minView OrdPSQ k p a
psq of
Maybe (k, p, a, OrdPSQ k p a)
Nothing -> Maybe ([k], p, [a], OrdPSQ k p a)
forall a. Maybe a
Nothing
Just (k
k, p
p, a
x, OrdPSQ k p a
psq') -> ([k], p, [a], OrdPSQ k p a) -> Maybe ([k], p, [a], OrdPSQ k p a)
forall a. a -> Maybe a
Just ([k] -> p -> [a] -> OrdPSQ k p a -> ([k], p, [a], OrdPSQ k p a)
forall {a} {b} {a}.
(Ord a, Ord b) =>
[a] -> b -> [a] -> OrdPSQ a b a -> ([a], b, [a], OrdPSQ a b a)
collectAll [k
k] p
p [a
x] OrdPSQ k p a
psq')
where
collectAll :: [a] -> b -> [a] -> OrdPSQ a b a -> ([a], b, [a], OrdPSQ a b a)
collectAll ![a]
ks !b
p ![a]
xs !OrdPSQ a b a
psq =
case OrdPSQ a b a -> Maybe (a, b, a, OrdPSQ a b a)
forall k p v.
(Ord k, Ord p) =>
OrdPSQ k p v -> Maybe (k, p, v, OrdPSQ k p v)
PSQ.minView OrdPSQ a b a
psq of
Just (a
k, b
p', a
x, OrdPSQ a b a
psq')
| b
p b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
p' -> [a] -> b -> [a] -> OrdPSQ a b a -> ([a], b, [a], OrdPSQ a b a)
collectAll (a
ka -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ks) b
p (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) OrdPSQ a b a
psq'
Maybe (a, b, a, OrdPSQ a b a)
_ -> ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
ks, b
p, [a] -> [a]
forall a. [a] -> [a]
reverse [a]
xs, OrdPSQ a b a
psq)
traceMany :: [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany :: forall a.
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany [] SimTrace a
trace = SimTrace a
trace
traceMany ((Time
time, IOSimThreadId
tid, Maybe ThreadLabel
tlbl, SimEventType
event):[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
ts) SimTrace a
trace =
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl SimEventType
event ([(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
ts SimTrace a
trace)
lookupThreadLabel :: IOSimThreadId -> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel :: forall s a.
IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel IOSimThreadId
tid Map IOSimThreadId (Thread s a)
threads = Maybe (Maybe ThreadLabel) -> Maybe ThreadLabel
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Thread s a -> Maybe ThreadLabel
forall s a. Thread s a -> Maybe ThreadLabel
threadLabel (Thread s a -> Maybe ThreadLabel)
-> Maybe (Thread s a) -> Maybe (Maybe ThreadLabel)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOSimThreadId
-> Map IOSimThreadId (Thread s a) -> Maybe (Thread s a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IOSimThreadId
tid Map IOSimThreadId (Thread s a)
threads)
runSimTraceST :: forall s a. IOSim s a -> ST s (SimTrace a)
runSimTraceST :: forall s a. IOSim s a -> ST s (SimTrace a)
runSimTraceST IOSim s a
mainAction = Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
mainThread SimState s a
forall s a. SimState s a
initialState
where
mainThread :: Thread s a
mainThread =
Thread {
threadId :: IOSimThreadId
threadId = [Int] -> IOSimThreadId
ThreadId [],
threadControl :: ThreadControl s a
threadControl = SimA s a -> ControlStack s a a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (IOSim s a -> SimA s a
forall s a. IOSim s a -> SimA s a
runIOSim IOSim s a
mainAction) ControlStack s a a
forall s b. ControlStack s b b
MainFrame,
threadStatus :: ThreadStatus
threadStatus = ThreadStatus
ThreadRunning,
threadMasking :: MaskingState
threadMasking = MaskingState
Unmasked,
threadThrowTo :: [(SomeException, Labelled IOSimThreadId)]
threadThrowTo = [],
threadClockId :: ClockId
threadClockId = [Int] -> ClockId
ClockId [],
threadLabel :: Maybe ThreadLabel
threadLabel = ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"main",
threadNextTId :: Int
threadNextTId = Int
1
}
execAtomically :: forall s a c.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> TVarId
-> StmA s a
-> (StmTxResult s a -> ST s (SimTrace c))
-> ST s (SimTrace c)
execAtomically :: forall s a c.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> TVarId
-> StmA s a
-> (StmTxResult s a -> ST s (SimTrace c))
-> ST s (SimTrace c)
execAtomically !Time
time !IOSimThreadId
tid !Maybe ThreadLabel
tlbl !TVarId
nextVid0 !StmA s a
action0 !StmTxResult s a -> ST s (SimTrace c)
k0 =
StmStack s a a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s a
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s a a
forall s b. StmStack s b b
AtomicallyFrame Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty [] [] TVarId
nextVid0 StmA s a
action0
where
go :: forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go :: forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go !StmStack s b a
ctl !Map TVarId (SomeTVar s)
read !Map TVarId (SomeTVar s)
written ![SomeTVar s]
writtenSeq ![SomeTVar s]
createdSeq !TVarId
nextVid !StmA s b
action =
Bool -> ST s (SimTrace c) -> ST s (SimTrace c)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert Bool
localInvariant (ST s (SimTrace c) -> ST s (SimTrace c))
-> ST s (SimTrace c) -> ST s (SimTrace c)
forall a b. (a -> b) -> a -> b
$
case StmA s b
action of
ReturnStm b
x ->
case StmStack s b a
ctl of
StmStack s b a
AtomicallyFrame -> do
![TraceValue]
ds <- (SomeTVar s -> ST s TraceValue)
-> [SomeTVar s] -> ST s [TraceValue]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(SomeTVar TVar s a
tvar) -> TVar s a -> Bool -> ST s TraceValue
forall s a. TVar s a -> Bool -> ST s TraceValue
traceTVarST TVar s a
tvar Bool
True) [SomeTVar s]
createdSeq
![TraceValue]
ds' <- Map TVarId TraceValue -> [TraceValue]
forall k a. Map k a -> [a]
Map.elems (Map TVarId TraceValue -> [TraceValue])
-> ST s (Map TVarId TraceValue) -> ST s [TraceValue]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SomeTVar s -> ST s TraceValue)
-> Map TVarId (SomeTVar s) -> ST s (Map TVarId TraceValue)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map TVarId a -> f (Map TVarId b)
traverse
(\(SomeTVar TVar s a
tvar) -> do
TraceValue
tr <- TVar s a -> Bool -> ST s TraceValue
forall s a. TVar s a -> Bool -> ST s TraceValue
traceTVarST TVar s a
tvar Bool
False
!()
_ <- TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
commitTVar TVar s a
tvar
[a]
undos <- TVar s a -> ST s [a]
forall s a. TVar s a -> ST s [a]
readTVarUndos TVar s a
tvar
Bool -> ST s TraceValue -> ST s TraceValue
forall a. (?callStack::CallStack) => Bool -> a -> a
assert ([a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
undos) (ST s TraceValue -> ST s TraceValue)
-> ST s TraceValue -> ST s TraceValue
forall a b. (a -> b) -> a -> b
$ TraceValue -> ST s TraceValue
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return TraceValue
tr
) Map TVarId (SomeTVar s)
written
StmTxResult s a -> ST s (SimTrace c)
k0 (StmTxResult s a -> ST s (SimTrace c))
-> StmTxResult s a -> ST s (SimTrace c)
forall a b. (a -> b) -> a -> b
$ a
-> [SomeTVar s]
-> [SomeTVar s]
-> [SomeTVar s]
-> [Dynamic]
-> [ThreadLabel]
-> TVarId
-> StmTxResult s a
forall s a.
a
-> [SomeTVar s]
-> [SomeTVar s]
-> [SomeTVar s]
-> [Dynamic]
-> [ThreadLabel]
-> TVarId
-> StmTxResult s a
StmTxCommitted a
b
x ([SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a]
reverse [SomeTVar s]
writtenSeq)
[]
([SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a]
reverse [SomeTVar s]
createdSeq)
((TraceValue -> Maybe Dynamic) -> [TraceValue] -> [Dynamic]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\TraceValue { Maybe tr
traceDynamic :: ()
traceDynamic :: Maybe tr
traceDynamic }
-> tr -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn (tr -> Dynamic) -> Maybe tr -> Maybe Dynamic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe tr
traceDynamic)
([TraceValue] -> [Dynamic]) -> [TraceValue] -> [Dynamic]
forall a b. (a -> b) -> a -> b
$ [TraceValue]
ds [TraceValue] -> [TraceValue] -> [TraceValue]
forall a. [a] -> [a] -> [a]
++ [TraceValue]
ds')
((TraceValue -> Maybe ThreadLabel) -> [TraceValue] -> [ThreadLabel]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TraceValue -> Maybe ThreadLabel
traceString ([TraceValue] -> [ThreadLabel]) -> [TraceValue] -> [ThreadLabel]
forall a b. (a -> b) -> a -> b
$ [TraceValue]
ds [TraceValue] -> [TraceValue] -> [TraceValue]
forall a. [a] -> [a] -> [a]
++ [TraceValue]
ds')
TVarId
nextVid
BranchFrame BranchStmA s b
_b b -> StmA s b1
k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b1 a
ctl' -> do
!()
_ <- (SomeTVar s -> ST s ()) -> Map TVarId (SomeTVar s) -> ST s ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
commitTVar TVar s a
tvar)
(Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection Map TVarId (SomeTVar s)
written Map TVarId (SomeTVar s)
writtenOuter)
let written' :: Map TVarId (SomeTVar s)
written' = Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map TVarId (SomeTVar s)
written Map TVarId (SomeTVar s)
writtenOuter
writtenSeq' :: [SomeTVar s]
writtenSeq' = (SomeTVar s -> Bool) -> [SomeTVar s] -> [SomeTVar s]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(SomeTVar TVar s a
tvar) ->
TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
tvar TVarId -> Map TVarId (SomeTVar s) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map TVarId (SomeTVar s)
writtenOuter)
[SomeTVar s]
writtenSeq
[SomeTVar s] -> [SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a] -> [a]
++ [SomeTVar s]
writtenOuterSeq
createdSeq' :: [SomeTVar s]
createdSeq' = [SomeTVar s]
createdSeq [SomeTVar s] -> [SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a] -> [a]
++ [SomeTVar s]
createdOuterSeq
StmStack s b1 a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b1
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b1 a
ctl' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written' [SomeTVar s]
writtenSeq' [SomeTVar s]
createdSeq' TVarId
nextVid (b -> StmA s b1
k b
x)
ThrowStm SomeException
e -> do
!()
_ <- (SomeTVar s -> ST s ()) -> Map TVarId (SomeTVar s) -> ST s ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
revertTVar TVar s a
tvar) Map TVarId (SomeTVar s)
written
case StmStack s b a
ctl of
StmStack s b a
AtomicallyFrame -> do
StmTxResult s a -> ST s (SimTrace c)
k0 (StmTxResult s a -> ST s (SimTrace c))
-> StmTxResult s a -> ST s (SimTrace c)
forall a b. (a -> b) -> a -> b
$ [SomeTVar s] -> SomeException -> StmTxResult s a
forall s a. [SomeTVar s] -> SomeException -> StmTxResult s a
StmTxAborted (Map TVarId (SomeTVar s) -> [SomeTVar s]
forall k a. Map k a -> [a]
Map.elems Map TVarId (SomeTVar s)
read) (SomeException -> SomeException
forall e. Exception e => e -> SomeException
toException SomeException
e)
BranchFrame (CatchStmA SomeException -> StmA s b
h) b -> StmA s b1
k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b1 a
ctl' -> do
let ctl'' :: StmStack s b a
ctl'' = BranchStmA s b
-> (b -> StmA s b1)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b1 a
-> StmStack s b a
forall s b b1 a.
BranchStmA s b
-> (b -> StmA s b1)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b1 a
-> StmStack s b a
BranchFrame BranchStmA s b
forall s a. BranchStmA s a
NoOpStmA b -> StmA s b1
k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b1 a
ctl'
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl'' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty [] [] TVarId
nextVid (SomeException -> StmA s b
h SomeException
e)
BranchFrame (OrElseStmA StmA s b
_r) b -> StmA s b1
_k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b1 a
ctl' -> do
StmStack s b1 a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b1
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b1 a
ctl' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq TVarId
nextVid (SomeException -> StmA s b1
forall s a. SomeException -> StmA s a
ThrowStm SomeException
e)
BranchFrame BranchStmA s b
NoOpStmA b -> StmA s b1
_k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b1 a
ctl' -> do
StmStack s b1 a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b1
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b1 a
ctl' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq TVarId
nextVid (SomeException -> StmA s b1
forall s a. SomeException -> StmA s a
ThrowStm SomeException
e)
CatchStm StmA s a1
a SomeException -> StmA s a1
h a1 -> StmA s b
k -> do
let ctl' :: StmStack s a1 a
ctl' = BranchStmA s a1
-> (a1 -> StmA s b)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b a
-> StmStack s a1 a
forall s b b1 a.
BranchStmA s b
-> (b -> StmA s b1)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b1 a
-> StmStack s b a
BranchFrame ((SomeException -> StmA s a1) -> BranchStmA s a1
forall s a. (SomeException -> StmA s a) -> BranchStmA s a
CatchStmA SomeException -> StmA s a1
h) a1 -> StmA s b
k Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq StmStack s b a
ctl
StmStack s a1 a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s a1
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s a1 a
ctl' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty [] [] TVarId
nextVid StmA s a1
a
StmA s b
Retry -> do
!()
_ <- (SomeTVar s -> ST s ()) -> Map TVarId (SomeTVar s) -> ST s ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
revertTVar TVar s a
tvar) Map TVarId (SomeTVar s)
written
case StmStack s b a
ctl of
StmStack s b a
AtomicallyFrame -> do
StmTxResult s a -> ST s (SimTrace c)
k0 (StmTxResult s a -> ST s (SimTrace c))
-> StmTxResult s a -> ST s (SimTrace c)
forall a b. (a -> b) -> a -> b
$! [SomeTVar s] -> StmTxResult s a
forall s a. [SomeTVar s] -> StmTxResult s a
StmTxBlocked ([SomeTVar s] -> StmTxResult s a)
-> [SomeTVar s] -> StmTxResult s a
forall a b. (a -> b) -> a -> b
$! Map TVarId (SomeTVar s) -> [SomeTVar s]
forall k a. Map k a -> [a]
Map.elems Map TVarId (SomeTVar s)
read
BranchFrame (OrElseStmA StmA s b
b) b -> StmA s b1
k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b1 a
ctl' -> do
let ctl'' :: StmStack s b a
ctl'' = BranchStmA s b
-> (b -> StmA s b1)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b1 a
-> StmStack s b a
forall s b b1 a.
BranchStmA s b
-> (b -> StmA s b1)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b1 a
-> StmStack s b a
BranchFrame BranchStmA s b
forall s a. BranchStmA s a
NoOpStmA b -> StmA s b1
k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b1 a
ctl'
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl'' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty [] [] TVarId
nextVid StmA s b
b
BranchFrame BranchStmA s b
_ b -> StmA s b1
_k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b1 a
ctl' -> do
StmStack s b1 a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b1
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b1 a
ctl' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq TVarId
nextVid StmA s b1
forall s a. StmA s a
Retry
OrElse StmA s a1
a StmA s a1
b a1 -> StmA s b
k -> do
let ctl' :: StmStack s a1 a
ctl' = BranchStmA s a1
-> (a1 -> StmA s b)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b a
-> StmStack s a1 a
forall s b b1 a.
BranchStmA s b
-> (b -> StmA s b1)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b1 a
-> StmStack s b a
BranchFrame (StmA s a1 -> BranchStmA s a1
forall s a. StmA s a -> BranchStmA s a
OrElseStmA StmA s a1
b) a1 -> StmA s b
k Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq StmStack s b a
ctl
StmStack s a1 a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s a1
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s a1 a
ctl' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty [] [] TVarId
nextVid StmA s a1
a
NewTVar !Maybe ThreadLabel
mbLabel x
x TVar s x -> StmA s b
k -> do
!TVar s x
v <- TVarId -> Maybe ThreadLabel -> x -> ST s (TVar s x)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar TVarId
nextVid Maybe ThreadLabel
mbLabel x
x
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq (TVar s x -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s x
v SomeTVar s -> [SomeTVar s] -> [SomeTVar s]
forall a. a -> [a] -> [a]
: [SomeTVar s]
createdSeq) (TVarId -> TVarId
forall a. Enum a => a -> a
succ TVarId
nextVid) (TVar s x -> StmA s b
k TVar s x
v)
LabelTVar !ThreadLabel
label TVar s a1
tvar StmA s b
k -> do
!()
_ <- STRef s (Maybe ThreadLabel) -> Maybe ThreadLabel -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef (TVar s a1 -> STRef s (Maybe ThreadLabel)
forall s a. TVar s a -> STRef s (Maybe ThreadLabel)
tvarLabel TVar s a1
tvar) (Maybe ThreadLabel -> ST s ()) -> Maybe ThreadLabel -> ST s ()
forall a b. (a -> b) -> a -> b
$! (ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
label)
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k
TraceTVar TVar s a1
tvar Maybe a1 -> a1 -> ST s TraceValue
f StmA s b
k -> do
!()
_ <- STRef s (Maybe (Maybe a1 -> a1 -> ST s TraceValue))
-> Maybe (Maybe a1 -> a1 -> ST s TraceValue) -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef (TVar s a1 -> STRef s (Maybe (Maybe a1 -> a1 -> ST s TraceValue))
forall s a.
TVar s a -> STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace TVar s a1
tvar) ((Maybe a1 -> a1 -> ST s TraceValue)
-> Maybe (Maybe a1 -> a1 -> ST s TraceValue)
forall a. a -> Maybe a
Just Maybe a1 -> a1 -> ST s TraceValue
f)
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k
ReadTVar TVar s a1
v a1 -> StmA s b
k
| TVar s a1 -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a1
v TVarId -> Map TVarId (SomeTVar s) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map TVarId (SomeTVar s)
read -> do
a1
x <- TVar s a1 -> ST s a1
forall s a. TVar s a -> ST s a
execReadTVar TVar s a1
v
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid (a1 -> StmA s b
k a1
x)
| Bool
otherwise ->
do
a1
x <- TVar s a1 -> ST s a1
forall s a. TVar s a -> ST s a
execReadTVar TVar s a1
v
let read' :: Map TVarId (SomeTVar s)
read' = TVarId
-> SomeTVar s -> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (TVar s a1 -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a1
v) (TVar s a1 -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s a1
v) Map TVarId (SomeTVar s)
read
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read' Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid (a1 -> StmA s b
k a1
x)
WriteTVar TVar s a1
v a1
x StmA s b
k
| TVar s a1 -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a1
v TVarId -> Map TVarId (SomeTVar s) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map TVarId (SomeTVar s)
written -> do
!()
_ <- TVar s a1 -> a1 -> ST s ()
forall s a. TVar s a -> a -> ST s ()
execWriteTVar TVar s a1
v a1
x
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k
| Bool
otherwise -> do
!()
_ <- TVar s a1 -> ST s ()
forall s a. TVar s a -> ST s ()
saveTVar TVar s a1
v
!()
_ <- TVar s a1 -> a1 -> ST s ()
forall s a. TVar s a -> a -> ST s ()
execWriteTVar TVar s a1
v a1
x
let written' :: Map TVarId (SomeTVar s)
written' = TVarId
-> SomeTVar s -> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (TVar s a1 -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a1
v) (TVar s a1 -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s a1
v) Map TVarId (SomeTVar s)
written
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written' (TVar s a1 -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s a1
v SomeTVar s -> [SomeTVar s] -> [SomeTVar s]
forall a. a -> [a] -> [a]
: [SomeTVar s]
writtenSeq) [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k
SayStm ThreadLabel
msg StmA s b
k -> do
SimTrace c
trace <- StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k
SimTrace c -> ST s (SimTrace c)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace c -> ST s (SimTrace c))
-> SimTrace c -> ST s (SimTrace c)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace c
-> SimTrace c
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (ThreadLabel -> SimEventType
EventSay ThreadLabel
msg) SimTrace c
trace
OutputStm Dynamic
x StmA s b
k -> do
SimTrace c
trace <- StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k
SimTrace c -> ST s (SimTrace c)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace c -> ST s (SimTrace c))
-> SimTrace c -> ST s (SimTrace c)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace c
-> SimTrace c
forall a.
Time
-> IOSimThreadId
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
time IOSimThreadId
tid Maybe ThreadLabel
tlbl (Dynamic -> SimEventType
EventLog Dynamic
x) SimTrace c
trace
LiftSTStm ST s a1
st a1 -> StmA s b
k -> do
a1
x <- ST s a1 -> ST s a1
forall s a. ST s a -> ST s a
strictToLazyST ST s a1
st
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid (a1 -> StmA s b
k a1
x)
FixStm x -> STM s x
f x -> StmA s b
k -> do
STRef s x
r <- x -> ST s (STRef s x)
forall a s. a -> ST s (STRef s a)
newSTRef (NonTermination -> x
forall a e. Exception e => e -> a
throw NonTermination
NonTermination)
x
x <- ST s x -> ST s x
forall s a. ST s a -> ST s a
unsafeInterleaveST (ST s x -> ST s x) -> ST s x -> ST s x
forall a b. (a -> b) -> a -> b
$ STRef s x -> ST s x
forall s a. STRef s a -> ST s a
readSTRef STRef s x
r
let k' :: StmA s b
k' = STM s x -> forall r. (x -> StmA s r) -> StmA s r
forall s a. STM s a -> forall r. (a -> StmA s r) -> StmA s r
unSTM (x -> STM s x
f x
x) ((x -> StmA s b) -> StmA s b) -> (x -> StmA s b) -> StmA s b
forall a b. (a -> b) -> a -> b
$ \x
x' ->
ST s () -> (() -> StmA s b) -> StmA s b
forall s a1 a. ST s a1 -> (a1 -> StmA s a) -> StmA s a
LiftSTStm (ST s () -> ST s ()
forall s a. ST s a -> ST s a
lazyToStrictST (STRef s x -> x -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s x
r x
x')) (\() -> x -> StmA s b
k x
x')
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k'
where
localInvariant :: Bool
localInvariant =
Map TVarId (SomeTVar s) -> Set TVarId
forall k a. Map k a -> Set k
Map.keysSet Map TVarId (SomeTVar s)
written
Set TVarId -> Set TVarId -> Bool
forall a. Eq a => a -> a -> Bool
== [TVarId] -> Set TVarId
forall a. Ord a => [a] -> Set a
Set.fromList [ TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
tvar | SomeTVar TVar s a
tvar <- [SomeTVar s]
writtenSeq ]
execAtomically' :: StmA s () -> ST s [SomeTVar s]
execAtomically' :: forall s. StmA s () -> ST s [SomeTVar s]
execAtomically' = Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
forall s. Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
go Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty
where
go :: Map TVarId (SomeTVar s)
-> StmA s ()
-> ST s [SomeTVar s]
go :: forall s. Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
go !Map TVarId (SomeTVar s)
written StmA s ()
action = case StmA s ()
action of
ReturnStm () -> do
[SomeTVar s] -> ST s [SomeTVar s]
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map TVarId (SomeTVar s) -> [SomeTVar s]
forall k a. Map k a -> [a]
Map.elems Map TVarId (SomeTVar s)
written)
ReadTVar TVar s a1
v a1 -> StmA s ()
k -> do
a1
x <- TVar s a1 -> ST s a1
forall s a. TVar s a -> ST s a
execReadTVar TVar s a1
v
Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
forall s. Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
go Map TVarId (SomeTVar s)
written (a1 -> StmA s ()
k a1
x)
WriteTVar TVar s a1
v a1
x StmA s ()
k
| TVar s a1 -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a1
v TVarId -> Map TVarId (SomeTVar s) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map TVarId (SomeTVar s)
written -> do
!()
_ <- TVar s a1 -> a1 -> ST s ()
forall s a. TVar s a -> a -> ST s ()
execWriteTVar TVar s a1
v a1
x
Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
forall s. Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
go Map TVarId (SomeTVar s)
written StmA s ()
k
| Bool
otherwise -> do
!()
_ <- TVar s a1 -> ST s ()
forall s a. TVar s a -> ST s ()
saveTVar TVar s a1
v
!()
_ <- TVar s a1 -> a1 -> ST s ()
forall s a. TVar s a -> a -> ST s ()
execWriteTVar TVar s a1
v a1
x
let written' :: Map TVarId (SomeTVar s)
written' = TVarId
-> SomeTVar s -> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (TVar s a1 -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a1
v) (TVar s a1 -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s a1
v) Map TVarId (SomeTVar s)
written
Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
forall s. Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
go Map TVarId (SomeTVar s)
written' StmA s ()
k
StmA s ()
_ -> ThreadLabel -> ST s [SomeTVar s]
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"execAtomically': only for special case of reads and writes"
execNewTVar :: TVarId -> Maybe String -> a -> ST s (TVar s a)
execNewTVar :: forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar TVarId
nextVid !Maybe ThreadLabel
mbLabel a
x = do
!STRef s (Maybe ThreadLabel)
tvarLabel <- Maybe ThreadLabel -> ST s (STRef s (Maybe ThreadLabel))
forall a s. a -> ST s (STRef s a)
newSTRef Maybe ThreadLabel
mbLabel
!STRef s a
tvarCurrent <- a -> ST s (STRef s a)
forall a s. a -> ST s (STRef s a)
newSTRef a
x
!STRef s [a]
tvarUndo <- [a] -> ST s (STRef s [a])
forall a s. a -> ST s (STRef s a)
newSTRef ([a] -> ST s (STRef s [a])) -> [a] -> ST s (STRef s [a])
forall a b. (a -> b) -> a -> b
$! []
!STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked <- ([IOSimThreadId], Set IOSimThreadId)
-> ST s (STRef s ([IOSimThreadId], Set IOSimThreadId))
forall a s. a -> ST s (STRef s a)
newSTRef ([], Set IOSimThreadId
forall a. Set a
Set.empty)
!STRef s VectorClock
tvarVClock <- VectorClock -> ST s (STRef s VectorClock)
forall a s. a -> ST s (STRef s a)
newSTRef (VectorClock -> ST s (STRef s VectorClock))
-> VectorClock -> ST s (STRef s VectorClock)
forall a b. (a -> b) -> a -> b
$! Map IOSimThreadId Int -> VectorClock
VectorClock Map IOSimThreadId Int
forall k a. Map k a
Map.empty
!STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace <- Maybe (Maybe a -> a -> ST s TraceValue)
-> ST s (STRef s (Maybe (Maybe a -> a -> ST s TraceValue)))
forall a s. a -> ST s (STRef s a)
newSTRef (Maybe (Maybe a -> a -> ST s TraceValue)
-> ST s (STRef s (Maybe (Maybe a -> a -> ST s TraceValue))))
-> Maybe (Maybe a -> a -> ST s TraceValue)
-> ST s (STRef s (Maybe (Maybe a -> a -> ST s TraceValue)))
forall a b. (a -> b) -> a -> b
$! Maybe (Maybe a -> a -> ST s TraceValue)
forall a. Maybe a
Nothing
TVar s a -> ST s (TVar s a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return TVar {tvarId :: TVarId
tvarId = TVarId
nextVid, STRef s (Maybe ThreadLabel)
tvarLabel :: STRef s (Maybe ThreadLabel)
tvarLabel :: STRef s (Maybe ThreadLabel)
tvarLabel,
STRef s a
tvarCurrent :: STRef s a
tvarCurrent :: STRef s a
tvarCurrent, STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo, STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked :: STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked :: STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked, STRef s VectorClock
tvarVClock :: STRef s VectorClock
tvarVClock :: STRef s VectorClock
tvarVClock,
STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace :: STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace :: STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace}
execWriteTVar :: TVar s a -> a -> ST s ()
execWriteTVar :: forall s a. TVar s a -> a -> ST s ()
execWriteTVar TVar{STRef s a
tvarCurrent :: forall s a. TVar s a -> STRef s a
tvarCurrent :: STRef s a
tvarCurrent} = STRef s a -> a -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s a
tvarCurrent
{-# INLINE execWriteTVar #-}
execTryPutTMVar :: TMVar (IOSim s) a -> a -> ST s Bool
execTryPutTMVar :: forall s a. TMVar (IOSim s) a -> a -> ST s Bool
execTryPutTMVar (TMVar TVar (IOSim s) (Maybe a)
var) a
a = do
Maybe a
v <- TVar s (Maybe a) -> ST s (Maybe a)
forall s a. TVar s a -> ST s a
execReadTVar TVar (IOSim s) (Maybe a)
TVar s (Maybe a)
var
case Maybe a
v of
Maybe a
Nothing -> TVar s (Maybe a) -> Maybe a -> ST s ()
forall s a. TVar s a -> a -> ST s ()
execWriteTVar TVar (IOSim s) (Maybe a)
TVar s (Maybe a)
var (a -> Maybe a
forall a. a -> Maybe a
Just a
a)
ST s () -> ST s Bool -> ST s Bool
forall a b. ST s a -> ST s b -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Just a
_ -> Bool -> ST s Bool
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
{-# INLINE execTryPutTMVar #-}
saveTVar :: TVar s a -> ST s ()
saveTVar :: forall s a. TVar s a -> ST s ()
saveTVar TVar{STRef s a
tvarCurrent :: forall s a. TVar s a -> STRef s a
tvarCurrent :: STRef s a
tvarCurrent, STRef s [a]
tvarUndo :: forall s a. TVar s a -> STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo} = do
a
v <- STRef s a -> ST s a
forall s a. STRef s a -> ST s a
readSTRef STRef s a
tvarCurrent
![a]
vs <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
STRef s [a] -> [a] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [a]
tvarUndo ([a] -> ST s ()) -> [a] -> ST s ()
forall a b. (a -> b) -> a -> b
$! a
va -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
vs
revertTVar :: TVar s a -> ST s ()
revertTVar :: forall s a. TVar s a -> ST s ()
revertTVar TVar{STRef s a
tvarCurrent :: forall s a. TVar s a -> STRef s a
tvarCurrent :: STRef s a
tvarCurrent, STRef s [a]
tvarUndo :: forall s a. TVar s a -> STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo} = do
![a]
vs <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
!()
_ <- STRef s a -> a -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s a
tvarCurrent ([a] -> a
forall a. (?callStack::CallStack) => [a] -> a
head [a]
vs)
STRef s [a] -> [a] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [a]
tvarUndo ([a] -> ST s ()) -> [a] -> ST s ()
forall a b. (a -> b) -> a -> b
$! [a] -> [a]
forall a. (?callStack::CallStack) => [a] -> [a]
tail [a]
vs
{-# INLINE revertTVar #-}
commitTVar :: TVar s a -> ST s ()
commitTVar :: forall s a. TVar s a -> ST s ()
commitTVar TVar{STRef s [a]
tvarUndo :: forall s a. TVar s a -> STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo} = do
![a]
vs <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
STRef s [a] -> [a] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [a]
tvarUndo ([a] -> ST s ()) -> [a] -> ST s ()
forall a b. (a -> b) -> a -> b
$! [a] -> [a]
forall a. (?callStack::CallStack) => [a] -> [a]
tail [a]
vs
{-# INLINE commitTVar #-}
readTVarUndos :: TVar s a -> ST s [a]
readTVarUndos :: forall s a. TVar s a -> ST s [a]
readTVarUndos TVar{STRef s [a]
tvarUndo :: forall s a. TVar s a -> STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo} = STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
traceTVarST :: TVar s a
-> Bool
-> ST s TraceValue
traceTVarST :: forall s a. TVar s a -> Bool -> ST s TraceValue
traceTVarST TVar{TVarId
tvarId :: forall s a. TVar s a -> TVarId
tvarId :: TVarId
tvarId, STRef s a
tvarCurrent :: forall s a. TVar s a -> STRef s a
tvarCurrent :: STRef s a
tvarCurrent, STRef s [a]
tvarUndo :: forall s a. TVar s a -> STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo, STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace :: forall s a.
TVar s a -> STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace :: STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace} Bool
new = do
Maybe (Maybe a -> a -> ST s TraceValue)
mf <- STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
-> ST s (Maybe (Maybe a -> a -> ST s TraceValue))
forall s a. STRef s a -> ST s a
readSTRef STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace
case Maybe (Maybe a -> a -> ST s TraceValue)
mf of
Maybe (Maybe a -> a -> ST s TraceValue)
Nothing -> TraceValue -> ST s TraceValue
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return TraceValue { traceDynamic :: Maybe ()
traceDynamic = (Maybe ()
forall a. Maybe a
Nothing :: Maybe ())
, traceString :: Maybe ThreadLabel
traceString = Maybe ThreadLabel
forall a. Maybe a
Nothing }
Just Maybe a -> a -> ST s TraceValue
f -> do
![a]
vs <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
a
v <- STRef s a -> ST s a
forall s a. STRef s a -> ST s a
readSTRef STRef s a
tvarCurrent
case (Bool
new, [a]
vs) of
(Bool
True, [a]
_) -> Maybe a -> a -> ST s TraceValue
f Maybe a
forall a. Maybe a
Nothing a
v
(Bool
_, a
_:[a]
_) -> Maybe a -> a -> ST s TraceValue
f (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [a] -> a
forall a. (?callStack::CallStack) => [a] -> a
last [a]
vs) a
v
(Bool, [a])
_ -> ThreadLabel -> ST s TraceValue
forall a. (?callStack::CallStack) => ThreadLabel -> a
error (ThreadLabel
"traceTVarST: unexpected tvar state " ThreadLabel -> ThreadLabel -> ThreadLabel
forall a. [a] -> [a] -> [a]
++ TVarId -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show TVarId
tvarId)
readTVarBlockedThreads :: TVar s a -> ST s [IOSimThreadId]
readTVarBlockedThreads :: forall s a. TVar s a -> ST s [IOSimThreadId]
readTVarBlockedThreads TVar{STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked :: forall s a.
TVar s a -> STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked :: STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked} = ([IOSimThreadId], Set IOSimThreadId) -> [IOSimThreadId]
forall a b. (a, b) -> a
fst (([IOSimThreadId], Set IOSimThreadId) -> [IOSimThreadId])
-> ST s ([IOSimThreadId], Set IOSimThreadId)
-> ST s [IOSimThreadId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef s ([IOSimThreadId], Set IOSimThreadId)
-> ST s ([IOSimThreadId], Set IOSimThreadId)
forall s a. STRef s a -> ST s a
readSTRef STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked
blockThreadOnTVar :: IOSimThreadId -> TVar s a -> ST s ()
blockThreadOnTVar :: forall s a. IOSimThreadId -> TVar s a -> ST s ()
blockThreadOnTVar IOSimThreadId
tid TVar{STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked :: forall s a.
TVar s a -> STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked :: STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked} = do
([IOSimThreadId]
tids, Set IOSimThreadId
tidsSet) <- STRef s ([IOSimThreadId], Set IOSimThreadId)
-> ST s ([IOSimThreadId], Set IOSimThreadId)
forall s a. STRef s a -> ST s a
readSTRef STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked
Bool -> ST s () -> ST s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IOSimThreadId
tid IOSimThreadId -> Set IOSimThreadId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set IOSimThreadId
tidsSet) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ do
let !tids' :: [IOSimThreadId]
tids' = IOSimThreadId
tid IOSimThreadId -> [IOSimThreadId] -> [IOSimThreadId]
forall a. a -> [a] -> [a]
: [IOSimThreadId]
tids
!tidsSet' :: Set IOSimThreadId
tidsSet' = IOSimThreadId -> Set IOSimThreadId -> Set IOSimThreadId
forall a. Ord a => a -> Set a -> Set a
Set.insert IOSimThreadId
tid Set IOSimThreadId
tidsSet
!()
_ <- STRef s ([IOSimThreadId], Set IOSimThreadId)
-> ([IOSimThreadId], Set IOSimThreadId) -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked ([IOSimThreadId]
tids', Set IOSimThreadId
tidsSet')
() -> ST s ()
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
unblockAllThreadsFromTVar :: TVar s a -> ST s ()
unblockAllThreadsFromTVar :: forall s a. TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar{STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked :: forall s a.
TVar s a -> STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked :: STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked} = do
!()
_ <- STRef s ([IOSimThreadId], Set IOSimThreadId)
-> ([IOSimThreadId], Set IOSimThreadId) -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked ([], Set IOSimThreadId
forall a. Set a
Set.empty)
() -> ST s ()
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
threadsUnblockedByWrites :: [SomeTVar s]
-> ST s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))
threadsUnblockedByWrites :: forall s.
[SomeTVar s]
-> ST
s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))
threadsUnblockedByWrites [SomeTVar s]
written = do
![(Labelled TVarId, [IOSimThreadId])]
tidss <- [ST s (Labelled TVarId, [IOSimThreadId])]
-> ST s [(Labelled TVarId, [IOSimThreadId])]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
[ (,) (Labelled TVarId
-> [IOSimThreadId] -> (Labelled TVarId, [IOSimThreadId]))
-> ST s (Labelled TVarId)
-> ST s ([IOSimThreadId] -> (Labelled TVarId, [IOSimThreadId]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVar s a -> ST s (Labelled TVarId)
forall s a. TVar s a -> ST s (Labelled TVarId)
labelledTVarId TVar s a
tvar ST s ([IOSimThreadId] -> (Labelled TVarId, [IOSimThreadId]))
-> ST s [IOSimThreadId] -> ST s (Labelled TVarId, [IOSimThreadId])
forall a b. ST s (a -> b) -> ST s a -> ST s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TVar s a -> ST s [IOSimThreadId]
forall s a. TVar s a -> ST s [IOSimThreadId]
readTVarBlockedThreads TVar s a
tvar
| SomeTVar TVar s a
tvar <- [SomeTVar s]
written ]
let !wakeup :: [IOSimThreadId]
wakeup = [IOSimThreadId] -> [IOSimThreadId]
forall a. Ord a => [a] -> [a]
ordNub [ IOSimThreadId
tid | (Labelled TVarId
_vid, [IOSimThreadId]
tids) <- [(Labelled TVarId, [IOSimThreadId])]
tidss, IOSimThreadId
tid <- [IOSimThreadId] -> [IOSimThreadId]
forall a. [a] -> [a]
reverse [IOSimThreadId]
tids ]
wokeby :: Map IOSimThreadId (Set (Labelled TVarId))
wokeby = (Set (Labelled TVarId)
-> Set (Labelled TVarId) -> Set (Labelled TVarId))
-> [(IOSimThreadId, Set (Labelled TVarId))]
-> Map IOSimThreadId (Set (Labelled TVarId))
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Set (Labelled TVarId)
-> Set (Labelled TVarId) -> Set (Labelled TVarId)
forall a. Ord a => Set a -> Set a -> Set a
Set.union
[ (IOSimThreadId
tid, Labelled TVarId -> Set (Labelled TVarId)
forall a. a -> Set a
Set.singleton Labelled TVarId
vid)
| (Labelled TVarId
vid, [IOSimThreadId]
tids) <- [(Labelled TVarId, [IOSimThreadId])]
tidss
, IOSimThreadId
tid <- [IOSimThreadId]
tids ]
([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))
-> ST
s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId)))
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ([IOSimThreadId]
wakeup, Map IOSimThreadId (Set (Labelled TVarId))
wokeby)
ordNub :: Ord a => [a] -> [a]
ordNub :: forall a. Ord a => [a] -> [a]
ordNub = Set a -> [a] -> [a]
forall {a}. Ord a => Set a -> [a] -> [a]
go Set a
forall a. Set a
Set.empty
where
go :: Set a -> [a] -> [a]
go !Set a
_ [] = []
go !Set a
s (a
x:[a]
xs)
| a
x a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set a
s = Set a -> [a] -> [a]
go Set a
s [a]
xs
| Bool
otherwise = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Set a -> [a] -> [a]
go (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
x Set a
s) [a]
xs
{-# INLINE ordNub #-}