{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
module Control.Monad.IOSim
(
IOSim
, STMSim
, runSim
, runSimOrThrow
, runSimStrictShutdown
, Failure (..)
, runSimTrace
, runSimTraceST
, exploreSimTrace
, controlSimTrace
, ScheduleMod (..)
, ScheduleControl (..)
, ExplorationSpec
, ExplorationOptions (..)
, stdExplorationOptions
, withScheduleBound
, withBranching
, withStepTimelimit
, withReplay
, liftST
, setCurrentTime
, unshareClock
, type SimTrace
, Trace (Cons, Nil, SimTrace, SimPORTrace, TraceDeadlock, TraceLoop, TraceMainReturn, TraceMainException, TraceRacesFound)
, SimResult (..)
, SimEvent (..)
, SimEventType (..)
, ThreadLabel
, Labelled (..)
, traceM
, traceSTM
, ppTrace
, ppTrace_
, ppEvents
, ppSimEvent
, ppDebug
, traceEvents
, traceResult
, selectTraceEvents
, selectTraceEvents'
, selectTraceEventsDynamic
, selectTraceEventsDynamic'
, selectTraceEventsSay
, selectTraceEventsSay'
, selectTraceRaces
, traceSelectTraceEvents
, traceSelectTraceEventsDynamic
, traceSelectTraceEventsSay
, printTraceEventsSay
, EventlogEvent (..)
, EventlogMarker (..)
, newTimeout
, readTimeout
, cancelTimeout
, awaitTimeout
) where
import Prelude
import Data.Bifoldable
import Data.Dynamic (fromDynamic)
import Data.List (intercalate)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable (Typeable)
import Data.List.Trace (Trace (..))
import Control.Exception (throw)
import Control.Monad.ST.Lazy
import Control.Monad.Class.MonadThrow as MonadThrow
import Control.Monad.IOSim.Internal (runSimTraceST)
import Control.Monad.IOSim.Types
import Control.Monad.IOSimPOR.Internal (controlSimTraceST)
import Control.Monad.IOSimPOR.QuickCheckUtils
import Test.QuickCheck
import Data.IORef
import System.IO.Unsafe
selectTraceEvents
:: (SimEventType -> Maybe b)
-> SimTrace a
-> [b]
selectTraceEvents :: forall b a. (SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents SimEventType -> Maybe b
fn =
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr ( \ SimResult a
v [b]
_
-> case SimResult a
v of
MainException Time
_ SomeException
e [Labelled ThreadId]
_ -> forall a e. Exception e => e -> a
throw (SomeException -> Failure
FailureException SomeException
e)
Deadlock Time
_ [Labelled ThreadId]
threads -> forall a e. Exception e => e -> a
throw ([Labelled ThreadId] -> Failure
FailureDeadlock [Labelled ThreadId]
threads)
MainReturn Time
_ a
_ [Labelled ThreadId]
_ -> []
SimResult a
Loop -> forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: selectTraceEvents _ TraceLoop{}"
)
( \ b
b [b]
acc -> b
b forall a. a -> [a] -> [a]
: [b]
acc )
[]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a.
(SimEventType -> Maybe b) -> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents SimEventType -> Maybe b
fn
selectTraceEvents'
:: (SimEventType -> Maybe b)
-> SimTrace a
-> [b]
selectTraceEvents' :: forall b a. (SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' 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.
(SimEventType -> Maybe b) -> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents SimEventType -> Maybe b
fn
selectTraceRaces :: SimTrace a -> [ScheduleControl]
selectTraceRaces :: forall a. SimTrace a -> [ScheduleControl]
selectTraceRaces = forall a. SimTrace a -> [ScheduleControl]
go
where
go :: SimTrace a -> [ScheduleControl]
go (SimTrace Time
_ ThreadId
_ Maybe [Char]
_ SimEventType
_ SimTrace a
trace) = SimTrace a -> [ScheduleControl]
go SimTrace a
trace
go (SimPORTrace Time
_ ThreadId
_ Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
trace) = SimTrace a -> [ScheduleControl]
go SimTrace a
trace
go (TraceRacesFound [ScheduleControl]
races SimTrace a
trace) =
[ScheduleControl]
races forall a. [a] -> [a] -> [a]
++ SimTrace a -> [ScheduleControl]
go SimTrace a
trace
go SimTrace a
_ = []
detachTraceRaces :: SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces :: forall a. SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces SimTrace a
trace = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
IORef [[ScheduleControl]]
races <- forall a. a -> IO (IORef a)
newIORef []
let readRaces :: () -> [ScheduleControl]
readRaces () = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef [[ScheduleControl]]
races
saveRaces :: [ScheduleControl] -> a -> a
saveRaces [ScheduleControl]
r a
t = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [[ScheduleControl]]
races ([ScheduleControl]
rforall a. a -> [a] -> [a]
:)
forall (m :: * -> *) a. Monad m => a -> m a
return a
t
let go :: SimTrace a -> SimTrace a
go (SimTrace Time
a ThreadId
b Maybe [Char]
c SimEventType
d SimTrace a
trace) = forall a.
Time
-> ThreadId
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
a ThreadId
b Maybe [Char]
c SimEventType
d forall a b. (a -> b) -> a -> b
$ SimTrace a -> SimTrace a
go SimTrace a
trace
go (SimPORTrace Time
a ThreadId
b Int
c Maybe [Char]
d SimEventType
e SimTrace a
trace) = forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
a ThreadId
b Int
c Maybe [Char]
d SimEventType
e forall a b. (a -> b) -> a -> b
$ SimTrace a -> SimTrace a
go SimTrace a
trace
go (TraceRacesFound [ScheduleControl]
r SimTrace a
trace) = forall {a}. [ScheduleControl] -> a -> a
saveRaces [ScheduleControl]
r forall a b. (a -> b) -> a -> b
$ SimTrace a -> SimTrace a
go SimTrace a
trace
go SimTrace a
t = SimTrace a
t
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> [ScheduleControl]
readRaces, forall {a}. SimTrace a -> SimTrace a
go SimTrace a
trace)
selectTraceEventsDynamic :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic = forall b a. (SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents SimEventType -> Maybe b
fn
where
fn :: SimEventType -> Maybe b
fn :: SimEventType -> Maybe b
fn (EventLog Dynamic
dyn) = forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
fn 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. (SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' SimEventType -> Maybe b
fn
where
fn :: SimEventType -> Maybe b
fn :: SimEventType -> Maybe b
fn (EventLog Dynamic
dyn) = forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
fn SimEventType
_ = forall a. Maybe a
Nothing
selectTraceEventsSay :: SimTrace a -> [String]
selectTraceEventsSay :: forall a. SimTrace a -> [[Char]]
selectTraceEventsSay = forall b a. (SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents SimEventType -> Maybe [Char]
fn
where
fn :: SimEventType -> Maybe String
fn :: SimEventType -> Maybe [Char]
fn (EventSay [Char]
s) = forall a. a -> Maybe a
Just [Char]
s
fn SimEventType
_ = forall a. Maybe a
Nothing
selectTraceEventsSay' :: SimTrace a -> [String]
selectTraceEventsSay' :: forall a. SimTrace a -> [[Char]]
selectTraceEventsSay' = forall b a. (SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' SimEventType -> Maybe [Char]
fn
where
fn :: SimEventType -> Maybe String
fn :: SimEventType -> Maybe [Char]
fn (EventSay [Char]
s) = forall a. a -> Maybe a
Just [Char]
s
fn 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
:: (SimEventType -> Maybe b)
-> SimTrace a
-> Trace (SimResult a) b
traceSelectTraceEvents :: forall b a.
(SimEventType -> Maybe b) -> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents 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 SimEventType -> Maybe b
fn (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 SimEventType -> Maybe b
fn (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.
(SimEventType -> Maybe b) -> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents SimEventType -> Maybe b
fn
where
fn :: SimEventType -> Maybe b
fn :: SimEventType -> Maybe b
fn (EventLog Dynamic
dyn) = forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
fn 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.
(SimEventType -> Maybe b) -> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents SimEventType -> Maybe [Char]
fn
where
fn :: SimEventType -> Maybe String
fn :: SimEventType -> Maybe [Char]
fn (EventSay [Char]
s) = forall a. a -> Maybe a
Just [Char]
s
fn SimEventType
_ = forall a. Maybe a
Nothing
data Failure =
FailureException SomeException
| FailureDeadlock ![Labelled ThreadId]
| FailureSloppyShutdown [Labelled ThreadId]
| FailureEvaluation SomeException
deriving Int -> Failure -> ShowS
[Failure] -> ShowS
Failure -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Failure] -> ShowS
$cshowList :: [Failure] -> ShowS
show :: Failure -> [Char]
$cshow :: Failure -> [Char]
showsPrec :: Int -> Failure -> ShowS
$cshowsPrec :: Int -> Failure -> ShowS
Show
instance Exception Failure where
displayException :: Failure -> [Char]
displayException (FailureException SomeException
err) = forall e. Exception e => e -> [Char]
displayException SomeException
err
displayException (FailureDeadlock [Labelled ThreadId]
threads) =
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<io-sim deadlock: "
, forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> [a] -> [b]
`map` [Labelled ThreadId]
threads)
, [Char]
">>"
]
displayException (FailureSloppyShutdown [Labelled ThreadId]
threads) =
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<io-sim sloppy shutdown: "
, forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> [a] -> [b]
`map` [Labelled ThreadId]
threads)
, [Char]
">>"
]
displayException (FailureEvaluation SomeException
err) = [Char]
"evaluation error:" forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> [Char]
displayException SomeException
err
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
_ ThreadId
_ Maybe [Char]
_ SimEventType
_ SimTrace a
t) = forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
go (SimPORTrace Time
_ ThreadId
_ Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
t) = forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
go (TraceRacesFound [ScheduleControl]
_ SimTrace a
t) = forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
go (TraceMainReturn Time
_ a
_ tids :: [Labelled ThreadId]
tids@(Labelled ThreadId
_:[Labelled ThreadId]
_))
| Bool
strict = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([Labelled ThreadId] -> Failure
FailureSloppyShutdown [Labelled ThreadId]
tids)
go (TraceMainReturn Time
_ a
x [Labelled ThreadId]
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right a
x
go (TraceMainException Time
_ SomeException
e [Labelled ThreadId]
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (SomeException -> Failure
FailureException SomeException
e)
go (TraceDeadlock Time
_ [Labelled ThreadId]
threads) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([Labelled ThreadId] -> Failure
FailureDeadlock [Labelled ThreadId]
threads)
go TraceLoop{} = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: traceResult TraceLoop{}"
traceEvents :: SimTrace a -> [(Time, ThreadId, Maybe ThreadLabel, SimEventType)]
traceEvents :: forall a.
SimTrace a -> [(Time, ThreadId, Maybe [Char], SimEventType)]
traceEvents (SimTrace Time
time ThreadId
tid Maybe [Char]
tlbl SimEventType
event SimTrace a
t) = (Time
time, ThreadId
tid, Maybe [Char]
tlbl, SimEventType
event)
forall a. a -> [a] -> [a]
: forall a.
SimTrace a -> [(Time, ThreadId, Maybe [Char], SimEventType)]
traceEvents SimTrace a
t
traceEvents (SimPORTrace Time
time ThreadId
tid Int
_ Maybe [Char]
tlbl SimEventType
event SimTrace a
t) = (Time
time, ThreadId
tid, Maybe [Char]
tlbl, SimEventType
event)
forall a. a -> [a] -> [a]
: forall a.
SimTrace a -> [(Time, ThreadId, Maybe [Char], SimEventType)]
traceEvents SimTrace a
t
traceEvents SimTrace a
_ = []
ppEvents :: [(Time, ThreadId, Maybe ThreadLabel, SimEventType)]
-> String
ppEvents :: [(Time, ThreadId, Maybe [Char], SimEventType)] -> [Char]
ppEvents [(Time, ThreadId, Maybe [Char], SimEventType)]
events =
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n"
[ Int -> Int -> Int -> SimEvent -> [Char]
ppSimEvent Int
timeWidth Int
tidWidth Int
width
SimEvent {Time
seTime :: Time
seTime :: Time
seTime, ThreadId
seThreadId :: ThreadId
seThreadId :: ThreadId
seThreadId, Maybe [Char]
seThreadLabel :: Maybe [Char]
seThreadLabel :: Maybe [Char]
seThreadLabel, SimEventType
seType :: SimEventType
seType :: SimEventType
seType }
| (Time
seTime, ThreadId
seThreadId, Maybe [Char]
seThreadLabel, SimEventType
seType) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
]
where
timeWidth :: Int
timeWidth = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
[ forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Show a => a -> [Char]
show Time
t)
| (Time
t, ThreadId
_, Maybe [Char]
_, SimEventType
_) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
]
tidWidth :: Int
tidWidth = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
[ forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Show a => a -> [Char]
show ThreadId
tid)
| (Time
_, ThreadId
tid, Maybe [Char]
_, SimEventType
_) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
]
width :: Int
width = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
[ forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 forall (t :: * -> *) a. Foldable t => t a -> Int
length Maybe [Char]
threadLabel
| (Time
_, ThreadId
_, Maybe [Char]
threadLabel, SimEventType
_) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
]
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
mainAction Maybe (SimTrace a) -> SimTrace a -> test
k =
case ExplorationOptions -> Maybe ScheduleControl
explorationReplay ExplorationOptions
opts of
Maybe ScheduleControl
Nothing ->
Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore (ExplorationOptions -> Int
explorationScheduleBound ExplorationOptions
opts) (ExplorationOptions -> Int
explorationBranching ExplorationOptions
opts) ScheduleControl
ControlDefault forall a. Maybe a
Nothing forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&.
let size :: Int
size = () -> Int
cacheSize() in Int
size seq :: forall a b. a -> b -> b
`seq`
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Modified schedules explored" [Int -> [Char]
bucket Int
size] Bool
True
Just ScheduleControl
control ->
forall a test.
Testable test =>
ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (SimTrace a -> test)
-> Property
replaySimTrace ExplorationOptions
opts forall s. IOSim s a
mainAction ScheduleControl
control (Maybe (SimTrace a) -> SimTrace a -> test
k forall a. Maybe a
Nothing)
where
opts :: ExplorationOptions
opts = ExplorationOptions -> ExplorationOptions
optsf ExplorationOptions
stdExplorationOptions
explore :: Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore :: Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore Int
n Int
m ScheduleControl
control Maybe (SimTrace a)
passingTrace =
let (() -> [ScheduleControl]
readRaces, SimTrace a
trace0) = forall a. SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces forall a b. (a -> b) -> a -> b
$
forall a.
Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
controlSimTrace
(ExplorationOptions -> Maybe Int
explorationStepTimelimit ExplorationOptions
opts) ScheduleControl
control forall s. IOSim s a
mainAction
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
sleeper,SimTrace a
trace) = forall a1 a2.
Maybe (SimTrace a1)
-> SimTrace a2
-> (Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
SimTrace a2)
compareTraces Maybe (SimTrace a)
passingTrace SimTrace a
trace0
in ( forall prop. Testable prop => [Char] -> prop -> Property
counterexample ([Char]
"Schedule control: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ScheduleControl
control)
forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => [Char] -> prop -> Property
counterexample
(case Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
sleeper of
Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
Nothing -> [Char]
"No thread delayed"
Just ((Time
t,ThreadId
tid,Maybe [Char]
lab),Set (ThreadId, Maybe [Char])
racing) ->
(ThreadId, Maybe [Char]) -> [Char]
showThread (ThreadId
tid,Maybe [Char]
lab) forall a. [a] -> [a] -> [a]
++
[Char]
" delayed at time "forall a. [a] -> [a] -> [a]
++
forall a. Show a => a -> [Char]
show Time
t forall a. [a] -> [a] -> [a]
++
[Char]
"\n until after:\n" forall a. [a] -> [a] -> [a]
++
[[Char]] -> [Char]
unlines (forall a b. (a -> b) -> [a] -> [b]
map (([Char]
" "forall a. [a] -> [a] -> [a]
++)forall b c a. (b -> c) -> (a -> b) -> a -> c
.(ThreadId, Maybe [Char]) -> [Char]
showThread) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set (ThreadId, Maybe [Char])
racing)
)
forall a b. (a -> b) -> a -> b
$ Maybe (SimTrace a) -> SimTrace a -> test
k Maybe (SimTrace a)
passingTrace SimTrace a
trace
)
forall prop. TestableNoCatch prop => prop -> prop -> Property
.&&| let limit :: Int
limit = (Int
nforall a. Num a => a -> a -> a
+Int
mforall a. Num a => a -> a -> a
-Int
1) forall a. Integral a => a -> a -> a
`div` Int
m
races :: [ScheduleControl]
races = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScheduleControl -> Bool
cached) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
limit forall a b. (a -> b) -> a -> b
$ () -> [ScheduleControl]
readRaces ()
branching :: Int
branching = forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleControl]
races
in
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Branching factor" [Int -> [Char]
bucket Int
branching] forall a b. (a -> b) -> a -> b
$
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Race reversals per schedule" [Int -> [Char]
bucket (ScheduleControl -> Int
raceReversals ScheduleControl
control)] forall a b. (a -> b) -> a -> b
$
forall prop. TestableNoCatch prop => [prop] -> Property
conjoinPar
[
Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore Int
n' ((Int
mforall a. Num a => a -> a -> a
-Int
1) forall a. Ord a => a -> a -> a
`max` Int
1) ScheduleControl
r (forall a. a -> Maybe a
Just SimTrace a
trace0)
| (ScheduleControl
r,Int
n') <- forall a b. [a] -> [b] -> [(a, b)]
zip [ScheduleControl]
races (Int -> Int -> [Int]
divide (Int
nforall a. Num a => a -> a -> a
-Int
branching) Int
branching) ]
bucket :: Int -> String
bucket :: Int -> [Char]
bucket Int
n | Int
nforall a. Ord a => a -> a -> Bool
<Int
10 = forall a. Show a => a -> [Char]
show Int
n
| Int
nforall a. Ord a => a -> a -> Bool
>=Int
10 = forall {t}. (Show t, Integral t) => t -> t -> [Char]
buck Int
n Int
1
| Bool
otherwise = forall a. HasCallStack => [Char] -> a
error [Char]
"Ord Int is not a total order!"
buck :: t -> t -> [Char]
buck t
n t
t | t
nforall a. Ord a => a -> a -> Bool
<t
10 = forall a. Show a => a -> [Char]
show (t
nforall a. Num a => a -> a -> a
*t
t) forall a. [a] -> [a] -> [a]
++ [Char]
"-" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ((t
nforall a. Num a => a -> a -> a
+t
1)forall a. Num a => a -> a -> a
*t
tforall a. Num a => a -> a -> a
-t
1)
| t
nforall a. Ord a => a -> a -> Bool
>=t
10 = t -> t -> [Char]
buck (t
n forall a. Integral a => a -> a -> a
`div` t
10) (t
tforall a. Num a => a -> a -> a
*t
10)
| Bool
otherwise = forall a. HasCallStack => [Char] -> a
error [Char]
"Ord Int is not a total order!"
divide :: Int -> Int -> [Int]
divide :: Int -> Int -> [Int]
divide Int
n Int
k =
[ Int
n forall a. Integral a => a -> a -> a
`div` Int
k forall a. Num a => a -> a -> a
+ if Int
iforall a. Ord a => a -> a -> Bool
<Int
n forall a. Integral a => a -> a -> a
`mod` Int
k then Int
1 else Int
0
| Int
i <- [Int
0..Int
kforall a. Num a => a -> a -> a
-Int
1] ]
showThread :: (ThreadId,Maybe ThreadLabel) -> String
showThread :: (ThreadId, Maybe [Char]) -> [Char]
showThread (ThreadId
tid,Maybe [Char]
lab) =
forall a. Show a => a -> [Char]
show ThreadId
tid forall a. [a] -> [a] -> [a]
++ (case Maybe [Char]
lab of Maybe [Char]
Nothing -> [Char]
""
Just [Char]
l -> [Char]
" ("forall a. [a] -> [a] -> [a]
++[Char]
lforall a. [a] -> [a] -> [a]
++[Char]
")")
cache :: IORef (Set ScheduleControl)
cache :: IORef (Set ScheduleControl)
cache = forall a. IO a -> a
unsafePerformIO IO (IORef (Set ScheduleControl))
cacheIO
cached :: ScheduleControl -> Bool
cached :: ScheduleControl -> Bool
cached = forall a. IO a -> a
unsafePerformIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScheduleControl -> IO Bool
cachedIO
cacheSize :: () -> Int
cacheSize :: () -> Int
cacheSize = forall a. IO a -> a
unsafePerformIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> IO Int
cacheSizeIO
cacheIO :: IO (IORef (Set ScheduleControl))
cacheIO :: IO (IORef (Set ScheduleControl))
cacheIO = forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$
if ExplorationOptions -> Int
explorationScheduleBound ExplorationOptions
opts forall a. Ord a => a -> a -> Bool
>=Int
0
then forall a. Set a
Set.empty
else forall a. HasCallStack => [Char] -> a
error [Char]
"exploreSimTrace: negative schedule bound"
cachedIO :: ScheduleControl -> IO Bool
cachedIO :: ScheduleControl -> IO Bool
cachedIO ScheduleControl
m = forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (Set ScheduleControl)
cache forall a b. (a -> b) -> a -> b
$ \Set ScheduleControl
set ->
(forall a. Ord a => a -> Set a -> Set a
Set.insert ScheduleControl
m Set ScheduleControl
set, forall a. Ord a => a -> Set a -> Bool
Set.member ScheduleControl
m Set ScheduleControl
set)
cacheSizeIO :: () -> IO Int
cacheSizeIO :: () -> IO Int
cacheSizeIO () = forall a. Set a -> Int
Set.size forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef IORef (Set ScheduleControl)
cache
replaySimTrace :: forall a test. (Testable test)
=> ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (SimTrace a -> test)
-> Property
replaySimTrace :: forall a test.
Testable test =>
ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (SimTrace a -> test)
-> Property
replaySimTrace ExplorationOptions
opts forall s. IOSim s a
mainAction ScheduleControl
control SimTrace a -> test
k =
let (() -> [ScheduleControl]
_,SimTrace a
trace) = forall a. SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces forall a b. (a -> b) -> a -> b
$
forall a.
Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
controlSimTrace (ExplorationOptions -> Maybe Int
explorationStepTimelimit ExplorationOptions
opts) ScheduleControl
control forall s. IOSim s a
mainAction
in forall prop. Testable prop => prop -> Property
property (SimTrace a -> test
k SimTrace a
trace)
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
mainAction =
forall a. (forall s. ST s a) -> a
runST (forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST Maybe Int
limit ScheduleControl
control forall s. IOSim s a
mainAction)
raceReversals :: ScheduleControl -> Int
raceReversals :: ScheduleControl -> Int
raceReversals ScheduleControl
ControlDefault = Int
0
raceReversals (ControlAwait [ScheduleMod]
mods) = forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleMod]
mods
raceReversals ControlFollow{} = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: raceReversals ControlFollow{}"
compareTraces :: Maybe (SimTrace a1)
-> SimTrace a2
-> (Maybe ((Time, ThreadId, Maybe ThreadLabel),
Set.Set (ThreadId, Maybe ThreadLabel)),
SimTrace a2)
compareTraces :: forall a1 a2.
Maybe (SimTrace a1)
-> SimTrace a2
-> (Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
SimTrace a2)
compareTraces Maybe (SimTrace a1)
Nothing SimTrace a2
trace = (forall a. Maybe a
Nothing, SimTrace a2
trace)
compareTraces (Just SimTrace a1
passing) SimTrace a2
trace = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper <- forall a. a -> IO (IORef a)
newIORef forall a. Maybe a
Nothing
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper,
forall {a} {a}.
IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace a -> SimTrace a
go IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper SimTrace a1
passing SimTrace a2
trace)
where go :: IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace a -> SimTrace a
go IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper (SimPORTrace Time
tpass ThreadId
tidpass Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
pass')
(SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail SimTrace a
fail')
| (Time
tpass,ThreadId
tidpass) forall a. Eq a => a -> a -> Bool
== (Time
tfail,ThreadId
tidfail) =
forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
forall a b. (a -> b) -> a -> b
$ IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace a -> SimTrace a
go IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper SimTrace a
pass' SimTrace a
fail'
go IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper (SimPORTrace Time
tpass ThreadId
tidpass Int
tsteppass Maybe [Char]
tlpass SimEventType
_ SimTrace a
_) SimTrace a
fail =
forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
forall a. IORef a -> a -> IO ()
writeIORef IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ((Time
tpass, ThreadId
tidpass, Maybe [Char]
tlpass),forall a. Set a
Set.empty)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tpass ThreadId
tidpass Int
tsteppass Maybe [Char]
tlpass SimEventType
EventThreadSleep
forall a b. (a -> b) -> a -> b
$ forall {a} {a}.
IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
-> ThreadId -> SimTrace a -> SimTrace a
wakeup IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper ThreadId
tidpass SimTrace a
fail
go IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
_ SimTrace {} SimTrace a
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraces: invariant violation"
go IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
_ SimTrace a
_ SimTrace {} = forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraces: invariant violation"
go IORef
(Maybe
((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
_ SimTrace a
_ SimTrace a
fail = SimTrace a
fail
wakeup :: IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
-> ThreadId -> SimTrace a -> SimTrace a
wakeup IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
sleeper ThreadId
tidpass
fail :: SimTrace a
fail@(SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail SimTrace a
fail')
| ThreadId
tidpass forall a. Eq a => a -> a -> Bool
== ThreadId
tidfail =
forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
EventThreadWake SimTrace a
fail
| Bool
otherwise = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
Just (a
slp,Set (ThreadId, Maybe [Char])
racing) <- forall a. IORef a -> IO a
readIORef IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
sleeper
forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
sleeper forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (a
slp,forall a. Ord a => a -> Set a -> Set a
Set.insert (ThreadId
tidfail,Maybe [Char]
tlfail) Set (ThreadId, Maybe [Char])
racing)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
forall a b. (a -> b) -> a -> b
$ IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
-> ThreadId -> SimTrace a -> SimTrace a
wakeup IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
sleeper ThreadId
tidpass SimTrace a
fail'
wakeup IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
_ ThreadId
_ SimTrace {} = forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraces: invariant violation"
wakeup IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
_ ThreadId
_ SimTrace a
fail = SimTrace a
fail