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

{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

module Control.Monad.IOSim
  ( -- * Simulation monad
    IOSim
  , STMSim
    -- ** Run simulation
  , runSim
  , runSimOrThrow
  , runSimStrictShutdown
  , Failure (..)
  , runSimTrace
  , runSimTraceST
    -- ** Explore races using /IOSimPOR/
    -- $iosimpor
  , exploreSimTrace
  , exploreSimTraceST
  , controlSimTrace
  , controlSimTraceST
  , 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, TraceInternalError)
  , SimResult (..)
  , SimEvent (..)
  , SimEventType (..)
  , ThreadLabel
  , IOSimThreadId (..)
  , 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
  , Timeout
  , newTimeout
  , readTimeout
  , cancelTimeout
  , awaitTimeout
  ) where

import Prelude

import Data.Bifoldable
import Data.Bifunctor (first)
import Data.Dynamic (fromDynamic)
import Data.Functor (void)
import Data.List (intercalate)
import Data.Maybe (catMaybes)
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Typeable (Typeable)

import Data.List.Trace (Trace (..))
import Data.List.Trace qualified as Trace

import Control.Exception (throw)

import Control.Monad.ST.Lazy
import Data.STRef.Lazy

import Control.Monad.Class.MonadThrow as MonadThrow

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

import Test.QuickCheck

import Debug.Trace qualified as Debug
import System.IO.Unsafe


-- | Select events according to the predicate function.  It throws an error if
-- the simulation ends with 'Failure'.
--
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 =
      (SimResult a -> [b] -> [b])
-> (b -> [b] -> [b]) -> [b] -> Trace (SimResult a) b -> [b]
forall a c b. (a -> c -> c) -> (b -> c -> c) -> c -> Trace a b -> c
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
_ Labelled IOSimThreadId
_ SomeException
e [Labelled IOSimThreadId]
_     -> Failure -> [b]
forall a e. Exception e => e -> a
throw (SomeException -> Failure
FailureException SomeException
e)
                    Deadlock      Time
_   [Labelled IOSimThreadId]
threads -> Failure -> [b]
forall a e. Exception e => e -> a
throw ([Labelled IOSimThreadId] -> Failure
FailureDeadlock [Labelled IOSimThreadId]
threads)
                    MainReturn    Time
_ Labelled IOSimThreadId
_ a
_ [Labelled IOSimThreadId]
_     -> []
                    SimResult a
Loop                      -> [Char] -> [b]
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: selectTraceEvents _ TraceLoop{}"
                    InternalError [Char]
msg         -> Failure -> [b]
forall a e. Exception e => e -> a
throw ([Char] -> Failure
FailureInternal [Char]
msg)
              )
              ( \ b
b [b]
acc -> b
b b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
acc )
              []
    (Trace (SimResult a) b -> [b])
-> (SimTrace a -> Trace (SimResult a) b) -> SimTrace a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
forall b a.
(Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents Time -> SimEventType -> Maybe b
fn

-- | Like 'selectTraceEvents', but it returns even if the simulation trace ends
-- with 'Failure'.
--
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 =
      (SimResult a -> [b] -> [b])
-> (b -> [b] -> [b]) -> [b] -> Trace (SimResult a) b -> [b]
forall a c b. (a -> c -> c) -> (b -> c -> c) -> c -> Trace a b -> c
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 b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
acc )
              []
    (Trace (SimResult a) b -> [b])
-> (SimTrace a -> Trace (SimResult a) b) -> SimTrace a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
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 = SimTrace a -> [ScheduleControl]
forall a. SimTrace a -> [ScheduleControl]
go
  where
    go :: SimTrace a -> [ScheduleControl]
go (SimTrace Time
_ IOSimThreadId
_ Maybe [Char]
_ SimEventType
_ SimTrace a
trace)      = SimTrace a -> [ScheduleControl]
go SimTrace a
trace
    go (SimPORTrace Time
_ IOSimThreadId
_ Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
trace) = SimTrace a -> [ScheduleControl]
go SimTrace a
trace
    go (TraceRacesFound [ScheduleControl]
races SimTrace a
trace) =
      [ScheduleControl]
races [ScheduleControl] -> [ScheduleControl] -> [ScheduleControl]
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.

-- | Detach discovered races.  This is written in `ST` monad to support
-- simulations which do not terminate, in which case we will only detach races
-- up to the point we evaluated the simulation.
--
detachTraceRacesST :: forall a s. SimTrace a -> ST s (ST s [ScheduleControl], SimTrace a)
detachTraceRacesST :: forall a s. SimTrace a -> ST s (ST s [ScheduleControl], SimTrace a)
detachTraceRacesST SimTrace a
trace0 = do
  STRef s [[ScheduleControl]]
races <- [[ScheduleControl]] -> ST s (STRef s [[ScheduleControl]])
forall a s. a -> ST s (STRef s a)
newSTRef []
  let readRaces :: ST s [ScheduleControl]
      readRaces :: ST s [ScheduleControl]
readRaces = [[ScheduleControl]] -> [ScheduleControl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[ScheduleControl]] -> [ScheduleControl])
-> ([[ScheduleControl]] -> [[ScheduleControl]])
-> [[ScheduleControl]]
-> [ScheduleControl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[ScheduleControl]] -> [[ScheduleControl]]
forall a. [a] -> [a]
reverse ([[ScheduleControl]] -> [ScheduleControl])
-> ST s [[ScheduleControl]] -> ST s [ScheduleControl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef s [[ScheduleControl]] -> ST s [[ScheduleControl]]
forall s a. STRef s a -> ST s a
readSTRef STRef s [[ScheduleControl]]
races

      saveRaces :: [ScheduleControl] -> ST s ()
      saveRaces :: [ScheduleControl] -> ST s ()
saveRaces [ScheduleControl]
rs = STRef s [[ScheduleControl]]
-> ([[ScheduleControl]] -> [[ScheduleControl]]) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef STRef s [[ScheduleControl]]
races ([ScheduleControl]
rs[ScheduleControl] -> [[ScheduleControl]] -> [[ScheduleControl]]
forall a. a -> [a] -> [a]
:)

      go :: SimTrace a -> ST s (SimTrace a)
      go :: SimTrace a -> ST s (SimTrace a)
go (SimTrace Time
a IOSimThreadId
b Maybe [Char]
c SimEventType
d SimTrace a
trace)      = Time
-> IOSimThreadId
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
a IOSimThreadId
b Maybe [Char]
c SimEventType
d (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SimTrace a -> ST s (SimTrace a)
go SimTrace a
trace
      go (SimPORTrace Time
_ IOSimThreadId
_ Int
_ Maybe [Char]
_ EventRaces {} SimTrace a
trace)
                                       = SimTrace a -> ST s (SimTrace a)
go SimTrace a
trace
      go (SimPORTrace Time
a IOSimThreadId
b Int
c Maybe [Char]
d SimEventType
e SimTrace a
trace) = Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
a IOSimThreadId
b Int
c Maybe [Char]
d SimEventType
e (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SimTrace a -> ST s (SimTrace a)
go SimTrace a
trace
      go (TraceRacesFound [ScheduleControl]
rs SimTrace a
trace)    = [ScheduleControl] -> ST s ()
saveRaces [ScheduleControl]
rs ST s () -> ST s (SimTrace a) -> ST s (SimTrace a)
forall a b. ST s a -> ST s b -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SimTrace a -> ST s (SimTrace a)
go SimTrace a
trace
      go SimTrace a
t                             = SimTrace a -> ST s (SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return SimTrace a
t

  SimTrace a
trace <- SimTrace a -> ST s (SimTrace a)
go SimTrace a
trace0
  (ST s [ScheduleControl], SimTrace a)
-> ST s (ST s [ScheduleControl], SimTrace a)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (ST s [ScheduleControl]
readRaces, SimTrace a
trace)


-- | Like `detachTraceRacesST`, but it doesn't expose discovered races.
--
detachTraceRaces :: forall a. SimTrace a -> SimTrace a
detachTraceRaces :: forall a. SimTrace a -> SimTrace a
detachTraceRaces = (SimEvent -> Bool)
-> Trace (SimResult a) SimEvent -> Trace (SimResult a) SimEvent
forall b a. (b -> Bool) -> Trace a b -> Trace a b
Trace.filter (\SimEvent
a -> case SimEvent
a of
                                         SimPOREvent { seType :: SimEvent -> SimEventType
seType = EventRaces {} } -> Bool
False
                                         SimRacesFound {} -> Bool
False
                                         SimEvent
_                -> Bool
True)

-- | Select all the traced values matching the expected type.  It relies on the
-- sim's dynamic trace facility.
--
-- For convenience, it 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 = (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
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) = Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = Maybe b
forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsDynamic' but it 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 = (Time -> SimEventType -> Maybe (Time, b))
-> SimTrace a -> [(Time, b)]
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,) (b -> (Time, b)) -> Maybe b -> Maybe (Time, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = Maybe (Time, b)
forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsDynamic' but it returns even if the simulation trace
-- ends with 'Failure'.
--
selectTraceEventsDynamic' :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic' :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic' = (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
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) = Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = Maybe b
forall a. Maybe a
Nothing

-- | Like `selectTraceEventsDynamic'` but it 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' = (Time -> SimEventType -> Maybe (Time, b))
-> SimTrace a -> [(Time, b)]
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,) (b -> (Time, b)) -> Maybe b -> Maybe (Time, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = Maybe (Time, b)
forall a. Maybe a
Nothing

-- | Get a trace of 'EventSay'.
--
-- For convenience, it throws exceptions for abnormal sim termination.
--
selectTraceEventsSay :: SimTrace a -> [String]
selectTraceEventsSay :: forall a. SimTrace a -> [[Char]]
selectTraceEventsSay = (Time -> SimEventType -> Maybe [Char]) -> SimTrace a -> [[Char]]
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) = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    fn Time
_ SimEventType
_            = Maybe [Char]
forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsSay' but it also captures time of the trace event.
--
selectTraceEventsSayWithTime :: SimTrace a -> [(Time, String)]
selectTraceEventsSayWithTime :: forall a. SimTrace a -> [(Time, [Char])]
selectTraceEventsSayWithTime = (Time -> SimEventType -> Maybe (Time, [Char]))
-> SimTrace a -> [(Time, [Char])]
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) = (Time, [Char]) -> Maybe (Time, [Char])
forall a. a -> Maybe a
Just (Time
t, [Char]
s)
    fn Time
_ SimEventType
_            = Maybe (Time, [Char])
forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsSay' but it returns even if the simulation trace
-- ends with 'Failure'.
--
selectTraceEventsSay' :: SimTrace a -> [String]
selectTraceEventsSay' :: forall a. SimTrace a -> [[Char]]
selectTraceEventsSay' = (Time -> SimEventType -> Maybe [Char]) -> SimTrace a -> [[Char]]
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) = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    fn Time
_ SimEventType
_            = Maybe [Char]
forall a. Maybe a
Nothing

-- | Like `selectTraceEventsSay'` but it also captures time of the trace event.
--
selectTraceEventsSayWithTime' :: SimTrace a -> [(Time, String)]
selectTraceEventsSayWithTime' :: forall a. SimTrace a -> [(Time, [Char])]
selectTraceEventsSayWithTime' = (Time -> SimEventType -> Maybe (Time, [Char]))
-> SimTrace a -> [(Time, [Char])]
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) = (Time, [Char]) -> Maybe (Time, [Char])
forall a. a -> Maybe a
Just (Time
t, [Char]
s)
    fn Time
_ SimEventType
_            = Maybe (Time, [Char])
forall a. Maybe a
Nothing

-- | Print all 'EventSay' to the console.
--
-- For convenience, it throws exceptions for abnormal sim termination.
--
printTraceEventsSay :: SimTrace a -> IO ()
printTraceEventsSay :: forall a. SimTrace a -> IO ()
printTraceEventsSay = ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
forall a. Show a => a -> IO ()
print ([[Char]] -> IO ())
-> (SimTrace a -> [[Char]]) -> SimTrace a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimTrace a -> [[Char]]
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 = (SimResult a -> Trace (SimResult a) b -> Trace (SimResult a) b)
-> (SimEvent -> Trace (SimResult a) b -> Trace (SimResult a) b)
-> Trace (SimResult a) b
-> Trace (SimResult a) SimEvent
-> Trace (SimResult a) b
forall a c b. (a -> c -> c) -> (b -> c -> c) -> c -> Trace a b -> c
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 -> SimResult a -> Trace (SimResult a) b
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  -> b -> Trace (SimResult a) b -> Trace (SimResult a) 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  -> b -> Trace (SimResult a) b -> Trace (SimResult a) b
forall a b. b -> Trace a b -> Trace a b
Cons b
b Trace (SimResult a) b
acc
                                    )
                                    Trace (SimResult a) b
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 = (Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
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) = Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = Maybe b
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 = (Time -> SimEventType -> Maybe [Char])
-> SimTrace a -> Trace (SimResult a) [Char]
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) = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    fn Time
_ SimEventType
_            = Maybe [Char]
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 IOSimThreadId]

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

       -- | 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

       -- | An internal failure of the simulator.
       --
       -- Please open an issue at
       -- <https://github.com/input-output-hk/io-sim/issues>.
     | FailureInternal String
  deriving Int -> Failure -> ShowS
[Failure] -> ShowS
Failure -> [Char]
(Int -> Failure -> ShowS)
-> (Failure -> [Char]) -> ([Failure] -> ShowS) -> Show Failure
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Failure -> ShowS
showsPrec :: Int -> Failure -> ShowS
$cshow :: Failure -> [Char]
show :: Failure -> [Char]
$cshowList :: [Failure] -> ShowS
showList :: [Failure] -> ShowS
Show

instance Exception Failure where
    displayException :: Failure -> [Char]
displayException (FailureException SomeException
err) = SomeException -> [Char]
forall e. Exception e => e -> [Char]
displayException  SomeException
err
    displayException (FailureDeadlock [Labelled IOSimThreadId]
threads) =
      [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<io-sim deadlock: "
             , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (Labelled IOSimThreadId -> [Char]
forall a. Show a => a -> [Char]
show (Labelled IOSimThreadId -> [Char])
-> [Labelled IOSimThreadId] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
`map` [Labelled IOSimThreadId]
threads)
             , [Char]
">>"
             ]
    displayException (FailureSloppyShutdown [Labelled IOSimThreadId]
threads) =
      [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<io-sim sloppy shutdown: "
             , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (Labelled IOSimThreadId -> [Char]
forall a. Show a => a -> [Char]
show (Labelled IOSimThreadId -> [Char])
-> [Labelled IOSimThreadId] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
`map` [Labelled IOSimThreadId]
threads)
             , [Char]
">>"
             ]
    displayException (FailureEvaluation SomeException
err) =
      [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<evaluation error: "
             , SomeException -> [Char]
forall e. Exception e => e -> [Char]
displayException  SomeException
err
             , [Char]
">>"
             ]
    displayException (FailureInternal [Char]
msg) =
      [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<internal failure: "
             , [Char]
msg
             , [Char]
">>\n"
             , [Char]
"please report the issue at\n"
             , [Char]
"https://github.com/input-output-hk/io-sim/issues"
             ]


-- | '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 = Bool -> SimTrace a -> Either Failure a
forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
False ((forall s. IOSim s a) -> SimTrace a
forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace IOSim s a
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 s. IOSim s a) -> Either Failure a
forall a. (forall s. IOSim s a) -> Either Failure a
runSim IOSim s a
forall s. IOSim s a
mainAction of
      Left  Failure
e -> Failure -> a
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
-- clean-up 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 = Bool -> SimTrace a -> Either Failure a
forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
True ((forall s. IOSim s a) -> SimTrace a
forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace IOSim s a
forall s. IOSim s a
mainAction)

-- | Fold through the trace and return either 'Failure' or a 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 = IO (Either Failure a) -> Either Failure a
forall a. IO a -> a
unsafePerformIO (IO (Either Failure a) -> Either Failure a)
-> (SimTrace a -> IO (Either Failure a))
-> SimTrace a
-> Either Failure a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimTrace a -> IO (Either Failure a)
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 <- IO (SimTrace a) -> IO (Either SomeException (SimTrace a))
forall e a. Exception e => IO a -> IO (Either e a)
forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> m (Either e a)
try (SimTrace a -> IO (SimTrace a)
forall a. a -> IO a
forall (m :: * -> *) a. MonadEvaluate m => a -> m a
evaluate SimTrace a
a)
      case Either SomeException (SimTrace a)
r of
        Left SomeException
e  -> Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failure -> Either Failure a
forall a b. a -> Either a b
Left (SomeException -> Failure
FailureEvaluation SomeException
e))
        Right SimTrace a
_ -> SimTrace a -> IO (Either Failure 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
_ IOSimThreadId
_ Maybe [Char]
_ SimEventType
_ SimTrace a
t)             = SimTrace a -> IO (Either Failure a)
forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
    go (SimPORTrace Time
_ IOSimThreadId
_ Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
t)        = SimTrace a -> IO (Either Failure a)
forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
    go (TraceRacesFound [ScheduleControl]
_ SimTrace a
t)            = SimTrace a -> IO (Either Failure a)
forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
    go (TraceMainReturn Time
_ Labelled IOSimThreadId
_ a
_ tids :: [Labelled IOSimThreadId]
tids@(Labelled IOSimThreadId
_:[Labelled IOSimThreadId]
_))
                               | Bool
strict = Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Failure a -> IO (Either Failure a))
-> Either Failure a -> IO (Either Failure a)
forall a b. (a -> b) -> a -> b
$ Failure -> Either Failure a
forall a b. a -> Either a b
Left ([Labelled IOSimThreadId] -> Failure
FailureSloppyShutdown [Labelled IOSimThreadId]
tids)
    go (TraceMainReturn Time
_ Labelled IOSimThreadId
_ a
x [Labelled IOSimThreadId]
_)        = Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Failure a -> IO (Either Failure a))
-> Either Failure a -> IO (Either Failure a)
forall a b. (a -> b) -> a -> b
$ a -> Either Failure a
forall a b. b -> Either a b
Right a
x
    go (TraceMainException Time
_ Labelled IOSimThreadId
_ SomeException
e [Labelled IOSimThreadId]
_)     = Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Failure a -> IO (Either Failure a))
-> Either Failure a -> IO (Either Failure a)
forall a b. (a -> b) -> a -> b
$ Failure -> Either Failure a
forall a b. a -> Either a b
Left (SomeException -> Failure
FailureException SomeException
e)
    go (TraceDeadlock   Time
_   [Labelled IOSimThreadId]
threads)    = Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Failure a -> IO (Either Failure a))
-> Either Failure a -> IO (Either Failure a)
forall a b. (a -> b) -> a -> b
$ Failure -> Either Failure a
forall a b. a -> Either a b
Left ([Labelled IOSimThreadId] -> Failure
FailureDeadlock [Labelled IOSimThreadId]
threads)
    go TraceLoop{}                      = [Char] -> IO (Either Failure a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: traceResult TraceLoop{}"
    go (TraceInternalError [Char]
msg)         = Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Failure a -> IO (Either Failure a))
-> Either Failure a -> IO (Either Failure a)
forall a b. (a -> b) -> a -> b
$ Failure -> Either Failure a
forall a b. a -> Either a b
Left ([Char] -> Failure
FailureInternal [Char]
msg)

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


-- | Pretty print a timestamped event.
--
ppEvents :: [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
         -> String
ppEvents :: [(Time, IOSimThreadId, Maybe [Char], SimEventType)] -> [Char]
ppEvents [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
events =
    [Char] -> [[Char]] -> [Char]
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, IOSimThreadId
seThreadId :: IOSimThreadId
seThreadId :: IOSimThreadId
seThreadId, Maybe [Char]
seThreadLabel :: Maybe [Char]
seThreadLabel :: Maybe [Char]
seThreadLabel, SimEventType
seType :: SimEventType
seType :: SimEventType
seType }
      | (Time
seTime, IOSimThreadId
seThreadId, Maybe [Char]
seThreadLabel, SimEventType
seType) <- [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
events
      ]
  where
    timeWidth :: Int
timeWidth = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Time -> [Char]
forall a. Show a => a -> [Char]
show Time
t)
                | (Time
t, IOSimThreadId
_, Maybe [Char]
_, SimEventType
_) <- [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
events
                ]
    tidWidth :: Int
tidWidth  = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (IOSimThreadId -> [Char]
forall a. Show a => a -> [Char]
show IOSimThreadId
tid)
                | (Time
_, IOSimThreadId
tid, Maybe [Char]
_, SimEventType
_) <- [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
events
                ]
    width :: Int
width     = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ Int -> ([Char] -> Int) -> Maybe [Char] -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Maybe [Char]
threadLabel
                | (Time
_, IOSimThreadId
_, Maybe [Char]
threadLabel, SimEventType
_) <- [(Time, IOSimThreadId, 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 s. ST s (SimTrace a)) -> SimTrace a
forall a. (forall s. ST s a) -> a
runST (IOSim s a -> ST s (SimTrace a)
forall s a. IOSim s a -> ST s (SimTrace a)
runSimTraceST IOSim s a
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.MonadTimeout.NonStandard` 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 it is slower).
--
-- On property failure it will show the failing schedule (`ScheduleControl`)
-- which can be passed to `controlSimTrace` to reproduce the failure without
-- discovering the schedule.
--
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
main Maybe (SimTrace a) -> SimTrace a -> test
k =
    (forall s. ST s Property) -> Property
forall a. (forall s. ST s a) -> a
runST ((ExplorationOptions -> ExplorationOptions)
-> (forall s. IOSim s a)
-> (Maybe (SimTrace a) -> SimTrace a -> ST s test)
-> ST s Property
forall s a test.
Testable test =>
(ExplorationOptions -> ExplorationOptions)
-> (forall s. IOSim s a)
-> (Maybe (SimTrace a) -> SimTrace a -> ST s test)
-> ST s Property
exploreSimTraceST ExplorationOptions -> ExplorationOptions
optsf IOSim s a
forall s. IOSim s a
main (\Maybe (SimTrace a)
a SimTrace a
b -> test -> ST s test
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (SimTrace a) -> SimTrace a -> test
k Maybe (SimTrace a)
a SimTrace a
b)))


-- | An 'ST' version of 'exploreSimTrace'. The callback also receives
-- 'ScheduleControl'.  This is mostly useful for testing /IOSimPOR/ itself.
--
exploreSimTraceST
  :: forall s a test. Testable test
  => (ExplorationOptions -> ExplorationOptions)
  -> (forall s. IOSim s a)
  -> (Maybe (SimTrace a) -> SimTrace a -> ST s test)
  -> ST s Property
exploreSimTraceST :: forall s a test.
Testable test =>
(ExplorationOptions -> ExplorationOptions)
-> (forall s. IOSim s a)
-> (Maybe (SimTrace a) -> SimTrace a -> ST s test)
-> ST s Property
exploreSimTraceST ExplorationOptions -> ExplorationOptions
optsf forall s. IOSim s a
main Maybe (SimTrace a) -> SimTrace a -> ST s test
k =
    case ExplorationOptions -> Maybe ScheduleControl
explorationReplay ExplorationOptions
opts of
      Just ScheduleControl
control -> do
        SimTrace a
trace <- Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST (ExplorationOptions -> Maybe Int
explorationStepTimelimit ExplorationOptions
opts) ScheduleControl
control IOSim s a
forall s. IOSim s a
main
        [Char] -> test -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample ([Char]
"Schedule control: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ScheduleControl -> [Char]
forall a. Show a => a -> [Char]
show ScheduleControl
control)
          (test -> Property) -> ST s test -> ST s Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SimTrace a) -> SimTrace a -> ST s test
k Maybe (SimTrace a)
forall a. Maybe a
Nothing SimTrace a
trace
      Maybe ScheduleControl
Nothing -> do
        STRef s (Set ScheduleControl)
cacheRef <- ST s (STRef s (Set ScheduleControl))
createCacheST
        Property
prop <- STRef s (Set ScheduleControl)
-> Int
-> Int
-> ScheduleControl
-> Maybe (SimTrace a)
-> ST s Property
go STRef s (Set ScheduleControl)
cacheRef (ExplorationOptions -> Int
explorationScheduleBound ExplorationOptions
opts)
                            (ExplorationOptions -> Int
explorationBranching ExplorationOptions
opts)
                            ScheduleControl
ControlDefault Maybe (SimTrace a)
forall a. Maybe a
Nothing
        !Int
size <- STRef s (Set ScheduleControl) -> ST s Int
cacheSizeST STRef s (Set ScheduleControl)
cacheRef
        Property -> ST s Property
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> ST s Property) -> Property -> ST s Property
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> Property -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Modified schedules explored" [Int -> [Char]
bucket Int
size] Property
prop
  where
    opts :: ExplorationOptions
opts = ExplorationOptions -> ExplorationOptions
optsf ExplorationOptions
stdExplorationOptions

    go :: STRef s (Set ScheduleControl)
       -> Int -- schedule bound
       -> Int -- branching factor
       -> ScheduleControl
       -> Maybe (SimTrace a)
       -> ST s Property
    go :: STRef s (Set ScheduleControl)
-> Int
-> Int
-> ScheduleControl
-> Maybe (SimTrace a)
-> ST s Property
go STRef s (Set ScheduleControl)
cacheRef Int
n Int
m ScheduleControl
control Maybe (SimTrace a)
passingTrace = do
      SimTrace a
traceWithRaces <- Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
IOSimPOR.controlSimTraceST (ExplorationOptions -> Maybe Int
explorationStepTimelimit ExplorationOptions
opts) ScheduleControl
control IOSim s a
forall s. IOSim s a
main
      (ST s [ScheduleControl]
readRaces, SimTrace a
trace0) <- SimTrace a -> ST s (ST s [ScheduleControl], SimTrace a)
forall a s. SimTrace a -> ST s (ST s [ScheduleControl], SimTrace a)
detachTraceRacesST SimTrace a
traceWithRaces
      (ST
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
readSleeperST, SimTrace a
trace) <- Maybe (SimTrace a)
-> SimTrace a
-> ST
     s
     (ST
        s
        (Maybe
           ((Time, IOSimThreadId, Maybe [Char]),
            Set (IOSimThreadId, Maybe [Char]))),
      SimTrace a)
forall a b s.
Maybe (SimTrace a)
-> SimTrace b
-> ST
     s
     (ST
        s
        (Maybe
           ((Time, IOSimThreadId, Maybe [Char]),
            Set (IOSimThreadId, Maybe [Char]))),
      SimTrace b)
compareTracesST Maybe (SimTrace a)
passingTrace SimTrace a
trace0
      () <- Int -> SimTrace a -> ST s ()
forall a s. Int -> SimTrace a -> ST s ()
traceDebugLog (ExplorationOptions -> Int
explorationDebugLevel ExplorationOptions
opts) SimTrace a
traceWithRaces
      [ST s Property] -> ST s Property
forall prop s. TestableNoCatch prop => [ST s prop] -> ST s Property
conjoinNoCatchST
        [ do Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
sleeper <- ST
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
readSleeperST
             test
prop <- Maybe (SimTrace a) -> SimTrace a -> ST s test
k Maybe (SimTrace a)
passingTrace SimTrace a
trace
             Property -> ST s Property
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> ST s Property) -> Property -> ST s Property
forall a b. (a -> b) -> a -> b
$ [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample ([Char]
"Schedule control: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ScheduleControl -> [Char]
forall a. Show a => a -> [Char]
show ScheduleControl
control)
                    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ [Char] -> test -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample
                       (case Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
sleeper of
                         Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
Nothing -> [Char]
"No thread delayed"
                         Just ((Time
t,IOSimThreadId
tid,Maybe [Char]
lab),Set (IOSimThreadId, Maybe [Char])
racing) ->
                           (IOSimThreadId, Maybe [Char]) -> [Char]
showThread (IOSimThreadId
tid,Maybe [Char]
lab) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
                           [Char]
" delayed at time "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
                           Time -> [Char]
forall a. Show a => a -> [Char]
show Time
t [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
                           [Char]
"\n  until after:\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
                           [[Char]] -> [Char]
unlines (((IOSimThreadId, Maybe [Char]) -> [Char])
-> [(IOSimThreadId, Maybe [Char])] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"    "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++)ShowS
-> ((IOSimThreadId, Maybe [Char]) -> [Char])
-> (IOSimThreadId, Maybe [Char])
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(IOSimThreadId, Maybe [Char]) -> [Char]
showThread) ([(IOSimThreadId, Maybe [Char])] -> [[Char]])
-> [(IOSimThreadId, Maybe [Char])] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set (IOSimThreadId, Maybe [Char])
-> [(IOSimThreadId, Maybe [Char])]
forall a. Set a -> [a]
Set.toList Set (IOSimThreadId, Maybe [Char])
racing)
                        )
                      test
prop
        , do let limit :: Int
limit = (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int -> Int -> Int
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.
             [ScheduleControl]
races <- [Maybe ScheduleControl] -> [ScheduleControl]
forall a. [Maybe a] -> [a]
catMaybes
                  ([Maybe ScheduleControl] -> [ScheduleControl])
-> ST s [Maybe ScheduleControl] -> ST s [ScheduleControl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ST s [ScheduleControl]
readRaces ST s [ScheduleControl]
-> ([ScheduleControl] -> ST s [Maybe ScheduleControl])
-> ST s [Maybe ScheduleControl]
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (ScheduleControl -> ST s (Maybe ScheduleControl))
-> [ScheduleControl] -> ST s [Maybe ScheduleControl]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (STRef s (Set ScheduleControl)
-> ScheduleControl -> ST s (Maybe ScheduleControl)
cachedST STRef s (Set ScheduleControl)
cacheRef) ([ScheduleControl] -> ST s [Maybe ScheduleControl])
-> ([ScheduleControl] -> [ScheduleControl])
-> [ScheduleControl]
-> ST s [Maybe ScheduleControl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [ScheduleControl] -> [ScheduleControl]
forall a. Int -> [a] -> [a]
take Int
limit)
             let branching :: Int
branching = [ScheduleControl] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleControl]
races
             -- tabulate "Races explored" (map show races) $
             [Char] -> [[Char]] -> Property -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Branching factor" [Int -> [Char]
bucket Int
branching]
                (Property -> Property)
-> ([Property] -> Property) -> [Property] -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  [Char] -> [[Char]] -> Property -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Race reversals per schedule" [Int -> [Char]
bucket (ScheduleControl -> Int
raceReversals ScheduleControl
control)]
                (Property -> Property)
-> ([Property] -> Property) -> [Property] -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
               ([Property] -> Property) -> ST s [Property] -> ST s Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ST s Property] -> ST s [Property]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
                     [ STRef s (Set ScheduleControl)
-> Int
-> Int
-> ScheduleControl
-> Maybe (SimTrace a)
-> ST s Property
go STRef s (Set ScheduleControl)
cacheRef Int
n' ((Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` Int
1) ScheduleControl
r (SimTrace a -> Maybe (SimTrace a)
forall a. a -> Maybe a
Just SimTrace a
trace0)
                     | (ScheduleControl
r,Int
n') <- [ScheduleControl] -> [Int] -> [(ScheduleControl, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ScheduleControl]
races (Int -> Int -> [Int]
divide (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
branching) Int
branching) ]
        ]

    bucket :: Int -> String
    bucket :: Int -> [Char]
bucket Int
n | Int
nInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
10      = Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n
             | Bool
otherwise = Int -> Int -> [Char]
forall {t}. (Show t, Integral t) => t -> t -> [Char]
buck Int
n Int
1
    buck :: t -> t -> [Char]
buck t
n t
t | t
nt -> t -> Bool
forall a. Ord a => a -> a -> Bool
<t
10      = t -> [Char]
forall a. Show a => a -> [Char]
show (t
nt -> t -> t
forall a. Num a => a -> a -> a
*t
t) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"-" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> [Char]
forall a. Show a => a -> [Char]
show ((t
nt -> t -> t
forall a. Num a => a -> a -> a
+t
1)t -> t -> t
forall a. Num a => a -> a -> a
*t
tt -> t -> t
forall a. Num a => a -> a -> a
-t
1)
             | Bool
otherwise = t -> t -> [Char]
buck (t
n t -> t -> t
forall a. Integral a => a -> a -> a
`div` t
10) (t
tt -> t -> t
forall a. Num a => a -> a -> a
*t
10)

    -- divide n into k factors which sums up to n
    divide :: Int -> Int -> [Int]
    divide :: Int -> Int -> [Int]
divide Int
n Int
k =
      [ Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
k then Int
1 else Int
0
      | Int
i <- [Int
0..Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]

    showThread :: (IOSimThreadId,Maybe ThreadLabel) -> String
    showThread :: (IOSimThreadId, Maybe [Char]) -> [Char]
showThread (IOSimThreadId
tid,Maybe [Char]
lab) =
      IOSimThreadId -> [Char]
ppIOSimThreadId IOSimThreadId
tid [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (case Maybe [Char]
lab of Maybe [Char]
Nothing -> [Char]
""
                                          Just [Char]
l  -> [Char]
" ("[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
l[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
")")

    -- insert a schedule into the cache
    cachedST :: STRef s (Set ScheduleControl) -> ScheduleControl -> ST s (Maybe ScheduleControl)
    cachedST :: STRef s (Set ScheduleControl)
-> ScheduleControl -> ST s (Maybe ScheduleControl)
cachedST STRef s (Set ScheduleControl)
cacheRef ScheduleControl
a = do
      Set ScheduleControl
set <- STRef s (Set ScheduleControl) -> ST s (Set ScheduleControl)
forall s a. STRef s a -> ST s a
readSTRef STRef s (Set ScheduleControl)
cacheRef
      STRef s (Set ScheduleControl) -> Set ScheduleControl -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s (Set ScheduleControl)
cacheRef (ScheduleControl -> Set ScheduleControl -> Set ScheduleControl
forall a. Ord a => a -> Set a -> Set a
Set.insert ScheduleControl
a Set ScheduleControl
set)
      Maybe ScheduleControl -> ST s (Maybe ScheduleControl)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ScheduleControl -> ST s (Maybe ScheduleControl))
-> Maybe ScheduleControl -> ST s (Maybe ScheduleControl)
forall a b. (a -> b) -> a -> b
$ if ScheduleControl -> Set ScheduleControl -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ScheduleControl
a Set ScheduleControl
set
               then Maybe ScheduleControl
forall a. Maybe a
Nothing
               else ScheduleControl -> Maybe ScheduleControl
forall a. a -> Maybe a
Just ScheduleControl
a

    --
    -- Caching in ST 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.
    createCacheST :: ST s (STRef s (Set ScheduleControl))
    createCacheST :: ST s (STRef s (Set ScheduleControl))
createCacheST = Set ScheduleControl -> ST s (STRef s (Set ScheduleControl))
forall a s. a -> ST s (STRef s a)
newSTRef (Set ScheduleControl -> ST s (STRef s (Set ScheduleControl)))
-> Set ScheduleControl -> ST s (STRef s (Set ScheduleControl))
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>=Int
0
                then Set ScheduleControl
forall a. Set a
Set.empty
                else [Char] -> Set ScheduleControl
forall a. HasCallStack => [Char] -> a
error [Char]
"exploreSimTrace: negative schedule bound"

    cacheSizeST :: STRef s (Set ScheduleControl) -> ST s Int
    cacheSizeST :: STRef s (Set ScheduleControl) -> ST s Int
cacheSizeST = (Set ScheduleControl -> Int)
-> ST s (Set ScheduleControl) -> ST s Int
forall a b. (a -> b) -> ST s a -> ST s b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Set ScheduleControl -> Int
forall a. Set a -> Int
Set.size (ST s (Set ScheduleControl) -> ST s Int)
-> (STRef s (Set ScheduleControl) -> ST s (Set ScheduleControl))
-> STRef s (Set ScheduleControl)
-> ST s Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef s (Set ScheduleControl) -> ST s (Set ScheduleControl)
forall s a. STRef s a -> ST s a
readSTRef


-- |  Trace `SimTrace` to `stderr`.
--
traceDebugLog :: Int -> SimTrace a -> ST s ()
traceDebugLog :: forall a s. Int -> SimTrace a -> ST s ()
traceDebugLog Int
logLevel SimTrace a
_trace | Int
logLevel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = () -> ST s ()
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
traceDebugLog Int
1 SimTrace a
trace = [Char] -> ST s ()
forall (f :: * -> *). Applicative f => [Char] -> f ()
Debug.traceM ([Char] -> ST s ()) -> [Char] -> ST s ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Simulation trace with discovered schedules:\n"
                                    [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SimResult () -> [Char])
-> (SimEvent -> [Char]) -> Trace (SimResult ()) SimEvent -> [Char]
forall a b. (a -> [Char]) -> (b -> [Char]) -> Trace a b -> [Char]
Trace.ppTrace (Int -> Int -> Int -> SimResult () -> [Char]
forall a. Show a => Int -> Int -> Int -> SimResult a -> [Char]
ppSimResult Int
0 Int
0 Int
0) (Int -> Int -> Int -> SimEvent -> [Char]
ppSimEvent Int
0 Int
0 Int
0) (Trace (SimResult ()) SimEvent -> Trace (SimResult ()) SimEvent
forall a. SimTrace a -> SimTrace a
ignoreRaces (Trace (SimResult ()) SimEvent -> Trace (SimResult ()) SimEvent)
-> Trace (SimResult ()) SimEvent -> Trace (SimResult ()) SimEvent
forall a b. (a -> b) -> a -> b
$ SimResult a -> SimResult ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (SimResult a -> SimResult ())
-> SimTrace a -> Trace (SimResult ()) SimEvent
forall a b c. (a -> b) -> Trace a c -> Trace b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
`first` SimTrace a
trace)
traceDebugLog Int
_ SimTrace a
trace = [Char] -> ST s ()
forall (f :: * -> *). Applicative f => [Char] -> f ()
Debug.traceM ([Char] -> ST s ()) -> [Char] -> ST s ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Simulation trace with discovered schedules:\n"
                                    [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SimResult () -> [Char])
-> (SimEvent -> [Char]) -> Trace (SimResult ()) SimEvent -> [Char]
forall a b. (a -> [Char]) -> (b -> [Char]) -> Trace a b -> [Char]
Trace.ppTrace (Int -> Int -> Int -> SimResult () -> [Char]
forall a. Show a => Int -> Int -> Int -> SimResult a -> [Char]
ppSimResult Int
0 Int
0 Int
0) (Int -> Int -> Int -> SimEvent -> [Char]
ppSimEvent Int
0 Int
0 Int
0) (SimResult a -> SimResult ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (SimResult a -> SimResult ())
-> SimTrace a -> Trace (SimResult ()) SimEvent
forall a b c. (a -> b) -> Trace a c -> Trace b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
`first` 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
main =
    (forall s. ST s (SimTrace a)) -> SimTrace a
forall a. (forall s. ST s a) -> a
runST (Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST Maybe Int
limit ScheduleControl
control IOSim s a
forall s. IOSim s a
main)

controlSimTraceST :: Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST :: forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST Maybe Int
limit ScheduleControl
control IOSim s a
main =
  SimTrace a -> SimTrace a
forall a. SimTrace a -> SimTrace a
detachTraceRaces (SimTrace a -> SimTrace a)
-> ST s (SimTrace a) -> ST s (SimTrace a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
IOSimPOR.controlSimTraceST Maybe Int
limit ScheduleControl
control IOSim s a
main


--
-- Utils
--

ignoreRaces :: SimTrace a -> SimTrace a
ignoreRaces :: forall a. SimTrace a -> SimTrace a
ignoreRaces = (SimEvent -> Bool)
-> Trace (SimResult a) SimEvent -> Trace (SimResult a) SimEvent
forall b a. (b -> Bool) -> Trace a b -> Trace a b
Trace.filter (\SimEvent
a -> case SimEvent
a of
                                    SimPOREvent { seType :: SimEvent -> SimEventType
seType = EventRaces {} } -> Bool
False
                                    SimEvent
_ -> Bool
True)

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

-- `compareTracesST` 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`.

-- TODO: return StepId
compareTracesST :: forall a b s.
                   Maybe (SimTrace a) -- ^ passing
                -> SimTrace b         -- ^ failing
                -> ST s ( ST s (Maybe ( (Time, IOSimThreadId, Maybe ThreadLabel)
                                      , Set.Set (IOSimThreadId, Maybe ThreadLabel)
                                      ))
                        , SimTrace b
                        )
compareTracesST :: forall a b s.
Maybe (SimTrace a)
-> SimTrace b
-> ST
     s
     (ST
        s
        (Maybe
           ((Time, IOSimThreadId, Maybe [Char]),
            Set (IOSimThreadId, Maybe [Char]))),
      SimTrace b)
compareTracesST Maybe (SimTrace a)
Nothing SimTrace b
trace = (ST
   s
   (Maybe
      ((Time, IOSimThreadId, Maybe [Char]),
       Set (IOSimThreadId, Maybe [Char]))),
 SimTrace b)
-> ST
     s
     (ST
        s
        (Maybe
           ((Time, IOSimThreadId, Maybe [Char]),
            Set (IOSimThreadId, Maybe [Char]))),
      SimTrace b)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
-> ST
     s
     (Maybe
        ((Time, IOSimThreadId, Maybe [Char]),
         Set (IOSimThreadId, Maybe [Char])))
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
forall a. Maybe a
Nothing, SimTrace b
trace)
compareTracesST (Just SimTrace a
passing) SimTrace b
trace = do
  STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper <- Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
-> ST
     s
     (STRef
        s
        (Maybe
           ((Time, IOSimThreadId, Maybe [Char]),
            Set (IOSimThreadId, Maybe [Char]))))
forall a s. a -> ST s (STRef s a)
newSTRef Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
forall a. Maybe a
Nothing
  SimTrace b
trace' <- STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace b -> ST s (SimTrace b)
go STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper SimTrace a
passing SimTrace b
trace
  (ST
   s
   (Maybe
      ((Time, IOSimThreadId, Maybe [Char]),
       Set (IOSimThreadId, Maybe [Char]))),
 SimTrace b)
-> ST
     s
     (ST
        s
        (Maybe
           ((Time, IOSimThreadId, Maybe [Char]),
            Set (IOSimThreadId, Maybe [Char]))),
      SimTrace b)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ( STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> ST
     s
     (Maybe
        ((Time, IOSimThreadId, Maybe [Char]),
         Set (IOSimThreadId, Maybe [Char])))
forall s a. STRef s a -> ST s a
readSTRef STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper
         , SimTrace b
trace'
         )
  where
        go :: STRef s (Maybe ( (Time, IOSimThreadId, Maybe ThreadLabel)
                             , Set.Set (IOSimThreadId, Maybe ThreadLabel)
                             ))
           -> SimTrace a -- ^ passing
           -> SimTrace b -- ^ failing
           -> ST s (SimTrace b)
        go :: STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace b -> ST s (SimTrace b)
go STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper (SimPORTrace Time
tpass IOSimThreadId
tidpass Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
pass')
                   (SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail SimTrace b
fail')
          | (Time
tpass,IOSimThreadId
tidpass) (Time, IOSimThreadId) -> (Time, IOSimThreadId) -> Bool
forall a. Eq a => a -> a -> Bool
== (Time
tfail,IOSimThreadId
tidfail) =
              Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace b
-> SimTrace b
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
                (SimTrace b -> SimTrace b)
-> ST s (SimTrace b) -> ST s (SimTrace b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace b -> ST s (SimTrace b)
go STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper SimTrace a
pass' SimTrace b
fail'
        go STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper (SimPORTrace Time
tpass IOSimThreadId
tidpass Int
tsteppass Maybe [Char]
tlpass SimEventType
_ SimTrace a
_) SimTrace b
fail = do
          STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
-> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper (Maybe
   ((Time, IOSimThreadId, Maybe [Char]),
    Set (IOSimThreadId, Maybe [Char]))
 -> ST s ())
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
-> ST s ()
forall a b. (a -> b) -> a -> b
$ ((Time, IOSimThreadId, Maybe [Char]),
 Set (IOSimThreadId, Maybe [Char]))
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
forall a. a -> Maybe a
Just ((Time
tpass, IOSimThreadId
tidpass, Maybe [Char]
tlpass),Set (IOSimThreadId, Maybe [Char])
forall a. Set a
Set.empty)
          Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace b
-> SimTrace b
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tpass IOSimThreadId
tidpass Int
tsteppass Maybe [Char]
tlpass SimEventType
EventThreadSleep
            (SimTrace b -> SimTrace b)
-> ST s (SimTrace b) -> ST s (SimTrace b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> IOSimThreadId -> SimTrace b -> ST s (SimTrace b)
wakeup STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper IOSimThreadId
tidpass SimTrace b
fail
        go STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
_ SimTrace {} SimTrace b
_ = [Char] -> ST s (SimTrace b)
forall a. HasCallStack => [Char] -> a
error [Char]
"compareTracesST: invariant violation"
        go STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
_ SimTrace a
_ SimTrace {} = [Char] -> ST s (SimTrace b)
forall a. HasCallStack => [Char] -> a
error [Char]
"compareTracesST: invariant violation"
        go STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
_ SimTrace a
_ SimTrace b
fail = SimTrace b -> ST s (SimTrace b)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return SimTrace b
fail

        wakeup :: STRef s (Maybe ( (Time, IOSimThreadId, Maybe ThreadLabel)
                                 , Set.Set (IOSimThreadId, Maybe ThreadLabel)
                                 ))
               -> IOSimThreadId
               -> SimTrace b
               -> ST s (SimTrace b)
        wakeup :: STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> IOSimThreadId -> SimTrace b -> ST s (SimTrace b)
wakeup STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper IOSimThreadId
tidpass
               fail :: SimTrace b
fail@(SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail SimTrace b
fail')
          | IOSimThreadId
tidpass IOSimThreadId -> IOSimThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== IOSimThreadId
tidfail =
              SimTrace b -> ST s (SimTrace b)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace b -> ST s (SimTrace b))
-> SimTrace b -> ST s (SimTrace b)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace b
-> SimTrace b
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
EventThreadWake SimTrace b
fail
          | Bool
otherwise = do
              Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
ms <- STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> ST
     s
     (Maybe
        ((Time, IOSimThreadId, Maybe [Char]),
         Set (IOSimThreadId, Maybe [Char])))
forall s a. STRef s a -> ST s a
readSTRef STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper
              case Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
ms of
                Just ((Time, IOSimThreadId, Maybe [Char])
slp, Set (IOSimThreadId, Maybe [Char])
racing) -> do
                  STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
-> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper (Maybe
   ((Time, IOSimThreadId, Maybe [Char]),
    Set (IOSimThreadId, Maybe [Char]))
 -> ST s ())
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
-> ST s ()
forall a b. (a -> b) -> a -> b
$ ((Time, IOSimThreadId, Maybe [Char]),
 Set (IOSimThreadId, Maybe [Char]))
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
forall a. a -> Maybe a
Just ((Time, IOSimThreadId, Maybe [Char])
slp,(IOSimThreadId, Maybe [Char])
-> Set (IOSimThreadId, Maybe [Char])
-> Set (IOSimThreadId, Maybe [Char])
forall a. Ord a => a -> Set a -> Set a
Set.insert (IOSimThreadId
tidfail,Maybe [Char]
tlfail) Set (IOSimThreadId, Maybe [Char])
racing)
                  Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace b
-> SimTrace b
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
                    (SimTrace b -> SimTrace b)
-> ST s (SimTrace b) -> ST s (SimTrace b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> IOSimThreadId -> SimTrace b -> ST s (SimTrace b)
wakeup STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper IOSimThreadId
tidpass SimTrace b
fail'
                Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
Nothing -> [Char] -> ST s (SimTrace b)
forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraceST: invariant violation"
        wakeup STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
_ IOSimThreadId
_ SimTrace {} = [Char] -> ST s (SimTrace b)
forall a. HasCallStack => [Char] -> a
error [Char]
"compareTracesST: invariant violation"
        wakeup STRef
  s
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
_ IOSimThreadId
_ SimTrace b
fail = SimTrace b -> ST s (SimTrace b)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return SimTrace b
fail