    module GHC.RTS.Events.Analysis.Capability
      ( capabilityThreadPoolMachine
      , capabilityThreadRunMachine
      , capabilityThreadIndexer
      , capabilityTaskPoolMachine
      , capabilityTaskOSMachine
      )
     where

    import GHC.RTS.Events
    import GHC.RTS.Events.Analysis

    import Data.Map (Map)
    import qualified Data.Map as M

    -- | This state machine tracks threads residing on capabilities.
    -- Each thread can only reside on one capability, but can be migrated between
    -- them.
    capabilityThreadPoolMachine :: Machine (Map ThreadId Int) Event
    capabilityThreadPoolMachine :: Machine (Map ThreadId Int) Event
    capabilityThreadPoolMachine = Machine
      { initial :: Map ThreadId Int
    initial = Map ThreadId Int
    forall k a. Map k a
    M.empty
      , final :: Map ThreadId Int -> Bool
    final   = Bool -> Map ThreadId Int -> Bool
    forall a b. a -> b -> a
    const Bool
    False
      , alpha :: Event -> Bool
    alpha   = Event -> Bool
    capabilityThreadPoolMachineAlpha
      , delta :: Map ThreadId Int -> Event -> Maybe (Map ThreadId Int)
    delta   = Map ThreadId Int -> Event -> Maybe (Map ThreadId Int)
    capabilityThreadPoolMachineDelta
      }
     where
      capabilityThreadPoolMachineAlpha :: Event -> Bool
    capabilityThreadPoolMachineAlpha Event
    evt = case Event -> EventInfo
    evSpec Event
    evt of
         (CreateThread ThreadId
    _)    -> Bool
    True
         (StopThread ThreadId
    _ ThreadStopStatus
    _)    -> Bool
    True
         (MigrateThread ThreadId
    _ Int
    _) -> Bool
    True
         EventInfo
    _                   -> Bool
    False

      capabilityThreadPoolMachineDelta :: Map ThreadId Int -> Event -> Maybe (Map ThreadId Int)
    capabilityThreadPoolMachineDelta Map ThreadId Int
    mapping Event
    evt = do
        capId <- Event -> Maybe Int
    evCap Event
    evt
        case evSpec evt of
          (CreateThread ThreadId
    threadId)              -> ThreadId -> Int -> Map ThreadId Int -> Maybe (Map ThreadId Int)
    insertThread ThreadId
    threadId Int
    capId Map ThreadId Int
    mapping
          (StopThread ThreadId
    threadId ThreadStopStatus
    ThreadFinished) -> ThreadId -> Map ThreadId Int -> Maybe (Map ThreadId Int)
    deleteThread ThreadId
    threadId Map ThreadId Int
    mapping
          (StopThread ThreadId
    _ ThreadStopStatus
    _)                     -> Map ThreadId Int -> Maybe (Map ThreadId Int)
    forall a. a -> Maybe a
    Just Map ThreadId Int
    mapping
          (MigrateThread ThreadId
    threadId Int
    capId')      -> ThreadId -> Map ThreadId Int -> Maybe (Map ThreadId Int)
    deleteThread ThreadId
    threadId Map ThreadId Int
    mapping Maybe (Map ThreadId Int)
    -> (Map ThreadId Int -> Maybe (Map ThreadId Int))
    -> Maybe (Map ThreadId Int)
    forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>=
                                                    ThreadId -> Int -> Map ThreadId Int -> Maybe (Map ThreadId Int)
    insertThread ThreadId
    threadId Int
    capId'
          EventInfo
    _                                    -> Maybe (Map ThreadId Int)
    forall a. Maybe a
    Nothing
       where
        insertThread :: ThreadId -> Int -> Map ThreadId Int -> Maybe (Map ThreadId Int)
        insertThread :: ThreadId -> Int -> Map ThreadId Int -> Maybe (Map ThreadId Int)
    insertThread ThreadId
    threadId Int
    capId Map ThreadId Int
    m
          | ThreadId
    threadId ThreadId -> Map ThreadId Int -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `M.member` Map ThreadId Int
    m = Maybe (Map ThreadId Int)
    forall a. Maybe a
    Nothing -- The thread already exists
          | Bool
    otherwise             = Map ThreadId Int -> Maybe (Map ThreadId Int)
    forall a. a -> Maybe a
    Just (Map ThreadId Int -> Maybe (Map ThreadId Int))
    -> Map ThreadId Int -> Maybe (Map ThreadId Int)
    forall a b. (a -> b) -> a -> b
    $ ThreadId -> Int -> Map ThreadId Int -> Map ThreadId Int
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert ThreadId
    threadId Int
    capId Map ThreadId Int
    m

        deleteThread :: ThreadId -> Map ThreadId Int -> Maybe (Map ThreadId Int)
        deleteThread :: ThreadId -> Map ThreadId Int -> Maybe (Map ThreadId Int)
    deleteThread ThreadId
    threadId Map ThreadId Int
    m
          | ThreadId
    threadId ThreadId -> Map ThreadId Int -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `M.notMember` Map ThreadId Int
    m = Maybe (Map ThreadId Int)
    forall a. Maybe a
    Nothing -- The thread doesn't exist
          | Bool
    otherwise                = Map ThreadId Int -> Maybe (Map ThreadId Int)
    forall a. a -> Maybe a
    Just (Map ThreadId Int -> Maybe (Map ThreadId Int))
    -> Map ThreadId Int -> Maybe (Map ThreadId Int)
    forall a b. (a -> b) -> a -> b
    $ ThreadId -> Map ThreadId Int -> Map ThreadId Int
    forall k a. Ord k => k -> Map k a -> Map k a
    M.delete ThreadId
    threadId Map ThreadId Int
    m

    -- | This state machine tracks threads running on capabilities, only one thread
    -- may run on a capability at a time.
    capabilityThreadRunMachine :: Machine (Map Int ThreadId) Event
    capabilityThreadRunMachine :: Machine (Map Int ThreadId) Event
    capabilityThreadRunMachine = Machine
      { initial :: Map Int ThreadId
    initial = Map Int ThreadId
    forall k a. Map k a
    M.empty
      , final :: Map Int ThreadId -> Bool
    final   = Bool -> Map Int ThreadId -> Bool
    forall a b. a -> b -> a
    const Bool
    False
      , alpha :: Event -> Bool
    alpha   = Event -> Bool
    threadRunAlpha
      , delta :: Map Int ThreadId -> Event -> Maybe (Map Int ThreadId)
    delta   = Map Int ThreadId -> Event -> Maybe (Map Int ThreadId)
    threadRunDelta
      }
     where
      threadRunAlpha :: Event -> Bool
    threadRunAlpha Event
    event = case Event -> EventInfo
    evSpec Event
    event of
        -- TODO: can threads be migrated while they are running?
        -- TODO: take into account paused threads
        (RunThread ThreadId
    _)     -> Bool
    True
        (StopThread ThreadId
    _ ThreadStopStatus
    _ ) -> Bool
    True
        EventInfo
    _                 -> Bool
    False

      -- The indexer fails if a thread is inserted where one already exists,
      -- or if a thread is deleted that doesn't exist.
      threadRunDelta :: Map Int ThreadId -> Event -> Maybe (Map Int ThreadId)
    threadRunDelta Map Int ThreadId
    mapping Event
    e = do
        capId <- Event -> Maybe Int
    evCap Event
    e
        case evSpec $ e of
          (RunThread ThreadId
    threadId)     -> Int -> ThreadId -> Map Int ThreadId -> Maybe (Map Int ThreadId)
    runThread Int
    capId ThreadId
    threadId Map Int ThreadId
    mapping
          (StopThread ThreadId
    threadId ThreadStopStatus
    _ ) -> ThreadId -> Map Int ThreadId -> Maybe (Map Int ThreadId)
    stopThread ThreadId
    threadId Map Int ThreadId
    mapping
          EventInfo
    _                        -> Map Int ThreadId -> Maybe (Map Int ThreadId)
    forall a. a -> Maybe a
    Just Map Int ThreadId
    mapping
       where
        runThread :: Int -> ThreadId -> Map Int ThreadId -> Maybe (Map Int ThreadId)
        runThread :: Int -> ThreadId -> Map Int ThreadId -> Maybe (Map Int ThreadId)
    runThread Int
    capId ThreadId
    threadId Map Int ThreadId
    m
          | Int
    capId Int -> Map Int ThreadId -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `M.member` Map Int ThreadId
    m        = Maybe (Map Int ThreadId)
    forall a. Maybe a
    Nothing -- A thread is already on this cap
          | ThreadId
    threadId ThreadId -> [ThreadId] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` Map Int ThreadId -> [ThreadId]
    forall k a. Map k a -> [a]
    M.elems Map Int ThreadId
    m = Maybe (Map Int ThreadId)
    forall a. Maybe a
    Nothing -- This thread is already on a cap
          | Bool
    otherwise                 = Map Int ThreadId -> Maybe (Map Int ThreadId)
    forall a. a -> Maybe a
    Just (Map Int ThreadId -> Maybe (Map Int ThreadId))
    -> Map Int ThreadId -> Maybe (Map Int ThreadId)
    forall a b. (a -> b) -> a -> b
    $ Int -> ThreadId -> Map Int ThreadId -> Map Int ThreadId
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert Int
    capId ThreadId
    threadId Map Int ThreadId
    m
        stopThread :: ThreadId -> Map Int ThreadId -> Maybe (Map Int ThreadId)
        stopThread :: ThreadId -> Map Int ThreadId -> Maybe (Map Int ThreadId)
    stopThread ThreadId
    threadId Map Int ThreadId
    m
          | ThreadId -> [ThreadId] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    notElem ThreadId
    threadId ([ThreadId] -> Bool)
    -> (Map Int ThreadId -> [ThreadId]) -> Map Int ThreadId -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map Int ThreadId -> [ThreadId]
    forall k a. Map k a -> [a]
    M.elems (Map Int ThreadId -> Bool) -> Map Int ThreadId -> Bool
    forall a b. (a -> b) -> a -> b
    $ Map Int ThreadId
    m = Maybe (Map Int ThreadId)
    forall a. Maybe a
    Nothing -- The thread doesn't exist
          | Bool
    otherwise                      = Map Int ThreadId -> Maybe (Map Int ThreadId)
    forall a. a -> Maybe a
    Just (Map Int ThreadId -> Maybe (Map Int ThreadId))
    -> Map Int ThreadId -> Maybe (Map Int ThreadId)
    forall a b. (a -> b) -> a -> b
    $ (ThreadId -> Bool) -> Map Int ThreadId -> Map Int ThreadId
    forall a k. (a -> Bool) -> Map k a -> Map k a
    M.filter (ThreadId -> ThreadId -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ThreadId
    threadId) Map Int ThreadId
    m

    capabilityThreadIndexer :: Map Int ThreadId -> Event -> Maybe ThreadId
    capabilityThreadIndexer :: Map Int ThreadId -> Event -> Maybe ThreadId
    capabilityThreadIndexer Map Int ThreadId
    m Event
    evt = case Event -> EventInfo
    evSpec Event
    evt of
      (CreateSparkThread ThreadId
    threadId)  -> ThreadId -> Maybe ThreadId
    forall a. a -> Maybe a
    Just ThreadId
    threadId
      (CreateThread ThreadId
    threadId)       -> ThreadId -> Maybe ThreadId
    forall a. a -> Maybe a
    Just ThreadId
    threadId
      (RunThread ThreadId
    threadId)          -> ThreadId -> Maybe ThreadId
    forall a. a -> Maybe a
    Just ThreadId
    threadId
      (StopThread ThreadId
    threadId ThreadStopStatus
    _)       -> ThreadId -> Maybe ThreadId
    forall a. a -> Maybe a
    Just ThreadId
    threadId
      (ThreadRunnable ThreadId
    threadId)     -> ThreadId -> Maybe ThreadId
    forall a. a -> Maybe a
    Just ThreadId
    threadId
      (MigrateThread ThreadId
    threadId Int
    _)    -> ThreadId -> Maybe ThreadId
    forall a. a -> Maybe a
    Just ThreadId
    threadId
      (WakeupThread ThreadId
    threadId Int
    capId) -> if Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    capId Maybe Int -> Maybe Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Event -> Maybe Int
    evCap Event
    evt
                                       then ThreadId -> Maybe ThreadId
    forall a. a -> Maybe a
    Just ThreadId
    threadId
                                       else Maybe ThreadId
    forall a. Maybe a
    Nothing
      EventInfo
    _                             -> Maybe ThreadId
    mThreadId
     where
      mThreadId :: Maybe ThreadId
    mThreadId = Event -> Maybe Int
    evCap Event
    evt Maybe Int -> (Int -> Maybe ThreadId) -> Maybe ThreadId
    forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (\Int
    capId -> Int -> Map Int ThreadId -> Maybe ThreadId
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Int
    capId Map Int ThreadId
    m)

    -- | This state machine tracks Haskell tasks, represented by TaskId,
    -- residing on capabilities.
    -- Each Haskell task can only reside on one capability, but can be migrated
    -- between them.
    capabilityTaskPoolMachine :: Machine (Map TaskId Int) Event
    capabilityTaskPoolMachine :: Machine (Map TaskId Int) Event
    capabilityTaskPoolMachine = Machine
      { initial :: Map TaskId Int
    initial = Map TaskId Int
    forall k a. Map k a
    M.empty
      , final :: Map TaskId Int -> Bool
    final   = Bool -> Map TaskId Int -> Bool
    forall a b. a -> b -> a
    const Bool
    False
      , alpha :: Event -> Bool
    alpha   = Event -> Bool
    capabilityTaskPoolMachineAlpha
      , delta :: Map TaskId Int -> Event -> Maybe (Map TaskId Int)
    delta   = Map TaskId Int -> Event -> Maybe (Map TaskId Int)
    capabilityTaskPoolMachineDelta
      }
     where
      capabilityTaskPoolMachineAlpha :: Event -> Bool
    capabilityTaskPoolMachineAlpha Event
    evt = case Event -> EventInfo
    evSpec Event
    evt of
         TaskCreate{}  -> Bool
    True
         TaskDelete{}  -> Bool
    True
         TaskMigrate{} -> Bool
    True
         EventInfo
    _             -> Bool
    False

      capabilityTaskPoolMachineDelta :: Map TaskId Int -> Event -> Maybe (Map TaskId Int)
    capabilityTaskPoolMachineDelta Map TaskId Int
    mapping Event
    evt = do
        case Event -> EventInfo
    evSpec Event
    evt of
          TaskCreate {TaskId
    taskId :: TaskId
    taskId :: EventInfo -> TaskId
    taskId, Int
    cap :: Int
    cap :: EventInfo -> Int
    cap}           -> TaskId -> Int -> Map TaskId Int -> Maybe (Map TaskId Int)
    insertTask TaskId
    taskId Int
    cap Map TaskId Int
    mapping
          TaskDelete {TaskId
    taskId :: EventInfo -> TaskId
    taskId :: TaskId
    taskId}                -> TaskId -> Maybe Int -> Map TaskId Int -> Maybe (Map TaskId Int)
    deleteTask TaskId
    taskId Maybe Int
    forall a. Maybe a
    Nothing Map TaskId Int
    mapping
          TaskMigrate {TaskId
    taskId :: EventInfo -> TaskId
    taskId :: TaskId
    taskId, Int
    cap :: EventInfo -> Int
    cap :: Int
    cap, Int
    new_cap :: Int
    new_cap :: EventInfo -> Int
    new_cap} ->
            TaskId -> Maybe Int -> Map TaskId Int -> Maybe (Map TaskId Int)
    deleteTask TaskId
    taskId (Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    cap) Map TaskId Int
    mapping Maybe (Map TaskId Int)
    -> (Map TaskId Int -> Maybe (Map TaskId Int))
    -> Maybe (Map TaskId Int)
    forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>=
              TaskId -> Int -> Map TaskId Int -> Maybe (Map TaskId Int)
    insertTask TaskId
    taskId Int
    new_cap
          EventInfo
    _                                  -> Maybe (Map TaskId Int)
    forall a. Maybe a
    Nothing
       where
        insertTask :: TaskId -> Int -> Map TaskId Int
                   -> Maybe (Map TaskId Int)
        insertTask :: TaskId -> Int -> Map TaskId Int -> Maybe (Map TaskId Int)
    insertTask TaskId
    taskId Int
    cap Map TaskId Int
    m
          | TaskId
    taskId TaskId -> Map TaskId Int -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `M.member` Map TaskId Int
    m = Maybe (Map TaskId Int)
    forall a. Maybe a
    Nothing  -- The task already exists.
          | Bool
    otherwise           = Map TaskId Int -> Maybe (Map TaskId Int)
    forall a. a -> Maybe a
    Just (Map TaskId Int -> Maybe (Map TaskId Int))
    -> Map TaskId Int -> Maybe (Map TaskId Int)
    forall a b. (a -> b) -> a -> b
    $ TaskId -> Int -> Map TaskId Int -> Map TaskId Int
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert TaskId
    taskId Int
    cap Map TaskId Int
    m

        deleteTask :: TaskId -> Maybe Int -> Map TaskId Int
                   -> Maybe (Map TaskId Int)
        deleteTask :: TaskId -> Maybe Int -> Map TaskId Int -> Maybe (Map TaskId Int)
    deleteTask TaskId
    taskId Maybe Int
    expectedcap Map TaskId Int
    m
          | Just Int
    oldcap <- TaskId -> Map TaskId Int -> Maybe Int
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup TaskId
    taskId Map TaskId Int
    m
          , Bool -> (Int -> Bool) -> Maybe Int -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True (Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    ==Int
    oldcap) Maybe Int
    expectedcap
          = Map TaskId Int -> Maybe (Map TaskId Int)
    forall a. a -> Maybe a
    Just (Map TaskId Int -> Maybe (Map TaskId Int))
    -> Map TaskId Int -> Maybe (Map TaskId Int)
    forall a b. (a -> b) -> a -> b
    $ TaskId -> Map TaskId Int -> Map TaskId Int
    forall k a. Ord k => k -> Map k a -> Map k a
    M.delete TaskId
    taskId Map TaskId Int
    m
          | Bool
    otherwise
          = Maybe (Map TaskId Int)
    forall a. Maybe a
    Nothing  -- The task doesn't exist, or does but with an unexpected cap.

    -- | This state machine tracks Haskell tasks (represented by the KernelThreadId
    -- of their OS thread) residing on capabilities and additionally
    -- tracks the (immutable) assignment of OS thread ids (KernelThreadId)
    -- to tasks ids (TaskId).
    -- Each Haskell task can only reside on one capability, but can be migrated
    -- between them.
    --
    -- Invariant for the @(Map KernelThreadId Int, Map TaskId KernelThreadId)@
    -- type: the second map is an injection (verified by the machine
    -- in 'insertTaskOS') and the following sets are equal:
    -- keys of the fist map and values of the second
    -- (follows from the construction of the maps by the machine).
    --
    -- The machine verifies as much as 'capabilityTaskPoolMachine' and additionally
    -- the data invariant, and offers a richer verification profile.
    capabilityTaskOSMachine :: Machine (Map KernelThreadId Int,
                                        Map TaskId KernelThreadId)
                                       Event
    capabilityTaskOSMachine :: Machine (Map KernelThreadId Int, Map TaskId KernelThreadId) Event
    capabilityTaskOSMachine = Machine
      { initial :: (Map KernelThreadId Int, Map TaskId KernelThreadId)
    initial = (Map KernelThreadId Int
    forall k a. Map k a
    M.empty, Map TaskId KernelThreadId
    forall k a. Map k a
    M.empty)
      , final :: (Map KernelThreadId Int, Map TaskId KernelThreadId) -> Bool
    final   = Bool -> (Map KernelThreadId Int, Map TaskId KernelThreadId) -> Bool
    forall a b. a -> b -> a
    const Bool
    False
      , alpha :: Event -> Bool
    alpha   = Event -> Bool
    capabilityTaskOSMachineAlpha
      , delta :: (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Event
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    delta   = (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Event
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    capabilityTaskOSMachineDelta
      }
     where
      capabilityTaskOSMachineAlpha :: Event -> Bool
    capabilityTaskOSMachineAlpha Event
    evt = case Event -> EventInfo
    evSpec Event
    evt of
         TaskCreate{}  -> Bool
    True
         TaskDelete{}  -> Bool
    True
         TaskMigrate{} -> Bool
    True
         EventInfo
    _             -> Bool
    False

      capabilityTaskOSMachineDelta :: (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Event
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    capabilityTaskOSMachineDelta (Map KernelThreadId Int, Map TaskId KernelThreadId)
    mapping Event
    evt = do
        case Event -> EventInfo
    evSpec Event
    evt of
          TaskCreate {TaskId
    taskId :: EventInfo -> TaskId
    taskId :: TaskId
    taskId, Int
    cap :: EventInfo -> Int
    cap :: Int
    cap, KernelThreadId
    tid :: KernelThreadId
    tid :: EventInfo -> KernelThreadId
    tid} -> TaskId
    -> Int
    -> KernelThreadId
    -> (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    insertTaskOS TaskId
    taskId Int
    cap KernelThreadId
    tid (Map KernelThreadId Int, Map TaskId KernelThreadId)
    mapping
          TaskDelete {TaskId
    taskId :: EventInfo -> TaskId
    taskId :: TaskId
    taskId}           -> TaskId
    -> (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    deleteTaskOS TaskId
    taskId (Map KernelThreadId Int, Map TaskId KernelThreadId)
    mapping
          TaskMigrate {TaskId
    taskId :: EventInfo -> TaskId
    taskId :: TaskId
    taskId, Int
    new_cap :: EventInfo -> Int
    new_cap :: Int
    new_cap} -> TaskId
    -> Int
    -> (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    migrateTaskOS TaskId
    taskId Int
    new_cap (Map KernelThreadId Int, Map TaskId KernelThreadId)
    mapping
          EventInfo
    _                             -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    forall a. Maybe a
    Nothing
       where
        insertTaskOS :: TaskId -> Int -> KernelThreadId
                     -> (Map KernelThreadId Int, Map TaskId KernelThreadId)
                     -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
        insertTaskOS :: TaskId
    -> Int
    -> KernelThreadId
    -> (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    insertTaskOS TaskId
    taskId Int
    cap KernelThreadId
    tid (Map KernelThreadId Int
    m, Map TaskId KernelThreadId
    ma)
          | TaskId
    taskId TaskId -> Map TaskId KernelThreadId -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `M.member` Map TaskId KernelThreadId
    ma = Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    forall a. Maybe a
    Nothing  -- The task already exists.
          | KernelThreadId
    tid KernelThreadId -> Map KernelThreadId Int -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `M.member` Map KernelThreadId Int
    m     = Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    forall a. Maybe a
    Nothing  -- The OS thread already exists.
          | Bool
    otherwise            = (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    forall a. a -> Maybe a
    Just (KernelThreadId
    -> Int -> Map KernelThreadId Int -> Map KernelThreadId Int
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert KernelThreadId
    tid Int
    cap Map KernelThreadId Int
    m,
                                         TaskId
    -> KernelThreadId
    -> Map TaskId KernelThreadId
    -> Map TaskId KernelThreadId
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert TaskId
    taskId KernelThreadId
    tid Map TaskId KernelThreadId
    ma)

        deleteTaskOS :: TaskId -> (Map KernelThreadId Int,
                                   Map TaskId KernelThreadId)
                     -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
        deleteTaskOS :: TaskId
    -> (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    deleteTaskOS TaskId
    taskId (Map KernelThreadId Int
    m, Map TaskId KernelThreadId
    ma) =
          case TaskId -> Map TaskId KernelThreadId -> Maybe KernelThreadId
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup TaskId
    taskId Map TaskId KernelThreadId
    ma of
            Maybe KernelThreadId
    Nothing  -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    forall a. Maybe a
    Nothing  -- The task doesn't exist.
            Just KernelThreadId
    tid -> (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    forall a. a -> Maybe a
    Just (KernelThreadId -> Map KernelThreadId Int -> Map KernelThreadId Int
    forall k a. Ord k => k -> Map k a -> Map k a
    M.delete KernelThreadId
    tid Map KernelThreadId Int
    m,
                              TaskId -> Map TaskId KernelThreadId -> Map TaskId KernelThreadId
    forall k a. Ord k => k -> Map k a -> Map k a
    M.delete TaskId
    taskId Map TaskId KernelThreadId
    ma)

        migrateTaskOS :: TaskId -> Int -> (Map KernelThreadId Int,
                                           Map TaskId KernelThreadId)
                      -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
        migrateTaskOS :: TaskId
    -> Int
    -> (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    migrateTaskOS TaskId
    taskId Int
    new_cap (Map KernelThreadId Int
    m, Map TaskId KernelThreadId
    ma) =
          case TaskId -> Map TaskId KernelThreadId -> Maybe KernelThreadId
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup TaskId
    taskId Map TaskId KernelThreadId
    ma of
            Maybe KernelThreadId
    Nothing -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    forall a. Maybe a
    Nothing  -- The task doesn't exist.
            Just KernelThreadId
    tid -> (Map KernelThreadId Int, Map TaskId KernelThreadId)
    -> Maybe (Map KernelThreadId Int, Map TaskId KernelThreadId)
    forall a. a -> Maybe a
    Just (KernelThreadId
    -> Int -> Map KernelThreadId Int -> Map KernelThreadId Int
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert KernelThreadId
    tid Int
    new_cap Map KernelThreadId Int
    m,
                              Map TaskId KernelThreadId
    ma)  -- The assignment is immutable.