diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,4 +1,18 @@ -# Revsion history of io-sim +# Revision history of io-sim + +## 1.5.0.0 + +### Breaking changes + +- Generalised the type of `traceSelectTraceEvents` & co. + +### Non-breaking changes + +- Added `writeTMVar` to `MonadSTM` instance for `(IOSim s)`. +- Fixes IOSimPOR test failure (see issue #154). +- Reverted commit 4534b6eae64072a87bd81584f479a123681358a3 which uses + `unsafePerformIO` instead of ST, to regain lazyness on infinite simulations. +- Added a test to check for lazyness on infinite simulations ## 1.4.1.0 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.4.1.0 +version: 1.5.0.0 synopsis: A pure simulator for monadic concurrency with STM. description: A pure simulator monad with support of concurency (base & async style), 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, 9.8 } +tested-with: GHC == { 8.10, 9.2, 9.4, 9.6, 9.8, 9.10 } flag asserts description: Enable assertions @@ -75,19 +75,20 @@ RankNTypes, ScopedTypeVariables, TypeFamilies - build-depends: base >=4.9 && <4.20, - io-classes ^>=1.4.1, + build-depends: base >=4.9 && <4.21, + io-classes ^>=1.5, exceptions >=0.10, containers, deepseq, nothunks, - primitive >=0.7 && <0.10, + primitive >=0.7 && <0.11, psqueues >=0.2 && <0.3, - strict-stm ^>=1.4, - si-timers ^>=1.4, + strict-stm ^>=1.5, + si-timers ^>=1.5, time >=1.9.1 && <1.13, quiet, QuickCheck, + parallel if flag(asserts) @@ -130,7 +131,7 @@ default-language: Haskell2010 default-extensions: ImportQualifiedPost build-depends: base, - criterion, + criterion ^>= 1.6, io-classes, io-sim, 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,15 +1,11 @@ -{-# LANGUAGE BangPatterns #-} {-# LANGUAGE ExplicitNamespaces #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} - +{-# LANGUAGE QuantifiedConstraints #-} module Control.Monad.IOSim ( -- * Simulation monad IOSim @@ -28,9 +24,7 @@ -- ** Explore races using /IOSimPOR/ -- $iosimpor , exploreSimTrace - , exploreSimTraceST , controlSimTrace - , controlSimTraceST , ScheduleMod (..) , ScheduleControl (..) -- *** Exploration options @@ -99,22 +93,17 @@ import Prelude import Data.Bifoldable -import Data.Bifunctor (first) import Data.Dynamic (fromDynamic) -import Data.Functor (void) import Data.List (intercalate) -import Data.Maybe (catMaybes) import Data.Set (Set) import Data.Set qualified as Set import Data.Typeable (Typeable) import Data.List.Trace (Trace (..)) -import Data.List.Trace qualified as Trace import Control.Exception (throw) import Control.Monad.ST.Lazy -import Data.STRef.Lazy import Control.Monad.Class.MonadThrow as MonadThrow @@ -127,10 +116,13 @@ import Test.QuickCheck.Gen.Unsafe (Capture (..), capture) import Test.QuickCheck.Monadic (PropertyM, monadic') -import Debug.Trace qualified as Debug import System.IO.Unsafe +import Data.Functor (void) +import Data.IORef +import Debug.Trace qualified as Debug + -- | Select events according to the predicate function. It throws an error if -- the simulation ends with 'Failure'. -- @@ -187,38 +179,29 @@ -- unsafe, of course, since that function may return different results -- at different times. --- | Detach discovered races. This is written in `ST` monad to support --- simulations which do not terminate, in which case we will only detach races --- up to the point we evaluated the simulation. --- -detachTraceRacesST :: forall a s. SimTrace a -> ST s (ST s [ScheduleControl], SimTrace a) -detachTraceRacesST 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 +detachTraceRaces :: forall a. Int -> SimTrace a -> (() -> [ScheduleControl], SimTrace a) +detachTraceRaces debugLevel trace = unsafePerformIO $ do + races <- newIORef [] + let readRaces :: () -> [ScheduleControl] + readRaces () = concat . reverse . unsafePerformIO $ readIORef races - trace <- go trace0 - return (readRaces, trace) + saveRaces :: [ScheduleControl] -> x -> x + saveRaces rs t = unsafePerformIO $ modifyIORef races (rs:) + >> return t + go :: SimTrace a -> SimTrace a + go (SimTrace a b c d trace) = traceDebugLog debugLevel (Left (SimEvent a b c d)) + $ SimTrace a b c d $ go trace + go (SimPORTrace a b c d e trace) = traceDebugLog debugLevel (Left (SimPOREvent a b c d e)) + $ SimPORTrace a b c d e $ go trace + go (TraceRacesFound rs trace) = traceDebugLog debugLevel (Left (SimRacesFound rs)) + $ saveRaces rs $ go trace + go (Cons a as) = traceDebugLog debugLevel (Left a) + $ Cons a (go as) + go (Nil a) = traceDebugLog debugLevel (Right a) + $ Nil a --- | 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) + return (readRaces, go trace) -- | Select all the traced values matching the expected type. It relies on the -- sim's dynamic trace facility. @@ -313,8 +296,8 @@ -- traceSelectTraceEvents :: (Time -> SimEventType -> Maybe b) - -> SimTrace a - -> Trace (SimResult a) b + -> Trace a SimEvent + -> Trace a b traceSelectTraceEvents fn = bifoldr ( \ v _acc -> Nil v ) ( \ eventCtx acc -> case eventCtx of @@ -333,7 +316,8 @@ -- | Select dynamic events. It is a /total function/. -- traceSelectTraceEventsDynamic :: forall a b. Typeable b - => SimTrace a -> Trace (SimResult a) b + => Trace a SimEvent + -> Trace a b traceSelectTraceEventsDynamic = traceSelectTraceEvents fn where fn :: Time -> SimEventType -> Maybe b @@ -343,7 +327,7 @@ -- | Select say events. It is a /total function/. -- -traceSelectTraceEventsSay :: forall a. SimTrace a -> Trace (SimResult a) String +traceSelectTraceEventsSay :: forall a. Trace a SimEvent -> Trace a String traceSelectTraceEventsSay = traceSelectTraceEvents fn where fn :: Time -> SimEventType -> Maybe String @@ -531,77 +515,57 @@ -- ^ a callback which receives the previous trace (e.g. before reverting -- a race condition) and current trace -> Property -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. --- -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 +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) where opts = optsf stdExplorationOptions - 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) ] - ] + explore :: Int -- schedule bound + -> Int -- branching factor + -> 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 (explorationDebugLevel opts) + $ 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) ] + bucket :: Int -> String bucket n | n<10 = show n | otherwise = buck n 1 @@ -619,42 +583,69 @@ ppIOSimThreadId tid ++ (case lab of Nothing -> "" Just l -> " ("++l++")") + -- cache of explored schedules + cache :: IORef (Set ScheduleControl) + cache = unsafePerformIO cacheIO + -- insert a schedule into the cache - 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 + 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 + -- - -- Caching in ST monad + -- Caching in IO monad -- -- It is possible for the same control to be generated several times. -- To avoid exploring them twice, we keep a cache of explored schedules. - createCacheST :: ST s (STRef s (Set ScheduleControl)) - createCacheST = newSTRef $ + cacheIO :: IO (IORef (Set ScheduleControl)) + cacheIO = newIORef $ -- 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" - cacheSizeST :: STRef s (Set ScheduleControl) -> ST s Int - cacheSizeST = fmap Set.size . readSTRef + 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 + -- | Trace `SimTrace` to `stderr`. -- -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) +-- An internal function. +-- +traceDebugLog :: Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a +traceDebugLog logLevel _event trace | logLevel <= 0 = trace +-- Discard races if log level is 1 +traceDebugLog 1 (Left SimPOREvent { seType = EventRaces {} }) trace = trace +traceDebugLog 1 (Left event) trace = Debug.trace (ppSimEvent 0 0 0 event) trace +traceDebugLog 1 (Right event) trace = Debug.trace (ppSimResult 0 0 0 (void event)) trace +-- Otherwise, show races +traceDebugLog _ (Left event) trace = Debug.trace (ppSimEvent 0 0 0 event) trace +traceDebugLog _ (Right event) trace = Debug.trace (ppSimResult 0 0 0 (void event)) trace +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 (explorationDebugLevel opts) $ + controlSimTrace (explorationStepTimelimit opts) control mainAction + in property (k trace) -- | Run a simulation using a given schedule. This is useful to reproduce -- failing cases without exploring the races. @@ -671,22 +662,12 @@ -- ^ a simulation to run -> SimTrace a 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 - + runST (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 @@ -702,62 +683,41 @@ -- this far, then we collect its identity only if it is reached using -- `unsafePerformIO`. --- TODO: return StepId -compareTracesST :: forall a b s. - Maybe (SimTrace a) -- ^ passing - -> SimTrace b -- ^ failing - -> ST s ( ST s (Maybe ( (Time, IOSimThreadId, Maybe ThreadLabel) - , Set.Set (IOSimThreadId, Maybe ThreadLabel) - )) - , SimTrace b - ) -compareTracesST 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') +compareTraces :: Maybe (SimTrace a1) + -> SimTrace a2 + -> (Maybe ((Time, IOSimThreadId, Maybe ThreadLabel), + Set.Set (IOSimThreadId, 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') (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 = 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 + $ 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 - 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 = - 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 + 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 -- -- QuickCheck monadic combinators 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 @@ -16,7 +16,7 @@ {-# LANGUAGE TypeFamilies #-} -- Needed for `SimEvent` type. -{-# OPTIONS_GHC -Wno-partial-fields #-} +{-# OPTIONS_GHC -Wno-partial-fields #-} module Control.Monad.IOSim.Types ( IOSim (..) @@ -75,8 +75,8 @@ ) where import Control.Applicative -import Control.Exception (ErrorCall (..), asyncExceptionFromException, - asyncExceptionToException) +import Control.Exception (ErrorCall (..)) +import Control.Exception qualified as IO import Control.Monad import Control.Monad.Fix (MonadFix (..)) @@ -340,6 +340,9 @@ instance MonadThrow (IOSim s) where throwIO e = IOSim $ oneShot $ \_ -> Throw (toException e) +#if __GLASGOW_HASKELL__ >= 910 + annotateIO ann io = io `catch` \e -> throwIO (IO.addExceptionContext ann e) +#endif instance MonadEvaluate (IOSim s) where evaluate a = IOSim $ oneShot $ \k -> Evaluate a k @@ -354,6 +357,9 @@ instance MonadThrow (STM s) where throwIO e = STM $ oneShot $ \_ -> ThrowStm (toException e) +#if __GLASGOW_HASKELL__ >= 910 + annotateIO ann io = io `catch` \e -> throwIO (IO.addExceptionContext ann e) +#endif -- Since these involve re-throwing the exception and we don't provide -- CatchSTM at all, then we can get away with trivial versions: @@ -516,6 +522,7 @@ readTMVar = MonadSTM.readTMVarDefault tryReadTMVar = MonadSTM.tryReadTMVarDefault swapTMVar = MonadSTM.swapTMVarDefault + writeTMVar = MonadSTM.writeTMVarDefault isEmptyTMVar = MonadSTM.isEmptyTMVarDefault newTQueue = newTQueueDefault @@ -644,8 +651,7 @@ primitive st = IOSim $ oneShot $ \k -> LiftST (Prim.primitive st) k instance MonadST (IOSim s) where - stToIO f = IOSim $ oneShot $ \k -> LiftST f k - withLiftST f = f liftST + stToIO = liftST -- | Lift an 'StrictST.ST' computation to 'IOSim'. -- @@ -742,8 +748,8 @@ show (TimeoutException tmid) = "<>" instance Exception TimeoutException where - toException = asyncExceptionToException - fromException = asyncExceptionFromException + toException = IO.asyncExceptionToException + fromException = IO.asyncExceptionFromException -- | Wrapper for Eventlog events so they can be retrieved from the trace with -- 'selectTraceEventsDynamic'. 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 @@ -1771,17 +1771,27 @@ 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 = concurrent Set.\\ effectWakeup newEffect in + let !lessConcurrent = concurrent Set.\\ effectWakeup newEffect + -- `step` happened before `newStep` (`newStep` happened after + -- `step`) + happensBefore = step `happensBeforeStep` newStep + + !stepInfoNonDep' + -- `newStep` happened after `step` + | happensBefore = stepInfoNonDep + -- `newStep` did not happen after `step` + | otherwise = newStep : stepInfoNonDep in + if tid `notElem` concurrent - then stepInfo { stepInfoConcurrent = lessConcurrent } + then let + in stepInfo { stepInfoConcurrent = lessConcurrent + , stepInfoNonDep = stepInfoNonDep' + } -- 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 @@ -1794,12 +1804,6 @@ | 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 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 @@ -4,19 +4,32 @@ module Control.Monad.IOSimPOR.QuickCheckUtils where -import Control.Monad.ST.Lazy +import Control.Parallel 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 _ -> (case ok result of { Nothing -> (); Just !_ -> (); }) + `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 @@ -84,7 +97,7 @@ propertyNoCatch = MkProperty . return . MkProp . return instance TestableNoCatch Prop where - propertyNoCatch = MkProperty . return + propertyNoCatch p = MkProperty . return $ p instance TestableNoCatch prop => TestableNoCatch (Gen prop) where propertyNoCatch mp = MkProperty $ do p <- mp; unProperty (againNoCatch $ propertyNoCatch p) diff --git a/src/Data/Deque/Strict.hs b/src/Data/Deque/Strict.hs --- a/src/Data/Deque/Strict.hs +++ b/src/Data/Deque/Strict.hs @@ -1,10 +1,15 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE LambdaCase #-} -- | A minimal implementation of a strict deque. -- module Data.Deque.Strict where +#if __GLASGOW_HASKELL__ >= 910 +import Data.Foldable (foldr') +#else import Data.Foldable (foldl', foldr') +#endif import Data.List qualified as List import Prelude hiding (head, init, tail) diff --git a/src/Data/List/Trace.hs b/src/Data/List/Trace.hs --- a/src/Data/List/Trace.hs +++ b/src/Data/List/Trace.hs @@ -10,9 +10,14 @@ , tail , filter , length + , take + , takeWhile + , drop + , dropWhile ) where -import Prelude hiding (filter, head, length, tail) +import Prelude hiding (drop, dropWhile, filter, head, length, tail, take, + takeWhile) import Control.Applicative (Alternative (..)) import Control.Monad (MonadPlus (..)) @@ -64,6 +69,32 @@ ppTrace :: (a -> String) -> (b -> String) -> Trace a b -> String ppTrace sa sb (Cons b bs) = sb b ++ "\n" ++ ppTrace sa sb bs ppTrace sa _sb (Nil a) = sa a + +-- | Take the first n elements of a Trace, converting each to (). +take :: Int -> Trace a b -> Trace (Maybe a) b +take n _ | n <= 0 = Nil Nothing +take _ (Nil a) = Nil (Just a) +take n (Cons b o) = Cons b (take (n - 1) o) + +-- | Take elements from the Trace while the predicate holds, converting each to (). +takeWhile :: (b -> Bool) -> Trace a b -> Trace (Maybe a) b +takeWhile _ (Nil a) = Nil (Just a) +takeWhile p (Cons b o) + | p b = Cons b (takeWhile p o) + | otherwise = Nil Nothing + +-- | Drop the first n elements of a Trace. +drop :: Int -> Trace a b -> Trace a b +drop n o | n <= 0 = o +drop _ (Nil a) = Nil a +drop n (Cons _ o) = drop (n - 1) o + +-- | Drop elements from the Trace while the predicate holds. +dropWhile :: (b -> Bool) -> Trace a b -> Trace a b +dropWhile _ o@Nil {} = o +dropWhile p o@(Cons b o') + | p b = dropWhile p o' + | otherwise = o instance Bifunctor Trace where bimap f g (Cons b bs) = Cons (g b) (bimap f g bs) 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 @@ -24,7 +24,9 @@ import Data.Either (isLeft) import Data.Fixed (Micro) +#if __GLASGOW_HASKELL__ < 910 import Data.Foldable (foldl') +#endif import Data.Functor (($>)) import Data.Time.Clock (picosecondsToDiffTime) 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,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} @@ -11,12 +12,15 @@ module Test.Control.Monad.IOSimPOR (tests) where import Data.Fixed (Micro) +#if __GLASGOW_HASKELL__ >= 910 +import Data.Foldable (traverse_) +#else import Data.Foldable (foldl', traverse_) +#endif import Data.Functor (($>)) import Data.List qualified as List import Data.Map (Map) import Data.Map qualified as Map -import Data.STRef.Lazy import System.Exit import System.IO.Error (ioeGetErrorString, isUserError) @@ -24,7 +28,6 @@ import Control.Exception (ArithException (..), AsyncException) import Control.Monad import Control.Monad.Fix -import Control.Monad.ST.Lazy (ST, runST) import Control.Concurrent.Class.MonadSTM import Control.Monad.Class.MonadAsync @@ -49,6 +52,13 @@ import Test.Tasty (TestTree, testGroup) import Test.Tasty.QuickCheck +import System.IO.Unsafe + +import Data.IORef +import Data.Time (secondsToDiffTime) +import Data.Void (Void) +import GHC.Conc (pseq) + tests :: TestTree tests = testGroup "IOSimPOR" @@ -72,6 +82,7 @@ , testProperty "stacked timeouts" prop_stacked_timeouts , testProperty "{register,thread}Delay" unit_registerDelay_threadDelay ] + , testProperty "infinite simulation" prop_explore_endless_simulation , testProperty "threadId order (IOSim)" (withMaxSuccess 1000 prop_threadId_order_order_Sim) , testProperty "forkIO order (IOSim)" (withMaxSuccess 1000 prop_fork_order_ST) , testGroup "throw/catch unit tests" @@ -344,18 +355,17 @@ -- NOTE: This property needs to be executed sequentially, otherwise it fails -- undeterministically, which `exploreSimTraceST` does. -- -propExploration :: Compare -> (Shrink2 Tasks) -> Property +propExploration :: Compare -> Shrink2 Tasks -> Property propExploration cmp (Shrink2 ts@(Tasks tasks)) = - any (not . null . (\(Task steps)->steps)) tasks ==> - runST $ - -- traceNoDuplicates $ \addTrace-> - exploreSimTraceST (\a -> a { explorationDebugLevel = 0 }) - (say (show ts) >> runTasks cmp tasks) - $ \_ trace -> do - -- addTrace trace + not (all (null . (\(Task steps)->steps)) tasks) ==> + traceNoDuplicates $ \addTrace-> + exploreSimTrace (\a -> a { explorationDebugLevel = 0 }) + (say (show ts) >> runTasks cmp tasks) + $ \_ trace -> + 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) $ + counterexample (Trace.ppTrace show (ppSimEvent 0 0 0) trace) $ case traceResult False trace of Right (m,a) -> property (m >= a) Left (FailureInternal msg) @@ -410,32 +420,66 @@ -- Test manually, and supply a small value of n. propPermutations :: Int -> Property propPermutations n = - runST $ traceNoDuplicates $ \addTrace -> - exploreSimTraceST (withScheduleBound 10000) (doit n) $ \_ trace -> do - addTrace trace + exploreSimTrace (withScheduleBound 10000) (doit n) $ \_ trace -> + addTrace trace $ let Right result = traceResult False trace - return $ tabulate "Result" [show $ result] $ True + in tabulate "Result" [show result] True doit :: Int -> IOSim s [Int] doit n = do - r <- atomically $ newTVar [] + r <- newTVarIO [] exploreRaces mapM_ (\i -> forkIO $ atomically $ modifyTVar r (++[i])) [1..n] threadDelay 1 - atomically $ readTVar r + readTVarIO r -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) +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 +-- | Checks that IOSimPOR is capable of analysing an infinite simulation +-- lazily. +-- +-- If the test fails with "outer timeout" error it means that 'exploreSimTrace' +-- is not lazy and there's something wrong with IOSimPOR implementation and +-- the trace is being forced way too soon. If, on the other hand, this property +-- fails with "inner timeout" error, it means that 'exploreSimTrace' is somewhat +-- lazy, however the trace is not being lazily generated. +-- +-- +prop_explore_endless_simulation :: Positive (Small Integer) -> Property +prop_explore_endless_simulation (Positive (Small finalTime)) = + counterexample "outer timeout" + $ label (show (secondsToDiffTime finalTime)) + $ within 15000000 -- 15 seconds + $ exploreSimTrace + id sim $ \_ trace -> do + let l = takeWhile (\(t, _, _, _) -> t < Time (secondsToDiffTime finalTime)) + . traceEvents + $ trace + in ioProperty $ do + r <- timeout 10 $ evaluate (foldl' (flip seq) True l) + case r of + Nothing -> return $ counterexample "inner timeout" False + Just _ -> return (property True) + where + thread :: forall s. IOSim s Void + thread = do + threadDelay 1 + thread + sim :: forall s. IOSim s Void + sim = do + exploreRaces + withAsync thread wait + -- -- IOSim reused properties -- @@ -446,11 +490,10 @@ prop_stm_graph_sim :: TestThreadGraph -> Property prop_stm_graph_sim g = - runST $ traceNoDuplicates $ \addTrace -> - exploreSimTraceST id (prop_stm_graph g) $ \_ trace -> do + exploreSimTrace id (prop_stm_graph g) $ \_ trace -> do addTrace trace - return $ counterexample (Trace.ppTrace show show trace) $ + $ counterexample (Trace.ppTrace show show trace) $ case traceResult False trace of Right () -> property True Left e -> counterexample (show e) False @@ -498,7 +541,7 @@ Left e -> counterexample (show e) False where factorial :: (Int -> Int) -> Int -> Int - factorial = \rec_ k -> if k <= 1 then 1 else k * rec_ (k - 1) + factorial rec_ k = if k <= 1 then 1 else k * rec_ (k - 1) prop_mfix_purity_2 :: [Positive Int] -> Property prop_mfix_purity_2 as =