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 = forall k a. Map k a
M.empty
  , final :: Map ThreadId Int -> Bool
final   = 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
    Int
capId <- Event -> Maybe Int
evCap Event
evt
    case Event -> EventInfo
evSpec Event
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
_)                     -> 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 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
_                                    -> 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 forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map ThreadId Int
m = forall a. Maybe a
Nothing -- The thread already exists
      | Bool
otherwise             = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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 forall k a. Ord k => k -> Map k a -> Bool
`M.notMember` Map ThreadId Int
m = forall a. Maybe a
Nothing -- The thread doesn't exist
      | Bool
otherwise                = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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 = forall k a. Map k a
M.empty
  , final :: Map Int ThreadId -> Bool
final   = 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
    Int
capId <- Event -> Maybe Int
evCap Event
e
    case Event -> EventInfo
evSpec forall a b. (a -> b) -> a -> b
$ Event
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
_                        -> 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 forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map Int ThreadId
m        = forall a. Maybe a
Nothing -- A thread is already on this cap
      | ThreadId
threadId forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall k a. Map k a -> [a]
M.elems Map Int ThreadId
m = forall a. Maybe a
Nothing -- This thread is already on a cap
      | Bool
otherwise                 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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
      | forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem ThreadId
threadId forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems forall a b. (a -> b) -> a -> b
$ Map Int ThreadId
m = forall a. Maybe a
Nothing -- The thread doesn't exist
      | Bool
otherwise                      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (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)  -> forall a. a -> Maybe a
Just ThreadId
threadId
  (CreateThread ThreadId
threadId)       -> forall a. a -> Maybe a
Just ThreadId
threadId
  (RunThread ThreadId
threadId)          -> forall a. a -> Maybe a
Just ThreadId
threadId
  (StopThread ThreadId
threadId ThreadStopStatus
_)       -> forall a. a -> Maybe a
Just ThreadId
threadId
  (ThreadRunnable ThreadId
threadId)     -> forall a. a -> Maybe a
Just ThreadId
threadId
  (MigrateThread ThreadId
threadId Int
_)    -> forall a. a -> Maybe a
Just ThreadId
threadId
  (WakeupThread ThreadId
threadId Int
capId) -> if forall a. a -> Maybe a
Just Int
capId forall a. Eq a => a -> a -> Bool
== Event -> Maybe Int
evCap Event
evt
                                   then forall a. a -> Maybe a
Just ThreadId
threadId
                                   else forall a. Maybe a
Nothing
  EventInfo
_                             -> Maybe ThreadId
mThreadId
 where
  mThreadId :: Maybe ThreadId
mThreadId = Event -> Maybe Int
evCap Event
evt forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Int
capId -> 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 = forall k a. Map k a
M.empty
  , final :: Map TaskId Int -> Bool
final   = 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 :: EventInfo -> TaskId
taskId :: TaskId
taskId, Int
cap :: EventInfo -> Int
cap :: Int
cap}           -> TaskId -> Int -> Map TaskId Int -> Maybe (Map TaskId Int)
insertTask TaskId
taskId Int
cap Map TaskId Int
mapping
      TaskDelete {TaskId
taskId :: TaskId
taskId :: EventInfo -> TaskId
taskId}                -> TaskId -> Maybe Int -> Map TaskId Int -> Maybe (Map TaskId Int)
deleteTask TaskId
taskId forall a. Maybe a
Nothing Map TaskId Int
mapping
      TaskMigrate {TaskId
taskId :: TaskId
taskId :: EventInfo -> TaskId
taskId, Int
cap :: Int
cap :: EventInfo -> Int
cap, Int
new_cap :: EventInfo -> Int
new_cap :: Int
new_cap} ->
        TaskId -> Maybe Int -> Map TaskId Int -> Maybe (Map TaskId Int)
deleteTask TaskId
taskId (forall a. a -> Maybe a
Just Int
cap) Map TaskId Int
mapping 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
_                                  -> 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 forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map TaskId Int
m = forall a. Maybe a
Nothing  -- The task already exists.
      | Bool
otherwise           = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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 <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup TaskId
taskId Map TaskId Int
m
      , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (forall a. Eq a => a -> a -> Bool
==Int
oldcap) Maybe Int
expectedcap
      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Map k a
M.delete TaskId
taskId Map TaskId Int
m
      | Bool
otherwise
      = 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 = (forall k a. Map k a
M.empty, forall k a. Map k a
M.empty)
  , final :: (Map KernelThreadId Int, Map TaskId KernelThreadId) -> Bool
final   = 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 :: TaskId
taskId :: EventInfo -> TaskId
taskId, Int
cap :: Int
cap :: EventInfo -> Int
cap, KernelThreadId
tid :: EventInfo -> KernelThreadId
tid :: 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 :: TaskId
taskId :: EventInfo -> 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 :: TaskId
taskId :: EventInfo -> TaskId
taskId, Int
new_cap :: Int
new_cap :: EventInfo -> 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
_                             -> 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 forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map TaskId KernelThreadId
ma = forall a. Maybe a
Nothing  -- The task already exists.
      | KernelThreadId
tid forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map KernelThreadId Int
m     = forall a. Maybe a
Nothing  -- The OS thread already exists.
      | Bool
otherwise            = forall a. a -> Maybe a
Just (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert KernelThreadId
tid Int
cap Map KernelThreadId Int
m,
                                     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 forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup TaskId
taskId Map TaskId KernelThreadId
ma of
        Maybe KernelThreadId
Nothing  -> forall a. Maybe a
Nothing  -- The task doesn't exist.
        Just KernelThreadId
tid -> forall a. a -> Maybe a
Just (forall k a. Ord k => k -> Map k a -> Map k a
M.delete KernelThreadId
tid Map KernelThreadId Int
m,
                          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 forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup TaskId
taskId Map TaskId KernelThreadId
ma of
        Maybe KernelThreadId
Nothing -> forall a. Maybe a
Nothing  -- The task doesn't exist.
        Just KernelThreadId
tid -> forall a. a -> Maybe a
Just (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.