{-# LANGUAGE ExplicitNamespaces  #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections       #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}
module Control.Monad.IOSim
  ( -- * Simulation monad
    IOSim
  , STMSim
    -- ** Run simulation
  , runSim
  , runSimOrThrow
  , runSimStrictShutdown
  , Failure (..)
  , runSimTrace
  , runSimTraceST
    -- ** Explore races using /IOSimPOR/
    -- $iosimpor
  , exploreSimTrace
  , controlSimTrace
  , ScheduleMod (..)
  , ScheduleControl (..)
    -- *** Exploration options
  , ExplorationSpec
  , ExplorationOptions (..)
  , stdExplorationOptions
  , withScheduleBound
  , withBranching
  , withStepTimelimit
  , withReplay
    -- * Lift ST computations
  , liftST
    -- * Simulation time
  , setCurrentTime
  , unshareClock
    -- * Simulation trace
  , type SimTrace
  , Trace (Cons, Nil, SimTrace, SimPORTrace, TraceDeadlock, TraceLoop, TraceMainReturn, TraceMainException, TraceRacesFound)
  , SimResult (..)
  , SimEvent (..)
  , SimEventType (..)
  , ThreadLabel
  , Labelled (..)
    -- ** Dynamic Tracing
  , traceM
  , traceSTM
    -- ** Pretty printers
  , ppTrace
  , ppTrace_
  , ppEvents
  , ppSimEvent
  , ppDebug
    -- ** Selectors
  , traceEvents
  , traceResult
    -- *** list selectors
  , selectTraceEvents
  , selectTraceEvents'
  , selectTraceEventsDynamic
  , selectTraceEventsDynamicWithTime
  , selectTraceEventsDynamic'
  , selectTraceEventsDynamicWithTime'
  , selectTraceEventsSay
  , selectTraceEventsSayWithTime
  , selectTraceEventsSay'
  , selectTraceEventsSayWithTime'
  , selectTraceRaces
    -- *** trace selectors
  , traceSelectTraceEvents
  , traceSelectTraceEventsDynamic
  , traceSelectTraceEventsSay
    -- ** IO printer
  , printTraceEventsSay
    -- * Eventlog
  , EventlogEvent (..)
  , EventlogMarker (..)
    -- * Low-level API
  , newTimeout
  , readTimeout
  , cancelTimeout
  , awaitTimeout
  ) where

import           Prelude

import           Data.Bifoldable
import           Data.Dynamic (fromDynamic)
import           Data.List (intercalate)
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Typeable (Typeable)

import           Data.List.Trace (Trace (..))

import           Control.Exception (throw)

import           Control.Monad.ST.Lazy

import           Control.Monad.Class.MonadThrow as MonadThrow

import           Control.Monad.IOSim.Internal (runSimTraceST)
import           Control.Monad.IOSim.Types
import           Control.Monad.IOSimPOR.Internal (controlSimTraceST)
import           Control.Monad.IOSimPOR.QuickCheckUtils

import           Test.QuickCheck


import           Data.IORef
import           System.IO.Unsafe


selectTraceEvents
    :: (Time -> SimEventType -> Maybe b)
    -> SimTrace a
    -> [b]
selectTraceEvents :: forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents Time -> SimEventType -> Maybe b
fn =
      forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr ( \ SimResult a
v [b]
_
               -> case SimResult a
v of
                    MainException Time
_ SomeException
e [Labelled ThreadId]
_       -> forall a e. Exception e => e -> a
throw (SomeException -> Failure
FailureException SomeException
e)
                    Deadlock      Time
_   [Labelled ThreadId]
threads -> forall a e. Exception e => e -> a
throw ([Labelled ThreadId] -> Failure
FailureDeadlock [Labelled ThreadId]
threads)
                    MainReturn    Time
_ a
_ [Labelled ThreadId]
_       -> []
                    SimResult a
Loop                      -> forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: selectTraceEvents _ TraceLoop{}"
              )
              ( \ b
b [b]
acc -> b
b forall a. a -> [a] -> [a]
: [b]
acc )
              []
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a.
(Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents Time -> SimEventType -> Maybe b
fn

selectTraceEvents'
    :: (Time ->  SimEventType -> Maybe b)
    -> SimTrace a
    -> [b]
selectTraceEvents' :: forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' Time -> SimEventType -> Maybe b
fn =
      forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr ( \ SimResult a
_ [b]
_   -> []  )
              ( \ b
b [b]
acc -> b
b forall a. a -> [a] -> [a]
: [b]
acc )
              []
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a.
(Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents Time -> SimEventType -> Maybe b
fn

selectTraceRaces :: SimTrace a -> [ScheduleControl]
selectTraceRaces :: forall a. SimTrace a -> [ScheduleControl]
selectTraceRaces = forall a. SimTrace a -> [ScheduleControl]
go
  where
    go :: SimTrace a -> [ScheduleControl]
go (SimTrace Time
_ ThreadId
_ Maybe [Char]
_ SimEventType
_ SimTrace a
trace)      = SimTrace a -> [ScheduleControl]
go SimTrace a
trace
    go (SimPORTrace Time
_ ThreadId
_ Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
trace) = SimTrace a -> [ScheduleControl]
go SimTrace a
trace
    go (TraceRacesFound [ScheduleControl]
races SimTrace a
trace) =
      [ScheduleControl]
races forall a. [a] -> [a] -> [a]
++ SimTrace a -> [ScheduleControl]
go SimTrace a
trace
    go SimTrace a
_                             = []

-- Extracting races from a trace.  There is a subtlety in doing so: we
-- must return a defined list of races even in the case where the
-- trace is infinite, and there are no races occurring in it! For
-- example, if the system falls into a deterministic infinite loop,
-- then there will be no races to find.

-- In reality we only want to extract races from *the part of the
-- trace used in a test*. We can only observe that by tracking lazy
-- evaluation: only races that were found in the evaluated prefix of
-- an infinite trace should contribute to the "races found". Hence we
-- return a function that returns the races found "so far". This is
-- unsafe, of course, since that function may return different results
-- at different times.

detachTraceRaces :: SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces :: forall a. SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces SimTrace a
trace = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
  IORef [[ScheduleControl]]
races <- forall a. a -> IO (IORef a)
newIORef []
  let readRaces :: () -> [ScheduleControl]
readRaces ()  = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef [[ScheduleControl]]
races
      saveRaces :: [ScheduleControl] -> a -> a
saveRaces [ScheduleControl]
r a
t = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
                        forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [[ScheduleControl]]
races ([ScheduleControl]
rforall a. a -> [a] -> [a]
:)
                        forall (m :: * -> *) a. Monad m => a -> m a
return a
t
  let go :: SimTrace a -> SimTrace a
go (SimTrace Time
a ThreadId
b Maybe [Char]
c SimEventType
d SimTrace a
trace)      = forall a.
Time
-> ThreadId
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
a ThreadId
b Maybe [Char]
c SimEventType
d forall a b. (a -> b) -> a -> b
$ SimTrace a -> SimTrace a
go SimTrace a
trace
      go (SimPORTrace Time
a ThreadId
b Int
c Maybe [Char]
d SimEventType
e SimTrace a
trace) = forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
a ThreadId
b Int
c Maybe [Char]
d SimEventType
e forall a b. (a -> b) -> a -> b
$ SimTrace a -> SimTrace a
go SimTrace a
trace
      go (TraceRacesFound [ScheduleControl]
r SimTrace a
trace)     = forall {a}. [ScheduleControl] -> a -> a
saveRaces [ScheduleControl]
r forall a b. (a -> b) -> a -> b
$ SimTrace a -> SimTrace a
go SimTrace a
trace
      go SimTrace a
t                             = SimTrace a
t
  forall (m :: * -> *) a. Monad m => a -> m a
return (() -> [ScheduleControl]
readRaces, forall {a}. SimTrace a -> SimTrace a
go SimTrace a
trace)

-- | Select all the traced values matching the expected type. This relies on
-- the sim's dynamic trace facility.
--
-- For convenience, this throws exceptions for abnormal sim termination.
--
selectTraceEventsDynamic :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic = forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents Time -> SimEventType -> Maybe b
fn
  where
    fn :: Time -> SimEventType -> Maybe b
    fn :: Time -> SimEventType -> Maybe b
fn Time
_ (EventLog Dynamic
dyn) = forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsDynamic' but also captures time of the trace event.
--
selectTraceEventsDynamicWithTime :: forall a b. Typeable b => SimTrace a -> [(Time, b)]
selectTraceEventsDynamicWithTime :: forall a b. Typeable b => SimTrace a -> [(Time, b)]
selectTraceEventsDynamicWithTime = forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents Time -> SimEventType -> Maybe (Time, b)
fn
  where
    fn :: Time -> SimEventType -> Maybe (Time, b)
    fn :: Time -> SimEventType -> Maybe (Time, b)
fn Time
t (EventLog Dynamic
dyn) = (Time
t,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsDynamic' but returns partial trace if an exception
-- is found in it.
--
selectTraceEventsDynamic' :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic' :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic' = forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' Time -> SimEventType -> Maybe b
fn
  where
    fn :: Time -> SimEventType -> Maybe b
    fn :: Time -> SimEventType -> Maybe b
fn Time
_ (EventLog Dynamic
dyn) = forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = forall a. Maybe a
Nothing

-- | Like `selectTraceEventsDynamic'` but also captures time of the trace event.
--
selectTraceEventsDynamicWithTime' :: forall a b. Typeable b => SimTrace a -> [(Time, b)]
selectTraceEventsDynamicWithTime' :: forall a b. Typeable b => SimTrace a -> [(Time, b)]
selectTraceEventsDynamicWithTime' = forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' Time -> SimEventType -> Maybe (Time, b)
fn
  where
    fn :: Time -> SimEventType -> Maybe (Time, b)
    fn :: Time -> SimEventType -> Maybe (Time, b)
fn Time
t (EventLog Dynamic
dyn) = (Time
t,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = forall a. Maybe a
Nothing

-- | Get a trace of 'EventSay'.
--
-- For convenience, this throws exceptions for abnormal sim termination.
--
selectTraceEventsSay :: SimTrace a -> [String]
selectTraceEventsSay :: forall a. SimTrace a -> [[Char]]
selectTraceEventsSay = forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents Time -> SimEventType -> Maybe [Char]
fn
  where
    fn :: Time -> SimEventType -> Maybe String
    fn :: Time -> SimEventType -> Maybe [Char]
fn Time
_ (EventSay [Char]
s) = forall a. a -> Maybe a
Just [Char]
s
    fn Time
_ SimEventType
_            = forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsSay' but also captures time of the trace event.
--
selectTraceEventsSayWithTime :: SimTrace a -> [(Time, String)]
selectTraceEventsSayWithTime :: forall a. SimTrace a -> [(Time, [Char])]
selectTraceEventsSayWithTime = forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents Time -> SimEventType -> Maybe (Time, [Char])
fn
  where
    fn :: Time -> SimEventType -> Maybe (Time, String)
    fn :: Time -> SimEventType -> Maybe (Time, [Char])
fn Time
t (EventSay [Char]
s) = forall a. a -> Maybe a
Just (Time
t, [Char]
s)
    fn Time
_ SimEventType
_            = forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsSay' but return partial trace if an exception is
-- found in it.
--
selectTraceEventsSay' :: SimTrace a -> [String]
selectTraceEventsSay' :: forall a. SimTrace a -> [[Char]]
selectTraceEventsSay' = forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' Time -> SimEventType -> Maybe [Char]
fn
  where
    fn :: Time -> SimEventType -> Maybe String
    fn :: Time -> SimEventType -> Maybe [Char]
fn Time
_ (EventSay [Char]
s) = forall a. a -> Maybe a
Just [Char]
s
    fn Time
_ SimEventType
_            = forall a. Maybe a
Nothing

-- | Like `selectTraceEventsSay'` but also captures time of the trace event.
--
selectTraceEventsSayWithTime' :: SimTrace a -> [(Time, String)]
selectTraceEventsSayWithTime' :: forall a. SimTrace a -> [(Time, [Char])]
selectTraceEventsSayWithTime' = forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' Time -> SimEventType -> Maybe (Time, [Char])
fn
  where
    fn :: Time -> SimEventType -> Maybe (Time, String)
    fn :: Time -> SimEventType -> Maybe (Time, [Char])
fn Time
t (EventSay [Char]
s) = forall a. a -> Maybe a
Just (Time
t, [Char]
s)
    fn Time
_ SimEventType
_            = forall a. Maybe a
Nothing

-- | Print all 'EventSay' to the console.
--
-- For convenience, this throws exceptions for abnormal sim termination.
--
printTraceEventsSay :: SimTrace a -> IO ()
printTraceEventsSay :: forall a. SimTrace a -> IO ()
printTraceEventsSay = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall a. Show a => a -> IO ()
print forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SimTrace a -> [[Char]]
selectTraceEventsSay


-- | The most general select function.  It is a _total_ function.
--
traceSelectTraceEvents
    :: (Time -> SimEventType -> Maybe b)
    -> SimTrace a
    -> Trace (SimResult a) b
traceSelectTraceEvents :: forall b a.
(Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents Time -> SimEventType -> Maybe b
fn = forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr ( \ SimResult a
v Trace (SimResult a) b
_acc -> forall a b. a -> Trace a b
Nil SimResult a
v )
                                    ( \ SimEvent
eventCtx Trace (SimResult a) b
acc
                                     -> case SimEvent
eventCtx of
                                          SimRacesFound [ScheduleControl]
_ -> Trace (SimResult a) b
acc
                                          SimEvent{} ->
                                            case Time -> SimEventType -> Maybe b
fn (SimEvent -> Time
seTime SimEvent
eventCtx) (SimEvent -> SimEventType
seType SimEvent
eventCtx) of
                                              Maybe b
Nothing -> Trace (SimResult a) b
acc
                                              Just b
b  -> forall a b. b -> Trace a b -> Trace a b
Cons b
b Trace (SimResult a) b
acc
                                          SimPOREvent{} ->
                                            case Time -> SimEventType -> Maybe b
fn (SimEvent -> Time
seTime SimEvent
eventCtx) (SimEvent -> SimEventType
seType SimEvent
eventCtx) of
                                              Maybe b
Nothing -> Trace (SimResult a) b
acc
                                              Just b
b  -> forall a b. b -> Trace a b -> Trace a b
Cons b
b Trace (SimResult a) b
acc
                                    )
                                    forall a. HasCallStack => a
undefined -- it is ignored

-- | Select dynamic events.  It is a _total_ function.
--
traceSelectTraceEventsDynamic :: forall a b. Typeable b
                              => SimTrace a -> Trace (SimResult a) b
traceSelectTraceEventsDynamic :: forall a b. Typeable b => SimTrace a -> Trace (SimResult a) b
traceSelectTraceEventsDynamic = forall b a.
(Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents Time -> SimEventType -> Maybe b
fn
  where
    fn :: Time -> SimEventType -> Maybe b
    fn :: Time -> SimEventType -> Maybe b
fn Time
_ (EventLog Dynamic
dyn) = forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = forall a. Maybe a
Nothing


-- | Select say events.  It is a _total_ function.
--
traceSelectTraceEventsSay :: forall a.  SimTrace a -> Trace (SimResult a) String
traceSelectTraceEventsSay :: forall a. SimTrace a -> Trace (SimResult a) [Char]
traceSelectTraceEventsSay = forall b a.
(Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents Time -> SimEventType -> Maybe [Char]
fn
  where
    fn :: Time -> SimEventType -> Maybe String
    fn :: Time -> SimEventType -> Maybe [Char]
fn Time
_ (EventSay [Char]
s) = forall a. a -> Maybe a
Just [Char]
s
    fn Time
_ SimEventType
_            = forall a. Maybe a
Nothing

-- | Simulation terminated a failure.
--
data Failure =
       -- | The main thread terminated with an exception.
       FailureException SomeException

       -- | The threads all deadlocked.
     | FailureDeadlock ![Labelled ThreadId]

       -- | The main thread terminated normally but other threads were still
       -- alive, and strict shutdown checking was requested.
       -- See 'runSimStrictShutdown'.
     | FailureSloppyShutdown [Labelled ThreadId]

       -- | An exception was thrown while evaluation the trace.
       -- This could be an internal assertion failure of `io-sim` or an
       -- unhandled exception in the simulation.
     | FailureEvaluation SomeException
  deriving Int -> Failure -> ShowS
[Failure] -> ShowS
Failure -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Failure] -> ShowS
$cshowList :: [Failure] -> ShowS
show :: Failure -> [Char]
$cshow :: Failure -> [Char]
showsPrec :: Int -> Failure -> ShowS
$cshowsPrec :: Int -> Failure -> ShowS
Show

instance Exception Failure where
    displayException :: Failure -> [Char]
displayException (FailureException SomeException
err) = forall e. Exception e => e -> [Char]
displayException  SomeException
err
    displayException (FailureDeadlock [Labelled ThreadId]
threads) =
      forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<io-sim deadlock: "
             , forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> [a] -> [b]
`map` [Labelled ThreadId]
threads)
             , [Char]
">>"
             ]
    displayException (FailureSloppyShutdown [Labelled ThreadId]
threads) =
      forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<io-sim sloppy shutdown: "
             , forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> [a] -> [b]
`map` [Labelled ThreadId]
threads)
             , [Char]
">>"
             ]
    displayException (FailureEvaluation SomeException
err) = [Char]
"evaluation error:" forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> [Char]
displayException  SomeException
err
    

-- | 'IOSim' is a pure monad.
--
runSim :: forall a. (forall s. IOSim s a) -> Either Failure a
runSim :: forall a. (forall s. IOSim s a) -> Either Failure a
runSim forall s. IOSim s a
mainAction = forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
False (forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace forall s. IOSim s a
mainAction)

-- | For quick experiments and tests it is often appropriate and convenient to
-- simply throw failures as exceptions.
--
runSimOrThrow :: forall a. (forall s. IOSim s a) -> a
runSimOrThrow :: forall a. (forall s. IOSim s a) -> a
runSimOrThrow forall s. IOSim s a
mainAction =
    case forall a. (forall s. IOSim s a) -> Either Failure a
runSim forall s. IOSim s a
mainAction of
      Left  Failure
e -> forall a e. Exception e => e -> a
throw Failure
e
      Right a
x -> a
x

-- | Like 'runSim' but fail when the main thread terminates if there are other
-- threads still running or blocked. If one is trying to follow a strict thread
-- cleanup policy then this helps testing for that.
--
runSimStrictShutdown :: forall a. (forall s. IOSim s a) -> Either Failure a
runSimStrictShutdown :: forall a. (forall s. IOSim s a) -> Either Failure a
runSimStrictShutdown forall s. IOSim s a
mainAction = forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
True (forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace forall s. IOSim s a
mainAction)

-- | Fold through the trace and return either a 'Failure' or the simulation
-- result, i.e. the return value of the main thread.
--
traceResult :: Bool
            -- ^ if True the simulation will fail if there are any threads which
            -- didn't terminated when the main thread terminated.
            -> SimTrace a
            -- ^ simulation trace
            -> Either Failure a
traceResult :: forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
strict = forall a. IO a -> a
unsafePerformIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SimTrace a -> IO (Either Failure a)
eval
  where
    eval :: SimTrace a -> IO (Either Failure a)
    eval :: forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
a = do
      Either SomeException (SimTrace a)
r <- forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> m (Either e a)
try (forall (m :: * -> *) a. MonadEvaluate m => a -> m a
evaluate SimTrace a
a)
      case Either SomeException (SimTrace a)
r of
        Left SomeException
e  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left (SomeException -> Failure
FailureEvaluation SomeException
e))
        Right SimTrace a
_ -> forall a. SimTrace a -> IO (Either Failure a)
go SimTrace a
a

    go :: SimTrace a -> IO (Either Failure a)
    go :: forall a. SimTrace a -> IO (Either Failure a)
go (SimTrace Time
_ ThreadId
_ Maybe [Char]
_ SimEventType
_ SimTrace a
t)             = forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
    go (SimPORTrace Time
_ ThreadId
_ Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
t)        = forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
    go (TraceRacesFound [ScheduleControl]
_ SimTrace a
t)            = forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
    go (TraceMainReturn Time
_ a
_ tids :: [Labelled ThreadId]
tids@(Labelled ThreadId
_:[Labelled ThreadId]
_))
                               | Bool
strict = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([Labelled ThreadId] -> Failure
FailureSloppyShutdown [Labelled ThreadId]
tids)
    go (TraceMainReturn Time
_ a
x [Labelled ThreadId]
_)          = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right a
x
    go (TraceMainException Time
_ SomeException
e [Labelled ThreadId]
_)       = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (SomeException -> Failure
FailureException SomeException
e)
    go (TraceDeadlock   Time
_   [Labelled ThreadId]
threads)    = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([Labelled ThreadId] -> Failure
FailureDeadlock [Labelled ThreadId]
threads)
    go TraceLoop{}                      = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: traceResult TraceLoop{}"

-- | Turn 'SimTrace' into a list of timestamped events.
--
traceEvents :: SimTrace a -> [(Time, ThreadId, Maybe ThreadLabel, SimEventType)]
traceEvents :: forall a.
SimTrace a -> [(Time, ThreadId, Maybe [Char], SimEventType)]
traceEvents (SimTrace Time
time ThreadId
tid Maybe [Char]
tlbl SimEventType
event SimTrace a
t)      = (Time
time, ThreadId
tid, Maybe [Char]
tlbl, SimEventType
event)
                                                  forall a. a -> [a] -> [a]
: forall a.
SimTrace a -> [(Time, ThreadId, Maybe [Char], SimEventType)]
traceEvents SimTrace a
t
traceEvents (SimPORTrace Time
time ThreadId
tid Int
_ Maybe [Char]
tlbl SimEventType
event SimTrace a
t) = (Time
time, ThreadId
tid, Maybe [Char]
tlbl, SimEventType
event)
                                                  forall a. a -> [a] -> [a]
: forall a.
SimTrace a -> [(Time, ThreadId, Maybe [Char], SimEventType)]
traceEvents SimTrace a
t
traceEvents SimTrace a
_                                     = []


-- | Pretty print a timestamped event.
--
ppEvents :: [(Time, ThreadId, Maybe ThreadLabel, SimEventType)]
         -> String
ppEvents :: [(Time, ThreadId, Maybe [Char], SimEventType)] -> [Char]
ppEvents [(Time, ThreadId, Maybe [Char], SimEventType)]
events =
    forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n"
      [ Int -> Int -> Int -> SimEvent -> [Char]
ppSimEvent Int
timeWidth Int
tidWidth Int
width
                   SimEvent {Time
seTime :: Time
seTime :: Time
seTime, ThreadId
seThreadId :: ThreadId
seThreadId :: ThreadId
seThreadId, Maybe [Char]
seThreadLabel :: Maybe [Char]
seThreadLabel :: Maybe [Char]
seThreadLabel, SimEventType
seType :: SimEventType
seType :: SimEventType
seType }
      | (Time
seTime, ThreadId
seThreadId, Maybe [Char]
seThreadLabel, SimEventType
seType) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
      ]
  where
    timeWidth :: Int
timeWidth = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Show a => a -> [Char]
show Time
t)
                | (Time
t, ThreadId
_, Maybe [Char]
_, SimEventType
_) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
                ]
    tidWidth :: Int
tidWidth  = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Show a => a -> [Char]
show ThreadId
tid)
                | (Time
_, ThreadId
tid, Maybe [Char]
_, SimEventType
_) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
                ]
    width :: Int
width     = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 forall (t :: * -> *) a. Foldable t => t a -> Int
length Maybe [Char]
threadLabel
                | (Time
_, ThreadId
_, Maybe [Char]
threadLabel, SimEventType
_) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
                ]


-- | See 'runSimTraceST' below.
--
runSimTrace :: forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace :: forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace forall s. IOSim s a
mainAction = forall a. (forall s. ST s a) -> a
runST (forall s a. IOSim s a -> ST s (SimTrace a)
runSimTraceST forall s. IOSim s a
mainAction)

--
-- IOSimPOR
--
--
-- $iosimpor
--
-- /IOSimPOR/ is a different interpreter of 'IOSim' which has the ability to
-- discover race conditions and replay the simulation using a schedule which
-- reverts them.  For extended documentation how to use it see
-- [here](https://github.com/input-output-hk/io-sim/blob/main/io-sim/how-to-use-IOSimPOR.md).
--
-- /IOSimPOR/ only discovers races between events which happen in the same time
-- slot.  In /IOSim/ and /IOSimPOR/ time only moves explicitly through timer
-- events, e.g. things like `Control.Monad.Class.MonadTimer.SI.threadDelay`,
-- `Control.Monad.Class.MonadTimer.SI.registerDelay` or the
-- `Control.Monad.Class.MonadTimer.NonStandard.MonadTimeout` api.  The usual
-- quickcheck techniques can help explore different schedules of
-- threads too.

-- | Execute a simulation, discover & revert races.  Note that this will execute
-- the simulation multiple times with different schedules, and thus it's much
-- more costly than a simple `runSimTrace` (also the simulation environments has
-- much more state to track and hence is slower).
--
-- On property failure it will show the failing schedule (`ScheduleControl`)
-- which can be plugged to `controlSimTrace`.
--
exploreSimTrace
  :: forall a test. Testable test
  => (ExplorationOptions -> ExplorationOptions)
  -- ^ modify default exploration options
  -> (forall s. IOSim s a)
  -- ^ a simulation to run
  -> (Maybe (SimTrace a) -> SimTrace a -> test)
  -- ^ a callback which receives the previous trace (e.g. before reverting
  -- a race condition) and current trace
  -> Property
exploreSimTrace :: forall a test.
Testable test =>
(ExplorationOptions -> ExplorationOptions)
-> (forall s. IOSim s a)
-> (Maybe (SimTrace a) -> SimTrace a -> test)
-> Property
exploreSimTrace ExplorationOptions -> ExplorationOptions
optsf forall s. IOSim s a
mainAction Maybe (SimTrace a) -> SimTrace a -> test
k =
  case ExplorationOptions -> Maybe ScheduleControl
explorationReplay ExplorationOptions
opts of
    Maybe ScheduleControl
Nothing ->
      Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore (ExplorationOptions -> Int
explorationScheduleBound ExplorationOptions
opts) (ExplorationOptions -> Int
explorationBranching ExplorationOptions
opts) ScheduleControl
ControlDefault forall a. Maybe a
Nothing forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&.
      let size :: Int
size = () -> Int
cacheSize() in Int
size seq :: forall a b. a -> b -> b
`seq`
      forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Modified schedules explored" [Int -> [Char]
bucket Int
size] Bool
True
    Just ScheduleControl
control ->
      forall a test.
Testable test =>
ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (SimTrace a -> test)
-> Property
replaySimTrace ExplorationOptions
opts forall s. IOSim s a
mainAction ScheduleControl
control (Maybe (SimTrace a) -> SimTrace a -> test
k forall a. Maybe a
Nothing)
  where
    opts :: ExplorationOptions
opts = ExplorationOptions -> ExplorationOptions
optsf ExplorationOptions
stdExplorationOptions

    explore :: Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
    explore :: Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore Int
n Int
m ScheduleControl
control Maybe (SimTrace a)
passingTrace =

      -- ALERT!!! Impure code: readRaces must be called *after* we have
      -- finished with trace.
      let (() -> [ScheduleControl]
readRaces, SimTrace a
trace0) = forall a. SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces forall a b. (a -> b) -> a -> b
$
                                forall a.
Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
controlSimTrace
                                  (ExplorationOptions -> Maybe Int
explorationStepTimelimit ExplorationOptions
opts) ScheduleControl
control forall s. IOSim s a
mainAction
          (Maybe
  ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
sleeper,SimTrace a
trace) = forall a1 a2.
Maybe (SimTrace a1)
-> SimTrace a2
-> (Maybe
      ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
    SimTrace a2)
compareTraces Maybe (SimTrace a)
passingTrace SimTrace a
trace0
      in ( forall prop. Testable prop => [Char] -> prop -> Property
counterexample ([Char]
"Schedule control: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ScheduleControl
control)
         forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => [Char] -> prop -> Property
counterexample
            (case Maybe
  ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
sleeper of
              Maybe
  ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
Nothing -> [Char]
"No thread delayed"
              Just ((Time
t,ThreadId
tid,Maybe [Char]
lab),Set (ThreadId, Maybe [Char])
racing) ->
                (ThreadId, Maybe [Char]) -> [Char]
showThread (ThreadId
tid,Maybe [Char]
lab) forall a. [a] -> [a] -> [a]
++
                [Char]
" delayed at time "forall a. [a] -> [a] -> [a]
++
                forall a. Show a => a -> [Char]
show Time
t forall a. [a] -> [a] -> [a]
++
                [Char]
"\n  until after:\n" forall a. [a] -> [a] -> [a]
++
                [[Char]] -> [Char]
unlines (forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"    "forall a. [a] -> [a] -> [a]
++)forall b c a. (b -> c) -> (a -> b) -> a -> c
.(ThreadId, Maybe [Char]) -> [Char]
showThread) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set (ThreadId, Maybe [Char])
racing)
             )
         forall a b. (a -> b) -> a -> b
$ Maybe (SimTrace a) -> SimTrace a -> test
k Maybe (SimTrace a)
passingTrace SimTrace a
trace
         )
      forall prop. TestableNoCatch prop => prop -> prop -> Property
.&&| let limit :: Int
limit     = (Int
nforall a. Num a => a -> a -> a
+Int
mforall a. Num a => a -> a -> a
-Int
1) forall a. Integral a => a -> a -> a
`div` Int
m
               -- To ensure the set of schedules explored is deterministic, we
               -- filter out cached ones *after* selecting the children of this
               -- node.
               races :: [ScheduleControl]
races     = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScheduleControl -> Bool
cached) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
limit forall a b. (a -> b) -> a -> b
$ () -> [ScheduleControl]
readRaces ()
               branching :: Int
branching = forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleControl]
races
           in -- tabulate "Races explored" (map show races) $
              forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Branching factor" [Int -> [Char]
bucket Int
branching] forall a b. (a -> b) -> a -> b
$
              forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Race reversals per schedule" [Int -> [Char]
bucket (ScheduleControl -> Int
raceReversals ScheduleControl
control)] forall a b. (a -> b) -> a -> b
$
              forall prop. TestableNoCatch prop => [prop] -> Property
conjoinPar
                [ --Debug.trace "New schedule:" $
                  --Debug.trace ("  "++show r) $
                  --counterexample ("Schedule control: " ++ show r) $
                  Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore Int
n' ((Int
mforall a. Num a => a -> a -> a
-Int
1) forall a. Ord a => a -> a -> a
`max` Int
1) ScheduleControl
r (forall a. a -> Maybe a
Just SimTrace a
trace0)
                | (ScheduleControl
r,Int
n') <- forall a b. [a] -> [b] -> [(a, b)]
zip [ScheduleControl]
races (Int -> Int -> [Int]
divide (Int
nforall a. Num a => a -> a -> a
-Int
branching) Int
branching) ]

    bucket :: Int -> String
    bucket :: Int -> [Char]
bucket Int
n | Int
nforall a. Ord a => a -> a -> Bool
<Int
10  = forall a. Show a => a -> [Char]
show Int
n
             | Int
nforall a. Ord a => a -> a -> Bool
>=Int
10 = forall {t}. (Show t, Integral t) => t -> t -> [Char]
buck Int
n Int
1
             | Bool
otherwise = forall a. HasCallStack => [Char] -> a
error [Char]
"Ord Int is not a total order!"  -- GHC made me do it!
    buck :: t -> t -> [Char]
buck t
n t
t | t
nforall a. Ord a => a -> a -> Bool
<t
10      = forall a. Show a => a -> [Char]
show (t
nforall a. Num a => a -> a -> a
*t
t) forall a. [a] -> [a] -> [a]
++ [Char]
"-" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ((t
nforall a. Num a => a -> a -> a
+t
1)forall a. Num a => a -> a -> a
*t
tforall a. Num a => a -> a -> a
-t
1)
             | t
nforall a. Ord a => a -> a -> Bool
>=t
10     = t -> t -> [Char]
buck (t
n forall a. Integral a => a -> a -> a
`div` t
10) (t
tforall a. Num a => a -> a -> a
*t
10)
             | Bool
otherwise = forall a. HasCallStack => [Char] -> a
error [Char]
"Ord Int is not a total order!"  -- GHC made me do it!

    divide :: Int -> Int -> [Int]
    divide :: Int -> Int -> [Int]
divide Int
n Int
k =
      [ Int
n forall a. Integral a => a -> a -> a
`div` Int
k forall a. Num a => a -> a -> a
+ if Int
iforall a. Ord a => a -> a -> Bool
<Int
n forall a. Integral a => a -> a -> a
`mod` Int
k then Int
1 else Int
0
      | Int
i <- [Int
0..Int
kforall a. Num a => a -> a -> a
-Int
1] ]

    showThread :: (ThreadId,Maybe ThreadLabel) -> String
    showThread :: (ThreadId, Maybe [Char]) -> [Char]
showThread (ThreadId
tid,Maybe [Char]
lab) =
      forall a. Show a => a -> [Char]
show ThreadId
tid forall a. [a] -> [a] -> [a]
++ (case Maybe [Char]
lab of Maybe [Char]
Nothing -> [Char]
""
                               Just [Char]
l  -> [Char]
" ("forall a. [a] -> [a] -> [a]
++[Char]
lforall a. [a] -> [a] -> [a]
++[Char]
")")

    -- cache of explored schedules
    cache :: IORef (Set ScheduleControl)
    cache :: IORef (Set ScheduleControl)
cache = forall a. IO a -> a
unsafePerformIO IO (IORef (Set ScheduleControl))
cacheIO

    -- insert a schedule into the cache
    cached :: ScheduleControl -> Bool
    cached :: ScheduleControl -> Bool
cached = forall a. IO a -> a
unsafePerformIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScheduleControl -> IO Bool
cachedIO

    -- compute cache size; it's a function to make sure that `GHC` does not
    -- inline it (and share the same thunk).
    cacheSize :: () -> Int
    cacheSize :: () -> Int
cacheSize = forall a. IO a -> a
unsafePerformIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> IO Int
cacheSizeIO

    --
    -- Caching in IO monad
    --

    -- It is possible for the same control to be generated several times.
    -- To avoid exploring them twice, we keep a cache of explored schedules.
    cacheIO :: IO (IORef (Set ScheduleControl))
    cacheIO :: IO (IORef (Set ScheduleControl))
cacheIO = forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$
              -- we use opts here just to be sure the reference cannot be
              -- lifted out of exploreSimTrace
              if ExplorationOptions -> Int
explorationScheduleBound ExplorationOptions
opts forall a. Ord a => a -> a -> Bool
>=Int
0
                then forall a. Set a
Set.empty
                else forall a. HasCallStack => [Char] -> a
error [Char]
"exploreSimTrace: negative schedule bound"

    cachedIO :: ScheduleControl -> IO Bool
    cachedIO :: ScheduleControl -> IO Bool
cachedIO ScheduleControl
m = forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (Set ScheduleControl)
cache forall a b. (a -> b) -> a -> b
$ \Set ScheduleControl
set ->
      (forall a. Ord a => a -> Set a -> Set a
Set.insert ScheduleControl
m Set ScheduleControl
set, forall a. Ord a => a -> Set a -> Bool
Set.member ScheduleControl
m Set ScheduleControl
set)


    cacheSizeIO :: () -> IO Int
    cacheSizeIO :: () -> IO Int
cacheSizeIO () = forall a. Set a -> Int
Set.size forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef IORef (Set ScheduleControl)
cache


-- | A specialised version of `controlSimTrace'.
--
-- An internal function.
--
replaySimTrace :: forall a test. (Testable test)
               => ExplorationOptions
               -- ^ race exploration options
               -> (forall s. IOSim s a)
               -> ScheduleControl
               -- ^ a schedule control to reproduce
               -> (SimTrace a -> test)
               -- ^ a callback which receives the simulation trace. The trace
               -- will not contain any race events
               -> Property
replaySimTrace :: forall a test.
Testable test =>
ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (SimTrace a -> test)
-> Property
replaySimTrace ExplorationOptions
opts forall s. IOSim s a
mainAction ScheduleControl
control SimTrace a -> test
k =
  let (() -> [ScheduleControl]
_,SimTrace a
trace) = forall a. SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces forall a b. (a -> b) -> a -> b
$
                  forall a.
Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
controlSimTrace (ExplorationOptions -> Maybe Int
explorationStepTimelimit ExplorationOptions
opts) ScheduleControl
control forall s. IOSim s a
mainAction
  in forall prop. Testable prop => prop -> Property
property (SimTrace a -> test
k SimTrace a
trace)

-- | Run a simulation using a given schedule.  This is useful to reproduce
-- failing cases without exploring the races.
--
controlSimTrace :: forall a.
                   Maybe Int
                -- ^ limit on the computation time allowed per scheduling step, for
                -- catching infinite loops etc.
                -> ScheduleControl
                -- ^ a schedule to replay
                --
                -- /note/: must be either `ControlDefault` or `ControlAwait`.
                -> (forall s. IOSim s a)
                -- ^ a simulation to run
                -> SimTrace a
controlSimTrace :: forall a.
Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
controlSimTrace Maybe Int
limit ScheduleControl
control forall s. IOSim s a
mainAction =
    forall a. (forall s. ST s a) -> a
runST (forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST Maybe Int
limit ScheduleControl
control forall s. IOSim s a
mainAction)

raceReversals :: ScheduleControl -> Int
raceReversals :: ScheduleControl -> Int
raceReversals ScheduleControl
ControlDefault      = Int
0
raceReversals (ControlAwait [ScheduleMod]
mods) = forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleMod]
mods
raceReversals ControlFollow{}     = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: raceReversals ControlFollow{}"

-- compareTraces is given (maybe) a passing trace and a failing trace,
-- and identifies the point at which they diverge, where it inserts a
-- "sleep" event for the thread that is delayed in the failing case,
-- and a "wake" event before its next action. It also returns the
-- identity and time of the sleeping thread. Since we expect the trace
-- to be consumed lazily (and perhaps only partially), and since the
-- sleeping thread is not of interest unless the trace is consumed
-- this far, then we collect its identity only if it is reached using
-- unsafePerformIO.

compareTraces :: Maybe (SimTrace a1)
              -> SimTrace a2
              -> (Maybe ((Time, ThreadId, Maybe ThreadLabel),
                         Set.Set (ThreadId, Maybe ThreadLabel)),
                  SimTrace a2)
compareTraces :: forall a1 a2.
Maybe (SimTrace a1)
-> SimTrace a2
-> (Maybe
      ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
    SimTrace a2)
compareTraces Maybe (SimTrace a1)
Nothing SimTrace a2
trace = (forall a. Maybe a
Nothing, SimTrace a2
trace)
compareTraces (Just SimTrace a1
passing) SimTrace a2
trace = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
  IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper <- forall a. a -> IO (IORef a)
newIORef forall a. Maybe a
Nothing
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper,
          forall {a} {a}.
IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace a -> SimTrace a
go IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper SimTrace a1
passing SimTrace a2
trace)
  where go :: IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace a -> SimTrace a
go IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper (SimPORTrace Time
tpass ThreadId
tidpass Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
pass')
                   (SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail SimTrace a
fail')
          | (Time
tpass,ThreadId
tidpass) forall a. Eq a => a -> a -> Bool
== (Time
tfail,ThreadId
tidfail) =
              forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
                forall a b. (a -> b) -> a -> b
$ IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace a -> SimTrace a
go IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper SimTrace a
pass' SimTrace a
fail'
        go IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper (SimPORTrace Time
tpass ThreadId
tidpass Int
tsteppass Maybe [Char]
tlpass SimEventType
_ SimTrace a
_) SimTrace a
fail =
          forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
            forall a. IORef a -> a -> IO ()
writeIORef IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ((Time
tpass, ThreadId
tidpass, Maybe [Char]
tlpass),forall a. Set a
Set.empty)
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tpass ThreadId
tidpass Int
tsteppass Maybe [Char]
tlpass SimEventType
EventThreadSleep
                   forall a b. (a -> b) -> a -> b
$ forall {a} {a}.
IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
-> ThreadId -> SimTrace a -> SimTrace a
wakeup IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper ThreadId
tidpass SimTrace a
fail
        go IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
_ SimTrace {} SimTrace a
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraces: invariant violation"
        go IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
_ SimTrace a
_ SimTrace {} = forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraces: invariant violation"
        go IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
_ SimTrace a
_ SimTrace a
fail = SimTrace a
fail

        wakeup :: IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
-> ThreadId -> SimTrace a -> SimTrace a
wakeup IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
sleeper ThreadId
tidpass
               fail :: SimTrace a
fail@(SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail SimTrace a
fail')
          | ThreadId
tidpass forall a. Eq a => a -> a -> Bool
== ThreadId
tidfail =
              forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
EventThreadWake SimTrace a
fail
          | Bool
otherwise = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
              Just (a
slp,Set (ThreadId, Maybe [Char])
racing) <- forall a. IORef a -> IO a
readIORef IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
sleeper
              forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
sleeper forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (a
slp,forall a. Ord a => a -> Set a -> Set a
Set.insert (ThreadId
tidfail,Maybe [Char]
tlfail) Set (ThreadId, Maybe [Char])
racing)
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
                     forall a b. (a -> b) -> a -> b
$ IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
-> ThreadId -> SimTrace a -> SimTrace a
wakeup IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
sleeper ThreadId
tidpass SimTrace a
fail'
        wakeup IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
_ ThreadId
_ SimTrace {} = forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraces: invariant violation"
        wakeup IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
_ ThreadId
_ SimTrace a
fail = SimTrace a
fail