diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,47 @@ # Revsion history of io-sim +## next release + +### Breaking changes + +### Non-breaking changes + +## 1.3.0.0 + +### Breaking changes + +* `MainReturn`, `MainException` and the pattern synonyms `TraceMainReturn`, + `TraceMainException` changed their signature. They will now also show the main thread id. +* Renamed `ThreadId` to `IOSimThreadId` to avoid a clash with `ThreadId` + associated type family of `MonadFork`. It makes it much simpler to paste + failing `ScheduleControl` in `ghci` or tests. +* `BlockedReason` was modified: `BlockedOnOther` was removed, in favour of `BlockedOnDelay` and `BlockOnThrowTo`. +* The `Failure` type (for example returned by `runSim`) now also contains + a constructor for internal failures. This improved error reporting when + there's a bug in `IOSimPOR`. Currently it's only used by some of the + assertions in `IOSimPOR`. + +#### Non-breaking changes + +* Refactored the internal API to avoid `unsafePerformIO`. +* Fixed bugs which lead to discovery of schedules which are impossible to run. +* Added haddocks, refactored the code base to improve readability. +* Fixed reported `step` in `EventTxWakup` +* Added debugging information schedule, (`explorationDebugLevel` option). + Mostly useful for debugging `IOSimPOR` itself. This information will + contains `Effect`, discovered races and schedules. +* Addded or improved pretty printers for `SimTrace`. Among other changes, + a racy `StepId`: `(RacyThreadId [1,2], 2)`, is now pretty printed as `Thread + {1,2}.2`, a non racy step is printed as `Thread [1,2].2`. +* Fixed trace of calls to the `deschedule` function. +* Exposed `Timeout` type as part of the `newTimeout` API. +* When `explorationDebugLevel` is set, avoid printing the same trace twice. +* Reimplemented `labelTVarIO` and `traceTVarIO` in `ST` monad, which simplifies + trace of these calls. +* Fixed `traceTVar` for `TVar`'s created with `registerDelay`. +* Added pretty printer for `SimResult`, and other pretty printer improvements. +* Support `ghc-9.8`. + ## 1.2.0.0 ### Breaking changes @@ -11,20 +53,20 @@ - `selectTraceEventsSayWithTime` - `selectTraceEventsSayWithTime'` -### Non breaking changes +### Non-breaking changes * Provide `MonadInspectMVar` instance for `IOSim`. - Added NFData & NoThunks instances for `ThreadId` ## 1.1.0.0 -### Non breaking changes +### Non-breaking changes * `io-classes-1.1.0.0` ## 1.0.0.1 -### Non breaking changes +### Non-breaking changes * Support `ghc-9.6`. @@ -41,7 +83,7 @@ * Added `TimeoutId` to `EventThreadDelay` and `EventThreadFired` events. -### Non breaking changes +### Non-breaking changes * Fixed `threadDelay` in presence of asynchronous exceptions (in `IOSim` and `IOSimPOR`) (#80). * Fixed bug in `IOSim` & `IOSimPOR` which resulted in reusing existing diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -15,6 +15,7 @@ * inspection of `STM` mutable data structures; * deadlock detection; * `MonadFix` instances for both `IOSim` and its corresponding `STM` monad. + * partial order reduction (see [IOSimPOR]). `io-sim` together with [`io-classes`] is a drop-in replacement for the `IO` monad (with some ramifications). It was designed to write easily testable @@ -42,3 +43,4 @@ [`io-classes`]: https://hackage.haskell.org/package/io-classes [`si-timers`]: https://hackage.haskell.org/package/si-timers +[IOSimPOR]: https://github.com/input-output-hk/io-sim/tree/main/io-sim/how-to-use-IOSimPOR.md diff --git a/io-sim.cabal b/io-sim.cabal --- a/io-sim.cabal +++ b/io-sim.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: io-sim -version: 1.2.0.0 +version: 1.3.0.0 synopsis: A pure simulator for monadic concurrency with STM. description: A pure simulator monad with support of concurency (base, async), stm, @@ -15,7 +15,7 @@ build-type: Simple extra-doc-files: CHANGELOG.md README.md bug-reports: https://github.com/input-output-hk/io-sim/issues -tested-with: GHC == { 8.10, 9.2, 9.4, 9.6 } +tested-with: GHC == { 8.10, 9.2, 9.4, 9.6, 9.8 } flag asserts description: Enable assertions @@ -74,16 +74,15 @@ RankNTypes, ScopedTypeVariables, TypeFamilies - build-depends: base >=4.9 && <4.19, - io-classes ^>=1.2, + build-depends: base >=4.9 && <4.20, + io-classes ^>=1.3, exceptions >=0.10, containers, deepseq, nothunks, - parallel, psqueues >=0.2 && <0.3, - strict-stm ^>=1.2, - si-timers ^>=1.2, + strict-stm ^>=1.3, + si-timers ^>=1.3, time >=1.9.1 && <1.13, quiet, QuickCheck, @@ -108,7 +107,6 @@ containers, io-classes, io-sim, - parallel, QuickCheck, si-timers, strict-stm, @@ -117,6 +115,9 @@ tasty-hunit, time ghc-options: -fno-ignore-asserts + -rtsopts + if impl(ghc >= 9.8) + ghc-options: -Wno-x-partial benchmark bench import: warnings diff --git a/src/Control/Monad/IOSim.hs b/src/Control/Monad/IOSim.hs --- a/src/Control/Monad/IOSim.hs +++ b/src/Control/Monad/IOSim.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RankNTypes #-} @@ -5,6 +7,8 @@ {-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + module Control.Monad.IOSim ( -- * Simulation monad IOSim @@ -19,7 +23,9 @@ -- ** Explore races using /IOSimPOR/ -- $iosimpor , exploreSimTrace + , exploreSimTraceST , controlSimTrace + , controlSimTraceST , ScheduleMod (..) , ScheduleControl (..) -- *** Exploration options @@ -37,11 +43,21 @@ , unshareClock -- * Simulation trace , type SimTrace - , Trace (Cons, Nil, SimTrace, SimPORTrace, TraceDeadlock, TraceLoop, TraceMainReturn, TraceMainException, TraceRacesFound) + , Trace (Cons, + Nil, + SimTrace, + SimPORTrace, + TraceDeadlock, + TraceLoop, + TraceMainReturn, + TraceMainException, + TraceRacesFound, + TraceInternalError) , SimResult (..) , SimEvent (..) , SimEventType (..) , ThreadLabel + , IOSimThreadId (..) , Labelled (..) -- ** Dynamic Tracing , traceM @@ -77,6 +93,7 @@ , EventlogEvent (..) , EventlogMarker (..) -- * Low-level API + , Timeout , newTimeout , readTimeout , cancelTimeout @@ -86,30 +103,34 @@ 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 Control.Monad.IOSimPOR.Internal (controlSimTraceST) +import qualified Control.Monad.IOSimPOR.Internal as IOSimPOR (controlSimTraceST) import Control.Monad.IOSimPOR.QuickCheckUtils import Test.QuickCheck - -import Data.IORef import System.IO.Unsafe +import qualified Debug.Trace as Debug selectTraceEvents @@ -119,10 +140,11 @@ selectTraceEvents fn = bifoldr ( \ v _ -> case v of - MainException _ e _ -> throw (FailureException e) + MainException _ _ e _ -> throw (FailureException e) Deadlock _ threads -> throw (FailureDeadlock threads) - MainReturn _ _ _ -> [] + MainReturn _ _ _ _ -> [] Loop -> error "Impossible: selectTraceEvents _ TraceLoop{}" + InternalError msg -> throw (FailureInternal msg) ) ( \ b acc -> b : acc ) [] @@ -161,19 +183,39 @@ -- unsafe, of course, since that function may return different results -- at different times. -detachTraceRaces :: SimTrace a -> (() -> [ScheduleControl], SimTrace a) -detachTraceRaces trace = unsafePerformIO $ do - races <- newIORef [] - let readRaces () = concat . reverse . unsafePerformIO $ readIORef races - saveRaces r t = unsafePerformIO $ do - modifyIORef races (r:) - return t - let go (SimTrace a b c d trace) = SimTrace a b c d $ go trace - go (SimPORTrace a b c d e trace) = SimPORTrace a b c d e $ go trace - go (TraceRacesFound r trace) = saveRaces r $ go trace - go t = t - return (readRaces, go trace) +-- | Detach discovered races. This is written in `ST` monad to support +-- simulations which do not terminate, in which case we will only detach races +-- up to the point we evaluated the simulation. +-- +detachTraceRacesST :: forall a s. SimTrace a -> ST s (ST s [ScheduleControl], SimTrace a) +detachTraceRacesST trace0 = do + races <- newSTRef [] + let readRaces :: ST s [ScheduleControl] + readRaces = concat . reverse <$> readSTRef races + saveRaces :: [ScheduleControl] -> ST s () + saveRaces rs = modifySTRef races (rs:) + + go :: SimTrace a -> ST s (SimTrace a) + go (SimTrace a b c d trace) = SimTrace a b c d <$> go trace + go (SimPORTrace _ _ _ _ EventRaces {} trace) + = go trace + go (SimPORTrace a b c d e trace) = SimPORTrace a b c d e <$> go trace + go (TraceRacesFound rs trace) = saveRaces rs >> go trace + go t = return t + + trace <- go trace0 + return (readRaces, trace) + + +-- | Like `detachTraceRacesST`, but it doesn't expose discovered races. +-- +detachTraceRaces :: forall a. SimTrace a -> SimTrace a +detachTraceRaces = Trace.filter (\a -> case a of + SimPOREvent { seType = EventRaces {} } -> False + SimRacesFound {} -> False + _ -> True) + -- | Select all the traced values matching the expected type. This relies on -- the sim's dynamic trace facility. -- @@ -309,17 +351,23 @@ FailureException SomeException -- | The threads all deadlocked. - | FailureDeadlock ![Labelled ThreadId] + | FailureDeadlock ![Labelled IOSimThreadId] -- | The main thread terminated normally but other threads were still -- alive, and strict shutdown checking was requested. -- See 'runSimStrictShutdown'. - | FailureSloppyShutdown [Labelled ThreadId] + | FailureSloppyShutdown [Labelled IOSimThreadId] -- | An exception was thrown while evaluation the trace. -- This could be an internal assertion failure of `io-sim` or an -- unhandled exception in the simulation. | FailureEvaluation SomeException + + -- | An internal failure of the simulator. + -- + -- Please open an issue at + -- . + | FailureInternal String deriving Show instance Exception Failure where @@ -334,7 +382,18 @@ , intercalate ", " (show `map` threads) , ">>" ] - displayException (FailureEvaluation err) = "evaluation error:" ++ displayException err + displayException (FailureEvaluation err) = + concat [ "<>" + ] + displayException (FailureInternal msg) = + concat [ "<>\n" + , "please report the issue at\n" + , "https://github.com/input-output-hk/io-sim/issues" + ] -- | 'IOSim' is a pure monad. @@ -353,7 +412,7 @@ -- | Like 'runSim' but fail when the main thread terminates if there are other -- threads still running or blocked. If one is trying to follow a strict thread --- cleanup policy then this helps testing for that. +-- clean-up policy then this helps testing for that. -- runSimStrictShutdown :: forall a. (forall s. IOSim s a) -> Either Failure a runSimStrictShutdown mainAction = traceResult True (runSimTrace mainAction) @@ -380,16 +439,17 @@ go (SimTrace _ _ _ _ t) = eval t go (SimPORTrace _ _ _ _ _ t) = eval t go (TraceRacesFound _ t) = eval t - go (TraceMainReturn _ _ tids@(_:_)) + go (TraceMainReturn _ _ _ tids@(_:_)) | strict = pure $ Left (FailureSloppyShutdown tids) - go (TraceMainReturn _ x _) = pure $ Right x - go (TraceMainException _ e _) = pure $ Left (FailureException e) + go (TraceMainReturn _ _ x _) = pure $ Right x + go (TraceMainException _ _ e _) = pure $ Left (FailureException e) go (TraceDeadlock _ threads) = pure $ Left (FailureDeadlock threads) go TraceLoop{} = error "Impossible: traceResult TraceLoop{}" + go (TraceInternalError msg) = pure $ Left (FailureInternal msg) -- | Turn 'SimTrace' into a list of timestamped events. -- -traceEvents :: SimTrace a -> [(Time, ThreadId, Maybe ThreadLabel, SimEventType)] +traceEvents :: SimTrace a -> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)] traceEvents (SimTrace time tid tlbl event t) = (time, tid, tlbl, event) : traceEvents t traceEvents (SimPORTrace time tid _ tlbl event t) = (time, tid, tlbl, event) @@ -399,7 +459,7 @@ -- | Pretty print a timestamped event. -- -ppEvents :: [(Time, ThreadId, Maybe ThreadLabel, SimEventType)] +ppEvents :: [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)] -> String ppEvents events = intercalate "\n" @@ -442,8 +502,8 @@ -- slot. In /IOSim/ and /IOSimPOR/ time only moves explicitly through timer -- events, e.g. things like `Control.Monad.Class.MonadTimer.SI.threadDelay`, -- `Control.Monad.Class.MonadTimer.SI.registerDelay` or the --- `Control.Monad.Class.MonadTimer.NonStandard.MonadTimeout` api. The usual --- quickcheck techniques can help explore different schedules of +-- `Control.Monad.Class.MonadTimer.NonStandard.MonadTimeout` API. The usual +-- QuickCheck techniques can help explore different schedules of -- threads too. -- | Execute a simulation, discover & revert races. Note that this will execute @@ -454,6 +514,8 @@ -- On property failure it will show the failing schedule (`ScheduleControl`) -- which can be plugged to `controlSimTrace`. -- +-- Note: `exploreSimTrace` evaluates each schedule in parallel (using `par`). +-- exploreSimTrace :: forall a test. Testable test => (ExplorationOptions -> ExplorationOptions) @@ -464,128 +526,133 @@ -- ^ a callback which receives the previous trace (e.g. before reverting -- a race condition) and current trace -> Property -exploreSimTrace optsf mainAction k = - case explorationReplay opts of - Nothing -> - explore (explorationScheduleBound opts) (explorationBranching opts) ControlDefault Nothing .&&. - let size = cacheSize() in size `seq` - tabulate "Modified schedules explored" [bucket size] True - Just control -> - replaySimTrace opts mainAction control (k Nothing) +exploreSimTrace optsf main k = + runST (exploreSimTraceST optsf main (\a b -> pure (k a b))) + + +-- | An 'ST' version of 'exploreSimTrace'. The callback also receives +-- 'ScheduleControl'. This is mostly useful for testing /IOSimPOR/ itself. +-- +-- Note: `exploreSimTraceST` evaluates each schedule sequentially. +-- +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 optsf main k = + case explorationReplay opts of + Just control -> do + trace <- controlSimTraceST (explorationStepTimelimit opts) control main + counterexample ("Schedule control: " ++ show control) + <$> k Nothing trace + Nothing -> do + cacheRef <- createCacheST + prop <- go cacheRef (explorationScheduleBound opts) + (explorationBranching opts) + ControlDefault Nothing + !size <- cacheSizeST cacheRef + return $ tabulate "Modified schedules explored" [bucket size] prop where opts = optsf stdExplorationOptions - explore :: Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property - explore n m control passingTrace = - - -- ALERT!!! Impure code: readRaces must be called *after* we have - -- finished with trace. - let (readRaces, trace0) = detachTraceRaces $ - controlSimTrace - (explorationStepTimelimit opts) control mainAction - (sleeper,trace) = compareTraces passingTrace trace0 - in ( counterexample ("Schedule control: " ++ show control) - $ counterexample - (case sleeper of - Nothing -> "No thread delayed" - Just ((t,tid,lab),racing) -> - showThread (tid,lab) ++ - " delayed at time "++ - show t ++ - "\n until after:\n" ++ - unlines (map ((" "++).showThread) $ Set.toList racing) - ) - $ k passingTrace trace - ) - .&&| let limit = (n+m-1) `div` m - -- To ensure the set of schedules explored is deterministic, we - -- filter out cached ones *after* selecting the children of this - -- node. - races = filter (not . cached) . take limit $ readRaces () - branching = length races - in -- tabulate "Races explored" (map show races) $ - tabulate "Branching factor" [bucket branching] $ - tabulate "Race reversals per schedule" [bucket (raceReversals control)] $ - conjoinPar - [ --Debug.trace "New schedule:" $ - --Debug.trace (" "++show r) $ - --counterexample ("Schedule control: " ++ show r) $ - explore n' ((m-1) `max` 1) r (Just trace0) - | (r,n') <- zip races (divide (n-branching) branching) ] + go :: STRef s (Set ScheduleControl) + -> Int -- schedule bound + -> Int -- branching factor + -> ScheduleControl + -> Maybe (SimTrace a) + -> ST s Property + go cacheRef n m control passingTrace = do + traceWithRaces <- IOSimPOR.controlSimTraceST (explorationStepTimelimit opts) control main + (readRaces, trace0) <- detachTraceRacesST traceWithRaces + (readSleeperST, trace) <- compareTracesST passingTrace trace0 + () <- traceDebugLog (explorationDebugLevel opts) traceWithRaces + conjoinNoCatchST + [ do sleeper <- readSleeperST + prop <- k passingTrace trace + return $ counterexample ("Schedule control: " ++ show control) + $ counterexample + (case sleeper of + Nothing -> "No thread delayed" + Just ((t,tid,lab),racing) -> + showThread (tid,lab) ++ + " delayed at time "++ + show t ++ + "\n until after:\n" ++ + unlines (map ((" "++).showThread) $ Set.toList racing) + ) + prop + , do let limit = (n+m-1) `div` m + -- To ensure the set of schedules explored is deterministic, we + -- filter out cached ones *after* selecting the children of this + -- node. + races <- catMaybes + <$> (readRaces >>= traverse (cachedST cacheRef) . take limit) + let branching = length races + -- tabulate "Races explored" (map show races) $ + tabulate "Branching factor" [bucket branching] + . tabulate "Race reversals per schedule" [bucket (raceReversals control)] + . conjoin + <$> sequence + [ go cacheRef n' ((m-1) `max` 1) r (Just trace0) + | (r,n') <- zip races (divide (n-branching) branching) ] + ] bucket :: Int -> String - bucket n | n<10 = show n - | n>=10 = buck n 1 - | otherwise = error "Ord Int is not a total order!" -- GHC made me do it! + bucket n | n<10 = show n + | otherwise = buck n 1 buck n t | n<10 = show (n*t) ++ "-" ++ show ((n+1)*t-1) - | n>=10 = buck (n `div` 10) (t*10) - | otherwise = error "Ord Int is not a total order!" -- GHC made me do it! + | otherwise = buck (n `div` 10) (t*10) + -- divide n into k factors which sums up to n divide :: Int -> Int -> [Int] divide n k = - [ n `div` k + if i String + showThread :: (IOSimThreadId,Maybe ThreadLabel) -> String showThread (tid,lab) = - show tid ++ (case lab of Nothing -> "" - Just l -> " ("++l++")") - - -- cache of explored schedules - cache :: IORef (Set ScheduleControl) - cache = unsafePerformIO cacheIO + ppIOSimThreadId tid ++ (case lab of Nothing -> "" + Just l -> " ("++l++")") -- insert a schedule into the cache - cached :: ScheduleControl -> Bool - cached = unsafePerformIO . cachedIO - - -- compute cache size; it's a function to make sure that `GHC` does not - -- inline it (and share the same thunk). - cacheSize :: () -> Int - cacheSize = unsafePerformIO . cacheSizeIO + cachedST :: STRef s (Set ScheduleControl) -> ScheduleControl -> ST s (Maybe ScheduleControl) + cachedST cacheRef a = do + set <- readSTRef cacheRef + writeSTRef cacheRef (Set.insert a set) + return $ if Set.member a set + then Nothing + else Just a -- - -- Caching in IO monad + -- Caching in ST monad -- -- It is possible for the same control to be generated several times. -- To avoid exploring them twice, we keep a cache of explored schedules. - cacheIO :: IO (IORef (Set ScheduleControl)) - cacheIO = newIORef $ + createCacheST :: ST s (STRef s (Set ScheduleControl)) + createCacheST = newSTRef $ -- we use opts here just to be sure the reference cannot be -- lifted out of exploreSimTrace if explorationScheduleBound opts >=0 then Set.empty else error "exploreSimTrace: negative schedule bound" - cachedIO :: ScheduleControl -> IO Bool - cachedIO m = atomicModifyIORef' cache $ \set -> - (Set.insert m set, Set.member m set) - - - cacheSizeIO :: () -> IO Int - cacheSizeIO () = Set.size <$> readIORef cache + cacheSizeST :: STRef s (Set ScheduleControl) -> ST s Int + cacheSizeST = fmap Set.size . readSTRef --- | A specialised version of `controlSimTrace'. --- --- An internal function. +-- | Trace `SimTrace` to `stderr`. -- -replaySimTrace :: forall a test. (Testable test) - => ExplorationOptions - -- ^ race exploration options - -> (forall s. IOSim s a) - -> ScheduleControl - -- ^ a schedule control to reproduce - -> (SimTrace a -> test) - -- ^ a callback which receives the simulation trace. The trace - -- will not contain any race events - -> Property -replaySimTrace opts mainAction control k = - let (_,trace) = detachTraceRaces $ - controlSimTrace (explorationStepTimelimit opts) control mainAction - in property (k trace) +traceDebugLog :: Int -> SimTrace a -> ST s () +traceDebugLog logLevel _trace | logLevel <= 0 = pure () +traceDebugLog 1 trace = Debug.traceM $ "Simulation trace with discovered schedules:\n" + ++ Trace.ppTrace (ppSimResult 0 0 0) (ppSimEvent 0 0 0) (ignoreRaces $ void `first` trace) +traceDebugLog _ trace = Debug.traceM $ "Simulation trace with discovered schedules:\n" + ++ Trace.ppTrace (ppSimResult 0 0 0) (ppSimEvent 0 0 0) (void `first` trace) + -- | Run a simulation using a given schedule. This is useful to reproduce -- failing cases without exploring the races. -- @@ -600,9 +667,23 @@ -> (forall s. IOSim s a) -- ^ a simulation to run -> SimTrace a -controlSimTrace limit control mainAction = - runST (controlSimTraceST limit control mainAction) +controlSimTrace limit control main = + runST (controlSimTraceST limit control main) +controlSimTraceST :: Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a) +controlSimTraceST limit control main = + detachTraceRaces <$> IOSimPOR.controlSimTraceST limit control main + + +-- +-- Utils +-- + +ignoreRaces :: SimTrace a -> SimTrace a +ignoreRaces = Trace.filter (\a -> case a of + SimPOREvent { seType = EventRaces {} } -> False + _ -> True) + raceReversals :: ScheduleControl -> Int raceReversals ControlDefault = 0 raceReversals (ControlAwait mods) = length mods @@ -618,38 +699,59 @@ -- 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 Nothing trace = (Nothing, trace) -compareTraces (Just passing) trace = unsafePerformIO $ do - sleeper <- newIORef Nothing - return (unsafePerformIO $ readIORef sleeper, - go sleeper passing trace) - where go sleeper (SimPORTrace tpass tidpass _ _ _ pass') +-- TODO: return StepId +compareTracesST :: forall a b s. + Maybe (SimTrace a) -- ^ passing + -> SimTrace b -- ^ failing + -> ST s ( ST s (Maybe ( (Time, IOSimThreadId, Maybe ThreadLabel) + , Set.Set (IOSimThreadId, Maybe ThreadLabel) + )) + , SimTrace b + ) +compareTracesST Nothing trace = return (return Nothing, trace) +compareTracesST (Just passing) trace = do + sleeper <- newSTRef Nothing + trace' <- go sleeper passing trace + return ( readSTRef sleeper + , trace' + ) + where + go :: STRef s (Maybe ( (Time, IOSimThreadId, Maybe ThreadLabel) + , Set.Set (IOSimThreadId, Maybe ThreadLabel) + )) + -> SimTrace a -- ^ passing + -> SimTrace b -- ^ failing + -> ST s (SimTrace b) + go sleeper (SimPORTrace tpass tidpass _ _ _ pass') (SimPORTrace tfail tidfail tstepfail tlfail evfail fail') | (tpass,tidpass) == (tfail,tidfail) = SimPORTrace tfail tidfail tstepfail tlfail evfail - $ go sleeper pass' fail' - go sleeper (SimPORTrace tpass tidpass tsteppass tlpass _ _) fail = - unsafePerformIO $ do - writeIORef sleeper $ Just ((tpass, tidpass, tlpass),Set.empty) - return $ SimPORTrace tpass tidpass tsteppass tlpass EventThreadSleep - $ wakeup sleeper tidpass fail - go _ SimTrace {} _ = error "compareTraces: invariant violation" - go _ _ SimTrace {} = error "compareTraces: invariant violation" - go _ _ fail = fail + <$> go sleeper pass' fail' + go sleeper (SimPORTrace tpass tidpass tsteppass tlpass _ _) fail = do + writeSTRef sleeper $ Just ((tpass, tidpass, tlpass),Set.empty) + SimPORTrace tpass tidpass tsteppass tlpass EventThreadSleep + <$> wakeup sleeper tidpass fail + go _ SimTrace {} _ = error "compareTracesST: invariant violation" + go _ _ SimTrace {} = error "compareTracesST: invariant violation" + go _ _ fail = return fail + wakeup :: STRef s (Maybe ( (Time, IOSimThreadId, Maybe ThreadLabel) + , Set.Set (IOSimThreadId, Maybe ThreadLabel) + )) + -> IOSimThreadId + -> SimTrace b + -> ST s (SimTrace b) wakeup sleeper tidpass fail@(SimPORTrace tfail tidfail tstepfail tlfail evfail fail') | tidpass == tidfail = - SimPORTrace tfail tidfail tstepfail tlfail EventThreadWake fail - | otherwise = unsafePerformIO $ do - Just (slp,racing) <- readIORef sleeper - writeIORef sleeper $ Just (slp,Set.insert (tidfail,tlfail) racing) - return $ SimPORTrace tfail tidfail tstepfail tlfail evfail - $ wakeup sleeper tidpass fail' - wakeup _ _ SimTrace {} = error "compareTraces: invariant violation" - wakeup _ _ fail = fail + return $ SimPORTrace tfail tidfail tstepfail tlfail EventThreadWake fail + | otherwise = do + ms <- readSTRef sleeper + case ms of + Just (slp, racing) -> do + writeSTRef sleeper $ Just (slp,Set.insert (tidfail,tlfail) racing) + SimPORTrace tfail tidfail tstepfail tlfail evfail + <$> wakeup sleeper tidpass fail' + Nothing -> error "compareTraceST: invariant violation" + wakeup _ _ SimTrace {} = error "compareTracesST: invariant violation" + wakeup _ _ fail = return fail diff --git a/src/Control/Monad/IOSim/CommonTypes.hs b/src/Control/Monad/IOSim/CommonTypes.hs --- a/src/Control/Monad/IOSim/CommonTypes.hs +++ b/src/Control/Monad/IOSim/CommonTypes.hs @@ -1,13 +1,36 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE DerivingVia #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ScopedTypeVariables #-} -- | Common types shared between `IOSim` and `IOSimPOR`. -- -module Control.Monad.IOSim.CommonTypes where +module Control.Monad.IOSim.CommonTypes + ( IOSimThreadId (..) + , ppIOSimThreadId + , StepId + , ppStepId + , childThreadId + , setRacyThread + , TVarId (..) + , TimeoutId (..) + , ClockId (..) + , VectorClock (..) + , ppVectorClock + , unTimeoutId + , ThreadLabel + , TVarLabel + , TVar (..) + , SomeTVar (..) + , Deschedule (..) + , ThreadStatus (..) + , BlockedReason (..) + -- * Utils + , ppList + ) where import Control.DeepSeq (NFData (..)) import Control.Monad.Class.MonadSTM (TraceValue) @@ -15,10 +38,13 @@ import NoThunks.Class +import Data.List (intercalate, intersperse) import Data.Map (Map) +import qualified Data.Map as Map import Data.STRef.Lazy import Data.Set (Set) import GHC.Generics +import Quiet -- | A thread id. @@ -28,28 +54,50 @@ -- `Control.Monad.Class.MonadTest.exploreRaces` was -- executed in it or it's a thread forked by a racy thread. -- -data ThreadId = RacyThreadId [Int] - | ThreadId [Int] -- non racy threads have higher priority +data IOSimThreadId = + -- | A racy thread (`IOSimPOR` only), shown in the trace with curly braces, + -- e.g. `Thread {2,3}`. + RacyThreadId [Int] + -- | A non racy thread. They have higher priority than racy threads in + -- `IOSimPOR` scheduler. + | ThreadId [Int] deriving stock (Eq, Ord, Show, Generic) deriving anyclass NFData deriving anyclass NoThunks +ppIOSimThreadId :: IOSimThreadId -> String +ppIOSimThreadId (RacyThreadId as) = "Thread {"++ intercalate "," (map show as) ++"}" +ppIOSimThreadId (ThreadId as) = "Thread " ++ show as -childThreadId :: ThreadId -> Int -> ThreadId +childThreadId :: IOSimThreadId -> Int -> IOSimThreadId childThreadId (RacyThreadId is) i = RacyThreadId (is ++ [i]) childThreadId (ThreadId is) i = ThreadId (is ++ [i]) -setRacyThread :: ThreadId -> ThreadId +setRacyThread :: IOSimThreadId -> IOSimThreadId setRacyThread (ThreadId is) = RacyThreadId is setRacyThread tid@RacyThreadId{} = tid +-- | Execution step in `IOSimPOR` is identified by the thread id and +-- a monotonically increasing number (thread specific). +-- +type StepId = (IOSimThreadId, Int) +ppStepId :: (IOSimThreadId, Int) -> String +ppStepId (tid, step) | step < 0 + = concat [ppIOSimThreadId tid, ".-"] +ppStepId (tid, step) = concat [ppIOSimThreadId tid, ".", show step] + + newtype TVarId = TVarId Int deriving (Eq, Ord, Enum, Show) newtype TimeoutId = TimeoutId Int deriving (Eq, Ord, Enum, Show) newtype ClockId = ClockId [Int] deriving (Eq, Ord, Show) -newtype VectorClock = VectorClock { getVectorClock :: Map ThreadId Int } - deriving Show +newtype VectorClock = VectorClock { getVectorClock :: Map IOSimThreadId Int } + deriving Generic + deriving Show via Quiet VectorClock +ppVectorClock :: VectorClock -> String +ppVectorClock (VectorClock m) = "VectorClock " ++ "[" ++ concat (intersperse ", " (ppStepId <$> Map.toList m)) ++ "]" + unTimeoutId :: TimeoutId -> Int unTimeoutId (TimeoutId a) = a @@ -80,7 +128,7 @@ -- To avoid duplicates efficiently, the operations rely on a copy of the -- thread Ids represented as a set. -- - tvarBlocked :: !(STRef s ([ThreadId], Set ThreadId)), + tvarBlocked :: !(STRef s ([IOSimThreadId], Set IOSimThreadId)), -- | The vector clock of the current value. -- @@ -110,5 +158,13 @@ deriving (Eq, Show) data BlockedReason = BlockedOnSTM - | BlockedOnOther + | BlockedOnDelay + | BlockedOnThrowTo deriving (Eq, Show) + +-- +-- Utils +-- + +ppList :: (a -> String) -> [a] -> String +ppList pp as = "[" ++ concat (intersperse ", " (map pp as)) ++ "]" diff --git a/src/Control/Monad/IOSim/Internal.hs b/src/Control/Monad/IOSim/Internal.hs --- a/src/Control/Monad/IOSim/Internal.hs +++ b/src/Control/Monad/IOSim/Internal.hs @@ -1,4 +1,5 @@ {-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleInstances #-} @@ -12,6 +13,10 @@ -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') -- and 'reschedule'. {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} +#if __GLASGOW_HASKELL__ >= 908 +-- We use partial functions from `Data.List`. +{-# OPTIONS_GHC -Wno-x-partial #-} +#endif module Control.Monad.IOSim.Internal ( IOSim (..) @@ -26,7 +31,7 @@ , TimeoutException (..) , EventlogEvent (..) , EventlogMarker (..) - , ThreadId + , IOSimThreadId , ThreadLabel , Labelled (..) , SimTrace @@ -83,12 +88,12 @@ -- data Thread s a = Thread { - threadId :: !ThreadId, + threadId :: !IOSimThreadId, threadControl :: !(ThreadControl s a), threadStatus :: !ThreadStatus, threadMasking :: !MaskingState, -- other threads blocked in a ThrowTo to us because we are or were masked - threadThrowTo :: ![(SomeException, Labelled ThreadId)], + threadThrowTo :: ![(SomeException, Labelled IOSimThreadId)], threadClockId :: !ClockId, threadLabel :: Maybe ThreadLabel, threadNextTId :: !Int @@ -102,7 +107,7 @@ labelledTVarId :: TVar s a -> ST s (Labelled TVarId) labelledTVarId TVar { tvarId, tvarLabel } = (Labelled tvarId) <$> readSTRef tvarLabel -labelledThreads :: Map ThreadId (Thread s a) -> [Labelled ThreadId] +labelledThreads :: Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId] labelledThreads threadMap = -- @Map.foldr'@ (and alikes) are not strict enough, to not ratain the -- original thread map we need to evaluate the spine of the list. @@ -121,11 +126,11 @@ -- ^ `newTimeout` timer. | TimerRegisterDelay !(TVar s Bool) -- ^ `registerDelay` timer. - | TimerThreadDelay !ThreadId !TimeoutId - -- ^ `threadDelay` timer run by `ThreadId` which was assigned the given + | TimerThreadDelay !IOSimThreadId !TimeoutId + -- ^ `threadDelay` timer run by `IOSimThreadId` which was assigned the given -- `TimeoutId` (only used to report in a trace). - | TimerTimeout !ThreadId !TimeoutId !(TMVar (IOSim s) ThreadId) - -- ^ `timeout` timer run by `ThreadId` which was assigned the given + | TimerTimeout !IOSimThreadId !TimeoutId !(TMVar (IOSim s) IOSimThreadId) + -- ^ `timeout` timer run by `IOSimThreadId` which was assigned the given -- `TimeoutId` (only used to report in a trace). @@ -134,10 +139,10 @@ -- | Internal state. -- data SimState s a = SimState { - runqueue :: !(Deque ThreadId), + runqueue :: !(Deque IOSimThreadId), -- | All threads other than the currently running thread: both running -- and blocked threads. - threads :: !(Map ThreadId (Thread s a)), + threads :: !(Map IOSimThreadId (Thread s a)), -- | current time curTime :: !Time, -- | ordered list of timers and timeouts @@ -211,7 +216,7 @@ -- the main thread is done, so we're done -- even if other threads are still running return $ SimTrace time tid tlbl EventThreadFinished - $ TraceMainReturn time x (labelledThreads threads) + $ TraceMainReturn time (Labelled tid tlbl) x (labelledThreads threads) ForkFrame -> do -- this thread is done @@ -278,7 +283,7 @@ -- An unhandled exception in the main thread terminates the program return (SimTrace time tid tlbl (EventThrow e) $ SimTrace time tid tlbl (EventThreadUnhandled e) $ - TraceMainException time e (labelledThreads threads)) + TraceMainException time (Labelled tid tlbl) e (labelledThreads threads)) | otherwise -> do -- An unhandled exception in any other thread terminates the thread @@ -424,7 +429,7 @@ let !expiry = d `addTime` time !timers' = PSQ.insert nextTmid expiry (TimerThreadDelay tid nextTmid) timers !thread' = thread { threadControl = ThreadControl (Return ()) (DelayFrame nextTmid k ctl) } - !trace <- deschedule (Blocked BlockedOnOther) thread' simstate { timers = timers' + !trace <- deschedule (Blocked BlockedOnDelay) thread' simstate { timers = timers' , nextTmid = succ nextTmid } return (SimTrace time tid tlbl (EventThreadDelay nextTmid expiry) trace) @@ -460,6 +465,9 @@ let !timers' = PSQ.delete tmid timers !thread' = thread { threadControl = ThreadControl k ctl } !written <- execAtomically' (runSTM $ writeTVar tvar TimeoutCancelled) + -- note: we are not running traceTVar on 'tvar', since its not exposed to + -- the user, and thus it cannot have an attached callback. + !_ <- traverse_ (\(SomeTVar tvar') -> commitTVar tvar') written (wakeup, wokeby) <- threadsUnblockedByWrites written mapM_ (\(SomeTVar var) -> unblockAllThreadsFromTVar var) written let (unblocked, @@ -609,10 +617,10 @@ -- exception and the source thread id to the pending async exceptions. let adjustTarget t = t { threadThrowTo = (e, Labelled tid tlbl) : threadThrowTo t } threads' = Map.adjust adjustTarget tid' threads - !trace <- deschedule (Blocked BlockedOnOther) thread' simstate { threads = threads' } + !trace <- deschedule (Blocked BlockedOnThrowTo) thread' simstate { threads = threads' } return $ SimTrace time tid tlbl (EventThrowTo e tid') $ SimTrace time tid tlbl EventThrowToBlocked - $ SimTrace time tid tlbl (EventDeschedule (Blocked BlockedOnOther)) + $ SimTrace time tid tlbl (EventDeschedule (Blocked BlockedOnThrowTo)) $ trace else do -- The target thread has async exceptions unmasked, or is masked but @@ -769,6 +777,10 @@ -- Reuse the STM functionality here to write all the timer TVars. -- Simplify to a special case that only reads and writes TVars. !written <- execAtomically' (runSTM $ mapM_ timeoutSTMAction fired) + !ds <- traverse (\(SomeTVar tvar) -> do + tr <- traceTVarST tvar False + !_ <- commitTVar tvar + return tr) written (wakeupSTM, wokeby) <- threadsUnblockedByWrites written !_ <- mapM_ (\(SomeTVar tvar) -> unblockAllThreadsFromTVar tvar) written @@ -794,6 +806,10 @@ ++ [ ( time', ThreadId [-1], Just "register delay timer" , EventRegisterDelayFired tmid) | (tmid, TimerRegisterDelay _) <- zip tmids fired ] + ++ [ (time', ThreadId [-1], Just "register delay timer", EventLog (toDyn a)) + | TraceValue { traceDynamic = Just a } <- ds ] + ++ [ (time', ThreadId [-1], Just "register delay timer", EventSay a) + | TraceValue { traceString = Just a } <- ds ] ++ [ (time', tid', tlbl', EventTxWakeup vids) | tid' <- wakeupSTM , let tlbl' = lookupThreadLabel tid' threads @@ -809,6 +825,7 @@ | (tid, _, _) <- timeoutExpired ]) trace where + timeoutSTMAction :: TimerCompletionInfo s -> STM s () timeoutSTMAction (Timer var) = do x <- readTVar var case x of @@ -821,7 +838,7 @@ timeoutSTMAction TimerThreadDelay{} = return () timeoutSTMAction TimerTimeout{} = return () -unblockThreads :: Bool -> [ThreadId] -> SimState s a -> ([ThreadId], SimState s a) +unblockThreads :: Bool -> [IOSimThreadId] -> SimState s a -> ([IOSimThreadId], SimState s a) unblockThreads !onlySTM !wakeup !simstate@SimState {runqueue, threads} = -- To preserve our invariants (that threadBlocked is correct) -- we update the runqueue and threads together here @@ -834,10 +851,10 @@ !unblocked = [ tid | tid <- wakeup , case Map.lookup tid threads of - Just Thread { threadStatus = ThreadBlocked BlockedOnOther } - -> not onlySTM Just Thread { threadStatus = ThreadBlocked BlockedOnSTM } -> True + Just Thread { threadStatus = ThreadBlocked _ } + -> not onlySTM _ -> False ] -- and in which case we mark them as now running @@ -863,7 +880,7 @@ -- receive a 'ThreadKilled' exception. -- forkTimeoutInterruptThreads :: forall s a. - [(ThreadId, TimeoutId, TMVar (IOSim s) ThreadId)] + [(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)] -> SimState s a -> ST s (SimState s a) forkTimeoutInterruptThreads timeoutExpired simState = @@ -883,13 +900,13 @@ where -- we launch a thread responsible for throwing an AsyncCancelled exception -- to the thread which timeout expired - throwToThread :: [(Thread s a, TMVar (IOSim s) ThreadId)] + throwToThread :: [(Thread s a, TMVar (IOSim s) IOSimThreadId)] (simState', throwToThread) = List.mapAccumR fn simState timeoutExpired where fn :: SimState s a - -> (ThreadId, TimeoutId, TMVar (IOSim s) ThreadId) - -> (SimState s a, (Thread s a, TMVar (IOSim s) ThreadId)) + -> (IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId) + -> (SimState s a, (Thread s a, TMVar (IOSim s) IOSimThreadId)) fn state@SimState { threads } (tid, tmid, lock) = let t = case tid `Map.lookup` threads of Just t' -> t' @@ -1003,13 +1020,13 @@ | p == p' -> collectAll (k:ks) p (x:xs) psq' _ -> (reverse ks, p, reverse xs, psq) -traceMany :: [(Time, ThreadId, Maybe ThreadLabel, SimEventType)] +traceMany :: [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)] -> SimTrace a -> SimTrace a traceMany [] trace = trace traceMany ((time, tid, tlbl, event):ts) trace = SimTrace time tid tlbl event (traceMany ts trace) -lookupThreadLabel :: ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel +lookupThreadLabel :: IOSimThreadId -> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel lookupThreadLabel tid threads = join (threadLabel <$> Map.lookup tid threads) @@ -1041,7 +1058,7 @@ execAtomically :: forall s a c. Time - -> ThreadId + -> IOSimThreadId -> Maybe ThreadLabel -> TVarId -> StmA s a @@ -1244,7 +1261,6 @@ -> ST s [SomeTVar s] go !written action = case action of ReturnStm () -> do - !_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar) written return (Map.elems written) ReadTVar v k -> do x <- execReadTVar v @@ -1322,7 +1338,7 @@ traceTVarST :: TVar s a -> Bool -- true if it's a new 'TVar' -> ST s TraceValue -traceTVarST TVar{tvarCurrent, tvarUndo, tvarTrace} new = do +traceTVarST TVar{tvarId, tvarCurrent, tvarUndo, tvarTrace} new = do mf <- readSTRef tvarTrace case mf of Nothing -> return TraceValue { traceDynamic = (Nothing :: Maybe ()) @@ -1333,7 +1349,7 @@ case (new, vs) of (True, _) -> f Nothing v (_, _:_) -> f (Just $ last vs) v - _ -> error "traceTVarST: unexpected tvar state" + _ -> error ("traceTVarST: unexpected tvar state " ++ show tvarId) @@ -1341,10 +1357,10 @@ -- Blocking and unblocking on TVars -- -readTVarBlockedThreads :: TVar s a -> ST s [ThreadId] +readTVarBlockedThreads :: TVar s a -> ST s [IOSimThreadId] readTVarBlockedThreads TVar{tvarBlocked} = fst <$> readSTRef tvarBlocked -blockThreadOnTVar :: ThreadId -> TVar s a -> ST s () +blockThreadOnTVar :: IOSimThreadId -> TVar s a -> ST s () blockThreadOnTVar tid TVar{tvarBlocked} = do (tids, tidsSet) <- readSTRef tvarBlocked when (tid `Set.notMember` tidsSet) $ do @@ -1365,7 +1381,7 @@ -- the var writes that woke them. -- threadsUnblockedByWrites :: [SomeTVar s] - -> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId))) + -> ST s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId))) threadsUnblockedByWrites written = do !tidss <- sequence [ (,) <$> labelledTVarId tvar <*> readTVarBlockedThreads tvar diff --git a/src/Control/Monad/IOSim/InternalTypes.hs b/src/Control/Monad/IOSim/InternalTypes.hs --- a/src/Control/Monad/IOSim/InternalTypes.hs +++ b/src/Control/Monad/IOSim/InternalTypes.hs @@ -15,7 +15,7 @@ import Control.Concurrent.Class.MonadSTM import Control.Monad.Class.MonadThrow (MaskingState (..)) -import Control.Monad.IOSim.Types (IOSim (..), SimA (..), ThreadId, TimeoutId) +import Control.Monad.IOSim.Types (IOSim (..), SimA (..), IOSimThreadId, TimeoutId) import GHC.Exts (oneShot) @@ -43,7 +43,7 @@ -> !(ControlStack s c a) -> ControlStack s b a TimeoutFrame :: TimeoutId - -> TMVar (IOSim s) ThreadId + -> TMVar (IOSim s) IOSimThreadId -> (Maybe b -> SimA s c) -> !(ControlStack s c a) -> ControlStack s b a @@ -74,7 +74,7 @@ | DelayFrame' TimeoutId ControlStackDash deriving Show -data IsLocked = NotLocked | Locked !ThreadId +data IsLocked = NotLocked | Locked !IOSimThreadId deriving (Eq, Show) -- | Unsafe method which removes a timeout. diff --git a/src/Control/Monad/IOSim/Types.hs b/src/Control/Monad/IOSim/Types.hs --- a/src/Control/Monad/IOSim/Types.hs +++ b/src/Control/Monad/IOSim/Types.hs @@ -5,6 +5,7 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE NumericUnderscores #-} @@ -22,7 +23,6 @@ , traceSTM , liftST , SimA (..) - , StepId , STMSim , STM (..) , runSTM @@ -34,6 +34,7 @@ , setCurrentTime , unshareClock , ScheduleControl (..) + , isDefaultSchedule , ScheduleMod (..) , ExplorationOptions (..) , ExplorationSpec @@ -45,10 +46,12 @@ , EventlogEvent (..) , EventlogMarker (..) , SimEventType (..) + , ppSimEventType , SimEvent (..) , SimResult (..) + , ppSimResult , SimTrace - , Trace.Trace (SimTrace, SimPORTrace, TraceMainReturn, TraceMainException, TraceDeadlock, TraceRacesFound, TraceLoop) + , Trace.Trace (SimTrace, SimPORTrace, TraceMainReturn, TraceMainException, TraceDeadlock, TraceRacesFound, TraceLoop, TraceInternalError) , ppTrace , ppTrace_ , ppSimEvent @@ -81,8 +84,7 @@ import Control.Monad.Class.MonadAsync hiding (Async) import qualified Control.Monad.Class.MonadAsync as MonadAsync import Control.Monad.Class.MonadEventlog -import Control.Monad.Class.MonadFork hiding (ThreadId) -import qualified Control.Monad.Class.MonadFork as MonadFork +import Control.Monad.Class.MonadFork import Control.Monad.Class.MonadST import Control.Monad.Class.MonadSTM.Internal (MonadInspectSTM (..), MonadLabelledSTM (..), MonadSTM, MonadTraceSTM (..), @@ -132,6 +134,7 @@ import qualified System.IO.Error as IO.Error (userError) +import Data.List (intercalate) {-# ANN module "HLint: ignore Use readTVarIO" #-} newtype IOSim s a = IOSim { unIOSim :: forall r. (a -> SimA s r) -> SimA s r } @@ -180,13 +183,13 @@ SimA s a -> (e -> SimA s a) -> (a -> SimA s b) -> SimA s b Evaluate :: a -> (a -> SimA s b) -> SimA s b - Fork :: IOSim s () -> (ThreadId -> SimA s b) -> SimA s b - GetThreadId :: (ThreadId -> SimA s b) -> SimA s b - LabelThread :: ThreadId -> String -> SimA s b -> SimA s b + Fork :: IOSim s () -> (IOSimThreadId -> SimA s b) -> SimA s b + GetThreadId :: (IOSimThreadId -> SimA s b) -> SimA s b + LabelThread :: IOSimThreadId -> String -> SimA s b -> SimA s b Atomically :: STM s a -> (a -> SimA s b) -> SimA s b - ThrowTo :: SomeException -> ThreadId -> SimA s a -> SimA s a + ThrowTo :: SomeException -> IOSimThreadId -> SimA s a -> SimA s a SetMaskState :: MaskingState -> IOSim s a -> (a -> SimA s b) -> SimA s b GetMaskState :: (MaskingState -> SimA s b) -> SimA s b @@ -447,7 +450,7 @@ blockUninterruptible a = IOSim (SetMaskState MaskedUninterruptible a) instance MonadThread (IOSim s) where - type ThreadId (IOSim s) = ThreadId + type ThreadId (IOSim s) = IOSimThreadId myThreadId = IOSim $ oneShot $ \k -> GetThreadId k labelThread t l = IOSim $ oneShot $ \k -> LabelThread t l (k ()) @@ -467,6 +470,10 @@ instance MonadLabelledSTM (IOSim s) where labelTVar tvar label = STM $ \k -> LabelTVar label tvar (k ()) + labelTVarIO tvar label = IOSim $ oneShot $ \k -> + LiftST ( lazyToStrictST $ + writeSTRef (tvarLabel tvar) $! (Just label) + ) k labelTQueue = labelTQueueDefault labelTBQueue = labelTBQueueDefault @@ -551,6 +558,10 @@ -- instance MonadTraceSTM (IOSim s) where traceTVar _ tvar f = STM $ \k -> TraceTVar tvar f (k ()) + traceTVarIO tvar f = IOSim $ oneShot $ \k -> + LiftST ( lazyToStrictST $ + writeSTRef (tvarTrace tvar) $! Just f + ) k traceTQueue = traceTQueueDefault traceTBQueue = traceTBQueueDefault @@ -575,7 +586,7 @@ MVarEmpty _ _ -> pure Nothing MVarFull x _ -> pure (Just x) -data Async s a = Async !ThreadId (STM s (Either SomeException a)) +data Async s a = Async !IOSimThreadId (STM s (Either SomeException a)) instance Eq (Async s a) where Async tid _ == Async tid' _ = tid == tid' @@ -742,14 +753,14 @@ -- | Used when using `IOSim`. = SimEvent { seTime :: !Time, - seThreadId :: !ThreadId, + seThreadId :: !IOSimThreadId, seThreadLabel :: !(Maybe ThreadLabel), seType :: !SimEventType } -- | Only used for /IOSimPOR/ | SimPOREvent { seTime :: !Time, - seThreadId :: !ThreadId, + seThreadId :: !IOSimThreadId, seStep :: !Int, seThreadLabel :: !(Maybe ThreadLabel), seType :: !SimEventType @@ -767,46 +778,92 @@ -> Int -- ^ width of thread label -> SimEvent -> String -ppSimEvent timeWidth tidWidth tLabelWidth SimEvent {seTime, seThreadId, seThreadLabel, seType} = + +ppSimEvent timeWidth tidWidth tLabelWidth SimEvent {seTime = Time time, seThreadId, seThreadLabel, seType} = printf "%-*s - %-*s %-*s - %s" timeWidth - (show seTime) + (show time) tidWidth - (show seThreadId) + (ppIOSimThreadId seThreadId) tLabelWidth threadLabel - (show seType) + (ppSimEventType seType) where threadLabel = fromMaybe "" seThreadLabel -ppSimEvent timeWidth tidWidth tLableWidth SimPOREvent {seTime, seThreadId, seStep, seThreadLabel, seType} = + +ppSimEvent timeWidth tidWidth tLableWidth SimPOREvent {seTime = Time time, seThreadId, seStep, seThreadLabel, seType} = printf "%-*s - %-*s %-*s - %s" timeWidth - (show seTime) + (show time) tidWidth - (show (seThreadId, seStep)) + (ppStepId (seThreadId, seStep)) tLableWidth threadLabel - (show seType) + (ppSimEventType seType) where threadLabel = fromMaybe "" seThreadLabel + ppSimEvent _ _ _ (SimRacesFound controls) = "RacesFound "++show controls + -- | A result type of a simulation. data SimResult a - = MainReturn !Time a ![Labelled ThreadId] + = MainReturn !Time !(Labelled IOSimThreadId) a ![Labelled IOSimThreadId] -- ^ Return value of the main thread. - | MainException !Time SomeException ![Labelled ThreadId] + | MainException !Time !(Labelled IOSimThreadId) SomeException ![Labelled IOSimThreadId] -- ^ Exception thrown by the main thread. - | Deadlock !Time ![Labelled ThreadId] + | Deadlock !Time ![Labelled IOSimThreadId] -- ^ Deadlock discovered in the simulation. Deadlocks are discovered if -- simply the simulation cannot do any progress in a given time slot and -- there's no event which would advance the time. | Loop -- ^ Only returned by /IOSimPOR/ when a step execution took longer than -- 'explorationStepTimelimit` was exceeded. + | InternalError String deriving (Show, Functor) +ppSimResult :: Show a + => Int + -> Int + -> Int + -> SimResult a + -> String +ppSimResult timeWidth tidWidth thLabelWidth r = case r of + MainReturn (Time time) tid a tids -> + printf "%-*s - %-*s %-*s - %s %s" + timeWidth + (show time) + tidWidth + (ppIOSimThreadId (l_labelled tid)) + thLabelWidth + (fromMaybe "" $ l_label tid) + ("MainReturn " ++ show a) + ("[" ++ intercalate "," (ppLabelled ppIOSimThreadId `map` tids) ++ "]") + MainException (Time time) tid e tids -> + printf "%-*s - %-*s %-*s - %s %s" + timeWidth + (show time) + tidWidth + (ppIOSimThreadId (l_labelled tid)) + thLabelWidth + (fromMaybe "" $ l_label tid) + ("MainException " ++ show e) + ("[" ++ intercalate "," (ppLabelled ppIOSimThreadId `map` tids) ++ "]") + Deadlock (Time time) tids -> + printf "%-*s - %-*s %-*s - %s %s" + timeWidth + (show time) + tidWidth + "" + thLabelWidth + "" + "Deadlock" + ("[" ++ intercalate "," (ppLabelled ppIOSimThreadId `map` tids) ++ "]") + Loop -> "<>" + InternalError e -> "<>" + + -- | A type alias for 'IOSim' simulation trace. It comes with useful pattern -- synonyms. -- @@ -816,21 +873,21 @@ -- ppTrace :: Show a => SimTrace a -> String ppTrace tr = Trace.ppTrace - show - (ppSimEvent timeWidth tidWith labelWidth) + (ppSimResult timeWidth tidWidth labelWidth) + (ppSimEvent timeWidth tidWidth labelWidth) tr where - (Max timeWidth, Max tidWith, Max labelWidth) = + (Max timeWidth, Max tidWidth, Max labelWidth) = bimaximum . bimap (const (Max 0, Max 0, Max 0)) (\a -> case a of - SimEvent {seTime, seThreadId, seThreadLabel} -> - ( Max (length (show seTime)) + SimEvent {seTime = Time time, seThreadId, seThreadLabel} -> + ( Max (length (show time)) , Max (length (show (seThreadId))) , Max (length seThreadLabel) ) - SimPOREvent {seTime, seThreadId, seThreadLabel} -> - ( Max (length (show seTime)) + SimPOREvent {seTime = Time time, seThreadId, seThreadLabel} -> + ( Max (length (show time)) , Max (length (show (seThreadId))) , Max (length seThreadLabel) ) @@ -845,10 +902,10 @@ ppTrace_ :: SimTrace a -> String ppTrace_ tr = Trace.ppTrace (const "") - (ppSimEvent timeWidth tidWith labelWidth) + (ppSimEvent timeWidth tidWidth labelWidth) tr where - (Max timeWidth, Max tidWith, Max labelWidth) = + (Max timeWidth, Max tidWidth, Max labelWidth) = bimaximum . bimap (const (Max 0, Max 0, Max 0)) (\a -> case a of @@ -867,6 +924,8 @@ ) $ tr + + -- | Trace each event using 'Debug.trace'; this is useful when a trace ends with -- a pure error, e.g. an assertion. -- @@ -876,13 +935,13 @@ . Trace.toList -pattern SimTrace :: Time -> ThreadId -> Maybe ThreadLabel -> SimEventType -> SimTrace a +pattern SimTrace :: Time -> IOSimThreadId -> Maybe ThreadLabel -> SimEventType -> SimTrace a -> SimTrace a pattern SimTrace time threadId threadLabel traceEvent trace = Trace.Cons (SimEvent time threadId threadLabel traceEvent) trace -pattern SimPORTrace :: Time -> ThreadId -> Int -> Maybe ThreadLabel -> SimEventType -> SimTrace a +pattern SimPORTrace :: Time -> IOSimThreadId -> Int -> Maybe ThreadLabel -> SimEventType -> SimTrace a -> SimTrace a pattern SimPORTrace time threadId step threadLabel traceEvent trace = Trace.Cons (SimPOREvent time threadId step threadLabel traceEvent) @@ -894,24 +953,27 @@ Trace.Cons (SimRacesFound controls) trace -pattern TraceMainReturn :: Time -> a -> [Labelled ThreadId] +pattern TraceMainReturn :: Time -> Labelled IOSimThreadId -> a -> [Labelled IOSimThreadId] -> SimTrace a -pattern TraceMainReturn time a threads = Trace.Nil (MainReturn time a threads) +pattern TraceMainReturn time tid a threads = Trace.Nil (MainReturn time tid a threads) -pattern TraceMainException :: Time -> SomeException -> [Labelled ThreadId] +pattern TraceMainException :: Time -> Labelled IOSimThreadId -> SomeException -> [Labelled IOSimThreadId] -> SimTrace a -pattern TraceMainException time err threads = Trace.Nil (MainException time err threads) +pattern TraceMainException time tid err threads = Trace.Nil (MainException time tid err threads) -pattern TraceDeadlock :: Time -> [Labelled ThreadId] +pattern TraceDeadlock :: Time -> [Labelled IOSimThreadId] -> SimTrace a pattern TraceDeadlock time threads = Trace.Nil (Deadlock time threads) pattern TraceLoop :: SimTrace a pattern TraceLoop = Trace.Nil Loop -{-# COMPLETE SimTrace, SimPORTrace, TraceMainReturn, TraceMainException, TraceDeadlock, TraceLoop #-} +pattern TraceInternalError :: String -> SimTrace a +pattern TraceInternalError msg = Trace.Nil (InternalError msg) +{-# COMPLETE SimTrace, SimPORTrace, TraceMainReturn, TraceMainException, TraceDeadlock, TraceLoop, TraceInternalError #-} + -- | Events recorded by the simulation. -- data SimEventType @@ -924,17 +986,17 @@ | EventThrow SomeException -- ^ throw exception - | EventThrowTo SomeException ThreadId + | EventThrowTo SomeException IOSimThreadId -- ^ throw asynchronous exception (`throwTo`) | EventThrowToBlocked -- ^ the thread which executed `throwTo` is blocked | EventThrowToWakeup -- ^ the thread which executed `throwTo` is woken up - | EventThrowToUnmasked (Labelled ThreadId) + | EventThrowToUnmasked (Labelled IOSimThreadId) -- ^ a target thread of `throwTo` unmasked its exceptions, this is paired -- with `EventThrowToWakeup` for threads which were blocked on `throwTo` - | EventThreadForked ThreadId + | EventThreadForked IOSimThreadId -- ^ forked a thread | EventThreadFinished -- ^ thread terminated normally @@ -958,7 +1020,7 @@ (Maybe Effect) -- ^ effect performed (only for `IOSimPOR`) | EventTxWakeup [Labelled TVarId] -- ^ changed vars causing retry - | EventUnblocked [ThreadId] + | EventUnblocked [IOSimThreadId] -- ^ unblocked threads by a committed STM transaction -- @@ -970,7 +1032,7 @@ | EventThreadDelayFired TimeoutId -- ^ thread woken up after a delay - | EventTimeoutCreated TimeoutId ThreadId Time + | EventTimeoutCreated TimeoutId IOSimThreadId Time -- ^ new timeout created (via `timeout`) | EventTimeoutFired TimeoutId -- ^ timeout fired @@ -994,8 +1056,8 @@ -- -- | event traced when `threadStatus` is executed - | EventThreadStatus ThreadId -- ^ current thread - ThreadId -- ^ queried thread + | EventThreadStatus IOSimThreadId -- ^ current thread + IOSimThreadId -- ^ queried thread -- -- /IOSimPOR/ events @@ -1020,12 +1082,104 @@ | EventPerformAction StepId -- ^ /IOSimPOR/ event: perform action of the given step | EventReschedule ScheduleControl + + | EventEffect VectorClock Effect + -- ^ /IOSimPOR/ event: executed effect; Useful for debugging IOSimPOR or + -- showing compact information about thread execution. + | EventRaces Races + -- ^ /IOSimPOR/ event: races. Races are updated while we execute + -- a simulation. Useful for debugging IOSimPOR. deriving Show +ppSimEventType :: SimEventType -> String +ppSimEventType = \case + EventSay a -> "Say " ++ a + EventLog a -> "Dynamic " ++ show a + EventMask a -> "Mask " ++ show a + EventThrow a -> "Throw " ++ show a + EventThrowTo err tid -> + concat [ "ThrowTo (", + show err, ") ", + ppIOSimThreadId tid ] + EventThrowToBlocked -> "ThrowToBlocked" + EventThrowToWakeup -> "ThrowToWakeup" + EventThrowToUnmasked a -> + "ThrowToUnmasked " ++ ppLabelled ppIOSimThreadId a + EventThreadForked a -> + "ThreadForked " ++ ppIOSimThreadId a + EventThreadFinished -> "ThreadFinished" + EventThreadUnhandled a -> + "ThreadUnhandled " ++ show a + EventTxCommitted written created mbEff -> + concat [ "TxCommitted ", + ppList (ppLabelled show) written, " ", + ppList (ppLabelled show) created, + maybe "" ((' ' :) . ppEffect) mbEff ] + EventTxAborted mbEff -> + concat [ "TxAborted", + maybe "" ((' ' :) . ppEffect) mbEff ] + EventTxBlocked blocked mbEff -> + concat [ "TxBlocked ", + ppList (ppLabelled show) blocked, + maybe "" ((' ' :) . ppEffect) mbEff ] + EventTxWakeup changed -> + "TxWakeup " ++ ppList (ppLabelled show) changed + EventUnblocked unblocked -> + "Unblocked " ++ ppList ppIOSimThreadId unblocked + EventThreadDelay tid t -> + concat [ "ThreadDelay ", + show tid, " ", + show t ] + EventThreadDelayFired tid -> "ThreadDelayFired " ++ show tid + EventTimeoutCreated timer tid t -> + concat [ "TimeoutCreated ", + show timer, " ", + ppIOSimThreadId tid, " ", + show t ] + EventTimeoutFired timer -> + "TimeoutFired " ++ show timer + EventRegisterDelayCreated timer tvarId t -> + concat [ "RegisterDelayCreated ", + show timer, " ", + show tvarId, " ", + show t ] + EventRegisterDelayFired timer -> "RegisterDelayFired " ++ show timer + EventTimerCreated timer tvarId t -> + concat [ "TimerCreated ", + show timer, " ", + show tvarId, " ", + show t ] + EventTimerUpdated timer t -> + concat [ "TimerUpdated ", + show timer, " ", + show t ] + EventTimerCancelled timer -> "TimerCancelled " ++ show timer + EventTimerFired timer -> "TimerFired " ++ show timer + EventThreadStatus tid tid' -> + concat [ "ThreadStatus ", + ppIOSimThreadId tid, " ", + ppIOSimThreadId tid' ] + EventSimStart a -> "SimStart " ++ show a + EventThreadSleep -> "ThreadSleep" + EventThreadWake -> "ThreadWake" + EventDeschedule a -> "Deschedule " ++ show a + EventFollowControl a -> "FollowControl " ++ show a + EventAwaitControl s a -> + concat [ "AwaitControl ", + ppStepId s, " ", + show a ] + EventPerformAction a -> "PerformAction " ++ ppStepId a + EventReschedule a -> "Reschedule " ++ show a + EventEffect clock eff -> + concat [ "Effect ", + ppVectorClock clock, " ", + ppEffect eff ] + EventRaces a -> show a + -- | A labelled value. -- --- For example 'labelThread' or `labelTVar' will insert a label to `ThreadId` +-- For example 'labelThread' or `labelTVar' will insert a label to `IOSimThreadId` -- (or `TVarId`). data Labelled a = Labelled { l_labelled :: !a, @@ -1034,6 +1188,10 @@ deriving (Eq, Ord, Generic) deriving Show via Quiet (Labelled a) +ppLabelled :: (a -> String) -> Labelled a -> String +ppLabelled pp Labelled { l_labelled = a, l_label = Nothing } = pp a +ppLabelled pp Labelled { l_labelled = a, l_label = Just lbl } = concat ["Labelled ", pp a, " ", lbl] + -- -- Executing STM Transactions -- @@ -1102,58 +1260,7 @@ -> StmStack s b c -> StmStack s a c - --- ---- Schedules ---- - --- | Modified execution schedule. --- -data ScheduleControl = ControlDefault - -- ^ default scheduling mode - | ControlAwait [ScheduleMod] - -- ^ if the current control is 'ControlAwait', the normal - -- scheduling will proceed, until the thread found in the - -- first 'ScheduleMod' reaches the given step. At this - -- point the thread is put to sleep, until after all the - -- steps are followed. - | ControlFollow [StepId] [ScheduleMod] - -- ^ follow the steps then continue with schedule - -- modifications. This control is set by 'followControl' - -- when 'controlTargets' returns true. - deriving (Eq, Ord, Show) - --- | A schedule modification inserted at given execution step. --- -data ScheduleMod = ScheduleMod{ - -- | Step at which the 'ScheduleMod' is activated. - scheduleModTarget :: StepId, - -- | 'ScheduleControl' at the activation step. It is needed by - -- 'extendScheduleControl' when combining the discovered schedule with the - -- initial one. - scheduleModControl :: ScheduleControl, - -- | Series of steps which are executed at the target step. This *includes* - -- the target step, not necessarily as the last step. - scheduleModInsertion :: [StepId] - } - deriving (Eq, Ord) - --- | Execution step is identified by the thread id and a monotonically --- increasing number (thread specific). --- -type StepId = (ThreadId, Int) - -instance Show ScheduleMod where - showsPrec d (ScheduleMod tgt ctrl insertion) = - showParen (d>10) $ - showString "ScheduleMod " . - showsPrec 11 tgt . - showString " " . - showsPrec 11 ctrl . - showString " " . - showsPrec 11 insertion - ---- --- Exploration options --- @@ -1189,10 +1296,21 @@ -- catching infinite loops etc. -- -- The default value is `Nothing`. - explorationReplay :: Maybe ScheduleControl + explorationReplay :: Maybe ScheduleControl, -- ^ A schedule to replay. -- -- The default value is `Nothing`. + explorationDebugLevel :: Int + -- ^ Log detailed trace to stderr containing information on discovered + -- races. The trace does not contain the result of the simulation, unless + -- one will do that explicitly inside the simulation. + -- + -- level 0: don't show any output, + -- level 1: show simulation trace with discovered schedules + -- level 2: show simulation trace with discovered schedules and races + -- + -- NOTE: discovered schedules & races are not exposed to the user in the + -- callback of `exploreSimTrace` or in the output of `controlSimTrace`. } deriving Show @@ -1201,7 +1319,8 @@ explorationScheduleBound = 100, explorationBranching = 3, explorationStepTimelimit = Nothing, - explorationReplay = Nothing + explorationReplay = Nothing, + explorationDebugLevel = 0 } type ExplorationSpec = ExplorationOptions -> ExplorationOptions diff --git a/src/Control/Monad/IOSimPOR/Internal.hs b/src/Control/Monad/IOSimPOR/Internal.hs --- a/src/Control/Monad/IOSimPOR/Internal.hs +++ b/src/Control/Monad/IOSimPOR/Internal.hs @@ -1,4 +1,5 @@ {-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} @@ -7,12 +8,18 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RankNTypes #-} +-- only used to construct records if its clear to do so +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') -- and 'reschedule'. {-# OPTIONS_GHC -Wno-incomplete-uni-patterns -Wno-unused-matches #-} +#if __GLASGOW_HASKELL__ >= 908 +-- We use partial functions from `Data.List`. +{-# OPTIONS_GHC -Wno-x-partial #-} +#endif module Control.Monad.IOSimPOR.Internal ( IOSim (..) @@ -27,7 +34,7 @@ , TimeoutException (..) , EventlogEvent (..) , EventlogMarker (..) - , ThreadId + , IOSimThreadId , ThreadLabel , Labelled (..) , SimTrace @@ -86,12 +93,12 @@ -- data Thread s a = Thread { - threadId :: !ThreadId, + threadId :: !IOSimThreadId, threadControl :: !(ThreadControl s a), threadStatus :: !ThreadStatus, threadMasking :: !MaskingState, -- other threads blocked in a ThrowTo to us because we are or were masked - threadThrowTo :: ![(SomeException, Labelled ThreadId, VectorClock)], + threadThrowTo :: ![(SomeException, Labelled IOSimThreadId, VectorClock)], threadClockId :: !ClockId, threadLabel :: Maybe ThreadLabel, threadNextTId :: !Int, @@ -112,21 +119,21 @@ ThreadDone -> True _ -> False -threadStepId :: Thread s a -> (ThreadId, Int) +threadStepId :: Thread s a -> (IOSimThreadId, Int) threadStepId Thread{ threadId, threadStep } = (threadId, threadStep) -isRacyThreadId :: ThreadId -> Bool +isRacyThreadId :: IOSimThreadId -> Bool isRacyThreadId (RacyThreadId _) = True isRacyThreadId _ = True -isNotRacyThreadId :: ThreadId -> Bool +isNotRacyThreadId :: IOSimThreadId -> Bool isNotRacyThreadId (ThreadId _) = True isNotRacyThreadId _ = False bottomVClock :: VectorClock bottomVClock = VectorClock Map.empty -insertVClock :: ThreadId -> Int -> VectorClock -> VectorClock +insertVClock :: IOSimThreadId -> Int -> VectorClock -> VectorClock insertVClock tid !step (VectorClock m) = VectorClock (Map.insert tid step m) leastUpperBoundVClock :: VectorClock -> VectorClock -> VectorClock @@ -147,7 +154,7 @@ labelledTVarId :: TVar s a -> ST s (Labelled TVarId) labelledTVarId TVar { tvarId, tvarLabel } = Labelled tvarId <$> readSTRef tvarLabel -labelledThreads :: Map ThreadId (Thread s a) -> [Labelled ThreadId] +labelledThreads :: Map IOSimThreadId (Thread s a) -> [Labelled IOSimThreadId] labelledThreads threadMap = -- @Map.foldr'@ (and alikes) are not strict enough, to not retain the -- original thread map we need to evaluate the spine of the list. @@ -166,14 +173,14 @@ -- ^ `newTimeout` timer. | TimerRegisterDelay !(TVar s Bool) -- ^ `registerDelay` timer. - | TimerThreadDelay !ThreadId !TimeoutId - -- ^ `threadDelay` timer run by `ThreadId` which was assigned the given + | TimerThreadDelay !IOSimThreadId !TimeoutId + -- ^ `threadDelay` timer run by `IOSimThreadId` which was assigned the given -- `TimeoutId` (only used to report in a trace). - | TimerTimeout !ThreadId !TimeoutId !(TMVar (IOSim s) ThreadId) - -- ^ `timeout` timer run by `ThreadId` which was assigned the given + | TimerTimeout !IOSimThreadId !TimeoutId !(TMVar (IOSim s) IOSimThreadId) + -- ^ `timeout` timer run by `IOSimThreadId` which was assigned the given -- `TimeoutId` (only used to report in a trace). -type RunQueue = OrdPSQ (Down ThreadId) (Down ThreadId) () +type RunQueue = OrdPSQ (Down IOSimThreadId) (Down IOSimThreadId) () type Timeouts s = OrdPSQ TimeoutId Time (TimerCompletionInfo s) -- | Internal state. @@ -182,7 +189,7 @@ runqueue :: !RunQueue, -- | All threads other than the currently running thread: both running -- and blocked threads. - threads :: !(Map ThreadId (Thread s a)), + threads :: !(Map IOSimThreadId (Thread s a)), -- | current time curTime :: !Time, -- | ordered list of timers and timeouts @@ -312,10 +319,11 @@ -- even if other threads are still running return $ SimPORTrace time tid tstep tlbl EventThreadFinished $ traceFinalRacesFound simstate - $ TraceMainReturn time x ( labelledThreads - . Map.filter (not . isThreadDone) - $ threads - ) + $ TraceMainReturn time (Labelled tid tlbl) x + ( labelledThreads + . Map.filter (not . isThreadDone) + $ threads + ) ForkFrame -> do -- this thread is done @@ -374,14 +382,17 @@ (Right thread0@Thread { threadMasking = maskst' }, timers'') -> do -- We found a suitable exception handler, continue with that -- We record a step, in case there is no exception handler on replay. - let thread' = stepThread thread0 - control' = advanceControl (threadStepId thread0) control - races' = updateRacesInSimState thread0 simstate + let (thread', eff) = stepThread thread0 + control' = advanceControl (threadStepId thread0) control + races' = updateRaces thread0 simstate trace <- schedule thread' simstate{ races = races', control = control', timers = timers'' } return (SimPORTrace time tid tstep tlbl (EventThrow e) $ - SimPORTrace time tid tstep tlbl (EventMask maskst') trace) + SimPORTrace time tid tstep tlbl (EventMask maskst') $ + SimPORTrace time tid tstep tlbl (EventEffect vClock eff) $ + SimPORTrace time tid tstep tlbl (EventRaces races') + trace) (Left isMain, timers'') -- We unwound and did not find any suitable exception handler, so we @@ -392,7 +403,7 @@ return (SimPORTrace time tid tstep tlbl (EventThrow e) $ SimPORTrace time tid tstep tlbl (EventThreadUnhandled e) $ traceFinalRacesFound simstate { threads = Map.insert tid thread' threads } $ - TraceMainException time e (labelledThreads threads)) + TraceMainException time (Labelled tid tlbl) e (labelledThreads threads)) | otherwise -> do -- An unhandled exception in any other thread terminates the thread @@ -525,7 +536,7 @@ let expiry = d `addTime` time timers' = PSQ.insert nextTmid expiry (TimerThreadDelay tid nextTmid) timers thread' = thread { threadControl = ThreadControl (Return ()) (DelayFrame nextTmid k ctl) } - trace <- deschedule (Blocked BlockedOnOther) thread' + trace <- deschedule (Blocked BlockedOnDelay) thread' simstate { timers = timers', nextTmid = succ nextTmid } return (SimPORTrace time tid tstep tlbl (EventThreadDelay nextTmid expiry) trace) @@ -599,7 +610,7 @@ thread'' = Thread { threadId = tid' , threadControl = ThreadControl (runIOSim a) ForkFrame - , threadStatus = ThreadRunning + , threadStatus = ThreadRunning , threadMasking = threadMasking thread , threadThrowTo = [] , threadClockId = threadClockId thread @@ -646,7 +657,7 @@ return $ SimPORTrace time tid tstep tlbl (EventTxCommitted written' created' (Just effect')) $ traceMany - [ (time, tid', tstep, tlbl', EventTxWakeup vids') + [ (time, tid', (-1), tlbl', EventTxWakeup vids') | tid' <- unblocked , let tlbl' = lookupThreadLabel tid' threads , let Just vids' = Set.toList <$> Map.lookup tid' wokeby ] $ @@ -759,10 +770,10 @@ let adjustTarget t = t { threadThrowTo = (e, Labelled tid tlbl, vClock) : threadThrowTo t } threads' = Map.adjust adjustTarget tid' threads - trace <- deschedule (Blocked BlockedOnOther) thread' simstate { threads = threads' } + trace <- deschedule (Blocked BlockedOnThrowTo) thread' simstate { threads = threads' } return $ SimPORTrace time tid tstep tlbl (EventThrowTo e tid') $ SimPORTrace time tid tstep tlbl EventThrowToBlocked - $ SimPORTrace time tid tstep tlbl (EventDeschedule (Blocked BlockedOnOther)) + $ SimPORTrace time tid tstep tlbl (EventDeschedule (Blocked BlockedOnThrowTo)) $ trace else do -- The target thread has async exceptions unmasked, or is masked but @@ -807,19 +818,29 @@ deschedule :: Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a) -deschedule Yield thread@Thread { threadId = tid } - simstate@SimState{runqueue, threads, control} = +deschedule Yield thread@Thread { threadId = tid, + threadStep = tstep, + threadLabel = tlbl, + threadVClock = vClock } + simstate@SimState{runqueue, + threads, + curTime = time, + control } = -- We don't interrupt runnable threads anywhere else. -- We do it here by inserting the current thread into the runqueue in priority order. - let thread' = stepThread thread - runqueue' = insertThread thread' runqueue - threads' = Map.insert tid thread' threads - control' = advanceControl (threadStepId thread) control in + let (thread', eff) = stepThread thread + runqueue' = insertThread thread' runqueue + threads' = Map.insert tid thread' threads + control' = advanceControl (threadStepId thread) control + races' = updateRaces thread simstate in + + SimPORTrace time tid tstep tlbl (EventEffect vClock eff) . + SimPORTrace time tid tstep tlbl (EventRaces races') <$> reschedule simstate { runqueue = runqueue', threads = threads', - races = updateRacesInSimState thread simstate, + races = races', control = control' } deschedule Interruptable thread@Thread { @@ -834,79 +855,109 @@ } simstate@SimState{ curTime = time, threads } = do - -- We're unmasking, but there are pending blocked async exceptions. - -- So immediately raise the exception and unblock the blocked thread - -- if possible. - let thread' = thread { threadControl = ThreadControl (Throw e) ctl + let effect' = effect <> wakeupEffects unblocked + -- We're unmasking, but there are pending blocked async exceptions. + -- So immediately raise the exception and unblock the blocked thread + -- if possible. + thread' = thread { threadControl = ThreadControl (Throw e) ctl , threadMasking = MaskedInterruptible , threadThrowTo = etids , threadVClock = vClock `leastUpperBoundVClock` vClock' + , threadEffect = effect' } (unblocked, simstate') = unblockThreads False vClock [l_labelled tid'] simstate -- the thread is stepped when we Yield !trace <- deschedule Yield thread' simstate' - return $ SimPORTrace time tid tstep tlbl (EventDeschedule Yield) - $ SimPORTrace time tid tstep tlbl (EventThrowToUnmasked tid') + return $ SimPORTrace time tid tstep tlbl (EventThrowToUnmasked tid') + $ SimPORTrace time tid tstep tlbl (EventEffect vClock effect') -- TODO: step $ traceMany [ (time, tid'', (-1), tlbl'', EventThrowToWakeup) | tid'' <- unblocked , let tlbl'' = lookupThreadLabel tid'' threads ] + $ SimPORTrace time tid tstep tlbl (EventDeschedule Yield) trace -deschedule Interruptable thread@Thread{threadId = tid } simstate@SimState{ control } = +deschedule Interruptable thread@Thread{threadId = tid, + threadStep = tstep, + threadLabel = tlbl, + threadVClock = vClock} + simstate@SimState{ control, + curTime = time } = -- Either masked or unmasked but no pending async exceptions. -- Either way, just carry on. -- Record a step, though, in case on replay there is an async exception. - let thread' = stepThread thread in + let (thread', eff) = stepThread thread + races' = updateRaces thread simstate in + + SimPORTrace time tid tstep tlbl (EventEffect vClock eff) . + SimPORTrace time tid tstep tlbl (EventRaces races') <$> schedule thread' - simstate{ races = updateRacesInSimState thread simstate, + simstate{ races = races', control = advanceControl (threadStepId thread) control } deschedule (Blocked _blockedReason) thread@Thread { threadId = tid + , threadStep = tstep + , threadLabel = tlbl , threadThrowTo = _ : _ , threadMasking = maskst - , threadEffect = effect } simstate + , threadEffect = effect } + simstate@SimState{ curTime = time } | maskst /= MaskedUninterruptible = -- We're doing a blocking operation, which is an interrupt point even if -- we have async exceptions masked, and there are pending blocked async -- exceptions. So immediately raise the exception and unblock the blocked -- thread if possible. - deschedule Interruptable thread { threadMasking = Unmasked } simstate + SimPORTrace time tid tstep tlbl (EventDeschedule Interruptable) <$> + deschedule Interruptable thread { threadMasking = Unmasked } simstate -deschedule (Blocked blockedReason) thread@Thread{ threadId = tid, threadEffect = effect } simstate@SimState{threads, control} = - let thread1 = thread { threadStatus = ThreadBlocked blockedReason } - thread' = stepThread thread1 - threads' = Map.insert (threadId thread') thread' threads in +deschedule (Blocked blockedReason) thread@Thread{ threadId = tid, + threadStep = tstep, + threadLabel = tlbl, + threadVClock = vClock} + simstate@SimState{ threads, + curTime = time, + control } = + let thread1 = thread { threadStatus = ThreadBlocked blockedReason } + (thread', eff) = stepThread thread1 + threads' = Map.insert (threadId thread') thread' threads + races' = updateRaces thread1 simstate in + + SimPORTrace time tid tstep tlbl (EventEffect vClock eff) . + SimPORTrace time tid tstep tlbl (EventRaces races') <$> reschedule simstate { threads = threads', - races = updateRacesInSimState thread1 simstate, + races = races', control = advanceControl (threadStepId thread1) control } -deschedule Terminated thread@Thread { threadId = tid, threadVClock = vClock, threadEffect = effect } +deschedule Terminated thread@Thread { threadId = tid, threadStep = tstep, threadLabel = tlbl, + threadVClock = vClock, threadEffect = effect } simstate@SimState{ curTime = time, control } = do -- This thread is done. If there are other threads blocked in a -- ThrowTo targeted at this thread then we can wake them up now. - let thread1 = thread - thread' = stepThread $ thread { threadStatus = ThreadDone } - wakeup = map (\(_,tid',_) -> l_labelled tid') (reverse (threadThrowTo thread)) + let wakeup = map (\(_,tid',_) -> l_labelled tid') (reverse (threadThrowTo thread)) (unblocked, simstate'@SimState{threads}) = unblockThreads False vClock wakeup simstate - threads' = Map.insert tid thread' threads + effect' = effect <> wakeupEffects unblocked + (thread', eff) = stepThread $ thread { threadStatus = ThreadDone, + threadEffect = effect' } + threads' = Map.insert tid thread' threads + races' = threadTerminatesRaces tid $ updateRaces thread { threadEffect = effect' } simstate -- We must keep terminated threads in the state to preserve their vector clocks, -- which matters when other threads throwTo them. - !trace <- reschedule simstate' { races = threadTerminatesRaces tid $ - updateRacesInSimState thread1 simstate, - control = advanceControl (threadStepId thread) control, - threads = threads' } + !trace <- reschedule simstate' { races = races', + control = advanceControl (threadStepId thread) control, + threads = threads' } return $ traceMany -- TODO: step [ (time, tid', (-1), tlbl', EventThrowToWakeup) | tid' <- unblocked , let tlbl' = lookupThreadLabel tid' threads ] - trace + $ SimPORTrace time tid tstep tlbl (EventEffect vClock eff) + $ SimPORTrace time tid tstep tlbl (EventRaces races') + trace -deschedule Sleep thread@Thread { threadId = tid , threadEffect = effect } +deschedule Sleep thread@Thread { threadId = tid , threadEffect = effect' } simstate@SimState{runqueue, threads} = -- Schedule control says we should run a different thread. Put @@ -921,13 +972,18 @@ reschedule :: SimState s a -> ST s (SimTrace a) -- If we are following a controlled schedule, just do that. -reschedule simstate@SimState{ runqueue, threads, - control=control@(ControlFollow ((tid,tstep):_) _), - curTime=time - } = +reschedule simstate@SimState { runqueue, control = control@(ControlFollow ((tid,_):_) _) } + | not (Down tid `PSQ.member` runqueue) = + return (Trace.Nil (InternalError ("assertion failure: " ++ ppIOSimThreadId tid ++ " not runnable"))) + +reschedule simstate@SimState { threads, control = control@(ControlFollow ((tid,_):_) _) } + | not (tid `Map.member` threads) = + return (Trace.Nil (InternalError ("assertion failure: " ++ ppIOSimThreadId tid ++ " not in threads"))) + +reschedule simstate@SimState { runqueue, threads, + control = control@(ControlFollow ((tid,tstep):_) _), + curTime = time } = fmap (SimPORTrace time tid tstep Nothing (EventReschedule control)) $ - assert (Down tid `PSQ.member` runqueue) $ - assert (tid `Map.member` threads) $ invariant Nothing simstate $ let thread = threads Map.! tid in assert (threadId thread == tid) $ @@ -971,6 +1027,10 @@ -- Reuse the STM functionality here to write all the timer TVars. -- Simplify to a special case that only reads and writes TVars. written <- execAtomically' (runSTM $ mapM_ timeoutAction fired) + !ds <- traverse (\(SomeTVar tvar) -> do + tr <- traceTVarST tvar False + !_ <- commitTVar tvar + return tr) written (wakeupSTM, wokeby) <- threadsUnblockedByWrites written mapM_ (\(SomeTVar tvar) -> unblockAllThreadsFromTVar tvar) written @@ -996,6 +1056,10 @@ ++ [ ( time', ThreadId [-1], -1, Just "register delay timer" , EventRegisterDelayFired tmid) | (tmid, TimerRegisterDelay _) <- zip tmids fired ] + ++ [ (time', ThreadId [-1], -1, Just "register delay timer", EventLog (toDyn a)) + | TraceValue { traceDynamic = Just a } <- ds ] + ++ [ (time', ThreadId [-1], -1, Just "register delay timer", EventSay a) + | TraceValue { traceString = Just a } <- ds ] ++ [ (time', tid', -1, tlbl', EventTxWakeup vids) | tid' <- wakeupSTM , let tlbl' = lookupThreadLabel tid' threads @@ -1021,15 +1085,15 @@ TimeoutFired -> error "MonadTimer(Sim): invariant violation" TimeoutCancelled -> return () timeoutAction (TimerRegisterDelay var) = writeTVar var True - timeoutAction (TimerThreadDelay _ _) = return () + timeoutAction (TimerThreadDelay _ _) = return () timeoutAction (TimerTimeout _ _ _) = return () unblockThreads :: forall s a. Bool -- ^ `True` if we are blocked on STM -> VectorClock - -> [ThreadId] + -> [IOSimThreadId] -> SimState s a - -> ([ThreadId], SimState s a) + -> ([IOSimThreadId], SimState s a) unblockThreads !onlySTM vClock wakeup simstate@SimState {runqueue, threads} = -- To preserve our invariants (that threadBlocked is correct) -- we update the runqueue and threads together here @@ -1046,17 +1110,18 @@ case Map.lookup tid threads of Just Thread { threadStatus = ThreadRunning } -> [ ] - Just t@Thread { threadStatus = ThreadBlocked BlockedOnOther } + Just t@Thread { threadStatus = ThreadBlocked BlockedOnSTM } + -> [t] + Just t@Thread { threadStatus = ThreadBlocked _ } | onlySTM -> [ ] | otherwise -> [t] - Just t@Thread { threadStatus = ThreadBlocked BlockedOnSTM } - -> [t] - _ -> [ ] + Just Thread { threadStatus = ThreadDone } -> [ ] + Nothing -> [ ] ] - unblockedIds :: [ThreadId] + unblockedIds :: [IOSimThreadId] !unblockedIds = map threadId unblocked -- and in which case we mark them as now running @@ -1083,7 +1148,7 @@ -- receive a 'ThreadKilled' exception. -- forkTimeoutInterruptThreads :: forall s a. - [(ThreadId, TimeoutId, TMVar (IOSim s) ThreadId)] + [(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)] -> SimState s a -> ST s (SimState s a) forkTimeoutInterruptThreads timeoutExpired simState = @@ -1103,13 +1168,13 @@ where -- we launch a thread responsible for throwing an AsyncCancelled exception -- to the thread which timeout expired - throwToThread :: [(Thread s a, TMVar (IOSim s) ThreadId)] + throwToThread :: [(Thread s a, TMVar (IOSim s) IOSimThreadId)] (simState', throwToThread) = List.mapAccumR fn simState timeoutExpired where fn :: SimState s a - -> (ThreadId, TimeoutId, TMVar (IOSim s) ThreadId) - -> (SimState s a, (Thread s a, TMVar (IOSim s) ThreadId)) + -> (IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId) + -> (SimState s a, (Thread s a, TMVar (IOSim s) IOSimThreadId)) fn state@SimState { threads } (tid, tmid, lock) = let t = case tid `Map.lookup` threads of Just t' -> t' @@ -1141,8 +1206,8 @@ , lock ) ) - + -- | Iterate through the control stack to find an enclosing exception handler -- of the right type, or unwind all the way to the top level for the thread. -- @@ -1226,13 +1291,13 @@ | p == p' -> collectAll (k:ks) p (x:xs) psq' _ -> (reverse ks, p, reverse xs, psq) -traceMany :: [(Time, ThreadId, Int, Maybe ThreadLabel, SimEventType)] +traceMany :: [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)] -> SimTrace a -> SimTrace a traceMany [] trace = trace traceMany ((time, tid, tstep, tlbl, event):ts) trace = SimPORTrace time tid tstep tlbl event (traceMany ts trace) -lookupThreadLabel :: ThreadId -> Map ThreadId (Thread s a) -> Maybe ThreadLabel +lookupThreadLabel :: IOSimThreadId -> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel lookupThreadLabel tid threads = join (threadLabel <$> Map.lookup tid threads) @@ -1247,10 +1312,10 @@ controlSimTraceST :: Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a) controlSimTraceST limit control mainAction = SimPORTrace (curTime initialState) - (threadId mainThread) - 0 - (threadLabel mainThread) - (EventSimStart control) + (threadId mainThread) + 0 + (threadLabel mainThread) + (EventSimStart control) <$> schedule mainThread initialState { control = control, control0 = control, perStepTimeLimit = limit @@ -1279,7 +1344,7 @@ execAtomically :: forall s a c. Time - -> ThreadId + -> IOSimThreadId -> Maybe ThreadLabel -> TVarId -> StmA s a @@ -1583,10 +1648,10 @@ -- Blocking and unblocking on TVars -- -readTVarBlockedThreads :: TVar s a -> ST s [ThreadId] +readTVarBlockedThreads :: TVar s a -> ST s [IOSimThreadId] readTVarBlockedThreads TVar{tvarBlocked} = fst <$> readSTRef tvarBlocked -blockThreadOnTVar :: ThreadId -> TVar s a -> ST s () +blockThreadOnTVar :: IOSimThreadId -> TVar s a -> ST s () blockThreadOnTVar tid TVar{tvarBlocked} = do (tids, tidsSet) <- readSTRef tvarBlocked when (tid `Set.notMember` tidsSet) $ do @@ -1605,7 +1670,7 @@ -- the var writes that woke them. -- threadsUnblockedByWrites :: [SomeTVar s] - -> ST s ([ThreadId], Map ThreadId (Set (Labelled TVarId))) + -> ST s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId))) threadsUnblockedByWrites written = do tidss <- sequence [ (,) <$> labelledTVarId tvar <*> readTVarBlockedThreads tvar @@ -1633,91 +1698,47 @@ -- Steps -- -data Step = Step { - stepThreadId :: !ThreadId, - stepStep :: !Int, - stepEffect :: !Effect, - stepVClock :: !VectorClock - } - deriving Show - --- steps race if they can be reordered with a possibly different outcome +-- | Check if two steps can be reordered with a possibly different outcome. +-- racingSteps :: Step -- ^ an earlier step -> Step -- ^ a later step -> Bool racingSteps s s' = - stepThreadId s /= stepThreadId s' + -- is s executed by a racy thread + isRacyThreadId (stepThreadId s) + -- steps which belong to the same thread cannot race + && stepThreadId s /= stepThreadId s' + -- if s wakes up s' then s and s' cannot race && not (stepThreadId s' `elem` effectWakeup (stepEffect s)) - && (stepEffect s `racingEffects` stepEffect s' - || throwsTo s s' - || throwsTo s' s) + -- s effects races with s' effects or either one throws to the other + && ( stepEffect s `racingEffects` stepEffect s' + || throwsTo s s' + || throwsTo s' s + ) where throwsTo s1 s2 = stepThreadId s2 `elem` effectThrows (stepEffect s1) + -- `throwTo` races with any other effect && stepEffect s2 /= mempty currentStep :: Thread s a -> Step -currentStep Thread { threadId = tid, - threadStep = tstep, - threadEffect = teffect, - threadVClock = vClock - } = - Step { stepThreadId = tid, - stepStep = tstep, - stepEffect = teffect, - stepVClock = vClock - } +currentStep Thread { threadId = stepThreadId, + threadStep = stepStep, + threadEffect = stepEffect, + threadVClock = stepVClock + } = Step {..} -stepThread :: Thread s a -> Thread s a +-- | Step a thread and return the previous `StepId` and its `Effect`. +-- +stepThread :: Thread s a -> (Thread s a, Effect) stepThread thread@Thread { threadId = tid, threadStep = tstep, threadVClock = vClock } = - thread { threadStep = tstep+1, - threadEffect = mempty, - threadVClock = insertVClock tid (tstep+1) vClock - } - --- As we run a simulation, we collect info about each previous step -data StepInfo = StepInfo { - stepInfoStep :: Step, - -- Control information when we reached this step - stepInfoControl :: ScheduleControl, - -- threads that are still concurrent with this step - stepInfoConcurrent :: Set ThreadId, - -- steps following this one that did not happen after it - -- (in reverse order) - stepInfoNonDep :: [Step], - -- later steps that race with this one - stepInfoRaces :: [Step] - } - deriving Show - --- --- Races --- - -data Races = Races { -- These steps may still race with future steps - activeRaces :: ![StepInfo], - -- These steps cannot be concurrent with future steps - completeRaces :: ![StepInfo] - } - deriving Show - -noRaces :: Races -noRaces = Races [] [] - -updateRacesInSimState :: Thread s a -> SimState s a -> Races -updateRacesInSimState thread SimState{ control, threads, races } = - traceRaces $ - updateRaces step - (isThreadBlocked thread) - control - (Map.keysSet (Map.filter (\t -> not (isThreadDone t) - && threadId t `Set.notMember` - effectForks (stepEffect step) - ) threads)) - races - where - step = currentStep thread + ( thread { threadStep = tstep+1, + threadEffect = mempty, + threadVClock = insertVClock tid (tstep+1) vClock + }, + threadEffect thread + ) -- | 'updateRaces' turns a current 'Step' into 'StepInfo', and updates all -- 'activeRaces'. @@ -1726,89 +1747,124 @@ -- concurrent set. When this becomes empty, a step can be retired into -- the "complete" category, but only if there are some steps racing -- with it. -updateRaces :: Step -> Bool -> ScheduleControl -> Set ThreadId -> Races -> Races -updateRaces newStep@Step{ stepThreadId = tid, stepEffect = newEffect } - blocking - control - newConcurrent0 - races@Races{ activeRaces } = +updateRaces :: Thread s a -> SimState s a -> Races +updateRaces thread@Thread { threadId = tid } + SimState{ control, threads, races = races@Races { activeRaces } } = + let + newStep@Step{ stepEffect = newEffect } = currentStep thread - let justBlocking :: Bool - justBlocking = blocking && onlyReadEffect newEffect + concurrent0 = + Map.keysSet (Map.filter (\t -> not (isThreadDone t) + && threadId t `Set.notMember` + effectForks newEffect + ) threads) - -- a new step cannot race with any threads that it just woke up - new :: [StepInfo] - !new | isNotRacyThreadId tid = [] -- non-racy threads do not race - | Set.null newConcurrent = [] -- cannot race with anything - | justBlocking = [] -- no need to defer a blocking transaction - | otherwise = - [StepInfo { stepInfoStep = newStep, - stepInfoControl = control, - stepInfoConcurrent = newConcurrent, - stepInfoNonDep = [], - stepInfoRaces = [] - }] - where - newConcurrent :: Set ThreadId - newConcurrent = foldr Set.delete newConcurrent0 (effectWakeup newEffect) + -- A new step to add to the `activeRaces` list. + newStepInfo :: Maybe StepInfo + !newStepInfo | isNotRacyThreadId tid = Nothing + -- non-racy threads do not race - activeRaces' :: [StepInfo] - !activeRaces' = - [ -- if this step depends on the previous step, or is not concurrent, + | Set.null concurrent = Nothing + -- cannot race with nothing + + | isBlocking = Nothing + -- no need to defer a blocking transaction + + | otherwise = + Just $! StepInfo { stepInfoStep = newStep, + stepInfoControl = control, + stepInfoConcurrent = concurrent, + stepInfoNonDep = [], + stepInfoRaces = [] + } + where + concurrent :: Set IOSimThreadId + concurrent = concurrent0 Set.\\ effectWakeup newEffect + + isBlocking :: Bool + isBlocking = isThreadBlocked thread && onlyReadEffect newEffect + + -- Used to update each `StepInfo` in `activeRaces`. + updateStepInfo :: StepInfo -> StepInfo + updateStepInfo stepInfo@StepInfo { stepInfoStep = step, + stepInfoConcurrent = concurrent, + stepInfoNonDep, + stepInfoRaces } = + -- if this step depends on the previous step, or is not concurrent, -- then any threads that it wakes up become non-concurrent also. - let !lessConcurrent = foldr Set.delete concurrent (effectWakeup newEffect) in - if tid `elem` concurrent then - let theseStepsRace = isRacyThreadId tid && racingSteps step newStep - happensBefore = step `happensBeforeStep` newStep - !nondep' | happensBefore = nondep - | otherwise = newStep : nondep - -- We will only record the first race with each thread---reversing - -- the first race makes the next race detectable. Thus we remove a - -- thread from the concurrent set after the first race. - concurrent' | happensBefore = Set.delete tid lessConcurrent - | theseStepsRace = Set.delete tid concurrent - | otherwise = concurrent - -- Here we record discovered races. - -- We only record a new race if we are following the default schedule, - -- to avoid finding the same race in different parts of the search space. - !stepRaces' | (control == ControlDefault || - control == ControlFollow [] []) && - theseStepsRace = newStep : stepRaces - | otherwise = stepRaces + let !lessConcurrent = concurrent Set.\\ effectWakeup newEffect in + if tid `notElem` concurrent + then stepInfo { stepInfoConcurrent = lessConcurrent } + + -- The core of IOSimPOR. Detect if `newStep` is racing with any + -- previous steps and update each `StepInfo`. + else let theseStepsRace = step `racingSteps` newStep + -- `step` happened before `newStep` (`newStep` happened after + -- `step`) + happensBefore = step `happensBeforeStep` newStep + -- `newStep` happens after any of the racing steps + afterRacingStep = any (`happensBeforeStep` newStep) stepInfoRaces + + -- We will only record the first race with each thread. + -- Reversing the first race makes the next race detectable. + -- Thus we remove a thread from the concurrent set after the + -- first race. + !concurrent' + | happensBefore = Set.delete tid lessConcurrent + | theseStepsRace = Set.delete tid concurrent + | afterRacingStep = Set.delete tid concurrent + | otherwise = concurrent + + !stepInfoNonDep' + -- `newStep` happened after `step` + | happensBefore = stepInfoNonDep + -- `newStep` did not happen after `step` + | otherwise = newStep : stepInfoNonDep + + -- Here we record discovered races. We only record a new + -- race if we are following the default schedule, to avoid + -- finding the same race in different parts of the search + -- space. + !stepInfoRaces' + | theseStepsRace && isDefaultSchedule control + = newStep : stepInfoRaces + | otherwise = stepInfoRaces + in stepInfo { stepInfoConcurrent = effectForks newEffect - `Set.union` concurrent', - stepInfoNonDep = nondep', - stepInfoRaces = stepRaces' + `Set.union` concurrent', + stepInfoNonDep = stepInfoNonDep', + stepInfoRaces = stepInfoRaces' } - else stepInfo { stepInfoConcurrent = lessConcurrent } + activeRaces' :: [StepInfo] + !activeRaces' = + case newStepInfo of + Nothing -> updateStepInfo <$> activeRaces + Just si -> si : (updateStepInfo <$> activeRaces) - | !stepInfo@StepInfo { stepInfoStep = step, - stepInfoConcurrent = concurrent, - stepInfoNonDep = nondep, - stepInfoRaces = stepRaces - } - <- activeRaces ] - in normalizeRaces $ races { activeRaces = new ++ activeRaces' } + in normalizeRaces races { activeRaces = activeRaces' } + +normalizeRaces :: Races -> Races +normalizeRaces Races{ activeRaces, completeRaces } = + let !activeRaces' = filter (not . null . stepInfoConcurrent) activeRaces + !completeRaces' = ( filter (not . null . stepInfoRaces) + . filter (null . stepInfoConcurrent) + $ activeRaces + ) + ++ completeRaces + in Races{ activeRaces = activeRaces', completeRaces = completeRaces' } + + -- When a thread terminates, we remove it from the concurrent thread -- sets of active races. - -threadTerminatesRaces :: ThreadId -> Races -> Races +threadTerminatesRaces :: IOSimThreadId -> Races -> Races threadTerminatesRaces tid races@Races{ activeRaces } = let activeRaces' = [ s{stepInfoConcurrent = Set.delete tid stepInfoConcurrent} | s@StepInfo{ stepInfoConcurrent } <- activeRaces ] in normalizeRaces $ races{ activeRaces = activeRaces' } -normalizeRaces :: Races -> Races -normalizeRaces Races{ activeRaces, completeRaces } = - let !activeRaces' = filter (not . null. stepInfoConcurrent) activeRaces - !completeRaces' = filter (not . null. stepInfoRaces) - (filter (null . stepInfoConcurrent) activeRaces) - ++ completeRaces - in Races{ activeRaces = activeRaces', completeRaces = completeRaces' } - -- We assume that steps do not race with later steps after a quiescent -- period. Quiescent periods end when simulated time advances, thus we -- are assuming here that all work is completed before a timer @@ -1822,12 +1878,7 @@ , not (null (stepInfoRaces s)) ] ++ completeRaces } -traceRaces :: Races -> Races -traceRaces r = r --- traceRaces r@Races{activeRaces,completeRaces} = --- Debug.trace ("Tracking "++show (length (concatMap stepInfoRaces activeRaces)) ++" races") r - -- -- Schedule control -- @@ -1878,7 +1929,7 @@ -- Schedule modifications -- -stepStepId :: Step -> (ThreadId, Int) +stepStepId :: Step -> (IOSimThreadId, Int) stepStepId Step{ stepThreadId = tid, stepStep = n } = (tid,n) stepInfoToScheduleMods :: StepInfo -> [ScheduleMod] @@ -1895,7 +1946,7 @@ { scheduleModTarget = stepStepId step , scheduleModControl = control , scheduleModInsertion = takeWhile (/=stepStepId step') - (map stepStepId (reverse nondep)) + (stepStepId `map` reverse nondep) ++ [stepStepId step'] -- It should be unnecessary to include the delayed -- step in the insertion, since the default @@ -1954,4 +2005,4 @@ "Extending "++show control, " with "++show m, " yields "++show control']) -} - control' + control' diff --git a/src/Control/Monad/IOSimPOR/QuickCheckUtils.hs b/src/Control/Monad/IOSimPOR/QuickCheckUtils.hs --- a/src/Control/Monad/IOSimPOR/QuickCheckUtils.hs +++ b/src/Control/Monad/IOSimPOR/QuickCheckUtils.hs @@ -1,32 +1,22 @@ +{-# LANGUAGE BangPatterns #-} + {-# OPTIONS_GHC -Wno-name-shadowing #-} module Control.Monad.IOSimPOR.QuickCheckUtils where -import Control.Parallel +import Control.Monad.ST.Lazy import Test.QuickCheck.Gen import Test.QuickCheck.Property --- Take the conjunction of several properties, in parallel This is a --- modification of code from Test.QuickCheck.Property, to run non-IO --- properties in parallel. It also takes care NOT to label its result --- as an IO property (using IORose), unless one of its arguments is --- itself an IO property. This is needed to permit parallel testing. -conjoinPar :: TestableNoCatch prop => [prop] -> Property -conjoinPar = conjoinSpeculate speculate - where - -- speculation tries to evaluate each Rose tree in parallel, to WHNF - -- This will not perform any IO, but should evaluate non-IO properties - -- completely. - speculate [] = [] - speculate (rose:roses) = roses' `par` rose' `pseq` (rose':roses') - where rose' = case rose of - MkRose result _ -> let ans = maybe True id $ ok result in ans `pseq` rose - IORose _ -> rose - roses' = speculate roses - -- We also need a version of conjoin that is sequential, but does not -- label its result as an IO property unless one of its arguments -- is. Consequently it does not catch exceptions in its arguments. + +conjoinNoCatchST :: TestableNoCatch prop => [ST s prop] -> ST s Property +conjoinNoCatchST sts = do + ps <- sequence sts + return $ conjoinNoCatch ps + conjoinNoCatch :: TestableNoCatch prop => [prop] -> Property conjoinNoCatch = conjoinSpeculate id @@ -65,17 +55,7 @@ classes = classes result ++ classes r, tables = tables result ++ tables r } --- |&&| is a replacement for .&&. that evaluates its arguments in --- parallel. |&&| does NOT label its result as an IO property, unless --- one of its arguments is--which .&&. does. This means that using --- .&&. inside an argument to conjoinPar limits parallelism, while --- |&&| does not. -infixr 1 |&&| - -(|&&|) :: TestableNoCatch prop => prop -> prop -> Property -p |&&| q = conjoinPar [p, q] - -- .&&| is a sequential, but parallelism-friendly version of .&&., that -- tests its arguments in sequence, but does not label its result as -- an IO property unless one of its arguments is. @@ -104,7 +84,7 @@ propertyNoCatch = MkProperty . return . MkProp . return instance TestableNoCatch Prop where - propertyNoCatch p = MkProperty . return $ p + propertyNoCatch = MkProperty . return instance TestableNoCatch prop => TestableNoCatch (Gen prop) where propertyNoCatch mp = MkProperty $ do p <- mp; unProperty (againNoCatch $ propertyNoCatch p) diff --git a/src/Control/Monad/IOSimPOR/Types.hs b/src/Control/Monad/IOSimPOR/Types.hs --- a/src/Control/Monad/IOSimPOR/Types.hs +++ b/src/Control/Monad/IOSimPOR/Types.hs @@ -1,4 +1,28 @@ -module Control.Monad.IOSimPOR.Types where +{-# LANGUAGE NamedFieldPuns #-} +module Control.Monad.IOSimPOR.Types + ( -- * Effects + Effect (..) + , readEffects + , writeEffects + , forkEffect + , throwToEffect + , wakeupEffects + , onlyReadEffect + , racingEffects + , ppEffect + -- * Schedules + , ScheduleControl (..) + , isDefaultSchedule + , ScheduleMod (..) + -- * Steps + , StepId + , ppStepId + , Step (..) + , StepInfo (..) + -- * Races + , Races (..) + , noRaces + ) where import qualified Data.List as List import Data.Set (Set) @@ -10,25 +34,41 @@ -- Effects -- --- | An `Effect` aggregates effects performed by a thread. Only used by --- *IOSimPOR*. +-- | An `Effect` aggregates effects performed by a thread in a given +-- execution step. Only used by *IOSimPOR*. -- data Effect = Effect { effectReads :: !(Set TVarId), effectWrites :: !(Set TVarId), - effectForks :: !(Set ThreadId), - effectThrows :: ![ThreadId], - effectWakeup :: ![ThreadId] + effectForks :: !(Set IOSimThreadId), + effectThrows :: ![IOSimThreadId], + effectWakeup :: !(Set IOSimThreadId) } - deriving (Eq, Show) + deriving (Show, Eq) +ppEffect :: Effect -> String +ppEffect Effect { effectReads, effectWrites, effectForks, effectThrows, effectWakeup } = + "Effect { " ++ + concat (List.intersperse ", " $ + [ "reads = " ++ show effectReads | not (null effectReads) ] + ++ [ "writes = " ++ show effectWrites | not (null effectWrites) ] + ++ [ "forks = " ++ ppList ppIOSimThreadId (Set.toList effectForks) | not (null effectForks) ] + ++ [ "throws = " ++ ppList ppIOSimThreadId effectThrows | not (null effectThrows) ] + ++ [ "wakeup = " ++ ppList ppIOSimThreadId (Set.toList effectWakeup) | not (null effectWakeup) ]) + ++ " }" + + instance Semigroup Effect where Effect r w s ts wu <> Effect r' w' s' ts' wu' = - Effect (r <> r') (w <> w') (s <> s') (ts ++ ts') (wu++wu') + Effect (r <> r') (w <> w') (s <> s') (ts ++ ts') (wu <> wu') instance Monoid Effect where - mempty = Effect Set.empty Set.empty Set.empty [] [] + mempty = Effect Set.empty Set.empty Set.empty [] Set.empty +-- +-- Effect smart constructors +-- + -- readEffect :: SomeTVar s -> Effect -- readEffect r = mempty{effectReads = Set.singleton $ someTvarId r } @@ -41,30 +81,154 @@ writeEffects :: [SomeTVar s] -> Effect writeEffects rs = mempty{effectWrites = Set.fromList (map someTvarId rs)} -forkEffect :: ThreadId -> Effect -forkEffect tid = mempty{effectForks = Set.singleton $ tid} +forkEffect :: IOSimThreadId -> Effect +forkEffect tid = mempty{effectForks = Set.singleton tid} -throwToEffect :: ThreadId -> Effect +throwToEffect :: IOSimThreadId -> Effect throwToEffect tid = mempty{ effectThrows = [tid] } -wakeupEffects :: [ThreadId] -> Effect -wakeupEffects tids = mempty{effectWakeup = tids} +wakeupEffects :: [IOSimThreadId] -> Effect +wakeupEffects tids = mempty{effectWakeup = Set.fromList tids} +-- +-- Utils +-- + someTvarId :: SomeTVar s -> TVarId someTvarId (SomeTVar r) = tvarId r onlyReadEffect :: Effect -> Bool onlyReadEffect e = e { effectReads = effectReads mempty } == mempty +-- | Check if two effects race. The two effects are assumed to come from +-- different threads, from steps which do not wake one another, see +-- `racingSteps`. +-- racingEffects :: Effect -> Effect -> Bool racingEffects e e' = - effectThrows e `intersectsL` effectThrows e' - || effectReads e `intersects` effectWrites e' - || effectWrites e `intersects` effectReads e' - || effectWrites e `intersects` effectWrites e' + + -- both effects throw to the same threads + effectThrows e `intersectsL` effectThrows e' + + -- concurrent reads & writes of the same TVars + || effectReads e `intersects` effectWrites e' + || effectWrites e `intersects` effectReads e' + + -- concurrent writes to the same TVars + || effectWrites e `intersects` effectWrites e' + where intersects :: Ord a => Set a -> Set a -> Bool intersects a b = not $ a `Set.disjoint` b intersectsL :: Eq a => [a] -> [a] -> Bool intersectsL a b = not $ null $ a `List.intersect` b + + +--- +--- Schedules +--- + +-- | Modified execution schedule. +-- +data ScheduleControl = ControlDefault + -- ^ default scheduling mode + | ControlAwait [ScheduleMod] + -- ^ if the current control is 'ControlAwait', the normal + -- scheduling will proceed, until the thread found in the + -- first 'ScheduleMod' reaches the given step. At this + -- point the thread is put to sleep, until after all the + -- steps are followed. + | ControlFollow [StepId] [ScheduleMod] + -- ^ follow the steps then continue with schedule + -- modifications. This control is set by 'followControl' + -- when 'controlTargets' returns true. + deriving (Eq, Ord, Show) + + +isDefaultSchedule :: ScheduleControl -> Bool +isDefaultSchedule ControlDefault = True +isDefaultSchedule (ControlFollow [] []) = True +isDefaultSchedule _ = False + +-- | A schedule modification inserted at given execution step. +-- +data ScheduleMod = ScheduleMod{ + -- | Step at which the 'ScheduleMod' is activated. + scheduleModTarget :: StepId, + -- | 'ScheduleControl' at the activation step. It is needed by + -- 'extendScheduleControl' when combining the discovered schedule with the + -- initial one. + scheduleModControl :: ScheduleControl, + -- | Series of steps which are executed at the target step. This *includes* + -- the target step, not necessarily as the last step. + scheduleModInsertion :: [StepId] + } + deriving (Eq, Ord) + + +instance Show ScheduleMod where + showsPrec d (ScheduleMod tgt ctrl insertion) = + showParen (d>10) $ + showString "ScheduleMod " . + showsPrec 11 tgt . + showString " " . + showsPrec 11 ctrl . + showString " " . + showsPrec 11 insertion + +-- +-- Steps +-- + +data Step = Step { + stepThreadId :: !IOSimThreadId, + stepStep :: !Int, + stepEffect :: !Effect, + stepVClock :: !VectorClock + } + deriving Show + + +-- +-- StepInfo +-- + +-- | As we execute a simulation, we collect information about each step. This +-- information is updated as the simulation evolves by +-- `Control.Monad.IOSimPOR.Types.updateRaces`. +-- +data StepInfo = StepInfo { + -- | Step that we want to reschedule to run after a step in `stepInfoRaces` + -- (there will be one schedule modification per step in + -- `stepInfoRaces`). + stepInfoStep :: !Step, + + -- | Control information when we reached this step. + stepInfoControl :: !ScheduleControl, + + -- | Threads that are still concurrent with this step. + stepInfoConcurrent :: !(Set IOSimThreadId), + + -- | Steps following this one that did not happen after it + -- (in reverse order). + stepInfoNonDep :: ![Step], + + -- | Later steps that race with `stepInfoStep`. + stepInfoRaces :: ![Step] + } + deriving Show + +-- +-- Races +-- + +data Races = Races { -- These steps may still race with future steps + activeRaces :: ![StepInfo], + -- These steps cannot be concurrent with future steps + completeRaces :: ![StepInfo] + } + deriving Show + +noRaces :: Races +noRaces = Races [] [] diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -11,7 +11,7 @@ tests :: TestTree tests = - testGroup "IO Sim" + testGroup "io-sim-tests" [ Test.Control.Concurrent.Class.MonadMVar.tests , Test.Control.Monad.IOSim.tests , Test.Control.Monad.IOSimPOR.tests diff --git a/test/Test/Control/Monad/IOSim.hs b/test/Test/Control/Monad/IOSim.hs --- a/test/Test/Control/Monad/IOSim.hs +++ b/test/Test/Control/Monad/IOSim.hs @@ -52,7 +52,7 @@ tests :: TestTree tests = - testGroup "IO simulator" + testGroup "IOSim" [ testProperty "read/write graph (IO)" prop_stm_graph_io , testProperty "read/write graph (IOSim)" (withMaxSuccess 1000 prop_stm_graph_sim) , testGroup "timeouts" diff --git a/test/Test/Control/Monad/IOSimPOR.hs b/test/Test/Control/Monad/IOSimPOR.hs --- a/test/Test/Control/Monad/IOSimPOR.hs +++ b/test/Test/Control/Monad/IOSimPOR.hs @@ -1,8 +1,9 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wno-unused-top-binds #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -10,24 +11,24 @@ module Test.Control.Monad.IOSimPOR (tests) where import Data.Fixed (Micro) -import Data.Foldable (foldl') +import Data.Foldable (foldl', traverse_) import Data.Functor (($>)) -import Data.IORef import qualified Data.List as List import Data.Map (Map) import qualified Data.Map as Map +import Data.STRef.Lazy import System.Exit import System.IO.Error (ioeGetErrorString, isUserError) -import System.IO.Unsafe import Control.Exception (ArithException (..), AsyncException) import Control.Monad import Control.Monad.Fix -import Control.Parallel +import Control.Monad.ST.Lazy (ST, runST) -import Control.Monad.Class.MonadFork import Control.Concurrent.Class.MonadSTM +import Control.Monad.Class.MonadAsync +import Control.Monad.Class.MonadFork import Control.Monad.Class.MonadSay import Control.Monad.Class.MonadTest import Control.Monad.Class.MonadThrow @@ -47,13 +48,21 @@ import Test.QuickCheck import Test.Tasty (TestTree, testGroup) import Test.Tasty.QuickCheck +import qualified Data.List.Trace as Trace tests :: TestTree tests = - testGroup "IO simulator POR" - [ testProperty "propSimulates" propSimulates - , testProperty "propExploration" propExploration - -- , testProperty "propPermutations" propPermutations + testGroup "IOSimPOR" + [ testGroup "schedule exploration" + [ testProperty "propSimulates" propSimulates + , testProperty "propExploration" propExploration + , testGroup "issue113" + [ testProperty "wakeup" unit_issue113_wakeup + , testProperty "racy" unit_issue113_racy + , testProperty "nonDep" unit_issue113_nonDep + ] + -- , testProperty "propPermutations" propPermutations + ] , testGroup "IO simulator properties" [ testProperty "read/write graph (IOSim)" (withMaxSuccess 1000 prop_stm_graph_sim) , testGroup "timeouts" @@ -256,39 +265,64 @@ sortTasks (x:xs) = (x:) <$> sortTasks xs sortTasks [] = [] -interpret :: forall s. TVar (IOSim s) Int -> TVar (IOSim s) [ThreadId (IOSim s)] -> Task -> IOSim s (ThreadId (IOSim s)) -interpret r t (Task steps) = forkIO $ do - context <- atomically $ do +data Compare = AreEqual | AreNotEqual + deriving Show + +instance Arbitrary Compare where + arbitrary = frequency [(8, pure AreEqual), + (2, pure AreNotEqual)] + + shrink AreEqual = [] + shrink AreNotEqual = [AreEqual] + + +interpret :: forall s. + Compare + -> TVar (IOSim s) Int + -> TVar (IOSim s) [ThreadId (IOSim s)] + -> (Int, Task) + -> IOSim s (Async (IOSim s) ()) +interpret cmp r t (tlbl, Task steps) = async $ do + labelThisThread (show tlbl) + (ts, timer) <- atomically $ do ts <- readTVar t - when (null ts) retry + check (not (null ts)) timer <- newTVar Nothing return (ts,timer) - mapM_ (interpretStep context) steps - where interpretStep _ (WhenSet m n) = atomically $ do - a <- readTVar r - when (a/=m) retry - writeTVar r n - interpretStep (ts,_) (ThrowTo i) = throwTo (ts !! i) (ExitFailure 0) - interpretStep _ (Delay i) = threadDelay (fromIntegral i) - interpretStep (_,timer) (Timeout tstep) = do - timerVal <- atomically $ readTVar timer - case (timerVal,tstep) of - (_,NewTimeout n) -> do tout <- newTimeout (fromIntegral n) - atomically $ writeTVar timer (Just tout) - (Just tout,CancelTimeout) -> cancelTimeout tout - (Just tout,AwaitTimeout) -> atomically $ awaitTimeout tout >> return () - (Nothing,_) -> return () + mapM_ (interpretStep ts timer) steps + where + compareFn = case cmp of + AreEqual -> (==) + AreNotEqual -> (/=) + interpretStep :: [ThreadId (IOSim s)] + -> TVar (IOSim s) (Maybe (Timeout s)) + -> Step + -> IOSim s () + interpretStep _ _ (WhenSet m n) = atomically $ do + readTVar r >>= check . compareFn m + writeTVar r n + interpretStep ts _ (ThrowTo i) = throwTo (ts !! i) (ExitFailure 0) + interpretStep _ _ (Delay i) = threadDelay (fromIntegral i) + interpretStep _ timer (Timeout tstep) = do + timerVal <- readTVarIO timer + case (timerVal,tstep) of + (_,NewTimeout n) -> do tout <- newTimeout (fromIntegral n) + atomically $ writeTVar timer (Just tout) + (Just tout,CancelTimeout) -> cancelTimeout tout + (Just tout,AwaitTimeout) -> atomically $ awaitTimeout tout >> return () + (Nothing,_) -> return () -runTasks :: [Task] -> IOSim s (Int,Int) -runTasks tasks = do +runTasks :: Compare -> [Task] -> IOSim s (Int,Int) +runTasks cmp tasks = do let m = maximum [maxTaskValue t | Task t <- tasks] - r <- atomically $ newTVar m - t <- atomically $ newTVar [] + r <- newTVarIO m + traceTVarIO r (\_ a -> return (TraceString (show a))) + t <- newTVarIO [] exploreRaces - ts <- mapM (interpret r t) tasks - atomically $ writeTVar t ts - threadDelay 1000000000 -- allow the SUT threads to run - a <- atomically $ readTVar r + ts <- mapM (interpret cmp r t) (zip [1..] tasks) + atomically $ writeTVar t (asyncThreadId <$> ts) + traverse_ wait ts -- allow the SUT threads to run + a <- readTVarIO r return (m,a) maxTaskValue :: [Step] -> Int @@ -296,100 +330,133 @@ maxTaskValue (_:t) = maxTaskValue t maxTaskValue [] = 0 -propSimulates :: Tasks -> Property -propSimulates (Tasks tasks) = +propSimulates :: Compare -> Shrink2 Tasks -> Property +propSimulates cmp (Shrink2 (Tasks tasks)) = any (not . null . (\(Task steps)->steps)) tasks ==> - let Right (m,a) = runSim (runTasks tasks) in - m>=a + let trace = runSimTrace (runTasks cmp tasks) in + case traceResult False trace of + Right (m,a) -> property (m >= a) + Left (FailureInternal msg) + -> counterexample msg False + Left x -> counterexample (ppTrace trace) + $ counterexample (show x) True -propExploration :: Tasks -> Property -propExploration (Tasks tasks) = - -- Debug.trace ("\nTasks:\n"++ show tasks) $ +-- NOTE: This property needs to be executed sequentially, otherwise it fails +-- undeterministically, which `exploreSimTraceST` does. +-- +propExploration :: Compare -> (Shrink2 Tasks) -> Property +propExploration cmp (Shrink2 ts@(Tasks tasks)) = any (not . null . (\(Task steps)->steps)) tasks ==> - traceNoDuplicates $ \addTrace -> - --traceCounter $ \addTrace -> - exploreSimTrace id (runTasks tasks) $ \_ trace -> - --Debug.trace (("\nTrace:\n"++) . splitTrace . noExceptions $ show trace) $ - addTrace trace $ - counterexample (splitTrace . noExceptions $ show trace) $ - case traceResult False trace of - Right (m,a) -> property $ m>=a - Left e -> counterexample (show e) False + runST $ + -- traceNoDuplicates $ \addTrace-> + exploreSimTraceST (\a -> a { explorationDebugLevel = 0 }) + (say (show ts) >> runTasks cmp tasks) + $ \_ trace -> do + -- addTrace trace + -- TODO: for now @coot is leaving `Trace.ppTrace`, but once we change all + -- assertions into `FailureInternal`, we can use `ppTrace` instead + return $ counterexample (Trace.ppTrace show (ppSimEvent 0 0 0) trace) $ + case traceResult False trace of + Right (m,a) -> property (m >= a) + Left (FailureInternal msg) + -> counterexample msg False + Left _ -> property True + +-- | This is a counterexample for a fix included in the commit: "io-sim-por: +-- fixed counterexample in issue #113". There was a missing wakeup effect when +-- a thread terminates, for threads that were blocked on `throwTo`. +-- +unit_issue113_wakeup :: Property +unit_issue113_wakeup = + propExploration AreEqual (Shrink2 tasks) + where + tasks = Tasks [Task [ThrowTo 1, WhenSet 0 0], + Task [Delay 1], + Task [WhenSet 0 0], + Task [WhenSet 1 0, ThrowTo 1]] + + +-- | This test checks that we don't build a schedule which execute a racing +-- step that depends on something that wasn't added to `stepInfoNonDep`. +-- +unit_issue113_racy :: Property +unit_issue113_racy = + propExploration AreNotEqual (Shrink2 tasks) + where + tasks = Tasks [Task [WhenSet 1 0,ThrowTo 1], + Task [], + Task [ThrowTo 1,WhenSet 0 0], + Task [ThrowTo 1]] + + +-- | This test checks that we don't build a schedule which execute a non +-- dependent step that depends on something that wasn't added to +-- `stepInfoNonDep`. +-- +unit_issue113_nonDep :: Property +unit_issue113_nonDep = + propExploration AreNotEqual (Shrink2 tasks) + where + tasks = Tasks [Task [WhenSet 0 0], + Task [], + Task [WhenSet 0 0], + Task [ThrowTo 1,WhenSet 1 1], + Task [ThrowTo 5], + Task [ThrowTo 1]] + + -- Testing propPermutations n should collect every permutation of [1..n] once only. -- Test manually, and supply a small value of n. propPermutations :: Int -> Property propPermutations n = + runST $ traceNoDuplicates $ \addTrace -> - exploreSimTrace (withScheduleBound 10000) (doit n) $ \_ trace -> - addTrace trace $ - let Right result = traceResult False trace in - tabulate "Result" [noExceptions $ show $ result] $ - True + exploreSimTraceST (withScheduleBound 10000) (doit n) $ \_ trace -> do + addTrace trace + let Right result = traceResult False trace + return $ tabulate "Result" [show $ result] $ True doit :: Int -> IOSim s [Int] doit n = do - r <- atomically $ newTVar [] - exploreRaces - mapM_ (\i -> forkIO $ atomically $ modifyTVar r (++[i])) [1..n] - threadDelay 1 - atomically $ readTVar r + r <- atomically $ newTVar [] + exploreRaces + mapM_ (\i -> forkIO $ atomically $ modifyTVar r (++[i])) [1..n] + threadDelay 1 + atomically $ readTVar r -ordered :: Ord a => [a] -> Bool -ordered xs = and (zipWith (<) xs (drop 1 xs)) -noExceptions :: [Char] -> [Char] -noExceptions xs = unsafePerformIO $ try (evaluate xs) >>= \case - Right [] -> return [] - Right (x:ys) -> return (x:noExceptions ys) - Left e -> return ("\n"++show (e :: SomeException)) +traceNoDuplicates :: forall s a prop. (Show a, Testable prop) + => ((a -> ST s ()) -> ST s prop) + -> ST s Property +traceNoDuplicates k = do + v <- newSTRef Map.empty :: ST s (STRef s (Map String Int)) + prop <- k (\a -> modifySTRef v (Map.insertWith (+) (show a) 1)) + m <- readSTRef v + return $ prop .&&. counterexample (show (Map.keys $ Map.filter (> 1) m)) (maximum m === 1) -splitTrace :: [Char] -> [Char] -splitTrace [] = [] -splitTrace (x:xs) | begins "(Trace" = "\n(" ++ splitTrace xs - | otherwise = x:splitTrace xs - where begins s = take (length s) (x:xs) == s -traceCounter :: (Testable prop1, Show a1) => ((a1 -> a2 -> a2) -> prop1) -> Property -traceCounter k = r `pseq` (k addTrace .&&. - tabulate "Trace repetitions" (map show $ traceCounts ()) True) - where - r = unsafePerformIO $ newIORef (Map.empty :: Map String Int) - addTrace t x = unsafePerformIO $ do - atomicModifyIORef r (\m->(Map.insertWith (+) (show t) 1 m,())) - return x - traceCounts () = unsafePerformIO $ Map.elems <$> readIORef r - -traceNoDuplicates :: (Testable prop1, Show a1) => ((a1 -> a2 -> a2) -> prop1) -> Property -traceNoDuplicates k = r `pseq` (k addTrace .&&. maximum (traceCounts ()) == 1) - where - r = unsafePerformIO $ newIORef (Map.empty :: Map String Int) - addTrace t x = unsafePerformIO $ do - atomicModifyIORef r (\m->(Map.insertWith (+) (show t) 1 m,())) - return x - traceCounts () = unsafePerformIO $ Map.elems <$> readIORef r - -- -- IOSim reused properties -- - -- -- Read/Write graph -- prop_stm_graph_sim :: TestThreadGraph -> Property prop_stm_graph_sim g = + runST $ traceNoDuplicates $ \addTrace -> - exploreSimTrace id (prop_stm_graph g) $ \_ trace -> - addTrace trace $ - counterexample (splitTrace . noExceptions $ show trace) $ - case traceResult False trace of - Right () -> property True - Left e -> counterexample (show e) False - -- TODO: Note that we do not use runSimStrictShutdown here to check - -- that all other threads finished, but perhaps we should and structure - -- the graph tests so that's the case. + exploreSimTraceST id (prop_stm_graph g) $ \_ trace -> do + addTrace trace + return $ counterexample (Trace.ppTrace show show trace) $ + case traceResult False trace of + Right () -> property True + Left e -> counterexample (show e) False + -- TODO: Note that we do not use runSimStrictShutdown here to check + -- that all other threads finished, but perhaps we should and structure + -- the graph tests so that's the case. prop_timers_ST :: TestMicro -> Property prop_timers_ST (TestMicro xs) =