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

{-# OPTIONS_GHC -Wno-name-shadowing #-}
module Control.Monad.IOSim
  ( -- * Simulation monad
    IOSim
  , STMSim
    -- ** Run simulation
  , runSim
  , runSimOrThrow
  , runSimStrictShutdown
  , Failure (..)
  , runSimTrace
  , controlSimTrace
  , exploreSimTrace
  , ScheduleMod (..)
  , ScheduleControl (..)
  , runSimTraceST
  , liftST
  , traceM
  , traceSTM
    -- * Simulation time
  , setCurrentTime
  , unshareClock
    -- * Simulation trace
  , type SimTrace
  , Trace (Cons, Nil, Trace, SimTrace, SimPORTrace, TraceDeadlock, TraceLoop, TraceMainReturn, TraceMainException, TraceRacesFound)
  , SimResult (..)
  , SimEvent (..)
  , SimEventType (..)
  , ThreadLabel
  , Labelled (..)
    -- ** Pretty printers
  , ppTrace
  , ppTrace_
  , ppEvents
  , ppSimEvent
  , ppDebug
    -- ** Selectors
  , traceEvents
  , traceResult
    -- *** list selectors
  , selectTraceEvents
  , selectTraceEvents'
  , selectTraceEventsDynamic
  , selectTraceEventsDynamic'
  , selectTraceEventsSay
  , selectTraceEventsSay'
  , selectTraceRaces
    -- *** trace selectors
  , traceSelectTraceEvents
  , traceSelectTraceEventsDynamic
  , traceSelectTraceEventsSay
    -- ** IO printer
  , printTraceEventsSay
    -- * Exploration options
  , ExplorationSpec
  , ExplorationOptions (..)
  , stdExplorationOptions
  , withScheduleBound
  , withBranching
  , withStepTimelimit
  , withReplay
    -- * Eventlog
  , EventlogEvent (..)
  , EventlogMarker (..)
    -- * Low-level API
  , execReadTVar
    -- * Deprecated interfaces
  , SimM
  , SimSTM
  , TraceEvent
  ) where

import           Prelude

import           Data.Bifoldable
import           Data.Dynamic (fromDynamic)
import           Data.List (intercalate)
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.Class.MonadTime

import           Control.Monad.IOSim.Internal
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 :: (SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents SimEventType -> Maybe b
fn =
      (SimResult a -> [b] -> [b])
-> (b -> [b] -> [b]) -> [b] -> Trace (SimResult a) b -> [b]
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]
_       -> Failure -> [b]
forall a e. Exception e => e -> a
throw (SomeException -> Failure
FailureException SomeException
e)
                    Deadlock      Time
_   [Labelled ThreadId]
threads -> Failure -> [b]
forall a e. Exception e => e -> a
throw ([Labelled ThreadId] -> Failure
FailureDeadlock [Labelled ThreadId]
threads)
                    MainReturn    Time
_ a
_ [Labelled ThreadId]
_       -> []
                    SimResult a
Loop                      -> [Char] -> [b]
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: selectTraceEvents _ TraceLoop{}"
              )
              ( \ 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
. (SimEventType -> Maybe b) -> SimTrace a -> Trace (SimResult a) b
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' :: (SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' SimEventType -> Maybe b
fn =
      (SimResult a -> [b] -> [b])
-> (b -> [b] -> [b]) -> [b] -> Trace (SimResult a) b -> [b]
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
. (SimEventType -> Maybe b) -> SimTrace a -> Trace (SimResult a) b
forall b a.
(SimEventType -> Maybe b) -> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents SimEventType -> Maybe b
fn

selectTraceRaces :: SimTrace a -> [ScheduleControl]
selectTraceRaces :: SimTrace a -> [ScheduleControl]
selectTraceRaces = SimTrace a -> [ScheduleControl]
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 [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.

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

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

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

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

-- | Like 'selectTraceEventsSay' but return partial trace if an exception is
-- found in it.
--
selectTraceEventsSay' :: SimTrace a -> [String]
selectTraceEventsSay' :: SimTrace a -> [[Char]]
selectTraceEventsSay' = (SimEventType -> Maybe [Char]) -> SimTrace a -> [[Char]]
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) = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    fn SimEventType
_            = Maybe [Char]
forall a. Maybe a
Nothing

-- | Print all 'EventSay' to the console.
--
-- For convenience, this throws exceptions for abnormal sim termination.
--
printTraceEventsSay :: SimTrace a -> IO ()
printTraceEventsSay :: 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
    :: (SimEventType -> Maybe b)
    -> SimTrace a
    -> Trace (SimResult a) b
traceSelectTraceEvents :: (SimEventType -> Maybe b) -> SimTrace a -> Trace (SimResult a) b
traceSelectTraceEvents 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
-> SimTrace a
-> Trace (SimResult a) b
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 SimEventType -> Maybe b
fn (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 SimEventType -> Maybe b
fn (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 :: SimTrace a -> Trace (SimResult a) b
traceSelectTraceEventsDynamic = (SimEventType -> Maybe b) -> SimTrace a -> Trace (SimResult a) b
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) = Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn 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 :: SimTrace a -> Trace (SimResult a) [Char]
traceSelectTraceEventsSay = (SimEventType -> Maybe [Char])
-> SimTrace a -> Trace (SimResult a) [Char]
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) = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    fn SimEventType
_            = Maybe [Char]
forall a. Maybe a
Nothing

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

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

       -- | The main thread terminated normally but other threads were still
       -- alive, and strict shutdown checking was requested.
       -- See 'runSimStrictShutdown'
     | FailureSloppyShutdown [Labelled ThreadId]
  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
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) = SomeException -> [Char]
forall e. Exception e => e -> [Char]
displayException  SomeException
err
    displayException (FailureDeadlock [Labelled ThreadId]
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 ThreadId -> [Char]
forall a. Show a => a -> [Char]
show (Labelled ThreadId -> [Char]) -> [Labelled ThreadId] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
`map` [Labelled ThreadId]
threads)
             , [Char]
">>"
             ]
    displayException (FailureSloppyShutdown [Labelled ThreadId]
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 ThreadId -> [Char]
forall a. Show a => a -> [Char]
show (Labelled ThreadId -> [Char]) -> [Labelled ThreadId] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
`map` [Labelled ThreadId]
threads)
             , [Char]
">>"
             ]

-- | 'IOSim' is a pure monad.
--
runSim :: forall a. (forall s. IOSim s a) -> Either Failure a
runSim :: (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 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 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 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 also fail if when the main thread terminates, there
-- are other threads still running or blocked. If one is trying to follow
-- a strict thread cleanup policy then this helps testing for that.
--
runSimStrictShutdown :: forall a. (forall s. IOSim s a) -> Either Failure a
runSimStrictShutdown :: (forall 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 forall s. IOSim s a
mainAction)

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

traceEvents :: SimTrace a -> [(Time, ThreadId, Maybe ThreadLabel, SimEventType)]
traceEvents :: 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)
                                                  (Time, ThreadId, Maybe [Char], SimEventType)
-> [(Time, ThreadId, Maybe [Char], SimEventType)]
-> [(Time, ThreadId, Maybe [Char], SimEventType)]
forall a. a -> [a] -> [a]
: SimTrace a -> [(Time, ThreadId, Maybe [Char], SimEventType)]
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)
                                                  (Time, ThreadId, Maybe [Char], SimEventType)
-> [(Time, ThreadId, Maybe [Char], SimEventType)]
-> [(Time, ThreadId, Maybe [Char], SimEventType)]
forall a. a -> [a] -> [a]
: SimTrace a -> [(Time, ThreadId, Maybe [Char], SimEventType)]
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 =
    [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 -> ThreadId -> Maybe [Char] -> SimEventType -> SimEvent
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 = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ [Char] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Time -> [Char]
forall a. Show a => a -> [Char]
show Time
t)
                | (Time
t, ThreadId
_, Maybe [Char]
_, SimEventType
_) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
                ]
    tidWidth :: Int
tidWidth  = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ [Char] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (ThreadId -> [Char]
forall a. Show a => a -> [Char]
show ThreadId
tid)
                | (Time
_, ThreadId
tid, Maybe [Char]
_, SimEventType
_) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
                ]
    width :: Int
width     = [Int] -> Int
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 (t :: * -> *) a. Foldable t => t a -> Int
length Maybe [Char]
threadLabel
                | (Time
_, ThreadId
_, Maybe [Char]
threadLabel, SimEventType
_) <- [(Time, ThreadId, Maybe [Char], SimEventType)]
events
                ]


-- | See 'runSimTraceST' below.
--
runSimTrace :: forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace :: (forall 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)

controlSimTrace :: forall a.
                   Maybe Int
                -> ScheduleControl
                -- ^ note: must be either `ControlDefault` or `ControlAwait`.
                -> (forall s. IOSim s a)
                -> SimTrace a
controlSimTrace :: Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
controlSimTrace Maybe Int
limit ScheduleControl
control forall s. IOSim s a
mainAction =
    (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
mainAction)

exploreSimTrace
  :: forall a test. Testable test
  => (ExplorationOptions -> ExplorationOptions)
  -> (forall s. IOSim s a)
  -> (Maybe (SimTrace a) -> SimTrace a -> test)
  -> Property
exploreSimTrace :: (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 Maybe (SimTrace a)
forall a. Maybe a
Nothing Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&.
      let size :: Int
size = () -> Int
cacheSize() in Int
size Int -> Property -> Property
`seq`
      [Char] -> [[Char]] -> Bool -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Modified schedules explored" [Int -> [Char]
forall t. (Show t, Integral t) => t -> [Char]
bucket Int
size] Bool
True
    Just ScheduleControl
control ->
      ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (Maybe (SimTrace a) -> SimTrace a -> test)
-> Property
forall a test.
Testable test =>
ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (Maybe (SimTrace a) -> SimTrace a -> test)
-> Property
replaySimTrace ExplorationOptions
opts forall s. IOSim s a
mainAction ScheduleControl
control Maybe (SimTrace a) -> SimTrace a -> test
k
  where
    opts :: ExplorationOptions
opts = ExplorationOptions -> ExplorationOptions
optsf ExplorationOptions
stdExplorationOptions

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

      -- ALERT!!! Impure code: readRaces must be called *after* we have
      -- finished with trace.
      let (() -> [ScheduleControl]
readRaces,SimTrace a
trace0) = SimTrace a -> (() -> [ScheduleControl], SimTrace a)
forall a. SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces (SimTrace a -> (() -> [ScheduleControl], SimTrace a))
-> SimTrace a -> (() -> [ScheduleControl], SimTrace a)
forall a b. (a -> b) -> a -> b
$
                                 Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
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) = Maybe (SimTrace a)
-> SimTrace a
-> (Maybe
      ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
    SimTrace a)
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 ([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, 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) [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 (((ThreadId, Maybe [Char]) -> [Char])
-> [(ThreadId, Maybe [Char])] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"    "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++)ShowS
-> ((ThreadId, Maybe [Char]) -> [Char])
-> (ThreadId, Maybe [Char])
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(ThreadId, Maybe [Char]) -> [Char]
showThread) ([(ThreadId, Maybe [Char])] -> [[Char]])
-> [(ThreadId, Maybe [Char])] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set (ThreadId, Maybe [Char]) -> [(ThreadId, Maybe [Char])]
forall a. Set a -> [a]
Set.toList Set (ThreadId, Maybe [Char])
racing)
                                            ) (test -> Property) -> test -> Property
forall a b. (a -> b) -> a -> b
$
          Maybe (SimTrace a) -> SimTrace a -> test
k Maybe (SimTrace a)
passingTrace SimTrace a
trace) Property -> Property -> Property
forall prop. TestableNoCatch prop => prop -> prop -> Property
.&&|
         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.
             races :: [ScheduleControl]
races     = (ScheduleControl -> Bool) -> [ScheduleControl] -> [ScheduleControl]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (ScheduleControl -> Bool) -> ScheduleControl -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScheduleControl -> Bool
forall a. Ord a => a -> Bool
cached) ([ScheduleControl] -> [ScheduleControl])
-> ([ScheduleControl] -> [ScheduleControl])
-> [ScheduleControl]
-> [ScheduleControl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [ScheduleControl] -> [ScheduleControl]
forall a. Int -> [a] -> [a]
take Int
limit ([ScheduleControl] -> [ScheduleControl])
-> [ScheduleControl] -> [ScheduleControl]
forall a b. (a -> b) -> a -> b
$ () -> [ScheduleControl]
readRaces()
             branching :: Int
branching = [ScheduleControl] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleControl]
races
         in -- tabulate "Races explored" (map show races) $
            [Char] -> [[Char]] -> Property -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Branching factor" [Int -> [Char]
forall t. (Show t, Integral t) => t -> [Char]
bucket Int
branching] (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            [Char] -> [[Char]] -> Property -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Race reversals per schedule" [Int -> [Char]
forall t. (Show t, Integral t) => t -> [Char]
bucket (ScheduleControl -> Int
raceReversals ScheduleControl
control)] (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            [Property] -> Property
forall prop. TestableNoCatch prop => [prop] -> Property
conjoinPar
              [ --Debug.trace "New schedule:" $
                --Debug.trace ("  "++show r) $
                --counterexample ("Schedule control: " ++ show r) $
                Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore Int
n' ((Int
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]
forall a. Integral a => a -> a -> [a]
divide (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
branching) Int
branching) ]

    bucket :: t -> [Char]
bucket t
n | t
nt -> t -> Bool
forall a. Ord a => a -> a -> Bool
<t
10  = t -> [Char]
forall a. Show a => a -> [Char]
show t
n
             | t
nt -> t -> Bool
forall a. Ord a => a -> a -> Bool
>=t
10 = t -> t -> [Char]
forall t. (Show t, Integral t) => t -> t -> [Char]
buck t
n t
1
             | Bool
otherwise = ShowS
forall a. HasCallStack => [Char] -> a
error [Char]
"Ord Int is not a total order!"  -- GHC made me do it!
    buck :: t -> t -> [Char]
buck t
n t
t | t
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)
             | t
nt -> t -> Bool
forall a. Ord a => a -> a -> Bool
>=t
10     = 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)
             | Bool
otherwise = ShowS
forall a. HasCallStack => [Char] -> a
error [Char]
"Ord Int is not a total order!"  -- GHC made me do it!

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

    showThread :: (ThreadId,Maybe ThreadLabel) -> String
    showThread :: (ThreadId, Maybe [Char]) -> [Char]
showThread (ThreadId
tid,Maybe [Char]
lab) =
      ThreadId -> [Char]
forall a. Show a => a -> [Char]
show ThreadId
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]
")")

    -- It is possible for the same control to be generated several times.
    -- To avoid exploring them twice, we keep a cache of explored schedules.
    cache :: IORef (Set a)
cache = IO (IORef (Set a)) -> IORef (Set a)
forall a. IO a -> a
unsafePerformIO (IO (IORef (Set a)) -> IORef (Set a))
-> IO (IORef (Set a)) -> IORef (Set a)
forall a b. (a -> b) -> a -> b
$ Set a -> IO (IORef (Set a))
forall a. a -> IO (IORef a)
newIORef (Set a -> IO (IORef (Set a))) -> Set a -> IO (IORef (Set a))
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
optsInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>=Int
0
                then Set a
forall a. Set a
Set.empty
                else [Char] -> Set a
forall a. HasCallStack => [Char] -> a
error [Char]
"exploreSimTrace: negative schedule bound"
    cached :: a -> Bool
cached a
m = IO Bool -> Bool
forall a. IO a -> a
unsafePerformIO (IO Bool -> Bool) -> IO Bool -> Bool
forall a b. (a -> b) -> a -> b
$ IORef (Set a) -> (Set a -> (Set a, Bool)) -> IO Bool
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (Set a)
forall a. IORef (Set a)
cache ((Set a -> (Set a, Bool)) -> IO Bool)
-> (Set a -> (Set a, Bool)) -> IO Bool
forall a b. (a -> b) -> a -> b
$ \Set a
set ->
      (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
m Set a
set, a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
m Set a
set)
    cacheSize :: () -> Int
cacheSize () = IO Int -> Int
forall a. IO a -> a
unsafePerformIO (IO Int -> Int) -> IO Int -> Int
forall a b. (a -> b) -> a -> b
$ Set Any -> Int
forall a. Set a -> Int
Set.size (Set Any -> Int) -> IO (Set Any) -> IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Set Any) -> IO (Set Any)
forall a. IORef a -> IO a
readIORef IORef (Set Any)
forall a. IORef (Set a)
cache

replaySimTrace :: forall a test. (Testable test)
               => ExplorationOptions
               -> (forall s. IOSim s a)
               -> ScheduleControl
               -> (Maybe (SimTrace a) -> SimTrace a -> test)
               -> Property
replaySimTrace :: ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (Maybe (SimTrace a) -> SimTrace a -> test)
-> Property
replaySimTrace ExplorationOptions
opts forall s. IOSim s a
mainAction ScheduleControl
control Maybe (SimTrace a) -> SimTrace a -> test
k =
  let (() -> [ScheduleControl]
_,SimTrace a
trace) = SimTrace a -> (() -> [ScheduleControl], SimTrace a)
forall a. SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces (SimTrace a -> (() -> [ScheduleControl], SimTrace a))
-> SimTrace a -> (() -> [ScheduleControl], SimTrace a)
forall a b. (a -> b) -> a -> b
$
                            Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
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 test -> Property
forall prop. Testable prop => prop -> Property
property (Maybe (SimTrace a) -> SimTrace a -> test
k Maybe (SimTrace a)
forall a. Maybe a
Nothing SimTrace a
trace)

raceReversals :: ScheduleControl -> Int
raceReversals :: ScheduleControl -> Int
raceReversals ScheduleControl
ControlDefault      = Int
0
raceReversals (ControlAwait [ScheduleMod]
mods) = [ScheduleMod] -> 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{}"

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

compareTraces :: Maybe (SimTrace a1)
              -> SimTrace a2
              -> (Maybe ((Time, ThreadId, Maybe ThreadLabel),
                         Set.Set (ThreadId, Maybe ThreadLabel)),
                  SimTrace a2)
compareTraces :: Maybe (SimTrace a1)
-> SimTrace a2
-> (Maybe
      ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
    SimTrace a2)
compareTraces Maybe (SimTrace a1)
Nothing SimTrace a2
trace = (Maybe
  ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
forall a. Maybe a
Nothing, SimTrace a2
trace)
compareTraces (Just SimTrace a1
passing) SimTrace a2
trace = IO
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
   SimTrace a2)
-> (Maybe
      ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
    SimTrace a2)
forall a. IO a -> a
unsafePerformIO (IO
   (Maybe
      ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
    SimTrace a2)
 -> (Maybe
       ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
     SimTrace a2))
-> IO
     (Maybe
        ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
      SimTrace a2)
-> (Maybe
      ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
    SimTrace a2)
forall a b. (a -> b) -> a -> b
$ do
  IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper <- Maybe
  ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
-> IO
     (IORef
        (Maybe
           ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))))
forall a. a -> IO (IORef a)
newIORef Maybe
  ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
forall a. Maybe a
Nothing
  (Maybe
   ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
 SimTrace a2)
-> IO
     (Maybe
        ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])),
      SimTrace a2)
forall (m :: * -> *) a. Monad m => a -> m a
return (IO
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
forall a. IO a -> a
unsafePerformIO (IO
   (Maybe
      ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
 -> Maybe
      ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> IO
     (Maybe
        ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
forall a b. (a -> b) -> a -> b
$ IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> IO
     (Maybe
        ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
forall a. IORef a -> IO a
readIORef IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper,
          IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> SimTrace a1 -> SimTrace a2 -> SimTrace a2
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) (Time, ThreadId) -> (Time, ThreadId) -> Bool
forall a. Eq a => a -> a -> Bool
== (Time
tfail,ThreadId
tidfail) =
              Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
                (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
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 =
          IO (SimTrace a) -> SimTrace a
forall a. IO a -> a
unsafePerformIO (IO (SimTrace a) -> SimTrace a) -> IO (SimTrace a) -> SimTrace a
forall a b. (a -> b) -> a -> b
$ do
            IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
-> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
sleeper (Maybe
   ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
 -> IO ())
-> Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
-> IO ()
forall a b. (a -> b) -> a -> b
$ ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
-> Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char]))
forall a. a -> Maybe a
Just ((Time
tpass, ThreadId
tidpass, Maybe [Char]
tlpass),Set (ThreadId, Maybe [Char])
forall a. Set a
Set.empty)
            SimTrace a -> IO (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> IO (SimTrace a)) -> SimTrace a -> IO (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tpass ThreadId
tidpass Int
tsteppass Maybe [Char]
tlpass SimEventType
EventThreadSleep
                   (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ IORef
  (Maybe
     ((Time, ThreadId, Maybe [Char]), Set (ThreadId, Maybe [Char])))
-> ThreadId -> SimTrace a -> SimTrace a
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
_ = [Char] -> 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 {} = [Char] -> 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 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 ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tidfail =
              Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
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 = IO (SimTrace a) -> SimTrace a
forall a. IO a -> a
unsafePerformIO (IO (SimTrace a) -> SimTrace a) -> IO (SimTrace a) -> SimTrace a
forall a b. (a -> b) -> a -> b
$ do
              Just (a
slp,Set (ThreadId, Maybe [Char])
racing) <- IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
-> IO (Maybe (a, Set (ThreadId, Maybe [Char])))
forall a. IORef a -> IO a
readIORef IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
sleeper
              IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
-> Maybe (a, Set (ThreadId, Maybe [Char])) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe (a, Set (ThreadId, Maybe [Char])))
sleeper (Maybe (a, Set (ThreadId, Maybe [Char])) -> IO ())
-> Maybe (a, Set (ThreadId, Maybe [Char])) -> IO ()
forall a b. (a -> b) -> a -> b
$ (a, Set (ThreadId, Maybe [Char]))
-> Maybe (a, Set (ThreadId, Maybe [Char]))
forall a. a -> Maybe a
Just (a
slp,(ThreadId, Maybe [Char])
-> Set (ThreadId, Maybe [Char]) -> Set (ThreadId, Maybe [Char])
forall a. Ord a => a -> Set a -> Set a
Set.insert (ThreadId
tidfail,Maybe [Char]
tlfail) Set (ThreadId, Maybe [Char])
racing)
              SimTrace a -> IO (SimTrace a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> IO (SimTrace a)) -> SimTrace a -> IO (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> ThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail ThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
                     (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
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 {} = [Char] -> SimTrace a
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