{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- |
-- Module      : Test.DejaFu.Conc.Internal
-- Copyright   : (c) 2016--2021 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : FlexibleContexts, LambdaCase, RankNTypes, RecordWildCards, ScopedTypeVariables
--
-- Concurrent monads with a fixed scheduler: internal types and
-- functions. This module is NOT considered to form part of the public
-- interface of this library.
module Test.DejaFu.Conc.Internal where

import           Control.Exception                   (Exception,
                                                      MaskingState(..),
                                                      toException)
import qualified Control.Monad.Catch                 as E
import           Data.Foldable                       (foldrM)
import           Data.Functor                        (void)
import           Data.List                           (nub, partition, sortOn)
import qualified Data.Map.Strict                     as M
import           Data.Maybe                          (isJust, isNothing)
import           Data.Monoid                         ((<>))
import           Data.Sequence                       (Seq)
import qualified Data.Sequence                       as Seq
import           GHC.Stack                           (HasCallStack)

import           Test.DejaFu.Conc.Internal.Common
import           Test.DejaFu.Conc.Internal.Memory
import           Test.DejaFu.Conc.Internal.STM
import           Test.DejaFu.Conc.Internal.Threading
import           Test.DejaFu.Internal
import           Test.DejaFu.Schedule
import           Test.DejaFu.Types

--------------------------------------------------------------------------------
-- * Set-up

-- | 'Trace' but as a sequence.
type SeqTrace
  = Seq (Decision, [(ThreadId, Lookahead)], ThreadAction)

-- | The result of running a concurrent program.
data CResult n g a = CResult
  { forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext :: Context n g
  , forall (n :: * -> *) g a.
CResult n g a -> Ref n (Maybe (Either Condition a))
finalRef :: Ref n (Maybe (Either Condition a))
  , forall (n :: * -> *) g a. CResult n g a -> Threads n -> n ()
finalRestore :: Threads n -> n ()
  -- ^ Meaningless if this result doesn't come from a snapshotting
  -- execution.
  , forall (n :: * -> *) g a. CResult n g a -> SeqTrace
finalTrace :: SeqTrace
  , forall (n :: * -> *) g a.
CResult n g a -> Maybe (ThreadId, ThreadAction)
finalDecision :: Maybe (ThreadId, ThreadAction)
  }

-- | Run a concurrent computation with a given 'Scheduler' and initial
-- state, returning a Condition reason on error. Also returned is the
-- final state of the scheduler, and an execution trace.
runConcurrency :: (MonadDejaFu n, HasCallStack)
  => [Invariant n ()]
  -> Bool
  -> Scheduler g
  -> MemType
  -> g
  -> IdSource
  -> Int
  -> ModelConc n a
  -> n (CResult n g a)
runConcurrency :: forall (n :: * -> *) g a.
(MonadDejaFu n, HasCallStack) =>
[Invariant n ()]
-> Bool
-> Scheduler g
-> MemType
-> g
-> IdSource
-> Int
-> ModelConc n a
-> n (CResult n g a)
runConcurrency [Invariant n ()]
invariants Bool
forSnapshot Scheduler g
sched MemType
memtype g
g IdSource
idsrc Int
caps ModelConc n a
ma = do
  let ctx :: Context n g
ctx = Context { cSchedState :: g
cSchedState    = g
g
                    , cIdSource :: IdSource
cIdSource      = IdSource
idsrc
                    , cThreads :: Threads n
cThreads       = forall k a. Map k a
M.empty
                    , cWriteBuf :: WriteBuffer n
cWriteBuf      = forall (n :: * -> *). WriteBuffer n
emptyBuffer
                    , cCaps :: Int
cCaps          = Int
caps
                    , cInvariants :: InvariantContext n
cInvariants    = InvariantContext { icActive :: [Invariant n ()]
icActive = [Invariant n ()]
invariants, icBlocked :: [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
icBlocked = [] }
                    , cNewInvariants :: [Invariant n ()]
cNewInvariants = []
                    , cCState :: ConcurrencyState
cCState        = ConcurrencyState
initialCState
                    }
  (Action n
c, Ref n (Maybe (Either Condition a))
ref) <- forall (n :: * -> *) x a b.
MonadDejaFu n =>
(n () -> x)
-> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref n (Maybe b))
runRefCont forall (n :: * -> *). n () -> Action n
AStop (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right) (forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc ModelConc n a
ma)
  let threads0 :: Threads n
threads0 = forall (n :: * -> *).
HasCallStack =>
MaskingState
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
launch' MaskingState
Unmasked ThreadId
initialThread (\forall b. ModelConc n b -> ModelConc n b
_ -> Action n
c) (forall (n :: * -> *) g. Context n g -> Threads n
cThreads Context n g
ctx)
  Threads n
threads <- case forall (m :: * -> *) a.
MonadDejaFu m =>
Maybe (m (BoundThread m a))
forkBoundThread of
    Just n (BoundThread n (Action n))
fbt -> forall (n :: * -> *).
(MonadDejaFu n, HasCallStack) =>
n (BoundThread n (Action n))
-> ThreadId -> Threads n -> n (Threads n)
makeBound n (BoundThread n (Action n))
fbt ThreadId
initialThread Threads n
threads0
    Maybe (n (BoundThread n (Action n)))
Nothing  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Threads n
threads0
  CResult n g a
res <- forall (n :: * -> *) g a.
(MonadDejaFu n, HasCallStack) =>
Bool
-> Scheduler g
-> MemType
-> Ref n (Maybe (Either Condition a))
-> Context n g
-> n (CResult n g a)
runThreads Bool
forSnapshot Scheduler g
sched MemType
memtype Ref n (Maybe (Either Condition a))
ref Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads }
  forall (n :: * -> *) g.
(MonadDejaFu n, HasCallStack) =>
Context n g -> n ()
killAllThreads (forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext CResult n g a
res)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure CResult n g a
res

-- | Like 'runConcurrency' but starts from a snapshot.
runConcurrencyWithSnapshot :: (MonadDejaFu n, HasCallStack)
  => Scheduler g
  -> MemType
  -> Context n g
  -> (Threads n -> n ())
  -> ModelConc n a
  -> n (CResult n g a)
runConcurrencyWithSnapshot :: forall (n :: * -> *) g a.
(MonadDejaFu n, HasCallStack) =>
Scheduler g
-> MemType
-> Context n g
-> (Threads n -> n ())
-> ModelConc n a
-> n (CResult n g a)
runConcurrencyWithSnapshot Scheduler g
sched MemType
memtype Context n g
ctx Threads n -> n ()
restore ModelConc n a
ma = do
  (Action n
c, Ref n (Maybe (Either Condition a))
ref) <- forall (n :: * -> *) x a b.
MonadDejaFu n =>
(n () -> x)
-> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref n (Maybe b))
runRefCont forall (n :: * -> *). n () -> Action n
AStop (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right) (forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc ModelConc n a
ma)
  let threads0 :: Threads n
threads0 = forall k a. Ord k => k -> Map k a -> Map k a
M.delete ThreadId
initialThread (forall (n :: * -> *) g. Context n g -> Threads n
cThreads Context n g
ctx)
  let threads1 :: Threads n
threads1 = forall (n :: * -> *).
HasCallStack =>
MaskingState
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
launch' MaskingState
Unmasked ThreadId
initialThread (\forall b. ModelConc n b -> ModelConc n b
_ -> Action n
c) Threads n
threads0
  Threads n
threads <- case forall (m :: * -> *) a.
MonadDejaFu m =>
Maybe (m (BoundThread m a))
forkBoundThread of
    Just n (BoundThread n (Action n))
fbt -> do
      let boundThreads :: Threads n
boundThreads = forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *). Thread n -> Maybe (BoundThread n (Action n))
_bound) Threads n
threads1
      Threads n
threads' <- forall (n :: * -> *).
(MonadDejaFu n, HasCallStack) =>
n (BoundThread n (Action n))
-> ThreadId -> Threads n -> n (Threads n)
makeBound n (BoundThread n (Action n))
fbt ThreadId
initialThread Threads n
threads1
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (forall (n :: * -> *).
(MonadDejaFu n, HasCallStack) =>
n (BoundThread n (Action n))
-> ThreadId -> Threads n -> n (Threads n)
makeBound n (BoundThread n (Action n))
fbt) Threads n
threads' (forall k a. Map k a -> [k]
M.keys Threads n
boundThreads)
    Maybe (n (BoundThread n (Action n)))
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Threads n
threads1
  Threads n -> n ()
restore Threads n
threads
  CResult n g a
res <- forall (n :: * -> *) g a.
(MonadDejaFu n, HasCallStack) =>
Bool
-> Scheduler g
-> MemType
-> Ref n (Maybe (Either Condition a))
-> Context n g
-> n (CResult n g a)
runThreads Bool
False Scheduler g
sched MemType
memtype Ref n (Maybe (Either Condition a))
ref Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads }
  forall (n :: * -> *) g.
(MonadDejaFu n, HasCallStack) =>
Context n g -> n ()
killAllThreads (forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext CResult n g a
res)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure CResult n g a
res

-- | Kill the remaining threads
killAllThreads :: (MonadDejaFu n, HasCallStack) => Context n g -> n ()
killAllThreads :: forall (n :: * -> *) g.
(MonadDejaFu n, HasCallStack) =>
Context n g -> n ()
killAllThreads Context n g
ctx =
  let finalThreads :: Threads n
finalThreads = forall (n :: * -> *) g. Context n g -> Threads n
cThreads Context n g
ctx
  in forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (n :: * -> *).
(MonadDejaFu n, HasCallStack) =>
ThreadId -> Threads n -> n (Threads n)
`kill` Threads n
finalThreads) (forall k a. Map k a -> [k]
M.keys Threads n
finalThreads)

-------------------------------------------------------------------------------
-- * Execution

-- | The context a collection of threads are running in.
data Context n g = Context
  { forall (n :: * -> *) g. Context n g -> g
cSchedState    :: g
  , forall (n :: * -> *) g. Context n g -> IdSource
cIdSource      :: IdSource
  , forall (n :: * -> *) g. Context n g -> Threads n
cThreads       :: Threads n
  , forall (n :: * -> *) g. Context n g -> WriteBuffer n
cWriteBuf      :: WriteBuffer n
  , forall (n :: * -> *) g. Context n g -> Int
cCaps          :: Int
  , forall (n :: * -> *) g. Context n g -> InvariantContext n
cInvariants    :: InvariantContext n
  , forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cNewInvariants :: [Invariant n ()]
  , forall (n :: * -> *) g. Context n g -> ConcurrencyState
cCState        :: ConcurrencyState
  }

-- | Run a collection of threads, until there are no threads left.
runThreads :: (MonadDejaFu n, HasCallStack)
  => Bool
  -> Scheduler g
  -> MemType
  -> Ref n (Maybe (Either Condition a))
  -> Context n g
  -> n (CResult n g a)
runThreads :: forall (n :: * -> *) g a.
(MonadDejaFu n, HasCallStack) =>
Bool
-> Scheduler g
-> MemType
-> Ref n (Maybe (Either Condition a))
-> Context n g
-> n (CResult n g a)
runThreads Bool
forSnapshot Scheduler g
sched MemType
memtype Ref n (Maybe (Either Condition a))
ref = (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
schedule (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) forall a. Seq a
Seq.empty forall a. Maybe a
Nothing where
  -- signal failure & terminate
  die :: Condition
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
die Condition
reason Map ThreadId (Thread n) -> n ()
finalR SeqTrace
finalT Maybe (ThreadId, ThreadAction)
finalD Context n g
finalC = do
    forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Maybe (Either Condition a))
ref (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Condition
reason)
    forall {f :: * -> *} {g}.
Applicative f =>
(Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> f (CResult n g a)
stop Map ThreadId (Thread n) -> n ()
finalR SeqTrace
finalT Maybe (ThreadId, ThreadAction)
finalD Context n g
finalC

  -- just terminate; 'ref' must have been written to before calling
  -- this
  stop :: (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> f (CResult n g a)
stop Map ThreadId (Thread n) -> n ()
finalR SeqTrace
finalT Maybe (ThreadId, ThreadAction)
finalD Context n g
finalC = forall (f :: * -> *) a. Applicative f => a -> f a
pure CResult
    { finalContext :: Context n g
finalContext  = Context n g
finalC
    , finalRef :: Ref n (Maybe (Either Condition a))
finalRef      = Ref n (Maybe (Either Condition a))
ref
    , finalRestore :: Map ThreadId (Thread n) -> n ()
finalRestore  = Map ThreadId (Thread n) -> n ()
finalR
    , finalTrace :: SeqTrace
finalTrace    = SeqTrace
finalT
    , finalDecision :: Maybe (ThreadId, ThreadAction)
finalDecision = Maybe (ThreadId, ThreadAction)
finalD
    }

  -- check for termination, pick a thread, and call 'step'
  schedule :: (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
schedule Map ThreadId (Thread n) -> n ()
restore SeqTrace
sofar Maybe (ThreadId, ThreadAction)
prior Context n g
ctx
    | Bool
isTerminated  = forall {f :: * -> *} {g}.
Applicative f =>
(Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> f (CResult n g a)
stop Map ThreadId (Thread n) -> n ()
restore SeqTrace
sofar Maybe (ThreadId, ThreadAction)
prior Context n g
ctx
    | Bool
isDeadlocked  = forall {g}.
Condition
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
die Condition
Deadlock Map ThreadId (Thread n) -> n ()
restore SeqTrace
sofar Maybe (ThreadId, ThreadAction)
prior Context n g
ctx
    | Bool
otherwise =
      let ctx' :: Context n g
ctx' = Context n g
ctx { cSchedState :: g
cSchedState = g
g' }
      in case Maybe ThreadId
choice of
           Just ThreadId
chosen -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ThreadId
chosen Map ThreadId (Thread n)
threadsc of
             Just Thread n
thread
               | forall {n :: * -> *}. Thread n -> Bool
isBlocked Thread n
thread -> forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
E.throwM Error
ScheduledBlockedThread
               | Bool
otherwise ->
                 let decision :: Decision
decision
                       | forall a. a -> Maybe a
Just ThreadId
chosen forall a. Eq a => a -> a -> Bool
== (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ThreadId, ThreadAction)
prior) = Decision
Continue
                       | (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ThreadId, ThreadAction)
prior) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(ThreadId, Lookahead)]
runnable' = ThreadId -> Decision
Start ThreadId
chosen
                       | Bool
otherwise = ThreadId -> Decision
SwitchTo ThreadId
chosen
                     alternatives :: [(ThreadId, Lookahead)]
alternatives = forall a. (a -> Bool) -> [a] -> [a]
filter (\(ThreadId
t, Lookahead
_) -> ThreadId
t forall a. Eq a => a -> a -> Bool
/= ThreadId
chosen) [(ThreadId, Lookahead)]
runnable'
                 in Decision
-> [(ThreadId, Lookahead)]
-> ThreadId
-> Thread n
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
step Decision
decision [(ThreadId, Lookahead)]
alternatives ThreadId
chosen Thread n
thread Map ThreadId (Thread n) -> n ()
restore SeqTrace
sofar Maybe (ThreadId, ThreadAction)
prior Context n g
ctx'
             Maybe (Thread n)
Nothing -> forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
E.throwM Error
ScheduledMissingThread
           Maybe ThreadId
Nothing -> forall {g}.
Condition
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
die Condition
Abort Map ThreadId (Thread n) -> n ()
restore SeqTrace
sofar Maybe (ThreadId, ThreadAction)
prior Context n g
ctx'
    where
      (Maybe ThreadId
choice, g
g')  = forall state.
Scheduler state
-> Maybe (ThreadId, ThreadAction)
-> NonEmpty (ThreadId, Lookahead)
-> ConcurrencyState
-> state
-> (Maybe ThreadId, state)
scheduleThread Scheduler g
sched Maybe (ThreadId, ThreadAction)
prior (forall a. HasCallStack => [a] -> NonEmpty a
efromList [(ThreadId, Lookahead)]
runnable') (forall (n :: * -> *) g. Context n g -> ConcurrencyState
cCState Context n g
ctx) (forall (n :: * -> *) g. Context n g -> g
cSchedState Context n g
ctx)
      runnable' :: [(ThreadId, Lookahead)]
runnable'     = [(ThreadId
t, forall (n :: * -> *). Action n -> Lookahead
lookahead (forall (n :: * -> *). Thread n -> Action n
_continuation Thread n
a)) | (ThreadId
t, Thread n
a) <- forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.assocs Map ThreadId (Thread n)
runnable]
      runnable :: Map ThreadId (Thread n)
runnable      = forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {n :: * -> *}. Thread n -> Bool
isBlocked) Map ThreadId (Thread n)
threadsc
      threadsc :: Map ThreadId (Thread n)
threadsc      = forall (n :: * -> *). WriteBuffer n -> Threads n -> Threads n
addCommitThreads (forall (n :: * -> *) g. Context n g -> WriteBuffer n
cWriteBuf Context n g
ctx) Map ThreadId (Thread n)
threads
      threads :: Map ThreadId (Thread n)
threads       = forall (n :: * -> *) g. Context n g -> Threads n
cThreads Context n g
ctx
      isBlocked :: Thread n -> Bool
isBlocked     = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *). Thread n -> Maybe BlockedOn
_blocking
      isTerminated :: Bool
isTerminated  = ThreadId
initialThread forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall k a. Map k a -> [k]
M.keys Map ThreadId (Thread n)
threads
      isDeadlocked :: Bool
isDeadlocked  = forall k a. Map k a -> Bool
M.null (forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {n :: * -> *}. Thread n -> Bool
isBlocked) Map ThreadId (Thread n)
threads)

  -- run the chosen thread for one step and then pass control back to
  -- 'schedule'
  step :: Decision
-> [(ThreadId, Lookahead)]
-> ThreadId
-> Thread n
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
step Decision
decision [(ThreadId, Lookahead)]
alternatives ThreadId
chosen Thread n
thread Map ThreadId (Thread n) -> n ()
restore SeqTrace
sofar Maybe (ThreadId, ThreadAction)
prior Context n g
ctx = do
      (What n g
res, ThreadAction
actOrTrc, Map ThreadId (Thread n) -> n ()
actionSnap) <- forall (n :: * -> *) g.
(MonadDejaFu n, HasCallStack) =>
Bool
-> Bool
-> Scheduler g
-> MemType
-> ThreadId
-> Action n
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
stepThread
          Bool
forSnapshot
          (forall a. Maybe a -> Bool
isNothing Maybe (ThreadId, ThreadAction)
prior)
          Scheduler g
sched
          MemType
memtype
          ThreadId
chosen
          (forall (n :: * -> *). Thread n -> Action n
_continuation Thread n
thread)
          Context n g
ctx
      let sofar' :: SeqTrace
sofar' = SeqTrace
sofar forall a. Semigroup a => a -> a -> a
<> forall {c}. c -> Seq (Decision, [(ThreadId, Lookahead)], c)
getTrc ThreadAction
actOrTrc
      let prior' :: Maybe (ThreadId, ThreadAction)
prior' = forall {b}. b -> Maybe (ThreadId, b)
getPrior ThreadAction
actOrTrc
      let restore' :: Map ThreadId (Thread n) -> n ()
restore' Map ThreadId (Thread n)
threads' =
            if Bool
forSnapshot
            then Map ThreadId (Thread n) -> n ()
restore Map ThreadId (Thread n)
threads' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Map ThreadId (Thread n) -> n ()
actionSnap Map ThreadId (Thread n)
threads'
            else Map ThreadId (Thread n) -> n ()
restore Map ThreadId (Thread n)
threads'
      let ctx' :: Context n g
ctx' = forall (n :: * -> *) g.
MemType
-> ThreadId
-> ThreadAction
-> What n g
-> Context n g
-> Context n g
fixContext MemType
memtype ThreadId
chosen ThreadAction
actOrTrc What n g
res Context n g
ctx
      case What n g
res of
        Succeeded Context n g
_ -> forall (n :: * -> *).
MonadDejaFu n =>
InvariantContext n -> n (Either SomeException (InvariantContext n))
checkInvariants (forall (n :: * -> *) g. Context n g -> InvariantContext n
cInvariants Context n g
ctx') forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Right InvariantContext n
ic ->
            (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
schedule Map ThreadId (Thread n) -> n ()
restore' SeqTrace
sofar' Maybe (ThreadId, ThreadAction)
prior' Context n g
ctx' { cInvariants :: InvariantContext n
cInvariants = InvariantContext n
ic }
          Left SomeException
exc ->
            forall {g}.
Condition
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
die (SomeException -> Condition
InvariantFailure SomeException
exc) Map ThreadId (Thread n) -> n ()
restore' SeqTrace
sofar' Maybe (ThreadId, ThreadAction)
prior' Context n g
ctx'
        Failed Condition
failure ->
          forall {g}.
Condition
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
die Condition
failure Map ThreadId (Thread n) -> n ()
restore' SeqTrace
sofar' Maybe (ThreadId, ThreadAction)
prior' Context n g
ctx'
    where
      getTrc :: c -> Seq (Decision, [(ThreadId, Lookahead)], c)
getTrc c
a = forall a. a -> Seq a
Seq.singleton (Decision
decision, [(ThreadId, Lookahead)]
alternatives, c
a)

      getPrior :: b -> Maybe (ThreadId, b)
getPrior b
a = forall a. a -> Maybe a
Just (ThreadId
chosen, b
a)

-- | Apply the context update from stepping an action.
fixContext :: MemType -> ThreadId -> ThreadAction -> What n g -> Context n g -> Context n g
fixContext :: forall (n :: * -> *) g.
MemType
-> ThreadId
-> ThreadAction
-> What n g
-> Context n g
-> Context n g
fixContext MemType
memtype ThreadId
tid ThreadAction
act What n g
what Context n g
ctx0 = forall {n :: * -> *} {g}. Context n g -> Context n g
fixContextCommon forall a b. (a -> b) -> a -> b
$ case What n g
what of
    Succeeded ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> Context n g
ctx
      { cThreads :: Threads n
cThreads =
          if (forall {n :: * -> *}. Thread n -> Bool
interruptible forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ThreadId
tid Threads n
cThreads) forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Bool
False
          then forall (n :: * -> *). ThreadId -> Threads n -> Threads n
unblockWaitingOn ThreadId
tid Threads n
cThreads
          else Threads n
cThreads
      }
    What n g
_ -> Context n g
ctx0
  where
  fixContextCommon :: Context n g -> Context n g
fixContextCommon ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} = Context n g
ctx
    { cThreads :: Threads n
cThreads    = forall (n :: * -> *). Threads n -> Threads n
delCommitThreads Threads n
cThreads
    , cInvariants :: InvariantContext n
cInvariants = forall (n :: * -> *).
ThreadAction -> InvariantContext n -> InvariantContext n
unblockInvariants ThreadAction
act InvariantContext n
cInvariants
    , cCState :: ConcurrencyState
cCState     = MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
cCState ThreadId
tid ThreadAction
act
    }

-- | @unblockWaitingOn tid@ unblocks every thread blocked in a
-- @throwTo tid@.
unblockWaitingOn :: ThreadId -> Threads n -> Threads n
unblockWaitingOn :: forall (n :: * -> *). ThreadId -> Threads n -> Threads n
unblockWaitingOn ThreadId
tid = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ \Thread n
thread -> case forall (n :: * -> *). Thread n -> Maybe BlockedOn
_blocking Thread n
thread of
  Just (OnMask ThreadId
t) | ThreadId
t forall a. Eq a => a -> a -> Bool
== ThreadId
tid -> Thread n
thread { _blocking :: Maybe BlockedOn
_blocking = forall a. Maybe a
Nothing }
  Maybe BlockedOn
_ -> Thread n
thread

--------------------------------------------------------------------------------
-- * Single-step execution

-- | What a thread did, for execution purposes.
data What n g
  = Succeeded (Context n g)
  -- ^ Action succeeded: continue execution.
  | Failed Condition
  -- ^ Action caused computation to fail: stop.

-- | Run a single thread one step, by dispatching on the type of
-- 'Action'.
--
-- Each case looks very similar.  This is deliberate, so that the
-- essential differences between actions are more apparent, and not
-- hidden by accidental differences in how things are expressed.
--
-- Note: the returned snapshot action will definitely not do the right
-- thing with relaxed memory.
stepThread :: forall n g. (MonadDejaFu n, HasCallStack)
  => Bool
  -- ^ Should we record a snapshot?
  -> Bool
  -- ^ Is this the first action?
  -> Scheduler g
  -- ^ The scheduler.
  -> MemType
  -- ^ The memory model to use.
  -> ThreadId
  -- ^ ID of the current thread
  -> Action n
  -- ^ Action to step
  -> Context n g
  -- ^ The execution context.
  -> n (What n g, ThreadAction, Threads n -> n ())
-- start a new thread, assigning it the next 'ThreadId'
stepThread :: forall (n :: * -> *) g.
(MonadDejaFu n, HasCallStack) =>
Bool
-> Bool
-> Scheduler g
-> MemType
-> ThreadId
-> Action n
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AFork String
n (forall b. ModelConc n b -> ModelConc n b) -> Action n
a ThreadId -> Action n
b) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
  let (IdSource
idSource', ThreadId
newtid) = String -> IdSource -> (IdSource, ThreadId)
nextTId String
n IdSource
cIdSource
      threads' :: Threads n
threads' = forall (n :: * -> *).
HasCallStack =>
ThreadId
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
launch ThreadId
tid ThreadId
newtid (forall b. ModelConc n b -> ModelConc n b) -> Action n
a Threads n
cThreads
  in ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (ThreadId -> Action n
b ThreadId
newtid) ThreadId
tid Threads n
threads', cIdSource :: IdSource
cIdSource = IdSource
idSource' }
     , ThreadId -> ThreadAction
Fork ThreadId
newtid
     , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
     )

-- start a new bound thread, assigning it the next 'ThreadId'
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AForkOS String
n (forall b. ModelConc n b -> ModelConc n b) -> Action n
a ThreadId -> Action n
b) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> case forall (m :: * -> *) a.
MonadDejaFu m =>
Maybe (m (BoundThread m a))
forkBoundThread of
  Just n (BoundThread n (Action n))
fbt -> do
    let (IdSource
idSource', ThreadId
newtid) = String -> IdSource -> (IdSource, ThreadId)
nextTId String
n IdSource
cIdSource
    let threads' :: Threads n
threads' = forall (n :: * -> *).
HasCallStack =>
ThreadId
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
launch ThreadId
tid ThreadId
newtid (forall b. ModelConc n b -> ModelConc n b) -> Action n
a Threads n
cThreads
    Threads n
threads'' <- forall (n :: * -> *).
(MonadDejaFu n, HasCallStack) =>
n (BoundThread n (Action n))
-> ThreadId -> Threads n -> n (Threads n)
makeBound n (BoundThread n (Action n))
fbt ThreadId
newtid Threads n
threads'
    forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (ThreadId -> Action n
b ThreadId
newtid) ThreadId
tid Threads n
threads'', cIdSource :: IdSource
cIdSource = IdSource
idSource' }
         , ThreadId -> ThreadAction
ForkOS ThreadId
newtid
         , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
         )
  Maybe (n (BoundThread n (Action n)))
Nothing ->
    forall (n :: * -> *) e g.
(MonadDejaFu n, Exception e) =>
(Maybe MaskingState -> ThreadAction)
-> ThreadId
-> e
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
stepThrow Maybe MaskingState -> ThreadAction
Throw ThreadId
tid (String -> MonadFailException
MonadFailException String
"dejafu is running with bound threads disabled - do not use forkOS") Context n g
ctx

-- check if we support bound threads
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ASupportsBoundThreads Bool -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  let sbt :: Bool
sbt = forall a. Maybe a -> Bool
isJust (forall (m :: * -> *) a.
MonadDejaFu m =>
Maybe (m (BoundThread m a))
forkBoundThread :: Maybe (n (BoundThread n ())))
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (Bool -> Action n
c Bool
sbt) ThreadId
tid Threads n
cThreads }
       , Bool -> ThreadAction
SupportsBoundThreads Bool
sbt
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- check if the current thread is bound
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AIsBound Bool -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  let isBound :: Bool
isBound = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *). Thread n -> Maybe (BoundThread n (Action n))
_bound forall a b. (a -> b) -> a -> b
$ forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
tid Threads n
cThreads
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (Bool -> Action n
c Bool
isBound) ThreadId
tid Threads n
cThreads }
       , Bool -> ThreadAction
IsCurrentThreadBound Bool
isBound
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- get the 'ThreadId' of the current thread
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AMyTId ThreadId -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} ->
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (ThreadId -> Action n
c ThreadId
tid) ThreadId
tid Threads n
cThreads }
       , ThreadAction
MyThreadId
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- get the number of capabilities
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AGetNumCapabilities Int -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} ->
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (Int -> Action n
c Int
cCaps) ThreadId
tid Threads n
cThreads }
       , Int -> ThreadAction
GetNumCapabilities Int
cCaps
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- set the number of capabilities
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ASetNumCapabilities Int
i Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} ->
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid Threads n
cThreads, cCaps :: Int
cCaps = Int
i }
       , Int -> ThreadAction
SetNumCapabilities Int
i
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- yield the current thread
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AYield Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} ->
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid Threads n
cThreads }
       , ThreadAction
Yield
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- yield the current thread (delay is ignored)
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ADelay Int
n Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} ->
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid Threads n
cThreads }
       , Int -> ThreadAction
ThreadDelay Int
n
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- create a new @MVar@, using the next 'MVarId'.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ANewMVar String
n ModelMVar n a -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  let (IdSource
idSource', MVarId
newmvid) = String -> IdSource -> (IdSource, MVarId)
nextMVId String
n IdSource
cIdSource
  Ref n (Maybe a)
ref <- forall (m :: * -> *) a. MonadDejaFu m => a -> m (Ref m a)
newRef forall a. Maybe a
Nothing
  let mvar :: ModelMVar n a
mvar = forall (n :: * -> *) a. MVarId -> Ref n (Maybe a) -> ModelMVar n a
ModelMVar MVarId
newmvid Ref n (Maybe a)
ref
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (ModelMVar n a -> Action n
c ModelMVar n a
mvar) ThreadId
tid Threads n
cThreads, cIdSource :: IdSource
cIdSource = IdSource
idSource' }
       , MVarId -> ThreadAction
NewMVar MVarId
newmvid
       , forall a b. a -> b -> a
const (forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Maybe a)
ref forall a. Maybe a
Nothing)
       )

-- put a value into a @MVar@, blocking the thread until it's empty.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (APutMVar mvar :: ModelMVar n a
mvar@ModelMVar{MVarId
Ref n (Maybe a)
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
mvarRef :: Ref n (Maybe a)
mvarId :: MVarId
..} a
a Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
woken, n ()
effect) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelMVar n a
-> a
-> Action n
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
putIntoMVar ModelMVar n a
mvar a
a Action n
c ThreadId
tid Threads n
cThreads
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads' }
       , if Bool
success then MVarId -> [ThreadId] -> ThreadAction
PutMVar MVarId
mvarId [ThreadId]
woken else MVarId -> ThreadAction
BlockedPutMVar MVarId
mvarId
       , forall a b. a -> b -> a
const n ()
effect
       )

-- try to put a value into a @MVar@, without blocking.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ATryPutMVar mvar :: ModelMVar n a
mvar@ModelMVar{MVarId
Ref n (Maybe a)
mvarRef :: Ref n (Maybe a)
mvarId :: MVarId
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
..} a
a Bool -> Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
woken, n ()
effect) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelMVar n a
-> a
-> (Bool -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
tryPutIntoMVar ModelMVar n a
mvar a
a Bool -> Action n
c ThreadId
tid Threads n
cThreads
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads' }
       , MVarId -> Bool -> [ThreadId] -> ThreadAction
TryPutMVar MVarId
mvarId Bool
success [ThreadId]
woken
       , forall a b. a -> b -> a
const n ()
effect
       )

-- get the value from a @MVar@, without emptying, blocking the thread
-- until it's full.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AReadMVar mvar :: ModelMVar n a
mvar@ModelMVar{MVarId
Ref n (Maybe a)
mvarRef :: Ref n (Maybe a)
mvarId :: MVarId
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
..} a -> Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
_, n ()
_) <- forall (n :: * -> *) a.
(MonadDejaFu n, HasCallStack) =>
ModelMVar n a
-> (a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
readFromMVar ModelMVar n a
mvar a -> Action n
c ThreadId
tid Threads n
cThreads
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads' }
       , if Bool
success then MVarId -> ThreadAction
ReadMVar MVarId
mvarId else MVarId -> ThreadAction
BlockedReadMVar MVarId
mvarId
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- try to get the value from a @MVar@, without emptying, without
-- blocking.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ATryReadMVar mvar :: ModelMVar n a
mvar@ModelMVar{MVarId
Ref n (Maybe a)
mvarRef :: Ref n (Maybe a)
mvarId :: MVarId
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
..} Maybe a -> Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
_, n ()
_) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
tryReadFromMVar ModelMVar n a
mvar Maybe a -> Action n
c ThreadId
tid Threads n
cThreads
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads' }
       , MVarId -> Bool -> ThreadAction
TryReadMVar MVarId
mvarId Bool
success
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- take the value from a @MVar@, blocking the thread until it's full.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ATakeMVar mvar :: ModelMVar n a
mvar@ModelMVar{MVarId
Ref n (Maybe a)
mvarRef :: Ref n (Maybe a)
mvarId :: MVarId
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
..} a -> Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
woken, n ()
effect) <- forall (n :: * -> *) a.
(MonadDejaFu n, HasCallStack) =>
ModelMVar n a
-> (a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
takeFromMVar ModelMVar n a
mvar a -> Action n
c ThreadId
tid Threads n
cThreads
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads' }
       , if Bool
success then MVarId -> [ThreadId] -> ThreadAction
TakeMVar MVarId
mvarId [ThreadId]
woken else MVarId -> ThreadAction
BlockedTakeMVar MVarId
mvarId
       , forall a b. a -> b -> a
const n ()
effect
       )

-- try to take the value from a @MVar@, without blocking.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ATryTakeMVar mvar :: ModelMVar n a
mvar@ModelMVar{MVarId
Ref n (Maybe a)
mvarRef :: Ref n (Maybe a)
mvarId :: MVarId
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
..} Maybe a -> Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
woken, n ()
effect) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
tryTakeFromMVar ModelMVar n a
mvar Maybe a -> Action n
c ThreadId
tid Threads n
cThreads
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads' }
       , MVarId -> Bool -> [ThreadId] -> ThreadAction
TryTakeMVar MVarId
mvarId Bool
success [ThreadId]
woken
       , forall a b. a -> b -> a
const n ()
effect
       )

-- create a new @IORef@, using the next 'IORefId'.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_  ThreadId
tid (ANewIORef String
n a
a ModelIORef n a -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  let (IdSource
idSource', IORefId
newiorid) = String -> IdSource -> (IdSource, IORefId)
nextIORId String
n IdSource
cIdSource
  let val :: (Map k a, Integer, a)
val = (forall k a. Map k a
M.empty, Integer
0, a
a)
  Ref n (Map ThreadId a, Integer, a)
ioref <- forall (m :: * -> *) a. MonadDejaFu m => a -> m (Ref m a)
newRef forall {k} {a}. (Map k a, Integer, a)
val
  let ref :: ModelIORef n a
ref = forall (n :: * -> *) a.
IORefId -> Ref n (Map ThreadId a, Integer, a) -> ModelIORef n a
ModelIORef IORefId
newiorid Ref n (Map ThreadId a, Integer, a)
ioref
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (ModelIORef n a -> Action n
c ModelIORef n a
ref) ThreadId
tid Threads n
cThreads, cIdSource :: IdSource
cIdSource = IdSource
idSource' }
       , IORefId -> ThreadAction
NewIORef IORefId
newiorid
       , forall a b. a -> b -> a
const (forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Map ThreadId a, Integer, a)
ioref forall {k} {a}. (Map k a, Integer, a)
val)
       )

-- read from a @IORef@.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_  ThreadId
tid (AReadIORef ref :: ModelIORef n a
ref@ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
..} a -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  a
val <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n a
readIORef ModelIORef n a
ref ThreadId
tid
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (a -> Action n
c a
val) ThreadId
tid Threads n
cThreads }
       , IORefId -> ThreadAction
ReadIORef IORefId
iorefId
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- read from a @IORef@ for future compare-and-swap operations.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AReadIORefCas ref :: ModelIORef n a
ref@ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} ModelTicket a -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  ModelTicket a
tick <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (ModelTicket a)
readForTicket ModelIORef n a
ref ThreadId
tid
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (ModelTicket a -> Action n
c ModelTicket a
tick) ThreadId
tid Threads n
cThreads }
       , IORefId -> ThreadAction
ReadIORefCas IORefId
iorefId
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- modify a @IORef@.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AModIORef ref :: ModelIORef n a
ref@ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} a -> (a, b)
f b -> Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  (a
new, b
val) <- a -> (a, b)
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n a
readIORef ModelIORef n a
ref ThreadId
tid
  n ()
effect <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> a -> n (n ())
writeImmediate ModelIORef n a
ref a
new
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (b -> Action n
c b
val) ThreadId
tid Threads n
cThreads }
       , IORefId -> ThreadAction
ModIORef IORefId
iorefId
       , forall a b. a -> b -> a
const n ()
effect
       )

-- modify a @IORef@ using a compare-and-swap.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AModIORefCas ref :: ModelIORef n a
ref@ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} a -> (a, b)
f b -> Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  tick :: ModelTicket a
tick@(ModelTicket IORefId
_ Integer
_ a
old) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (ModelTicket a)
readForTicket ModelIORef n a
ref ThreadId
tid
  let (a
new, b
val) = a -> (a, b)
f a
old
  (Bool
_, ModelTicket a
_, n ()
effect) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a
-> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())
casIORef ModelIORef n a
ref ThreadId
tid ModelTicket a
tick a
new
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (b -> Action n
c b
val) ThreadId
tid Threads n
cThreads }
       , IORefId -> ThreadAction
ModIORefCas IORefId
iorefId
       , forall a b. a -> b -> a
const n ()
effect
       )

-- write to a @IORef@ without synchronising.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
memtype ThreadId
tid (AWriteIORef ref :: ModelIORef n a
ref@ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} a
a Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> case MemType
memtype of
  -- write immediately.
  MemType
SequentialConsistency -> do
    n ()
effect <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> a -> n (n ())
writeImmediate ModelIORef n a
ref a
a
    forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid Threads n
cThreads }
         , IORefId -> ThreadAction
WriteIORef IORefId
iorefId
         , forall a b. a -> b -> a
const n ()
effect
         )
  -- add to buffer using thread id.
  MemType
TotalStoreOrder -> do
    WriteBuffer n
wb' <- forall (n :: * -> *) a.
MonadDejaFu n =>
WriteBuffer n
-> (ThreadId, Maybe IORefId)
-> ModelIORef n a
-> a
-> n (WriteBuffer n)
bufferWrite WriteBuffer n
cWriteBuf (ThreadId
tid, forall a. Maybe a
Nothing) ModelIORef n a
ref a
a
    forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid Threads n
cThreads, cWriteBuf :: WriteBuffer n
cWriteBuf = WriteBuffer n
wb' }
         , IORefId -> ThreadAction
WriteIORef IORefId
iorefId
         , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
         )
  -- add to buffer using both thread id and IORef id
  MemType
PartialStoreOrder -> do
    WriteBuffer n
wb' <- forall (n :: * -> *) a.
MonadDejaFu n =>
WriteBuffer n
-> (ThreadId, Maybe IORefId)
-> ModelIORef n a
-> a
-> n (WriteBuffer n)
bufferWrite WriteBuffer n
cWriteBuf (ThreadId
tid, forall a. a -> Maybe a
Just IORefId
iorefId) ModelIORef n a
ref a
a
    forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid Threads n
cThreads, cWriteBuf :: WriteBuffer n
cWriteBuf = WriteBuffer n
wb' }
         , IORefId -> ThreadAction
WriteIORef IORefId
iorefId
         , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
         )

-- perform a compare-and-swap on a @IORef@.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ACasIORef ref :: ModelIORef n a
ref@ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} ModelTicket a
tick a
a (Bool, ModelTicket a) -> Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  (Bool
suc, ModelTicket a
tick', n ()
effect) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a
-> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())
casIORef ModelIORef n a
ref ThreadId
tid ModelTicket a
tick a
a
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto ((Bool, ModelTicket a) -> Action n
c (Bool
suc, ModelTicket a
tick')) ThreadId
tid Threads n
cThreads }
       , IORefId -> Bool -> ThreadAction
CasIORef IORefId
iorefId Bool
suc
       , forall a b. a -> b -> a
const n ()
effect
       )

-- commit a @IORef@ write
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
memtype ThreadId
_ (ACommit ThreadId
t IORefId
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  WriteBuffer n
wb' <- case MemType
memtype of
    -- shouldn't ever get here
    MemType
SequentialConsistency ->
      forall a. HasCallStack => String -> a
fatal String
"stepThread.ACommit" String
"Attempting to commit under SequentialConsistency"
    -- commit using the thread id.
    MemType
TotalStoreOrder ->
      forall (n :: * -> *).
MonadDejaFu n =>
WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
commitWrite WriteBuffer n
cWriteBuf (ThreadId
t, forall a. Maybe a
Nothing)
    -- commit using the IORef id.
    MemType
PartialStoreOrder ->
      forall (n :: * -> *).
MonadDejaFu n =>
WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
commitWrite WriteBuffer n
cWriteBuf (ThreadId
t, forall a. a -> Maybe a
Just IORefId
c)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cWriteBuf :: WriteBuffer n
cWriteBuf = WriteBuffer n
wb' }
       , ThreadId -> IORefId -> ThreadAction
CommitIORef ThreadId
t IORefId
c
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- run a STM transaction atomically.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AAtom ModelSTM n a
stm a -> Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  (Result a
res, n ()
effect, IdSource
idSource', [TAction]
trace) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelSTM n a -> IdSource -> n (Result a, n (), IdSource, [TAction])
runTransaction ModelSTM n a
stm IdSource
cIdSource
  case Result a
res of
    Success [TVarId]
_ [TVarId]
written a
val -> do
      let (Threads n
threads', [ThreadId]
woken) = forall (n :: * -> *).
BlockedOn -> Threads n -> (Threads n, [ThreadId])
wake ([TVarId] -> BlockedOn
OnTVar [TVarId]
written) Threads n
cThreads
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (a -> Action n
c a
val) ThreadId
tid Threads n
threads', cIdSource :: IdSource
cIdSource = IdSource
idSource' }
           , [TAction] -> [ThreadId] -> ThreadAction
STM [TAction]
trace [ThreadId]
woken
           , forall a b. a -> b -> a
const n ()
effect
           )
    Retry [TVarId]
touched -> do
      let threads' :: Threads n
threads' = forall (n :: * -> *).
HasCallStack =>
BlockedOn -> ThreadId -> Threads n -> Threads n
block ([TVarId] -> BlockedOn
OnTVar [TVarId]
touched) ThreadId
tid Threads n
cThreads
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads', cIdSource :: IdSource
cIdSource = IdSource
idSource'}
           , [TAction] -> ThreadAction
BlockedSTM [TAction]
trace
           , forall a b. a -> b -> a
const n ()
effect
           )
    Exception SomeException
e -> do
      (What n g, ThreadAction, Threads n -> n ())
res' <- forall (n :: * -> *) e g.
(MonadDejaFu n, Exception e) =>
(Maybe MaskingState -> ThreadAction)
-> ThreadId
-> e
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
stepThrow ([TAction] -> Maybe MaskingState -> ThreadAction
ThrownSTM [TAction]
trace) ThreadId
tid SomeException
e Context n g
ctx
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case (What n g, ThreadAction, Threads n -> n ())
res' of
        (Succeeded Context n g
ctx', ThreadAction
act, Threads n -> n ()
effect') -> (forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx' { cIdSource :: IdSource
cIdSource = IdSource
idSource' }, ThreadAction
act, Threads n -> n ()
effect')
        (Failed Condition
err, ThreadAction
act, Threads n -> n ()
effect') -> (forall (n :: * -> *) g. Condition -> What n g
Failed Condition
err, ThreadAction
act, Threads n -> n ()
effect')

-- lift an action from the underlying monad into the @Conc@
-- computation.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ALift n (Action n)
na) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  let effect :: Threads n -> n (Action n)
effect Threads n
threads = forall (n :: * -> *).
MonadDejaFu n =>
ThreadId -> Threads n -> n (Action n) -> n (Action n)
runLiftedAct ThreadId
tid Threads n
threads n (Action n)
na
  Action n
a <- Threads n -> n (Action n)
effect Threads n
cThreads
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
a ThreadId
tid Threads n
cThreads }
       , ThreadAction
LiftIO
       , forall (f :: * -> *) a. Functor f => f a -> f ()
void forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Threads n -> n (Action n)
effect
       )

-- throw an exception, and propagate it to the appropriate handler.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AThrow e
e) = forall (n :: * -> *) e g.
(MonadDejaFu n, Exception e) =>
(Maybe MaskingState -> ThreadAction)
-> ThreadId
-> e
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
stepThrow Maybe MaskingState -> ThreadAction
Throw ThreadId
tid e
e

-- throw an exception to the target thread, and propagate it to the
-- appropriate handler.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AThrowTo ThreadId
t e
e Action n
c) = forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised forall a b. (a -> b) -> a -> b
$ \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} ->
  let threads' :: Threads n
threads' = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid Threads n
cThreads
      blocked :: Threads n
blocked  = forall (n :: * -> *).
HasCallStack =>
BlockedOn -> ThreadId -> Threads n -> Threads n
block (ThreadId -> BlockedOn
OnMask ThreadId
t) ThreadId
tid Threads n
cThreads
  in case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ThreadId
t Threads n
cThreads of
       Just Thread n
thread
         | forall {n :: * -> *}. Thread n -> Bool
interruptible Thread n
thread Bool -> Bool -> Bool
|| ThreadId
t forall a. Eq a => a -> a -> Bool
== ThreadId
tid -> forall (n :: * -> *) e g.
(MonadDejaFu n, Exception e) =>
(Maybe MaskingState -> ThreadAction)
-> ThreadId
-> e
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
stepThrow (ThreadId -> Maybe MaskingState -> ThreadAction
ThrowTo ThreadId
t) ThreadId
t e
e Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads' }
         | Bool
otherwise -> forall (f :: * -> *) a. Applicative f => a -> f a
pure
           ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
blocked }
           , ThreadId -> ThreadAction
BlockedThrowTo ThreadId
t
           , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
           )
       Maybe (Thread n)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure
         (forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads' }
         , ThreadId -> Maybe MaskingState -> ThreadAction
ThrowTo ThreadId
t forall a. Maybe a
Nothing
         , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
         )

-- run a subcomputation in an exception-catching context.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ACatching e -> ModelConc n a
h ModelConc n a
ma a -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
  let a :: Action n
a     = forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc ModelConc n a
ma (forall (n :: * -> *). Action n -> Action n
APopCatching forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Action n
c)
      e :: e -> Action n
e e
exc = forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc (e -> ModelConc n a
h e
exc) a -> Action n
c
  in ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
a ThreadId
tid (forall e (n :: * -> *).
(Exception e, HasCallStack) =>
(e -> Action n) -> ThreadId -> Threads n -> Threads n
catching e -> Action n
e ThreadId
tid Threads n
cThreads) }
     , ThreadAction
Catching
     , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
     )

-- pop the top exception handler from the thread's stack.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (APopCatching Action n
a) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} ->
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
a ThreadId
tid (forall (n :: * -> *).
HasCallStack =>
ThreadId -> Threads n -> Threads n
uncatching ThreadId
tid Threads n
cThreads) }
       , ThreadAction
PopCatching
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- execute a subcomputation with a new masking state, and give it a
-- function to run a computation with the current masking state.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AMasking MaskingState
m (forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a
ma a -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
  let resetMask :: Bool -> MaskingState -> Program Basic n ()
resetMask Bool
typ MaskingState
ms = forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc forall a b. (a -> b) -> a -> b
$ \() -> Action n
k -> forall (n :: * -> *).
Bool -> Bool -> MaskingState -> Action n -> Action n
AResetMask Bool
typ Bool
True MaskingState
ms forall a b. (a -> b) -> a -> b
$ () -> Action n
k ()
      umask :: Program Basic n b -> Program Basic n b
umask Program Basic n b
mb = forall {n :: * -> *}. Bool -> MaskingState -> Program Basic n ()
resetMask Bool
True MaskingState
m' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Program Basic n b
mb forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b
b -> forall {n :: * -> *}. Bool -> MaskingState -> Program Basic n ()
resetMask Bool
False MaskingState
m forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure b
b
      m' :: MaskingState
m' = forall (n :: * -> *). Thread n -> MaskingState
_masking forall a b. (a -> b) -> a -> b
$ forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
tid Threads n
cThreads
      a :: Action n
a  = forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a
ma forall {n :: * -> *} {b}. Program Basic n b -> Program Basic n b
umask) (forall (n :: * -> *).
Bool -> Bool -> MaskingState -> Action n -> Action n
AResetMask Bool
False Bool
False MaskingState
m' forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Action n
c)
  in ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
a ThreadId
tid (forall (n :: * -> *).
HasCallStack =>
MaskingState -> ThreadId -> Threads n -> Threads n
mask MaskingState
m ThreadId
tid Threads n
cThreads) }
     , Bool -> MaskingState -> ThreadAction
SetMasking Bool
False MaskingState
m
     , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
     )

-- reset the masking thread of the state.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AResetMask Bool
b1 Bool
b2 MaskingState
m Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} ->
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid (forall (n :: * -> *).
HasCallStack =>
MaskingState -> ThreadId -> Threads n -> Threads n
mask MaskingState
m ThreadId
tid Threads n
cThreads) }
       , (if Bool
b1 then Bool -> MaskingState -> ThreadAction
SetMasking else Bool -> MaskingState -> ThreadAction
ResetMasking) Bool
b2 MaskingState
m
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- get the current masking state.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AGetMasking MaskingState -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
  let m :: MaskingState
m = forall (n :: * -> *). Thread n -> MaskingState
_masking forall a b. (a -> b) -> a -> b
$ forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
tid Threads n
cThreads
  in ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto (MaskingState -> Action n
c MaskingState
m) ThreadId
tid Threads n
cThreads }
     , MaskingState -> ThreadAction
GetMaskingState MaskingState
m
     , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
     )

-- execute a 'return' or 'pure'.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AReturn Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} ->
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid Threads n
cThreads }
       , ThreadAction
Return
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- kill the current thread.
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (AStop n ()
na) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} -> do
  n ()
na
  Threads n
threads' <- forall (n :: * -> *).
(MonadDejaFu n, HasCallStack) =>
ThreadId -> Threads n -> n (Threads n)
kill ThreadId
tid Threads n
cThreads
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
threads' }
       , ThreadAction
Stop
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- register an invariant to be checked in the next execution
stepThread Bool
_ Bool
_ Scheduler g
_ MemType
_ ThreadId
tid (ANewInvariant Invariant n ()
inv Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} ->
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx
         { cThreads :: Threads n
cThreads = forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid Threads n
cThreads
         , cNewInvariants :: [Invariant n ()]
cNewInvariants = Invariant n ()
inv forall a. a -> [a] -> [a]
: [Invariant n ()]
cNewInvariants
         }
       , ThreadAction
RegisterInvariant
       , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
       )

-- | Handle an exception being thrown from an @AAtom@, @AThrow@, or
-- @AThrowTo@.
stepThrow :: (MonadDejaFu n, Exception e)
  => (Maybe MaskingState -> ThreadAction)
  -- ^ Action to include in the trace.
  -> ThreadId
  -- ^ The thread receiving the exception.
  -> e
  -- ^ Exception to raise.
  -> Context n g
  -- ^ The execution context.
  -> n (What n g, ThreadAction, Threads n -> n ())
stepThrow :: forall (n :: * -> *) e g.
(MonadDejaFu n, Exception e) =>
(Maybe MaskingState -> ThreadAction)
-> ThreadId
-> e
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
stepThrow Maybe MaskingState -> ThreadAction
act ThreadId
tid e
e ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} = case forall (n :: * -> *).
HasCallStack =>
SomeException -> ThreadId -> Threads n -> Maybe (Threads n)
propagate SomeException
some ThreadId
tid Threads n
cThreads of
    Just Threads n
ts' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
ts' }
      , Maybe MaskingState -> ThreadAction
act (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *). Thread n -> MaskingState
_masking forall a b. (a -> b) -> a -> b
$ forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
tid Threads n
ts')
      , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
      )
    Maybe (Threads n)
Nothing
      | ThreadId
tid forall a. Eq a => a -> a -> Bool
== ThreadId
initialThread -> forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall (n :: * -> *) g. Condition -> What n g
Failed (SomeException -> Condition
UncaughtException SomeException
some)
        , Maybe MaskingState -> ThreadAction
act forall a. Maybe a
Nothing
        , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
        )
      | Bool
otherwise -> do
          Threads n
ts' <- forall (n :: * -> *).
(MonadDejaFu n, HasCallStack) =>
ThreadId -> Threads n -> n (Threads n)
kill ThreadId
tid Threads n
cThreads
          forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads :: Threads n
cThreads = Threads n
ts' }
               , Maybe MaskingState -> ThreadAction
act forall a. Maybe a
Nothing
               , forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
               )
  where
    some :: SomeException
some = forall e. Exception e => e -> SomeException
toException e
e

-- | Helper for actions impose a write barrier.
synchronised :: MonadDejaFu n
  => (Context n g -> n x)
  -- ^ Action to run after the write barrier.
  -> Context n g
  -- ^ The original execution context.
  -> n x
synchronised :: forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised Context n g -> n x
ma ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cCState :: ConcurrencyState
cNewInvariants :: [Invariant n ()]
cInvariants :: InvariantContext n
cCaps :: Int
cWriteBuf :: WriteBuffer n
cThreads :: Threads n
cIdSource :: IdSource
cSchedState :: g
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cSchedState :: forall (n :: * -> *) g. Context n g -> g
..} = do
  forall (n :: * -> *). MonadDejaFu n => WriteBuffer n -> n ()
writeBarrier WriteBuffer n
cWriteBuf
  Context n g -> n x
ma Context n g
ctx { cWriteBuf :: WriteBuffer n
cWriteBuf = forall (n :: * -> *). WriteBuffer n
emptyBuffer }

--------------------------------------------------------------------------------
-- * Invariants

-- | The state of the invariants
data InvariantContext n = InvariantContext
  { forall (n :: * -> *). InvariantContext n -> [Invariant n ()]
icActive  :: [Invariant n ()]
  , forall (n :: * -> *).
InvariantContext n
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
icBlocked :: [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
  }

-- | @unblockInvariants act@ unblocks every invariant which could have
-- its result changed by @act@.
unblockInvariants ::  ThreadAction -> InvariantContext n -> InvariantContext n
unblockInvariants :: forall (n :: * -> *).
ThreadAction -> InvariantContext n -> InvariantContext n
unblockInvariants ThreadAction
act InvariantContext n
ic = forall (n :: * -> *).
[Invariant n ()]
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
-> InvariantContext n
InvariantContext [Invariant n ()]
active [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
blocked where
  active :: [Invariant n ()]
active = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
unblocked forall a. [a] -> [a] -> [a]
++ forall (n :: * -> *). InvariantContext n -> [Invariant n ()]
icActive InvariantContext n
ic

  ([(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
unblocked, [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
blocked) = (forall a. (a -> Bool) -> [a] -> ([a], [a])
`partition` forall (n :: * -> *).
InvariantContext n
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
icBlocked InvariantContext n
ic) forall a b. (a -> b) -> a -> b
$
    \(Invariant n ()
_, ([IORefId]
ioridsB, [MVarId]
mvidsB, [TVarId]
tvidsB)) ->
      forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [IORefId]
ioridsB) (ActionType -> Maybe IORefId
iorefOf (ThreadAction -> ActionType
simplifyAction ThreadAction
act)) Bool -> Bool -> Bool
||
      forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MVarId]
mvidsB)  (ActionType -> Maybe MVarId
mvarOf (ThreadAction -> ActionType
simplifyAction ThreadAction
act))  Bool -> Bool -> Bool
||
      forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TVarId]
tvidsB) (ThreadAction -> Set TVarId
tvarsOf ThreadAction
act)

-- | Check all active invariants, returning an arbitrary failure if
-- multiple ones fail.
checkInvariants :: MonadDejaFu n
  => InvariantContext n
  -> n (Either E.SomeException (InvariantContext n))
checkInvariants :: forall (n :: * -> *).
MonadDejaFu n =>
InvariantContext n -> n (Either SomeException (InvariantContext n))
checkInvariants InvariantContext n
ic = forall {m :: * -> *} {a}.
MonadDejaFu m =>
[Invariant m a]
-> m (Either
        SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
go (forall (n :: * -> *). InvariantContext n -> [Invariant n ()]
icActive InvariantContext n
ic) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
blocked -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall (n :: * -> *).
[Invariant n ()]
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
-> InvariantContext n
InvariantContext [] ([(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
blocked forall a. [a] -> [a] -> [a]
++ forall (n :: * -> *).
InvariantContext n
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
icBlocked InvariantContext n
ic)))
    Left SomeException
exc -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left SomeException
exc)
  where
    go :: [Invariant m a]
-> m (Either
        SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
go (Invariant m a
inv:[Invariant m a]
is) = forall (n :: * -> *) a.
MonadDejaFu n =>
Invariant n a
-> n (Either SomeException ([IORefId], [MVarId], [TVarId]))
checkInvariant Invariant m a
inv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right ([IORefId], [MVarId], [TVarId])
o -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Invariant m a
inv,([IORefId], [MVarId], [TVarId])
o)forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Invariant m a]
-> m (Either
        SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
go [Invariant m a]
is
      Left SomeException
exc -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left SomeException
exc)
    go [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right [])

-- | Check an invariant.
checkInvariant :: MonadDejaFu n
  => Invariant n a
  -> n (Either E.SomeException ([IORefId], [MVarId], [TVarId]))
checkInvariant :: forall (n :: * -> *) a.
MonadDejaFu n =>
Invariant n a
-> n (Either SomeException ([IORefId], [MVarId], [TVarId]))
checkInvariant Invariant n a
inv = forall (n :: * -> *) a.
MonadDejaFu n =>
Invariant n a
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
doInvariant Invariant n a
inv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  (Right a
_, [IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right ([IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars))
  (Left SomeException
exc, [IORefId]
_, [MVarId]
_, [TVarId]
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left SomeException
exc)

-- | Run an invariant (more primitive)
doInvariant :: MonadDejaFu n
  => Invariant n a
  -> n (Either E.SomeException a, [IORefId], [MVarId], [TVarId])
doInvariant :: forall (n :: * -> *) a.
MonadDejaFu n =>
Invariant n a
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
doInvariant Invariant n a
inv = do
    (IAction n
c, Ref n (Maybe (Either SomeException a))
ref) <- forall (n :: * -> *) x a b.
MonadDejaFu n =>
(n () -> x)
-> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref n (Maybe b))
runRefCont forall (n :: * -> *). n () -> IAction n
IStop (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right) (forall (n :: * -> *) a.
Invariant n a -> (a -> IAction n) -> IAction n
runInvariant Invariant n a
inv)
    ([IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars) <- forall {m :: * -> *} {b}.
MonadDejaFu m =>
Ref m (Maybe (Either SomeException b))
-> IAction m
-> [IORefId]
-> [MVarId]
-> [TVarId]
-> m ([IORefId], [MVarId], [TVarId])
go Ref n (Maybe (Either SomeException a))
ref IAction n
c [] [] []
    Maybe (Either SomeException a)
val <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe (Either SomeException a))
ref
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. HasCallStack => Maybe a -> a
efromJust Maybe (Either SomeException a)
val, forall a. Eq a => [a] -> [a]
nub [IORefId]
iorefs, forall a. Eq a => [a] -> [a]
nub [MVarId]
mvars, forall a. Eq a => [a] -> [a]
nub [TVarId]
tvars)
  where
    go :: Ref m (Maybe (Either SomeException b))
-> IAction m
-> [IORefId]
-> [MVarId]
-> [TVarId]
-> m ([IORefId], [MVarId], [TVarId])
go Ref m (Maybe (Either SomeException b))
ref IAction m
act [IORefId]
iorefs [MVarId]
mvars [TVarId]
tvars = do
      (Either SomeException (Maybe (IAction m))
res, [IORefId]
iorefs', [MVarId]
mvars', [TVarId]
tvars') <- forall (n :: * -> *).
MonadDejaFu n =>
IAction n
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
stepInvariant IAction m
act
      let newIORefs :: [IORefId]
newIORefs = [IORefId]
iorefs' forall a. [a] -> [a] -> [a]
++ [IORefId]
iorefs
      let newMVars :: [MVarId]
newMVars  = [MVarId]
mvars'  forall a. [a] -> [a] -> [a]
++ [MVarId]
mvars
      let newTVars :: [TVarId]
newTVars  = [TVarId]
tvars'  forall a. [a] -> [a] -> [a]
++ [TVarId]
tvars
      case Either SomeException (Maybe (IAction m))
res of
        Right (Just IAction m
act') ->
          Ref m (Maybe (Either SomeException b))
-> IAction m
-> [IORefId]
-> [MVarId]
-> [TVarId]
-> m ([IORefId], [MVarId], [TVarId])
go Ref m (Maybe (Either SomeException b))
ref IAction m
act' [IORefId]
newIORefs [MVarId]
newMVars [TVarId]
newTVars
        Right Maybe (IAction m)
Nothing ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure ([IORefId]
newIORefs, [MVarId]
newMVars, [TVarId]
newTVars)
        Left SomeException
exc -> do
          forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref m (Maybe (Either SomeException b))
ref (forall a. a -> Maybe a
Just (forall a b. a -> Either a b
Left SomeException
exc))
          forall (f :: * -> *) a. Applicative f => a -> f a
pure ([IORefId]
newIORefs, [MVarId]
newMVars, [TVarId]
newTVars)

-- | Run an invariant for one step
stepInvariant :: MonadDejaFu n
  => IAction n
  -> n (Either E.SomeException (Maybe (IAction n)), [IORefId], [MVarId], [TVarId])
stepInvariant :: forall (n :: * -> *).
MonadDejaFu n =>
IAction n
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
stepInvariant (IInspectIORef ioref :: ModelIORef n a
ioref@ModelIORef{IORefId
Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
iorefId :: IORefId
iorefRef :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
..} a -> IAction n
k) = do
  a
a <- forall (n :: * -> *) a. MonadDejaFu n => ModelIORef n a -> n a
readIORefGlobal ModelIORef n a
ioref
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall a. a -> Maybe a
Just (a -> IAction n
k a
a)), [IORefId
iorefId], [], [])
stepInvariant (IInspectMVar ModelMVar{MVarId
Ref n (Maybe a)
mvarRef :: Ref n (Maybe a)
mvarId :: MVarId
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
..} Maybe a -> IAction n
k) = do
  Maybe a
a <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe a)
mvarRef
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall a. a -> Maybe a
Just (Maybe a -> IAction n
k Maybe a
a)), [], [MVarId
mvarId], [])
stepInvariant (IInspectTVar ModelTVar{TVarId
Ref n a
tvarRef :: forall (n :: * -> *) a. ModelTVar n a -> Ref n a
tvarId :: forall (n :: * -> *) a. ModelTVar n a -> TVarId
tvarRef :: Ref n a
tvarId :: TVarId
..} a -> IAction n
k) = do
  a
a <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n a
tvarRef
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall a. a -> Maybe a
Just (a -> IAction n
k a
a)), [], [], [TVarId
tvarId])
stepInvariant (ICatch e -> Invariant n a
h Invariant n a
nx a -> IAction n
k) = forall (n :: * -> *) a.
MonadDejaFu n =>
Invariant n a
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
doInvariant Invariant n a
nx forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  (Right a
a, [IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars) ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall a. a -> Maybe a
Just (a -> IAction n
k a
a)), [IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars)
  (Left SomeException
exc, [IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars) -> case forall e. Exception e => SomeException -> Maybe e
E.fromException SomeException
exc of
    Just e
exc' -> forall (n :: * -> *) a.
MonadDejaFu n =>
Invariant n a
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
doInvariant (e -> Invariant n a
h e
exc') forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      (Right a
a, [IORefId]
iorefs', [MVarId]
mvars', [TVarId]
tvars') ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall a. a -> Maybe a
Just (a -> IAction n
k a
a)), [IORefId]
iorefs' forall a. [a] -> [a] -> [a]
++ [IORefId]
iorefs, [MVarId]
mvars' forall a. [a] -> [a] -> [a]
++ [MVarId]
mvars, [TVarId]
tvars' forall a. [a] -> [a] -> [a]
++ [TVarId]
tvars)
      (Left SomeException
exc'', [IORefId]
iorefs', [MVarId]
mvars', [TVarId]
tvars') ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left SomeException
exc'', [IORefId]
iorefs' forall a. [a] -> [a] -> [a]
++ [IORefId]
iorefs, [MVarId]
mvars' forall a. [a] -> [a] -> [a]
++ [MVarId]
mvars, [TVarId]
tvars' forall a. [a] -> [a] -> [a]
++ [TVarId]
tvars)
    Maybe e
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left SomeException
exc, [IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars)
stepInvariant (IThrow e
exc) =
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left (forall e. Exception e => e -> SomeException
toException e
exc), [], [], [])
stepInvariant (IStop n ()
finalise) = do
  n ()
finalise
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right forall a. Maybe a
Nothing, [], [], [])