{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
module Control.Monad.IOSim
(
IOSim
, STMSim
, runSim
, runSimOrThrow
, runSimStrictShutdown
, Failure (..)
, runSimTrace
, runSimTraceST
, exploreSimTrace
, exploreSimTraceST
, controlSimTrace
, controlSimTraceST
, ScheduleMod (..)
, ScheduleControl (..)
, ExplorationSpec
, ExplorationOptions (..)
, stdExplorationOptions
, withScheduleBound
, withBranching
, withStepTimelimit
, withReplay
, liftST
, setCurrentTime
, unshareClock
, type SimTrace
, Trace (Cons,
Nil,
SimTrace,
SimPORTrace,
TraceDeadlock,
TraceLoop,
TraceMainReturn,
TraceMainException,
TraceRacesFound,
TraceInternalError)
, SimResult (..)
, SimEvent (..)
, SimEventType (..)
, ThreadLabel
, IOSimThreadId (..)
, Labelled (..)
, traceM
, traceSTM
, ppTrace
, ppTrace_
, ppEvents
, ppSimEvent
, ppDebug
, traceEvents
, traceResult
, selectTraceEvents
, selectTraceEvents'
, selectTraceEventsDynamic
, selectTraceEventsDynamicWithTime
, selectTraceEventsDynamic'
, selectTraceEventsDynamicWithTime'
, selectTraceEventsSay
, selectTraceEventsSayWithTime
, selectTraceEventsSay'
, selectTraceEventsSayWithTime'
, selectTraceRaces
, traceSelectTraceEvents
, traceSelectTraceEventsDynamic
, traceSelectTraceEventsSay
, printTraceEventsSay
, EventlogEvent (..)
, EventlogMarker (..)
, 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 qualified Data.Set as Set
import Data.Typeable (Typeable)
import Data.List.Trace (Trace (..))
import qualified Data.List.Trace 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 qualified Control.Monad.IOSimPOR.Internal as IOSimPOR (controlSimTraceST)
import Control.Monad.IOSimPOR.QuickCheckUtils
import Test.QuickCheck
import System.IO.Unsafe
import qualified Debug.Trace as Debug
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
_ Labelled IOSimThreadId
_ SomeException
e [Labelled IOSimThreadId]
_ -> forall a e. Exception e => e -> a
throw (SomeException -> Failure
FailureException SomeException
e)
Deadlock Time
_ [Labelled IOSimThreadId]
threads -> 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 -> forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: selectTraceEvents _ TraceLoop{}"
InternalError [Char]
msg -> forall a e. Exception e => e -> a
throw ([Char] -> Failure
FailureInternal [Char]
msg)
)
( \ 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
_ 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 forall a. [a] -> [a] -> [a]
++ SimTrace a -> [ScheduleControl]
go SimTrace a
trace
go SimTrace a
_ = []
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 <- forall a s. a -> ST s (STRef s a)
newSTRef []
let readRaces :: ST s [ScheduleControl]
readRaces :: ST s [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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef STRef s [[ScheduleControl]]
races ([ScheduleControl]
rsforall 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) = forall a.
Time
-> IOSimThreadId
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
a IOSimThreadId
b Maybe [Char]
c SimEventType
d 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) = forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
a IOSimThreadId
b Int
c Maybe [Char]
d SimEventType
e 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 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 = 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
forall (m :: * -> *) a. Monad m => a -> m a
return (ST s [ScheduleControl]
readRaces, SimTrace a
trace)
detachTraceRaces :: forall a. SimTrace a -> SimTrace a
detachTraceRaces :: forall a. SimTrace a -> SimTrace a
detachTraceRaces = 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)
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
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
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
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
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
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
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
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
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
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
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
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
data Failure =
FailureException SomeException
| FailureDeadlock ![Labelled IOSimThreadId]
| FailureSloppyShutdown [Labelled IOSimThreadId]
| FailureEvaluation SomeException
| FailureInternal String
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 IOSimThreadId]
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 IOSimThreadId]
threads)
, [Char]
">>"
]
displayException (FailureSloppyShutdown [Labelled IOSimThreadId]
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 IOSimThreadId]
threads)
, [Char]
">>"
]
displayException (FailureEvaluation SomeException
err) =
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<evaluation error: "
, forall e. Exception e => e -> [Char]
displayException SomeException
err
, [Char]
">>"
]
displayException (FailureInternal [Char]
msg) =
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"
]
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)
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
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)
traceResult :: Bool
-> SimTrace a
-> 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
_ IOSimThreadId
_ Maybe [Char]
_ SimEventType
_ SimTrace a
t) = forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
go (SimPORTrace Time
_ IOSimThreadId
_ 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
_ Labelled IOSimThreadId
_ a
_ tids :: [Labelled IOSimThreadId]
tids@(Labelled IOSimThreadId
_:[Labelled IOSimThreadId]
_))
| 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 IOSimThreadId] -> Failure
FailureSloppyShutdown [Labelled IOSimThreadId]
tids)
go (TraceMainReturn Time
_ Labelled IOSimThreadId
_ a
x [Labelled IOSimThreadId]
_) = 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
_ Labelled IOSimThreadId
_ SomeException
e [Labelled IOSimThreadId]
_) = 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 IOSimThreadId]
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 IOSimThreadId] -> Failure
FailureDeadlock [Labelled IOSimThreadId]
threads)
go TraceLoop{} = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: traceResult TraceLoop{}"
go (TraceInternalError [Char]
msg) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([Char] -> Failure
FailureInternal [Char]
msg)
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)
forall a. a -> [a] -> [a]
: 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)
forall a. a -> [a] -> [a]
: forall a.
SimTrace a -> [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
traceEvents SimTrace a
t
traceEvents SimTrace a
_ = []
ppEvents :: [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
-> String
ppEvents :: [(Time, IOSimThreadId, Maybe [Char], SimEventType)] -> [Char]
ppEvents [(Time, IOSimThreadId, 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, 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 = 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, IOSimThreadId
_, Maybe [Char]
_, SimEventType
_) <- [(Time, IOSimThreadId, 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 IOSimThreadId
tid)
| (Time
_, IOSimThreadId
tid, Maybe [Char]
_, SimEventType
_) <- [(Time, IOSimThreadId, 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
_, IOSimThreadId
_, Maybe [Char]
threadLabel, SimEventType
_) <- [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
events
]
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)
exploreSimTrace
:: forall a test. Testable test
=> (ExplorationOptions -> ExplorationOptions)
-> (forall s. IOSim s a)
-> (Maybe (SimTrace a) -> SimTrace a -> test)
-> 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 a. (forall s. ST s a) -> a
runST (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)
a SimTrace a
b -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (SimTrace a) -> SimTrace a -> test
k Maybe (SimTrace a)
a SimTrace a
b)))
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 <- forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST (ExplorationOptions -> Maybe Int
explorationStepTimelimit ExplorationOptions
opts) ScheduleControl
control forall s. IOSim s a
main
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SimTrace a) -> SimTrace a -> ST s test
k 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 forall a. Maybe a
Nothing
!Int
size <- STRef s (Set ScheduleControl) -> ST s Int
cacheSizeST STRef s (Set ScheduleControl)
cacheRef
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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
-> Int
-> 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 <- forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
IOSimPOR.controlSimTraceST (ExplorationOptions -> Maybe Int
explorationStepTimelimit ExplorationOptions
opts) ScheduleControl
control forall s. IOSim s a
main
(ST s [ScheduleControl]
readRaces, SimTrace a
trace0) <- 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) <- 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
() <- forall a s. Int -> SimTrace a -> ST s ()
traceDebugLog (ExplorationOptions -> Int
explorationDebugLevel ExplorationOptions
opts) SimTrace a
traceWithRaces
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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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, 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) 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
.(IOSimThreadId, Maybe [Char]) -> [Char]
showThread) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set (IOSimThreadId, Maybe [Char])
racing)
)
test
prop
, do 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
[ScheduleControl]
races <- forall a. [Maybe a] -> [a]
catMaybes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ST s [ScheduleControl]
readRaces forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (STRef s (Set ScheduleControl)
-> ScheduleControl -> ST s (Maybe ScheduleControl)
cachedST STRef s (Set ScheduleControl)
cacheRef) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
limit)
let branching :: Int
branching = forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleControl]
races
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Branching factor" [Int -> [Char]
bucket Int
branching]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Race reversals per schedule" [Int -> [Char]
bucket (ScheduleControl -> Int
raceReversals ScheduleControl
control)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => [prop] -> Property
conjoin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
[ STRef s (Set ScheduleControl)
-> Int
-> Int
-> ScheduleControl
-> Maybe (SimTrace a)
-> ST s Property
go STRef s (Set ScheduleControl)
cacheRef 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
| Bool
otherwise = forall {t}. (Show t, Integral t) => t -> t -> [Char]
buck Int
n Int
1
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)
| Bool
otherwise = 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)
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
i forall 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 :: (IOSimThreadId,Maybe ThreadLabel) -> String
showThread :: (IOSimThreadId, Maybe [Char]) -> [Char]
showThread (IOSimThreadId
tid,Maybe [Char]
lab) =
IOSimThreadId -> [Char]
ppIOSimThreadId IOSimThreadId
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]
")")
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 <- forall s a. STRef s a -> ST s a
readSTRef STRef s (Set ScheduleControl)
cacheRef
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s (Set ScheduleControl)
cacheRef (forall a. Ord a => a -> Set a -> Set a
Set.insert ScheduleControl
a Set ScheduleControl
set)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if forall a. Ord a => a -> Set a -> Bool
Set.member ScheduleControl
a Set ScheduleControl
set
then forall a. Maybe a
Nothing
else forall a. a -> Maybe a
Just ScheduleControl
a
createCacheST :: ST s (STRef s (Set ScheduleControl))
createCacheST :: ST s (STRef s (Set ScheduleControl))
createCacheST = forall a s. a -> ST s (STRef s a)
newSTRef forall a b. (a -> b) -> a -> b
$
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"
cacheSizeST :: STRef s (Set ScheduleControl) -> ST s Int
cacheSizeST :: STRef s (Set ScheduleControl) -> ST s Int
cacheSizeST = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Set a -> Int
Set.size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. STRef s a -> ST s a
readSTRef
traceDebugLog :: Int -> SimTrace a -> ST s ()
traceDebugLog :: forall a s. Int -> SimTrace a -> ST s ()
traceDebugLog Int
logLevel SimTrace a
_trace | Int
logLevel forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
traceDebugLog Int
1 SimTrace a
trace = forall (f :: * -> *). Applicative f => [Char] -> f ()
Debug.traceM forall a b. (a -> b) -> a -> b
$ [Char]
"Simulation trace with discovered schedules:\n"
forall a. [a] -> [a] -> [a]
++ forall a b. (a -> [Char]) -> (b -> [Char]) -> Trace a b -> [Char]
Trace.ppTrace (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) (forall a. SimTrace a -> SimTrace a
ignoreRaces forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Functor f => f a -> f ()
void forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
`first` SimTrace a
trace)
traceDebugLog Int
_ SimTrace a
trace = forall (f :: * -> *). Applicative f => [Char] -> f ()
Debug.traceM forall a b. (a -> b) -> a -> b
$ [Char]
"Simulation trace with discovered schedules:\n"
forall a. [a] -> [a] -> [a]
++ forall a b. (a -> [Char]) -> (b -> [Char]) -> Trace a b -> [Char]
Trace.ppTrace (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) (forall (f :: * -> *) a. Functor f => f a -> f ()
void forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
`first` SimTrace a
trace)
controlSimTrace :: forall a.
Maybe Int
-> ScheduleControl
-> (forall s. IOSim s a)
-> 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 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
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 =
forall a. SimTrace a -> SimTrace a
detachTraceRaces forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
IOSimPOR.controlSimTraceST Maybe Int
limit ScheduleControl
control IOSim s a
main
ignoreRaces :: SimTrace a -> SimTrace a
ignoreRaces :: forall a. SimTrace a -> SimTrace a
ignoreRaces = 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) = forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleMod]
mods
raceReversals ControlFollow{} = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: raceReversals ControlFollow{}"
compareTracesST :: forall a b s.
Maybe (SimTrace a)
-> SimTrace b
-> 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall a s. a -> ST s (STRef s a)
newSTRef 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
forall (m :: * -> *) a. Monad m => a -> m a
return ( 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
-> SimTrace b
-> 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) forall a. Eq a => a -> a -> Bool
== (Time
tfail,IOSimThreadId
tidfail) =
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
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
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef
s
(Maybe
((Time, IOSimThreadId, Maybe [Char]),
Set (IOSimThreadId, Maybe [Char])))
sleeper forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ((Time
tpass, IOSimThreadId
tidpass, Maybe [Char]
tlpass),forall a. Set a
Set.empty)
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tpass IOSimThreadId
tidpass Int
tsteppass Maybe [Char]
tlpass SimEventType
EventThreadSleep
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
_ = 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 {} = 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 = 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 forall a. Eq a => a -> a -> Bool
== IOSimThreadId
tidfail =
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> 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 <- 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
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef
s
(Maybe
((Time, IOSimThreadId, Maybe [Char]),
Set (IOSimThreadId, Maybe [Char])))
sleeper forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ((Time, IOSimThreadId, Maybe [Char])
slp,forall a. Ord a => a -> Set a -> Set a
Set.insert (IOSimThreadId
tidfail,Maybe [Char]
tlfail) Set (IOSimThreadId, Maybe [Char])
racing)
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
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 -> forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraceST: invariant violation"
wakeup STRef
s
(Maybe
((Time, IOSimThreadId, Maybe [Char]),
Set (IOSimThreadId, Maybe [Char])))
_ IOSimThreadId
_ SimTrace {} = 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 = forall (m :: * -> *) a. Monad m => a -> m a
return SimTrace b
fail