{-# 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       = Threads n
forall k a. Map k a
M.empty
                    , cWriteBuf :: WriteBuffer n
cWriteBuf      = WriteBuffer n
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) <- (n () -> Action n)
-> (a -> Maybe (Either Condition a))
-> ((a -> Action n) -> Action n)
-> n (Action n, Ref n (Maybe (Either Condition a)))
forall (n :: * -> *) x a b.
MonadDejaFu n =>
(n () -> x)
-> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref n (Maybe b))
runRefCont n () -> Action n
forall (n :: * -> *). n () -> Action n
AStop (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just (Either Condition a -> Maybe (Either Condition a))
-> (a -> Either Condition a) -> a -> Maybe (Either Condition a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either Condition a
forall a b. b -> Either a b
Right) (ModelConc n a -> (a -> Action n) -> Action n
forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc ModelConc n a
ma)
  let threads0 :: Threads n
threads0 = MaskingState
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
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) (Context n g -> Threads n
forall (n :: * -> *) g. Context n g -> Threads n
cThreads Context n g
ctx)
  Threads n
threads <- case Maybe (n (BoundThread n (Action n)))
forall a. Maybe (n (BoundThread n a))
forall (m :: * -> *) a.
MonadDejaFu m =>
Maybe (m (BoundThread m a))
forkBoundThread of
    Just n (BoundThread n (Action n))
fbt -> n (BoundThread n (Action n))
-> ThreadId -> Threads n -> n (Threads n)
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  -> Threads n -> n (Threads n)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Threads n
threads0
  CResult n g a
res <- Bool
-> Scheduler g
-> MemType
-> Ref n (Maybe (Either Condition a))
-> Context n g
-> n (CResult n g a)
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 }
  Context n g -> n ()
forall (n :: * -> *) g.
(MonadDejaFu n, HasCallStack) =>
Context n g -> n ()
killAllThreads (CResult n g a -> Context n g
forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext CResult n g a
res)
  CResult n g a -> n (CResult n g a)
forall a. a -> n a
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) <- (n () -> Action n)
-> (a -> Maybe (Either Condition a))
-> ((a -> Action n) -> Action n)
-> n (Action n, Ref n (Maybe (Either Condition a)))
forall (n :: * -> *) x a b.
MonadDejaFu n =>
(n () -> x)
-> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref n (Maybe b))
runRefCont n () -> Action n
forall (n :: * -> *). n () -> Action n
AStop (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just (Either Condition a -> Maybe (Either Condition a))
-> (a -> Either Condition a) -> a -> Maybe (Either Condition a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either Condition a
forall a b. b -> Either a b
Right) (ModelConc n a -> (a -> Action n) -> Action n
forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc ModelConc n a
ma)
  let threads0 :: Threads n
threads0 = ThreadId -> Threads n -> Threads n
forall k a. Ord k => k -> Map k a -> Map k a
M.delete ThreadId
initialThread (Context n g -> Threads n
forall (n :: * -> *) g. Context n g -> Threads n
cThreads Context n g
ctx)
  let threads1 :: Threads n
threads1 = MaskingState
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
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 Maybe (n (BoundThread n (Action n)))
forall a. Maybe (n (BoundThread n a))
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 = (Thread n -> Bool) -> Threads n -> Threads n
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Maybe (BoundThread n (Action n)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (BoundThread n (Action n)) -> Bool)
-> (Thread n -> Maybe (BoundThread n (Action n)))
-> Thread n
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thread n -> Maybe (BoundThread n (Action n))
forall (n :: * -> *). Thread n -> Maybe (BoundThread n (Action n))
_bound) Threads n
threads1
      Threads n
threads' <- n (BoundThread n (Action n))
-> ThreadId -> Threads n -> n (Threads n)
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
      (ThreadId -> Threads n -> n (Threads n))
-> Threads n -> [ThreadId] -> n (Threads n)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (n (BoundThread n (Action n))
-> ThreadId -> Threads n -> n (Threads n)
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' (Threads n -> [ThreadId]
forall k a. Map k a -> [k]
M.keys Threads n
boundThreads)
    Maybe (n (BoundThread n (Action n)))
Nothing -> Threads n -> n (Threads n)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Threads n
threads1
  Threads n -> n ()
restore Threads n
threads
  CResult n g a
res <- Bool
-> Scheduler g
-> MemType
-> Ref n (Maybe (Either Condition a))
-> Context n g
-> n (CResult n g a)
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 }
  Context n g -> n ()
forall (n :: * -> *) g.
(MonadDejaFu n, HasCallStack) =>
Context n g -> n ()
killAllThreads (CResult n g a -> Context n g
forall (n :: * -> *) g a. CResult n g a -> Context n g
finalContext CResult n g a
res)
  CResult n g a -> n (CResult n g a)
forall a. a -> n a
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 = Context n g -> Threads n
forall (n :: * -> *) g. Context n g -> Threads n
cThreads Context n g
ctx
  in (ThreadId -> n (Threads n)) -> [ThreadId] -> n ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ThreadId -> Threads n -> n (Threads n)
forall (n :: * -> *).
(MonadDejaFu n, HasCallStack) =>
ThreadId -> Threads n -> n (Threads n)
`kill` Threads n
finalThreads) (Threads n -> [ThreadId]
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)
forall {n :: * -> *}.
(Ref n ~ Ref n, MonadDejaFu n) =>
(Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
schedule (n () -> Map ThreadId (Thread n) -> n ()
forall a b. a -> b -> a
const (n () -> Map ThreadId (Thread n) -> n ())
-> n () -> Map ThreadId (Thread n) -> n ()
forall a b. (a -> b) -> a -> b
$ () -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) SeqTrace
forall a. Seq a
Seq.empty Maybe (ThreadId, ThreadAction)
forall a. Maybe a
Nothing where
  -- signal failure & terminate
  die :: Condition
-> (Threads n -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> m (CResult n g a)
die Condition
reason Threads n -> n ()
finalR SeqTrace
finalT Maybe (ThreadId, ThreadAction)
finalD Context n g
finalC = do
    Ref m (Maybe (Either Condition a))
-> Maybe (Either Condition a) -> m ()
forall a. Ref m a -> a -> m ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Maybe (Either Condition a))
Ref m (Maybe (Either Condition a))
ref (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just (Either Condition a -> Maybe (Either Condition a))
-> Either Condition a -> Maybe (Either Condition a)
forall a b. (a -> b) -> a -> b
$ Condition -> Either Condition a
forall a b. a -> Either a b
Left Condition
reason)
    (Threads n -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> m (CResult n g a)
forall {n :: * -> *} {f :: * -> *} {g}.
(Ref n ~ Ref n, Applicative f) =>
(Threads n -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> f (CResult n g a)
stop Threads 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 :: (Threads n -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> f (CResult n g a)
stop Threads n -> n ()
finalR SeqTrace
finalT Maybe (ThreadId, ThreadAction)
finalD Context n g
finalC = CResult n g a -> f (CResult n g a)
forall a. a -> f a
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 n (Maybe (Either Condition a))
ref
    , finalRestore :: Threads n -> n ()
finalRestore  = Threads 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  = (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
forall {n :: * -> *} {f :: * -> *} {g}.
(Ref n ~ Ref n, Applicative f) =>
(Threads 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  = Condition
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
forall {m :: * -> *} {n :: * -> *} {g}.
(Ref m ~ Ref n, Ref n ~ Ref n, MonadDejaFu m) =>
Condition
-> (Threads n -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> m (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' }
      in case Maybe ThreadId
choice of
           Just ThreadId
chosen -> case ThreadId -> Map ThreadId (Thread n) -> Maybe (Thread n)
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
               | Thread n -> Bool
forall {n :: * -> *}. Thread n -> Bool
isBlocked Thread n
thread -> Error -> n (CResult n g a)
forall e a. (HasCallStack, Exception e) => e -> n a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
E.throwM Error
ScheduledBlockedThread
               | Bool
otherwise ->
                 let decision :: Decision
decision
                       | ThreadId -> Maybe ThreadId
forall a. a -> Maybe a
Just ThreadId
chosen Maybe ThreadId -> Maybe ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ((ThreadId, ThreadAction) -> ThreadId
forall a b. (a, b) -> a
fst ((ThreadId, ThreadAction) -> ThreadId)
-> Maybe (ThreadId, ThreadAction) -> Maybe ThreadId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ThreadId, ThreadAction)
prior) = Decision
Continue
                       | ((ThreadId, ThreadAction) -> ThreadId
forall a b. (a, b) -> a
fst ((ThreadId, ThreadAction) -> ThreadId)
-> Maybe (ThreadId, ThreadAction) -> Maybe ThreadId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ThreadId, ThreadAction)
prior) Maybe ThreadId -> [Maybe ThreadId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((ThreadId, Lookahead) -> Maybe ThreadId)
-> [(ThreadId, Lookahead)] -> [Maybe ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (ThreadId -> Maybe ThreadId
forall a. a -> Maybe a
Just (ThreadId -> Maybe ThreadId)
-> ((ThreadId, Lookahead) -> ThreadId)
-> (ThreadId, Lookahead)
-> Maybe ThreadId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ThreadId, Lookahead) -> ThreadId
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 = ((ThreadId, Lookahead) -> Bool)
-> [(ThreadId, Lookahead)] -> [(ThreadId, Lookahead)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(ThreadId
t, Lookahead
_) -> ThreadId
t ThreadId -> ThreadId -> Bool
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 -> Error -> n (CResult n g a)
forall e a. (HasCallStack, Exception e) => e -> n a
forall (m :: * -> *) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> m a
E.throwM Error
ScheduledMissingThread
           Maybe ThreadId
Nothing -> Condition
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
forall {m :: * -> *} {n :: * -> *} {g}.
(Ref m ~ Ref n, Ref n ~ Ref n, MonadDejaFu m) =>
Condition
-> (Threads n -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> m (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')  = Scheduler g
-> Maybe (ThreadId, ThreadAction)
-> NonEmpty (ThreadId, Lookahead)
-> ConcurrencyState
-> g
-> (Maybe ThreadId, g)
forall state.
Scheduler state
-> Maybe (ThreadId, ThreadAction)
-> NonEmpty (ThreadId, Lookahead)
-> ConcurrencyState
-> state
-> (Maybe ThreadId, state)
scheduleThread Scheduler g
sched Maybe (ThreadId, ThreadAction)
prior ([(ThreadId, Lookahead)] -> NonEmpty (ThreadId, Lookahead)
forall a. HasCallStack => [a] -> NonEmpty a
efromList [(ThreadId, Lookahead)]
runnable') (Context n g -> ConcurrencyState
forall (n :: * -> *) g. Context n g -> ConcurrencyState
cCState Context n g
ctx) (Context n g -> g
forall (n :: * -> *) g. Context n g -> g
cSchedState Context n g
ctx)
      runnable' :: [(ThreadId, Lookahead)]
runnable'     = [(ThreadId
t, Action n -> Lookahead
forall (n :: * -> *). Action n -> Lookahead
lookahead (Thread n -> Action n
forall (n :: * -> *). Thread n -> Action n
_continuation Thread n
a)) | (ThreadId
t, Thread n
a) <- ((ThreadId, Thread n) -> ThreadId)
-> [(ThreadId, Thread n)] -> [(ThreadId, Thread n)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (ThreadId, Thread n) -> ThreadId
forall a b. (a, b) -> a
fst ([(ThreadId, Thread n)] -> [(ThreadId, Thread n)])
-> [(ThreadId, Thread n)] -> [(ThreadId, Thread n)]
forall a b. (a -> b) -> a -> b
$ Map ThreadId (Thread n) -> [(ThreadId, Thread n)]
forall k a. Map k a -> [(k, a)]
M.assocs Map ThreadId (Thread n)
runnable]
      runnable :: Map ThreadId (Thread n)
runnable      = (Thread n -> Bool)
-> Map ThreadId (Thread n) -> Map ThreadId (Thread n)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Bool -> Bool
not (Bool -> Bool) -> (Thread n -> Bool) -> Thread n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thread n -> Bool
forall {n :: * -> *}. Thread n -> Bool
isBlocked) Map ThreadId (Thread n)
threadsc
      threadsc :: Map ThreadId (Thread n)
threadsc      = WriteBuffer n -> Map ThreadId (Thread n) -> Map ThreadId (Thread n)
forall (n :: * -> *). WriteBuffer n -> Threads n -> Threads n
addCommitThreads (Context n g -> WriteBuffer n
forall (n :: * -> *) g. Context n g -> WriteBuffer n
cWriteBuf Context n g
ctx) Map ThreadId (Thread n)
threads
      threads :: Map ThreadId (Thread n)
threads       = Context n g -> Map ThreadId (Thread n)
forall (n :: * -> *) g. Context n g -> Threads n
cThreads Context n g
ctx
      isBlocked :: Thread n -> Bool
isBlocked     = Maybe BlockedOn -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BlockedOn -> Bool)
-> (Thread n -> Maybe BlockedOn) -> Thread n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thread n -> Maybe BlockedOn
forall (n :: * -> *). Thread n -> Maybe BlockedOn
_blocking
      isTerminated :: Bool
isTerminated  = ThreadId
initialThread ThreadId -> [ThreadId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map ThreadId (Thread n) -> [ThreadId]
forall k a. Map k a -> [k]
M.keys Map ThreadId (Thread n)
threads
      isDeadlocked :: Bool
isDeadlocked  = Map ThreadId (Thread n) -> Bool
forall k a. Map k a -> Bool
M.null ((Thread n -> Bool)
-> Map ThreadId (Thread n) -> Map ThreadId (Thread n)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Bool -> Bool
not (Bool -> Bool) -> (Thread n -> Bool) -> Thread n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thread n -> Bool
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) <- Bool
-> Bool
-> Scheduler g
-> MemType
-> ThreadId
-> Action n
-> Context n g
-> n (What n g, ThreadAction, Map ThreadId (Thread n) -> n ())
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
          (Maybe (ThreadId, ThreadAction) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (ThreadId, ThreadAction)
prior)
          Scheduler g
sched
          MemType
memtype
          ThreadId
chosen
          (Thread n -> Action n
forall (n :: * -> *). Thread n -> Action n
_continuation Thread n
thread)
          Context n g
ctx
      let sofar' :: SeqTrace
sofar' = SeqTrace
sofar SeqTrace -> SeqTrace -> SeqTrace
forall a. Semigroup a => a -> a -> a
<> ThreadAction -> SeqTrace
forall {c}. c -> Seq (Decision, [(ThreadId, Lookahead)], c)
getTrc ThreadAction
actOrTrc
      let prior' :: Maybe (ThreadId, ThreadAction)
prior' = ThreadAction -> Maybe (ThreadId, ThreadAction)
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' n () -> n () -> n ()
forall a b. n a -> n b -> n b
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' = MemType
-> ThreadId
-> ThreadAction
-> What n g
-> Context n g
-> Context n g
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
_ -> InvariantContext n -> n (Either SomeException (InvariantContext n))
forall (n :: * -> *).
MonadDejaFu n =>
InvariantContext n -> n (Either SomeException (InvariantContext n))
checkInvariants (Context n g -> InvariantContext n
forall (n :: * -> *) g. Context n g -> InvariantContext n
cInvariants Context n g
ctx') n (Either SomeException (InvariantContext n))
-> (Either SomeException (InvariantContext n) -> n (CResult n g a))
-> n (CResult n g a)
forall a b. n a -> (a -> n b) -> n b
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 = ic }
          Left SomeException
exc ->
            Condition
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
forall {m :: * -> *} {n :: * -> *} {g}.
(Ref m ~ Ref n, Ref n ~ Ref n, MonadDejaFu m) =>
Condition
-> (Threads n -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> m (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 ->
          Condition
-> (Map ThreadId (Thread n) -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> n (CResult n g a)
forall {m :: * -> *} {n :: * -> *} {g}.
(Ref m ~ Ref n, Ref n ~ Ref n, MonadDejaFu m) =>
Condition
-> (Threads n -> n ())
-> SeqTrace
-> Maybe (ThreadId, ThreadAction)
-> Context n g
-> m (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 = (Decision, [(ThreadId, Lookahead)], c)
-> Seq (Decision, [(ThreadId, Lookahead)], c)
forall a. a -> Seq a
Seq.singleton (Decision
decision, [(ThreadId, Lookahead)]
alternatives, c
a)

      getPrior :: b -> Maybe (ThreadId, b)
getPrior b
a = (ThreadId, b) -> Maybe (ThreadId, b)
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 = Context n g -> Context n g
forall {n :: * -> *} {g}. Context n g -> Context n g
fixContextCommon (Context n g -> Context n g) -> Context n g -> Context n g
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> Context n g
ctx
      { cThreads =
          if (interruptible <$> M.lookup tid cThreads) /= Just False
          then unblockWaitingOn tid cThreads
          else 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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} = Context n g
ctx
    { cThreads    = delCommitThreads cThreads
    , cInvariants = unblockInvariants act cInvariants
    , cCState     = updateCState memtype cCState tid 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 = (Thread n -> Thread n)
-> Map ThreadId (Thread n) -> Map ThreadId (Thread n)
forall a b. (a -> b) -> Map ThreadId a -> Map ThreadId b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Thread n -> Thread n)
 -> Map ThreadId (Thread n) -> Map ThreadId (Thread n))
-> (Thread n -> Thread n)
-> Map ThreadId (Thread n)
-> Map ThreadId (Thread n)
forall a b. (a -> b) -> a -> b
$ \Thread n
thread -> case Thread n -> Maybe BlockedOn
forall (n :: * -> *). Thread n -> Maybe BlockedOn
_blocking Thread n
thread of
  Just (OnMask ThreadId
t) | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid -> Thread n
thread { _blocking = 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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((What n g, ThreadAction, Threads n -> n ())
 -> n (What n g, ThreadAction, Threads n -> n ()))
-> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
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' = ThreadId
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
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 ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (b newtid) tid threads', cIdSource = idSource' }
     , ThreadId -> ThreadAction
Fork ThreadId
newtid
     , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> case Maybe (n (BoundThread n (Action n)))
forall a. Maybe (n (BoundThread n a))
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' = ThreadId
-> ThreadId
-> ((forall b. ModelConc n b -> ModelConc n b) -> Action n)
-> Threads n
-> Threads n
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'' <- n (BoundThread n (Action n))
-> ThreadId -> Threads n -> n (Threads n)
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'
    (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (b newtid) tid threads'', cIdSource = idSource' }
         , ThreadId -> ThreadAction
ForkOS ThreadId
newtid
         , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
         )
  Maybe (n (BoundThread n (Action n)))
Nothing ->
    (Maybe MaskingState -> ThreadAction)
-> ThreadId
-> MonadFailException
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  let sbt :: Bool
sbt = Maybe (n (BoundThread n ())) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (n (BoundThread n ()))
forall a. Maybe (n (BoundThread n a))
forall (m :: * -> *) a.
MonadDejaFu m =>
Maybe (m (BoundThread m a))
forkBoundThread :: Maybe (n (BoundThread n ())))
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c sbt) tid cThreads }
       , Bool -> ThreadAction
SupportsBoundThreads Bool
sbt
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  let isBound :: Bool
isBound = Maybe (BoundThread n (Action n)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (BoundThread n (Action n)) -> Bool)
-> (Thread n -> Maybe (BoundThread n (Action n)))
-> Thread n
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thread n -> Maybe (BoundThread n (Action n))
forall (n :: * -> *). Thread n -> Maybe (BoundThread n (Action n))
_bound (Thread n -> Bool) -> Thread n -> Bool
forall a b. (a -> b) -> a -> b
$ ThreadId -> Threads n -> Thread n
forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
tid Threads n
cThreads
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c isBound) tid cThreads }
       , Bool -> ThreadAction
IsCurrentThreadBound Bool
isBound
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} ->
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c tid) tid cThreads }
       , ThreadAction
MyThreadId
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} ->
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c cCaps) tid cThreads }
       , Int -> ThreadAction
GetNumCapabilities Int
cCaps
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} ->
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto c tid cThreads, cCaps = i }
       , Int -> ThreadAction
SetNumCapabilities Int
i
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} ->
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto c tid cThreads }
       , ThreadAction
Yield
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} ->
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto c tid cThreads }
       , Int -> ThreadAction
ThreadDelay Int
n
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  let (IdSource
idSource', MVarId
newmvid) = String -> IdSource -> (IdSource, MVarId)
nextMVId String
n IdSource
cIdSource
  Ref n (Maybe a)
ref <- Maybe a -> n (Ref n (Maybe a))
forall a. a -> n (Ref n a)
forall (m :: * -> *) a. MonadDejaFu m => a -> m (Ref m a)
newRef Maybe a
forall a. Maybe a
Nothing
  let mvar :: ModelMVar n a
mvar = MVarId -> Ref n (Maybe a) -> ModelMVar n a
forall (n :: * -> *) a. MVarId -> Ref n (Maybe a) -> ModelMVar n a
ModelMVar MVarId
newmvid Ref n (Maybe a)
ref
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c mvar) tid cThreads, cIdSource = idSource' }
       , MVarId -> ThreadAction
NewMVar MVarId
newmvid
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (Ref n (Maybe a) -> Maybe a -> n ()
forall a. Ref n a -> a -> n ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Maybe a)
ref Maybe a
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)
mvarId :: MVarId
mvarRef :: Ref n (Maybe a)
mvarRef :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
..} a
a Action n
c) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
woken, n ()
effect) <- ModelMVar n a
-> a
-> Action n
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
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
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = threads' }
       , if Bool
success then MVarId -> [ThreadId] -> ThreadAction
PutMVar MVarId
mvarId [ThreadId]
woken else MVarId -> ThreadAction
BlockedPutMVar MVarId
mvarId
       , n () -> Threads n -> n ()
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 :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
mvarId :: MVarId
mvarRef :: Ref n (Maybe a)
..} a
a Bool -> Action n
c) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
woken, n ()
effect) <- ModelMVar n a
-> a
-> (Bool -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
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
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = threads' }
       , MVarId -> Bool -> [ThreadId] -> ThreadAction
TryPutMVar MVarId
mvarId Bool
success [ThreadId]
woken
       , n () -> Threads n -> n ()
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 :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
mvarId :: MVarId
mvarRef :: Ref n (Maybe a)
..} a -> Action n
c) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
_, n ()
_) <- ModelMVar n a
-> (a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [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
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = threads' }
       , if Bool
success then MVarId -> ThreadAction
ReadMVar MVarId
mvarId else MVarId -> ThreadAction
BlockedReadMVar MVarId
mvarId
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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 :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
mvarId :: MVarId
mvarRef :: Ref n (Maybe a)
..} Maybe a -> Action n
c) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
_, n ()
_) <- ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [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
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = threads' }
       , MVarId -> Bool -> ThreadAction
TryReadMVar MVarId
mvarId Bool
success
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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 :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
mvarId :: MVarId
mvarRef :: Ref n (Maybe a)
..} a -> Action n
c) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
woken, n ()
effect) <- ModelMVar n a
-> (a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
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
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = threads' }
       , if Bool
success then MVarId -> [ThreadId] -> ThreadAction
TakeMVar MVarId
mvarId [ThreadId]
woken else MVarId -> ThreadAction
BlockedTakeMVar MVarId
mvarId
       , n () -> Threads n -> n ()
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 :: forall (n :: * -> *) a. ModelMVar n a -> Ref n (Maybe a)
mvarId :: forall (n :: * -> *) a. ModelMVar n a -> MVarId
mvarId :: MVarId
mvarRef :: Ref n (Maybe a)
..} Maybe a -> Action n
c) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  (Bool
success, Threads n
threads', [ThreadId]
woken, n ()
effect) <- ModelMVar n a
-> (Maybe a -> Action n)
-> ThreadId
-> Threads n
-> n (Bool, Threads n, [ThreadId], n ())
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
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = threads' }
       , MVarId -> Bool -> [ThreadId] -> ThreadAction
TryTakeMVar MVarId
mvarId Bool
success [ThreadId]
woken
       , n () -> Threads n -> n ()
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  let (IdSource
idSource', IORefId
newiorid) = String -> IdSource -> (IdSource, IORefId)
nextIORId String
n IdSource
cIdSource
  let val :: (Map k a, Integer, a)
val = (Map k a
forall k a. Map k a
M.empty, Integer
0, a
a)
  Ref n (Map ThreadId a, Integer, a)
ioref <- (Map ThreadId a, Integer, a)
-> n (Ref n (Map ThreadId a, Integer, a))
forall a. a -> n (Ref n a)
forall (m :: * -> *) a. MonadDejaFu m => a -> m (Ref m a)
newRef (Map ThreadId a, Integer, a)
forall {k} {a}. (Map k a, Integer, a)
val
  let ref :: ModelIORef n a
ref = IORefId -> Ref n (Map ThreadId a, Integer, a) -> ModelIORef n a
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
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c ref) tid cThreads, cIdSource = idSource' }
       , IORefId -> ThreadAction
NewIORef IORefId
newiorid
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (Ref n (Map ThreadId a, Integer, a)
-> (Map ThreadId a, Integer, a) -> n ()
forall a. Ref n a -> a -> n ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Map ThreadId a, Integer, a)
ioref (Map ThreadId a, Integer, a)
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)
iorefId :: IORefId
iorefRef :: 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
..} a -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  a
val <- ModelIORef n a -> ThreadId -> n a
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n a
readIORef ModelIORef n a
ref ThreadId
tid
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c val) tid cThreads }
       , IORefId -> ThreadAction
ReadIORef IORefId
iorefId
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} ModelTicket a -> Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  ModelTicket a
tick <- ModelIORef n a -> ThreadId -> n (ModelTicket a)
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n (ModelTicket a)
readForTicket ModelIORef n a
ref ThreadId
tid
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c tick) tid cThreads }
       , IORefId -> ThreadAction
ReadIORefCas IORefId
iorefId
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} a -> (a, b)
f b -> Action n
c) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  (a
new, b
val) <- a -> (a, b)
f (a -> (a, b)) -> n a -> n (a, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelIORef n a -> ThreadId -> n a
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> ThreadId -> n a
readIORef ModelIORef n a
ref ThreadId
tid
  n ()
effect <- ModelIORef n a -> a -> n (n ())
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> a -> n (n ())
writeImmediate ModelIORef n a
ref a
new
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c val) tid cThreads }
       , IORefId -> ThreadAction
ModIORef IORefId
iorefId
       , n () -> Threads n -> n ()
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} a -> (a, b)
f b -> Action n
c) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  tick :: ModelTicket a
tick@(ModelTicket IORefId
_ Integer
_ a
old) <- ModelIORef n a -> ThreadId -> n (ModelTicket a)
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) <- ModelIORef n a
-> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())
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
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c val) tid cThreads }
       , IORefId -> ThreadAction
ModIORefCas IORefId
iorefId
       , n () -> Threads n -> n ()
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} a
a Action n
c) = \ctx :: Context n g
ctx@Context{g
Int
[Invariant n ()]
Threads n
ConcurrencyState
IdSource
WriteBuffer n
InvariantContext n
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> case MemType
memtype of
  -- write immediately.
  MemType
SequentialConsistency -> do
    n ()
effect <- ModelIORef n a -> a -> n (n ())
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelIORef n a -> a -> n (n ())
writeImmediate ModelIORef n a
ref a
a
    (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto c tid cThreads }
         , IORefId -> ThreadAction
WriteIORef IORefId
iorefId
         , n () -> Threads n -> n ()
forall a b. a -> b -> a
const n ()
effect
         )
  -- add to buffer using thread id.
  MemType
TotalStoreOrder -> do
    WriteBuffer n
wb' <- WriteBuffer n
-> (ThreadId, Maybe IORefId)
-> ModelIORef n a
-> a
-> n (WriteBuffer n)
forall (n :: * -> *) a.
MonadDejaFu n =>
WriteBuffer n
-> (ThreadId, Maybe IORefId)
-> ModelIORef n a
-> a
-> n (WriteBuffer n)
bufferWrite WriteBuffer n
cWriteBuf (ThreadId
tid, Maybe IORefId
forall a. Maybe a
Nothing) ModelIORef n a
ref a
a
    (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }
         , IORefId -> ThreadAction
WriteIORef IORefId
iorefId
         , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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' <- WriteBuffer n
-> (ThreadId, Maybe IORefId)
-> ModelIORef n a
-> a
-> n (WriteBuffer n)
forall (n :: * -> *) a.
MonadDejaFu n =>
WriteBuffer n
-> (ThreadId, Maybe IORefId)
-> ModelIORef n a
-> a
-> n (WriteBuffer n)
bufferWrite WriteBuffer n
cWriteBuf (ThreadId
tid, IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
iorefId) ModelIORef n a
ref a
a
    (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }
         , IORefId -> ThreadAction
WriteIORef IORefId
iorefId
         , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} ModelTicket a
tick a
a (Bool, ModelTicket a) -> Action n
c) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  (Bool
suc, ModelTicket a
tick', n ()
effect) <- ModelIORef n a
-> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())
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
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c (suc, tick')) tid cThreads }
       , IORefId -> Bool -> ThreadAction
CasIORef IORefId
iorefId Bool
suc
       , n () -> Threads n -> n ()
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  WriteBuffer n
wb' <- case MemType
memtype of
    -- shouldn't ever get here
    MemType
SequentialConsistency ->
      String -> String -> n (WriteBuffer n)
forall a. HasCallStack => String -> a
fatal String
"stepThread.ACommit" String
"Attempting to commit under SequentialConsistency"
    -- commit using the thread id.
    MemType
TotalStoreOrder ->
      WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
forall (n :: * -> *).
MonadDejaFu n =>
WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
commitWrite WriteBuffer n
cWriteBuf (ThreadId
t, Maybe IORefId
forall a. Maybe a
Nothing)
    -- commit using the IORef id.
    MemType
PartialStoreOrder ->
      WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
forall (n :: * -> *).
MonadDejaFu n =>
WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
commitWrite WriteBuffer n
cWriteBuf (ThreadId
t, IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
c)
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cWriteBuf = wb' }
       , ThreadId -> IORefId -> ThreadAction
CommitIORef ThreadId
t IORefId
c
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  (Result a
res, n ()
effect, IdSource
idSource', [TAction]
trace) <- ModelSTM n a -> IdSource -> n (Result a, n (), IdSource, [TAction])
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) = BlockedOn -> Threads n -> (Threads n, [ThreadId])
forall (n :: * -> *).
BlockedOn -> Threads n -> (Threads n, [ThreadId])
wake ([TVarId] -> BlockedOn
OnTVar [TVarId]
written) Threads n
cThreads
      (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c val) tid threads', cIdSource = idSource' }
           , [TAction] -> [ThreadId] -> ThreadAction
STM [TAction]
trace [ThreadId]
woken
           , n () -> Threads n -> n ()
forall a b. a -> b -> a
const n ()
effect
           )
    Retry [TVarId]
touched -> do
      let threads' :: Threads n
threads' = BlockedOn -> ThreadId -> Threads n -> Threads n
forall (n :: * -> *).
HasCallStack =>
BlockedOn -> ThreadId -> Threads n -> Threads n
block ([TVarId] -> BlockedOn
OnTVar [TVarId]
touched) ThreadId
tid Threads n
cThreads
      (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = threads', cIdSource = idSource'}
           , [TAction] -> ThreadAction
BlockedSTM [TAction]
trace
           , n () -> Threads n -> n ()
forall a b. a -> b -> a
const n ()
effect
           )
    Exception SomeException
e -> do
      (What n g, ThreadAction, Threads n -> n ())
res' <- (Maybe MaskingState -> ThreadAction)
-> ThreadId
-> SomeException
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
      (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((What n g, ThreadAction, Threads n -> n ())
 -> n (What n g, ThreadAction, Threads n -> n ()))
-> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
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') -> (Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx' { cIdSource = idSource' }, ThreadAction
act, Threads n -> n ()
effect')
        (Failed Condition
err, ThreadAction
act, Threads n -> n ()
effect') -> (Condition -> What n g
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  let effect :: Threads n -> n (Action n)
effect Threads n
threads = ThreadId -> Threads n -> n (Action n) -> n (Action n)
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
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto a tid cThreads }
       , ThreadAction
LiftIO
       , n (Action n) -> n ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (n (Action n) -> n ())
-> (Threads n -> n (Action n)) -> Threads n -> n ()
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) = (Maybe MaskingState -> ThreadAction)
-> ThreadId
-> e
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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) = (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g -> n (What n g, ThreadAction, Threads n -> n ())
forall (n :: * -> *) g x.
MonadDejaFu n =>
(Context n g -> n x) -> Context n g -> n x
synchronised ((Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
 -> Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> (Context n g -> n (What n g, ThreadAction, Threads n -> n ()))
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} ->
  let threads' :: Threads n
threads' = Action n -> ThreadId -> Threads n -> Threads n
forall (n :: * -> *).
HasCallStack =>
Action n -> ThreadId -> Threads n -> Threads n
goto Action n
c ThreadId
tid Threads n
cThreads
      blocked :: Threads n
blocked  = BlockedOn -> ThreadId -> Threads n -> Threads n
forall (n :: * -> *).
HasCallStack =>
BlockedOn -> ThreadId -> Threads n -> Threads n
block (ThreadId -> BlockedOn
OnMask ThreadId
t) ThreadId
tid Threads n
cThreads
  in case ThreadId -> Threads n -> Maybe (Thread n)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ThreadId
t Threads n
cThreads of
       Just Thread n
thread
         | Thread n -> Bool
forall {n :: * -> *}. Thread n -> Bool
interruptible Thread n
thread Bool -> Bool -> Bool
|| ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid -> (Maybe MaskingState -> ThreadAction)
-> ThreadId
-> e
-> Context n g
-> n (What n g, ThreadAction, Threads n -> n ())
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' }
         | Bool
otherwise -> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
           ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = blocked }
           , ThreadId -> ThreadAction
BlockedThrowTo ThreadId
t
           , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
           )
       Maybe (Thread n)
Nothing -> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
         (Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = threads' }
         , ThreadId -> Maybe MaskingState -> ThreadAction
ThrowTo ThreadId
t Maybe MaskingState
forall a. Maybe a
Nothing
         , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((What n g, ThreadAction, Threads n -> n ())
 -> n (What n g, ThreadAction, Threads n -> n ()))
-> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a b. (a -> b) -> a -> b
$
  let a :: Action n
a     = ModelConc n a -> (a -> Action n) -> Action n
forall a (n :: * -> *).
Program Basic n a -> (a -> Action n) -> Action n
runModelConc ModelConc n a
ma (Action n -> Action n
forall (n :: * -> *). Action n -> Action n
APopCatching (Action n -> Action n) -> (a -> Action n) -> a -> Action n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Action n
c)
      e :: e -> Action n
e e
exc = ModelConc n a -> (a -> Action n) -> Action n
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 ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto a tid (catching e tid cThreads) }
     , ThreadAction
Catching
     , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} ->
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto a tid (uncatching tid cThreads) }
       , ThreadAction
PopCatching
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((What n g, ThreadAction, Threads n -> n ())
 -> n (What n g, ThreadAction, Threads n -> n ()))
-> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a b. (a -> b) -> a -> b
$
  let resetMask :: Bool -> MaskingState -> Program Basic n ()
resetMask Bool
typ MaskingState
ms = ((() -> Action n) -> Action n) -> Program Basic n ()
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (((() -> Action n) -> Action n) -> Program Basic n ())
-> ((() -> Action n) -> Action n) -> Program Basic n ()
forall a b. (a -> b) -> a -> b
$ \() -> Action n
k -> Bool -> Bool -> MaskingState -> Action n -> Action n
forall (n :: * -> *).
Bool -> Bool -> MaskingState -> Action n -> Action n
AResetMask Bool
typ Bool
True MaskingState
ms (Action n -> Action n) -> Action n -> Action n
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 = Bool -> MaskingState -> Program Basic n ()
forall {n :: * -> *}. Bool -> MaskingState -> Program Basic n ()
resetMask Bool
True MaskingState
m' Program Basic n () -> Program Basic n b -> Program Basic n b
forall a b.
Program Basic n a -> Program Basic n b -> Program Basic n b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Program Basic n b
mb Program Basic n b -> (b -> Program Basic n b) -> Program Basic n b
forall a b.
Program Basic n a -> (a -> Program Basic n b) -> Program Basic n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b
b -> Bool -> MaskingState -> Program Basic n ()
forall {n :: * -> *}. Bool -> MaskingState -> Program Basic n ()
resetMask Bool
False MaskingState
m Program Basic n () -> Program Basic n b -> Program Basic n b
forall a b.
Program Basic n a -> Program Basic n b -> Program Basic n b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> b -> Program Basic n b
forall a. a -> Program Basic n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
b
      m' :: MaskingState
m' = Thread n -> MaskingState
forall (n :: * -> *). Thread n -> MaskingState
_masking (Thread n -> MaskingState) -> Thread n -> MaskingState
forall a b. (a -> b) -> a -> b
$ ThreadId -> Threads n -> Thread n
forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
tid Threads n
cThreads
      a :: Action n
a  = ModelConc n a -> (a -> Action n) -> Action n
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 Program Basic n b -> Program Basic n b
forall b. ModelConc n b -> ModelConc n b
forall {n :: * -> *} {b}. Program Basic n b -> Program Basic n b
umask) (Bool -> Bool -> MaskingState -> Action n -> Action n
forall (n :: * -> *).
Bool -> Bool -> MaskingState -> Action n -> Action n
AResetMask Bool
False Bool
False MaskingState
m' (Action n -> Action n) -> (a -> Action n) -> a -> Action n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Action n
c)
  in ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto a tid (mask m tid cThreads) }
     , Bool -> MaskingState -> ThreadAction
SetMasking Bool
False MaskingState
m
     , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} ->
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto c tid (mask m tid cThreads) }
       , (if Bool
b1 then Bool -> MaskingState -> ThreadAction
SetMasking else Bool -> MaskingState -> ThreadAction
ResetMasking) Bool
b2 MaskingState
m
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((What n g, ThreadAction, Threads n -> n ())
 -> n (What n g, ThreadAction, Threads n -> n ()))
-> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a b. (a -> b) -> a -> b
$
  let m :: MaskingState
m = Thread n -> MaskingState
forall (n :: * -> *). Thread n -> MaskingState
_masking (Thread n -> MaskingState) -> Thread n -> MaskingState
forall a b. (a -> b) -> a -> b
$ ThreadId -> Threads n -> Thread n
forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
tid Threads n
cThreads
  in ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto (c m) tid cThreads }
     , MaskingState -> ThreadAction
GetMaskingState MaskingState
m
     , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} ->
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = goto c tid cThreads }
       , ThreadAction
Return
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} -> do
  n ()
na
  Threads n
threads' <- ThreadId -> Threads n -> n (Threads n)
forall (n :: * -> *).
(MonadDejaFu n, HasCallStack) =>
ThreadId -> Threads n -> n (Threads n)
kill ThreadId
tid Threads n
cThreads
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = threads' }
       , ThreadAction
Stop
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} ->
  (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx
         { cThreads = goto c tid cThreads
         , cNewInvariants = inv : cNewInvariants
         }
       , ThreadAction
RegisterInvariant
       , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} = case SomeException -> ThreadId -> Threads n -> Maybe (Threads n)
forall (n :: * -> *).
HasCallStack =>
SomeException -> ThreadId -> Threads n -> Maybe (Threads n)
propagate SomeException
some ThreadId
tid Threads n
cThreads of
    Just Threads n
ts' -> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = ts' }
      , Maybe MaskingState -> ThreadAction
act (MaskingState -> Maybe MaskingState
forall a. a -> Maybe a
Just (MaskingState -> Maybe MaskingState)
-> (Thread n -> MaskingState) -> Thread n -> Maybe MaskingState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thread n -> MaskingState
forall (n :: * -> *). Thread n -> MaskingState
_masking (Thread n -> Maybe MaskingState) -> Thread n -> Maybe MaskingState
forall a b. (a -> b) -> a -> b
$ ThreadId -> Threads n -> Thread n
forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup ThreadId
tid Threads n
ts')
      , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
      )
    Maybe (Threads n)
Nothing
      | ThreadId
tid ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
initialThread -> (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( Condition -> What n g
forall (n :: * -> *) g. Condition -> What n g
Failed (SomeException -> Condition
UncaughtException SomeException
some)
        , Maybe MaskingState -> ThreadAction
act Maybe MaskingState
forall a. Maybe a
Nothing
        , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
        )
      | Bool
otherwise -> do
          Threads n
ts' <- ThreadId -> Threads n -> n (Threads n)
forall (n :: * -> *).
(MonadDejaFu n, HasCallStack) =>
ThreadId -> Threads n -> n (Threads n)
kill ThreadId
tid Threads n
cThreads
          (What n g, ThreadAction, Threads n -> n ())
-> n (What n g, ThreadAction, Threads n -> n ())
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Context n g -> What n g
forall (n :: * -> *) g. Context n g -> What n g
Succeeded Context n g
ctx { cThreads = ts' }
               , Maybe MaskingState -> ThreadAction
act Maybe MaskingState
forall a. Maybe a
Nothing
               , n () -> Threads n -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
               )
  where
    some :: SomeException
some = e -> SomeException
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
cSchedState :: forall (n :: * -> *) g. Context n g -> g
cIdSource :: forall (n :: * -> *) g. Context n g -> IdSource
cThreads :: forall (n :: * -> *) g. Context n g -> Threads n
cWriteBuf :: forall (n :: * -> *) g. Context n g -> WriteBuffer n
cCaps :: forall (n :: * -> *) g. Context n g -> Int
cInvariants :: forall (n :: * -> *) g. Context n g -> InvariantContext n
cNewInvariants :: forall (n :: * -> *) g. Context n g -> [Invariant n ()]
cCState :: forall (n :: * -> *) g. Context n g -> ConcurrencyState
cSchedState :: g
cIdSource :: IdSource
cThreads :: Threads n
cWriteBuf :: WriteBuffer n
cCaps :: Int
cInvariants :: InvariantContext n
cNewInvariants :: [Invariant n ()]
cCState :: ConcurrencyState
..} = do
  WriteBuffer n -> n ()
forall (n :: * -> *). MonadDejaFu n => WriteBuffer n -> n ()
writeBarrier WriteBuffer n
cWriteBuf
  Context n g -> n x
ma Context n g
ctx { cWriteBuf = 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 = [Invariant n ()]
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
-> InvariantContext n
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 = ((Invariant n (), ([IORefId], [MVarId], [TVarId]))
 -> Invariant n ())
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
-> [Invariant n ()]
forall a b. (a -> b) -> [a] -> [b]
map (Invariant n (), ([IORefId], [MVarId], [TVarId])) -> Invariant n ()
forall a b. (a, b) -> a
fst [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
unblocked [Invariant n ()] -> [Invariant n ()] -> [Invariant n ()]
forall a. [a] -> [a] -> [a]
++ InvariantContext n -> [Invariant n ()]
forall (n :: * -> *). InvariantContext n -> [Invariant n ()]
icActive InvariantContext n
ic

  ([(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
unblocked, [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
blocked) = (((Invariant n (), ([IORefId], [MVarId], [TVarId])) -> Bool)
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
-> ([(Invariant n (), ([IORefId], [MVarId], [TVarId]))],
    [(Invariant n (), ([IORefId], [MVarId], [TVarId]))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
`partition` InvariantContext n
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
forall (n :: * -> *).
InvariantContext n
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
icBlocked InvariantContext n
ic) (((Invariant n (), ([IORefId], [MVarId], [TVarId])) -> Bool)
 -> ([(Invariant n (), ([IORefId], [MVarId], [TVarId]))],
     [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]))
-> ((Invariant n (), ([IORefId], [MVarId], [TVarId])) -> Bool)
-> ([(Invariant n (), ([IORefId], [MVarId], [TVarId]))],
    [(Invariant n (), ([IORefId], [MVarId], [TVarId]))])
forall a b. (a -> b) -> a -> b
$
    \(Invariant n ()
_, ([IORefId]
ioridsB, [MVarId]
mvidsB, [TVarId]
tvidsB)) ->
      Bool -> (IORefId -> Bool) -> Maybe IORefId -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (IORefId -> [IORefId] -> Bool
forall a. Eq a => a -> [a] -> Bool
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
||
      Bool -> (MVarId -> Bool) -> Maybe MVarId -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (MVarId -> [MVarId] -> Bool
forall a. Eq a => a -> [a] -> Bool
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
||
      (TVarId -> Bool) -> Set TVarId -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TVarId -> [TVarId] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 = [Invariant n ()]
-> n (Either
        SomeException [(Invariant n (), ([IORefId], [MVarId], [TVarId]))])
forall {m :: * -> *} {a}.
MonadDejaFu m =>
[Invariant m a]
-> m (Either
        SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
go (InvariantContext n -> [Invariant n ()]
forall (n :: * -> *). InvariantContext n -> [Invariant n ()]
icActive InvariantContext n
ic) n (Either
     SomeException [(Invariant n (), ([IORefId], [MVarId], [TVarId]))])
-> (Either
      SomeException [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
    -> n (Either SomeException (InvariantContext n)))
-> n (Either SomeException (InvariantContext n))
forall a b. n a -> (a -> n b) -> n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
blocked -> Either SomeException (InvariantContext n)
-> n (Either SomeException (InvariantContext n))
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (InvariantContext n -> Either SomeException (InvariantContext n)
forall a b. b -> Either a b
Right ([Invariant n ()]
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
-> InvariantContext n
forall (n :: * -> *).
[Invariant n ()]
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
-> InvariantContext n
InvariantContext [] ([(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
blocked [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
forall a. [a] -> [a] -> [a]
++ InvariantContext n
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
forall (n :: * -> *).
InvariantContext n
-> [(Invariant n (), ([IORefId], [MVarId], [TVarId]))]
icBlocked InvariantContext n
ic)))
    Left SomeException
exc -> Either SomeException (InvariantContext n)
-> n (Either SomeException (InvariantContext n))
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeException -> Either SomeException (InvariantContext n)
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) = Invariant m a
-> m (Either SomeException ([IORefId], [MVarId], [TVarId]))
forall (n :: * -> *) a.
MonadDejaFu n =>
Invariant n a
-> n (Either SomeException ([IORefId], [MVarId], [TVarId]))
checkInvariant Invariant m a
inv m (Either SomeException ([IORefId], [MVarId], [TVarId]))
-> (Either SomeException ([IORefId], [MVarId], [TVarId])
    -> m (Either
            SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))]))
-> m (Either
        SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right ([IORefId], [MVarId], [TVarId])
o -> ([(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
 -> [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
-> Either
     SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
-> Either
     SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
forall a b.
(a -> b) -> Either SomeException a -> Either SomeException b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Invariant m a
inv,([IORefId], [MVarId], [TVarId])
o)(Invariant m a, ([IORefId], [MVarId], [TVarId]))
-> [(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
-> [(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
forall a. a -> [a] -> [a]
:) (Either
   SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
 -> Either
      SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
-> m (Either
        SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
-> m (Either
        SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
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 -> Either
  SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
-> m (Either
        SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeException
-> Either
     SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
forall a b. a -> Either a b
Left SomeException
exc)
    go [] = Either
  SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
-> m (Either
        SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
-> Either
     SomeException [(Invariant m a, ([IORefId], [MVarId], [TVarId]))]
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 = Invariant n a
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
forall (n :: * -> *) a.
MonadDejaFu n =>
Invariant n a
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
doInvariant Invariant n a
inv n (Either SomeException a, [IORefId], [MVarId], [TVarId])
-> ((Either SomeException a, [IORefId], [MVarId], [TVarId])
    -> n (Either SomeException ([IORefId], [MVarId], [TVarId])))
-> n (Either SomeException ([IORefId], [MVarId], [TVarId]))
forall a b. n a -> (a -> n b) -> n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  (Right a
_, [IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars) -> Either SomeException ([IORefId], [MVarId], [TVarId])
-> n (Either SomeException ([IORefId], [MVarId], [TVarId]))
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([IORefId], [MVarId], [TVarId])
-> Either SomeException ([IORefId], [MVarId], [TVarId])
forall a b. b -> Either a b
Right ([IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars))
  (Left SomeException
exc, [IORefId]
_, [MVarId]
_, [TVarId]
_) -> Either SomeException ([IORefId], [MVarId], [TVarId])
-> n (Either SomeException ([IORefId], [MVarId], [TVarId]))
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeException
-> Either SomeException ([IORefId], [MVarId], [TVarId])
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) <- (n () -> IAction n)
-> (a -> Maybe (Either SomeException a))
-> ((a -> IAction n) -> IAction n)
-> n (IAction n, Ref n (Maybe (Either SomeException a)))
forall (n :: * -> *) x a b.
MonadDejaFu n =>
(n () -> x)
-> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref n (Maybe b))
runRefCont n () -> IAction n
forall (n :: * -> *). n () -> IAction n
IStop (Either SomeException a -> Maybe (Either SomeException a)
forall a. a -> Maybe a
Just (Either SomeException a -> Maybe (Either SomeException a))
-> (a -> Either SomeException a)
-> a
-> Maybe (Either SomeException a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either SomeException a
forall a b. b -> Either a b
Right) (Invariant n a -> (a -> IAction n) -> IAction n
forall (n :: * -> *) a.
Invariant n a -> (a -> IAction n) -> IAction n
runInvariant Invariant n a
inv)
    ([IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars) <- Ref n (Maybe (Either SomeException a))
-> IAction n
-> [IORefId]
-> [MVarId]
-> [TVarId]
-> n ([IORefId], [MVarId], [TVarId])
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 <- Ref n (Maybe (Either SomeException a))
-> n (Maybe (Either SomeException a))
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe (Either SomeException a))
ref
    (Either SomeException a, [IORefId], [MVarId], [TVarId])
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Either SomeException a) -> Either SomeException a
forall a. HasCallStack => Maybe a -> a
efromJust Maybe (Either SomeException a)
val, [IORefId] -> [IORefId]
forall a. Eq a => [a] -> [a]
nub [IORefId]
iorefs, [MVarId] -> [MVarId]
forall a. Eq a => [a] -> [a]
nub [MVarId]
mvars, [TVarId] -> [TVarId]
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') <- IAction m
-> m (Either SomeException (Maybe (IAction m)), [IORefId],
      [MVarId], [TVarId])
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' [IORefId] -> [IORefId] -> [IORefId]
forall a. [a] -> [a] -> [a]
++ [IORefId]
iorefs
      let newMVars :: [MVarId]
newMVars  = [MVarId]
mvars'  [MVarId] -> [MVarId] -> [MVarId]
forall a. [a] -> [a] -> [a]
++ [MVarId]
mvars
      let newTVars :: [TVarId]
newTVars  = [TVarId]
tvars'  [TVarId] -> [TVarId] -> [TVarId]
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 ->
          ([IORefId], [MVarId], [TVarId])
-> m ([IORefId], [MVarId], [TVarId])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([IORefId]
newIORefs, [MVarId]
newMVars, [TVarId]
newTVars)
        Left SomeException
exc -> do
          Ref m (Maybe (Either SomeException b))
-> Maybe (Either SomeException b) -> m ()
forall a. Ref m a -> a -> m ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref m (Maybe (Either SomeException b))
ref (Either SomeException b -> Maybe (Either SomeException b)
forall a. a -> Maybe a
Just (SomeException -> Either SomeException b
forall a b. a -> Either a b
Left SomeException
exc))
          ([IORefId], [MVarId], [TVarId])
-> m ([IORefId], [MVarId], [TVarId])
forall a. a -> m a
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 :: forall (n :: * -> *) a.
ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefId :: forall (n :: * -> *) a. ModelIORef n a -> IORefId
iorefId :: IORefId
iorefRef :: Ref n (Map ThreadId a, Integer, a)
..} a -> IAction n
k) = do
  a
a <- ModelIORef n a -> n a
forall (n :: * -> *) a. MonadDejaFu n => ModelIORef n a -> n a
readIORefGlobal ModelIORef n a
ioref
  (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId],
 [TVarId])
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (IAction n) -> Either SomeException (Maybe (IAction n))
forall a b. b -> Either a b
Right (IAction n -> Maybe (IAction n)
forall a. a -> Maybe a
Just (a -> IAction n
k a
a)), [IORefId
iorefId], [], [])
stepInvariant (IInspectMVar 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
mvarId :: MVarId
mvarRef :: Ref n (Maybe a)
..} Maybe a -> IAction n
k) = do
  Maybe a
a <- Ref n (Maybe a) -> n (Maybe a)
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe a)
mvarRef
  (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId],
 [TVarId])
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (IAction n) -> Either SomeException (Maybe (IAction n))
forall a b. b -> Either a b
Right (IAction n -> Maybe (IAction n)
forall a. a -> Maybe a
Just (Maybe a -> IAction n
k Maybe a
a)), [], [MVarId
mvarId], [])
stepInvariant (IInspectTVar ModelTVar{TVarId
Ref n a
tvarId :: TVarId
tvarRef :: Ref n a
tvarRef :: forall (n :: * -> *) a. ModelTVar n a -> Ref n a
tvarId :: forall (n :: * -> *) a. ModelTVar n a -> TVarId
..} a -> IAction n
k) = do
  a
a <- Ref n a -> n a
forall a. Ref n a -> n a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n a
tvarRef
  (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId],
 [TVarId])
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (IAction n) -> Either SomeException (Maybe (IAction n))
forall a b. b -> Either a b
Right (IAction n -> Maybe (IAction n)
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) = Invariant n a
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
forall (n :: * -> *) a.
MonadDejaFu n =>
Invariant n a
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
doInvariant Invariant n a
nx n (Either SomeException a, [IORefId], [MVarId], [TVarId])
-> ((Either SomeException a, [IORefId], [MVarId], [TVarId])
    -> n (Either SomeException (Maybe (IAction n)), [IORefId],
          [MVarId], [TVarId]))
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a b. n a -> (a -> n b) -> n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  (Right a
a, [IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars) ->
    (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId],
 [TVarId])
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (IAction n) -> Either SomeException (Maybe (IAction n))
forall a b. b -> Either a b
Right (IAction n -> Maybe (IAction n)
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 SomeException -> Maybe e
forall e. Exception e => SomeException -> Maybe e
E.fromException SomeException
exc of
    Just e
exc' -> Invariant n a
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
forall (n :: * -> *) a.
MonadDejaFu n =>
Invariant n a
-> n (Either SomeException a, [IORefId], [MVarId], [TVarId])
doInvariant (e -> Invariant n a
h e
exc') n (Either SomeException a, [IORefId], [MVarId], [TVarId])
-> ((Either SomeException a, [IORefId], [MVarId], [TVarId])
    -> n (Either SomeException (Maybe (IAction n)), [IORefId],
          [MVarId], [TVarId]))
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a b. n a -> (a -> n b) -> n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      (Right a
a, [IORefId]
iorefs', [MVarId]
mvars', [TVarId]
tvars') ->
        (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId],
 [TVarId])
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (IAction n) -> Either SomeException (Maybe (IAction n))
forall a b. b -> Either a b
Right (IAction n -> Maybe (IAction n)
forall a. a -> Maybe a
Just (a -> IAction n
k a
a)), [IORefId]
iorefs' [IORefId] -> [IORefId] -> [IORefId]
forall a. [a] -> [a] -> [a]
++ [IORefId]
iorefs, [MVarId]
mvars' [MVarId] -> [MVarId] -> [MVarId]
forall a. [a] -> [a] -> [a]
++ [MVarId]
mvars, [TVarId]
tvars' [TVarId] -> [TVarId] -> [TVarId]
forall a. [a] -> [a] -> [a]
++ [TVarId]
tvars)
      (Left SomeException
exc'', [IORefId]
iorefs', [MVarId]
mvars', [TVarId]
tvars') ->
        (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId],
 [TVarId])
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeException -> Either SomeException (Maybe (IAction n))
forall a b. a -> Either a b
Left SomeException
exc'', [IORefId]
iorefs' [IORefId] -> [IORefId] -> [IORefId]
forall a. [a] -> [a] -> [a]
++ [IORefId]
iorefs, [MVarId]
mvars' [MVarId] -> [MVarId] -> [MVarId]
forall a. [a] -> [a] -> [a]
++ [MVarId]
mvars, [TVarId]
tvars' [TVarId] -> [TVarId] -> [TVarId]
forall a. [a] -> [a] -> [a]
++ [TVarId]
tvars)
    Maybe e
Nothing -> (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId],
 [TVarId])
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeException -> Either SomeException (Maybe (IAction n))
forall a b. a -> Either a b
Left SomeException
exc, [IORefId]
iorefs, [MVarId]
mvars, [TVarId]
tvars)
stepInvariant (IThrow e
exc) =
  (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId],
 [TVarId])
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeException -> Either SomeException (Maybe (IAction n))
forall a b. a -> Either a b
Left (e -> SomeException
forall e. Exception e => e -> SomeException
toException e
exc), [], [], [])
stepInvariant (IStop n ()
finalise) = do
  n ()
finalise
  (Either SomeException (Maybe (IAction n)), [IORefId], [MVarId],
 [TVarId])
-> n (Either SomeException (Maybe (IAction n)), [IORefId],
      [MVarId], [TVarId])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (IAction n) -> Either SomeException (Maybe (IAction n))
forall a b. b -> Either a b
Right Maybe (IAction n)
forall a. Maybe a
Nothing, [], [], [])