{-# LANGUAGE CPP             #-}
{-# LANGUAGE DerivingVia     #-}
-- only used to construct records if its clear to do so
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies    #-}

-- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted')
-- and 'reschedule'.
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns -Wno-unused-matches #-}
{-# OPTIONS_GHC -Wno-orphans #-}
#if __GLASGOW_HASKELL__ >= 908
-- We use partial functions from `Data.List`.
{-# OPTIONS_GHC -Wno-x-partial #-}
#endif

module Control.Monad.IOSimPOR.Internal
  ( IOSim (..)
  , runIOSim
  , runSimTraceST
  , traceM
  , traceSTM
  , STM
  , STMSim
  , setCurrentTime
  , unshareClock
  , TimeoutException (..)
  , EventlogEvent (..)
  , EventlogMarker (..)
  , IOSimThreadId
  , ThreadLabel
  , Labelled (..)
  , SimTrace
  , Trace.Trace (SimPORTrace, TraceMainReturn, TraceMainException, TraceDeadlock)
  , SimEvent (..)
  , SimResult (..)
  , SimEventType (..)
  , liftST
  , execReadTVar
  , controlSimTraceST
  , ScheduleControl (..)
  , ScheduleMod (..)
  ) where

import Prelude hiding (read)

import Data.Dynamic
import Data.Foldable (foldlM, traverse_)
import Data.HashPSQ (HashPSQ)
import Data.HashPSQ qualified as PSQ
import Data.IntPSQ (IntPSQ)
import Data.IntPSQ qualified as IPSQ
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.Ord
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Time (UTCTime (..), fromGregorian)

import Control.DeepSeq (force)
import Control.Exception (NonTermination (..), SomeAsyncException, 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 as MonadThrow
import Control.Monad.Class.MonadTime (NominalDiffTime)
import Control.Monad.Class.MonadTime qualified as Time
import Control.Monad.Class.MonadTime.SI qualified as SI
import Control.Monad.Class.MonadTimer.SI (TimeoutState (..))

import Control.Monad.IOSim.InternalTypes
import Control.Monad.IOSim.Types hiding (SimEvent (SimEvent), Time (..),
           Trace (SimTrace))
import Control.Monad.IOSim.Types (SimEvent)
import Control.Monad.IOSimPOR.Timeout (unsafeTimeout)
import Control.Monad.IOSimPOR.Types
import Data.Coerce (Coercible, coerce)
import Data.Hashable

--
-- Simulation interpreter
--

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,
    -- other threads blocked in a ThrowTo to us because we are or were masked
    forall s a.
Thread s a
-> [(SomeException, Labelled IOSimThreadId, VectorClock)]
threadThrowTo :: ![(SomeException, Labelled IOSimThreadId, VectorClock)],
    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,
    forall s a. Thread s a -> Int
threadStep    :: !Int,
    forall s a. Thread s a -> VectorClock
threadVClock  :: VectorClock,
    forall s a. Thread s a -> Effect
threadEffect  :: Effect,  -- in the current step
    forall s a. Thread s a -> Bool
threadRacy    :: !Bool
  }
  deriving Int -> Thread s a -> ShowS
[Thread s a] -> ShowS
Thread s a -> ThreadLabel
(Int -> Thread s a -> ShowS)
-> (Thread s a -> ThreadLabel)
-> ([Thread s a] -> ShowS)
-> Show (Thread s a)
forall a.
(Int -> a -> ShowS)
-> (a -> ThreadLabel) -> ([a] -> ShowS) -> Show a
forall s a. Int -> Thread s a -> ShowS
forall s a. [Thread s a] -> ShowS
forall s a. Thread s a -> ThreadLabel
$cshowsPrec :: forall s a. Int -> Thread s a -> ShowS
showsPrec :: Int -> Thread s a -> ShowS
$cshow :: forall s a. Thread s a -> ThreadLabel
show :: Thread s a -> ThreadLabel
$cshowList :: forall s a. [Thread s a] -> ShowS
showList :: [Thread s a] -> ShowS
Show

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

isThreadDone :: Thread s a -> Bool
isThreadDone :: forall s a. Thread s a -> Bool
isThreadDone Thread s a
t = case Thread s a -> ThreadStatus
forall s a. Thread s a -> ThreadStatus
threadStatus Thread s a
t of
    ThreadStatus
ThreadDone -> Bool
True
    ThreadStatus
_          -> Bool
False

threadStepId :: Thread s a -> (IOSimThreadId, Int)
threadStepId :: forall s a. Thread s a -> StepId
threadStepId Thread{ IOSimThreadId
threadId :: forall s a. Thread s a -> IOSimThreadId
threadId :: IOSimThreadId
threadId, Int
threadStep :: forall s a. Thread s a -> Int
threadStep :: Int
threadStep } = (IOSimThreadId
threadId, Int
threadStep)

isRacyThreadId :: IOSimThreadId -> Bool
isRacyThreadId :: IOSimThreadId -> Bool
isRacyThreadId (RacyThreadId [Int]
_) = Bool
True
isRacyThreadId IOSimThreadId
_                = Bool
True

isNotRacyThreadId :: IOSimThreadId -> Bool
isNotRacyThreadId :: IOSimThreadId -> Bool
isNotRacyThreadId (ThreadId [Int]
_) = Bool
True
isNotRacyThreadId IOSimThreadId
_            = Bool
False

bottomVClock :: VectorClock
bottomVClock :: VectorClock
bottomVClock = Map IOSimThreadId Int -> VectorClock
VectorClock Map IOSimThreadId Int
forall k a. Map k a
Map.empty

insertVClock :: IOSimThreadId -> Int -> VectorClock -> VectorClock
insertVClock :: IOSimThreadId -> Int -> VectorClock -> VectorClock
insertVClock IOSimThreadId
tid !Int
step (VectorClock Map IOSimThreadId Int
m) = Map IOSimThreadId Int -> VectorClock
VectorClock (IOSimThreadId
-> Int -> Map IOSimThreadId Int -> Map IOSimThreadId Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IOSimThreadId
tid Int
step Map IOSimThreadId Int
m)

leastUpperBoundVClock :: VectorClock -> VectorClock -> VectorClock
leastUpperBoundVClock :: VectorClock -> VectorClock -> VectorClock
leastUpperBoundVClock (VectorClock Map IOSimThreadId Int
m) (VectorClock Map IOSimThreadId Int
m') =
    Map IOSimThreadId Int -> VectorClock
VectorClock ((Int -> Int -> Int)
-> Map IOSimThreadId Int
-> Map IOSimThreadId Int
-> Map IOSimThreadId Int
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Map IOSimThreadId Int
m Map IOSimThreadId Int
m')

-- hbfVClock :: VectorClock -> VectorClock -> Bool
-- hbfVClock (VectorClock m) (VectorClock m') = Map.isSubmapOfBy (<=) m m'

happensBeforeStep :: Step -- ^ an earlier step
                  -> Step -- ^ a later step
                  -> Bool
happensBeforeStep :: Step -> Step -> Bool
happensBeforeStep Step
step Step
step' =
       Int -> Maybe Int
forall a. a -> Maybe a
Just (Step -> Int
stepStep Step
step)
    Maybe Int -> Maybe Int -> Bool
forall a. Ord a => a -> a -> Bool
<= IOSimThreadId -> Map IOSimThreadId Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Step -> IOSimThreadId
stepThreadId Step
step)
                  (VectorClock -> Map IOSimThreadId Int
getVectorClock (VectorClock -> Map IOSimThreadId Int)
-> VectorClock -> Map IOSimThreadId Int
forall a b. (a -> b) -> a -> b
$ Step -> VectorClock
stepVClock Step
step')

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 =
    -- @Map.foldr'@ (and alikes) are not strict enough, to not retain the
    -- original thread map we need to evaluate the spine of the list.
    -- TODO: https://github.com/haskell/containers/issues/749
    (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


-- | Timers mutable variables.  First one supports 'newTimeout' api, the second
-- one 'Control.Monad.Class.MonadTimer.SI.registerDelay', the third one
-- 'Control.Monad.Class.MonadTimer.SI.threadDelay'.
--
data TimerCompletionInfo s =
       Timer !(TVar s TimeoutState)
     -- ^ `newTimeout` timer.
     | TimerRegisterDelay !(TVar s Bool)
     -- ^ `registerDelay` timer.
     | TimerThreadDelay !IOSimThreadId !TimeoutId
     -- ^ `threadDelay` timer run by `IOSimThreadId` which was assigned the given
     -- `TimeoutId` (only used to report in a trace).
     | TimerTimeout !IOSimThreadId !TimeoutId !(TMVar (IOSim s) IOSimThreadId)
     -- ^ `timeout` timer run by `IOSimThreadId` which was assigned the given
     -- `TimeoutId` (only used to report in a trace).

instance Hashable a => Hashable (Down a)

type RunQueue   = HashPSQ (Down IOSimThreadId) (Down IOSimThreadId) ()
type Timeouts s = IntPSQ SI.Time (TimerCompletionInfo s)

-- | Internal state.
--
data SimState s a = SimState {
       forall s a. SimState s a -> RunQueue
runqueue         :: !RunQueue,
       -- | All threads other than the currently running thread: both running
       -- and blocked threads.
       forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads          :: !(Map IOSimThreadId (Thread s a)),
       -- | current time
       forall s a. SimState s a -> Time
curTime          :: !SI.Time,
       -- | ordered list of timers and timeouts
       forall s a. SimState s a -> Timeouts s
timers           :: !(Timeouts s),
       -- | timeout locks in order to synchronize the timeout handler and the
       -- main thread
       forall s a. SimState s a -> Map ClockId UTCTime
clocks           :: !(Map ClockId UTCTime),
       forall s a. SimState s a -> Int
nextVid          :: !VarId,     -- ^ next unused 'TVarId'
       forall s a. SimState s a -> TimeoutId
nextTmid         :: !TimeoutId,  -- ^ next unused 'TimeoutId'
       forall s a. SimState s a -> Unique s
nextUniq         :: !(Unique s), -- ^ next unused @'Unique' s@
       -- | previous steps (which we may race with).
       -- Note this is *lazy*, so that we don't compute races we will not reverse.
       forall s a. SimState s a -> Races
races            :: Races,
       -- | control the schedule followed, and initial value
       forall s a. SimState s a -> ScheduleControl
control          :: !ScheduleControl,
       forall s a. SimState s a -> ScheduleControl
control0         :: !ScheduleControl,
       -- | limit on the computation time allowed per scheduling step, for
       -- catching infinite loops etc
       forall s a. SimState s a -> Maybe Int
perStepTimeLimit :: Maybe Int

     }

initialState :: SimState s a
initialState :: forall s a. SimState s a
initialState =
    SimState {
      runqueue :: RunQueue
runqueue = RunQueue
forall k p v. HashPSQ k p v
PSQ.empty,
      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
SI.Time DiffTime
0,
      timers :: Timeouts s
timers   = Timeouts s
forall p v. IntPSQ p v
IPSQ.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 :: Int
nextVid  = Int
0,
      nextTmid :: TimeoutId
nextTmid = Int -> TimeoutId
TimeoutId Int
0,
      nextUniq :: Unique s
nextUniq = Integer -> Unique s
forall {k} (s :: k). Integer -> Unique s
MkUnique Integer
0,
      races :: Races
races    = Races
noRaces,
      control :: ScheduleControl
control  = ScheduleControl
ControlDefault,
      control0 :: ScheduleControl
control0 = ScheduleControl
ControlDefault,
      perStepTimeLimit :: Maybe Int
perStepTimeLimit = Maybe Int
forall a. Maybe a
Nothing
    }
  where
    epoch1970 :: UTCTime
epoch1970 = Day -> DiffTime -> UTCTime
UTCTime (Integer -> Int -> Int -> Day
fromGregorian Integer
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{RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue :: RunQueue
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 (Bool -> Bool
not (IOSimThreadId -> Down IOSimThreadId
forall a. a -> Down a
Down (Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
running) Down IOSimThreadId -> RunQueue -> Bool
forall k p v.
(Hashable k, Ord k, Ord p) =>
k -> HashPSQ k p v -> Bool
`PSQ.member` RunQueue
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{RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue :: RunQueue
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 ((Down IOSimThreadId -> Down IOSimThreadId -> () -> Bool -> Bool)
-> Bool -> RunQueue -> Bool
forall k p v a. (k -> p -> v -> a -> a) -> a -> HashPSQ k p v -> a
PSQ.fold' (\(Down IOSimThreadId
tid) Down IOSimThreadId
_ ()
_ Bool
a -> IOSimThreadId
tid 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 Bool -> Bool -> Bool
&& Bool
a) Bool
True RunQueue
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
|| Thread s a -> Bool
forall s a. Thread s a -> Bool
isThreadDone Thread s a
t) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Bool
not (IOSimThreadId -> Down IOSimThreadId
forall a. a -> Down a
Down (Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
t) Down IOSimThreadId -> RunQueue -> Bool
forall k p v.
(Hashable k, Ord k, Ord p) =>
k -> HashPSQ k p v -> Bool
`PSQ.member` RunQueue
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 ([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 ])

-- | Interpret the simulation monotonic time as a 'NominalDiffTime' since
-- the start.
timeSinceEpoch :: SI.Time -> NominalDiffTime
timeSinceEpoch :: Time -> NominalDiffTime
timeSinceEpoch (SI.Time DiffTime
t) = Rational -> NominalDiffTime
forall a. Fractional a => Rational -> a
fromRational (DiffTime -> Rational
forall a. Real a => a -> Rational
toRational DiffTime
t)


-- | Insert thread into `runqueue`.
--
insertThread :: Thread s a -> RunQueue -> RunQueue
insertThread :: forall s a. Thread s a -> RunQueue -> RunQueue
insertThread Thread { IOSimThreadId
threadId :: forall s a. Thread s a -> IOSimThreadId
threadId :: IOSimThreadId
threadId } = Down IOSimThreadId
-> Down IOSimThreadId -> () -> RunQueue -> RunQueue
forall k p v.
(Ord k, Hashable k, Ord p) =>
k -> p -> v -> HashPSQ k p v -> HashPSQ k p v
PSQ.insert (IOSimThreadId -> Down IOSimThreadId
forall a. a -> Down a
Down IOSimThreadId
threadId) (IOSimThreadId -> Down IOSimThreadId
forall a. a -> Down a
Down IOSimThreadId
threadId) ()


-- | Schedule / run a thread.
--
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,
           threadStep :: forall s a. Thread s a -> Int
threadStep    = Int
tstep,
           threadVClock :: forall s a. Thread s a -> VectorClock
threadVClock  = VectorClock
vClock,
           threadEffect :: forall s a. Thread s a -> Effect
threadEffect  = Effect
effect
         }
         simstate :: SimState s a
simstate@SimState {
           RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue :: RunQueue
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,
           Int
nextVid :: forall s a. SimState s a -> Int
nextVid :: Int
nextVid, TimeoutId
nextTmid :: forall s a. SimState s a -> TimeoutId
nextTmid :: TimeoutId
nextTmid, Unique s
nextUniq :: forall s a. SimState s a -> Unique s
nextUniq :: Unique s
nextUniq,
           curTime :: forall s a. SimState s a -> Time
curTime  = Time
time,
           ScheduleControl
control :: forall s a. SimState s a -> ScheduleControl
control :: ScheduleControl
control,
           Maybe Int
perStepTimeLimit :: forall s a. SimState s a -> Maybe Int
perStepTimeLimit :: Maybe Int
perStepTimeLimit
         }

  | StepId -> ScheduleControl -> Bool
controlTargets (IOSimThreadId
tid,Int
tstep) ScheduleControl
control =
      -- The next step is to be delayed according to the
      -- specified schedule. Switch to following the schedule.
      Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (ScheduleControl -> SimEventType
EventFollowControl ScheduleControl
control) (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      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{ control = followControl control }

  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ StepId -> ScheduleControl -> Bool
controlFollows (IOSimThreadId
tid,Int
tstep) ScheduleControl
control =
      -- the control says this is not the next step to
      -- follow. We should be at the beginning of a step;
      -- we put the present thread to sleep and reschedule
      -- the correct thread.
      -- The assertion says that the only effect that may have
      -- happened in the start of a thread is us waking up.
      ( Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (StepId -> ScheduleControl -> SimEventType
EventAwaitControl (IOSimThreadId
tid,Int
tstep) ScheduleControl
control)
      (SimTrace a -> SimTrace a)
-> (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Sleep)
      ) (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
Sleep Thread s a
thread SimState s a
simstate

  | Bool
otherwise =
  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 ScheduleControl
control of
    ControlFollow (StepId
s:[StepId]
_) [ScheduleMod]
_
      -> (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall a b. (a -> b) -> ST s a -> ST s b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (StepId -> SimEventType
EventPerformAction (IOSimThreadId
tid,Int
tstep)))
    ScheduleControl
_ -> ST s (SimTrace a) -> ST s (SimTrace a)
forall a. a -> a
id
  (ST s (SimTrace a) -> ST s (SimTrace a))
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$
  -- The next line forces the evaluation of action, which should be unevaluated up to
  -- this point. This is where we actually *run* user code.
  case (SimA s b -> Maybe (SimA s b))
-> (Int -> SimA s b -> Maybe (SimA s b))
-> Maybe Int
-> SimA s b
-> Maybe (SimA s b)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SimA s b -> Maybe (SimA s b)
forall a. a -> Maybe a
Just Int -> SimA s b -> Maybe (SimA s b)
forall a. Int -> a -> Maybe a
unsafeTimeout Maybe Int
perStepTimeLimit SimA s b
action of
    Maybe (SimA s b)
Nothing -> SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return SimTrace a
forall a. SimTrace a
TraceLoop
    Just SimA s b
_  -> case SimA s b
action of

      Return b
x -> case ControlStack s b a
ctl of
        ControlStack s b a
MainFrame ->
          -- the main thread is done, so we're done
          -- even if other threads are still running
          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
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl SimEventType
EventThreadFinished
                 (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimState s a -> SimTrace a -> SimTrace a
forall s a. SimState s a -> SimTrace a -> SimTrace a
traceFinalRacesFound SimState s a
simstate
                 (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) -> [Labelled IOSimThreadId])
-> (Map IOSimThreadId (Thread s a)
    -> Map IOSimThreadId (Thread s a))
-> Map IOSimThreadId (Thread s a)
-> [Labelled IOSimThreadId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Thread s a -> Bool)
-> Map IOSimThreadId (Thread s a) -> Map IOSimThreadId (Thread s a)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not (Bool -> Bool) -> (Thread s a -> Bool) -> Thread s a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thread s a -> Bool
forall s a. Thread s a -> Bool
isThreadDone)
                                        (Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId])
-> Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
forall a b. (a -> b) -> a -> b
$ Map IOSimThreadId (Thread s a)
threads
                                        )

        ControlStack s b a
ForkFrame -> do
          -- this thread is done
          let thread' :: Thread s a
thread' = Thread s a
thread
          !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
          return $ SimPORTrace time tid tstep tlbl EventThreadFinished
                 $ SimPORTrace time tid tstep tlbl (EventDeschedule Terminated)
                 $ trace

        MaskFrame b -> SimA s c
k MaskingState
maskst' ControlStack s c a
ctl' -> do
          -- pop the control stack, restore thread-local state
          let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k x) ctl'
                               , threadMasking = maskst'
                               }
          -- but if we're now unmasked, check for any pending async exceptions
          !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
          return $ SimPORTrace time tid tstep tlbl (EventMask maskst')
                 $ SimPORTrace time tid tstep tlbl (EventDeschedule Interruptable)
                 $ trace

        CatchFrame e -> SimA s b
_handler b -> SimA s c
k ControlStack s c a
ctl' -> do
          -- pop the control stack and continue
          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
          -- It could happen that the timeout action finished at the same time
          -- as the timeout expired, this will be a race condition. That's why
          -- we have the locks to solve this.

          -- We cannot do `tryPutMVar` in the `treadAction`, because we need to
          -- know if the `lock` is empty right now when we still have the frame.
          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 -- Kill the assassin throwing thread then unmask exceptions and
              -- carry on the continuation
              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
>>= IOSimThreadId -> IOSim s ()
ThreadId (IOSim s) -> IOSim s ()
forall (m :: * -> *). MonadFork m => ThreadId m -> m ()
killThread

              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'
                       }
          schedule thread' 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' = Int -> Timeouts s -> Timeouts s
forall p v. Ord p => Int -> IntPSQ p v -> IntPSQ p v
IPSQ.delete (TimeoutId -> Int
forall a b. Coercible a b => a -> b
coerce 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
        -- Found a CatchFrame
        (Right thread0 :: Thread s a
thread0@Thread { threadMasking :: forall s a. Thread s a -> MaskingState
threadMasking = MaskingState
maskst' }, Timeouts s
timers'') -> do
          -- We found a suitable exception handler, continue with that
          -- We record a step, in case there is no exception handler on replay.
          let (Thread s a
thread', Effect
eff)  = Thread s a -> (Thread s a, Effect)
forall s a. Thread s a -> (Thread s a, Effect)
stepThread Thread s a
thread0
              control' :: ScheduleControl
control'        = StepId -> ScheduleControl -> ScheduleControl
advanceControl (Thread s a -> StepId
forall s a. Thread s a -> StepId
threadStepId Thread s a
thread0) ScheduleControl
control
              races' :: Races
races'          = Thread s a -> SimState s a -> Races
forall s a. Thread s a -> SimState s a -> Races
updateRaces Thread s a
thread0 SimState s a
simstate
          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{ races = races',
                                              control = control',
                                              timers = timers'' }
          return (SimPORTrace time tid tstep tlbl (EventThrow e) $
                  SimPORTrace time tid tstep tlbl (EventMask maskst') $
                  SimPORTrace time tid tstep tlbl (EventEffect vClock eff) $
                  SimPORTrace time tid tstep tlbl (EventRaces races')
                  trace)

        (Left Bool
isMain, Timeouts s
timers'')
          -- We unwound and did not find any suitable exception handler, so we
          -- have an unhandled exception at the top level of the thread.
          | Bool
isMain -> do
            let thread' :: Thread s a
thread' = Thread s a
thread { threadStatus = ThreadDone }
            -- An unhandled exception in the main thread terminates the program
            SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep 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
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (SomeException -> SimEventType
EventThreadUnhandled SomeException
e) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
                    SimState s a -> SimTrace a -> SimTrace a
forall s a. SimState s a -> SimTrace a -> SimTrace a
traceFinalRacesFound SimState s a
simstate { threads = Map.insert tid thread' threads } (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
            -- An unhandled exception in any other thread terminates the thread
            let terminated :: Deschedule
terminated = Deschedule
Terminated
            !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'' }
            return $ SimPORTrace time tid tstep tlbl (EventThrow e)
                   $ SimPORTrace time tid tstep tlbl (EventThreadUnhandled e)
                   $ SimPORTrace time tid tstep tlbl (EventDeschedule terminated)
                   $ trace

      Catch SimA s a1
action' e -> SimA s a1
handler a1 -> SimA s b
k -> do
        -- push the failure and success continuations onto the control stack
        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
        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
$ (SomeException -> Maybe SomeException)
-> IO a1 -> IO (Either SomeException a1)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
forall (m :: * -> *) e b a.
(MonadCatch m, Exception e) =>
(e -> Maybe b) -> m a -> m (Either b a)
tryJust (\SomeException
e -> case forall e. Exception e => SomeException -> Maybe e
fromException @SomeAsyncException SomeException
e of
                                            Maybe SomeAsyncException
Nothing -> SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just SomeException
e
                                            Just {} -> Maybe SomeException
forall a. Maybe a
Nothing)
                               (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 mbWHNF of
          Left SomeException
e -> do
            -- schedule this thread to immediately raise the exception
            let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Throw e) ctl }
            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
            return $ SimPORTrace time tid tstep tlbl (EventEvaluationError e)
                   $ trace
          Right a1
whnf -> do
            -- continue with the resulting WHNF
            let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k whnf) ctl }
            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
            return $ SimPORTrace time tid tstep tlbl EventEvaluationSuccess
                   $ trace

      Say ThreadLabel
msg SimA s b
k -> do
        mbNF <- IO (Either SomeException ThreadLabel)
-> ST s (Either SomeException ThreadLabel)
forall a s. IO a -> ST s a
unsafeIOToST (IO (Either SomeException ThreadLabel)
 -> ST s (Either SomeException ThreadLabel))
-> IO (Either SomeException ThreadLabel)
-> ST s (Either SomeException ThreadLabel)
forall a b. (a -> b) -> a -> b
$ (SomeException -> Maybe SomeException)
-> IO ThreadLabel -> IO (Either SomeException ThreadLabel)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
forall (m :: * -> *) e b a.
(MonadCatch m, Exception e) =>
(e -> Maybe b) -> m a -> m (Either b a)
tryJust (\SomeException
e -> case forall e. Exception e => SomeException -> Maybe e
fromException @SomeAsyncException SomeException
e of
                                          Maybe SomeAsyncException
Nothing -> SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just SomeException
e
                                          Just {} -> Maybe SomeException
forall a. Maybe a
Nothing)
                             (IO ThreadLabel -> IO (Either SomeException ThreadLabel))
-> IO ThreadLabel -> IO (Either SomeException ThreadLabel)
forall a b. (a -> b) -> a -> b
$ ThreadLabel -> IO ThreadLabel
forall a. a -> IO a
forall (m :: * -> *) a. MonadEvaluate m => a -> m a
evaluate (ShowS
forall a. NFData a => a -> a
force ThreadLabel
msg)
        case mbNF of
          Left SomeException
e  -> do
            let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Throw e) ctl }
            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
            return $ SimPORTrace time tid tstep tlbl (EventSayEvaluationError e)
                   $ trace
          Right ThreadLabel
msg' -> do
            let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
            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
            return (SimPORTrace time tid tstep tlbl (EventSay msg') trace)

      Output x :: Dynamic
x@(Dynamic TypeRep a
_ a
x') SimA s b
k -> do
        mbWHNF <- IO (Either SomeException a) -> ST s (Either SomeException a)
forall a s. IO a -> ST s a
unsafeIOToST (IO (Either SomeException a) -> ST s (Either SomeException a))
-> IO (Either SomeException a) -> ST s (Either SomeException a)
forall a b. (a -> b) -> a -> b
$ (SomeException -> Maybe SomeException)
-> IO a -> IO (Either SomeException a)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
forall (m :: * -> *) e b a.
(MonadCatch m, Exception e) =>
(e -> Maybe b) -> m a -> m (Either b a)
tryJust (\SomeException
e -> case forall e. Exception e => SomeException -> Maybe e
fromException @SomeAsyncException SomeException
e of
                                            Maybe SomeAsyncException
Nothing -> SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just SomeException
e
                                            Just {} -> Maybe SomeException
forall a. Maybe a
Nothing)
                               (IO a -> IO (Either SomeException a))
-> IO a -> IO (Either SomeException a)
forall a b. (a -> b) -> a -> b
$ a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. MonadEvaluate m => a -> m a
evaluate a
x'
        case mbWHNF of
          Left SomeException
e  -> do
            let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Throw e) ctl }
            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
            return $ SimPORTrace time tid tstep tlbl (EventLogEvaluationError e)
                   $ trace
          Right {} -> do
            let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl k ctl }
            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
            return (SimPORTrace time tid tstep tlbl (EventLog x) trace)

      LiftST ST s a1
st a1 -> SimA s b
k -> do
        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 { threadControl = ThreadControl (k x) ctl }
        schedule thread' 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
`Time.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
`Time.addUTCTime` UTCTime
clockoff
            clockoff' :: UTCTime
clockoff' = (UTCTime
walltime' UTCTime -> UTCTime -> NominalDiffTime
`Time.diffUTCTime` UTCTime
walltime) NominalDiffTime -> UTCTime -> UTCTime
`Time.addUTCTime` 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 -- reuse the thread id
            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'

      -- This case is guarded by checks in 'timeout' itself.
      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
        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 (Int -> TVarId
TMVarId Int
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 -> ShowS
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    = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
            timers'   = Int -> Time -> TimerCompletionInfo s -> Timeouts s -> Timeouts s
forall p v. Ord p => Int -> p -> v -> IntPSQ p v -> IntPSQ p v
IPSQ.insert (TimeoutId -> Int
forall a b. Coercible a b => a -> b
coerce 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 TMVar (IOSim s) IOSimThreadId
TMVarDefault (IOSim s) IOSimThreadId
lock) Timeouts s
timers
            thread'   = Thread s a
thread { threadControl =
                                   ThreadControl action'
                                                 (TimeoutFrame nextTmid lock k ctl)
                                }
        trace <- deschedule Yield thread' simstate { timers   = timers'
                                                    , nextTmid = succ nextTmid }
        return (SimPORTrace time tid tstep tlbl (EventTimeoutCreated nextTmid tid expiry) 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 = IPSQ.delete (coerce 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 <- TVarId -> Maybe ThreadLabel -> Bool -> ST s (TVar s Bool)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar (Int -> TVarId
TVarId Int
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show (TimeoutId -> Int
unTimeoutId TimeoutId
nextTmid) ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadLabel
">>")
                            Bool
True
        modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock)
        let !expiry  = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
            !thread' = Thread s a
thread { threadControl = ThreadControl (k tvar) ctl }
        trace <- schedule thread' simstate { nextVid = succ nextVid }
        return (SimPORTrace time tid tstep tlbl (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) $
                SimPORTrace time tid tstep tlbl (EventRegisterDelayFired nextTmid) $
                trace)

      RegisterDelay DiffTime
d TVar s Bool -> SimA s b
k -> do
        tvar <- TVarId -> Maybe ThreadLabel -> Bool -> ST s (TVar s Bool)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar (Int -> TVarId
TVarId Int
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show (TimeoutId -> Int
unTimeoutId TimeoutId
nextTmid) ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadLabel
">>")
                            Bool
False
        modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock)
        let !expiry  = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
            !timers' = Int -> Time -> TimerCompletionInfo s -> Timeouts s -> Timeouts s
forall p v. Ord p => Int -> p -> v -> IntPSQ p v -> IntPSQ p v
IPSQ.insert (TimeoutId -> Int
forall a b. Coercible a b => a -> b
coerce 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 { threadControl = ThreadControl (k tvar) ctl }
        trace <- schedule thread' simstate { timers   = timers'
                                           , nextVid  = succ nextVid
                                           , nextTmid = succ nextTmid }
        return (SimPORTrace time tid tstep tlbl
                  (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) 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 }
        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'
        return (SimPORTrace time tid tstep tlbl (EventThreadDelay nextTmid expiry) $
                SimPORTrace time tid tstep tlbl (EventThreadDelayFired nextTmid) $
                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' = Int -> Time -> TimerCompletionInfo s -> Timeouts s -> Timeouts s
forall p v. Ord p => Int -> p -> v -> IntPSQ p v -> IntPSQ p v
IPSQ.insert (TimeoutId -> Int
forall a b. Coercible a b => a -> b
coerce 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) }
        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 }
        return (SimPORTrace time tid tstep tlbl (EventThreadDelay nextTmid expiry) trace)

      -- we treat negative timers as cancelled ones; for the record we put
      -- `EventTimerCreated` and `EventTimerCancelled` in the trace; This differs
      -- from `GHC.Event` behaviour.
      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 }
        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 }
        return (SimPORTrace time tid tstep tlbl (EventTimerCreated nextTmid (TVarId nextVid) expiry) $
                SimPORTrace time tid tstep tlbl (EventTimerCancelled nextTmid) $
                trace)

      NewTimeout DiffTime
d Timeout s -> SimA s b
k -> do
        tvar  <- TVarId
-> Maybe ThreadLabel -> TimeoutState -> ST s (TVar s TimeoutState)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar (Int -> TVarId
TVarId Int
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show (TimeoutId -> Int
unTimeoutId TimeoutId
nextTmid) ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadLabel
">>")
                             TimeoutState
TimeoutPending
        modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock)
        let expiry  = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
            t       = TVar s TimeoutState -> TimeoutId -> Timeout s
forall s. TVar s TimeoutState -> TimeoutId -> Timeout s
Timeout TVar s TimeoutState
tvar TimeoutId
nextTmid
            timers' = Int -> Time -> TimerCompletionInfo s -> Timeouts s -> Timeouts s
forall p v. Ord p => Int -> p -> v -> IntPSQ p v -> IntPSQ p v
IPSQ.insert (TimeoutId -> Int
forall a b. Coercible a b => a -> b
coerce 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 { threadControl = ThreadControl (k t) ctl }
        trace <- schedule thread' simstate { timers   = timers'
                                           , nextVid  = succ (succ nextVid)
                                           , nextTmid = succ nextTmid }
        return (SimPORTrace time tid tstep tlbl (EventTimerCreated nextTmid (TVarId nextVid) expiry) trace)

      CancelTimeout (Timeout TVar s TimeoutState
tvar TimeoutId
tmid) SimA s b
k -> do
        let timers' :: Timeouts s
timers' = Int -> Timeouts s -> Timeouts s
forall p v. Ord p => Int -> IntPSQ p v -> IntPSQ p v
IPSQ.delete (TimeoutId -> Int
forall a b. Coercible a b => a -> b
coerce TimeoutId
tmid) Timeouts s
timers
        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)
        written' <- mapM someTVarToLabelled written
        (wakeup, wokeby) <- threadsUnblockedByWrites written
        mapM_ (\(SomeTVar TVar s a
var) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar s a
var) written
        let effect' = Effect
effect
                   Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [Labelled (SomeTVar s)] -> Effect
forall s. [Labelled (SomeTVar s)] -> Effect
writeEffects [Labelled (SomeTVar s)]
written'
                   Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [IOSimThreadId] -> Effect
wakeupEffects [IOSimThreadId]
wakeup
            thread' = Thread s a
thread { threadControl = ThreadControl k ctl
                             , threadEffect  = effect'
                             }
            (unblocked,
             simstate') = unblockThreads False vClock wakeup simstate
        modifySTRef (tvarVClock tvar)  (leastUpperBoundVClock vClock)
        !trace <- deschedule Yield thread' simstate' { timers = timers' }
        return $ SimPORTrace time tid tstep tlbl (EventTimerCancelled tmid)
               $ traceMany
                   -- TODO: step
                   [ (time, tid', (-1), tlbl', EventTxWakeup vids)
                   | tid' <- unblocked
                   , let 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 vids = Set.toList <$> Map.lookup tid' wokeby ]
               $ SimPORTrace time tid tstep tlbl (EventDeschedule Yield)
               $ trace

      -- cancelling a negative timer is a no-op
      CancelTimeout (NegativeTimeout TimeoutId
_tmid) SimA s b
k -> do
        -- negative timers are promptly removed from the state
        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 nextTId :: Int
nextTId = Thread s a -> Int
forall s a. Thread s a -> Int
threadNextTId Thread s a
thread
            tid' :: IOSimThreadId
tid' | Thread s a -> Bool
forall s a. Thread s a -> Bool
threadRacy Thread s a
thread = IOSimThreadId -> IOSimThreadId
setRacyThread (IOSimThreadId -> IOSimThreadId) -> IOSimThreadId -> IOSimThreadId
forall a b. (a -> b) -> a -> b
$ IOSimThreadId -> Int -> IOSimThreadId
childThreadId IOSimThreadId
tid Int
nextTId
                 | Bool
otherwise         = IOSimThreadId -> Int -> IOSimThreadId
childThreadId IOSimThreadId
tid Int
nextTId
            thread' :: Thread s a
thread'  = Thread s a
thread { threadControl = ThreadControl (k tid') ctl,
                                threadNextTId = nextTId + 1,
                                threadEffect  = effect
                                             <> forkEffect tid'
                                }
            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, VectorClock)]
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
                              , threadStep :: Int
threadStep    = Int
0
                              , threadVClock :: VectorClock
threadVClock  = IOSimThreadId -> Int -> VectorClock -> VectorClock
insertVClock IOSimThreadId
tid' Int
0
                                              (VectorClock -> VectorClock) -> VectorClock -> VectorClock
forall a b. (a -> b) -> a -> b
$ VectorClock
vClock
                              , threadEffect :: Effect
threadEffect  = Effect
forall a. Monoid a => a
mempty
                              , threadRacy :: Bool
threadRacy    = Thread s a -> Bool
forall s a. Thread s a -> Bool
threadRacy Thread s a
thread
                              }
            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
        -- A newly forked thread may have a higher priority, so we deschedule this one.
        !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 { runqueue = insertThread thread'' runqueue
                             , threads  = threads' }
        return $ SimPORTrace time tid tstep tlbl (EventThreadForked tid')
               $ SimPORTrace time tid tstep tlbl (EventDeschedule Yield)
               $ trace

      Atomically STM s a1
a a1 -> SimA s b
k -> Time
-> IOSimThreadId
-> [Labelled IOSimThreadId]
-> Maybe ThreadLabel
-> Int
-> StmA s a1
-> (StmTxResult s a1 -> ST s (SimTrace a))
-> ST s (SimTrace a)
forall s a c.
Time
-> IOSimThreadId
-> [Labelled IOSimThreadId]
-> Maybe ThreadLabel
-> Int
-> StmA s a
-> (StmTxResult s a -> ST s (SimTrace c))
-> ST s (SimTrace c)
execAtomically Time
time IOSimThreadId
tid (Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
forall s a.
Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId]
labelledThreads Map IOSimThreadId (Thread s a)
threads) Maybe ThreadLabel
tlbl Int
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 Int
nextVid' -> do
            (wakeup, 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
            mapM_ (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar s a
tvar) written
            vClockRead <- leastUpperBoundTVarVClocks read
            read' <- mapM someTVarToLabelled read
            written' <- mapM someTVarToLabelled written
            let vClock'     = VectorClock
vClock VectorClock -> VectorClock -> VectorClock
`leastUpperBoundVClock` VectorClock
vClockRead
                effect'     = Effect
effect
                           Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [Labelled (SomeTVar s)] -> Effect
forall s. [Labelled (SomeTVar s)] -> Effect
readEffects [Labelled (SomeTVar s)]
read'
                           Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [Labelled (SomeTVar s)] -> Effect
forall s. [Labelled (SomeTVar s)] -> Effect
writeEffects [Labelled (SomeTVar s)]
written'
                           Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [IOSimThreadId] -> Effect
wakeupEffects [IOSimThreadId]
unblocked
                thread'     = Thread s a
thread { threadControl = ThreadControl (k x) ctl,
                                       threadVClock  = vClock',
                                       threadEffect  = effect' }
                (unblocked,
                 simstate') = unblockThreads True vClock' wakeup simstate
            sequence_ [ modifySTRef (tvarVClock r) (leastUpperBoundVClock vClock')
                      | SomeTVar r <- created ++ written ]
            written'' <- 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) written
            created' <- 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) created
            -- We deschedule a thread after a transaction... another may have woken up.
            !trace <- deschedule Yield thread' simstate' { nextVid  = nextVid' }
            return $
              SimPORTrace time tid tstep tlbl (EventTxCommitted written'' created' (Just effect')) $
              traceMany
                [ (time, tid', (-1), tlbl', EventTxWakeup vids')
                | tid' <- unblocked
                , let 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 vids' = Set.toList <$> Map.lookup tid' wokeby ] $
              traceMany
                [ (time, tid, tstep, tlbl, EventLog tr)
                | tr <- tvarDynamicTraces
                ] $
              traceMany
                [ (time, tid, tstep, tlbl, EventSay str)
                | str <- tvarStringTraces
                ] $
              SimPORTrace time tid tstep tlbl (EventUnblocked unblocked) $
              SimPORTrace time tid tstep tlbl (EventDeschedule Yield) $
                trace

          StmTxAborted [SomeTVar s]
read SomeException
e -> do
            -- schedule this thread to immediately raise the exception
            vClockRead <- [SomeTVar s] -> ST s VectorClock
forall s. [SomeTVar s] -> ST s VectorClock
leastUpperBoundTVarVClocks [SomeTVar s]
read
            read' <- mapM someTVarToLabelled read
            let effect' = Effect
effect Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [Labelled (SomeTVar s)] -> Effect
forall s. [Labelled (SomeTVar s)] -> Effect
readEffects [Labelled (SomeTVar s)]
read'
                thread' = Thread s a
thread { threadControl = ThreadControl (Throw e) ctl,
                                   threadVClock  = vClock `leastUpperBoundVClock` vClockRead,
                                   threadEffect  = effect' }
            trace <- schedule thread' simstate
            return $ SimPORTrace time tid tstep tlbl (EventTxAborted (Just effect'))
                   $ 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
            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
            vClockRead <- leastUpperBoundTVarVClocks read
            read' <- mapM someTVarToLabelled read
            let effect' = Effect
effect Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [Labelled (SomeTVar s)] -> Effect
forall s. [Labelled (SomeTVar s)] -> Effect
readEffects [Labelled (SomeTVar s)]
read'
                thread' = Thread s a
thread { threadVClock  = vClock `leastUpperBoundVClock` vClockRead,
                                   threadEffect  = effect' }
            !trace <- deschedule (Blocked BlockedOnSTM) thread' simstate
            return $ SimPORTrace time tid tstep tlbl (EventTxBlocked vids (Just effect'))
                   $ SimPORTrace time tid tstep tlbl (EventDeschedule (Blocked BlockedOnSTM))
                   $ 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

      GetThreadLabel IOSimThreadId
tid' Maybe ThreadLabel -> SimA s b
k -> do
        let tlbl' :: Maybe ThreadLabel
tlbl' | IOSimThreadId
tid' IOSimThreadId -> IOSimThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== IOSimThreadId
tid = Maybe ThreadLabel
tlbl
                  | Bool
otherwise   = 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
                              Maybe (Thread s a)
-> (Thread s a -> Maybe ThreadLabel) -> Maybe ThreadLabel
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Thread s a -> Maybe ThreadLabel
forall s a. Thread s a -> Maybe ThreadLabel
threadLabel
            thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (k tlbl') 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 -> 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' }

      ExploreRaces SimA s b
k -> do
        let thread' :: Thread s a
thread'  = Thread s a
thread { threadControl = ThreadControl k ctl
                              , threadRacy    = True }
        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

      Fix x -> IOSim s x
f x -> SimA s b
k -> do
        r <- x -> ST s (STRef s x)
forall a s. a -> ST s (STRef s a)
newSTRef (NonTermination -> x
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw NonTermination
NonTermination)
        x <- unsafeInterleaveST $ readSTRef r
        let 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 { threadControl = ThreadControl k' ctl }
        schedule thread' simstate

      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' }
        trace <-
          case MaskingState
maskst' of
            -- If we're now unmasked then check for any pending async exceptions
            MaskingState
Unmasked -> Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep 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
        return $ SimPORTrace time tid tstep tlbl (EventMask maskst')
               $ trace

      ThrowTo SomeException
e IOSimThreadId
tid' SimA s b
_ | IOSimThreadId
tid' IOSimThreadId -> IOSimThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== IOSimThreadId
tid -> do
        -- Throw to ourself is equivalent to a synchronous throw,
        -- and works irrespective of masking state since it does not block.
        let thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Throw e) ctl
                             , threadEffect  = effect
                             }
        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
        return (SimPORTrace time tid tstep tlbl (EventThrowTo e tid) 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,
                                  threadEffect  = effect <> throwToEffect tid'
                                                         <> wakeUpEffect,
                                  threadVClock  = vClock `leastUpperBoundVClock` vClockTgt
                                }
            (VectorClock
vClockTgt,
             Effect
wakeUpEffect,
             Bool
willBlock) = (Thread s a -> VectorClock
forall s a. Thread s a -> VectorClock
threadVClock Thread s a
t,
                           if Thread s a -> Bool
forall s a. Thread s a -> Bool
isThreadBlocked Thread s a
t then [IOSimThreadId] -> Effect
wakeupEffects [IOSimThreadId
tid'] else Effect
forall a. Monoid a => a
mempty,
                           Bool -> Bool
not (Thread s a -> Bool
forall s a. Thread s a -> Bool
threadInterruptible Thread s a
t Bool -> Bool -> Bool
|| Thread s a -> Bool
forall s a. Thread s a -> Bool
isThreadDone Thread s a
t))
              where Just Thread s a
t = 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

        if Bool
willBlock
          then do
            -- The target thread has async exceptions masked so we add the
            -- exception and the source thread id to the pending async exceptions.
            let adjustTarget :: Thread s a -> Thread s a
adjustTarget Thread s a
t =
                  Thread s a
t { threadThrowTo = (e, Labelled tid tlbl, vClock) : 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
            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' }
            return $ SimPORTrace time tid tstep tlbl (EventThrowTo e tid')
                   $ SimPORTrace time tid tstep tlbl EventThrowToBlocked
                   $ SimPORTrace time tid tstep tlbl (EventDeschedule (Blocked BlockedOnThrowTo))
                   $ trace
          else do
            -- The target thread has async exceptions unmasked, or is masked but
            -- is blocked (and all blocking operations are interruptible) then we
            -- raise the exception in that thread immediately. This will either
            -- cause it to terminate or enter an exception handler.
            -- In the meantime the thread masks new async exceptions. This will
            -- be resolved if the thread terminates or if it leaves the exception
            -- handler (when restoring the masking state would trigger the any
            -- new pending async exception).
            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',
                                       threadVClock :: forall s a. Thread s a -> VectorClock
threadVClock  = VectorClock
vClock' } =
                  Thread s a
t { threadControl = ThreadControl (Throw e) ctl'
                    , threadStatus  = if isThreadDone t
                                      then threadStatus t
                                      else ThreadRunning
                    , threadVClock  = vClock' `leastUpperBoundVClock` vClock }
                ([IOSimThreadId]
_unblocked, 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' }) = Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
False VectorClock
vClock [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'' }

            -- We yield at this point because the target thread may be higher
            -- priority, so this should be a step for race detection.
            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''
            return $ SimPORTrace time tid tstep tlbl (EventThrowTo e tid')
                   $ trace

      -- intentionally a no-op (at least for now)
      YieldSim 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

      NewUnique Unique s -> SimA s b
k -> do
        let thread' :: Thread s a
thread'   = Thread s a
thread{ threadControl = ThreadControl (k nextUniq) ctl }
            n :: Integer
n         = Unique s -> Integer
forall {k} (s :: k). Unique s -> Integer
unMkUnique Unique s
nextUniq
            simstate' :: SimState s a
simstate' = SimState s a
simstate{ nextUniq = MkUnique (n + 1) }
        Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Integer -> SimEventType
EventUniqueCreated Integer
n)
          (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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  -- blocking operations are interruptible
        | Bool
otherwise              -> Bool
False
      MaskingState
MaskedUninterruptible      -> Bool
False


-- | Deschedule a thread.
--
-- A thread is descheduled, which marks a boundary of a `Step` when:
--
-- * forking a new thread
-- * thread termination
-- * setting the masking state to interruptible
-- * popping masking frame (which resets masking state)
-- * starting or cancelling a timeout
-- * thread delays
-- * on committed or blocked, but not aborted STM transactions
-- * on blocking or non-blocking `throwTo`
-- * unhandled exception in a (non-main) thread
--
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 :: Thread s a
thread@Thread { threadId :: forall s a. Thread s a -> IOSimThreadId
threadId     = IOSimThreadId
tid,
                                 threadStep :: forall s a. Thread s a -> Int
threadStep   = Int
tstep,
                                 threadLabel :: forall s a. Thread s a -> Maybe ThreadLabel
threadLabel  = Maybe ThreadLabel
tlbl,
                                 threadVClock :: forall s a. Thread s a -> VectorClock
threadVClock = VectorClock
vClock }
                 simstate :: SimState s a
simstate@SimState{RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue :: RunQueue
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,
                                   curTime :: forall s a. SimState s a -> Time
curTime  = Time
time,
                                   ScheduleControl
control :: forall s a. SimState s a -> ScheduleControl
control :: ScheduleControl
control } =

    -- We don't interrupt runnable threads anywhere else.
    -- We do it here by inserting the current thread into the runqueue in priority order.

    let (Thread s a
thread', Effect
eff) = Thread s a -> (Thread s a, Effect)
forall s a. Thread s a -> (Thread s a, Effect)
stepThread Thread s a
thread
        runqueue' :: RunQueue
runqueue'      = Thread s a -> RunQueue -> RunQueue
forall s a. Thread s a -> RunQueue -> RunQueue
insertThread Thread s a
thread' RunQueue
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 IOSimThreadId
tid Thread s a
thread' Map IOSimThreadId (Thread s a)
threads
        control' :: ScheduleControl
control'       = StepId -> ScheduleControl -> ScheduleControl
advanceControl (Thread s a -> StepId
forall s a. Thread s a -> StepId
threadStepId Thread s a
thread) ScheduleControl
control
        races' :: Races
races'         = Thread s a -> SimState s a -> Races
forall s a. Thread s a -> SimState s a -> Races
updateRaces Thread s a
thread SimState s a
simstate in

    Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (VectorClock -> Effect -> SimEventType
EventEffect VectorClock
vClock Effect
eff) (SimTrace a -> SimTrace a)
-> (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Races -> SimEventType
EventRaces Races
races') (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    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',
                          races    = races',
                          control  = control' }

deschedule Deschedule
Interruptable thread :: Thread s a
thread@Thread {
                           threadId :: forall s a. Thread s a -> IOSimThreadId
threadId      = IOSimThreadId
tid,
                           threadStep :: forall s a. Thread s a -> Int
threadStep    = Int
tstep,
                           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, VectorClock)]
threadThrowTo = (SomeException
e, Labelled IOSimThreadId
tid', VectorClock
vClock') : [(SomeException, Labelled IOSimThreadId, VectorClock)]
etids,
                           threadLabel :: forall s a. Thread s a -> Maybe ThreadLabel
threadLabel   = Maybe ThreadLabel
tlbl,
                           threadVClock :: forall s a. Thread s a -> VectorClock
threadVClock  = VectorClock
vClock,
                           threadEffect :: forall s a. Thread s a -> Effect
threadEffect  = Effect
effect
                         }
                        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 } = do

    let effect' :: Effect
effect' = Effect
effect Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [IOSimThreadId] -> Effect
wakeupEffects [IOSimThreadId]
unblocked
        -- We're unmasking, but there are pending blocked async exceptions.
        -- So immediately raise the exception and unblock the blocked thread
        -- if possible.
        thread' :: Thread s a
thread' = Thread s a
thread { threadControl = ThreadControl (Throw e) ctl
                         , threadMasking = MaskedInterruptible
                         , threadThrowTo = etids
                         , threadVClock  = vClock `leastUpperBoundVClock` vClock'
                         , threadEffect  = effect'
                         }
        ([IOSimThreadId]
unblocked,
         SimState s a
simstate') = Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
False VectorClock
vClock [Labelled IOSimThreadId -> IOSimThreadId
forall a. Labelled a -> a
l_labelled Labelled IOSimThreadId
tid'] SimState s a
simstate
    -- the thread is stepped when we Yield
    !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'
    return $ SimPORTrace time tid tstep tlbl (EventThrowToUnmasked tid')
           $ SimPORTrace time tid tstep tlbl (EventEffect vClock effect')
           -- TODO: step
           $ traceMany [ (time, tid'', (-1), tlbl'', EventThrowToWakeup)
                       | tid'' <- unblocked
                       , let 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 ]
           $ SimPORTrace time tid tstep tlbl (EventDeschedule Yield)
             trace

deschedule Deschedule
Interruptable thread :: Thread s a
thread@Thread{threadId :: forall s a. Thread s a -> IOSimThreadId
threadId     = IOSimThreadId
tid,
                                       threadStep :: forall s a. Thread s a -> Int
threadStep   = Int
tstep,
                                       threadLabel :: forall s a. Thread s a -> Maybe ThreadLabel
threadLabel  = Maybe ThreadLabel
tlbl,
                                       threadVClock :: forall s a. Thread s a -> VectorClock
threadVClock = VectorClock
vClock}
                         simstate :: SimState s a
simstate@SimState{ ScheduleControl
control :: forall s a. SimState s a -> ScheduleControl
control :: ScheduleControl
control,
                                            curTime :: forall s a. SimState s a -> Time
curTime = Time
time } =
    -- Either masked or unmasked but no pending async exceptions.
    -- Either way, just carry on.
    -- Record a step, though, in case on replay there is an async exception.
    let (Thread s a
thread', Effect
eff) = Thread s a -> (Thread s a, Effect)
forall s a. Thread s a -> (Thread s a, Effect)
stepThread Thread s a
thread
        races' :: Races
races' = Thread s a -> SimState s a -> Races
forall s a. Thread s a -> SimState s a -> Races
updateRaces Thread s a
thread SimState s a
simstate in

    Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (VectorClock -> Effect -> SimEventType
EventEffect VectorClock
vClock Effect
eff) (SimTrace a -> SimTrace a)
-> (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Races -> SimEventType
EventRaces Races
races') (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    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{ races   = races',
                       control = advanceControl (threadStepId thread) control }

deschedule (Blocked BlockedReason
_blockedReason) thread :: Thread s a
thread@Thread { threadId :: forall s a. Thread s a -> IOSimThreadId
threadId      = IOSimThreadId
tid
                                                  , threadStep :: forall s a. Thread s a -> Int
threadStep    = Int
tstep
                                                  , threadLabel :: forall s a. Thread s a -> Maybe ThreadLabel
threadLabel   = Maybe ThreadLabel
tlbl
                                                  , threadThrowTo :: forall s a.
Thread s a
-> [(SomeException, Labelled IOSimThreadId, VectorClock)]
threadThrowTo = (SomeException, Labelled IOSimThreadId, VectorClock)
_ : [(SomeException, Labelled IOSimThreadId, VectorClock)]
_
                                                  , threadMasking :: forall s a. Thread s a -> MaskingState
threadMasking = MaskingState
maskst
                                                  , threadEffect :: forall s a. Thread s a -> Effect
threadEffect  = Effect
effect }
                                    simstate :: SimState s a
simstate@SimState{ curTime :: forall s a. SimState s a -> Time
curTime = Time
time }
    | MaskingState
maskst MaskingState -> MaskingState -> Bool
forall a. Eq a => a -> a -> Bool
/= MaskingState
MaskedUninterruptible =
    -- We're doing a blocking operation, which is an interrupt point even if
    -- we have async exceptions masked, and there are pending blocked async
    -- exceptions. So immediately raise the exception and unblock the blocked
    -- thread if possible.
    Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep 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 { threadMasking = Unmasked } SimState s a
simstate

deschedule (Blocked BlockedReason
blockedReason) thread :: Thread s a
thread@Thread{ threadId :: forall s a. Thread s a -> IOSimThreadId
threadId     = IOSimThreadId
tid,
                                                  threadStep :: forall s a. Thread s a -> Int
threadStep   = Int
tstep,
                                                  threadLabel :: forall s a. Thread s a -> Maybe ThreadLabel
threadLabel  = Maybe ThreadLabel
tlbl,
                                                  threadVClock :: forall s a. Thread s a -> VectorClock
threadVClock = VectorClock
vClock}
                                   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,
                                                      curTime :: forall s a. SimState s a -> Time
curTime = Time
time,
                                                      ScheduleControl
control :: forall s a. SimState s a -> ScheduleControl
control :: ScheduleControl
control } =
    let thread1 :: Thread s a
thread1        = Thread s a
thread { threadStatus = ThreadBlocked blockedReason }
        (Thread s a
thread', Effect
eff) = Thread s a -> (Thread s a, Effect)
forall s a. Thread s a -> (Thread s a, Effect)
stepThread Thread s a
thread1
        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
        races' :: Races
races'         = Thread s a -> SimState s a -> Races
forall s a. Thread s a -> SimState s a -> Races
updateRaces Thread s a
thread1 SimState s a
simstate in

    Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (VectorClock -> Effect -> SimEventType
EventEffect VectorClock
vClock Effect
eff) (SimTrace a -> SimTrace a)
-> (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Races -> SimEventType
EventRaces Races
races') (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    SimState s a -> ST s (SimTrace a)
forall s a. SimState s a -> ST s (SimTrace a)
reschedule SimState s a
simstate { threads = threads',
                          races   = races',
                          control = advanceControl (threadStepId thread1) control }

deschedule Deschedule
Terminated thread :: Thread s a
thread@Thread { threadId :: forall s a. Thread s a -> IOSimThreadId
threadId = IOSimThreadId
tid, threadStep :: forall s a. Thread s a -> Int
threadStep = Int
tstep, threadLabel :: forall s a. Thread s a -> Maybe ThreadLabel
threadLabel = Maybe ThreadLabel
tlbl,
                                      threadVClock :: forall s a. Thread s a -> VectorClock
threadVClock = VectorClock
vClock, threadEffect :: forall s a. Thread s a -> Effect
threadEffect = Effect
effect }
                               simstate :: SimState s a
simstate@SimState{ curTime :: forall s a. SimState s a -> Time
curTime = Time
time, ScheduleControl
control :: forall s a. SimState s a -> ScheduleControl
control :: ScheduleControl
control } = do
    -- This thread is done. If there are other threads blocked in a
    -- ThrowTo targeted at this thread then we can wake them up now.
    let wakeup :: [IOSimThreadId]
wakeup         = ((SomeException, Labelled IOSimThreadId, VectorClock)
 -> IOSimThreadId)
-> [(SomeException, Labelled IOSimThreadId, VectorClock)]
-> [IOSimThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeException
_,Labelled IOSimThreadId
tid',VectorClock
_) -> Labelled IOSimThreadId -> IOSimThreadId
forall a. Labelled a -> a
l_labelled Labelled IOSimThreadId
tid') ([(SomeException, Labelled IOSimThreadId, VectorClock)]
-> [(SomeException, Labelled IOSimThreadId, VectorClock)]
forall a. [a] -> [a]
reverse (Thread s a
-> [(SomeException, Labelled IOSimThreadId, VectorClock)]
forall s a.
Thread s a
-> [(SomeException, Labelled IOSimThreadId, VectorClock)]
threadThrowTo Thread s a
thread))
        ([IOSimThreadId]
unblocked,
         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}) =
                      Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
False VectorClock
vClock [IOSimThreadId]
wakeup SimState s a
simstate
        effect' :: Effect
effect'        = Effect
effect Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [IOSimThreadId] -> Effect
wakeupEffects [IOSimThreadId]
unblocked
        (Thread s a
thread', Effect
eff) = Thread s a -> (Thread s a, Effect)
forall s a. Thread s a -> (Thread s a, Effect)
stepThread (Thread s a -> (Thread s a, Effect))
-> Thread s a -> (Thread s a, Effect)
forall a b. (a -> b) -> a -> b
$ Thread s a
thread { threadStatus = ThreadDone,
                                               threadEffect = effect' }
        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
        races' :: Races
races'         = IOSimThreadId -> Races -> Races
threadTerminatesRaces IOSimThreadId
tid (Races -> Races) -> Races -> Races
forall a b. (a -> b) -> a -> b
$ Thread s a -> SimState s a -> Races
forall s a. Thread s a -> SimState s a -> Races
updateRaces Thread s a
thread { threadEffect = effect' } SimState s a
simstate
    -- We must keep terminated threads in the state to preserve their vector clocks,
    -- which matters when other threads throwTo them.
    !trace <- SimState s a -> ST s (SimTrace a)
forall s a. SimState s a -> ST s (SimTrace a)
reschedule SimState s a
simstate' { races   = races',
                                     control = advanceControl (threadStepId thread) control,
                                     threads = threads' }
    return $ traceMany
               -- TODO: step
               [ (time, tid', (-1), tlbl', EventThrowToWakeup)
               | tid' <- unblocked
               , let 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 ]
          $ SimPORTrace time tid tstep tlbl (EventEffect vClock eff)
          $ SimPORTrace time tid tstep tlbl (EventRaces races')
            trace

deschedule Deschedule
Sleep thread :: Thread s a
thread@Thread { threadId :: forall s a. Thread s a -> IOSimThreadId
threadId = IOSimThreadId
tid , threadEffect :: forall s a. Thread s a -> Effect
threadEffect = Effect
effect' }
                 simstate :: SimState s a
simstate@SimState{RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue :: RunQueue
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} =

    -- Schedule control says we should run a different thread. Put
    -- this one to sleep without recording a step.

    let runqueue' :: RunQueue
runqueue' = Thread s a -> RunQueue -> RunQueue
forall s a. Thread s a -> RunQueue -> RunQueue
insertThread Thread s a
thread RunQueue
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 IOSimThreadId
tid 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' }


-- Choose the next thread to run.
reschedule :: SimState s a -> ST s (SimTrace a)

-- If we are following a controlled schedule, just do that.
reschedule :: forall s a. SimState s a -> ST s (SimTrace a)
reschedule simstate :: SimState s a
simstate@SimState { RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue :: RunQueue
runqueue, control :: forall s a. SimState s a -> ScheduleControl
control = control :: ScheduleControl
control@(ControlFollow ((IOSimThreadId
tid,Int
_):[StepId]
_) [ScheduleMod]
_) }
                             | Bool -> Bool
not (IOSimThreadId -> Down IOSimThreadId
forall a. a -> Down a
Down IOSimThreadId
tid Down IOSimThreadId -> RunQueue -> Bool
forall k p v.
(Hashable k, Ord k, Ord p) =>
k -> HashPSQ k p v -> Bool
`PSQ.member` RunQueue
runqueue) =
    SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimResult a -> SimTrace a
forall a b. a -> Trace a b
Trace.Nil (ThreadLabel -> SimResult a
forall a. ThreadLabel -> SimResult a
InternalError (ThreadLabel
"assertion failure: " ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ IOSimThreadId -> ThreadLabel
ppIOSimThreadId IOSimThreadId
tid ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadLabel
" not runnable")))

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, control :: forall s a. SimState s a -> ScheduleControl
control = control :: ScheduleControl
control@(ControlFollow ((IOSimThreadId
tid,Int
_):[StepId]
_) [ScheduleMod]
_) }
                             | Bool -> Bool
not (IOSimThreadId
tid 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) =
    SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimResult a -> SimTrace a
forall a b. a -> Trace a b
Trace.Nil (ThreadLabel -> SimResult a
forall a. ThreadLabel -> SimResult a
InternalError (ThreadLabel
"assertion failure: " ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ IOSimThreadId -> ThreadLabel
ppIOSimThreadId IOSimThreadId
tid ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadLabel
" not in threads")))

reschedule simstate :: SimState s a
simstate@SimState { RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue :: RunQueue
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,
                               control :: forall s a. SimState s a -> ScheduleControl
control = control :: ScheduleControl
control@(ControlFollow ((IOSimThreadId
tid,Int
tstep):[StepId]
_) [ScheduleMod]
_),
                               curTime :: forall s a. SimState s a -> Time
curTime = Time
time } =
    (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall a b. (a -> b) -> ST s a -> ST s b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
forall a. Maybe a
Nothing (ScheduleControl -> SimEventType
EventReschedule ScheduleControl
control)) (ST s (SimTrace a) -> ST s (SimTrace a))
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$
    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 Maybe (Thread s a)
forall a. Maybe a
Nothing 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
$
    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
    Bool -> ST s (SimTrace a) -> ST s (SimTrace a)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
thread IOSimThreadId -> IOSimThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== IOSimThreadId
tid) (ST s (SimTrace a) -> ST s (SimTrace a))
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$
    --assert (threadStep thread == tstep) $
    if Thread s a -> Int
forall s a. Thread s a -> Int
threadStep Thread s a
thread Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
tstep then
      ThreadLabel -> ST s (SimTrace a)
forall a. (?callStack::CallStack) => ThreadLabel -> a
error (ThreadLabel -> ST s (SimTrace a))
-> ThreadLabel -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ ThreadLabel
"Thread step out of sync\n"
           ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadLabel
"  runqueue:    "ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++RunQueue -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show RunQueue
runqueueThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ThreadLabel
"\n"
           ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadLabel
"  follows:     "ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++IOSimThreadId -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show IOSimThreadId
tidThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ThreadLabel
", step "ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++Int -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show Int
tstepThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ThreadLabel
"\n"
           ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadLabel
"  actual step: "ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++Int -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show (Thread s a -> Int
forall s a. Thread s a -> Int
threadStep Thread s a
thread)ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ThreadLabel
"\n"
           ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadLabel
"Thread:\n" ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ Thread s a -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show Thread s a
thread ThreadLabel -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadLabel
"\n"
    else
    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 = PSQ.delete (Down tid) runqueue
                             , threads  = Map.delete tid threads }

-- When there is no current running thread but the runqueue is non-empty then
-- schedule the next one to run.
reschedule simstate :: SimState s a
simstate@SimState{ RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue :: RunQueue
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 (Down !IOSimThreadId
tid, Down IOSimThreadId
_, ()
_, RunQueue
runqueue') <- RunQueue
-> Maybe (Down IOSimThreadId, Down IOSimThreadId, (), RunQueue)
forall k p v.
(Hashable k, Ord k, Ord p) =>
HashPSQ k p v -> Maybe (k, p, v, HashPSQ k p v)
PSQ.minView RunQueue
runqueue =
    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 Maybe (Thread s a)
forall a. Maybe a
Nothing 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
$

    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 }

-- But when there are no runnable threads, we advance the time to the next
-- timer event, or stop.
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, Races
races :: forall s a. SimState s a -> Races
races :: Races
races } =
    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 Maybe (Thread s a)
forall a. Maybe a
Nothing 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
$

    -- time is moving on
    --Debug.trace ("Rescheduling at "++show time++", "++
      --show (length (concatMap stepInfoRaces (activeRaces races++completeRaces races)))++" races") $

    -- important to get all events that expire at this time
    case Timeouts s
-> Maybe ([TimeoutId], Time, [TimerCompletionInfo s], Timeouts s)
forall k p a.
(Coercible Int k, Ord p) =>
IntPSQ p a -> Maybe ([k], p, [a], IntPSQ 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 (SimState s a -> SimTrace a -> SimTrace a
forall s a. SimState s a -> SimTrace a -> SimTrace a
traceFinalRacesFound SimState s a
simstate (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
                         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

        -- Reuse the STM functionality here to write all the timer TVars.
        -- Simplify to a special case that only reads and writes TVars.
        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 (IOSim s) ()
TimerCompletionInfo s -> STM s ()
forall {m :: * -> *} {s}.
(TVar m ~ TVar s, MonadSTM m) =>
TimerCompletionInfo s -> STM m ()
timeoutAction [TimerCompletionInfo s]
fired)
        !ds  <- traverse (\(SomeTVar TVar s a
tvar) -> do
                            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
                            !_ <- commitTVar tvar
                            return tr) written
        (wakeupSTM, wokeby) <- threadsUnblockedByWrites written
        mapM_ (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar s a
tvar) written

        let wakeupThreadDelay = [ (IOSimThreadId
tid, TimeoutId
tmid) | TimerThreadDelay IOSimThreadId
tid TimeoutId
tmid <- [TimerCompletionInfo s]
fired ]
            -- TODO: the vector clock below cannot be right, can it?
            !simstate'        =
                ([IOSimThreadId], SimState s a) -> SimState s a
forall a b. (a, b) -> b
snd (([IOSimThreadId], SimState s a) -> SimState s a)
-> (SimState s a -> ([IOSimThreadId], SimState s a))
-> SimState s a
-> SimState s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
False VectorClock
bottomVClock ((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)
              (SimState s a -> ([IOSimThreadId], SimState s a))
-> (SimState s a -> SimState s a)
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([IOSimThreadId], SimState s a) -> SimState s a
forall a b. (a, b) -> b
snd (([IOSimThreadId], SimState s a) -> SimState s a)
-> (SimState s a -> ([IOSimThreadId], SimState s a))
-> SimState s a
-> SimState s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
forall s a.
Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads Bool
True  VectorClock
bottomVClock [IOSimThreadId]
wakeupSTM
              (SimState s a -> SimState s a) -> SimState s a -> SimState s a
forall a b. (a -> b) -> a -> b
$ SimState s a
simstate

            -- For each 'timeout' action where the timeout has fired, start a
            -- new thread to execute throwTo to interrupt the action.
            !timeoutExpired = [ (IOSimThreadId
tid, TimeoutId
tmid, TMVar (IOSim s) IOSimThreadId
TMVarDefault (IOSim s) IOSimThreadId
lock)
                              | TimerTimeout IOSimThreadId
tid TimeoutId
tmid TMVar (IOSim s) IOSimThreadId
lock <- [TimerCompletionInfo s]
fired ]

        -- all open races will be completed and reported at this time
        !simstate'' <- forkTimeoutInterruptThreads timeoutExpired
                                                   simstate' { races = noRaces }
        !trace <- reschedule simstate'' { curTime = time'
                                        , timers  = timers' }
        let traceEntries =
                     [ ( Time
time', [Int] -> IOSimThreadId
ThreadId [-Int
1], -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, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ ( Time
time', [Int] -> IOSimThreadId
ThreadId [-Int
1], -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, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ (Time
time', [Int] -> IOSimThreadId
ThreadId [-Int
1], -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, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ (Time
time', [Int] -> IOSimThreadId
ThreadId [-Int
1], -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, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ (Time
time', IOSimThreadId
tid', -Int
1, 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, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ ( Time
time', IOSimThreadId
tid, -Int
1, 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, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ ( Time
time', IOSimThreadId
tid, -Int
1, 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, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ ( Time
time', IOSimThreadId
tid, -Int
1, ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"forked thread"
                       , IOSimThreadId -> SimEventType
EventThreadForked IOSimThreadId
tid)
                     | (IOSimThreadId
tid, TimeoutId
_, TMVarDefault (IOSim s) IOSimThreadId
_) <- [(IOSimThreadId, TimeoutId, TMVarDefault (IOSim s) IOSimThreadId)]
timeoutExpired ]

        return $
          traceFinalRacesFound simstate $
          traceMany traceEntries trace
  where
    timeoutAction :: TimerCompletionInfo s -> STM m ()
timeoutAction (Timer TVar s TimeoutState
var) = do
      x <- TVar m TimeoutState -> STM m TimeoutState
forall a. TVar m a -> STM m a
forall (m :: * -> *) a. MonadSTM m => TVar m a -> STM m a
readTVar TVar m TimeoutState
TVar s TimeoutState
var
      case x of
        TimeoutState
TimeoutPending   -> TVar m TimeoutState -> TimeoutState -> STM m ()
forall a. TVar m a -> a -> STM m ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar TVar m TimeoutState
TVar s TimeoutState
var TimeoutState
TimeoutFired
        TimeoutState
TimeoutFired     -> ThreadLabel -> STM m ()
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"MonadTimer(Sim): invariant violation"
        TimeoutState
TimeoutCancelled -> () -> STM m ()
forall a. a -> STM m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    timeoutAction (TimerRegisterDelay TVar s Bool
var) = TVar m Bool -> Bool -> STM m ()
forall a. TVar m a -> a -> STM m ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar TVar m Bool
TVar s Bool
var Bool
True
    timeoutAction (TimerThreadDelay IOSimThreadId
_ TimeoutId
_)   = () -> STM m ()
forall a. a -> STM m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    timeoutAction (TimerTimeout IOSimThreadId
_ TimeoutId
_ TMVar (IOSim s) IOSimThreadId
_)     = () -> STM m ()
forall a. a -> STM m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

unblockThreads :: forall s a.
                  Bool -- ^ `True` if we are blocked on STM
               -> VectorClock
               -> [IOSimThreadId]
               -> SimState s a
               -> ([IOSimThreadId], SimState s a)
unblockThreads :: forall s a.
Bool
-> VectorClock
-> [IOSimThreadId]
-> SimState s a
-> ([IOSimThreadId], SimState s a)
unblockThreads !Bool
onlySTM VectorClock
vClock [IOSimThreadId]
wakeup simstate :: SimState s a
simstate@SimState {RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue :: RunQueue
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} =
    -- To preserve our invariants (that threadBlocked is correct)
    -- we update the runqueue and threads together here
    ( [IOSimThreadId]
unblockedIds
    , SimState s a
simstate { runqueue = foldr insertThread runqueue unblocked,
                 threads  = threads'
               })
  where
    -- can only unblock if the thread exists and is blocked (not running)
    unblocked :: [Thread s a]
    !unblocked :: [Thread s a]
unblocked = [ Thread s a
thread
                 | IOSimThreadId
tid <- [IOSimThreadId]
wakeup
                 , Thread s a
thread <-
                     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 = ThreadStatus
ThreadRunning }
                         -> [ ]
                       Just t :: Thread s a
t@Thread { threadStatus :: forall s a. Thread s a -> ThreadStatus
threadStatus = ThreadBlocked BlockedReason
BlockedOnSTM }
                         -> [Thread s a
t]
                       Just t :: Thread s a
t@Thread { threadStatus :: forall s a. Thread s a -> ThreadStatus
threadStatus = ThreadBlocked BlockedReason
_ }
                         | Bool
onlySTM
                         -> [ ]
                         | Bool
otherwise
                         -> [Thread s a
t]
                       Just   Thread { threadStatus :: forall s a. Thread s a -> ThreadStatus
threadStatus = ThreadStatus
ThreadDone } -> [ ]
                       Maybe (Thread s a)
Nothing -> [ ]
                 ]

    unblockedIds :: [IOSimThreadId]
    !unblockedIds :: [IOSimThreadId]
unblockedIds = (Thread s a -> IOSimThreadId) -> [Thread s a] -> [IOSimThreadId]
forall a b. (a -> b) -> [a] -> [b]
map Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId [Thread s a]
unblocked

    -- and in which case we mark them as now running
    !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,
                                threadVClock = vClock `leastUpperBoundVClock` threadVClock t })))
                   Map IOSimThreadId (Thread s a)
threads [IOSimThreadId]
unblockedIds

-- | This function receives a list of TimerTimeout values that represent threads
-- for which the timeout expired and kills the running thread if needed.
--
-- This function is responsible for the second part of the race condition issue
-- and relates to the 'schedule's 'TimeoutFrame' locking explanation (here is
-- where the assassin threads are launched. So, as explained previously, at this
-- point in code, the timeout expired so we need to interrupt the running
-- thread. If the running thread finished at the same time the timeout expired
-- we have a race condition. To deal with this race condition what we do is
-- look at the lock value. If it is 'Locked' this means that the running thread
-- already finished (or won the race) so we can safely do nothing. Otherwise, if
-- the lock value is 'NotLocked' we need to acquire the lock and launch an
-- assassin thread that is going to interrupt the running one. Note that we
-- should run this interrupting thread in an unmasked state since it might
-- receive a 'ThreadKilled' exception.
--
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{ RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue :: RunQueue
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
            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
            return $ case v of
              Maybe IOSimThreadId
Nothing -> SimState s a
st { runqueue = insertThread t runqueue,
                              threads  = Map.insert (threadId t) t threads
                            }
              Just IOSimThreadId
_  -> SimState s a
st
          )
          SimState s a
simState'
          [(Thread s a, TMVar (IOSim s) IOSimThreadId)]
[(Thread s a, TMVarDefault (IOSim s) IOSimThreadId)]
throwToThread

  where
    -- we launch a thread responsible for throwing an AsyncCancelled exception
    -- to the thread which timeout expired
    throwToThread :: [(Thread s a, TMVar (IOSim s) IOSimThreadId)]

    (SimState s a
simState', [(Thread s a, TMVar (IOSim s) IOSimThreadId)]
[(Thread s a, TMVarDefault (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, TMVar (IOSim s) IOSimThreadId)
-> (SimState s a, (Thread s a, TMVar (IOSim s) IOSimThreadId))
SimState s a
-> (IOSimThreadId, TimeoutId, TMVarDefault (IOSim s) IOSimThreadId)
-> (SimState s a,
    (Thread s a, TMVarDefault (IOSim s) IOSimThreadId))
fn SimState s a
simState [(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)]
[(IOSimThreadId, TimeoutId, TMVarDefault (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
"IOSimPOR: internal error: unknown thread " ThreadLabel -> ShowS
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
              tid' :: IOSimThreadId
tid'     = IOSimThreadId -> Int -> IOSimThreadId
childThreadId IOSimThreadId
tid Int
nextId
           in ( SimState s a
state { threads = Map.insert tid t { threadNextTId = succ nextId } threads }
              , ( 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 () -> SimA s ()) -> IOSim s () -> SimA s ()
forall a b. (a -> b) -> a -> b
$ do
                                 mtid <- IOSim s IOSimThreadId
IOSim s (ThreadId (IOSim s))
forall (m :: * -> *). MonadThread m => m (ThreadId m)
myThreadId
                                 v2 <- atomically $ tryPutTMVar lock mtid
                                 when v2 $
                                   throwTo tid (toException (TimeoutException 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, VectorClock)]
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,
                           threadStep :: Int
threadStep    = Int
0,
                           threadVClock :: VectorClock
threadVClock  = IOSimThreadId -> Int -> VectorClock -> VectorClock
insertVClock IOSimThreadId
tid' Int
0
                                         (VectorClock -> VectorClock) -> VectorClock -> VectorClock
forall a b. (a -> b) -> a -> b
$ Thread s a -> VectorClock
forall s a. Thread s a -> VectorClock
threadVClock Thread s a
t,
                           threadEffect :: Effect
threadEffect  = Effect
forall a. Monoid a => a
mempty,
                           threadRacy :: Bool
threadRacy    = Thread s a -> Bool
forall s a. Thread s a -> Bool
threadRacy Thread s a
t
                         }
                , TMVar (IOSim s) IOSimThreadId
lock
                )
              )


-- | Iterate through the control stack to find an enclosing exception handler
-- of the right type, or unwind all the way to the top level for the thread.
--
-- Also return if it's the main thread or a forked thread since we handle the
-- cases differently.
--
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
timeouts ->
    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
timeouts
  where
    unwind :: forall s' c. MaskingState
           -> ControlStack s' c a
           -> Timeouts s
           -> (Either Bool (Thread s' a), Timeouts 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
        -- not the right type, unwind to the next containing handler
        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

        -- Ok! We will be able to continue the thread with the handler
        -- followed by the continuation after the catch
        Just e
e' -> ( Thread s' a -> Either Bool (Thread s' a)
forall a b. b -> Either a b
Right Thread s a
thread {
                          -- As per async exception rules, the handler is run
                          -- masked
                         threadControl = ThreadControl (handler e')
                                                       (MaskFrame k maskst ctl),
                         threadMasking = atLeastInterruptibleMask maskst
                       }
                   , Timeouts s
timers
                   )

    -- Either Timeout fired or the action threw an exception.
    -- - If Timeout fired, then it was possibly during this thread's execution
    --   so we need to run the continuation with a Nothing value.
    -- - If the timeout action threw an exception we need to keep unwinding the
    --   control stack looking for a handler to this exception.
    unwind MaskingState
maskst (TimeoutFrame TimeoutId
tmid TMVar (IOSim s') IOSimThreadId
isLockedRef 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
          -- Exception came from timeout expiring
          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')
            -- Exception came from a different exception
          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
        -- Remove the timeout associated with the 'TimeoutFrame'.
        timers' :: Timeouts s
timers' = Int -> Timeouts s -> Timeouts s
forall p v. Ord p => Int -> IntPSQ p v -> IntPSQ p v
IPSQ.delete (TimeoutId -> Int
forall a b. Coercible a b => a -> b
coerce 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
        -- Remove the timeout associated with the 'DelayFrame'.
        timers' :: Timeouts s
timers' = Int -> Timeouts s -> Timeouts s
forall p v. Ord p => Int -> IntPSQ p v -> IntPSQ p v
IPSQ.delete (TimeoutId -> Int
forall a b. Coercible a b => a -> b
coerce TimeoutId
tmid) Timeouts s
timers

    atLeastInterruptibleMask :: MaskingState -> MaskingState
    atLeastInterruptibleMask :: MaskingState -> MaskingState
atLeastInterruptibleMask MaskingState
Unmasked = MaskingState
MaskedInterruptible
    atLeastInterruptibleMask MaskingState
ms       = MaskingState
ms


removeMinimums :: (Coercible Int k, Ord p)
               => IntPSQ p a
               -> Maybe ([k], p, [a], IntPSQ p a)
removeMinimums :: forall k p a.
(Coercible Int k, Ord p) =>
IntPSQ p a -> Maybe ([k], p, [a], IntPSQ p a)
removeMinimums = \IntPSQ p a
psq -> Maybe ([Int], p, [a], IntPSQ p a)
-> Maybe ([k], p, [a], IntPSQ p a)
forall a b. Coercible a b => a -> b
coerce (Maybe ([Int], p, [a], IntPSQ p a)
 -> Maybe ([k], p, [a], IntPSQ p a))
-> Maybe ([Int], p, [a], IntPSQ p a)
-> Maybe ([k], p, [a], IntPSQ p a)
forall a b. (a -> b) -> a -> b
$
    case IntPSQ p a -> Maybe (Int, p, a, IntPSQ p a)
forall p v. Ord p => IntPSQ p v -> Maybe (Int, p, v, IntPSQ p v)
IPSQ.minView IntPSQ p a
psq of
      Maybe (Int, p, a, IntPSQ p a)
Nothing              -> Maybe ([Int], p, [a], IntPSQ p a)
forall a. Maybe a
Nothing
      Just (Int
k, p
p, a
x, IntPSQ p a
psq') -> ([Int], p, [a], IntPSQ p a) -> Maybe ([Int], p, [a], IntPSQ p a)
forall a. a -> Maybe a
Just ([Int] -> p -> [a] -> IntPSQ p a -> ([Int], p, [a], IntPSQ p a)
forall {b} {a}.
Ord b =>
[Int] -> b -> [a] -> IntPSQ b a -> ([Int], b, [a], IntPSQ b a)
collectAll [Int
k] p
p [a
x] IntPSQ p a
psq')
  where
    collectAll :: [Int] -> b -> [a] -> IntPSQ b a -> ([Int], b, [a], IntPSQ b a)
collectAll [Int]
ks b
p [a]
xs IntPSQ b a
psq =
      case IntPSQ b a -> Maybe (Int, b, a, IntPSQ b a)
forall p v. Ord p => IntPSQ p v -> Maybe (Int, p, v, IntPSQ p v)
IPSQ.minView IntPSQ b a
psq of
        Just (Int
k, b
p', a
x, IntPSQ b a
psq')
          | b
p b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
p' -> [Int] -> b -> [a] -> IntPSQ b a -> ([Int], b, [a], IntPSQ b a)
collectAll (Int
kInt -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[Int]
ks) b
p (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) IntPSQ b a
psq'
        Maybe (Int, b, a, IntPSQ b a)
_           -> ([Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
ks, b
p, [a] -> [a]
forall a. [a] -> [a]
reverse [a]
xs, IntPSQ b a
psq)

traceMany :: [(SI.Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
          -> SimTrace a -> SimTrace a
traceMany :: forall a.
[(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany []                                   SimTrace a
trace = SimTrace a
trace
traceMany ((Time
time, IOSimThreadId
tid, Int
tstep, Maybe ThreadLabel
tlbl, SimEventType
event):[(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
ts) SimTrace a
trace =
    Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time IOSimThreadId
tid Int
tstep Maybe ThreadLabel
tlbl SimEventType
event ([(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany [(Time, IOSimThreadId, Int, 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)


-- | The most general method of running 'IOSim' is in 'ST' monad.  One can
-- recover failures or the result from 'SimTrace' with 'traceResult', or access
-- 'TraceEvent's generated by the computation with 'traceEvents'.  A slightly
-- more convenient way is exposed by 'runSimTrace'.
--
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 = Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST Maybe Int
forall a. Maybe a
Nothing ScheduleControl
ControlDefault IOSim s a
mainAction

controlSimTraceST :: Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST :: forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST Maybe Int
limit ScheduleControl
control IOSim s a
mainAction =
  Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace (SimState (ZonkAny 1) (ZonkAny 0) -> Time
forall s a. SimState s a -> Time
curTime SimState (ZonkAny 1) (ZonkAny 0)
forall s a. SimState s a
initialState)
              (Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
mainThread)
              Int
0
              (Thread s a -> Maybe ThreadLabel
forall s a. Thread s a -> Maybe ThreadLabel
threadLabel Thread s a
mainThread)
              (ScheduleControl -> SimEventType
EventSimStart ScheduleControl
control)
  (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 { control  = control,
                                         control0 = control,
                                         perStepTimeLimit = limit
                                       }
  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, VectorClock)]
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,
        threadStep :: Int
threadStep    = Int
0,
        threadVClock :: VectorClock
threadVClock  = IOSimThreadId -> Int -> VectorClock -> VectorClock
insertVClock ([Int] -> IOSimThreadId
ThreadId []) Int
0 VectorClock
bottomVClock,
        threadEffect :: Effect
threadEffect  = Effect
forall a. Monoid a => a
mempty,
        threadRacy :: Bool
threadRacy    = Bool
False
      }


--
-- Executing STM Transactions
--

execAtomically :: forall s a c.
                  SI.Time
               -> IOSimThreadId
               -> [Labelled IOSimThreadId]
               -> Maybe ThreadLabel
               -> VarId
               -> StmA s a
               -> (StmTxResult s a -> ST s (SimTrace c))
               -> ST s (SimTrace c)
execAtomically :: forall s a c.
Time
-> IOSimThreadId
-> [Labelled IOSimThreadId]
-> Maybe ThreadLabel
-> Int
-> StmA s a
-> (StmTxResult s a -> ST s (SimTrace c))
-> ST s (SimTrace c)
execAtomically !Time
time !IOSimThreadId
tid [Labelled IOSimThreadId]
threads !Maybe ThreadLabel
tlbl !Int
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]
-> Int
-> 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]
-> Int
-> 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 [] [] Int
nextVid0 StmA s a
action0
  where
    go :: forall b.
          StmStack s b a
       -> Map TVarId (SomeTVar s)  -- set of vars read
       -> Map TVarId (SomeTVar s)  -- set of vars written
       -> [SomeTVar s]             -- vars written in order (no dups)
       -> [SomeTVar s]             -- vars created in order
       -> VarId                   -- var fresh name supply
       -> 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]
-> Int
-> 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 !Int
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
          -- Trace each created TVar
          !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
          -- Trace & commit each TVar
          !ds' <- Map.elems <$> traverse
                    (\(SomeTVar TVar s a
tvar) -> do
                        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
                        !_ <- commitTVar tvar
                        -- Also assert the data invariant that outside a tx
                        -- the undo stack is empty:
                        undos <- readTVarUndos tvar
                        assert (null undos) $ return tr
                    ) written

          -- Return the vars written, so readers can be unblocked
          k0 $ StmTxCommitted x (reverse writtenSeq)
                                (Map.elems read)
                                (reverse createdSeq)
                                (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)
                                          $ ds ++ ds')
                                (mapMaybe traceString $ ds ++ ds')
                                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
          -- The branch has successfully completed the transaction. Hence,
          -- the alternative branch can be ignored.
          -- Commit the TVars written in this sub-transaction that are also
          -- in the written set of the outer transaction
          !_ <- (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)
          -- Merge the written set of the inner with the outer
          let 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 -> 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] -> [SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a] -> [a]
++ [SomeTVar s]
createdOuterSeq
          -- Skip the orElse right hand and continue with the k continuation
          go ctl' read written' writtenSeq' createdSeq' nextVid (k x)

      ThrowStm SomeException
e ->
        StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> Int
-> SomeException
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> Int
-> SomeException
-> ST s (SimTrace c)
throwStm StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written Int
nextVid SomeException
e

      CatchStm StmA s a1
a SomeException -> StmA s a1
h a1 -> StmA s b
k -> do
        -- Execute the left side in a new frame with an empty written set
        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]
-> Int
-> 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]
-> Int
-> 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 [] [] Int
nextVid StmA s a1
a

      StmA s b
Retry -> do
        -- Always revert all the TVar writes for the retry
        !_ <- (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 ctl of
          StmStack s b a
AtomicallyFrame -> do
            -- Return vars read, so the thread can block on them
            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
            -- Execute the orElse right hand with an empty written set
            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]
-> Int
-> 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]
-> Int
-> 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 [] [] Int
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
            -- Retry makes sense only within a OrElse context. If it is a branch other than
            -- OrElse left side, then bubble up the `retry` to the frame above.
            -- Skip the continuation and propagate the retry into the outer frame
            -- using the written set for the outer frame
            StmStack s b1 a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> Int
-> 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]
-> Int
-> 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 Int
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
        -- Execute the left side in a new frame with an empty written set
        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]
-> Int
-> 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]
-> Int
-> 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 [] [] Int
nextVid StmA s a1
a

      NewTVar Int -> TVarId
mkId !Maybe ThreadLabel
mbLabel x
x TVar s x -> StmA s b
k -> do
        !v <- TVarId -> Maybe ThreadLabel -> x -> ST s (TVar s x)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar (Int -> TVarId
mkId Int
nextVid) Maybe ThreadLabel
mbLabel x
x
        -- record a write to the TVar so we know to update its VClock
        let 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 x -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s x
v) (TVar s x -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s x
v) Map TVarId (SomeTVar s)
written
        -- save the value: it will be committed or reverted
        !_ <- saveTVar v
        go ctl read written' writtenSeq (SomeTVar v : createdSeq) (succ nextVid) (k 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)
        go ctl read written writtenSeq createdSeq nextVid 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)
        go ctl read written writtenSeq createdSeq nextVid 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
            x <- TVar s a1 -> ST s a1
forall s a. TVar s a -> ST s a
execReadTVar TVar s a1
v
            go ctl read written writtenSeq createdSeq nextVid (k x)
        | Bool
otherwise -> do
            x <- TVar s a1 -> ST s a1
forall s a. TVar s a -> ST s a
execReadTVar TVar s a1
v
            let 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
            go ctl read' written writtenSeq createdSeq nextVid (k 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
            go ctl read written writtenSeq createdSeq nextVid k
        | Bool
otherwise -> do
            !_ <- TVar s a1 -> ST s ()
forall s a. TVar s a -> ST s ()
saveTVar TVar s a1
v
            !_ <- execWriteTVar v x
            let 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
            go ctl read written' (SomeTVar v : writtenSeq) createdSeq nextVid k

      SayStm ThreadLabel
msg StmA s b
k -> do
        mbNF <- IO (Either SomeException ThreadLabel)
-> ST s (Either SomeException ThreadLabel)
forall a s. IO a -> ST s a
unsafeIOToST (IO (Either SomeException ThreadLabel)
 -> ST s (Either SomeException ThreadLabel))
-> IO (Either SomeException ThreadLabel)
-> ST s (Either SomeException ThreadLabel)
forall a b. (a -> b) -> a -> b
$ (SomeException -> Maybe SomeException)
-> IO ThreadLabel -> IO (Either SomeException ThreadLabel)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
forall (m :: * -> *) e b a.
(MonadCatch m, Exception e) =>
(e -> Maybe b) -> m a -> m (Either b a)
tryJust (\SomeException
e -> case forall e. Exception e => SomeException -> Maybe e
fromException @SomeAsyncException SomeException
e of
                                          Maybe SomeAsyncException
Nothing -> SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just SomeException
e
                                          Just {} -> Maybe SomeException
forall a. Maybe a
Nothing)
                             (IO ThreadLabel -> IO (Either SomeException ThreadLabel))
-> IO ThreadLabel -> IO (Either SomeException ThreadLabel)
forall a b. (a -> b) -> a -> b
$ ThreadLabel -> IO ThreadLabel
forall a. a -> IO a
forall (m :: * -> *) a. MonadEvaluate m => a -> m a
evaluate (ShowS
forall a. NFData a => a -> a
force ThreadLabel
msg)
        case mbNF of
          Left SomeException
e -> do
            trace <- StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> Int
-> SomeException
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> Int
-> SomeException
-> ST s (SimTrace c)
throwStm StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written Int
nextVid SomeException
e
            -- TODO: step
            return $ SimPORTrace time tid (-1) tlbl (EventSayEvaluationError e)
                   $ trace
          Right ThreadLabel
msg' -> do
            trace <- StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> Int
-> 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]
-> Int
-> 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 Int
nextVid StmA s b
k
            -- TODO: step
            return $ SimPORTrace time tid (-1) tlbl (EventSay msg') trace

      OutputStm x :: Dynamic
x@(Dynamic TypeRep a
_ a
x') StmA s b
k -> do
        mbWHNF <- IO (Either SomeException a) -> ST s (Either SomeException a)
forall a s. IO a -> ST s a
unsafeIOToST (IO (Either SomeException a) -> ST s (Either SomeException a))
-> IO (Either SomeException a) -> ST s (Either SomeException a)
forall a b. (a -> b) -> a -> b
$ (SomeException -> Maybe SomeException)
-> IO a -> IO (Either SomeException a)
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
forall (m :: * -> *) e b a.
(MonadCatch m, Exception e) =>
(e -> Maybe b) -> m a -> m (Either b a)
tryJust (\SomeException
e -> case forall e. Exception e => SomeException -> Maybe e
fromException @SomeAsyncException SomeException
e of
                                            Maybe SomeAsyncException
Nothing -> SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just SomeException
e
                                            Just {} -> Maybe SomeException
forall a. Maybe a
Nothing)
                               (IO a -> IO (Either SomeException a))
-> IO a -> IO (Either SomeException a)
forall a b. (a -> b) -> a -> b
$ a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. MonadEvaluate m => a -> m a
evaluate a
x'
        case mbWHNF of
          Left SomeException
e -> do
            trace <- StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> Int
-> SomeException
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> Int
-> SomeException
-> ST s (SimTrace c)
throwStm StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written Int
nextVid SomeException
e
            -- TODO: step
            return $ SimPORTrace time tid (-1) tlbl (EventLogEvaluationError e)
                   $ trace
          Right {} -> do
            trace <- StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> Int
-> 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]
-> Int
-> 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 Int
nextVid StmA s b
k
            -- TODO: step
            return $ SimPORTrace time tid (-1) tlbl (EventLog x) trace

      LiftSTStm ST s a1
st a1 -> StmA s b
k -> do
        x <- ST s a1 -> ST s a1
forall s a. ST s a -> ST s a
strictToLazyST ST s a1
st
        go ctl read written writtenSeq createdSeq nextVid (k x)

      FixStm x -> STM s x
f x -> StmA s b
k -> do
        r <- x -> ST s (STRef s x)
forall a s. a -> ST s (STRef s a)
newSTRef (NonTermination -> x
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw NonTermination
NonTermination)
        x <- unsafeInterleaveST $ readSTRef r
        let 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')
        go ctl read written writtenSeq createdSeq nextVid 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 ]
                       [TVarId] -> [TVarId] -> [TVarId]
forall a. [a] -> [a] -> [a]
++ [ TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
tvar | SomeTVar TVar s a
tvar <- [SomeTVar s]
createdSeq ])

    -- throw an exception in an STM transaction
    throwStm :: forall b.
                StmStack s b a
             -> Map TVarId (SomeTVar s)
             -> Map TVarId (SomeTVar s)
             -> VarId
             -> SomeException
             -> ST s (SimTrace c)
    throwStm :: forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> Int
-> SomeException
-> ST s (SimTrace c)
throwStm StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written Int
nextVid SomeException
e = do
      -- Revert all the TVar writes
      !_ <- (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 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
          -- Execute the left side in a new frame with an empty written set.
          -- but preserve ones that were set prior to it, as specified in the
          -- [stm](https://hackage.haskell.org/package/stm/docs/Control-Monad-STM.html#v:catchSTM) package.
          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]
-> Int
-> 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]
-> Int
-> 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 [] [] Int
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]
-> Int
-> 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]
-> Int
-> 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 Int
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]
-> Int
-> 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]
-> Int
-> 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 Int
nextVid (SomeException -> StmA s b1
forall s a. SomeException -> StmA s a
ThrowStm SomeException
e)


-- | Special case of 'execAtomically' supporting only var reads and writes
--
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)  -- set of vars written
       -> 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
        x <- TVar s a1 -> ST s a1
forall s a. TVar s a -> ST s a
execReadTVar TVar s a1
v
        go written (k 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
            go written k
        | Bool
otherwise -> do
            !_ <- TVar s a1 -> ST s ()
forall s a. TVar s a -> ST s ()
saveTVar TVar s a1
v
            !_ <- execWriteTVar v x
            let 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
            go written' 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
tvarId !Maybe ThreadLabel
mbLabel a
x = do
    tvarLabel   <- Maybe ThreadLabel -> ST s (STRef s (Maybe ThreadLabel))
forall a s. a -> ST s (STRef s a)
newSTRef Maybe ThreadLabel
mbLabel
    tvarCurrent <- newSTRef x
    tvarUndo    <- newSTRef []
    tvarBlocked <- newSTRef ([], Set.empty)
    tvarVClock  <- newSTRef bottomVClock
    tvarTrace   <- newSTRef Nothing
    return TVar {tvarId, tvarLabel,
                 tvarCurrent, tvarUndo, tvarBlocked, tvarVClock,
                 tvarTrace}

-- 'execReadTVar' is defined in `Control.Monad.IOSim.Type` and shared with /IOSim/

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
    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 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
    -- push the current value onto the undo stack
    v   <- STRef s a -> ST s a
forall s a. STRef s a -> ST s a
readSTRef STRef s a
tvarCurrent
    !vs <- readSTRef tvarUndo
    writeSTRef tvarUndo $! v: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
    -- pop the undo stack, and revert the current value
    !vs <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
    !_  <- writeSTRef tvarCurrent (head vs)
    writeSTRef tvarUndo $! tail 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
    !vs <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
    -- pop the undo stack, leaving the current value unchanged
    writeSTRef tvarUndo $! tail 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

-- | Trace a 'TVar'.  It must be called only on 'TVar's that were new or
-- 'written.
traceTVarST :: TVar s a
            -> Bool -- true if it's a new 'TVar'
            -> ST s TraceValue
traceTVarST :: forall s a. TVar s a -> Bool -> ST s TraceValue
traceTVarST 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, 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
    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 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
        !vs <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
        v   <- readSTRef tvarCurrent
        case (new, 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"



leastUpperBoundTVarVClocks :: [SomeTVar s] -> ST s VectorClock
leastUpperBoundTVarVClocks :: forall s. [SomeTVar s] -> ST s VectorClock
leastUpperBoundTVarVClocks [SomeTVar s]
tvars =
  (VectorClock -> VectorClock -> VectorClock)
-> VectorClock -> [VectorClock] -> VectorClock
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr VectorClock -> VectorClock -> VectorClock
leastUpperBoundVClock VectorClock
bottomVClock ([VectorClock] -> VectorClock)
-> ST s [VectorClock] -> ST s VectorClock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [ST s VectorClock] -> ST s [VectorClock]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [STRef s VectorClock -> ST s VectorClock
forall s a. STRef s a -> ST s a
readSTRef (TVar s a -> STRef s VectorClock
forall s a. TVar s a -> STRef s VectorClock
tvarVClock TVar s a
r) | SomeTVar TVar s a
r <- [SomeTVar s]
tvars]

--
-- Blocking and unblocking on TVars
--

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
    (tids, 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
    when (tid `Set.notMember` tidsSet) $ do
      let !tids'    = IOSimThreadId
tid IOSimThreadId -> [IOSimThreadId] -> [IOSimThreadId]
forall a. a -> [a] -> [a]
: [IOSimThreadId]
tids
          !tidsSet' = IOSimThreadId -> Set IOSimThreadId -> Set IOSimThreadId
forall a. Ord a => a -> Set a -> Set a
Set.insert IOSimThreadId
tid Set IOSimThreadId
tidsSet
      writeSTRef tvarBlocked (tids', tidsSet')

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)

-- | For each TVar written to in a transaction (in order) collect the threads
-- that blocked on each one (in order).
--
-- Also, for logging purposes, return an association between the threads and
-- the var writes that woke them.
--
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
  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 ]
  -- Threads to wake up, in wake up order, annotated with the vars written that
  -- caused the unblocking.
  -- We reverse the individual lists because the tvarBlocked is used as a stack
  -- so it is in order of last written, LIFO, and we want FIFO behaviour.
  let 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 = (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 ]
  return (wakeup, 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

--
-- Steps
--

-- | Check if two steps can be reordered with a possibly different outcome.
--
racingSteps :: Step -- ^ an earlier step
            -> Step -- ^ a later step
            -> Bool
racingSteps :: Step -> Step -> Bool
racingSteps Step
s Step
s' =
     -- is s executed by a racy thread
     IOSimThreadId -> Bool
isRacyThreadId (Step -> IOSimThreadId
stepThreadId Step
s)
     -- steps which belong to the same thread cannot race
  Bool -> Bool -> Bool
&& Step -> IOSimThreadId
stepThreadId Step
s IOSimThreadId -> IOSimThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= Step -> IOSimThreadId
stepThreadId Step
s'
     -- if s wakes up s' then s and s' cannot race
  Bool -> Bool -> Bool
&& Bool -> Bool
not (Step -> IOSimThreadId
stepThreadId Step
s' IOSimThreadId -> Set IOSimThreadId -> Bool
forall a. Eq a => a -> Set a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Effect -> Set IOSimThreadId
effectWakeup (Step -> Effect
stepEffect Step
s))
     -- s effects races with s' effects or either one throws to the other
  Bool -> Bool -> Bool
&& (  Step -> Effect
stepEffect Step
s Effect -> Effect -> Bool
`racingEffects` Step -> Effect
stepEffect Step
s'
     Bool -> Bool -> Bool
|| Step -> Step -> Bool
throwsTo Step
s Step
s'
     Bool -> Bool -> Bool
|| Step -> Step -> Bool
throwsTo Step
s' Step
s
     )
  where throwsTo :: Step -> Step -> Bool
throwsTo Step
s1 Step
s2 =
             Step -> IOSimThreadId
stepThreadId Step
s2 IOSimThreadId -> [IOSimThreadId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Effect -> [IOSimThreadId]
effectThrows (Step -> Effect
stepEffect Step
s1)
          -- `throwTo` races with any other effect
          Bool -> Bool -> Bool
&& Step -> Effect
stepEffect Step
s2 Effect -> Effect -> Bool
forall a. Eq a => a -> a -> Bool
/= Effect
forall a. Monoid a => a
mempty

currentStep :: Thread s a -> Step
currentStep :: forall s a. Thread s a -> Step
currentStep Thread { threadId :: forall s a. Thread s a -> IOSimThreadId
threadId     = IOSimThreadId
stepThreadId,
                     threadStep :: forall s a. Thread s a -> Int
threadStep   = Int
stepStep,
                     threadEffect :: forall s a. Thread s a -> Effect
threadEffect = Effect
stepEffect,
                     threadVClock :: forall s a. Thread s a -> VectorClock
threadVClock = VectorClock
stepVClock
                   } = Step {Int
VectorClock
IOSimThreadId
Effect
stepStep :: Int
stepThreadId :: IOSimThreadId
stepVClock :: VectorClock
stepEffect :: Effect
stepThreadId :: IOSimThreadId
stepStep :: Int
stepEffect :: Effect
stepVClock :: VectorClock
..}

-- | Step a thread and return the previous `StepId` and its `Effect`.
--
stepThread :: Thread s a -> (Thread s a, Effect)
stepThread :: forall s a. Thread s a -> (Thread s a, Effect)
stepThread thread :: Thread s a
thread@Thread { threadId :: forall s a. Thread s a -> IOSimThreadId
threadId     = IOSimThreadId
tid,
                           threadStep :: forall s a. Thread s a -> Int
threadStep   = Int
tstep,
                           threadVClock :: forall s a. Thread s a -> VectorClock
threadVClock = VectorClock
vClock } =
  ( Thread s a
thread { threadStep   = tstep+1,
             threadEffect = mempty,
             threadVClock = insertVClock tid (tstep+1) vClock
           },
    Thread s a -> Effect
forall s a. Thread s a -> Effect
threadEffect Thread s a
thread
  )

-- | 'updateRaces' turns a current 'Step' into 'StepInfo', and updates all
-- 'activeRaces'.
--
-- We take care that steps can only race against threads in their
-- concurrent set. When this becomes empty, a step can be retired into
-- the "complete" category, but only if there are some steps racing
-- with it.
updateRaces :: Thread s a -> SimState s a -> Races
updateRaces :: forall s a. Thread s a -> SimState s a -> Races
updateRaces thread :: Thread s a
thread@Thread { threadId :: forall s a. Thread s a -> IOSimThreadId
threadId = IOSimThreadId
tid }
            SimState{ ScheduleControl
control :: forall s a. SimState s a -> ScheduleControl
control :: ScheduleControl
control, Map IOSimThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map IOSimThreadId (Thread s a)
threads :: Map IOSimThreadId (Thread s a)
threads, races :: forall s a. SimState s a -> Races
races = races :: Races
races@Races { [StepInfo]
activeRaces :: Races -> [StepInfo]
activeRaces :: [StepInfo]
activeRaces } } =
    let
        newStep :: Step
newStep@Step{ stepEffect :: Step -> Effect
stepEffect = Effect
newEffect } = Thread s a -> Step
forall s a. Thread s a -> Step
currentStep Thread s a
thread

        concurrent0 :: Set IOSimThreadId
concurrent0 =
          Map IOSimThreadId (Thread s a) -> Set IOSimThreadId
forall k a. Map k a -> Set k
Map.keysSet ((Thread s a -> Bool)
-> Map IOSimThreadId (Thread s a) -> Map IOSimThreadId (Thread s a)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\Thread s a
t -> Bool -> Bool
not (Thread s a -> Bool
forall s a. Thread s a -> Bool
isThreadDone Thread s a
t)
                                      Bool -> Bool -> Bool
&& Thread s a -> IOSimThreadId
forall s a. Thread s a -> IOSimThreadId
threadId Thread s a
t IOSimThreadId -> Set IOSimThreadId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember`
                                         Effect -> Set IOSimThreadId
effectForks Effect
newEffect
                                  ) Map IOSimThreadId (Thread s a)
threads)

        -- A new step to add to the `activeRaces` list.
        newStepInfo :: Maybe StepInfo
        !newStepInfo :: Maybe StepInfo
newStepInfo | IOSimThreadId -> Bool
isNotRacyThreadId IOSimThreadId
tid = Maybe StepInfo
forall a. Maybe a
Nothing
                       -- non-racy threads do not race

                     | Set IOSimThreadId -> Bool
forall a. Set a -> Bool
Set.null Set IOSimThreadId
concurrent   = Maybe StepInfo
forall a. Maybe a
Nothing
                       -- cannot race with nothing

                     | Bool
isBlocking            = Maybe StepInfo
forall a. Maybe a
Nothing
                     -- no need to defer a blocking transaction

                     | Bool
otherwise =
            StepInfo -> Maybe StepInfo
forall a. a -> Maybe a
Just (StepInfo -> Maybe StepInfo) -> StepInfo -> Maybe StepInfo
forall a b. (a -> b) -> a -> b
$! StepInfo { stepInfoStep :: Step
stepInfoStep       = Step
newStep,
                               stepInfoControl :: ScheduleControl
stepInfoControl    = ScheduleControl
control,
                               stepInfoConcurrent :: Set IOSimThreadId
stepInfoConcurrent = Set IOSimThreadId
concurrent,
                               stepInfoNonDep :: [Step]
stepInfoNonDep     = [],
                               stepInfoRaces :: [Step]
stepInfoRaces      = []
                             }
          where
            concurrent :: Set IOSimThreadId
            concurrent :: Set IOSimThreadId
concurrent = Set IOSimThreadId
concurrent0 Set IOSimThreadId -> Set IOSimThreadId -> Set IOSimThreadId
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Effect -> Set IOSimThreadId
effectWakeup Effect
newEffect

            isBlocking :: Bool
            isBlocking :: Bool
isBlocking = Thread s a -> Bool
forall s a. Thread s a -> Bool
isThreadBlocked Thread s a
thread Bool -> Bool -> Bool
&& Effect -> Bool
onlyReadEffect Effect
newEffect

        -- Used to update each `StepInfo` in `activeRaces`.
        updateStepInfo :: StepInfo -> StepInfo
        updateStepInfo :: StepInfo -> StepInfo
updateStepInfo stepInfo :: StepInfo
stepInfo@StepInfo { stepInfoStep :: StepInfo -> Step
stepInfoStep       = Step
step,
                                           stepInfoConcurrent :: StepInfo -> Set IOSimThreadId
stepInfoConcurrent = Set IOSimThreadId
concurrent,
                                           [Step]
stepInfoNonDep :: StepInfo -> [Step]
stepInfoNonDep :: [Step]
stepInfoNonDep,
                                           [Step]
stepInfoRaces :: StepInfo -> [Step]
stepInfoRaces :: [Step]
stepInfoRaces  } =
          -- if this step depends on the previous step, or is not concurrent,
          -- then any threads that it wakes up become non-concurrent also.
          let !lessConcurrent :: Set IOSimThreadId
lessConcurrent = Set IOSimThreadId
concurrent Set IOSimThreadId -> Set IOSimThreadId -> Set IOSimThreadId
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Effect -> Set IOSimThreadId
effectWakeup Effect
newEffect

              -- `step` happened before `newStep` (`newStep` happened after
              -- `step`)
              happensBefore :: Bool
happensBefore   = Step
step Step -> Step -> Bool
`happensBeforeStep` Step
newStep

              !stepInfoNonDep' :: [Step]
stepInfoNonDep'
                -- `newStep` happened after `step`
                | Bool
happensBefore =           [Step]
stepInfoNonDep
                -- `newStep` did not happen after `step`
                | Bool
otherwise     = Step
newStep Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
: [Step]
stepInfoNonDep in

          if IOSimThreadId
tid IOSimThreadId -> Set IOSimThreadId -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set IOSimThreadId
concurrent
            then let
                  in StepInfo
stepInfo { stepInfoConcurrent = lessConcurrent
                              , stepInfoNonDep     = stepInfoNonDep'
                              }

            -- The core of IOSimPOR.  Detect if `newStep` is racing with any
            -- previous steps and update each `StepInfo`.
            else let theseStepsRace :: Bool
theseStepsRace = Step
step Step -> Step -> Bool
`racingSteps` Step
newStep
                     -- `newStep` happens after any of the racing steps
                     afterRacingStep :: Bool
afterRacingStep = (Step -> Bool) -> [Step] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Step -> Step -> Bool
`happensBeforeStep` Step
newStep) [Step]
stepInfoRaces

                     -- We will only record the first race with each thread.
                     -- Reversing the first race makes the next race detectable.
                     -- Thus we remove a thread from the concurrent set after the
                     -- first race.
                     !concurrent' :: Set IOSimThreadId
concurrent'
                       | Bool
happensBefore   = IOSimThreadId -> Set IOSimThreadId -> Set IOSimThreadId
forall a. Ord a => a -> Set a -> Set a
Set.delete IOSimThreadId
tid Set IOSimThreadId
lessConcurrent
                       | Bool
theseStepsRace  = IOSimThreadId -> Set IOSimThreadId -> Set IOSimThreadId
forall a. Ord a => a -> Set a -> Set a
Set.delete IOSimThreadId
tid Set IOSimThreadId
concurrent
                       | Bool
afterRacingStep = IOSimThreadId -> Set IOSimThreadId -> Set IOSimThreadId
forall a. Ord a => a -> Set a -> Set a
Set.delete IOSimThreadId
tid Set IOSimThreadId
concurrent
                       | Bool
otherwise       = Set IOSimThreadId
concurrent

                     -- Here we record discovered races.  We only record a new
                     -- race if we are following the default schedule, to avoid
                     -- finding the same race in different parts of the search
                     -- space.
                     !stepInfoRaces' :: [Step]
stepInfoRaces'
                       | Bool
theseStepsRace Bool -> Bool -> Bool
&& ScheduleControl -> Bool
isDefaultSchedule ScheduleControl
control
                                   = Step
newStep Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
: [Step]
stepInfoRaces
                       | Bool
otherwise =           [Step]
stepInfoRaces

            in StepInfo
stepInfo { stepInfoConcurrent = effectForks newEffect
                                               `Set.union` concurrent',
                          stepInfoNonDep     = stepInfoNonDep',
                          stepInfoRaces      = stepInfoRaces'
                        }

        activeRaces' :: [StepInfo]
        !activeRaces' :: [StepInfo]
activeRaces' =
          case Maybe StepInfo
newStepInfo of
            Maybe StepInfo
Nothing ->       StepInfo -> StepInfo
updateStepInfo (StepInfo -> StepInfo) -> [StepInfo] -> [StepInfo]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [StepInfo]
activeRaces
            Just StepInfo
si -> StepInfo
si StepInfo -> [StepInfo] -> [StepInfo]
forall a. a -> [a] -> [a]
: (StepInfo -> StepInfo
updateStepInfo (StepInfo -> StepInfo) -> [StepInfo] -> [StepInfo]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [StepInfo]
activeRaces)

    in Races -> Races
normalizeRaces Races
races { activeRaces = activeRaces' }


normalizeRaces :: Races -> Races
normalizeRaces :: Races -> Races
normalizeRaces Races{ [StepInfo]
activeRaces :: Races -> [StepInfo]
activeRaces :: [StepInfo]
activeRaces, [StepInfo]
completeRaces :: [StepInfo]
completeRaces :: Races -> [StepInfo]
completeRaces } =
  let !activeRaces' :: [StepInfo]
activeRaces'   =   (StepInfo -> Bool) -> [StepInfo] -> [StepInfo]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (StepInfo -> Bool) -> StepInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set IOSimThreadId -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Set IOSimThreadId -> Bool)
-> (StepInfo -> Set IOSimThreadId) -> StepInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StepInfo -> Set IOSimThreadId
stepInfoConcurrent) [StepInfo]
activeRaces
      !completeRaces' :: [StepInfo]
completeRaces' = ( (StepInfo -> Bool) -> [StepInfo] -> [StepInfo]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (StepInfo -> Bool) -> StepInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Step] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Step] -> Bool) -> (StepInfo -> [Step]) -> StepInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StepInfo -> [Step]
stepInfoRaces)
                        ([StepInfo] -> [StepInfo])
-> ([StepInfo] -> [StepInfo]) -> [StepInfo] -> [StepInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StepInfo -> Bool) -> [StepInfo] -> [StepInfo]
forall a. (a -> Bool) -> [a] -> [a]
filter (Set IOSimThreadId -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Set IOSimThreadId -> Bool)
-> (StepInfo -> Set IOSimThreadId) -> StepInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StepInfo -> Set IOSimThreadId
stepInfoConcurrent)
                        ([StepInfo] -> [StepInfo]) -> [StepInfo] -> [StepInfo]
forall a b. (a -> b) -> a -> b
$ [StepInfo]
activeRaces
                        )
                     [StepInfo] -> [StepInfo] -> [StepInfo]
forall a. [a] -> [a] -> [a]
++ [StepInfo]
completeRaces
  in Races{ activeRaces :: [StepInfo]
activeRaces   = [StepInfo]
activeRaces',
            completeRaces :: [StepInfo]
completeRaces = [StepInfo]
completeRaces' }


-- When a thread terminates, we remove it from the concurrent thread
-- sets of active races.
threadTerminatesRaces :: IOSimThreadId -> Races -> Races
threadTerminatesRaces :: IOSimThreadId -> Races -> Races
threadTerminatesRaces IOSimThreadId
tid races :: Races
races@Races{ [StepInfo]
activeRaces :: Races -> [StepInfo]
activeRaces :: [StepInfo]
activeRaces } =
  let activeRaces' :: [StepInfo]
activeRaces' = [ StepInfo
s{stepInfoConcurrent = Set.delete tid stepInfoConcurrent}
                     | s :: StepInfo
s@StepInfo{ Set IOSimThreadId
stepInfoConcurrent :: StepInfo -> Set IOSimThreadId
stepInfoConcurrent :: Set IOSimThreadId
stepInfoConcurrent } <- [StepInfo]
activeRaces ]
  in Races -> Races
normalizeRaces (Races -> Races) -> Races -> Races
forall a b. (a -> b) -> a -> b
$ Races
races{ activeRaces = activeRaces' }

-- We assume that steps do not race with later steps after a quiescent
-- period. Quiescent periods end when simulated time advances, thus we
-- are assuming here that all work is completed before a timer
-- triggers.

quiescentRaces :: Races -> Races
quiescentRaces :: Races -> Races
quiescentRaces Races{ [StepInfo]
activeRaces :: Races -> [StepInfo]
activeRaces :: [StepInfo]
activeRaces, [StepInfo]
completeRaces :: Races -> [StepInfo]
completeRaces :: [StepInfo]
completeRaces } =
  Races{ activeRaces :: [StepInfo]
activeRaces = [],
         completeRaces :: [StepInfo]
completeRaces = [ StepInfo
s{stepInfoConcurrent = Set.empty}
                         | StepInfo
s <- [StepInfo]
activeRaces
                         , Bool -> Bool
not ([Step] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (StepInfo -> [Step]
stepInfoRaces StepInfo
s))
                         ] [StepInfo] -> [StepInfo] -> [StepInfo]
forall a. [a] -> [a] -> [a]
++ [StepInfo]
completeRaces }


--
-- Schedule control
--

controlTargets :: StepId -> ScheduleControl -> Bool
controlTargets :: StepId -> ScheduleControl -> Bool
controlTargets StepId
stepId
               (ControlAwait (ScheduleMod{ StepId
scheduleModTarget :: StepId
scheduleModTarget :: ScheduleMod -> StepId
scheduleModTarget }:[ScheduleMod]
_)) =
  StepId
stepId StepId -> StepId -> Bool
forall a. Eq a => a -> a -> Bool
== StepId
scheduleModTarget
controlTargets StepId
_stepId ScheduleControl
_ = Bool
False

followControl :: ScheduleControl -> ScheduleControl
followControl :: ScheduleControl -> ScheduleControl
followControl (ControlAwait (ScheduleMod { [StepId]
scheduleModInsertion :: [StepId]
scheduleModInsertion :: ScheduleMod -> [StepId]
scheduleModInsertion } : [ScheduleMod]
mods)) =
               [StepId] -> [ScheduleMod] -> ScheduleControl
ControlFollow [StepId]
scheduleModInsertion [ScheduleMod]
mods
followControl (ControlAwait []) = ThreadLabel -> ScheduleControl
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"Impossible: followControl (ControlAwait [])"
followControl ControlDefault{}  = ThreadLabel -> ScheduleControl
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"Impossible: followControl ControlDefault{}"
followControl ControlFollow{}   = ThreadLabel -> ScheduleControl
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"Impossible: followControl ControlFollow{}"

controlFollows :: StepId -> ScheduleControl -> Bool
controlFollows :: StepId -> ScheduleControl -> Bool
controlFollows StepId
_stepId  ScheduleControl
ControlDefault               = Bool
True
controlFollows StepId
_stepId (ControlFollow [] [ScheduleMod]
_)          = Bool
True
controlFollows StepId
stepId  (ControlFollow (StepId
stepId':[StepId]
_) [ScheduleMod]
_) = StepId
stepId StepId -> StepId -> Bool
forall a. Eq a => a -> a -> Bool
== StepId
stepId'
controlFollows StepId
stepId  (ControlAwait (ScheduleMod
smod:[ScheduleMod]
_))       = StepId
stepId StepId -> StepId -> Bool
forall a. Eq a => a -> a -> Bool
/= ScheduleMod -> StepId
scheduleModTarget ScheduleMod
smod
controlFollows StepId
_       (ControlAwait [])             = ThreadLabel -> Bool
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"Impossible: controlFollows _ (ControlAwait [])"

advanceControl :: StepId -> ScheduleControl -> ScheduleControl
advanceControl :: StepId -> ScheduleControl -> ScheduleControl
advanceControl (IOSimThreadId
tid,Int
step) control :: ScheduleControl
control@(ControlFollow ((IOSimThreadId
tid',Int
step'):[StepId]
sids') [ScheduleMod]
tgts)
  | IOSimThreadId
tid IOSimThreadId -> IOSimThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= IOSimThreadId
tid' =
      -- we are switching threads to follow the schedule
      --Debug.trace ("Switching threads from "++show (tid,step)++" to "++show (tid',step')++"\n") $
      ScheduleControl
control
  | Int
step Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
step' =
      [StepId] -> [ScheduleMod] -> ScheduleControl
ControlFollow [StepId]
sids' [ScheduleMod]
tgts
  | Bool
otherwise =
      ThreadLabel -> ScheduleControl
forall a. (?callStack::CallStack) => ThreadLabel -> a
error (ThreadLabel -> ScheduleControl) -> ThreadLabel -> ScheduleControl
forall a b. (a -> b) -> a -> b
$ [ThreadLabel] -> ThreadLabel
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ ThreadLabel
"advanceControl ", StepId -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show (IOSimThreadId
tid,Int
step)
            , ThreadLabel
" cannot follow step ", Int -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show Int
step'
            , ThreadLabel
"\n"
            ]
advanceControl StepId
stepId (ControlFollow [] []) =
  ScheduleControl
ControlDefault
advanceControl StepId
stepId (ControlFollow [] [ScheduleMod]
tgts) =
  [ScheduleMod] -> ScheduleControl
ControlAwait [ScheduleMod]
tgts
advanceControl StepId
stepId ScheduleControl
control =
  Bool -> ScheduleControl -> ScheduleControl
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ StepId -> ScheduleControl -> Bool
controlTargets StepId
stepId ScheduleControl
control) (ScheduleControl -> ScheduleControl)
-> ScheduleControl -> ScheduleControl
forall a b. (a -> b) -> a -> b
$
  ScheduleControl
control

--
-- Schedule modifications
--

stepStepId :: Step -> (IOSimThreadId, Int)
stepStepId :: Step -> StepId
stepStepId Step{ stepThreadId :: Step -> IOSimThreadId
stepThreadId = IOSimThreadId
tid, stepStep :: Step -> Int
stepStep = Int
n } = (IOSimThreadId
tid,Int
n)

stepInfoToScheduleMods :: StepInfo -> [ScheduleMod]
stepInfoToScheduleMods :: StepInfo -> [ScheduleMod]
stepInfoToScheduleMods
  StepInfo{ stepInfoStep :: StepInfo -> Step
stepInfoStep    = Step
step,
            stepInfoControl :: StepInfo -> ScheduleControl
stepInfoControl = ScheduleControl
control,
            stepInfoNonDep :: StepInfo -> [Step]
stepInfoNonDep  = [Step]
nondep,
            stepInfoRaces :: StepInfo -> [Step]
stepInfoRaces   = [Step]
races
          } =
  -- It is actually possible for a later step that races with an earlier one
  -- not to *depend* on it in a happens-before sense. But we don't want to try
  -- to follow any steps *after* the later one.
  [ ScheduleMod
      { scheduleModTarget :: StepId
scheduleModTarget    = Step -> StepId
stepStepId Step
step
      , scheduleModControl :: ScheduleControl
scheduleModControl   = ScheduleControl
control
      , scheduleModInsertion :: [StepId]
scheduleModInsertion = (StepId -> Bool) -> [StepId] -> [StepId]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (StepId -> StepId -> Bool
forall a. Eq a => a -> a -> Bool
/=Step -> StepId
stepStepId Step
step')
                                         (Step -> StepId
stepStepId (Step -> StepId) -> [Step] -> [StepId]
forall a b. (a -> b) -> [a] -> [b]
`map` [Step] -> [Step]
forall a. [a] -> [a]
reverse [Step]
nondep)
                            [StepId] -> [StepId] -> [StepId]
forall a. [a] -> [a] -> [a]
++ [Step -> StepId
stepStepId Step
step']
                            -- It should be unnecessary to include the delayed
                            -- step in the insertion, since the default
                            -- scheduling should run it anyway. Removing it may
                            -- help avoid redundant schedules.
                            -- ++ [stepStepId step]
      }
  | Step
step' <- [Step]
races ]

traceFinalRacesFound :: SimState s a -> SimTrace a -> SimTrace a
traceFinalRacesFound :: forall s a. SimState s a -> SimTrace a -> SimTrace a
traceFinalRacesFound SimState{ control0 :: forall s a. SimState s a -> ScheduleControl
control0 = ScheduleControl
control, Races
races :: forall s a. SimState s a -> Races
races :: Races
races } =
    [ScheduleControl] -> SimTrace a -> SimTrace a
forall a. [ScheduleControl] -> SimTrace a -> SimTrace a
TraceRacesFound [ScheduleControl -> ScheduleMod -> ScheduleControl
extendScheduleControl ScheduleControl
control ScheduleMod
m | ScheduleMod
m <- [ScheduleMod]
scheduleMods]
  where
    scheduleMods :: [ScheduleMod]
    scheduleMods :: [ScheduleMod]
scheduleMods =
        (StepInfo -> [ScheduleMod]) -> [StepInfo] -> [ScheduleMod]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap StepInfo -> [ScheduleMod]
stepInfoToScheduleMods
      ([StepInfo] -> [ScheduleMod])
-> (Races -> [StepInfo]) -> Races -> [ScheduleMod]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Races -> [StepInfo]
completeRaces
      (Races -> [StepInfo]) -> (Races -> Races) -> Races -> [StepInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Races -> Races
quiescentRaces
      (Races -> [ScheduleMod]) -> Races -> [ScheduleMod]
forall a b. (a -> b) -> a -> b
$ Races
races

-- Extend an existing schedule control with a newly discovered schedule mod
extendScheduleControl' :: ScheduleControl -> ScheduleMod -> ScheduleControl
extendScheduleControl' :: ScheduleControl -> ScheduleMod -> ScheduleControl
extendScheduleControl' ScheduleControl
ControlDefault ScheduleMod
m = [ScheduleMod] -> ScheduleControl
ControlAwait [ScheduleMod
m]
extendScheduleControl' (ControlAwait [ScheduleMod]
mods) ScheduleMod
m =
  case ScheduleMod -> ScheduleControl
scheduleModControl ScheduleMod
m of
    ScheduleControl
ControlDefault     -> [ScheduleMod] -> ScheduleControl
ControlAwait ([ScheduleMod]
mods[ScheduleMod] -> [ScheduleMod] -> [ScheduleMod]
forall a. [a] -> [a] -> [a]
++[ScheduleMod
m])
    ControlAwait [ScheduleMod]
mods' ->
      let common :: Int
common = [ScheduleMod] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleMod]
mods Int -> Int -> Int
forall a. Num a => a -> a -> a
- [ScheduleMod] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleMod]
mods' in
      Bool -> ScheduleControl -> ScheduleControl
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
common Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int -> [ScheduleMod] -> [ScheduleMod]
forall a. Int -> [a] -> [a]
drop Int
common [ScheduleMod]
mods[ScheduleMod] -> [ScheduleMod] -> Bool
forall a. Eq a => a -> a -> Bool
==[ScheduleMod]
mods') (ScheduleControl -> ScheduleControl)
-> ScheduleControl -> ScheduleControl
forall a b. (a -> b) -> a -> b
$
      [ScheduleMod] -> ScheduleControl
ControlAwait (Int -> [ScheduleMod] -> [ScheduleMod]
forall a. Int -> [a] -> [a]
take Int
common [ScheduleMod]
mods[ScheduleMod] -> [ScheduleMod] -> [ScheduleMod]
forall a. [a] -> [a] -> [a]
++[ScheduleMod
m{ scheduleModControl = ControlDefault }])
    ControlFollow [StepId]
stepIds [ScheduleMod]
mods' ->
      let common :: Int
common = [ScheduleMod] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleMod]
mods Int -> Int -> Int
forall a. Num a => a -> a -> a
- [ScheduleMod] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleMod]
mods' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
          m' :: ScheduleMod
m'     = [ScheduleMod]
mods [ScheduleMod] -> Int -> ScheduleMod
forall a. (?callStack::CallStack) => [a] -> Int -> a
!! Int
common
          isUndo :: Bool
isUndo = ScheduleMod -> StepId
scheduleModTarget ScheduleMod
m' StepId -> [StepId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ScheduleMod -> [StepId]
scheduleModInsertion ScheduleMod
m
          m'' :: ScheduleMod
m''    = ScheduleMod
m'{ scheduleModInsertion =
                         takeWhile (/=scheduleModTarget m)
                                   (scheduleModInsertion m')
                         ++
                         scheduleModInsertion m }
      in
      Bool -> ScheduleControl -> ScheduleControl
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
common Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) (ScheduleControl -> ScheduleControl)
-> ScheduleControl -> ScheduleControl
forall a b. (a -> b) -> a -> b
$
      Bool -> ScheduleControl -> ScheduleControl
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int -> [ScheduleMod] -> [ScheduleMod]
forall a. Int -> [a] -> [a]
drop (Int
commonInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [ScheduleMod]
mods [ScheduleMod] -> [ScheduleMod] -> Bool
forall a. Eq a => a -> a -> Bool
== [ScheduleMod]
mods') (ScheduleControl -> ScheduleControl)
-> ScheduleControl -> ScheduleControl
forall a b. (a -> b) -> a -> b
$
      if Bool
isUndo
        then [ScheduleMod] -> ScheduleControl
ControlAwait [ScheduleMod]
mods          -- reject this mod... it's undoing a previous one
        else [ScheduleMod] -> ScheduleControl
ControlAwait (Int -> [ScheduleMod] -> [ScheduleMod]
forall a. Int -> [a] -> [a]
take Int
common [ScheduleMod]
mods[ScheduleMod] -> [ScheduleMod] -> [ScheduleMod]
forall a. [a] -> [a] -> [a]
++[ScheduleMod
m''])
extendScheduleControl' ControlFollow{} ScheduleMod{} =
  -- note: this case is impossible, since `extendScheduleControl'` first
  -- argument is either the initial `ControlDefault` or a result of calling
  -- `extendScheduleControl'` itself.
  ThreadLabel -> ScheduleControl
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"Impossible: extendScheduleControl' ControlFollow{} ScheduleMod{}"

extendScheduleControl :: ScheduleControl -> ScheduleMod -> ScheduleControl
extendScheduleControl :: ScheduleControl -> ScheduleMod -> ScheduleControl
extendScheduleControl ScheduleControl
control ScheduleMod
m =
  let control' :: ScheduleControl
control' = ScheduleControl -> ScheduleMod -> ScheduleControl
extendScheduleControl' ScheduleControl
control ScheduleMod
m in
  {- Debug.trace (unlines ["",
                        "Extending "++show control,
                        "     with "++show m,
                        "   yields "++show control']) -}
  ScheduleControl
control'