io-sim 1.2.0.0 → 1.3.0.0

raw patch · 14 files changed

+1301/−701 lines, 14 filesdep −paralleldep ~basedep ~io-classesdep ~si-timersPVP ok

version bump matches the API change (PVP)

Dependencies removed: parallel

Dependency ranges changed: base, io-classes, si-timers, strict-stm

API changes (from Hackage documentation)

Files

• CHANGELOG.md +46/−4
• README.md +2/−0
• io-sim.cabal +9/−8
• src/Control/Monad/IOSim.hs +253/−151
• src/Control/Monad/IOSim/CommonTypes.hs +65/−9
• src/Control/Monad/IOSim/Internal.hs +47/−31
• src/Control/Monad/IOSim/InternalTypes.hs +3/−3
• src/Control/Monad/IOSim/Types.hs +220/−101
• src/Control/Monad/IOSimPOR/Internal.hs +287/−236
• src/Control/Monad/IOSimPOR/QuickCheckUtils.hs +10/−30
• src/Control/Monad/IOSimPOR/Types.hs +182/−18
• test/Main.hs +1/−1
• test/Test/Control/Monad/IOSim.hs +1/−1
• test/Test/Control/Monad/IOSimPOR.hs +175/−108

@@ -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

@@ -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

@@ -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

@@ -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+       -- <https://github.com/input-output-hk/io-sim/issues>.+     | 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 [ "<<evaluation error: "+             , displayException  err+             , ">>"+             ]+    displayException (FailureInternal msg) =+      concat [ "<<internal failure: "+             , msg+             , ">>\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<n `mod` k then 1 else 0+      [ n `div` k + if i < n `mod` k then 1 else 0       | i <- [0..k-1] ] -    showThread :: (ThreadId,Maybe ThreadLabel) -> 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

@@ -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)) ++ "]"

@@ -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

@@ -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.

@@ -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 -> "<<io-sim-por: step execution exceded explorationStepTimelimit>>"+    InternalError e -> "<<io-sim internal error: " ++ show 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

@@ -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'

@@ -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)

@@ -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 [] []

@@ -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

@@ -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"

@@ -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) =