Threading.hs

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}

-- |
-- Module      : Test.DejaFu.Conc.Internal.Threading
-- Copyright   : (c) 2016--2020 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : ExistentialQuantification, FlexibleContexts, RankNTypes
--
-- Operations and types for threads. This module is NOT considered to
-- form part of the public interface of this library.
module Test.DejaFu.Conc.Internal.Threading where

import           Control.Exception                (Exception, MaskingState(..),
                                                   SomeException, fromException)
import           Data.List                        (intersect)
import           Data.Map.Strict                  (Map)
import qualified Data.Map.Strict                  as M
import           Data.Maybe                       (isJust)
import           GHC.Stack                        (HasCallStack)

import           Test.DejaFu.Conc.Internal.Common
import           Test.DejaFu.Internal
import           Test.DejaFu.Types

--------------------------------------------------------------------------------
-- * Threads

-- | Threads are stored in a map index by 'ThreadId'.
type Threads n = Map ThreadId (Thread n)

-- | All the state of a thread.
data Thread n = Thread
  { _continuation :: Action n
  -- ^ The next action to execute.
  , _blocking     :: Maybe BlockedOn
  -- ^ The state of any blocks.
  , _handlers     :: [Handler n]
  -- ^ Stack of exception handlers
  , _masking      :: MaskingState
  -- ^ The exception masking state.
  , _bound        :: Maybe (BoundThread n (Action n))
  -- ^ State for the associated bound thread, if it exists.
  }

-- | Construct a thread with just one action
mkthread :: Action n -> Thread n
mkthread c = Thread c Nothing [] Unmasked Nothing

--------------------------------------------------------------------------------
-- * Blocking

-- | A @BlockedOn@ is used to determine what sort of variable a thread
-- is blocked on.
data BlockedOn = OnMVarFull MVarId | OnMVarEmpty MVarId | OnTVar [TVarId] | OnMask ThreadId deriving Eq

-- | Determine if a thread is blocked in a certain way.
(~=) :: Thread n -> BlockedOn -> Bool
thread ~= theblock = case (_blocking thread, theblock) of
  (Just (OnMVarFull  _), OnMVarFull  _) -> True
  (Just (OnMVarEmpty _), OnMVarEmpty _) -> True
  (Just (OnTVar      _), OnTVar      _) -> True
  (Just (OnMask      _), OnMask      _) -> True
  _ -> False

--------------------------------------------------------------------------------
-- * Exceptions

-- | An exception handler.
data Handler n = forall e. Exception e => Handler MaskingState (e -> Action n)

-- | Propagate an exception upwards, finding the closest handler
-- which can deal with it.
propagate :: HasCallStack => SomeException -> ThreadId -> Threads n -> Maybe (Threads n)
propagate e tid threads = raise <$> propagate' handlers where
  handlers = _handlers (elookup tid threads)

  raise (ms, act, hs) = except ms act hs tid threads

  propagate' [] = Nothing
  propagate' (Handler ms h:hs) = maybe (propagate' hs) ((\act -> Just (ms, act, hs)) . h) (fromException e)

-- | Check if a thread can be interrupted by an exception.
interruptible :: Thread n -> Bool
interruptible thread =
  _masking thread == Unmasked ||
  (_masking thread == MaskedInterruptible && isJust (_blocking thread))

-- | Register a new exception handler.
catching :: (Exception e, HasCallStack) => (e -> Action n) -> ThreadId -> Threads n -> Threads n
catching h = eadjust $ \thread ->
  let ms0 = _masking thread
      h'  = Handler ms0 h
  in thread { _handlers = h' : _handlers thread }

-- | Remove the most recent exception handler.
uncatching :: HasCallStack => ThreadId -> Threads n -> Threads n
uncatching = eadjust $ \thread ->
  thread { _handlers = etail (_handlers thread) }

-- | Raise an exception in a thread.
except :: HasCallStack => MaskingState -> Action n -> [Handler n] -> ThreadId -> Threads n -> Threads n
except ms act hs = eadjust $ \thread -> thread
  { _continuation = act
  , _masking = ms
  , _handlers = hs
  , _blocking = Nothing
  }

-- | Set the masking state of a thread.
mask :: HasCallStack => MaskingState -> ThreadId -> Threads n -> Threads n
mask ms = eadjust $ \thread -> thread { _masking = ms }

--------------------------------------------------------------------------------
-- * Manipulating threads

-- | Replace the @Action@ of a thread.
goto :: HasCallStack => Action n -> ThreadId -> Threads n -> Threads n
goto a = eadjust $ \thread -> thread { _continuation = a }

-- | Start a thread with the given ID, inheriting the masking state
-- from the parent thread. This ID must not already be in use!
launch :: HasCallStack => ThreadId -> ThreadId -> ((forall b. ModelConc n b -> ModelConc n b) -> Action n) -> Threads n -> Threads n
launch parent tid a threads = launch' ms tid a threads where
  ms = _masking (elookup parent threads)

-- | Start a thread with the given ID and masking state. This must not already be in use!
launch' :: HasCallStack => MaskingState -> ThreadId -> ((forall b. ModelConc n b -> ModelConc n b) -> Action n) -> Threads n -> Threads n
launch' ms tid a = einsert tid thread where
  thread = Thread (a umask) Nothing [] ms Nothing

  umask mb = resetMask True Unmasked >> mb >>= \b -> resetMask False ms >> pure b
  resetMask typ m = ModelConc $ \k -> AResetMask typ True m $ k ()

-- | Block a thread.
block :: HasCallStack => BlockedOn -> ThreadId -> Threads n -> Threads n
block blockedOn = eadjust $ \thread -> thread { _blocking = Just blockedOn }

-- | Unblock all threads waiting on the appropriate block. For 'TVar'
-- blocks, this will wake all threads waiting on at least one of the
-- given 'TVar's.
wake :: BlockedOn -> Threads n -> (Threads n, [ThreadId])
wake blockedOn threads = (unblock <$> threads, M.keys $ M.filter isBlocked threads) where
  unblock thread
    | isBlocked thread = thread { _blocking = Nothing }
    | otherwise = thread

  isBlocked thread = case (_blocking thread, blockedOn) of
    (Just (OnTVar tvids), OnTVar blockedOn') -> tvids `intersect` blockedOn' /= []
    (theblock, _) -> theblock == Just blockedOn

-------------------------------------------------------------------------------
-- ** Bound threads

-- | Turn a thread into a bound thread.
makeBound :: (MonadDejaFu n, HasCallStack)
  => n (BoundThread n (Action n)) -> ThreadId -> Threads n -> n (Threads n)
makeBound fbt tid threads = do
  bt <- fbt
  pure (eadjust (\t -> t { _bound = Just bt }) tid threads)

-- | Kill a thread and remove it from the thread map.
--
-- If the thread is bound, the worker thread is cleaned up.
kill :: (MonadDejaFu n, HasCallStack) => ThreadId -> Threads n -> n (Threads n)
kill tid threads = do
  let thread = elookup tid threads
  maybe (pure ()) killBoundThread (_bound thread)
  pure (M.delete tid threads)
-- | Run an action.
--
-- If the thread is bound, the action is run in the worker thread.
runLiftedAct :: MonadDejaFu n => ThreadId -> Threads n -> n (Action n) -> n (Action n)
runLiftedAct tid threads ma = case _bound =<< M.lookup tid threads of
  Just bt -> runInBoundThread bt ma
  Nothing -> ma