{-# LANGUAGE BangPatterns               #-}
{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE DerivingVia                #-}
{-# LANGUAGE ExistentialQuantification  #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTSyntax                 #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}

{-# OPTIONS_GHC -Wno-orphans            #-}
-- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted')
-- and 'reschedule'.
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns -Wno-unused-matches #-}

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

import           Prelude hiding (read)

import           Data.Dynamic
import           Data.Foldable (traverse_)
import qualified Data.List as List
import qualified Data.List.Trace as Trace
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Maybe (mapMaybe)
import           Data.Ord
import           Data.OrdPSQ (OrdPSQ)
import qualified Data.OrdPSQ as PSQ
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Time (UTCTime (..), fromGregorian)

import           Control.Exception (NonTermination (..), assert, throw)
import           Control.Monad (join)

import           Control.Monad (when)
import           Control.Monad.ST.Lazy
import           Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST)
import           Data.STRef.Lazy

import           Control.Monad.Class.MonadSTM hiding (STM, TVar)
import           Control.Monad.Class.MonadThrow as MonadThrow
import           Control.Monad.Class.MonadTime
import           Control.Monad.Class.MonadTimer

import           Control.Monad.IOSim.InternalTypes
import           Control.Monad.IOSim.Types hiding (SimEvent (SimEvent),
                     Trace (SimTrace))
import           Control.Monad.IOSim.Types (SimEvent)
import           Control.Monad.IOSimPOR.Timeout (unsafeTimeout)
import           Control.Monad.IOSimPOR.Types

--
-- Simulation interpreter
--

data Thread s a = Thread {
    Thread s a -> ThreadId
threadId      :: !ThreadId,
    Thread s a -> ThreadControl s a
threadControl :: !(ThreadControl s a),
    Thread s a -> Bool
threadBlocked :: !Bool,
    Thread s a -> Bool
threadDone    :: !Bool,
    Thread s a -> MaskingState
threadMasking :: !MaskingState,
    -- other threads blocked in a ThrowTo to us because we are or were masked
    Thread s a -> [(SomeException, Labelled ThreadId, VectorClock)]
threadThrowTo :: ![(SomeException, Labelled ThreadId, VectorClock)],
    Thread s a -> ClockId
threadClockId :: !ClockId,
    Thread s a -> Maybe ThreadLabel
threadLabel   :: Maybe ThreadLabel,
    Thread s a -> Int
threadNextTId :: !Int,
    Thread s a -> Int
threadStep    :: !Int,
    Thread s a -> VectorClock
threadVClock  :: VectorClock,
    Thread s a -> Effect
threadEffect  :: Effect,  -- in the current step
    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
showList :: [Thread s a] -> ShowS
$cshowList :: forall s a. [Thread s a] -> ShowS
show :: Thread s a -> ThreadLabel
$cshow :: forall s a. Thread s a -> ThreadLabel
showsPrec :: Int -> Thread s a -> ShowS
$cshowsPrec :: forall s a. Int -> Thread s a -> ShowS
Show

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

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

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


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

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

leastUpperBoundVClock :: VectorClock -> VectorClock -> VectorClock
leastUpperBoundVClock :: VectorClock -> VectorClock -> VectorClock
leastUpperBoundVClock (VectorClock Map ThreadId Int
m) (VectorClock Map ThreadId Int
m') =
    Map ThreadId Int -> VectorClock
VectorClock ((Int -> Int -> Int)
-> Map ThreadId Int -> Map ThreadId Int -> Map ThreadId 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 ThreadId Int
m Map ThreadId 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
<= ThreadId -> Map ThreadId Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Step -> ThreadId
stepThreadId Step
step)
                  (VectorClock -> Map ThreadId Int
getVectorClock (VectorClock -> Map ThreadId Int)
-> VectorClock -> Map ThreadId Int
forall a b. (a -> b) -> a -> b
$ Step -> VectorClock
stepVClock Step
step')

labelledTVarId :: TVar s a -> ST s (Labelled TVarId)
labelledTVarId :: TVar s a -> ST s (Labelled TVarId)
labelledTVarId TVar { TVarId
tvarId :: forall s a. TVar s a -> TVarId
tvarId :: TVarId
tvarId, STRef s (Maybe ThreadLabel)
tvarLabel :: forall s a. TVar s a -> STRef s (Maybe ThreadLabel)
tvarLabel :: 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 ThreadId (Thread s a) -> [Labelled ThreadId]
labelledThreads :: Map ThreadId (Thread s a) -> [Labelled ThreadId]
labelledThreads Map ThreadId (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 ThreadId] -> [Labelled ThreadId])
-> [Labelled ThreadId]
-> Map ThreadId (Thread s a)
-> [Labelled ThreadId]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr'
      (\Thread { ThreadId
threadId :: ThreadId
threadId :: forall s a. Thread s a -> ThreadId
threadId, Maybe ThreadLabel
threadLabel :: Maybe ThreadLabel
threadLabel :: forall s a. Thread s a -> Maybe ThreadLabel
threadLabel } ![Labelled ThreadId]
acc -> ThreadId -> Maybe ThreadLabel -> Labelled ThreadId
forall a. a -> Maybe ThreadLabel -> Labelled a
Labelled ThreadId
threadId Maybe ThreadLabel
threadLabel Labelled ThreadId -> [Labelled ThreadId] -> [Labelled ThreadId]
forall a. a -> [a] -> [a]
: [Labelled ThreadId]
acc)
      [] Map ThreadId (Thread s a)
threadMap


-- | Timers mutable variables.  First one supports 'newTimeout' api, the second
-- one 'registerDelay'.
--
data TimerVars s = TimerVars !(TVar s TimeoutState) !(TVar s Bool)

type RunQueue = OrdPSQ (Down ThreadId) (Down ThreadId) ()

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

     }

initialState :: SimState s a
initialState :: SimState s a
initialState =
    SimState :: forall s a.
RunQueue
-> Map ThreadId (Thread s a)
-> Time
-> OrdPSQ TimeoutId Time (TimerVars s)
-> Map ClockId UTCTime
-> TVarId
-> TimeoutId
-> Races
-> ScheduleControl
-> ScheduleControl
-> Maybe Int
-> SimState s a
SimState {
      runqueue :: RunQueue
runqueue = RunQueue
forall k p v. OrdPSQ k p v
PSQ.empty,
      threads :: Map ThreadId (Thread s a)
threads  = Map ThreadId (Thread s a)
forall k a. Map k a
Map.empty,
      curTime :: Time
curTime  = DiffTime -> Time
Time DiffTime
0,
      timers :: OrdPSQ TimeoutId Time (TimerVars s)
timers   = OrdPSQ TimeoutId Time (TimerVars s)
forall k p v. OrdPSQ k p v
PSQ.empty,
      clocks :: Map ClockId UTCTime
clocks   = ClockId -> UTCTime -> Map ClockId UTCTime
forall k a. k -> a -> Map k a
Map.singleton ([Int] -> ClockId
ClockId []) UTCTime
epoch1970,
      nextVid :: TVarId
nextVid  = Int -> TVarId
TVarId Int
0,
      nextTmid :: TimeoutId
nextTmid = Int -> TimeoutId
TimeoutId Int
0,
      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 :: Maybe (Thread s a) -> SimState s a -> x -> x
invariant (Just Thread s a
running) simstate :: SimState s a
simstate@SimState{RunQueue
runqueue :: RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue,Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads,Map ClockId UTCTime
clocks :: Map ClockId UTCTime
clocks :: forall s a. SimState s a -> 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
threadBlocked 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 -> ThreadId
forall s a. Thread s a -> ThreadId
threadId Thread s a
running ThreadId -> Map ThreadId (Thread s a) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map ThreadId (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 (ThreadId -> Down ThreadId
forall a. a -> Down a
Down (Thread s a -> ThreadId
forall s a. Thread s a -> ThreadId
threadId Thread s a
running) Down ThreadId -> RunQueue -> Bool
forall k p v. Ord k => k -> OrdPSQ 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 :: RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue,Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads,Map ClockId UTCTime
clocks :: Map ClockId UTCTime
clocks :: forall s a. SimState s a -> Map ClockId UTCTime
clocks} =
    Bool -> x -> x
forall a. (?callStack::CallStack) => Bool -> a -> a
assert ((Down ThreadId -> Down ThreadId -> () -> Bool -> Bool)
-> Bool -> RunQueue -> Bool
forall k p v a. (k -> p -> v -> a -> a) -> a -> OrdPSQ k p v -> a
PSQ.fold' (\(Down ThreadId
tid) Down ThreadId
_ ()
_ Bool
a -> ThreadId
tid ThreadId -> Map ThreadId (Thread s a) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map ThreadId (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
threadBlocked Thread s a
t Bool -> Bool -> Bool
|| Thread s a -> Bool
forall s a. Thread s a -> Bool
threadDone Thread s a
t) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Bool
not (ThreadId -> Down ThreadId
forall a. a -> Down a
Down (Thread s a -> ThreadId
forall s a. Thread s a -> ThreadId
threadId Thread s a
t) Down ThreadId -> RunQueue -> Bool
forall k p v. Ord k => k -> OrdPSQ k p v -> Bool
`PSQ.member` RunQueue
runqueue)
                | Thread s a
t <- Map ThreadId (Thread s a) -> [Thread s a]
forall k a. Map k a -> [a]
Map.elems Map ThreadId (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 (((Down ThreadId, Down ThreadId, ())
 -> (Down ThreadId, Down ThreadId, ()) -> Bool)
-> [(Down ThreadId, Down ThreadId, ())]
-> [(Down ThreadId, Down ThreadId, ())]
-> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Down ThreadId
tid, Down ThreadId
_, ()
_) (Down ThreadId
tid', Down ThreadId
_, ()
_) -> ThreadId
tid ThreadId -> ThreadId -> Bool
forall a. Ord a => a -> a -> Bool
> ThreadId
tid')
                         (RunQueue -> [(Down ThreadId, Down ThreadId, ())]
forall k p v. OrdPSQ k p v -> [(k, p, v)]
PSQ.toList RunQueue
runqueue)
                         (Int
-> [(Down ThreadId, Down ThreadId, ())]
-> [(Down ThreadId, Down ThreadId, ())]
forall a. Int -> [a] -> [a]
drop Int
1 (RunQueue -> [(Down ThreadId, Down ThreadId, ())]
forall k p v. OrdPSQ k p v -> [(k, p, v)]
PSQ.toList 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 -> 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 ThreadId (Thread s a) -> [Thread s a]
forall k a. Map k a -> [a]
Map.elems Map ThreadId (Thread s a)
threads ])

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


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


-- | Schedule / run a thread.
--
schedule :: Thread s a -> SimState s a -> ST s (SimTrace a)
schedule :: Thread s a -> SimState s a -> ST s (SimTrace a)
schedule thread :: Thread s a
thread@Thread{
           threadId :: forall s a. Thread s a -> ThreadId
threadId      = ThreadId
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 :: RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue,
           Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads,
           OrdPSQ TimeoutId Time (TimerVars s)
timers :: OrdPSQ TimeoutId Time (TimerVars s)
timers :: forall s a. SimState s a -> OrdPSQ TimeoutId Time (TimerVars s)
timers,
           Map ClockId UTCTime
clocks :: Map ClockId UTCTime
clocks :: forall s a. SimState s a -> Map ClockId UTCTime
clocks,
           TVarId
nextVid :: TVarId
nextVid :: forall s a. SimState s a -> TVarId
nextVid, TimeoutId
nextTmid :: TimeoutId
nextTmid :: forall s a. SimState s a -> TimeoutId
nextTmid,
           curTime :: forall s a. SimState s a -> Time
curTime  = Time
time,
           ScheduleControl
control :: ScheduleControl
control :: forall s a. SimState s a -> ScheduleControl
control,
           Maybe Int
perStepTimeLimit :: Maybe Int
perStepTimeLimit :: forall s a. SimState s a -> Maybe Int
perStepTimeLimit
         }

  | (ThreadId, Int) -> ScheduleControl -> Bool
controlTargets (ThreadId
tid,Int
tstep) ScheduleControl
control =
      -- The next step is to be delayed according to the
      -- specified schedule. Switch to following the schedule.
      Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
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 :: ScheduleControl
control = ScheduleControl -> ScheduleControl
followControl ScheduleControl
control }

  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (ThreadId, Int) -> ScheduleControl -> Bool
controlFollows (ThreadId
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.
      Bool -> ST s (SimTrace a) -> ST s (SimTrace a)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Effect
effect Effect -> Effect -> Bool
forall a. Eq a => a -> a -> Bool
== Effect
forall a. Monoid a => a
mempty) (ST s (SimTrace a) -> ST s (SimTrace a))
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$
      ( Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl ((ThreadId, Int) -> ScheduleControl -> SimEventType
EventAwaitControl (ThreadId
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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
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 ((ThreadId, Int)
s:[(ThreadId, Int)]
_) [ScheduleMod]
_
      -> (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl ((ThreadId, Int) -> SimEventType
EventPerformAction (ThreadId
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 (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 (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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
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 -> b -> [Labelled ThreadId] -> SimTrace b
forall a. Time -> a -> [Labelled ThreadId] -> SimTrace a
TraceMainReturn Time
time b
x ( Map ThreadId (Thread s a) -> [Labelled ThreadId]
forall s a. Map ThreadId (Thread s a) -> [Labelled ThreadId]
labelledThreads
                                        (Map ThreadId (Thread s a) -> [Labelled ThreadId])
-> (Map ThreadId (Thread s a) -> Map ThreadId (Thread s a))
-> Map ThreadId (Thread s a)
-> [Labelled ThreadId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Thread s a -> Bool)
-> Map ThreadId (Thread s a) -> Map ThreadId (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
threadDone)
                                        (Map ThreadId (Thread s a) -> [Labelled ThreadId])
-> Map ThreadId (Thread s a) -> [Labelled ThreadId]
forall a b. (a -> b) -> a -> b
$ Map ThreadId (Thread s a)
threads
                                        )

      ControlStack s b a
ForkFrame -> do
        -- this thread is done
        !SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Terminated Thread s a
thread SimState s a
simstate
        SimTrace a -> ST s (SimTrace a)
forall (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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl SimEventType
EventThreadFinished
               (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Terminated)
               (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace

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

      CatchFrame e -> SimA s b
_handler b -> SimA s c
k ControlStack s c a
ctl' -> do
        -- pop the control stack and continue
        let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s c -> ControlStack s c a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (b -> SimA s c
k b
x) ControlStack s c a
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

    Throw SomeException
e -> case SomeException -> Thread s a -> Either Bool (Thread s a)
forall s a. SomeException -> Thread s a -> Either Bool (Thread s a)
unwindControlStack SomeException
e Thread s a
thread of
      Right thread0 :: Thread s a
thread0@Thread { threadMasking :: forall s a. Thread s a -> MaskingState
threadMasking = MaskingState
maskst' } -> 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' :: Thread s a
thread'  = Thread s a -> Thread s a
forall s a. Thread s a -> Thread s a
stepThread Thread s a
thread0
            control' :: ScheduleControl
control' = (ThreadId, Int) -> ScheduleControl -> ScheduleControl
advanceControl (Thread s a -> (ThreadId, Int)
forall s a. Thread s a -> (ThreadId, Int)
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
updateRacesInSimState Thread s a
thread0 SimState s a
simstate
        SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate{ races :: Races
races = Races
races', control :: ScheduleControl
control = ScheduleControl
control' }
        SimTrace a -> ST s (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (MaskingState -> SimEventType
EventMask MaskingState
maskst') SimTrace a
trace)

      Left Bool
isMain
        -- 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 ->
          -- An unhandled exception in the main thread terminates the program
          SimTrace a -> ST s (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
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 (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
                  Time -> SomeException -> [Labelled ThreadId] -> SimTrace a
forall a.
Time -> SomeException -> [Labelled ThreadId] -> SimTrace a
TraceMainException Time
time SomeException
e (Map ThreadId (Thread s a) -> [Labelled ThreadId]
forall s a. Map ThreadId (Thread s a) -> [Labelled ThreadId]
labelledThreads Map ThreadId (Thread s a)
threads))

        | Bool
otherwise -> do
          -- An unhandled exception in any other thread terminates the thread
          !SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Terminated Thread s a
thread SimState s a
simstate
          SimTrace a -> ST s (SimTrace a)
forall (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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
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
$ Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Terminated)
                 (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace

    Catch SimA s a
action' e -> SimA s a
handler a -> 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 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 SimA s a
action'
                                               ((e -> SimA s a)
-> (a -> SimA s b) -> ControlStack s b a -> ControlStack s a a
forall e s b c a.
Exception e =>
(e -> SimA s b)
-> (b -> SimA s c) -> ControlStack s c a -> ControlStack s b a
CatchFrame e -> SimA s a
handler a -> SimA s b
k ControlStack s b a
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 a
expr a -> SimA s b
k -> do
      Either SomeException a
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
$ IO a -> IO (Either SomeException a)
forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> m (Either e a)
try (IO a -> IO (Either SomeException a))
-> IO a -> IO (Either SomeException a)
forall a b. (a -> b) -> a -> b
$ a -> IO a
forall (m :: * -> *) a. MonadEvaluate m => a -> m a
evaluate a
expr
      case Either SomeException a
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 s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (SomeException -> SimA s b
forall s a. SomeException -> SimA s a
Throw SomeException
e) ControlStack s b a
ctl }
          Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
        Right a
whnf -> do
          -- continue with the resulting WHNF
          let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (a -> SimA s b
k a
whnf) ControlStack s b a
ctl }
          Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate

    Say ThreadLabel
msg SimA s b
k -> do
      let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl }
      SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
      SimTrace a -> ST s (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (ThreadLabel -> SimEventType
EventSay ThreadLabel
msg) SimTrace a
trace)

    Output Dynamic
x SimA s b
k -> do
      let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl }
      SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
      SimTrace a -> ST s (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Dynamic -> SimEventType
EventLog Dynamic
x) SimTrace a
trace)

    LiftST ST s a
st a -> SimA s b
k -> do
      a
x <- ST s a -> ST s a
forall s a. ST s a -> ST s a
strictToLazyST ST s a
st
      let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (a -> SimA s b
k a
x) ControlStack s b a
ctl }
      Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate

    GetMonoTime Time -> SimA s b
k -> do
      let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (Time -> SimA s b
k Time
time) ControlStack s b a
ctl }
      Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate

    GetWallTime UTCTime -> SimA s b
k -> do
      let clockid :: ClockId
clockid  = Thread s a -> ClockId
forall s a. Thread s a -> ClockId
threadClockId Thread s a
thread
          clockoff :: UTCTime
clockoff = Map ClockId UTCTime
clocks Map ClockId UTCTime -> ClockId -> UTCTime
forall k a. Ord k => Map k a -> k -> a
Map.! ClockId
clockid
          walltime :: UTCTime
walltime = Time -> NominalDiffTime
timeSinceEpoch Time
time NominalDiffTime -> UTCTime -> UTCTime
`addUTCTime` UTCTime
clockoff
          thread' :: Thread s a
thread'  = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (UTCTime -> SimA s b
k UTCTime
walltime) ControlStack s b a
ctl }
      Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate

    SetWallTime UTCTime
walltime' SimA s b
k -> do
      let clockid :: ClockId
clockid   = Thread s a -> ClockId
forall s a. Thread s a -> ClockId
threadClockId Thread s a
thread
          clockoff :: UTCTime
clockoff  = Map ClockId UTCTime
clocks Map ClockId UTCTime -> ClockId -> UTCTime
forall k a. Ord k => Map k a -> k -> a
Map.! ClockId
clockid
          walltime :: UTCTime
walltime  = Time -> NominalDiffTime
timeSinceEpoch Time
time NominalDiffTime -> UTCTime -> UTCTime
`addUTCTime` UTCTime
clockoff
          clockoff' :: UTCTime
clockoff' = NominalDiffTime -> UTCTime -> UTCTime
addUTCTime (UTCTime -> UTCTime -> NominalDiffTime
diffUTCTime UTCTime
walltime' UTCTime
walltime) UTCTime
clockoff
          thread' :: Thread s a
thread'   = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl }
          simstate' :: SimState s a
simstate' = SimState s a
simstate { clocks :: Map ClockId UTCTime
clocks = ClockId -> UTCTime -> Map ClockId UTCTime -> Map ClockId UTCTime
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ClockId
clockid UTCTime
clockoff' Map ClockId UTCTime
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 = ThreadId
tid in [Int] -> ClockId
ClockId [Int]
i -- reuse the thread id
          thread' :: Thread s a
thread'   = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl
                             , threadClockId :: ClockId
threadClockId = ClockId
clockid' }
          simstate' :: SimState s a
simstate' = SimState s a
simstate { clocks :: Map ClockId UTCTime
clocks = ClockId -> UTCTime -> Map ClockId UTCTime -> Map ClockId UTCTime
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ClockId
clockid' UTCTime
clockoff Map ClockId UTCTime
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'

    -- 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 (IOSim s) -> SimA s b
k | DiffTime
d DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
< DiffTime
0 -> do
      let t :: Timeout (IOSim s)
t       = TimeoutId -> Timeout (IOSim s)
forall s. TimeoutId -> Timeout (IOSim 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 s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (Timeout (IOSim s) -> SimA s b
k Timeout (IOSim s)
t) ControlStack s b a
ctl }
      SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { nextTmid :: TimeoutId
nextTmid = TimeoutId -> TimeoutId
forall a. Enum a => a -> a
succ TimeoutId
nextTmid }
      SimTrace a -> ST s (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (TimeoutId -> TVarId -> Time -> SimEventType
EventTimerCreated TimeoutId
nextTmid TVarId
nextVid Time
expiry) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
              Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (TimeoutId -> SimEventType
EventTimerCancelled TimeoutId
nextTmid) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
              SimTrace a
trace)

    NewTimeout DiffTime
d Timeout (IOSim s) -> SimA s b
k -> do
      TVar s TimeoutState
tvar  <- TVarId
-> Maybe ThreadLabel -> TimeoutState -> ST s (TVar s TimeoutState)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar TVarId
nextVid
                           (ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just (ThreadLabel -> Maybe ThreadLabel)
-> ThreadLabel -> Maybe ThreadLabel
forall a b. (a -> b) -> a -> b
$ ThreadLabel
"<<timeout-state " ThreadLabel -> 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
      STRef s VectorClock -> (VectorClock -> VectorClock) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef (TVar s TimeoutState -> STRef s VectorClock
forall s a. TVar s a -> STRef s VectorClock
tvarVClock TVar s TimeoutState
tvar) (VectorClock -> VectorClock -> VectorClock
leastUpperBoundVClock VectorClock
vClock)
      TVar s Bool
tvar' <- TVarId -> Maybe ThreadLabel -> Bool -> ST s (TVar s Bool)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar (TVarId -> TVarId
forall a. Enum a => a -> a
succ TVarId
nextVid)
                           (ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just (ThreadLabel -> Maybe ThreadLabel)
-> ThreadLabel -> Maybe ThreadLabel
forall a b. (a -> b) -> a -> b
$ ThreadLabel
"<<timeout " ThreadLabel -> 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
      STRef s VectorClock -> (VectorClock -> VectorClock) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef (TVar s Bool -> STRef s VectorClock
forall s a. TVar s a -> STRef s VectorClock
tvarVClock TVar s Bool
tvar') (VectorClock -> VectorClock -> VectorClock
leastUpperBoundVClock VectorClock
vClock)
      let expiry :: Time
expiry  = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
          t :: Timeout (IOSim s)
t       = TVar s TimeoutState
-> TVar s Bool -> TimeoutId -> Timeout (IOSim s)
forall s.
TVar s TimeoutState
-> TVar s Bool -> TimeoutId -> Timeout (IOSim s)
Timeout TVar s TimeoutState
tvar TVar s Bool
tvar' TimeoutId
nextTmid
          timers' :: OrdPSQ TimeoutId Time (TimerVars s)
timers' = TimeoutId
-> Time
-> TimerVars s
-> OrdPSQ TimeoutId Time (TimerVars s)
-> OrdPSQ TimeoutId Time (TimerVars s)
forall k p v.
(Ord k, Ord p) =>
k -> p -> v -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.insert TimeoutId
nextTmid Time
expiry (TVar s TimeoutState -> TVar s Bool -> TimerVars s
forall s. TVar s TimeoutState -> TVar s Bool -> TimerVars s
TimerVars TVar s TimeoutState
tvar TVar s Bool
tvar') OrdPSQ TimeoutId Time (TimerVars s)
timers
          thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (Timeout (IOSim s) -> SimA s b
k Timeout (IOSim s)
t) ControlStack s b a
ctl }
      !SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { timers :: OrdPSQ TimeoutId Time (TimerVars s)
timers   = OrdPSQ TimeoutId Time (TimerVars s)
timers'
                                          , nextVid :: TVarId
nextVid  = TVarId -> TVarId
forall a. Enum a => a -> a
succ (TVarId -> TVarId
forall a. Enum a => a -> a
succ TVarId
nextVid)
                                          , nextTmid :: TimeoutId
nextTmid = TimeoutId -> TimeoutId
forall a. Enum a => a -> a
succ TimeoutId
nextTmid }
      SimTrace a -> ST s (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (TimeoutId -> TVarId -> Time -> SimEventType
EventTimerCreated TimeoutId
nextTmid TVarId
nextVid Time
expiry) SimTrace a
trace)

    -- we do not follow `GHC.Event` behaviour here; updating a timer to the past
    -- effectively cancels it.
    UpdateTimeout (Timeout _tvar _tvar' tmid) DiffTime
d SimA s b
k | DiffTime
d DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
< DiffTime
0 -> do
      let timers' :: OrdPSQ TimeoutId Time (TimerVars s)
timers' = TimeoutId
-> OrdPSQ TimeoutId Time (TimerVars s)
-> OrdPSQ TimeoutId Time (TimerVars s)
forall k p v. (Ord k, Ord p) => k -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.delete TimeoutId
tmid OrdPSQ TimeoutId Time (TimerVars s)
timers
          thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl }
      SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { timers :: OrdPSQ TimeoutId Time (TimerVars s)
timers = OrdPSQ TimeoutId Time (TimerVars s)
timers' }
      SimTrace a -> ST s (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (TimeoutId -> SimEventType
EventTimerCancelled TimeoutId
tmid) SimTrace a
trace)

    UpdateTimeout (Timeout _tvar _tvar' tmid) DiffTime
d SimA s b
k -> do
          -- updating an expired timeout is a noop, so it is safe
          -- to race using a timeout with updating or cancelling it
      let updateTimeout_ :: Maybe (Time, TimerVars s) -> ((), Maybe (Time, TimerVars s))
updateTimeout_  Maybe (Time, TimerVars s)
Nothing       = ((), Maybe (Time, TimerVars s)
forall a. Maybe a
Nothing)
          updateTimeout_ (Just (Time
_p, TimerVars s
v)) = ((), (Time, TimerVars s) -> Maybe (Time, TimerVars s)
forall a. a -> Maybe a
Just (Time
expiry, TimerVars s
v))
          expiry :: Time
expiry  = DiffTime
d DiffTime -> Time -> Time
`addTime` Time
time
          timers' :: OrdPSQ TimeoutId Time (TimerVars s)
timers' = ((), OrdPSQ TimeoutId Time (TimerVars s))
-> OrdPSQ TimeoutId Time (TimerVars s)
forall a b. (a, b) -> b
snd ((Maybe (Time, TimerVars s) -> ((), Maybe (Time, TimerVars s)))
-> TimeoutId
-> OrdPSQ TimeoutId Time (TimerVars s)
-> ((), OrdPSQ TimeoutId Time (TimerVars s))
forall k p v b.
(Ord k, Ord p) =>
(Maybe (p, v) -> (b, Maybe (p, v)))
-> k -> OrdPSQ k p v -> (b, OrdPSQ k p v)
PSQ.alter Maybe (Time, TimerVars s) -> ((), Maybe (Time, TimerVars s))
updateTimeout_ TimeoutId
tmid OrdPSQ TimeoutId Time (TimerVars s)
timers)
          thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl }
      SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate { timers :: OrdPSQ TimeoutId Time (TimerVars s)
timers = OrdPSQ TimeoutId Time (TimerVars s)
timers' }
      SimTrace a -> ST s (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (TimeoutId -> Time -> SimEventType
EventTimerUpdated TimeoutId
tmid Time
expiry) SimTrace a
trace)

    -- updating a negative timer is a no-op, unlike in `GHC.Event`.
    UpdateTimeout (NegativeTimeout _tmid) DiffTime
_d SimA s b
k -> do
      let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
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

    CancelTimeout (Timeout tvar tvar' tmid) SimA s b
k -> do
      let timers' :: OrdPSQ TimeoutId Time (TimerVars s)
timers' = TimeoutId
-> OrdPSQ TimeoutId Time (TimerVars s)
-> OrdPSQ TimeoutId Time (TimerVars s)
forall k p v. (Ord k, Ord p) => k -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.delete TimeoutId
tmid OrdPSQ TimeoutId Time (TimerVars s)
timers
      [SomeTVar s]
written <- StmA s () -> ST s [SomeTVar s]
forall s. StmA s () -> ST s [SomeTVar s]
execAtomically' (STM s () -> StmA s ()
forall s a. STM s a -> StmA s a
runSTM (STM s () -> StmA s ()) -> STM s () -> StmA s ()
forall a b. (a -> b) -> a -> b
$ TVar (IOSim s) TimeoutState -> TimeoutState -> STM (IOSim s) ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar TVar (IOSim s) TimeoutState
TVar s TimeoutState
tvar TimeoutState
TimeoutCancelled)
      ([ThreadId]
wakeup, Map ThreadId (Set (Labelled TVarId))
wokeby) <- [SomeTVar s]
-> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId)))
forall s.
[SomeTVar s]
-> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId)))
threadsUnblockedByWrites [SomeTVar s]
written
      (SomeTVar s -> ST s ()) -> [SomeTVar s] -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(SomeTVar TVar s a
var) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar s a
var) [SomeTVar s]
written
      let effect' :: Effect
effect' = Effect
effect
                 Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [SomeTVar s] -> Effect
forall s. [SomeTVar s] -> Effect
writeEffects [SomeTVar s]
written
                 Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [ThreadId] -> Effect
wakeupEffects [ThreadId]
wakeup
          thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl
                           , threadEffect :: Effect
threadEffect  = Effect
effect'
                           }
          ([ThreadId]
unblocked,
           SimState s a
simstate') = VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
forall s a.
VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
unblockThreads VectorClock
vClock [ThreadId]
wakeup SimState s a
simstate
      STRef s VectorClock -> (VectorClock -> VectorClock) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef (TVar s TimeoutState -> STRef s VectorClock
forall s a. TVar s a -> STRef s VectorClock
tvarVClock TVar s TimeoutState
tvar)  (VectorClock -> VectorClock -> VectorClock
leastUpperBoundVClock VectorClock
vClock)
      STRef s VectorClock -> (VectorClock -> VectorClock) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef (TVar s Bool -> STRef s VectorClock
forall s a. TVar s a -> STRef s VectorClock
tvarVClock TVar s Bool
tvar') (VectorClock -> VectorClock -> VectorClock
leastUpperBoundVClock VectorClock
vClock)
      !SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Yield Thread s a
thread' SimState s a
simstate' { timers :: OrdPSQ TimeoutId Time (TimerVars s)
timers = OrdPSQ TimeoutId Time (TimerVars s)
timers' }
      SimTrace a -> ST s (SimTrace 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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (TimeoutId -> SimEventType
EventTimerCancelled TimeoutId
tmid)
             (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany
                 -- TODO: step
                 [ (Time
time, ThreadId
tid', (-Int
1), Maybe ThreadLabel
tlbl', [Labelled TVarId] -> SimEventType
EventTxWakeup [Labelled TVarId]
vids)
                 | ThreadId
tid' <- [ThreadId]
unblocked
                 , let tlbl' :: Maybe ThreadLabel
tlbl' = ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
forall s a.
ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel ThreadId
tid' Map ThreadId (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
<$> ThreadId
-> Map ThreadId (Set (Labelled TVarId))
-> Maybe (Set (Labelled TVarId))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ThreadId
tid' Map ThreadId (Set (Labelled TVarId))
wokeby ]
             (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Yield)
             (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace

    -- cancelling a negative timer is a no-op
    CancelTimeout (NegativeTimeout _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 s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
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 ThreadId -> 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' :: ThreadId
tid' | Thread s a -> Bool
forall s a. Thread s a -> Bool
threadRacy Thread s a
thread = ThreadId -> ThreadId
setRacyThread (ThreadId -> ThreadId) -> ThreadId -> ThreadId
forall a b. (a -> b) -> a -> b
$ ThreadId -> Int -> ThreadId
childThreadId ThreadId
tid Int
nextTId
               | Bool
otherwise         = ThreadId -> Int -> ThreadId
childThreadId ThreadId
tid Int
nextTId
          thread' :: Thread s a
thread'  = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (ThreadId -> SimA s b
k ThreadId
tid') ControlStack s b a
ctl,
                              threadNextTId :: Int
threadNextTId = Int
nextTId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1,
                              threadEffect :: Effect
threadEffect  = Effect
effect Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> ThreadId -> Effect
forkEffect ThreadId
tid' }
          thread'' :: Thread s a
thread'' = Thread :: forall s a.
ThreadId
-> ThreadControl s a
-> Bool
-> Bool
-> MaskingState
-> [(SomeException, Labelled ThreadId, VectorClock)]
-> ClockId
-> Maybe ThreadLabel
-> Int
-> Int
-> VectorClock
-> Effect
-> Bool
-> Thread s a
Thread { threadId :: ThreadId
threadId      = ThreadId
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
                            , threadBlocked :: Bool
threadBlocked = Bool
False
                            , threadDone :: Bool
threadDone    = Bool
False
                            , threadMasking :: MaskingState
threadMasking = Thread s a -> MaskingState
forall s a. Thread s a -> MaskingState
threadMasking Thread s a
thread
                            , threadThrowTo :: [(SomeException, Labelled ThreadId, 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  = ThreadId -> Int -> VectorClock -> VectorClock
insertVClock ThreadId
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 ThreadId (Thread s a)
threads' = ThreadId
-> Thread s a
-> Map ThreadId (Thread s a)
-> Map ThreadId (Thread s a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ThreadId
tid' Thread s a
thread'' Map ThreadId (Thread s a)
threads
      -- A newly forked thread may have a higher priority, so we deschedule this one.
      !SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Yield Thread s a
thread'
                  SimState s a
simstate { 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 ThreadId (Thread s a)
threads  = Map ThreadId (Thread s a)
threads' }
      SimTrace a -> ST s (SimTrace 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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (ThreadId -> SimEventType
EventThreadForked ThreadId
tid')
             (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Yield)
             (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace

    Atomically STM s a
a a -> SimA s b
k -> Time
-> ThreadId
-> Maybe ThreadLabel
-> TVarId
-> StmA s a
-> (StmTxResult s a -> ST s (SimTrace a))
-> ST s (SimTrace a)
forall s a c.
Time
-> ThreadId
-> Maybe ThreadLabel
-> TVarId
-> StmA s a
-> (StmTxResult s a -> ST s (SimTrace c))
-> ST s (SimTrace c)
execAtomically Time
time ThreadId
tid Maybe ThreadLabel
tlbl TVarId
nextVid (STM s a -> StmA s a
forall s a. STM s a -> StmA s a
runSTM STM s a
a) ((StmTxResult s a -> ST s (SimTrace a)) -> ST s (SimTrace a))
-> (StmTxResult s a -> ST s (SimTrace a)) -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$ \StmTxResult s a
res ->
      case StmTxResult s a
res of
        StmTxCommitted a
x [SomeTVar s]
written [SomeTVar s]
read [SomeTVar s]
created
                         [Dynamic]
tvarDynamicTraces [ThreadLabel]
tvarStringTraces TVarId
nextVid' -> do
          ([ThreadId]
wakeup, Map ThreadId (Set (Labelled TVarId))
wokeby) <- [SomeTVar s]
-> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId)))
forall s.
[SomeTVar s]
-> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId)))
threadsUnblockedByWrites [SomeTVar s]
written
          (SomeTVar s -> ST s ()) -> [SomeTVar s] -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar s a
tvar) [SomeTVar s]
written
          VectorClock
vClockRead <- [SomeTVar s] -> ST s VectorClock
forall s. [SomeTVar s] -> ST s VectorClock
leastUpperBoundTVarVClocks [SomeTVar s]
read
          let vClock' :: VectorClock
vClock'     = VectorClock
vClock VectorClock -> VectorClock -> VectorClock
`leastUpperBoundVClock` VectorClock
vClockRead
              effect' :: Effect
effect'     = Effect
effect
                         Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [SomeTVar s] -> Effect
forall s. [SomeTVar s] -> Effect
readEffects [SomeTVar s]
read
                         Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [SomeTVar s] -> Effect
forall s. [SomeTVar s] -> Effect
writeEffects [SomeTVar s]
written
                         Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [ThreadId] -> Effect
wakeupEffects [ThreadId]
unblocked
              thread' :: Thread s a
thread'     = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (a -> SimA s b
k a
x) ControlStack s b a
ctl,
                                     threadVClock :: VectorClock
threadVClock  = VectorClock
vClock',
                                     threadEffect :: Effect
threadEffect  = Effect
effect' }
              ([ThreadId]
unblocked,
               SimState s a
simstate') = VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
forall s a.
VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
unblockThreads VectorClock
vClock' [ThreadId]
wakeup SimState s a
simstate
          [ST s ()] -> ST s ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ STRef s VectorClock -> (VectorClock -> VectorClock) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef (TVar s a -> STRef s VectorClock
forall s a. TVar s a -> STRef s VectorClock
tvarVClock TVar s a
r) (VectorClock -> VectorClock -> VectorClock
leastUpperBoundVClock VectorClock
vClock')
                    | SomeTVar TVar s a
r <- [SomeTVar s]
created [SomeTVar s] -> [SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a] -> [a]
++ [SomeTVar s]
written ]
          [Labelled TVarId]
written' <- (SomeTVar s -> ST s (Labelled TVarId))
-> [SomeTVar s] -> ST s [Labelled TVarId]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s (Labelled TVarId)
forall s a. TVar s a -> ST s (Labelled TVarId)
labelledTVarId TVar s a
tvar) [SomeTVar s]
written
          [Labelled TVarId]
created' <- (SomeTVar s -> ST s (Labelled TVarId))
-> [SomeTVar s] -> ST s [Labelled TVarId]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s (Labelled TVarId)
forall s a. TVar s a -> ST s (Labelled TVarId)
labelledTVarId TVar s a
tvar) [SomeTVar s]
created
          -- We deschedule a thread after a transaction... another may have woken up.
          !SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Yield Thread s a
thread' SimState s a
simstate' { nextVid :: TVarId
nextVid  = TVarId
nextVid' }
          SimTrace a -> ST s (SimTrace 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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl ([Labelled TVarId]
-> [Labelled TVarId] -> Maybe Effect -> SimEventType
EventTxCommitted [Labelled TVarId]
written' [Labelled TVarId]
created' (Effect -> Maybe Effect
forall a. a -> Maybe a
Just Effect
effect')) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
            [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany
              [ (Time
time, ThreadId
tid', Int
tstep, Maybe ThreadLabel
tlbl', [Labelled TVarId] -> SimEventType
EventTxWakeup [Labelled TVarId]
vids')
              | ThreadId
tid' <- [ThreadId]
unblocked
              , let tlbl' :: Maybe ThreadLabel
tlbl' = ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
forall s a.
ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel ThreadId
tid' Map ThreadId (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
<$> ThreadId
-> Map ThreadId (Set (Labelled TVarId))
-> Maybe (Set (Labelled TVarId))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ThreadId
tid' Map ThreadId (Set (Labelled TVarId))
wokeby ] (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
            [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany
              [ (Time
time, ThreadId
tid, Int
tstep, Maybe ThreadLabel
tlbl, Dynamic -> SimEventType
EventLog Dynamic
tr)
              | Dynamic
tr <- [Dynamic]
tvarDynamicTraces
              ] (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
            [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany
              [ (Time
time, ThreadId
tid, Int
tstep, Maybe ThreadLabel
tlbl, ThreadLabel -> SimEventType
EventSay ThreadLabel
str)
              | ThreadLabel
str <- [ThreadLabel]
tvarStringTraces
              ] (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
            Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl ([ThreadId] -> SimEventType
EventUnblocked [ThreadId]
unblocked) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
            Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Yield) (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$
              SimTrace a
trace

        StmTxAborted [SomeTVar s]
read SomeException
e -> do
          -- schedule this thread to immediately raise the exception
          VectorClock
vClockRead <- [SomeTVar s] -> ST s VectorClock
forall s. [SomeTVar s] -> ST s VectorClock
leastUpperBoundTVarVClocks [SomeTVar s]
read
          let effect' :: Effect
effect' = Effect
effect Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [SomeTVar s] -> Effect
forall s. [SomeTVar s] -> Effect
readEffects [SomeTVar s]
read
              thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (SomeException -> SimA s b
forall s a. SomeException -> SimA s a
Throw SomeException
e) ControlStack s b a
ctl,
                                 threadVClock :: VectorClock
threadVClock  = VectorClock
vClock VectorClock -> VectorClock -> VectorClock
`leastUpperBoundVClock` VectorClock
vClockRead,
                                 threadEffect :: Effect
threadEffect  = Effect
effect' }
          SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
          SimTrace a -> ST s (SimTrace a)
forall (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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Maybe Effect -> SimEventType
EventTxAborted (Effect -> Maybe Effect
forall a. a -> Maybe a
Just Effect
effect'))
                 (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace

        StmTxBlocked [SomeTVar s]
read -> do
          (SomeTVar s -> ST s ()) -> [SomeTVar s] -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(SomeTVar TVar s a
tvar) -> ThreadId -> TVar s a -> ST s ()
forall s a. ThreadId -> TVar s a -> ST s ()
blockThreadOnTVar ThreadId
tid TVar s a
tvar) [SomeTVar s]
read
          [Labelled TVarId]
vids <- (SomeTVar s -> ST s (Labelled TVarId))
-> [SomeTVar s] -> ST s [Labelled TVarId]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
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
          VectorClock
vClockRead <- [SomeTVar s] -> ST s VectorClock
forall s. [SomeTVar s] -> ST s VectorClock
leastUpperBoundTVarVClocks [SomeTVar s]
read
          let effect' :: Effect
effect' = Effect
effect Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> [SomeTVar s] -> Effect
forall s. [SomeTVar s] -> Effect
readEffects [SomeTVar s]
read
              thread' :: Thread s a
thread' = Thread s a
thread { threadVClock :: VectorClock
threadVClock  = VectorClock
vClock VectorClock -> VectorClock -> VectorClock
`leastUpperBoundVClock` VectorClock
vClockRead,
                                 threadEffect :: Effect
threadEffect  = Effect
effect' }
          !SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Blocked Thread s a
thread' SimState s a
simstate
          SimTrace a -> ST s (SimTrace 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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl ([Labelled TVarId] -> Maybe Effect -> SimEventType
EventTxBlocked [Labelled TVarId]
vids (Effect -> Maybe Effect
forall a. a -> Maybe a
Just Effect
effect'))
                 (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Blocked)
                 (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace

    GetThreadId ThreadId -> SimA s b
k -> do
      let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (ThreadId -> SimA s b
k ThreadId
tid) ControlStack s b a
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 ThreadId
tid' ThreadLabel
l SimA s b
k | ThreadId
tid' ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid -> do
      let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl
                           , threadLabel :: Maybe ThreadLabel
threadLabel   = ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
l }
      Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate

    LabelThread ThreadId
tid' ThreadLabel
l SimA s b
k -> do
      let thread' :: Thread s a
thread'  = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl }
          threads' :: Map ThreadId (Thread s a)
threads' = (Thread s a -> Thread s a)
-> ThreadId
-> Map ThreadId (Thread s a)
-> Map ThreadId (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 :: Maybe ThreadLabel
threadLabel = ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
l }) ThreadId
tid' Map ThreadId (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 :: Map ThreadId (Thread s a)
threads = Map ThreadId (Thread s a)
threads' }

    ExploreRaces SimA s b
k -> do
      let thread' :: Thread s a
thread'  = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl
                            , threadRacy :: Bool
threadRacy    = Bool
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
      STRef s x
r <- x -> ST s (STRef s x)
forall a s. a -> ST s (STRef s a)
newSTRef (NonTermination -> x
forall a e. Exception e => e -> a
throw NonTermination
NonTermination)
      x
x <- ST s x -> ST s x
forall s a. ST s a -> ST s a
unsafeInterleaveST (ST s x -> ST s x) -> ST s x -> ST s x
forall a b. (a -> b) -> a -> b
$ STRef s x -> ST s x
forall s a. STRef s a -> ST s a
readSTRef STRef s x
r
      let k' :: SimA s b
k' = IOSim s x -> forall r. (x -> SimA s r) -> SimA s r
forall s a. IOSim s a -> forall r. (a -> SimA s r) -> SimA s r
unIOSim (x -> IOSim s x
f x
x) ((x -> SimA s b) -> SimA s b) -> (x -> SimA s b) -> SimA s b
forall a b. (a -> b) -> a -> b
$ \x
x' ->
                  ST s () -> (() -> SimA s b) -> SimA s b
forall s a b. ST s a -> (a -> SimA s b) -> SimA s b
LiftST (ST s () -> ST s ()
forall s a. ST s a -> ST s a
lazyToStrictST (STRef s x -> x -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s x
r x
x')) (\() -> x -> SimA s b
k x
x')
          thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k' ControlStack s b a
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

    GetMaskState MaskingState -> SimA s b
k -> do
      let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (MaskingState -> SimA s b
k MaskingState
maskst) ControlStack s b a
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 a
action' a -> SimA s b
k -> do
      let thread' :: Thread s a
thread' = Thread s a
thread { 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
action')
                                               ((a -> SimA s b)
-> MaskingState -> ControlStack s b a -> ControlStack s a a
forall b s c a.
(b -> SimA s c)
-> MaskingState -> ControlStack s c a -> ControlStack s b a
MaskFrame a -> SimA s b
k MaskingState
maskst ControlStack s b a
ctl)
                           , threadMasking :: MaskingState
threadMasking = MaskingState
maskst' }
      SimTrace a
trace <-
        case MaskingState
maskst' of
          -- If we're now unmasked then check for any pending async exceptions
          MaskingState
Unmasked -> Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
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
      SimTrace a -> ST s (SimTrace 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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (MaskingState -> SimEventType
EventMask MaskingState
maskst')
             (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
trace

    ThrowTo SomeException
e ThreadId
tid' SimA s b
_ | ThreadId
tid' ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
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 s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (SomeException -> SimA s b
forall s a. SomeException -> SimA s a
Throw SomeException
e) ControlStack s b a
ctl }
      SimTrace a
trace <- Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate
      SimTrace a -> ST s (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (SomeException -> ThreadId -> SimEventType
EventThrowTo SomeException
e ThreadId
tid) SimTrace a
trace)

    ThrowTo SomeException
e ThreadId
tid' SimA s b
k -> do
      let thread' :: Thread s a
thread'    = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl,
                                threadEffect :: Effect
threadEffect  = Effect
effect Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> ThreadId -> Effect
throwToEffect ThreadId
tid' Effect -> Effect -> Effect
forall a. Semigroup a => a -> a -> a
<> Effect
wakeUpEffect,
                                threadVClock :: VectorClock
threadVClock  = VectorClock
vClock VectorClock -> VectorClock -> VectorClock
`leastUpperBoundVClock` VectorClock
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
threadBlocked Thread s a
t then [ThreadId] -> Effect
wakeupEffects [ThreadId
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
threadDone Thread s a
t))
            where Just Thread s a
t = ThreadId -> Map ThreadId (Thread s a) -> Maybe (Thread s a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ThreadId
tid' Map ThreadId (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 :: [(SomeException, Labelled ThreadId, VectorClock)]
threadThrowTo = (SomeException
e, ThreadId -> Maybe ThreadLabel -> Labelled ThreadId
forall a. a -> Maybe ThreadLabel -> Labelled a
Labelled ThreadId
tid Maybe ThreadLabel
tlbl, VectorClock
vClock) (SomeException, Labelled ThreadId, VectorClock)
-> [(SomeException, Labelled ThreadId, VectorClock)]
-> [(SomeException, Labelled ThreadId, VectorClock)]
forall a. a -> [a] -> [a]
: Thread s a -> [(SomeException, Labelled ThreadId, VectorClock)]
forall s a.
Thread s a -> [(SomeException, Labelled ThreadId, VectorClock)]
threadThrowTo Thread s a
t }
              threads' :: Map ThreadId (Thread s a)
threads'       = (Thread s a -> Thread s a)
-> ThreadId
-> Map ThreadId (Thread s a)
-> Map ThreadId (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 ThreadId
tid' Map ThreadId (Thread s a)
threads
          SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Blocked Thread s a
thread' SimState s a
simstate { threads :: Map ThreadId (Thread s a)
threads = Map ThreadId (Thread s a)
threads' }
          SimTrace a -> ST s (SimTrace 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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (SomeException -> ThreadId -> SimEventType
EventThrowTo SomeException
e ThreadId
tid')
                 (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl SimEventType
EventThrowToBlocked
                 (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Blocked)
                 (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
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 s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (SomeException -> SimA s b
forall s a. SomeException -> SimA s a
Throw SomeException
e) ControlStack s b a
ctl'
                  , threadBlocked :: Bool
threadBlocked = Bool
False
                  , threadVClock :: VectorClock
threadVClock  = VectorClock
vClock' VectorClock -> VectorClock -> VectorClock
`leastUpperBoundVClock` VectorClock
vClock }
              simstate' :: SimState s a
simstate'@SimState { threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads = Map ThreadId (Thread s a)
threads' }
                         = ([ThreadId], SimState s a) -> SimState s a
forall a b. (a, b) -> b
snd (VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
forall s a.
VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
unblockThreads VectorClock
vClock [ThreadId
tid'] SimState s a
simstate)
              threads'' :: Map ThreadId (Thread s a)
threads''  = (Thread s a -> Thread s a)
-> ThreadId
-> Map ThreadId (Thread s a)
-> Map ThreadId (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 ThreadId
tid' Map ThreadId (Thread s a)
threads'
              simstate'' :: SimState s a
simstate'' = SimState s a
simstate' { threads :: Map ThreadId (Thread s a)
threads = Map ThreadId (Thread s a)
threads'' }

          -- We yield at this point because the target thread may be higher
          -- priority, so this should be a step for race detection.
          SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Yield Thread s a
thread' SimState s a
simstate''
          SimTrace a -> ST s (SimTrace 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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (SomeException -> ThreadId -> SimEventType
EventThrowTo SomeException
e ThreadId
tid')
                 (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a
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 s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl SimA s b
k ControlStack s b a
ctl }
      Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a. Thread s a -> SimState s a -> ST s (SimTrace a)
schedule Thread s a
thread' SimState s a
simstate


threadInterruptible :: Thread s a -> Bool
threadInterruptible :: 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
threadBlocked Thread s a
thread -> Bool
True  -- blocking operations are interruptible
        | Bool
otherwise            -> Bool
False
      MaskingState
MaskedUninterruptible    -> Bool
False

deschedule :: Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)

deschedule :: 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 -> ThreadId
threadId     = ThreadId
tid }
                 simstate :: SimState s a
simstate@SimState{RunQueue
runqueue :: RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue, Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads, ScheduleControl
control :: ScheduleControl
control :: forall s a. SimState s a -> 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' :: Thread s a
thread'   = Thread s a -> Thread s a
forall s a. Thread s a -> Thread s a
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 ThreadId (Thread s a)
threads'  = ThreadId
-> Thread s a
-> Map ThreadId (Thread s a)
-> Map ThreadId (Thread s a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ThreadId
tid Thread s a
thread' Map ThreadId (Thread s a)
threads
        control' :: ScheduleControl
control'  = (ThreadId, Int) -> ScheduleControl -> ScheduleControl
advanceControl (Thread s a -> (ThreadId, Int)
forall s a. Thread s a -> (ThreadId, Int)
threadStepId Thread s a
thread) ScheduleControl
control 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
runqueue = RunQueue
runqueue', threads :: Map ThreadId (Thread s a)
threads  = Map ThreadId (Thread s a)
threads',
                          races :: Races
races    = Thread s a -> SimState s a -> Races
forall s a. Thread s a -> SimState s a -> Races
updateRacesInSimState Thread s a
thread SimState s a
simstate,
                          control :: ScheduleControl
control  = ScheduleControl
control' }

deschedule Deschedule
Interruptable thread :: Thread s a
thread@Thread {
                           threadId :: forall s a. Thread s a -> ThreadId
threadId      = ThreadId
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 ThreadId, VectorClock)]
threadThrowTo = (SomeException
e, Labelled ThreadId
tid', VectorClock
vClock') : [(SomeException, Labelled ThreadId, 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
                         }
                        simstate :: SimState s a
simstate@SimState{ curTime :: forall s a. SimState s a -> Time
curTime = Time
time, Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads } = do

    -- We're unmasking, but there are pending blocked async exceptions.
    -- So immediately raise the exception and unblock the blocked thread
    -- if possible.
    let thread' :: Thread s a
thread' = Thread s a
thread { threadControl :: ThreadControl s a
threadControl = SimA s b -> ControlStack s b a -> ThreadControl s a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (SomeException -> SimA s b
forall s a. SomeException -> SimA s a
Throw SomeException
e) ControlStack s b a
ctl
                         , threadMasking :: MaskingState
threadMasking = MaskingState
MaskedInterruptible
                         , threadThrowTo :: [(SomeException, Labelled ThreadId, VectorClock)]
threadThrowTo = [(SomeException, Labelled ThreadId, VectorClock)]
etids
                         , threadVClock :: VectorClock
threadVClock  = VectorClock
vClock VectorClock -> VectorClock -> VectorClock
`leastUpperBoundVClock` VectorClock
vClock' }
        ([ThreadId]
unblocked,
         SimState s a
simstate') = VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
forall s a.
VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
unblockThreads VectorClock
vClock [Labelled ThreadId -> ThreadId
forall a. Labelled a -> a
l_labelled Labelled ThreadId
tid'] SimState s a
simstate
    -- the thread is stepped when we Yield
    !SimTrace a
trace <- Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
forall s a.
Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a)
deschedule Deschedule
Yield Thread s a
thread' SimState s a
simstate'
    SimTrace a -> ST s (SimTrace 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
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Deschedule -> SimEventType
EventDeschedule Deschedule
Yield)
           (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl (Labelled ThreadId -> SimEventType
EventThrowToUnmasked Labelled ThreadId
tid')
           -- TODO: step
           (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany [ (Time
time, ThreadId
tid'', (-Int
1), Maybe ThreadLabel
tlbl'', SimEventType
EventThrowToWakeup)
                       | ThreadId
tid'' <- [ThreadId]
unblocked
                       , let tlbl'' :: Maybe ThreadLabel
tlbl'' = ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
forall s a.
ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel ThreadId
tid'' Map ThreadId (Thread s a)
threads ]
             SimTrace a
trace

deschedule Deschedule
Interruptable Thread s a
thread simstate :: SimState s a
simstate@SimState{ ScheduleControl
control :: ScheduleControl
control :: forall s a. SimState s a -> ScheduleControl
control } =
    -- 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' :: Thread s a
thread' = Thread s a -> Thread s a
forall s a. Thread s a -> Thread s a
stepThread Thread s a
thread 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{ races :: Races
races   = Thread s a -> SimState s a -> Races
forall s a. Thread s a -> SimState s a -> Races
updateRacesInSimState Thread s a
thread SimState s a
simstate,
                       control :: ScheduleControl
control = (ThreadId, Int) -> ScheduleControl -> ScheduleControl
advanceControl (Thread s a -> (ThreadId, Int)
forall s a. Thread s a -> (ThreadId, Int)
threadStepId Thread s a
thread) ScheduleControl
control }

deschedule Deschedule
Blocked thread :: Thread s a
thread@Thread { threadThrowTo :: forall s a.
Thread s a -> [(SomeException, Labelled ThreadId, VectorClock)]
threadThrowTo = (SomeException, Labelled ThreadId, VectorClock)
_ : [(SomeException, Labelled ThreadId, VectorClock)]
_
                                 , threadMasking :: forall s a. Thread s a -> MaskingState
threadMasking = MaskingState
maskst } SimState s a
simstate
    | MaskingState
maskst MaskingState -> MaskingState -> Bool
forall a. Eq a => a -> a -> Bool
/= MaskingState
MaskedUninterruptible =
    -- 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.
    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 :: MaskingState
threadMasking = MaskingState
Unmasked } SimState s a
simstate

deschedule Deschedule
Blocked Thread s a
thread simstate :: SimState s a
simstate@SimState{Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads, ScheduleControl
control :: ScheduleControl
control :: forall s a. SimState s a -> ScheduleControl
control} =
    let thread1 :: Thread s a
thread1 = Thread s a
thread { threadBlocked :: Bool
threadBlocked = Bool
True }
        thread' :: Thread s a
thread'  = Thread s a -> Thread s a
forall s a. Thread s a -> Thread s a
stepThread (Thread s a -> Thread s a) -> Thread s a -> Thread s a
forall a b. (a -> b) -> a -> b
$ Thread s a
thread1
        threads' :: Map ThreadId (Thread s a)
threads' = ThreadId
-> Thread s a
-> Map ThreadId (Thread s a)
-> Map ThreadId (Thread s a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Thread s a -> ThreadId
forall s a. Thread s a -> ThreadId
threadId Thread s a
thread') Thread s a
thread' Map ThreadId (Thread s a)
threads in
    SimState s a -> ST s (SimTrace a)
forall s a. SimState s a -> ST s (SimTrace a)
reschedule SimState s a
simstate { threads :: Map ThreadId (Thread s a)
threads = Map ThreadId (Thread s a)
threads',
                          races :: Races
races   = Thread s a -> SimState s a -> Races
forall s a. Thread s a -> SimState s a -> Races
updateRacesInSimState Thread s a
thread1 SimState s a
simstate,
                          control :: ScheduleControl
control = (ThreadId, Int) -> ScheduleControl -> ScheduleControl
advanceControl (Thread s a -> (ThreadId, Int)
forall s a. Thread s a -> (ThreadId, Int)
threadStepId Thread s a
thread1) ScheduleControl
control }

deschedule Deschedule
Terminated thread :: Thread s a
thread@Thread { threadId :: forall s a. Thread s a -> ThreadId
threadId = ThreadId
tid, threadVClock :: forall s a. Thread s a -> VectorClock
threadVClock = VectorClock
vClock }
                      simstate :: SimState s a
simstate@SimState{ curTime :: forall s a. SimState s a -> Time
curTime = Time
time, ScheduleControl
control :: ScheduleControl
control :: forall s a. SimState s a -> 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 thread' :: Thread s a
thread'     = Thread s a -> Thread s a
forall s a. Thread s a -> Thread s a
stepThread (Thread s a -> Thread s a) -> Thread s a -> Thread s a
forall a b. (a -> b) -> a -> b
$ Thread s a
thread{ threadDone :: Bool
threadDone = Bool
True }
        wakeup :: [ThreadId]
wakeup      = ((SomeException, Labelled ThreadId, VectorClock) -> ThreadId)
-> [(SomeException, Labelled ThreadId, VectorClock)] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeException
_,Labelled ThreadId
tid',VectorClock
_) -> Labelled ThreadId -> ThreadId
forall a. Labelled a -> a
l_labelled Labelled ThreadId
tid') ([(SomeException, Labelled ThreadId, VectorClock)]
-> [(SomeException, Labelled ThreadId, VectorClock)]
forall a. [a] -> [a]
reverse (Thread s a -> [(SomeException, Labelled ThreadId, VectorClock)]
forall s a.
Thread s a -> [(SomeException, Labelled ThreadId, VectorClock)]
threadThrowTo Thread s a
thread))
        ([ThreadId]
unblocked,
         simstate' :: SimState s a
simstate'@SimState{Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads}) =
                      VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
forall s a.
VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
unblockThreads VectorClock
vClock [ThreadId]
wakeup SimState s a
simstate
        threads' :: Map ThreadId (Thread s a)
threads'    = ThreadId
-> Thread s a
-> Map ThreadId (Thread s a)
-> Map ThreadId (Thread s a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ThreadId
tid Thread s a
thread' Map ThreadId (Thread s a)
threads
    -- We must keep terminated threads in the state to preserve their vector clocks,
    -- which matters when other threads throwTo them.
    !SimTrace a
trace <- SimState s a -> ST s (SimTrace a)
forall s a. SimState s a -> ST s (SimTrace a)
reschedule SimState s a
simstate' { races :: Races
races = ThreadId -> Races -> Races
threadTerminatesRaces ThreadId
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
updateRacesInSimState Thread s a
thread SimState s a
simstate,
                                    control :: ScheduleControl
control = (ThreadId, Int) -> ScheduleControl -> ScheduleControl
advanceControl (Thread s a -> (ThreadId, Int)
forall s a. Thread s a -> (ThreadId, Int)
threadStepId Thread s a
thread) ScheduleControl
control,
                                    threads :: Map ThreadId (Thread s a)
threads = Map ThreadId (Thread s a)
threads' }
    SimTrace a -> ST s (SimTrace 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, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany
               -- TODO: step
               [ (Time
time, ThreadId
tid', (-Int
1), Maybe ThreadLabel
tlbl', SimEventType
EventThrowToWakeup)
               | ThreadId
tid' <- [ThreadId]
unblocked
               , let tlbl' :: Maybe ThreadLabel
tlbl' = ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
forall s a.
ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel ThreadId
tid' Map ThreadId (Thread s a)
threads ]
               SimTrace a
trace

deschedule Deschedule
Sleep thread :: Thread s a
thread@Thread { threadId :: forall s a. Thread s a -> ThreadId
threadId = ThreadId
tid }
                 simstate :: SimState s a
simstate@SimState{RunQueue
runqueue :: RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue, Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (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 ThreadId (Thread s a)
threads'  = ThreadId
-> Thread s a
-> Map ThreadId (Thread s a)
-> Map ThreadId (Thread s a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ThreadId
tid Thread s a
thread Map ThreadId (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
runqueue = RunQueue
runqueue', threads :: Map ThreadId (Thread s a)
threads  = Map ThreadId (Thread s a)
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 :: SimState s a -> ST s (SimTrace a)
reschedule simstate :: SimState s a
simstate@SimState{ RunQueue
runqueue :: RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue, Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads,
                              control :: forall s a. SimState s a -> ScheduleControl
control=control :: ScheduleControl
control@(ControlFollow ((ThreadId
tid,Int
tstep):[(ThreadId, Int)]
_) [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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
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
$
    Bool -> ST s (SimTrace a) -> ST s (SimTrace a)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (ThreadId -> Down ThreadId
forall a. a -> Down a
Down ThreadId
tid Down ThreadId -> RunQueue -> Bool
forall k p v. Ord k => k -> OrdPSQ k p v -> Bool
`PSQ.member` RunQueue
runqueue) (ST s (SimTrace a) -> ST s (SimTrace a))
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall a b. (a -> b) -> a -> b
$
    Bool -> ST s (SimTrace a) -> ST s (SimTrace a)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (ThreadId
tid ThreadId -> Map ThreadId (Thread s a) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map ThreadId (Thread s a)
threads) (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 ThreadId (Thread s a)
threads Map ThreadId (Thread s a) -> ThreadId -> Thread s a
forall k a. Ord k => Map k a -> k -> a
Map.! ThreadId
tid in
    Bool -> ST s (SimTrace a) -> ST s (SimTrace a)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Thread s a -> ThreadId
forall s a. Thread s a -> ThreadId
threadId Thread s a
thread ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
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]
++ThreadId -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show ThreadId
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 :: RunQueue
runqueue = Down ThreadId -> RunQueue -> RunQueue
forall k p v. (Ord k, Ord p) => k -> OrdPSQ k p v -> OrdPSQ k p v
PSQ.delete (ThreadId -> Down ThreadId
forall a. a -> Down a
Down ThreadId
tid) RunQueue
runqueue
                             , threads :: Map ThreadId (Thread s a)
threads  = ThreadId -> Map ThreadId (Thread s a) -> Map ThreadId (Thread s a)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete ThreadId
tid Map ThreadId (Thread s a)
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 :: RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue, Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads }
    | Just (Down !ThreadId
tid, Down ThreadId
_, ()
_, RunQueue
runqueue') <- RunQueue -> Maybe (Down ThreadId, Down ThreadId, (), RunQueue)
forall k p v.
(Ord k, Ord p) =>
OrdPSQ k p v -> Maybe (k, p, v, OrdPSQ 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 ThreadId (Thread s a)
threads Map ThreadId (Thread s a) -> ThreadId -> Thread s a
forall k a. Ord k => Map k a -> k -> a
Map.! ThreadId
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
runqueue = RunQueue
runqueue'
                             , threads :: Map ThreadId (Thread s a)
threads  = ThreadId -> Map ThreadId (Thread s a) -> Map ThreadId (Thread s a)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete ThreadId
tid Map ThreadId (Thread s a)
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 ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads, OrdPSQ TimeoutId Time (TimerVars s)
timers :: OrdPSQ TimeoutId Time (TimerVars s)
timers :: forall s a. SimState s a -> OrdPSQ TimeoutId Time (TimerVars s)
timers, curTime :: forall s a. SimState s a -> Time
curTime = Time
time, Races
races :: Races
races :: forall s a. SimState s a -> 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 OrdPSQ TimeoutId Time (TimerVars s)
-> Maybe
     ([TimeoutId], Time, [TimerVars s],
      OrdPSQ TimeoutId Time (TimerVars s))
forall k p a.
(Ord k, Ord p) =>
OrdPSQ k p a -> Maybe ([k], p, [a], OrdPSQ k p a)
removeMinimums OrdPSQ TimeoutId Time (TimerVars s)
timers of
      Maybe
  ([TimeoutId], Time, [TimerVars s],
   OrdPSQ TimeoutId Time (TimerVars s))
Nothing -> SimTrace a -> ST s (SimTrace 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 ThreadId] -> SimTrace a
forall a. Time -> [Labelled ThreadId] -> SimTrace a
TraceDeadlock Time
time (Map ThreadId (Thread s a) -> [Labelled ThreadId]
forall s a. Map ThreadId (Thread s a) -> [Labelled ThreadId]
labelledThreads Map ThreadId (Thread s a)
threads))

      Just ([TimeoutId]
tmids, Time
time', [TimerVars s]
fired, OrdPSQ TimeoutId Time (TimerVars 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.
        [SomeTVar s]
written <- StmA s () -> ST s [SomeTVar s]
forall s. StmA s () -> ST s [SomeTVar s]
execAtomically' (STM s () -> StmA s ()
forall s a. STM s a -> StmA s a
runSTM (STM s () -> StmA s ()) -> STM s () -> StmA s ()
forall a b. (a -> b) -> a -> b
$ (TimerVars s -> STM s ()) -> [TimerVars s] -> STM s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TimerVars s -> STM s ()
forall (m :: * -> *) s.
(MonadSTM m, TVar m ~ TVar s) =>
TimerVars s -> STM m ()
timeoutAction [TimerVars s]
fired)
        ([ThreadId]
wakeup, Map ThreadId (Set (Labelled TVarId))
wokeby) <- [SomeTVar s]
-> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId)))
forall s.
[SomeTVar s]
-> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId)))
threadsUnblockedByWrites [SomeTVar s]
written
        (SomeTVar s -> ST s ()) -> [SomeTVar s] -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(SomeTVar TVar s a
tvar) -> TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar s a
tvar) [SomeTVar s]
written

        -- TODO: the vector clock below cannot be right, can it?
        let ([ThreadId]
unblocked,
             SimState s a
simstate') = VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
forall s a.
VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
unblockThreads VectorClock
bottomVClock [ThreadId]
wakeup SimState s a
simstate
            -- all open races will be completed and reported at this time
            simstate'' :: SimState s a
simstate''  = SimState s a
simstate'{ races :: Races
races = Races
noRaces }
        !SimTrace a
trace <- SimState s a -> ST s (SimTrace a)
forall s a. SimState s a -> ST s (SimTrace a)
reschedule SimState s a
simstate'' { curTime :: Time
curTime = Time
time'
                                        , timers :: OrdPSQ TimeoutId Time (TimerVars s)
timers  = OrdPSQ TimeoutId Time (TimerVars s)
timers' }
        let traceEntries :: [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
traceEntries =
                     [ (Time
time', [Int] -> ThreadId
ThreadId [-Int
1], (-Int
1), ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
"timer", TimeoutId -> SimEventType
EventTimerExpired TimeoutId
tmid)
                     | TimeoutId
tmid <- [TimeoutId]
tmids ]
                  [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
forall a. [a] -> [a] -> [a]
++ [ (Time
time', ThreadId
tid', (-Int
1), Maybe ThreadLabel
tlbl', [Labelled TVarId] -> SimEventType
EventTxWakeup [Labelled TVarId]
vids)
                     | ThreadId
tid' <- [ThreadId]
unblocked
                     , let tlbl' :: Maybe ThreadLabel
tlbl' = ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
forall s a.
ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel ThreadId
tid' Map ThreadId (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
<$> ThreadId
-> Map ThreadId (Set (Labelled TVarId))
-> Maybe (Set (Labelled TVarId))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ThreadId
tid' Map ThreadId (Set (Labelled TVarId))
wokeby ]
        SimTrace a -> ST s (SimTrace 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
$
          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, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
traceEntries SimTrace a
trace
  where
    timeoutAction :: TimerVars s -> STM m ()
timeoutAction (TimerVars TVar s TimeoutState
var TVar s Bool
bvar) = do
      TimeoutState
x <- TVar m TimeoutState -> STM m TimeoutState
forall (m :: * -> *) a. MonadSTM m => TVar m a -> STM m a
readTVar TVar m TimeoutState
TVar s TimeoutState
var
      case TimeoutState
x of
        TimeoutState
TimeoutPending   -> TVar m TimeoutState -> TimeoutState -> STM m ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar TVar m TimeoutState
TVar s TimeoutState
var  TimeoutState
TimeoutFired
                         STM m () -> STM m () -> STM m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TVar m Bool -> Bool -> STM m ()
forall (m :: * -> *) a. MonadSTM m => TVar m a -> a -> STM m ()
writeTVar TVar m Bool
TVar s Bool
bvar Bool
True
        TimeoutState
TimeoutFired     -> ThreadLabel -> STM m ()
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"MonadTimer(Sim): invariant violation"
        TimeoutState
TimeoutCancelled -> () -> STM m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

unblockThreads :: forall s a.
                  VectorClock
               -> [ThreadId]
               -> SimState s a
               -> ([ThreadId], SimState s a)
unblockThreads :: VectorClock
-> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a)
unblockThreads VectorClock
vClock [ThreadId]
wakeup simstate :: SimState s a
simstate@SimState {RunQueue
runqueue :: RunQueue
runqueue :: forall s a. SimState s a -> RunQueue
runqueue, Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads} =
    -- To preserve our invariants (that threadBlocked is correct)
    -- we update the runqueue and threads together here
    ( [ThreadId]
unblockedIds
    , SimState s a
simstate { runqueue :: RunQueue
runqueue = (Thread s a -> RunQueue -> RunQueue)
-> RunQueue -> [Thread s a] -> RunQueue
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Thread s a -> RunQueue -> RunQueue
forall s a. Thread s a -> RunQueue -> RunQueue
insertThread RunQueue
runqueue [Thread s a]
unblocked,
                 threads :: Map ThreadId (Thread s a)
threads  = Map ThreadId (Thread s a)
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
                 | ThreadId
tid <- [ThreadId]
wakeup
                 , Thread s a
thread <-
                     case ThreadId -> Map ThreadId (Thread s a) -> Maybe (Thread s a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ThreadId
tid Map ThreadId (Thread s a)
threads of
                       Just   Thread { threadDone :: forall s a. Thread s a -> Bool
threadDone    = Bool
True } -> [ ]
                       Just t :: Thread s a
t@Thread { threadBlocked :: forall s a. Thread s a -> Bool
threadBlocked = Bool
True } -> [Thread s a
t]
                       Maybe (Thread s a)
_                                      -> [ ]
                 ]

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

    -- and in which case we mark them as now running
    !threads' :: Map ThreadId (Thread s a)
threads'  = (Map ThreadId (Thread s a)
 -> ThreadId -> Map ThreadId (Thread s a))
-> Map ThreadId (Thread s a)
-> [ThreadId]
-> Map ThreadId (Thread s a)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl'
                   ((ThreadId
 -> Map ThreadId (Thread s a) -> Map ThreadId (Thread s a))
-> Map ThreadId (Thread s a)
-> ThreadId
-> Map ThreadId (Thread s a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Thread s a -> Thread s a)
-> ThreadId
-> Map ThreadId (Thread s a)
-> Map ThreadId (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 { threadBlocked :: Bool
threadBlocked = Bool
False,
                                threadVClock :: VectorClock
threadVClock = VectorClock
vClock VectorClock -> VectorClock -> VectorClock
`leastUpperBoundVClock` Thread s a -> VectorClock
forall s a. Thread s a -> VectorClock
threadVClock Thread s a
t })))
                   Map ThreadId (Thread s a)
threads [ThreadId]
unblockedIds


-- | 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
                   -> Either Bool (Thread s a)
unwindControlStack :: SomeException -> Thread s a -> Either Bool (Thread s a)
unwindControlStack SomeException
e Thread s a
thread =
    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 -> Either Bool (Thread s a)
forall s' c.
MaskingState -> ControlStack s' c a -> Either Bool (Thread s' a)
unwind (Thread s a -> MaskingState
forall s a. Thread s a -> MaskingState
threadMasking Thread s a
thread) ControlStack s b a
ctl
  where
    unwind :: forall s' c. MaskingState
           -> ControlStack s' c a -> Either Bool (Thread s' a)
    unwind :: MaskingState -> ControlStack s' c a -> Either Bool (Thread s' a)
unwind MaskingState
_  ControlStack s' c a
MainFrame                 = Bool -> Either Bool (Thread s' a)
forall a b. a -> Either a b
Left Bool
True
    unwind MaskingState
_  ControlStack s' c a
ForkFrame                 = Bool -> Either Bool (Thread s' a)
forall a b. a -> Either a b
Left Bool
False
    unwind MaskingState
_ (MaskFrame c -> SimA s' c
_k MaskingState
maskst' ControlStack s' c a
ctl) = MaskingState -> ControlStack s' c a -> Either Bool (Thread s' a)
forall s' c.
MaskingState -> ControlStack s' c a -> Either Bool (Thread s' a)
unwind MaskingState
maskst' ControlStack s' c a
ctl

    unwind MaskingState
maskst (CatchFrame e -> SimA s' c
handler c -> SimA s' c
k ControlStack s' c a
ctl) =
      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 -> Either Bool (Thread s' a)
forall s' c.
MaskingState -> ControlStack s' c a -> Either Bool (Thread s' a)
unwind MaskingState
maskst ControlStack s' c a
ctl

        -- 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 s' a
threadControl = SimA s' c -> ControlStack s' c a -> ThreadControl s' a
forall s b a. SimA s b -> ControlStack s b a -> ThreadControl s a
ThreadControl (e -> SimA s' c
handler e
e')
                                                   ((c -> SimA s' c)
-> MaskingState -> ControlStack s' c a -> ControlStack s' c a
forall b s c a.
(b -> SimA s c)
-> MaskingState -> ControlStack s c a -> ControlStack s b a
MaskFrame c -> SimA s' c
k MaskingState
maskst ControlStack s' c a
ctl),
                     threadMasking :: MaskingState
threadMasking = MaskingState -> MaskingState
atLeastInterruptibleMask MaskingState
maskst
                   }

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


removeMinimums :: (Ord k, Ord p)
               => OrdPSQ k p a
               -> Maybe ([k], p, [a], OrdPSQ k p a)
removeMinimums :: OrdPSQ k p a -> Maybe ([k], p, [a], OrdPSQ k p a)
removeMinimums = \OrdPSQ k p a
psq ->
    case OrdPSQ k p a -> Maybe (k, p, a, OrdPSQ k p a)
forall k p v.
(Ord k, Ord p) =>
OrdPSQ k p v -> Maybe (k, p, v, OrdPSQ k p v)
PSQ.minView OrdPSQ k p a
psq of
      Maybe (k, p, a, OrdPSQ k p a)
Nothing              -> Maybe ([k], p, [a], OrdPSQ k p a)
forall a. Maybe a
Nothing
      Just (k
k, p
p, a
x, OrdPSQ k p a
psq') -> ([k], p, [a], OrdPSQ k p a) -> Maybe ([k], p, [a], OrdPSQ k p a)
forall a. a -> Maybe a
Just ([k] -> p -> [a] -> OrdPSQ k p a -> ([k], p, [a], OrdPSQ k p a)
forall a b a.
(Ord a, Ord b) =>
[a] -> b -> [a] -> OrdPSQ a b a -> ([a], b, [a], OrdPSQ a b a)
collectAll [k
k] p
p [a
x] OrdPSQ k p a
psq')
  where
    collectAll :: [a] -> b -> [a] -> OrdPSQ a b a -> ([a], b, [a], OrdPSQ a b a)
collectAll [a]
ks b
p [a]
xs OrdPSQ a b a
psq =
      case OrdPSQ a b a -> Maybe (a, b, a, OrdPSQ a b a)
forall k p v.
(Ord k, Ord p) =>
OrdPSQ k p v -> Maybe (k, p, v, OrdPSQ k p v)
PSQ.minView OrdPSQ a b a
psq of
        Just (a
k, b
p', a
x, OrdPSQ a b a
psq')
          | b
p b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
p' -> [a] -> b -> [a] -> OrdPSQ a b a -> ([a], b, [a], OrdPSQ a b a)
collectAll (a
ka -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ks) b
p (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) OrdPSQ a b a
psq'
        Maybe (a, b, a, OrdPSQ a b a)
_           -> ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
ks, b
p, [a] -> [a]
forall a. [a] -> [a]
reverse [a]
xs, OrdPSQ a b a
psq)

traceMany :: [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
          -> SimTrace a -> SimTrace a
traceMany :: [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany []                                   SimTrace a
trace = SimTrace a
trace
traceMany ((Time
time, ThreadId
tid, Int
tstep, Maybe ThreadLabel
tlbl, SimEventType
event):[(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
ts) SimTrace a
trace =
    Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid Int
tstep Maybe ThreadLabel
tlbl SimEventType
event ([(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
forall a.
[(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
-> SimTrace a -> SimTrace a
traceMany [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)]
ts SimTrace a
trace)

lookupThreadLabel :: ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel :: ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel
lookupThreadLabel ThreadId
tid Map ThreadId (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
<$> ThreadId -> Map ThreadId (Thread s a) -> Maybe (Thread s a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ThreadId
tid Map ThreadId (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 :: 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 :: Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST Maybe Int
limit ScheduleControl
control IOSim s a
mainAction =
  Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace (SimState Any Any -> Time
forall s a. SimState s a -> Time
curTime SimState Any Any
forall s a. SimState s a
initialState)
           (Thread s a -> ThreadId
forall s a. Thread s a -> ThreadId
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 :: ScheduleControl
control  = ScheduleControl
control,
                                         control0 :: ScheduleControl
control0 = ScheduleControl
control,
                                         perStepTimeLimit :: Maybe Int
perStepTimeLimit = Maybe Int
limit
                                       }
  where
    mainThread :: Thread s a
mainThread =
      Thread :: forall s a.
ThreadId
-> ThreadControl s a
-> Bool
-> Bool
-> MaskingState
-> [(SomeException, Labelled ThreadId, VectorClock)]
-> ClockId
-> Maybe ThreadLabel
-> Int
-> Int
-> VectorClock
-> Effect
-> Bool
-> Thread s a
Thread {
        threadId :: ThreadId
threadId      = [Int] -> ThreadId
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 a. ControlStack s a a
MainFrame,
        threadBlocked :: Bool
threadBlocked = Bool
False,
        threadDone :: Bool
threadDone    = Bool
False,
        threadMasking :: MaskingState
threadMasking = MaskingState
Unmasked,
        threadThrowTo :: [(SomeException, Labelled ThreadId, 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  = ThreadId -> Int -> VectorClock -> VectorClock
insertVClock ([Int] -> ThreadId
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.
                  Time
               -> ThreadId
               -> Maybe ThreadLabel
               -> TVarId
               -> StmA s a
               -> (StmTxResult s a -> ST s (SimTrace c))
               -> ST s (SimTrace c)
execAtomically :: Time
-> ThreadId
-> Maybe ThreadLabel
-> TVarId
-> StmA s a
-> (StmTxResult s a -> ST s (SimTrace c))
-> ST s (SimTrace c)
execAtomically Time
time ThreadId
tid Maybe ThreadLabel
tlbl TVarId
nextVid0 StmA s a
action0 StmTxResult s a -> ST s (SimTrace c)
k0 =
    StmStack s a a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s a
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s a a
forall s a. StmStack s a a
AtomicallyFrame Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty [] [] TVarId
nextVid0 StmA s a
action0
  where
    go :: forall b.
          StmStack s b a
       -> Map TVarId (SomeTVar s)  -- 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
       -> TVarId                   -- var fresh name supply
       -> StmA s b
       -> ST s (SimTrace c)
    go :: StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go !StmStack s b a
ctl !Map TVarId (SomeTVar s)
read !Map TVarId (SomeTVar s)
written ![SomeTVar s]
writtenSeq ![SomeTVar s]
createdSeq !TVarId
nextVid StmA s b
action = Bool -> ST s (SimTrace c) -> ST s (SimTrace c)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert Bool
localInvariant (ST s (SimTrace c) -> ST s (SimTrace c))
-> ST s (SimTrace c) -> ST s (SimTrace c)
forall a b. (a -> b) -> a -> b
$
                                                       case StmA s b
action of
      ReturnStm b
x ->
        {-# SCC "execAtomically.go.ReturnStm" #-}
        case StmStack s b a
ctl of
        StmStack s b a
AtomicallyFrame -> do
          -- Trace each created TVar
          ![TraceValue]
ds  <- (SomeTVar s -> ST s TraceValue)
-> [SomeTVar s] -> ST s [TraceValue]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
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
          ![TraceValue]
ds' <- Map TVarId TraceValue -> [TraceValue]
forall k a. Map k a -> [a]
Map.elems (Map TVarId TraceValue -> [TraceValue])
-> ST s (Map TVarId TraceValue) -> ST s [TraceValue]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SomeTVar s -> ST s TraceValue)
-> Map TVarId (SomeTVar s) -> ST s (Map TVarId TraceValue)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse
                    (\(SomeTVar TVar s a
tvar) -> do
                        TraceValue
tr <- TVar s a -> Bool -> ST s TraceValue
forall s a. TVar s a -> Bool -> ST s TraceValue
traceTVarST TVar s a
tvar Bool
False
                        !()
_ <- TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
commitTVar TVar s a
tvar
                        -- Also assert the data invariant that outside a tx
                        -- the undo stack is empty:
                        [a]
undos <- TVar s a -> ST s [a]
forall s a. TVar s a -> ST s [a]
readTVarUndos TVar s a
tvar
                        Bool -> ST s TraceValue -> ST s TraceValue
forall a. (?callStack::CallStack) => Bool -> a -> a
assert ([a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
undos) (ST s TraceValue -> ST s TraceValue)
-> ST s TraceValue -> ST s TraceValue
forall a b. (a -> b) -> a -> b
$ TraceValue -> ST s TraceValue
forall (m :: * -> *) a. Monad m => a -> m a
return TraceValue
tr
                    ) Map TVarId (SomeTVar s)
written

          -- Return the vars written, so readers can be unblocked
          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
$ b
-> [SomeTVar s]
-> [SomeTVar s]
-> [SomeTVar s]
-> [Dynamic]
-> [ThreadLabel]
-> TVarId
-> StmTxResult s b
forall s a.
a
-> [SomeTVar s]
-> [SomeTVar s]
-> [SomeTVar s]
-> [Dynamic]
-> [ThreadLabel]
-> TVarId
-> StmTxResult s a
StmTxCommitted b
x ([SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a]
reverse [SomeTVar s]
writtenSeq)
                                (Map TVarId (SomeTVar s) -> [SomeTVar s]
forall k a. Map k a -> [a]
Map.elems Map TVarId (SomeTVar s)
read)
                                ([SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a]
reverse [SomeTVar s]
createdSeq)
                                ((TraceValue -> Maybe Dynamic) -> [TraceValue] -> [Dynamic]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\TraceValue { Maybe tr
traceDynamic :: ()
traceDynamic :: Maybe tr
traceDynamic }
                                            -> tr -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn (tr -> Dynamic) -> Maybe tr -> Maybe Dynamic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe tr
traceDynamic)
                                          ([TraceValue] -> [Dynamic]) -> [TraceValue] -> [Dynamic]
forall a b. (a -> b) -> a -> b
$ [TraceValue]
ds [TraceValue] -> [TraceValue] -> [TraceValue]
forall a. [a] -> [a] -> [a]
++ [TraceValue]
ds')
                                ((TraceValue -> Maybe ThreadLabel) -> [TraceValue] -> [ThreadLabel]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TraceValue -> Maybe ThreadLabel
traceString ([TraceValue] -> [ThreadLabel]) -> [TraceValue] -> [ThreadLabel]
forall a b. (a -> b) -> a -> b
$ [TraceValue]
ds [TraceValue] -> [TraceValue] -> [TraceValue]
forall a. [a] -> [a] -> [a]
++ [TraceValue]
ds')
                                TVarId
nextVid

        OrElseLeftFrame StmA s b
_b b -> StmA s b
k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b a
ctl' -> do
          -- 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)
written'    = Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map TVarId (SomeTVar s)
written Map TVarId (SomeTVar s)
writtenOuter
              writtenSeq' :: [SomeTVar s]
writtenSeq' = (SomeTVar s -> Bool) -> [SomeTVar s] -> [SomeTVar s]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(SomeTVar TVar s a
tvar) ->
                                      TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
tvar TVarId -> Map TVarId (SomeTVar s) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map TVarId (SomeTVar s)
writtenOuter)
                                    [SomeTVar s]
writtenSeq
                         [SomeTVar s] -> [SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a] -> [a]
++ [SomeTVar s]
writtenOuterSeq
          -- Skip the orElse right hand and continue with the k continuation
          StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written' [SomeTVar s]
writtenSeq' [SomeTVar s]
createdOuterSeq TVarId
nextVid (b -> StmA s b
k b
x)

        OrElseRightFrame b -> StmA s b
k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b a
ctl' -> do
          -- 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)
written'    = Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map TVarId (SomeTVar s)
written Map TVarId (SomeTVar s)
writtenOuter
              writtenSeq' :: [SomeTVar s]
writtenSeq' = (SomeTVar s -> Bool) -> [SomeTVar s] -> [SomeTVar s]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(SomeTVar TVar s a
tvar) ->
                                      TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
tvar TVarId -> Map TVarId (SomeTVar s) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map TVarId (SomeTVar s)
writtenOuter)
                                    [SomeTVar s]
writtenSeq
                         [SomeTVar s] -> [SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a] -> [a]
++ [SomeTVar s]
writtenOuterSeq
              createdSeq' :: [SomeTVar s]
createdSeq' = [SomeTVar s]
createdSeq [SomeTVar s] -> [SomeTVar s] -> [SomeTVar s]
forall a. [a] -> [a] -> [a]
++ [SomeTVar s]
createdOuterSeq
          -- Continue with the k continuation
          StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written' [SomeTVar s]
writtenSeq' [SomeTVar s]
createdSeq' TVarId
nextVid (b -> StmA s b
k b
x)

      ThrowStm SomeException
e ->
        {-# SCC "execAtomically.go.ThrowStm" #-} 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
        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)

      StmA s b
Retry ->
        {-# SCC "execAtomically.go.Retry" #-}
        case StmStack s b a
ctl of
        StmStack s b a
AtomicallyFrame -> 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
          -- 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

        OrElseLeftFrame StmA s b
b b -> StmA s b
k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b a
ctl' ->
          {-# SCC "execAtomically.go.OrElseLeftFrame" #-} do
          -- Revert all the TVar writes within this orElse
          !()
_ <- (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
          -- Execute the orElse right hand with an empty written set
          let ctl'' :: StmStack s b a
ctl'' = (b -> StmA s b)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b a
-> StmStack s b a
forall a s b c.
(a -> StmA s b)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b c
-> StmStack s a c
OrElseRightFrame b -> StmA s b
k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b a
ctl'
          StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl'' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty [] [] TVarId
nextVid StmA s b
b

        OrElseRightFrame b -> StmA s b
_k Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq StmStack s b a
ctl' ->
          {-# SCC "execAtomically.go.OrElseRightFrame" #-} do
          -- Revert all the TVar writes within this orElse branch
          !()
_ <- (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
          -- Skip the continuation and propagate the retry into the outer frame
          -- using the written set for the outer frame
          StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
writtenOuter [SomeTVar s]
writtenOuterSeq [SomeTVar s]
createdOuterSeq TVarId
nextVid StmA s b
forall s b. StmA s b
Retry

      OrElse StmA s a
a StmA s a
b a -> StmA s b
k ->
        {-# SCC "execAtomically.go.OrElse" #-} do
        -- Execute the left side in a new frame with an empty written set
        let ctl' :: StmStack s a a
ctl' = StmA s a
-> (a -> StmA s b)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b a
-> StmStack s a a
forall s a b c.
StmA s a
-> (a -> StmA s b)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> StmStack s b c
-> StmStack s a c
OrElseLeftFrame StmA s a
b a -> StmA s b
k Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq StmStack s b a
ctl
        StmStack s a a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s a
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s a a
ctl' Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
forall k a. Map k a
Map.empty [] [] TVarId
nextVid StmA s a
a

      NewTVar !Maybe ThreadLabel
mbLabel x
x TVar s x -> StmA s b
k ->
        {-# SCC "execAtomically.go.NewTVar" #-} do
        !TVar s x
v <- TVarId -> Maybe ThreadLabel -> x -> ST s (TVar s x)
forall a s. TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar TVarId
nextVid Maybe ThreadLabel
mbLabel x
x
        -- record a write to the TVar so we know to update its VClock
        let written' :: Map TVarId (SomeTVar s)
written' = TVarId
-> SomeTVar s -> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (TVar s 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
        !()
_ <- TVar s x -> ST s ()
forall s a. TVar s a -> ST s ()
saveTVar TVar s x
v
        StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written' [SomeTVar s]
writtenSeq (TVar s x -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s x
v SomeTVar s -> [SomeTVar s] -> [SomeTVar s]
forall a. a -> [a] -> [a]
: [SomeTVar s]
createdSeq) (TVarId -> TVarId
forall a. Enum a => a -> a
succ TVarId
nextVid) (TVar s x -> StmA s b
k TVar s x
v)

      LabelTVar !ThreadLabel
label TVar s a
tvar StmA s b
k ->
        {-# SCC "execAtomically.go.LabelTVar" #-} do
        !()
_ <- STRef s (Maybe ThreadLabel) -> Maybe ThreadLabel -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef (TVar s a -> STRef s (Maybe ThreadLabel)
forall s a. TVar s a -> STRef s (Maybe ThreadLabel)
tvarLabel TVar s a
tvar) (Maybe ThreadLabel -> ST s ()) -> Maybe ThreadLabel -> ST s ()
forall a b. (a -> b) -> a -> b
$! (ThreadLabel -> Maybe ThreadLabel
forall a. a -> Maybe a
Just ThreadLabel
label)
        StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k

      TraceTVar TVar s a
tvar Maybe a -> a -> ST s TraceValue
f StmA s b
k ->
        {-# SCC "execAtomically.go.TraceTVar" #-} do
        !()
_ <- STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
-> Maybe (Maybe a -> a -> ST s TraceValue) -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef (TVar s a -> STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
forall s a.
TVar s a -> STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace TVar s a
tvar) ((Maybe a -> a -> ST s TraceValue)
-> Maybe (Maybe a -> a -> ST s TraceValue)
forall a. a -> Maybe a
Just Maybe a -> a -> ST s TraceValue
f)
        StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k

      ReadTVar TVar s a
v a -> StmA s b
k
        | TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
v TVarId -> Map TVarId (SomeTVar s) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map TVarId (SomeTVar s)
read ->
            {-# SCC "execAtomically.go.ReadTVar" #-} do
            a
x <- TVar s a -> ST s a
forall s a. TVar s a -> ST s a
execReadTVar TVar s a
v
            StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid (a -> StmA s b
k a
x)
        | Bool
otherwise ->
            {-# SCC "execAtomically.go.ReadTVar" #-} do
            a
x <- TVar s a -> ST s a
forall s a. TVar s a -> ST s a
execReadTVar TVar s a
v
            let read' :: Map TVarId (SomeTVar s)
read' = TVarId
-> SomeTVar s -> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
v) (TVar s a -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s a
v) Map TVarId (SomeTVar s)
read
            StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read' Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid (a -> StmA s b
k a
x)

      WriteTVar TVar s a
v a
x StmA s b
k
        | TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
v TVarId -> Map TVarId (SomeTVar s) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map TVarId (SomeTVar s)
written ->
            {-# SCC "execAtomically.go.WriteTVar" #-} do
            !()
_ <- TVar s a -> a -> ST s ()
forall s a. TVar s a -> a -> ST s ()
execWriteTVar TVar s a
v a
x
            StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k
        | Bool
otherwise ->
            {-# SCC "execAtomically.go.WriteTVar" #-} do
            !()
_ <- TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
saveTVar TVar s a
v
            !()
_ <- TVar s a -> a -> ST s ()
forall s a. TVar s a -> a -> ST s ()
execWriteTVar TVar s a
v a
x
            let written' :: Map TVarId (SomeTVar s)
written' = TVarId
-> SomeTVar s -> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
v) (TVar s a -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s a
v) Map TVarId (SomeTVar s)
written
            StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written' (TVar s a -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s a
v SomeTVar s -> [SomeTVar s] -> [SomeTVar s]
forall a. a -> [a] -> [a]
: [SomeTVar s]
writtenSeq) [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k

      SayStm ThreadLabel
msg StmA s b
k ->
        {-# SCC "execAtomically.go.SayStm" #-} do
        SimTrace c
trace <- StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k
        -- TODO: step
        SimTrace c -> ST s (SimTrace c)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace c -> ST s (SimTrace c))
-> SimTrace c -> ST s (SimTrace c)
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace c
-> SimTrace c
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid (-Int
1) Maybe ThreadLabel
tlbl (ThreadLabel -> SimEventType
EventSay ThreadLabel
msg) SimTrace c
trace

      OutputStm Dynamic
x StmA s b
k ->
        {-# SCC "execAtomically.go.OutputStm" #-} do
        SimTrace c
trace <- StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
forall b.
StmStack s b a
-> Map TVarId (SomeTVar s)
-> Map TVarId (SomeTVar s)
-> [SomeTVar s]
-> [SomeTVar s]
-> TVarId
-> StmA s b
-> ST s (SimTrace c)
go StmStack s b a
ctl Map TVarId (SomeTVar s)
read Map TVarId (SomeTVar s)
written [SomeTVar s]
writtenSeq [SomeTVar s]
createdSeq TVarId
nextVid StmA s b
k
        -- TODO: step
        SimTrace c -> ST s (SimTrace c)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace c -> ST s (SimTrace c))
-> SimTrace c -> ST s (SimTrace c)
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace c
-> SimTrace c
forall a.
Time
-> ThreadId
-> Int
-> Maybe ThreadLabel
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
time ThreadId
tid (-Int
1) Maybe ThreadLabel
tlbl (Dynamic -> SimEventType
EventLog Dynamic
x) SimTrace c
trace

      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 ])


-- | Special case of 'execAtomically' supporting only var reads and writes
--
execAtomically' :: StmA s () -> ST s [SomeTVar s]
execAtomically' :: 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 :: 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 ()) -> 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)
written
        [SomeTVar s] -> ST s [SomeTVar s]
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 a
v a -> StmA s ()
k  -> do
        a
x <- TVar s a -> ST s a
forall s a. TVar s a -> ST s a
execReadTVar TVar s a
v
        Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
forall s. Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
go Map TVarId (SomeTVar s)
written (a -> StmA s ()
k a
x)
      WriteTVar TVar s a
v a
x StmA s ()
k
        | TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
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 a -> a -> ST s ()
forall s a. TVar s a -> a -> ST s ()
execWriteTVar TVar s a
v a
x
            Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
forall s. Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
go Map TVarId (SomeTVar s)
written StmA s ()
k
        | Bool
otherwise -> do
            !()
_ <- TVar s a -> ST s ()
forall s a. TVar s a -> ST s ()
saveTVar TVar s a
v
            !()
_ <- TVar s a -> a -> ST s ()
forall s a. TVar s a -> a -> ST s ()
execWriteTVar TVar s a
v a
x
            let written' :: Map TVarId (SomeTVar s)
written' = TVarId
-> SomeTVar s -> Map TVarId (SomeTVar s) -> Map TVarId (SomeTVar s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
v) (TVar s a -> SomeTVar s
forall s a. TVar s a -> SomeTVar s
SomeTVar TVar s a
v) Map TVarId (SomeTVar s)
written
            Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
forall s. Map TVarId (SomeTVar s) -> StmA s () -> ST s [SomeTVar s]
go Map TVarId (SomeTVar s)
written' StmA s ()
k
      StmA s ()
_ -> ThreadLabel -> ST s [SomeTVar s]
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"execAtomically': only for special case of reads and writes"


execNewTVar :: TVarId -> Maybe String -> a -> ST s (TVar s a)
execNewTVar :: TVarId -> Maybe ThreadLabel -> a -> ST s (TVar s a)
execNewTVar TVarId
nextVid !Maybe ThreadLabel
mbLabel a
x = do
    STRef s (Maybe ThreadLabel)
tvarLabel   <- Maybe ThreadLabel -> ST s (STRef s (Maybe ThreadLabel))
forall a s. a -> ST s (STRef s a)
newSTRef Maybe ThreadLabel
mbLabel
    STRef s a
tvarCurrent <- a -> ST s (STRef s a)
forall a s. a -> ST s (STRef s a)
newSTRef a
x
    STRef s [a]
tvarUndo    <- [a] -> ST s (STRef s [a])
forall a s. a -> ST s (STRef s a)
newSTRef []
    STRef s ([ThreadId], Set ThreadId)
tvarBlocked <- ([ThreadId], Set ThreadId)
-> ST s (STRef s ([ThreadId], Set ThreadId))
forall a s. a -> ST s (STRef s a)
newSTRef ([], Set ThreadId
forall a. Set a
Set.empty)
    STRef s VectorClock
tvarVClock  <- VectorClock -> ST s (STRef s VectorClock)
forall a s. a -> ST s (STRef s a)
newSTRef VectorClock
bottomVClock
    STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace   <- Maybe (Maybe a -> a -> ST s TraceValue)
-> ST s (STRef s (Maybe (Maybe a -> a -> ST s TraceValue)))
forall a s. a -> ST s (STRef s a)
newSTRef Maybe (Maybe a -> a -> ST s TraceValue)
forall a. Maybe a
Nothing
    TVar s a -> ST s (TVar s a)
forall (m :: * -> *) a. Monad m => a -> m a
return TVar :: forall s a.
TVarId
-> STRef s (Maybe ThreadLabel)
-> STRef s a
-> STRef s [a]
-> STRef s ([ThreadId], Set ThreadId)
-> STRef s VectorClock
-> STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
-> TVar s a
TVar {tvarId :: TVarId
tvarId = TVarId
nextVid, STRef s (Maybe ThreadLabel)
tvarLabel :: STRef s (Maybe ThreadLabel)
tvarLabel :: STRef s (Maybe ThreadLabel)
tvarLabel,
                 STRef s a
tvarCurrent :: STRef s a
tvarCurrent :: STRef s a
tvarCurrent, STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo, STRef s ([ThreadId], Set ThreadId)
tvarBlocked :: STRef s ([ThreadId], Set ThreadId)
tvarBlocked :: STRef s ([ThreadId], Set ThreadId)
tvarBlocked, STRef s VectorClock
tvarVClock :: STRef s VectorClock
tvarVClock :: STRef s VectorClock
tvarVClock,
                 STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace :: STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace :: STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace}

execReadTVar :: TVar s a -> ST s a
execReadTVar :: TVar s a -> ST s a
execReadTVar TVar{STRef s a
tvarCurrent :: STRef s a
tvarCurrent :: forall s a. TVar s a -> STRef s a
tvarCurrent} = STRef s a -> ST s a
forall s a. STRef s a -> ST s a
readSTRef STRef s a
tvarCurrent
{-# INLINE execReadTVar #-}

execWriteTVar :: TVar s a -> a -> ST s ()
execWriteTVar :: TVar s a -> a -> ST s ()
execWriteTVar TVar{STRef s a
tvarCurrent :: STRef s a
tvarCurrent :: forall s a. TVar s a -> 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 #-}

saveTVar :: TVar s a -> ST s ()
saveTVar :: TVar s a -> ST s ()
saveTVar TVar{STRef s a
tvarCurrent :: STRef s a
tvarCurrent :: forall s a. TVar s a -> STRef s a
tvarCurrent, STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo :: forall s a. TVar s a -> STRef s [a]
tvarUndo} = do
    -- push the current value onto the undo stack
    a
v  <- STRef s a -> ST s a
forall s a. STRef s a -> ST s a
readSTRef STRef s a
tvarCurrent
    [a]
vs <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
    STRef s [a] -> [a] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [a]
tvarUndo (a
va -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
vs)

revertTVar :: TVar s a -> ST s ()
revertTVar :: TVar s a -> ST s ()
revertTVar TVar{STRef s a
tvarCurrent :: STRef s a
tvarCurrent :: forall s a. TVar s a -> STRef s a
tvarCurrent, STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo :: forall s a. TVar s a -> STRef s [a]
tvarUndo} = do
    -- pop the undo stack, and revert the current value
    (a
v:[a]
vs) <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
    STRef s a -> a -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s a
tvarCurrent a
v
    STRef s [a] -> [a] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [a]
tvarUndo    [a]
vs
{-# INLINE revertTVar #-}

commitTVar :: TVar s a -> ST s ()
commitTVar :: TVar s a -> ST s ()
commitTVar TVar{STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo :: forall s a. TVar s a -> STRef s [a]
tvarUndo} = do
    -- pop the undo stack, leaving the current value unchanged
    (a
_:[a]
vs) <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
    STRef s [a] -> [a] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [a]
tvarUndo [a]
vs
{-# INLINE commitTVar #-}

readTVarUndos :: TVar s a -> ST s [a]
readTVarUndos :: TVar s a -> ST s [a]
readTVarUndos TVar{STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo :: forall s a. TVar s a -> 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 :: TVar s a -> Bool -> ST s TraceValue
traceTVarST TVar{STRef s a
tvarCurrent :: STRef s a
tvarCurrent :: forall s a. TVar s a -> STRef s a
tvarCurrent, STRef s [a]
tvarUndo :: STRef s [a]
tvarUndo :: forall s a. TVar s a -> STRef s [a]
tvarUndo, STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace :: 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} Bool
new = do
    Maybe (Maybe a -> a -> ST s TraceValue)
mf <- STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
-> ST s (Maybe (Maybe a -> a -> ST s TraceValue))
forall s a. STRef s a -> ST s a
readSTRef STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace
    case Maybe (Maybe a -> a -> ST s TraceValue)
mf of
      Maybe (Maybe a -> a -> ST s TraceValue)
Nothing -> TraceValue -> ST s TraceValue
forall (m :: * -> *) a. Monad m => a -> m a
return TraceValue :: forall tr.
Typeable tr =>
Maybe tr -> Maybe ThreadLabel -> TraceValue
TraceValue { traceDynamic :: Maybe ()
traceDynamic = (Maybe ()
forall a. Maybe a
Nothing :: Maybe ()), traceString :: Maybe ThreadLabel
traceString = Maybe ThreadLabel
forall a. Maybe a
Nothing }
      Just Maybe a -> a -> ST s TraceValue
f  -> do
        [a]
vs <- STRef s [a] -> ST s [a]
forall s a. STRef s a -> ST s a
readSTRef STRef s [a]
tvarUndo
        a
v <-  STRef s a -> ST s a
forall s a. STRef s a -> ST s a
readSTRef STRef s a
tvarCurrent
        case (Bool
new, [a]
vs) of
          (Bool
True, [a]
_) -> Maybe a -> a -> ST s TraceValue
f Maybe a
forall a. Maybe a
Nothing a
v
          (Bool
_, a
_:[a]
_)  -> Maybe a -> a -> ST s TraceValue
f (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [a] -> a
forall a. [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 :: [SomeTVar s] -> ST s VectorClock
leastUpperBoundTVarVClocks [SomeTVar s]
tvars =
  (VectorClock -> VectorClock -> VectorClock)
-> VectorClock -> [VectorClock] -> VectorClock
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)
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 [ThreadId]
readTVarBlockedThreads :: TVar s a -> ST s [ThreadId]
readTVarBlockedThreads TVar{STRef s ([ThreadId], Set ThreadId)
tvarBlocked :: STRef s ([ThreadId], Set ThreadId)
tvarBlocked :: forall s a. TVar s a -> STRef s ([ThreadId], Set ThreadId)
tvarBlocked} = ([ThreadId], Set ThreadId) -> [ThreadId]
forall a b. (a, b) -> a
fst (([ThreadId], Set ThreadId) -> [ThreadId])
-> ST s ([ThreadId], Set ThreadId) -> ST s [ThreadId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef s ([ThreadId], Set ThreadId)
-> ST s ([ThreadId], Set ThreadId)
forall s a. STRef s a -> ST s a
readSTRef STRef s ([ThreadId], Set ThreadId)
tvarBlocked

blockThreadOnTVar :: ThreadId -> TVar s a -> ST s ()
blockThreadOnTVar :: ThreadId -> TVar s a -> ST s ()
blockThreadOnTVar ThreadId
tid TVar{STRef s ([ThreadId], Set ThreadId)
tvarBlocked :: STRef s ([ThreadId], Set ThreadId)
tvarBlocked :: forall s a. TVar s a -> STRef s ([ThreadId], Set ThreadId)
tvarBlocked} = do
    ([ThreadId]
tids, Set ThreadId
tidsSet) <- STRef s ([ThreadId], Set ThreadId)
-> ST s ([ThreadId], Set ThreadId)
forall s a. STRef s a -> ST s a
readSTRef STRef s ([ThreadId], Set ThreadId)
tvarBlocked
    Bool -> ST s () -> ST s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ThreadId
tid ThreadId -> Set ThreadId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set ThreadId
tidsSet) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ do
      let !tids' :: [ThreadId]
tids'    = ThreadId
tid ThreadId -> [ThreadId] -> [ThreadId]
forall a. a -> [a] -> [a]
: [ThreadId]
tids
          !tidsSet' :: Set ThreadId
tidsSet' = ThreadId -> Set ThreadId -> Set ThreadId
forall a. Ord a => a -> Set a -> Set a
Set.insert ThreadId
tid Set ThreadId
tidsSet
      STRef s ([ThreadId], Set ThreadId)
-> ([ThreadId], Set ThreadId) -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s ([ThreadId], Set ThreadId)
tvarBlocked ([ThreadId]
tids', Set ThreadId
tidsSet')

unblockAllThreadsFromTVar :: TVar s a -> ST s ()
unblockAllThreadsFromTVar :: TVar s a -> ST s ()
unblockAllThreadsFromTVar TVar{STRef s ([ThreadId], Set ThreadId)
tvarBlocked :: STRef s ([ThreadId], Set ThreadId)
tvarBlocked :: forall s a. TVar s a -> STRef s ([ThreadId], Set ThreadId)
tvarBlocked} = do
    STRef s ([ThreadId], Set ThreadId)
-> ([ThreadId], Set ThreadId) -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s ([ThreadId], Set ThreadId)
tvarBlocked ([], Set ThreadId
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 ([ThreadId], Map ThreadId (Set (Labelled TVarId)))
threadsUnblockedByWrites :: [SomeTVar s]
-> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId)))
threadsUnblockedByWrites [SomeTVar s]
written = do
  [(Labelled TVarId, [ThreadId])]
tidss <- [ST s (Labelled TVarId, [ThreadId])]
-> ST s [(Labelled TVarId, [ThreadId])]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
             [ (,) (Labelled TVarId -> [ThreadId] -> (Labelled TVarId, [ThreadId]))
-> ST s (Labelled TVarId)
-> ST s ([ThreadId] -> (Labelled TVarId, [ThreadId]))
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 ([ThreadId] -> (Labelled TVarId, [ThreadId]))
-> ST s [ThreadId] -> ST s (Labelled TVarId, [ThreadId])
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TVar s a -> ST s [ThreadId]
forall s a. TVar s a -> ST s [ThreadId]
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 :: [ThreadId]
wakeup = [ThreadId] -> [ThreadId]
forall a. Ord a => [a] -> [a]
ordNub [ ThreadId
tid | (Labelled TVarId
_vid, [ThreadId]
tids) <- [(Labelled TVarId, [ThreadId])]
tidss, ThreadId
tid <- [ThreadId] -> [ThreadId]
forall a. [a] -> [a]
reverse [ThreadId]
tids ]
      wokeby :: Map ThreadId (Set (Labelled TVarId))
wokeby = (Set (Labelled TVarId)
 -> Set (Labelled TVarId) -> Set (Labelled TVarId))
-> [(ThreadId, Set (Labelled TVarId))]
-> Map ThreadId (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
                                [ (ThreadId
tid, Labelled TVarId -> Set (Labelled TVarId)
forall a. a -> Set a
Set.singleton Labelled TVarId
vid)
                                | (Labelled TVarId
vid, [ThreadId]
tids) <- [(Labelled TVarId, [ThreadId])]
tidss
                                , ThreadId
tid <- [ThreadId]
tids ]
  ([ThreadId], Map ThreadId (Set (Labelled TVarId)))
-> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId)))
forall (m :: * -> *) a. Monad m => a -> m a
return ([ThreadId]
wakeup, Map ThreadId (Set (Labelled TVarId))
wokeby)

ordNub :: Ord a => [a] -> [a]
ordNub :: [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
--

data Step = Step {
    Step -> ThreadId
stepThreadId :: !ThreadId,
    Step -> Int
stepStep     :: !Int,
    Step -> Effect
stepEffect   :: !Effect,
    Step -> VectorClock
stepVClock   :: !VectorClock
  }
  deriving Int -> Step -> ShowS
[Step] -> ShowS
Step -> ThreadLabel
(Int -> Step -> ShowS)
-> (Step -> ThreadLabel) -> ([Step] -> ShowS) -> Show Step
forall a.
(Int -> a -> ShowS)
-> (a -> ThreadLabel) -> ([a] -> ShowS) -> Show a
showList :: [Step] -> ShowS
$cshowList :: [Step] -> ShowS
show :: Step -> ThreadLabel
$cshow :: Step -> ThreadLabel
showsPrec :: Int -> Step -> ShowS
$cshowsPrec :: Int -> Step -> ShowS
Show

-- steps race if they 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' =
     Step -> ThreadId
stepThreadId Step
s ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= Step -> ThreadId
stepThreadId Step
s'
  Bool -> Bool -> Bool
&& Bool -> Bool
not (Step -> ThreadId
stepThreadId Step
s' ThreadId -> [ThreadId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Effect -> [ThreadId]
effectWakeup (Step -> Effect
stepEffect Step
s))
  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 -> ThreadId
stepThreadId Step
s1 ThreadId -> [ThreadId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Effect -> [ThreadId]
effectThrows (Step -> Effect
stepEffect Step
s2)
          Bool -> Bool -> Bool
&& Step -> Effect
stepEffect Step
s1 Effect -> Effect -> Bool
forall a. Eq a => a -> a -> Bool
/= Effect
forall a. Monoid a => a
mempty

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

stepThread :: Thread s a -> Thread s a
stepThread :: Thread s a -> Thread s a
stepThread thread :: Thread s a
thread@Thread { threadId :: forall s a. Thread s a -> ThreadId
threadId     = ThreadId
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 :: Int
threadStep   = Int
tstepInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,
           threadEffect :: Effect
threadEffect = Effect
forall a. Monoid a => a
mempty,
           threadVClock :: VectorClock
threadVClock = ThreadId -> Int -> VectorClock -> VectorClock
insertVClock ThreadId
tid (Int
tstepInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) VectorClock
vClock
         }

-- As we run a simulation, we collect info about each previous step
data StepInfo = StepInfo {
    StepInfo -> Step
stepInfoStep       :: Step,
    -- Control information when we reached this step
    StepInfo -> ScheduleControl
stepInfoControl    :: ScheduleControl,
    -- threads that are still concurrent with this step
    StepInfo -> Set ThreadId
stepInfoConcurrent :: Set ThreadId,
    -- steps following this one that did not happen after it
    -- (in reverse order)
    StepInfo -> [Step]
stepInfoNonDep     :: [Step],
    -- later steps that race with this one
    StepInfo -> [Step]
stepInfoRaces      :: [Step]
  }
  deriving Int -> StepInfo -> ShowS
[StepInfo] -> ShowS
StepInfo -> ThreadLabel
(Int -> StepInfo -> ShowS)
-> (StepInfo -> ThreadLabel)
-> ([StepInfo] -> ShowS)
-> Show StepInfo
forall a.
(Int -> a -> ShowS)
-> (a -> ThreadLabel) -> ([a] -> ShowS) -> Show a
showList :: [StepInfo] -> ShowS
$cshowList :: [StepInfo] -> ShowS
show :: StepInfo -> ThreadLabel
$cshow :: StepInfo -> ThreadLabel
showsPrec :: Int -> StepInfo -> ShowS
$cshowsPrec :: Int -> StepInfo -> ShowS
Show

--
-- Races
--

data Races = Races { -- These steps may still race with future steps
                     Races -> [StepInfo]
activeRaces   :: ![StepInfo],
                     -- These steps cannot be concurrent with future steps
                     Races -> [StepInfo]
completeRaces :: ![StepInfo]
                   }
  deriving Int -> Races -> ShowS
[Races] -> ShowS
Races -> ThreadLabel
(Int -> Races -> ShowS)
-> (Races -> ThreadLabel) -> ([Races] -> ShowS) -> Show Races
forall a.
(Int -> a -> ShowS)
-> (a -> ThreadLabel) -> ([a] -> ShowS) -> Show a
showList :: [Races] -> ShowS
$cshowList :: [Races] -> ShowS
show :: Races -> ThreadLabel
$cshow :: Races -> ThreadLabel
showsPrec :: Int -> Races -> ShowS
$cshowsPrec :: Int -> Races -> ShowS
Show

noRaces :: Races
noRaces :: Races
noRaces = [StepInfo] -> [StepInfo] -> Races
Races [] []

updateRacesInSimState :: Thread s a -> SimState s a -> Races
updateRacesInSimState :: Thread s a -> SimState s a -> Races
updateRacesInSimState Thread s a
thread SimState{ ScheduleControl
control :: ScheduleControl
control :: forall s a. SimState s a -> ScheduleControl
control, Map ThreadId (Thread s a)
threads :: Map ThreadId (Thread s a)
threads :: forall s a. SimState s a -> Map ThreadId (Thread s a)
threads, Races
races :: Races
races :: forall s a. SimState s a -> Races
races } =
    Races -> Races
traceRaces (Races -> Races) -> Races -> Races
forall a b. (a -> b) -> a -> b
$
    Step -> Bool -> ScheduleControl -> Set ThreadId -> Races -> Races
updateRaces Step
step
                (Thread s a -> Bool
forall s a. Thread s a -> Bool
threadBlocked Thread s a
thread)
                ScheduleControl
control
                (Map ThreadId (Thread s a) -> Set ThreadId
forall k a. Map k a -> Set k
Map.keysSet ((Thread s a -> Bool)
-> Map ThreadId (Thread s a) -> Map ThreadId (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
threadDone Thread s a
t)
                                             Bool -> Bool -> Bool
&& Thread s a -> ThreadId
forall s a. Thread s a -> ThreadId
threadId Thread s a
t ThreadId -> Set ThreadId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember`
                                                Effect -> Set ThreadId
effectForks (Step -> Effect
stepEffect Step
step)
                                         ) Map ThreadId (Thread s a)
threads))
                Races
races
  where
    step :: Step
step = Thread s a -> Step
forall s a. Thread s a -> Step
currentStep 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 :: Step -> Bool -> ScheduleControl -> Set ThreadId -> Races -> Races
updateRaces :: Step -> Bool -> ScheduleControl -> Set ThreadId -> Races -> Races
updateRaces newStep :: Step
newStep@Step{ stepThreadId :: Step -> ThreadId
stepThreadId = ThreadId
tid, stepEffect :: Step -> Effect
stepEffect = Effect
newEffect }
            Bool
blocking
            ScheduleControl
control
            Set ThreadId
newConcurrent0
            races :: Races
races@Races{ [StepInfo]
activeRaces :: [StepInfo]
activeRaces :: Races -> [StepInfo]
activeRaces } =

  let justBlocking :: Bool
      justBlocking :: Bool
justBlocking = Bool
blocking Bool -> Bool -> Bool
&& Effect -> Bool
onlyReadEffect Effect
newEffect

      -- a new step cannot race with any threads that it just woke up
      new :: [StepInfo]
      !new :: [StepInfo]
new | ThreadId -> Bool
isNotRacyThreadId ThreadId
tid  = []  -- non-racy threads do not race
           | Set ThreadId -> Bool
forall a. Set a -> Bool
Set.null Set ThreadId
newConcurrent = []  -- cannot race with anything
           | Bool
justBlocking           = []  -- no need to defer a blocking transaction
           | Bool
otherwise              =
               [StepInfo :: Step
-> ScheduleControl -> Set ThreadId -> [Step] -> [Step] -> StepInfo
StepInfo { stepInfoStep :: Step
stepInfoStep       = Step
newStep,
                           stepInfoControl :: ScheduleControl
stepInfoControl    = ScheduleControl
control,
                           stepInfoConcurrent :: Set ThreadId
stepInfoConcurrent = Set ThreadId
newConcurrent,
                           stepInfoNonDep :: [Step]
stepInfoNonDep     = [],
                           stepInfoRaces :: [Step]
stepInfoRaces      = []
                         }]
        where
          newConcurrent :: Set ThreadId
          newConcurrent :: Set ThreadId
newConcurrent = (ThreadId -> Set ThreadId -> Set ThreadId)
-> Set ThreadId -> [ThreadId] -> Set ThreadId
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ThreadId -> Set ThreadId -> Set ThreadId
forall a. Ord a => a -> Set a -> Set a
Set.delete Set ThreadId
newConcurrent0 (Effect -> [ThreadId]
effectWakeup Effect
newEffect)

      activeRaces' :: [StepInfo]
      !activeRaces' :: [StepInfo]
activeRaces' =
        [ -- 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 ThreadId
lessConcurrent = (ThreadId -> Set ThreadId -> Set ThreadId)
-> Set ThreadId -> [ThreadId] -> Set ThreadId
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ThreadId -> Set ThreadId -> Set ThreadId
forall a. Ord a => a -> Set a -> Set a
Set.delete Set ThreadId
concurrent (Effect -> [ThreadId]
effectWakeup Effect
newEffect) in
          if ThreadId
tid ThreadId -> Set ThreadId -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set ThreadId
concurrent then
            let theseStepsRace :: Bool
theseStepsRace = ThreadId -> Bool
isRacyThreadId ThreadId
tid Bool -> Bool -> Bool
&& Step -> Step -> Bool
racingSteps Step
step Step
newStep
                happensBefore :: Bool
happensBefore  = Step
step Step -> Step -> Bool
`happensBeforeStep` Step
newStep
                !nondep' :: [Step]
nondep' | Bool
happensBefore = [Step]
nondep
                         | Bool
otherwise     = Step
newStep Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
: [Step]
nondep
                -- 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 ThreadId
concurrent' | Bool
happensBefore  = ThreadId -> Set ThreadId -> Set ThreadId
forall a. Ord a => a -> Set a -> Set a
Set.delete ThreadId
tid Set ThreadId
lessConcurrent
                            | Bool
theseStepsRace = ThreadId -> Set ThreadId -> Set ThreadId
forall a. Ord a => a -> Set a -> Set a
Set.delete ThreadId
tid Set ThreadId
concurrent
                            | Bool
otherwise      = Set ThreadId
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.
                !stepRaces' :: [Step]
stepRaces' | (ScheduleControl
control ScheduleControl -> ScheduleControl -> Bool
forall a. Eq a => a -> a -> Bool
== ScheduleControl
ControlDefault Bool -> Bool -> Bool
||
                               ScheduleControl
control ScheduleControl -> ScheduleControl -> Bool
forall a. Eq a => a -> a -> Bool
== [(ThreadId, Int)] -> [ScheduleMod] -> ScheduleControl
ControlFollow [] []) Bool -> Bool -> Bool
&&
                              Bool
theseStepsRace  = Step
newStep Step -> [Step] -> [Step]
forall a. a -> [a] -> [a]
: [Step]
stepRaces
                            | Bool
otherwise       = [Step]
stepRaces

            in StepInfo
stepInfo { stepInfoConcurrent :: Set ThreadId
stepInfoConcurrent = Effect -> Set ThreadId
effectForks Effect
newEffect
                                             Set ThreadId -> Set ThreadId -> Set ThreadId
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set ThreadId
concurrent',
                          stepInfoNonDep :: [Step]
stepInfoNonDep     = [Step]
nondep',
                          stepInfoRaces :: [Step]
stepInfoRaces      = [Step]
stepRaces'
                        }

          else StepInfo
stepInfo { stepInfoConcurrent :: Set ThreadId
stepInfoConcurrent = Set ThreadId
lessConcurrent }

        | !stepInfo :: StepInfo
stepInfo@StepInfo { stepInfoStep :: StepInfo -> Step
stepInfoStep       = Step
step,
                               stepInfoConcurrent :: StepInfo -> Set ThreadId
stepInfoConcurrent = Set ThreadId
concurrent,
                               stepInfoNonDep :: StepInfo -> [Step]
stepInfoNonDep     = [Step]
nondep,
                               stepInfoRaces :: StepInfo -> [Step]
stepInfoRaces      = [Step]
stepRaces
                            }
            <- [StepInfo]
activeRaces ]
  in Races -> Races
normalizeRaces (Races -> Races) -> Races -> Races
forall a b. (a -> b) -> a -> b
$ Races
races { activeRaces :: [StepInfo]
activeRaces = [StepInfo]
new [StepInfo] -> [StepInfo] -> [StepInfo]
forall a. [a] -> [a] -> [a]
++ [StepInfo]
activeRaces' }

-- When a thread terminates, we remove it from the concurrent thread
-- sets of active races.

threadTerminatesRaces :: ThreadId -> Races -> Races
threadTerminatesRaces :: ThreadId -> Races -> Races
threadTerminatesRaces ThreadId
tid races :: Races
races@Races{ [StepInfo]
activeRaces :: [StepInfo]
activeRaces :: Races -> [StepInfo]
activeRaces } =
  let activeRaces' :: [StepInfo]
activeRaces' = [ StepInfo
s{stepInfoConcurrent :: Set ThreadId
stepInfoConcurrent = ThreadId -> Set ThreadId -> Set ThreadId
forall a. Ord a => a -> Set a -> Set a
Set.delete ThreadId
tid Set ThreadId
stepInfoConcurrent}
                     | s :: StepInfo
s@StepInfo{ Set ThreadId
stepInfoConcurrent :: Set ThreadId
stepInfoConcurrent :: StepInfo -> Set ThreadId
stepInfoConcurrent } <- [StepInfo]
activeRaces ]
  in Races -> Races
normalizeRaces (Races -> Races) -> Races -> Races
forall a b. (a -> b) -> a -> b
$ Races
races{ activeRaces :: [StepInfo]
activeRaces = [StepInfo]
activeRaces' }

normalizeRaces :: Races -> Races
normalizeRaces :: Races -> Races
normalizeRaces Races{ [StepInfo]
activeRaces :: [StepInfo]
activeRaces :: Races -> [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 ThreadId -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null(Set ThreadId -> Bool)
-> (StepInfo -> Set ThreadId) -> StepInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StepInfo -> Set ThreadId
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 (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 -> Bool) -> [StepInfo] -> [StepInfo]
forall a. (a -> Bool) -> [a] -> [a]
filter (Set ThreadId -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Set ThreadId -> Bool)
-> (StepInfo -> Set ThreadId) -> StepInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StepInfo -> Set ThreadId
stepInfoConcurrent) [StepInfo]
activeRaces)
                     [StepInfo] -> [StepInfo] -> [StepInfo]
forall a. [a] -> [a] -> [a]
++ [StepInfo]
completeRaces
  in Races :: [StepInfo] -> [StepInfo] -> Races
Races{ activeRaces :: [StepInfo]
activeRaces = [StepInfo]
activeRaces', completeRaces :: [StepInfo]
completeRaces = [StepInfo]
completeRaces' }

-- 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 :: [StepInfo]
activeRaces :: Races -> [StepInfo]
activeRaces, [StepInfo]
completeRaces :: [StepInfo]
completeRaces :: Races -> [StepInfo]
completeRaces } =
  Races :: [StepInfo] -> [StepInfo] -> Races
Races{ activeRaces :: [StepInfo]
activeRaces = [],
         completeRaces :: [StepInfo]
completeRaces = [ StepInfo
s{stepInfoConcurrent :: Set ThreadId
stepInfoConcurrent = Set ThreadId
forall a. Set a
Set.empty}
                         | StepInfo
s <- [StepInfo]
activeRaces
                         , Bool -> Bool
not ([Step] -> 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 }

traceRaces :: Races -> Races
traceRaces :: Races -> Races
traceRaces Races
r = Races
r
-- traceRaces r@Races{activeRaces,completeRaces} =
--   Debug.trace ("Tracking "++show (length (concatMap stepInfoRaces activeRaces)) ++" races") r


--
-- Schedule control
--

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

followControl :: ScheduleControl -> ScheduleControl
followControl :: ScheduleControl -> ScheduleControl
followControl (ControlAwait (ScheduleMod { [(ThreadId, Int)]
scheduleModInsertion :: ScheduleMod -> [(ThreadId, Int)]
scheduleModInsertion :: [(ThreadId, Int)]
scheduleModInsertion } : [ScheduleMod]
mods)) =
               [(ThreadId, Int)] -> [ScheduleMod] -> ScheduleControl
ControlFollow [(ThreadId, Int)]
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 :: (ThreadId, Int) -> ScheduleControl -> Bool
controlFollows (ThreadId, Int)
_stepId  ScheduleControl
ControlDefault               = Bool
True
controlFollows (ThreadId, Int)
_stepId (ControlFollow [] [ScheduleMod]
_)          = Bool
True
controlFollows (ThreadId, Int)
stepId  (ControlFollow ((ThreadId, Int)
stepId':[(ThreadId, Int)]
_) [ScheduleMod]
_) = (ThreadId, Int)
stepId (ThreadId, Int) -> (ThreadId, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (ThreadId, Int)
stepId'
controlFollows (ThreadId, Int)
stepId  (ControlAwait (ScheduleMod
smod:[ScheduleMod]
_))       = (ThreadId, Int)
stepId (ThreadId, Int) -> (ThreadId, Int) -> Bool
forall a. Eq a => a -> a -> Bool
/= ScheduleMod -> (ThreadId, Int)
scheduleModTarget ScheduleMod
smod
controlFollows (ThreadId, Int)
_       (ControlAwait [])             = ThreadLabel -> Bool
forall a. (?callStack::CallStack) => ThreadLabel -> a
error ThreadLabel
"Impossible: controlFollows _ (ControlAwait [])"

advanceControl :: StepId -> ScheduleControl -> ScheduleControl
advanceControl :: (ThreadId, Int) -> ScheduleControl -> ScheduleControl
advanceControl (ThreadId
tid,Int
step) control :: ScheduleControl
control@(ControlFollow ((ThreadId
tid',Int
step'):[(ThreadId, Int)]
sids') [ScheduleMod]
tgts)
  | ThreadId
tid ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= ThreadId
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' =
      [(ThreadId, Int)] -> [ScheduleMod] -> ScheduleControl
ControlFollow [(ThreadId, Int)]
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 ", (ThreadId, Int) -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show (ThreadId
tid,Int
step)
            , ThreadLabel
" cannot follow step ", Int -> ThreadLabel
forall a. Show a => a -> ThreadLabel
show Int
step'
            , ThreadLabel
"\n"
            ]
advanceControl (ThreadId, Int)
stepId (ControlFollow [] []) =
  ScheduleControl
ControlDefault
advanceControl (ThreadId, Int)
stepId (ControlFollow [] [ScheduleMod]
tgts) =
  [ScheduleMod] -> ScheduleControl
ControlAwait [ScheduleMod]
tgts
advanceControl (ThreadId, Int)
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
$ (ThreadId, Int) -> ScheduleControl -> Bool
controlTargets (ThreadId, Int)
stepId ScheduleControl
control) (ScheduleControl -> ScheduleControl)
-> ScheduleControl -> ScheduleControl
forall a b. (a -> b) -> a -> b
$
  ScheduleControl
control

--
-- Schedule modifications
--

stepStepId :: Step -> (ThreadId, Int)
stepStepId :: Step -> (ThreadId, Int)
stepStepId Step{ stepThreadId :: Step -> ThreadId
stepThreadId = ThreadId
tid, stepStep :: Step -> Int
stepStep = Int
n } = (ThreadId
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 :: (ThreadId, Int)
-> ScheduleControl -> [(ThreadId, Int)] -> ScheduleMod
ScheduleMod
      { scheduleModTarget :: (ThreadId, Int)
scheduleModTarget    = Step -> (ThreadId, Int)
stepStepId Step
step
      , scheduleModControl :: ScheduleControl
scheduleModControl   = ScheduleControl
control
      , scheduleModInsertion :: [(ThreadId, Int)]
scheduleModInsertion = ((ThreadId, Int) -> Bool) -> [(ThreadId, Int)] -> [(ThreadId, Int)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((ThreadId, Int) -> (ThreadId, Int) -> Bool
forall a. Eq a => a -> a -> Bool
/=Step -> (ThreadId, Int)
stepStepId Step
step')
                                         ((Step -> (ThreadId, Int)) -> [Step] -> [(ThreadId, Int)]
forall a b. (a -> b) -> [a] -> [b]
map Step -> (ThreadId, Int)
stepStepId ([Step] -> [Step]
forall a. [a] -> [a]
reverse [Step]
nondep))
                            [(ThreadId, Int)] -> [(ThreadId, Int)] -> [(ThreadId, Int)]
forall a. [a] -> [a] -> [a]
++ [Step -> (ThreadId, Int)
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 :: SimState s a -> SimTrace a -> SimTrace a
traceFinalRacesFound SimState{ control0 :: forall s a. SimState s a -> ScheduleControl
control0 = ScheduleControl
control, Races
races :: Races
races :: forall s a. SimState s a -> 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 (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleMod]
mods Int -> Int -> Int
forall a. Num a => a -> a -> a
- [ScheduleMod] -> 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 :: ScheduleControl
scheduleModControl = ScheduleControl
ControlDefault }])
    ControlFollow [(ThreadId, Int)]
stepIds [ScheduleMod]
mods' ->
      let common :: Int
common = [ScheduleMod] -> 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 (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. [a] -> Int -> a
!! Int
common
          isUndo :: Bool
isUndo = ScheduleMod -> (ThreadId, Int)
scheduleModTarget ScheduleMod
m' (ThreadId, Int) -> [(ThreadId, Int)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ScheduleMod -> [(ThreadId, Int)]
scheduleModInsertion ScheduleMod
m
          m'' :: ScheduleMod
m''    = ScheduleMod
m'{ scheduleModInsertion :: [(ThreadId, Int)]
scheduleModInsertion =
                         ((ThreadId, Int) -> Bool) -> [(ThreadId, Int)] -> [(ThreadId, Int)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((ThreadId, Int) -> (ThreadId, Int) -> Bool
forall a. Eq a => a -> a -> Bool
/=ScheduleMod -> (ThreadId, Int)
scheduleModTarget ScheduleMod
m)
                                   (ScheduleMod -> [(ThreadId, Int)]
scheduleModInsertion ScheduleMod
m')
                         [(ThreadId, Int)] -> [(ThreadId, Int)] -> [(ThreadId, Int)]
forall a. [a] -> [a] -> [a]
++
                         ScheduleMod -> [(ThreadId, Int)]
scheduleModInsertion ScheduleMod
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'