{-# 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 :: forall (n :: * -> *) a s t g pty.
(MonadDejaFu n, HasCallStack) =>
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 = 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (Right Snapshot pty n a
snap, Trace
_) -> forall {pty}. Snapshot pty n a -> n [(Either Condition a, Trace)]
sct'Snap Snapshot pty n a
snap
    Just (Left Condition
f, Trace
trace) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [(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 = 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 forall {s}. Scheduler s -> s -> n (Either Condition a, s, Trace)
runFull)
      forall {s}. Scheduler s -> s -> n (Either Condition a, s, Trace)
runFull
      (forall a. Coercible Id a => Int -> a
toId Int
1)
      (forall a. Coercible Id a => Int -> a
toId Int
1)

    sct'Snap :: Snapshot pty n a -> n [(Either Condition a, Trace)]
sct'Snap Snapshot pty n a
snap =
      let idsrc :: IdSource
idsrc = forall (n :: * -> *) g. Context n g -> IdSource
cIdSource (forall p (n :: * -> *) a. Snapshot p n a -> Context n ()
contextFromSnapshot Snapshot pty n a
snap)
          cstate :: ConcurrencyState
cstate = forall (n :: * -> *) g. Context n g -> ConcurrencyState
cCState (forall p (n :: * -> *) a. Snapshot p n a -> Context n ()
contextFromSnapshot Snapshot pty n a
snap)
      in 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 (forall a b. (a, b) -> a
fst (forall p (n :: * -> *) a.
Snapshot p n a -> ([ThreadId], [ThreadId])
threadsFromSnapshot Snapshot pty 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 (forall {n :: * -> *} {pty} {a} {s}.
MonadDejaFu n =>
Snapshot pty n a
-> Scheduler s -> s -> n (Either Condition a, s, Trace)
runSnap Snapshot pty n a
snap))
         (forall {n :: * -> *} {pty} {a} {s}.
MonadDejaFu n =>
Snapshot pty n a
-> Scheduler s -> s -> n (Either Condition a, s, Trace)
runSnap Snapshot pty n a
snap)
         (forall a. Coercible Id a => Int -> a
toId forall a b. (a -> b) -> a -> b
$ Int
1 forall a. Num a => a -> a -> a
+ forall a b. (a, b) -> a
fst (IdSource -> (Int, [String])
_tids IdSource
idsrc))
         (forall a. Coercible Id a => Int -> a
toId forall a b. (a -> b) -> a -> b
$ Int
1 forall a. Num a => a -> a -> a
+ 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 = 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 (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 = 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 (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' :: 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
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 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 = 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 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 (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 forall a. Maybe a
Nothing [Either Condition a]
seen s
s'
    Maybe t
Nothing -> 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 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 forall a. Eq a => a -> a -> Bool
== a
e2
          eq t -> t -> Bool
_ Either a t
_ Either a t
_ = Bool
False
      in if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (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 (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
resforall 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, []) forall a. a -> [a] -> [a]
:) 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 (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 (forall (n :: * -> *) a. Settings n a -> Bool
_simplify Settings n a
settings) = ((Either Condition a
res, Trace
trace) forall a. a -> [a] -> [a]
:) 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 (forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s
    | Bool
otherwise = do
        (Either Condition a, Trace)
shrunk <- 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 forall a. a -> [a] -> [a]
:) 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 (forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s

  earlyExit :: Either Condition a -> Bool
earlyExit = forall a. a -> Maybe a -> a
fromMaybe (forall a b. a -> b -> a
const Bool
False) (forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Bool)
_earlyExit Settings n a
settings)
  discard :: Either Condition a -> Maybe Discard
discard = forall a. a -> Maybe a -> a
fromMaybe (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) (forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Maybe Discard)
_discard Settings n a
settings)
  hideAborts :: Bool
hideAborts = Bool -> Bool
not (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 :: 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
    | [(ThreadId, ThreadAction)]
tidTrace forall a. Eq a => a -> a -> Bool
== [(ThreadId, ThreadAction)]
simplifiedTrace = do
        String -> n ()
debugPrint (String
"Simplifying new result '" forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res forall a. [a] -> [a] -> [a]
++ String
"': no simplification possible!")
        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 '" forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res forall a. [a] -> [a] -> [a]
++ String
"': OK!")
        (Either Condition a
res', [(ThreadId, ThreadAction)]
_, Trace
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 (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  -> 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 forall a. Eq a => a -> a -> Bool
== Condition
e2 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res', Trace
trace')
          (Maybe (a -> a -> Bool)
Nothing, Right a
_,  Right a
_) -> 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: '" forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res forall a. [a] -> [a] -> [a]
++ String
"' /= '" forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res' forall a. [a] -> [a] -> [a]
++ String
"'")
            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 (forall (n :: * -> *) a. Settings n a -> Bool
_safeIO Settings n a
settings) (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 (forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) (forall a. Coercible a Id => a -> Int
fromId ThreadId
nTId) (forall a. Coercible a Id => a -> Int
fromId IORefId
nCRId)

    debugFatal :: String -> n ()
debugFatal = if forall (n :: * -> *) a. Settings n a -> Bool
_debugFatal Settings n a
settings then forall a. HasCallStack => String -> a
fatal else String -> n ()
debugPrint
    debugPrint :: String -> n ()
debugPrint = forall a. a -> Maybe a -> a
fromMaybe (forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())) (forall (n :: * -> *) a. Settings n a -> Maybe (String -> n ())
_debugPrint Settings n a
settings)
    debugShow :: a -> String
debugShow = forall a. a -> Maybe a -> a
fromMaybe (forall a b. a -> b -> a
const String
"_") (forall (n :: * -> *) a. Settings n a -> Maybe (a -> String)
_debugShow Settings n a
settings)
    p :: Either Condition a -> String
p = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either 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 (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 = forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run (forall state.
(Maybe (ThreadId, ThreadAction)
 -> NonEmpty (ThreadId, Lookahead)
 -> ConcurrencyState
 -> state
 -> (Maybe ThreadId, state))
-> Scheduler state
Scheduler (forall a b. a -> b -> a
const forall {a} {a} {t :: * -> *} {b} {t}.
(Coercible a Id, Coercible a Id, Foldable t) =>
t (a, b)
-> t -> [(a, ThreadAction)] -> (Maybe a, [(a, ThreadAction)])
sched)) where
    sched :: t (a, b)
-> t -> [(a, ThreadAction)] -> (Maybe a, [(a, ThreadAction)])
sched t (a, b)
runnable t
cs ((a
t, ThreadAction
Stop):[(a, ThreadAction)]
ts) = case forall {a} {a} {t :: * -> *} {b}.
(Coercible a Id, Coercible a Id, Foldable t) =>
a -> t (a, b) -> Maybe a
findThread a
t t (a, b)
runnable of
      Just a
t' -> (forall a. a -> Maybe a
Just a
t', [(a, ThreadAction)]
ts)
      Maybe a
Nothing -> t (a, b)
-> t -> [(a, ThreadAction)] -> (Maybe a, [(a, ThreadAction)])
sched t (a, b)
runnable t
cs [(a, ThreadAction)]
ts
    sched t (a, b)
runnable t
_ ((a
t, ThreadAction
_):[(a, ThreadAction)]
ts) = (forall {a} {a} {t :: * -> *} {b}.
(Coercible a Id, Coercible a Id, Foldable t) =>
a -> t (a, b) -> Maybe a
findThread a
t t (a, b)
runnable, [(a, ThreadAction)]
ts)
    sched t (a, b)
_ t
_ [(a, ThreadAction)]
_ = (forall a. Maybe a
Nothing, [])

    -- find a thread ignoring names
    findThread :: a -> t (a, b) -> Maybe a
findThread a
tid0 =
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(a
tid,b
_) -> forall a. Coercible a Id => a -> Int
fromId a
tid forall a. Eq a => a -> a -> Bool
== 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 = forall {t}.
(Eq t, Num t) =>
t -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
loop (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 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 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' forall a. Eq a => a -> a -> Bool
/= [(ThreadId, ThreadAction)]
trc then t -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
loop (t
nforall 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 (forall a. a -> [a]
repeat forall a. Ord a => a -> a -> Bool
(>)) [(ThreadId, ThreadAction)]
trc
    in if [(ThreadId, ThreadAction)]
trc 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 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 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 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 = forall a b. a -> b -> a
const 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 forall a. Eq a => a -> a -> Bool
== Int
1 = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds ((ThreadId, ThreadAction)
t2forall 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 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)
t1forall a. a -> [a] -> [a]
:[(ThreadId, ThreadAction)]
trc)
  go ConcurrencyState
ds (t :: (ThreadId, ThreadAction)
t@(ThreadId
tid,ThreadAction
ta):[(ThreadId, ThreadAction)]
trc) = (ThreadId, ThreadAction)
t 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 forall a. Eq a => a -> a -> Bool
/= ThreadId
tid2
               then forall b a. b -> (a -> b) -> Maybe a -> b
maybe [(ThreadId, ThreadAction)]
trc (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 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 forall a. Eq a => a -> a -> Bool
== ThreadId
tid0 = 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 -> forall a. a -> Maybe a
Just ((ThreadId, ThreadAction)
ft, (ThreadId, ThreadAction)
tforall a. a -> [a] -> [a]
:[(ThreadId, ThreadAction)]
trc')
          Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
_ -> forall a. Maybe a
Nothing
    fgo ConcurrencyState
_ [(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 forall a. Eq a => a -> a -> Bool
/= ThreadId
tid2
       then forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((ThreadId, ThreadAction)
t1 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 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 forall a. Eq a => a -> a -> Bool
== ThreadId
tid0 = forall a. a -> Maybe a
Just ((ThreadId
tid0, ThreadAction
ta0) forall a. a -> [a] -> [a]
: (ThreadId, ThreadAction)
t 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)
tforall a. a -> [a] -> [a]
:) 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 = forall a. Maybe a
Nothing
    fgo ConcurrencyState
_ [(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 = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL (IntMap Int, Int, IntMap Int, Int)
-> (ThreadId, ThreadAction)
-> ((IntMap Int, Int, IntMap Int, Int), (ThreadId, ThreadAction))
go (forall a. IntMap a
I.empty, Int
tid0, 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'  = forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap  ThreadId
tid
        crid' :: IORefId
crid' = 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' (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' 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', (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' = forall a. Int -> a -> IntMap a -> IntMap a
I.insert (forall a. Coercible a Id => a -> Int
fromId ThreadId
old) Int
nTId IntMap Int
tidmap
        nTId' :: Int
nTId' = Int
nTId forall a. Num a => a -> a -> a
+ Int
1
    in ((IntMap Int
tidmap', Int
nTId', IntMap Int
cridmap, Int
nCRId), ThreadId -> ThreadAction
Fork (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' = forall a. Int -> a -> IntMap a -> IntMap a
I.insert (forall a. Coercible a Id => a -> Int
fromId ThreadId
old) Int
nTId IntMap Int
tidmap
        nTId' :: Int
nTId' = Int
nTId forall a. Num a => a -> a -> a
+ Int
1
    in ((IntMap Int
tidmap', Int
nTId', IntMap Int
cridmap, Int
nCRId), ThreadId -> ThreadAction
ForkOS (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 (forall a b. (a -> b) -> [a] -> [b]
map (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 (forall a b. (a -> b) -> [a] -> [b]
map (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 (forall a b. (a -> b) -> [a] -> [b]
map (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 (forall a b. (a -> b) -> [a] -> [b]
map (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' = forall a. Int -> a -> IntMap a -> IntMap a
I.insert (forall a. Coercible a Id => a -> Int
fromId IORefId
old) Int
nCRId IntMap Int
cridmap
        nCRId' :: Int
nCRId' = Int
nCRId forall a. Num a => a -> a -> a
+ Int
1
    in ((IntMap Int
tidmap, Int
nTId, IntMap Int
cridmap', Int
nCRId'), IORefId -> ThreadAction
NewIORef (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 (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 (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 (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 (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 (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 (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 (forall a b. (a -> b) -> [a] -> [b]
map (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 (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 (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 :: forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
idmap a
id_ = forall a. Coercible Id a => Int -> a
toId forall a b. (a -> b) -> a -> b
$ forall a. a -> Int -> IntMap a -> a
I.findWithDefault (forall a. Coercible a Id => a -> Int
fromId a
id_) (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 :: forall a. Coercible Id a => Int -> a
toId = coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe String -> Int -> Id
Id forall a. Maybe a
Nothing

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