{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}

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

import           Data.Coerce                       (Coercible, coerce)
import qualified Data.IntMap.Strict                as I
import           Data.List                         (find, mapAccumL)
import           Data.Maybe                        (fromMaybe)
import           GHC.Stack                         (HasCallStack)

import           Test.DejaFu.Conc
import           Test.DejaFu.Conc.Internal         (Context(..))
import           Test.DejaFu.Conc.Internal.Memory  (commitThreadId)
import           Test.DejaFu.Conc.Internal.Program
import           Test.DejaFu.Internal
import           Test.DejaFu.Schedule              (Scheduler(..))
import           Test.DejaFu.SCT.Internal.DPOR
import           Test.DejaFu.Types
import           Test.DejaFu.Utils

-------------------------------------------------------------------------------
-- * Exploration

-- | General-purpose SCT function.
sct :: (MonadDejaFu n, HasCallStack)
  => Settings n a
  -- ^ The SCT settings ('Way' is ignored)
  -> ([ThreadId] -> s)
  -- ^ Initial state
  -> (s -> Maybe t)
  -- ^ State predicate
  -> (ConcurrencyState -> (Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace)))
  -- ^ Run the computation and update the state
  -> Program pty n a
  -> n [(Either Condition a, Trace)]
sct :: Settings n a
-> ([ThreadId] -> s)
-> (s -> Maybe t)
-> (ConcurrencyState
    -> (Scheduler g -> g -> n (Either Condition a, g, Trace))
    -> s
    -> t
    -> n (s, Maybe (Either Condition a, Trace)))
-> Program pty n a
-> n [(Either Condition a, Trace)]
sct Settings n a
settings [ThreadId] -> s
s0 s -> Maybe t
sfun ConcurrencyState
-> (Scheduler g -> g -> n (Either Condition a, g, Trace))
-> s
-> t
-> n (s, Maybe (Either Condition a, Trace))
srun Program pty n a
conc = Program pty n a
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
forall (n :: * -> *) pty a.
MonadDejaFu n =>
Program pty n a
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
recordSnapshot Program pty n a
conc n (Maybe (Either Condition (Snapshot pty n a), Trace))
-> (Maybe (Either Condition (Snapshot pty n a), Trace)
    -> n [(Either Condition a, Trace)])
-> n [(Either Condition a, Trace)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (Right Snapshot pty n a
snap, Trace
_) -> Snapshot pty n a -> n [(Either Condition a, Trace)]
forall p. Snapshot p n a -> n [(Either Condition a, Trace)]
sct'Snap Snapshot pty n a
snap
    Just (Left Condition
f, Trace
trace) -> [(Either Condition a, Trace)] -> n [(Either Condition a, Trace)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Condition -> Either Condition a
forall a b. a -> Either a b
Left Condition
f, Trace
trace)]
    Maybe (Either Condition (Snapshot pty n a), Trace)
Nothing -> n [(Either Condition a, Trace)]
sct'Full
  where
    sct'Full :: n [(Either Condition a, Trace)]
sct'Full = Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
forall (n :: * -> *) a s t.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
sct'
      Settings n a
settings
      ConcurrencyState
initialCState
      ([ThreadId] -> s
s0 [ThreadId
initialThread])
      s -> Maybe t
sfun
      (ConcurrencyState
-> (Scheduler g -> g -> n (Either Condition a, g, Trace))
-> s
-> t
-> n (s, Maybe (Either Condition a, Trace))
srun ConcurrencyState
initialCState Scheduler g -> g -> n (Either Condition a, g, Trace)
forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
runFull)
      forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
runFull
      (Int -> ThreadId
forall a. Coercible Id a => Int -> a
toId Int
1)
      (Int -> IORefId
forall a. Coercible Id a => Int -> a
toId Int
1)

    sct'Snap :: Snapshot p n a -> n [(Either Condition a, Trace)]
sct'Snap Snapshot p n a
snap =
      let idsrc :: IdSource
idsrc = Context n () -> IdSource
forall (n :: * -> *) g. Context n g -> IdSource
cIdSource (Snapshot p n a -> Context n ()
forall p (n :: * -> *) a. Snapshot p n a -> Context n ()
contextFromSnapshot Snapshot p n a
snap)
          cstate :: ConcurrencyState
cstate = Context n () -> ConcurrencyState
forall (n :: * -> *) g. Context n g -> ConcurrencyState
cCState (Snapshot p n a -> Context n ()
forall p (n :: * -> *) a. Snapshot p n a -> Context n ()
contextFromSnapshot Snapshot p n a
snap)
      in Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
forall (n :: * -> *) a s t.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
sct'
         Settings n a
settings
         ConcurrencyState
cstate
         ([ThreadId] -> s
s0 (([ThreadId], [ThreadId]) -> [ThreadId]
forall a b. (a, b) -> a
fst (Snapshot p n a -> ([ThreadId], [ThreadId])
forall p (n :: * -> *) a.
Snapshot p n a -> ([ThreadId], [ThreadId])
threadsFromSnapshot Snapshot p n a
snap)))
         s -> Maybe t
sfun
         (ConcurrencyState
-> (Scheduler g -> g -> n (Either Condition a, g, Trace))
-> s
-> t
-> n (s, Maybe (Either Condition a, Trace))
srun ConcurrencyState
cstate (Snapshot p n a
-> Scheduler g -> g -> n (Either Condition a, g, Trace)
forall (n :: * -> *) pty a s.
MonadDejaFu n =>
Snapshot pty n a
-> Scheduler s -> s -> n (Either Condition a, s, Trace)
runSnap Snapshot p n a
snap))
         (Snapshot p n a
-> Scheduler x -> x -> n (Either Condition a, x, Trace)
forall (n :: * -> *) pty a s.
MonadDejaFu n =>
Snapshot pty n a
-> Scheduler s -> s -> n (Either Condition a, s, Trace)
runSnap Snapshot p n a
snap)
         (Int -> ThreadId
forall a. Coercible Id a => Int -> a
toId (Int -> ThreadId) -> Int -> ThreadId
forall a b. (a -> b) -> a -> b
$ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int, [String]) -> Int
forall a b. (a, b) -> a
fst (IdSource -> (Int, [String])
_tids IdSource
idsrc))
         (Int -> IORefId
forall a. Coercible Id a => Int -> a
toId (Int -> IORefId) -> Int -> IORefId
forall a b. (a -> b) -> a -> b
$ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int, [String]) -> Int
forall a b. (a, b) -> a
fst (IdSource -> (Int, [String])
_iorids IdSource
idsrc))

    runFull :: Scheduler s -> s -> n (Either Condition a, s, Trace)
runFull Scheduler s
sched s
s = Scheduler s
-> MemType
-> s
-> Program pty n a
-> n (Either Condition a, s, Trace)
forall (n :: * -> *) s pty a.
MonadDejaFu n =>
Scheduler s
-> MemType
-> s
-> Program pty n a
-> n (Either Condition a, s, Trace)
runConcurrent Scheduler s
sched (Settings n a -> MemType
forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) s
s Program pty n a
conc
    runSnap :: Snapshot pty n a
-> Scheduler s -> s -> n (Either Condition a, s, Trace)
runSnap Snapshot pty n a
snap Scheduler s
sched s
s = Scheduler s
-> MemType
-> s
-> Snapshot pty n a
-> n (Either Condition a, s, Trace)
forall (n :: * -> *) s pty a.
MonadDejaFu n =>
Scheduler s
-> MemType
-> s
-> Snapshot pty n a
-> n (Either Condition a, s, Trace)
runSnapshot Scheduler s
sched (Settings n a -> MemType
forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) s
s Snapshot pty n a
snap

-- | Like 'sct' but given a function to run the computation.
sct' :: (MonadDejaFu n, HasCallStack)
  => Settings n a
  -- ^ The SCT settings ('Way' is ignored)
  -> ConcurrencyState
  -- ^ The initial concurrency state
  -> s
  -- ^ Initial state
  -> (s -> Maybe t)
  -- ^ State predicate
  -> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
  -- ^ Run the computation and update the state
  -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
  -- ^ Just run the computation
  -> ThreadId
  -- ^ The first available @ThreadId@
  -> IORefId
  -- ^ The first available @IORefId@
  -> n [(Either Condition a, Trace)]
sct' :: Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
sct' Settings n a
settings ConcurrencyState
cstate0 s
s0 s -> Maybe t
sfun s -> t -> n (s, Maybe (Either Condition a, Trace))
srun forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run ThreadId
nTId IORefId
nCRId = Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go Maybe (Either Condition a)
forall a. Maybe a
Nothing [] s
s0 where
  go :: Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Just Either Condition a
res) [Either Condition a]
_ s
_ | Either Condition a -> Bool
earlyExit Either Condition a
res = [(Either Condition a, Trace)] -> n [(Either Condition a, Trace)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  go Maybe (Either Condition a)
res0 [Either Condition a]
seen !s
s = case s -> Maybe t
sfun s
s of
    Just t
t -> s -> t -> n (s, Maybe (Either Condition a, Trace))
srun s
s t
t n (s, Maybe (Either Condition a, Trace))
-> ((s, Maybe (Either Condition a, Trace))
    -> n [(Either Condition a, Trace)])
-> n [(Either Condition a, Trace)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      (s
s', Just (Left Condition
Abort, Trace
_)) | Bool
hideAborts -> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go Maybe (Either Condition a)
res0 [Either Condition a]
seen s
s'
      (s
s', Just (Either Condition a
res, Trace
trace)) -> case Either Condition a -> Maybe Discard
discard Either Condition a
res of
        Just Discard
DiscardResultAndTrace -> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s'
        Just Discard
DiscardTrace -> Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
result Either Condition a
res [] [Either Condition a]
seen s
s'
        Maybe Discard
Nothing -> Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
result Either Condition a
res Trace
trace [Either Condition a]
seen s
s'
      (s
s', Maybe (Either Condition a, Trace)
Nothing) -> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go Maybe (Either Condition a)
forall a. Maybe a
Nothing [Either Condition a]
seen s
s'
    Maybe t
Nothing -> [(Either Condition a, Trace)] -> n [(Either Condition a, Trace)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

  -- Sadly, we have to use a list to store the set of unique results,
  -- as we don't have an @Ord a@ dict hanging around.  I suspect that
  -- most test cases will have a relatively small number of unique
  -- results, compared to the number of executions, however.
  -- Pathological cases (like IORef ones in dejafu-tests which produce
  -- a different result on every execution) are probably uncommon.
  result :: Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
result = case Settings n a -> Maybe (a -> a -> Bool)
forall (n :: * -> *) a. Settings n a -> Maybe (a -> a -> Bool)
_equality Settings n a
settings of
    Just a -> a -> Bool
f -> \Either Condition a
res Trace
trace [Either Condition a]
seen s
s ->
      let eq :: (t -> t -> Bool) -> Either a t -> Either a t -> Bool
eq t -> t -> Bool
cmp (Right t
a1) (Right t
a2) = t -> t -> Bool
cmp t
a1 t
a2
          eq t -> t -> Bool
_   (Left  a
e1) (Left  a
e2) = a
e1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
e2
          eq t -> t -> Bool
_ Either a t
_ Either a t
_ = Bool
False
      in if (Either Condition a -> Bool) -> [Either Condition a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((a -> a -> Bool)
-> Either Condition a -> Either Condition a -> Bool
forall a t t.
Eq a =>
(t -> t -> Bool) -> Either a t -> Either a t -> Bool
eq a -> a -> Bool
f Either Condition a
res) [Either Condition a]
seen
         then Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s
         else Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
dosimplify Either Condition a
res Trace
trace (Either Condition a
resEither Condition a -> [Either Condition a] -> [Either Condition a]
forall a. a -> [a] -> [a]
:[Either Condition a]
seen) s
s
    Maybe (a -> a -> Bool)
Nothing -> Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
dosimplify

  dosimplify :: Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
dosimplify Either Condition a
res [] [Either Condition a]
seen s
s = ((Either Condition a
res, []) (Either Condition a, Trace)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall a. a -> [a] -> [a]
:) ([(Either Condition a, Trace)] -> [(Either Condition a, Trace)])
-> n [(Either Condition a, Trace)]
-> n [(Either Condition a, Trace)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s
  dosimplify Either Condition a
res Trace
trace [Either Condition a]
seen s
s
    | Bool -> Bool
not (Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_simplify Settings n a
settings) = ((Either Condition a
res, Trace
trace) (Either Condition a, Trace)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall a. a -> [a] -> [a]
:) ([(Either Condition a, Trace)] -> [(Either Condition a, Trace)])
-> n [(Either Condition a, Trace)]
-> n [(Either Condition a, Trace)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s
    | Bool
otherwise = do
        (Either Condition a, Trace)
shrunk <- Settings n a
-> ConcurrencyState
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> Either Condition a
-> Trace
-> n (Either Condition a, Trace)
forall (n :: * -> *) a.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ConcurrencyState
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> Either Condition a
-> Trace
-> n (Either Condition a, Trace)
simplifyExecution Settings n a
settings ConcurrencyState
cstate0 forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run ThreadId
nTId IORefId
nCRId Either Condition a
res Trace
trace
        ((Either Condition a, Trace)
shrunk (Either Condition a, Trace)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall a. a -> [a] -> [a]
:) ([(Either Condition a, Trace)] -> [(Either Condition a, Trace)])
-> n [(Either Condition a, Trace)]
-> n [(Either Condition a, Trace)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s

  earlyExit :: Either Condition a -> Bool
earlyExit = (Either Condition a -> Bool)
-> Maybe (Either Condition a -> Bool) -> Either Condition a -> Bool
forall a. a -> Maybe a -> a
fromMaybe (Bool -> Either Condition a -> Bool
forall a b. a -> b -> a
const Bool
False) (Settings n a -> Maybe (Either Condition a -> Bool)
forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Bool)
_earlyExit Settings n a
settings)
  discard :: Either Condition a -> Maybe Discard
discard = (Either Condition a -> Maybe Discard)
-> Maybe (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall a. a -> Maybe a -> a
fromMaybe (Maybe Discard -> Either Condition a -> Maybe Discard
forall a b. a -> b -> a
const Maybe Discard
forall a. Maybe a
Nothing) (Settings n a -> Maybe (Either Condition a -> Maybe Discard)
forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Maybe Discard)
_discard Settings n a
settings)
  hideAborts :: Bool
hideAborts = Bool -> Bool
not (Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_showAborts Settings n a
settings)

-- | Given a result and a trace, produce a more minimal trace.
--
-- In principle, simplification is semantics preserving and can be
-- done without needing to execute the computation again.  However,
-- there are two good reasons to do so:
--
--  * It's a sanity check that there are no bugs.
--  * It's easier to generate a reduced sequence of scheduling
--    decisions and let dejafu generate the full trace, than to
--    generate a reduced trace directly
--
-- Unlike shrinking in randomised property-testing tools like
-- QuickCheck or Hedgehog, we only run the test case /once/, at the
-- end, rather than after every simplification step.
simplifyExecution :: (MonadDejaFu n, HasCallStack)
  => Settings n a
  -- ^ The SCT settings ('Way' is ignored)
  -> ConcurrencyState
  -- ^ The initial concurrency state
  -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
  -- ^ Just run the computation
  -> ThreadId
  -- ^ The first available @ThreadId@
  -> IORefId
  -- ^ The first available @IORefId@
  -> Either Condition a
  -- ^ The expected result
  -> Trace
  -> n (Either Condition a, Trace)
simplifyExecution :: Settings n a
-> ConcurrencyState
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> Either Condition a
-> Trace
-> n (Either Condition a, Trace)
simplifyExecution Settings n a
settings ConcurrencyState
cstate0 forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run ThreadId
nTId IORefId
nCRId Either Condition a
res Trace
trace
    | [(ThreadId, ThreadAction)]
tidTrace [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(ThreadId, ThreadAction)]
simplifiedTrace = do
        String -> n ()
debugPrint (String
"Simplifying new result '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"': no simplification possible!")
        (Either Condition a, Trace) -> n (Either Condition a, Trace)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res, Trace
trace)
    | Bool
otherwise = do
        String -> n ()
debugPrint (String
"Simplifying new result '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"': OK!")
        (Either Condition a
res', [(ThreadId, ThreadAction)]
_, Trace
trace') <- (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> [(ThreadId, ThreadAction)]
-> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
forall (n :: * -> *) a.
MonadDejaFu n =>
(forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> [(ThreadId, ThreadAction)]
-> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
replay forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
fixup [(ThreadId, ThreadAction)]
simplifiedTrace)
        case (Settings n a -> Maybe (a -> a -> Bool)
forall (n :: * -> *) a. Settings n a -> Maybe (a -> a -> Bool)
_equality Settings n a
settings, Either Condition a
res, Either Condition a
res') of
          (Just a -> a -> Bool
f,  Right a
a1, Right a
a2) | a -> a -> Bool
f a
a1 a
a2  -> (Either Condition a, Trace) -> n (Either Condition a, Trace)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res', Trace
trace')
          (Maybe (a -> a -> Bool)
_,       Left  Condition
e1, Left  Condition
e2) | Condition
e1 Condition -> Condition -> Bool
forall a. Eq a => a -> a -> Bool
== Condition
e2 -> (Either Condition a, Trace) -> n (Either Condition a, Trace)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res', Trace
trace')
          (Maybe (a -> a -> Bool)
Nothing, Right a
_,  Right a
_) -> (Either Condition a, Trace) -> n (Either Condition a, Trace)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res', Trace
trace') -- this is a risky case!
          (Maybe (a -> a -> Bool), Either Condition a, Either Condition a)
_ -> do
            String -> n ()
debugFatal (String
"Got a different result after simplifying: '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' /= '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'")
            (Either Condition a, Trace) -> n (Either Condition a, Trace)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res, Trace
trace)
  where
    tidTrace :: [(ThreadId, ThreadAction)]
tidTrace = Trace -> [(ThreadId, ThreadAction)]
toTIdTrace Trace
trace
    simplifiedTrace :: [(ThreadId, ThreadAction)]
simplifiedTrace = Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
simplify (Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_safeIO Settings n a
settings) (Settings n a -> MemType
forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) ConcurrencyState
cstate0 [(ThreadId, ThreadAction)]
tidTrace
    fixup :: [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
fixup = MemType
-> Int
-> Int
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
renumber (Settings n a -> MemType
forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) (ThreadId -> Int
forall a. Coercible a Id => a -> Int
fromId ThreadId
nTId) (IORefId -> Int
forall a. Coercible a Id => a -> Int
fromId IORefId
nCRId)

    debugFatal :: String -> n ()
debugFatal = if Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_debugFatal Settings n a
settings then String -> n ()
forall a. HasCallStack => String -> a
fatal else String -> n ()
debugPrint
    debugPrint :: String -> n ()
debugPrint = (String -> n ()) -> Maybe (String -> n ()) -> String -> n ()
forall a. a -> Maybe a -> a
fromMaybe (n () -> String -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())) (Settings n a -> Maybe (String -> n ())
forall (n :: * -> *) a. Settings n a -> Maybe (String -> n ())
_debugPrint Settings n a
settings)
    debugShow :: a -> String
debugShow = (a -> String) -> Maybe (a -> String) -> a -> String
forall a. a -> Maybe a -> a
fromMaybe (String -> a -> String
forall a b. a -> b -> a
const String
"_") (Settings n a -> Maybe (a -> String)
forall (n :: * -> *) a. Settings n a -> Maybe (a -> String)
_debugShow Settings n a
settings)
    p :: Either Condition a -> String
p = (Condition -> String)
-> (a -> String) -> Either Condition a -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> String
forall a. Show a => a -> String
show a -> String
debugShow

-- | Replay an execution.
replay :: MonadDejaFu n
  => (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
  -- ^ Run the computation
  -> [(ThreadId, ThreadAction)]
  -- ^ The reduced sequence of scheduling decisions
  -> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
replay :: (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> [(ThreadId, ThreadAction)]
-> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
replay forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run = Scheduler [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
-> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run ((Maybe (ThreadId, ThreadAction)
 -> NonEmpty (ThreadId, Lookahead)
 -> ConcurrencyState
 -> [(ThreadId, ThreadAction)]
 -> (Maybe ThreadId, [(ThreadId, ThreadAction)]))
-> Scheduler [(ThreadId, ThreadAction)]
forall state.
(Maybe (ThreadId, ThreadAction)
 -> NonEmpty (ThreadId, Lookahead)
 -> ConcurrencyState
 -> state
 -> (Maybe ThreadId, state))
-> Scheduler state
Scheduler ((NonEmpty (ThreadId, Lookahead)
 -> ConcurrencyState
 -> [(ThreadId, ThreadAction)]
 -> (Maybe ThreadId, [(ThreadId, ThreadAction)]))
-> Maybe (ThreadId, ThreadAction)
-> NonEmpty (ThreadId, Lookahead)
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> (Maybe ThreadId, [(ThreadId, ThreadAction)])
forall a b. a -> b -> a
const NonEmpty (ThreadId, Lookahead)
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> (Maybe ThreadId, [(ThreadId, ThreadAction)])
forall (t :: * -> *) b a b t.
(Foldable t, Coercible b Id, Coercible a Id) =>
t (b, b)
-> t -> [(a, ThreadAction)] -> (Maybe b, [(a, ThreadAction)])
sched)) where
    sched :: t (b, b)
-> t -> [(a, ThreadAction)] -> (Maybe b, [(a, ThreadAction)])
sched t (b, b)
runnable t
cs ((a
t, ThreadAction
Stop):[(a, ThreadAction)]
ts) = case a -> t (b, b) -> Maybe b
forall (t :: * -> *) b a b.
(Foldable t, Coercible b Id, Coercible a Id) =>
a -> t (b, b) -> Maybe b
findThread a
t t (b, b)
runnable of
      Just b
t' -> (b -> Maybe b
forall a. a -> Maybe a
Just b
t', [(a, ThreadAction)]
ts)
      Maybe b
Nothing -> t (b, b)
-> t -> [(a, ThreadAction)] -> (Maybe b, [(a, ThreadAction)])
sched t (b, b)
runnable t
cs [(a, ThreadAction)]
ts
    sched t (b, b)
runnable t
_ ((a
t, ThreadAction
_):[(a, ThreadAction)]
ts) = (a -> t (b, b) -> Maybe b
forall (t :: * -> *) b a b.
(Foldable t, Coercible b Id, Coercible a Id) =>
a -> t (b, b) -> Maybe b
findThread a
t t (b, b)
runnable, [(a, ThreadAction)]
ts)
    sched t (b, b)
_ t
_ [(a, ThreadAction)]
_ = (Maybe b
forall a. Maybe a
Nothing, [])

    -- find a thread ignoring names
    findThread :: a -> t (b, b) -> Maybe b
findThread a
tid0 =
      ((b, b) -> b) -> Maybe (b, b) -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b, b) -> b
forall a b. (a, b) -> a
fst (Maybe (b, b) -> Maybe b)
-> (t (b, b) -> Maybe (b, b)) -> t (b, b) -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b, b) -> Bool) -> t (b, b) -> Maybe (b, b)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(b
tid,b
_) -> b -> Int
forall a. Coercible a Id => a -> Int
fromId b
tid Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Int
forall a. Coercible a Id => a -> Int
fromId a
tid0)

-------------------------------------------------------------------------------
-- * Schedule simplification

-- | Simplify a trace by permuting adjacent independent actions to
-- reduce context switching.
simplify
  :: Bool
  -> MemType
  -> ConcurrencyState
  -> [(ThreadId, ThreadAction)]
  -> [(ThreadId, ThreadAction)]
simplify :: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
simplify Bool
safeIO MemType
memtype ConcurrencyState
cstate0 [(ThreadId, ThreadAction)]
trc0 = Int -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall t.
(Eq t, Num t) =>
t -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
loop ([(ThreadId, ThreadAction)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(ThreadId, ThreadAction)]
trc0) ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
prepare [(ThreadId, ThreadAction)]
trc0) where
  prepare :: [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
prepare = Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
dropCommits Bool
safeIO MemType
memtype ConcurrencyState
cstate0 ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
lexicoNormalForm Bool
safeIO MemType
memtype ConcurrencyState
cstate0
  step :: [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
step = Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
pushForward Bool
safeIO MemType
memtype ConcurrencyState
cstate0 ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
pullBack Bool
safeIO MemType
memtype ConcurrencyState
cstate0

  loop :: t -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
loop t
0 [(ThreadId, ThreadAction)]
trc = [(ThreadId, ThreadAction)]
trc
  loop t
n [(ThreadId, ThreadAction)]
trc =
    let trc' :: [(ThreadId, ThreadAction)]
trc' = [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
step [(ThreadId, ThreadAction)]
trc
    in if [(ThreadId, ThreadAction)]
trc' [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [(ThreadId, ThreadAction)]
trc then t -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
loop (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) [(ThreadId, ThreadAction)]
trc' else [(ThreadId, ThreadAction)]
trc

-- | Put a trace into lexicographic (by thread ID) normal form.
lexicoNormalForm
  :: Bool
  -> MemType
  -> ConcurrencyState
  -> [(ThreadId, ThreadAction)]
  -> [(ThreadId, ThreadAction)]
lexicoNormalForm :: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
lexicoNormalForm Bool
safeIO MemType
memtype ConcurrencyState
cstate0 = [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go where
  go :: [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go [(ThreadId, ThreadAction)]
trc =
    let trc' :: [(ThreadId, ThreadAction)]
trc' = Bool
-> MemType
-> ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
permuteBy Bool
safeIO MemType
memtype ConcurrencyState
cstate0 ((ThreadId -> ThreadId -> Bool) -> [ThreadId -> ThreadId -> Bool]
forall a. a -> [a]
repeat ThreadId -> ThreadId -> Bool
forall a. Ord a => a -> a -> Bool
(>)) [(ThreadId, ThreadAction)]
trc
    in if [(ThreadId, ThreadAction)]
trc [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(ThreadId, ThreadAction)]
trc' then [(ThreadId, ThreadAction)]
trc else [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go [(ThreadId, ThreadAction)]
trc'

-- | Swap adjacent independent actions in the trace if a predicate
-- holds.
permuteBy
  :: Bool
  -> MemType
  -> ConcurrencyState
  -> [ThreadId -> ThreadId -> Bool]
  -> [(ThreadId, ThreadAction)]
  -> [(ThreadId, ThreadAction)]
permuteBy :: Bool
-> MemType
-> ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
permuteBy Bool
safeIO MemType
memtype = ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go where
  go :: ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds (ThreadId -> ThreadId -> Bool
p:[ThreadId -> ThreadId -> Bool]
ps) (t1 :: (ThreadId, ThreadAction)
t1@(ThreadId
tid1, ThreadAction
ta1):t2 :: (ThreadId, ThreadAction)
t2@(ThreadId
tid2, ThreadAction
ta2):[(ThreadId, ThreadAction)]
trc)
    | Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
independent Bool
safeIO ConcurrencyState
ds ThreadId
tid1 ThreadAction
ta1 ThreadId
tid2 ThreadAction
ta2 Bool -> Bool -> Bool
&& ThreadId -> ThreadId -> Bool
p ThreadId
tid1 ThreadId
tid2 = ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go' ConcurrencyState
ds [ThreadId -> ThreadId -> Bool]
ps (ThreadId, ThreadAction)
t2 ((ThreadId, ThreadAction)
t1 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: [(ThreadId, ThreadAction)]
trc)
    | Bool
otherwise = ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go' ConcurrencyState
ds [ThreadId -> ThreadId -> Bool]
ps (ThreadId, ThreadAction)
t1 ((ThreadId, ThreadAction)
t2 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: [(ThreadId, ThreadAction)]
trc)
  go ConcurrencyState
_ [ThreadId -> ThreadId -> Bool]
_ [(ThreadId, ThreadAction)]
trc = [(ThreadId, ThreadAction)]
trc

  go' :: ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go' ConcurrencyState
ds [ThreadId -> ThreadId -> Bool]
ps t :: (ThreadId, ThreadAction)
t@(ThreadId
tid, ThreadAction
ta) [(ThreadId, ThreadAction)]
trc = (ThreadId, ThreadAction)
t (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go (MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid ThreadAction
ta) [ThreadId -> ThreadId -> Bool]
ps [(ThreadId, ThreadAction)]
trc

-- | Throw away commit actions which are followed by a memory barrier.
dropCommits
  :: Bool
  -> MemType
  -> ConcurrencyState
  -> [(ThreadId, ThreadAction)]
  -> [(ThreadId, ThreadAction)]
dropCommits :: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
dropCommits Bool
_ MemType
SequentialConsistency = ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
forall a b. a -> b -> a
const [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> a
id
dropCommits Bool
safeIO MemType
memtype = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go where
  go :: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds (t1 :: (ThreadId, ThreadAction)
t1@(ThreadId
tid1, ta1 :: ThreadAction
ta1@(CommitIORef ThreadId
_ IORefId
iorefid)):t2 :: (ThreadId, ThreadAction)
t2@(ThreadId
tid2, ThreadAction
ta2):[(ThreadId, ThreadAction)]
trc)
    | ActionType -> Bool
isBarrier (ThreadAction -> ActionType
simplifyAction ThreadAction
ta2) Bool -> Bool -> Bool
&& ConcurrencyState -> IORefId -> Int
numBuffered ConcurrencyState
ds IORefId
iorefid Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds ((ThreadId, ThreadAction)
t2(ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
:[(ThreadId, ThreadAction)]
trc)
    | Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
independent Bool
safeIO ConcurrencyState
ds ThreadId
tid1 ThreadAction
ta1 ThreadId
tid2 ThreadAction
ta2 = (ThreadId, ThreadAction)
t2 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go (MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid2 ThreadAction
ta2) ((ThreadId, ThreadAction)
t1(ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
:[(ThreadId, ThreadAction)]
trc)
  go ConcurrencyState
ds (t :: (ThreadId, ThreadAction)
t@(ThreadId
tid,ThreadAction
ta):[(ThreadId, ThreadAction)]
trc) = (ThreadId, ThreadAction)
t (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go (MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid ThreadAction
ta) [(ThreadId, ThreadAction)]
trc
  go ConcurrencyState
_ [] = []

-- | Attempt to reduce context switches by \"pulling\" thread actions
-- back to a prior execution of that thread.
--
-- Simple example, say we have @[(tidA, act1), (tidB, act2), (tidA,
-- act3)]@, where @act2@ and @act3@ are independent.  In this case
-- 'pullBack' will swap them, giving the sequence @[(tidA, act1),
-- (tidA, act3), (tidB, act2)]@.  It works for arbitrary separations.
pullBack
  :: Bool
  -> MemType
  -> ConcurrencyState
  -> [(ThreadId, ThreadAction)]
  -> [(ThreadId, ThreadAction)]
pullBack :: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
pullBack Bool
safeIO MemType
memtype = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go where
  go :: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds (t1 :: (ThreadId, ThreadAction)
t1@(ThreadId
tid1, ThreadAction
ta1):trc :: [(ThreadId, ThreadAction)]
trc@((ThreadId
tid2, ThreadAction
_):[(ThreadId, ThreadAction)]
_)) =
    let ds' :: ConcurrencyState
ds' = MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid1 ThreadAction
ta1
        trc' :: [(ThreadId, ThreadAction)]
trc' = if ThreadId
tid1 ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= ThreadId
tid2
               then [(ThreadId, ThreadAction)]
-> (((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
    -> [(ThreadId, ThreadAction)])
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [(ThreadId, ThreadAction)]
trc (((ThreadId, ThreadAction)
 -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (:)) (ThreadId
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
findAction ThreadId
tid1 ConcurrencyState
ds' [(ThreadId, ThreadAction)]
trc)
               else [(ThreadId, ThreadAction)]
trc
    in (ThreadId, ThreadAction)
t1 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds' [(ThreadId, ThreadAction)]
trc'
  go ConcurrencyState
_ [(ThreadId, ThreadAction)]
trc = [(ThreadId, ThreadAction)]
trc

  findAction :: ThreadId
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
findAction ThreadId
tid0 = ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
fgo where
    fgo :: ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
fgo ConcurrencyState
ds (t :: (ThreadId, ThreadAction)
t@(ThreadId
tid, ThreadAction
ta):[(ThreadId, ThreadAction)]
trc)
      | ThreadId
tid ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid0 = ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
forall a. a -> Maybe a
Just ((ThreadId, ThreadAction)
t, [(ThreadId, ThreadAction)]
trc)
      | Bool
otherwise = case ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
fgo (MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid ThreadAction
ta) [(ThreadId, ThreadAction)]
trc of
          Just (ft :: (ThreadId, ThreadAction)
ft@(ThreadId
ftid, ThreadAction
fa), [(ThreadId, ThreadAction)]
trc')
            | Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
independent Bool
safeIO ConcurrencyState
ds ThreadId
tid ThreadAction
ta ThreadId
ftid ThreadAction
fa -> ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
forall a. a -> Maybe a
Just ((ThreadId, ThreadAction)
ft, (ThreadId, ThreadAction)
t(ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
:[(ThreadId, ThreadAction)]
trc')
          Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
_ -> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
forall a. Maybe a
Nothing
    fgo ConcurrencyState
_ [(ThreadId, ThreadAction)]
_ = Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
forall a. Maybe a
Nothing

-- | Attempt to reduce context switches by \"pushing\" thread actions
-- forward to a future execution of that thread.
--
-- This is kind of the opposite of 'pullBack', but there are cases
-- where one applies but not the other.
--
-- Simple example, say we have @[(tidA, act1), (tidB, act2), (tidA,
-- act3)]@, where @act1@ and @act2@ are independent.  In this case
-- 'pushForward' will swap them, giving the sequence @[(tidB, act2),
-- (tidA, act1), (tidA, act3)]@.  It works for arbitrary separations.
pushForward
  :: Bool
  -> MemType
  -> ConcurrencyState
  -> [(ThreadId, ThreadAction)]
  -> [(ThreadId, ThreadAction)]
pushForward :: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
pushForward Bool
safeIO MemType
memtype = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go where
  go :: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds (t1 :: (ThreadId, ThreadAction)
t1@(ThreadId
tid1, ThreadAction
ta1):trc :: [(ThreadId, ThreadAction)]
trc@((ThreadId
tid2, ThreadAction
_):[(ThreadId, ThreadAction)]
_)) =
    let ds' :: ConcurrencyState
ds' = MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid1 ThreadAction
ta1
    in if ThreadId
tid1 ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= ThreadId
tid2
       then [(ThreadId, ThreadAction)]
-> ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> Maybe [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((ThreadId, ThreadAction)
t1 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds' [(ThreadId, ThreadAction)]
trc) (ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds) (ThreadId
-> ThreadAction
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe [(ThreadId, ThreadAction)]
findAction ThreadId
tid1 ThreadAction
ta1 ConcurrencyState
ds [(ThreadId, ThreadAction)]
trc)
       else (ThreadId, ThreadAction)
t1 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds' [(ThreadId, ThreadAction)]
trc
  go ConcurrencyState
_ [(ThreadId, ThreadAction)]
trc = [(ThreadId, ThreadAction)]
trc

  findAction :: ThreadId
-> ThreadAction
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe [(ThreadId, ThreadAction)]
findAction ThreadId
tid0 ThreadAction
ta0 = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> Maybe [(ThreadId, ThreadAction)]
fgo where
    fgo :: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> Maybe [(ThreadId, ThreadAction)]
fgo ConcurrencyState
ds (t :: (ThreadId, ThreadAction)
t@(ThreadId
tid, ThreadAction
ta):[(ThreadId, ThreadAction)]
trc)
      | ThreadId
tid ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid0 = [(ThreadId, ThreadAction)] -> Maybe [(ThreadId, ThreadAction)]
forall a. a -> Maybe a
Just ((ThreadId
tid0, ThreadAction
ta0) (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: (ThreadId, ThreadAction)
t (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: [(ThreadId, ThreadAction)]
trc)
      | Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
independent Bool
safeIO ConcurrencyState
ds ThreadId
tid0 ThreadAction
ta0 ThreadId
tid ThreadAction
ta = ((ThreadId, ThreadAction)
t(ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
:) ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> Maybe [(ThreadId, ThreadAction)]
-> Maybe [(ThreadId, ThreadAction)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConcurrencyState
-> [(ThreadId, ThreadAction)] -> Maybe [(ThreadId, ThreadAction)]
fgo (MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid ThreadAction
ta) [(ThreadId, ThreadAction)]
trc
      | Bool
otherwise = Maybe [(ThreadId, ThreadAction)]
forall a. Maybe a
Nothing
    fgo ConcurrencyState
_ [(ThreadId, ThreadAction)]
_ = Maybe [(ThreadId, ThreadAction)]
forall a. Maybe a
Nothing

-- | Re-number threads and IORefs.
--
-- Permuting forks or newIORefs makes the existing numbering invalid,
-- which then causes problems for scheduling.  Just re-numbering
-- threads isn't enough, as IORef IDs are used to determine commit
-- thread IDs.
--
-- Renumbered things will not fix their names, so don't rely on those
-- at all.
renumber
  :: MemType
  -- ^ The memory model determines how commit threads are numbered.
  -> Int
  -- ^ First free thread ID.
  -> Int
  -- ^ First free @IORef@ ID.
  -> [(ThreadId, ThreadAction)]
  -> [(ThreadId, ThreadAction)]
renumber :: MemType
-> Int
-> Int
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
renumber MemType
memtype Int
tid0 Int
crid0 = ((IntMap Int, Int, IntMap Int, Int), [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)]
forall a b. (a, b) -> b
snd (((IntMap Int, Int, IntMap Int, Int), [(ThreadId, ThreadAction)])
 -> [(ThreadId, ThreadAction)])
-> ([(ThreadId, ThreadAction)]
    -> ((IntMap Int, Int, IntMap Int, Int),
        [(ThreadId, ThreadAction)]))
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((IntMap Int, Int, IntMap Int, Int)
 -> (ThreadId, ThreadAction)
 -> ((IntMap Int, Int, IntMap Int, Int), (ThreadId, ThreadAction)))
-> (IntMap Int, Int, IntMap Int, Int)
-> [(ThreadId, ThreadAction)]
-> ((IntMap Int, Int, IntMap Int, Int), [(ThreadId, ThreadAction)])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (IntMap Int, Int, IntMap Int, Int)
-> (ThreadId, ThreadAction)
-> ((IntMap Int, Int, IntMap Int, Int), (ThreadId, ThreadAction))
go (IntMap Int
forall a. IntMap a
I.empty, Int
tid0, IntMap Int
forall a. IntMap a
I.empty, Int
crid0) where
  go :: (IntMap Int, Int, IntMap Int, Int)
-> (ThreadId, ThreadAction)
-> ((IntMap Int, Int, IntMap Int, Int), (ThreadId, ThreadAction))
go s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
cridmap, Int
_) (ThreadId
_, CommitIORef ThreadId
tid IORefId
crid) =
    let tid' :: ThreadId
tid'  = IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap  ThreadId
tid
        crid' :: IORefId
crid' = IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
crid
        act' :: ThreadAction
act' = ThreadId -> IORefId -> ThreadAction
CommitIORef ThreadId
tid' IORefId
crid'
    in case MemType
memtype of
         MemType
PartialStoreOrder -> ((IntMap Int, Int, IntMap Int, Int)
s, (ThreadId -> Maybe IORefId -> ThreadId
commitThreadId ThreadId
tid' (IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
crid'), ThreadAction
act'))
         MemType
_ -> ((IntMap Int, Int, IntMap Int, Int)
s, (ThreadId -> Maybe IORefId -> ThreadId
commitThreadId ThreadId
tid' Maybe IORefId
forall a. Maybe a
Nothing, ThreadAction
act'))
  go s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (ThreadId
tid, ThreadAction
act) =
    let ((IntMap Int, Int, IntMap Int, Int)
s', ThreadAction
act') = (IntMap Int, Int, IntMap Int, Int)
-> ThreadAction
-> ((IntMap Int, Int, IntMap Int, Int), ThreadAction)
updateAction (IntMap Int, Int, IntMap Int, Int)
s ThreadAction
act
    in ((IntMap Int, Int, IntMap Int, Int)
s', (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap ThreadId
tid, ThreadAction
act'))

  -- I can't help but feel there should be some generic programming
  -- solution to this sort of thing (and to the many other functions
  -- operating over @ThreadAction@s / @Lookahead@s)
  updateAction :: (IntMap Int, Int, IntMap Int, Int)
-> ThreadAction
-> ((IntMap Int, Int, IntMap Int, Int), ThreadAction)
updateAction (IntMap Int
tidmap, Int
nTId, IntMap Int
cridmap, Int
nCRId) (Fork ThreadId
old) =
    let tidmap' :: IntMap Int
tidmap' = Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
I.insert (ThreadId -> Int
forall a. Coercible a Id => a -> Int
fromId ThreadId
old) Int
nTId IntMap Int
tidmap
        nTId' :: Int
nTId' = Int
nTId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    in ((IntMap Int
tidmap', Int
nTId', IntMap Int
cridmap, Int
nCRId), ThreadId -> ThreadAction
Fork (Int -> ThreadId
forall a. Coercible Id a => Int -> a
toId Int
nTId))
  updateAction (IntMap Int
tidmap, Int
nTId, IntMap Int
cridmap, Int
nCRId) (ForkOS ThreadId
old) =
    let tidmap' :: IntMap Int
tidmap' = Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
I.insert (ThreadId -> Int
forall a. Coercible a Id => a -> Int
fromId ThreadId
old) Int
nTId IntMap Int
tidmap
        nTId' :: Int
nTId' = Int
nTId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    in ((IntMap Int
tidmap', Int
nTId', IntMap Int
cridmap, Int
nCRId), ThreadId -> ThreadAction
ForkOS (Int -> ThreadId
forall a. Coercible Id a => Int -> a
toId Int
nTId))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (PutMVar MVarId
mvid [ThreadId]
olds) =
    ((IntMap Int, Int, IntMap Int, Int)
s, MVarId -> [ThreadId] -> ThreadAction
PutMVar MVarId
mvid ((ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap) [ThreadId]
olds))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (TryPutMVar MVarId
mvid Bool
b [ThreadId]
olds) =
    ((IntMap Int, Int, IntMap Int, Int)
s, MVarId -> Bool -> [ThreadId] -> ThreadAction
TryPutMVar MVarId
mvid Bool
b ((ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap) [ThreadId]
olds))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (TakeMVar MVarId
mvid [ThreadId]
olds) =
    ((IntMap Int, Int, IntMap Int, Int)
s, MVarId -> [ThreadId] -> ThreadAction
TakeMVar MVarId
mvid ((ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap) [ThreadId]
olds))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (TryTakeMVar MVarId
mvid Bool
b [ThreadId]
olds) =
    ((IntMap Int, Int, IntMap Int, Int)
s, MVarId -> Bool -> [ThreadId] -> ThreadAction
TryTakeMVar MVarId
mvid Bool
b ((ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap) [ThreadId]
olds))
  updateAction (IntMap Int
tidmap, Int
nTId, IntMap Int
cridmap, Int
nCRId) (NewIORef IORefId
old) =
    let cridmap' :: IntMap Int
cridmap' = Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
I.insert (IORefId -> Int
forall a. Coercible a Id => a -> Int
fromId IORefId
old) Int
nCRId IntMap Int
cridmap
        nCRId' :: Int
nCRId' = Int
nCRId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    in ((IntMap Int
tidmap, Int
nTId, IntMap Int
cridmap', Int
nCRId'), IORefId -> ThreadAction
NewIORef (Int -> IORefId
forall a. Coercible Id a => Int -> a
toId Int
nCRId))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (ReadIORef IORefId
old) =
    ((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> ThreadAction
ReadIORef (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (ReadIORefCas IORefId
old) =
    ((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> ThreadAction
ReadIORefCas (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (ModIORef IORefId
old) =
    ((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> ThreadAction
ModIORef (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (ModIORefCas IORefId
old) =
    ((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> ThreadAction
ModIORefCas (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (WriteIORef IORefId
old) =
    ((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> ThreadAction
WriteIORef (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (CasIORef IORefId
old Bool
b) =
    ((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> Bool -> ThreadAction
CasIORef (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old) Bool
b)
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (STM [TAction]
tas [ThreadId]
olds) =
    ((IntMap Int, Int, IntMap Int, Int)
s, [TAction] -> [ThreadId] -> ThreadAction
STM [TAction]
tas ((ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap) [ThreadId]
olds))
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (ThrowTo ThreadId
old Maybe MaskingState
ms) =
    ((IntMap Int, Int, IntMap Int, Int)
s, ThreadId -> Maybe MaskingState -> ThreadAction
ThrowTo (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap ThreadId
old) Maybe MaskingState
ms)
  updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (BlockedThrowTo ThreadId
old) =
    ((IntMap Int, Int, IntMap Int, Int)
s, ThreadId -> ThreadAction
BlockedThrowTo (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap ThreadId
old))
  updateAction (IntMap Int, Int, IntMap Int, Int)
s ThreadAction
act = ((IntMap Int, Int, IntMap Int, Int)
s, ThreadAction
act)

  renumbered :: (Coercible a Id, Coercible Id a) => I.IntMap Int -> a -> a
  renumbered :: IntMap Int -> a -> a
renumbered IntMap Int
idmap a
id_ = Int -> a
forall a. Coercible Id a => Int -> a
toId (Int -> a) -> Int -> a
forall a b. (a -> b) -> a -> b
$ Int -> Int -> IntMap Int -> Int
forall a. a -> Int -> IntMap a -> a
I.findWithDefault (a -> Int
forall a. Coercible a Id => a -> Int
fromId a
id_) (a -> Int
forall a. Coercible a Id => a -> Int
fromId a
id_) IntMap Int
idmap

-------------------------------------------------------------------------------
-- * Utilities

-- | Helper function for constructing IDs of any sort.
toId :: Coercible Id a => Int -> a
toId :: Int -> a
toId = Id -> a
coerce (Id -> a) -> (Int -> Id) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe String -> Int -> Id
Id Maybe String
forall a. Maybe a
Nothing

-- | Helper function for deconstructing IDs of any sort.
fromId :: Coercible a Id => a -> Int
fromId :: a -> Int
fromId a
a = let (Id Maybe String
_ Int
id_) = a -> Id
coerce a
a in Int
id_