diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,99 @@ # Revision history of io-sim +## 1.10.1.0 + +### Non-breaking changes + +* Added `IOSimPOR` `QuickCheck` combinators: + * `monadicIOSimPOR_` + * `monadicIOSimPOR` + * `runIOSimPORGen` +* Support ghc-9.14 +* Support QuickCheck-2.18.0.0 + +## 1.10.0.0 + +### Breaking changes + +* Added `EventEvaluationError`, `EventEvaluationSuccess` +* Added `EventSayEvaluationError`, `EventLogEvaluationError` +* Added `flushEventLog` to `MonadEventLog` instance. + +### Non-breaking changes + +* `ppSimEventType` (used by `Control.Monad.IOSim.ppTrace` and + `Control.Monad.IOSim.ppTrace_`): does not fail if `EventThrow` or + `EventThrowTo` contain a pure exception. This supports laziness of `throwIO` + and `throwTo`. +* `say`, `traceM` and `traceSTM` evaluate their arguments (first one to _NF_ + the other two to _WHNF_). They throw an exception (within the simulator) if + evaluation fails. For `say` this makes it behave like `putStrLn` does. + Previously all would throw a pure exception which would terminate the + simulator prematurely. If you want to verify that these calls do not fail, + you can check for absence of `EventSayEvaluationError` or + `EventLogEvaluationError`. +* Added `Data.List.Trace.last` +* Although `IOSim` and `IOSimPOR` are pure we use `evaluate` in a few places, + none of them now catch asynchronous exceptions. +* Added `IOSimPOR` QuickCheck monadic combinators: + `monadicIOSimPOR`, `monadicIOSimPOR_` and `runIOSimPORGen`. + +## 1.9.1.0 + +### Non-breaking changes + +* Reverted rounding of `si-timers` API to microsecond to match `IO` behaviour. + It may cause surprising issues downstream when time is not advancing as + expected because of rounding to `0`. + +## 1.9.0.0 + +The version is bumped to `1.9` in sync with `io-classes-1.9`. + +### Non-breaking changes + +* Added support for unique symbol generation à la `Data.Unique`. +* Removed a misleading internal comment. +* Fixed error handling in `traceResult` so one can combine it (or ather APIs + which are based on it: `runSim`, `runSimOrThrow`, or `runSimStrictShutdown`) + with `within` or `discardAfter` from `QuickCheck`. See the test suite how to + use `discardAfter` with `IOSim`. +* Round `si-timers` API (`MonadDelay`, `MonadTimer`) to microsecond to match + `IO` behaviour. + +## 1.8.0.1 + +* Added support for `ghc-9.2`. + +## 1.8.0.0 + +- Provided `MonadTraceMVar` +- Renamed `InspectMonad` to `InspectMonadSTM` +- Support `threadLabel` (`io-classes-1.8`) +- `IOSimPOR`'s `Effect` traces now will correctly show labels on read/written + `TVars`. +- `Show` instance for `ScheduleMod` now prints `ThreadId`s in a slightly nicer + way, matching the way those steps would be traced in the `SimTrace`. +- Implement `MonadLabelledMVar` instance for `(IOSim s)` +- `TVarId` is now a sum type with one constructor per `TVar` role, e.g. `TVar`, + `TMVar`, `MVar` and a few others - except for `TChan`. +- A blocked `takeTVar` is now safe in the presence of exceptions. It will relay + the value to other waiting threads. +- Faster handling of timeouts and timers by using a more efficient + internal representation. +- The signature of: + - `selectTraceEvents'`, + - `selectTraceEventsDynamic'`, + - `selectTraceEventsDynamicWithTime'`, + - `selectTraceEventsSay'` and + - `selectTraceEventsSayWithTime'` + is more general. These functions now accepts trace with any result, rather + than one that finishes with `SimResult`. +- More polymorphic `ppTrace_` type signature. +- Fixed `tryReadTBQueue` when returning `Nothing`. +- Support ghc 9.12 +- Export `Time` from `Control.Monad.IOSim`. + ## 1.6.0.0 - Upgraded to `io-classes-1.6.0.0` diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# [IO Simulator Monad][`io-sim`]: `io-sim` +# [IO Simulator Monad][`io-sim`]: `io-sim` package A pure simulator monad built on top of the lazy `ST` monad which supports: @@ -40,8 +40,18 @@ also the other way around: that `GHC`s `STM` implementation meets the specification. +## Supporting material + +* [Philipp Kant (@kantp) at Bobconf 2022][bob-conf] +* [Armando Santos (@bolt12) at ZuriHac 2022][zuriHac-2022] +* [Marcin Szamotulski (@coot) IOSim and Partial Order Reduction][io-sim-por-presentation] + [`io-sim`]: https://hackage.haskell.org/package/io-sim [`io-classes`]: https://input-output-hk.github.io/io-sim/io-classes/index.html [`si-timers`]: https://input-output-hk.github.io/io-sim/io-classes/si-timers/index.html [`IOSimPOR`]: https://github.com/input-output-hk/io-sim/tree/main/io-sim/how-to-use-IOSimPOR.md [`IOSim`]: https://hackage.haskell.org/package/io-sim/docs/Control-Monad-IOSim.html#t:IOSim + +[bob-conf]: https://youtu.be/uedUGeWN4ZM +[zuriHac-2022]: https://youtu.be/tKIYQgJnGkA +[io-sim-por-presentation]: https://coot.me/presentations/iosimpor.pdf diff --git a/bench/Main.hs b/bench/Main.hs --- a/bench/Main.hs +++ b/bench/Main.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE ScopedTypeVariables #-} - module Main (main) where import Control.Concurrent.Class.MonadSTM diff --git a/io-sim.cabal b/io-sim.cabal --- a/io-sim.cabal +++ b/io-sim.cabal @@ -1,21 +1,25 @@ -cabal-version: 3.0 +cabal-version: 3.4 name: io-sim -version: 1.6.0.0 +version: 1.10.1.0 synopsis: A pure simulator for monadic concurrency with STM. description: - A pure simulator monad with support of concurency (base & async style), stm, + A pure simulator monad with support of concurrency (base & async style), stm, synchronous and asynchronous exceptions, timeouts & delays, dynamic traces, - partial order reduction and more. + partial order reduction, and more. + + = Documentation + Documentation is published + [here](https://input-output-hk.github.io/io-sim/io-sim). license: Apache-2.0 license-files: LICENSE NOTICE -copyright: 2022-2024 Input Output Global Inc (IOG) +copyright: 2022-2025 Input Output Global Inc (IOG) author: Alexander Vieth, Duncan Coutts, John Hughes, Marcin Szamotulski maintainer: Duncan Coutts duncan@well-typed.com, Marcin Szamotulski coot@coot.me category: Testing build-type: Simple extra-doc-files: CHANGELOG.md README.md bug-reports: https://github.com/input-output-hk/io-sim/issues -tested-with: GHC == { 8.10, 9.2, 9.4, 9.6, 9.8, 9.10 } +tested-with: GHC == { 9.6, 9.8, 9.10, 9.12, 9.14 } flag asserts description: Enable assertions @@ -56,35 +60,21 @@ Control.Monad.IOSimPOR.QuickCheckUtils, Control.Monad.IOSimPOR.Timeout, Data.Deque.Strict - default-language: Haskell2010 - default-extensions: ImportQualifiedPost - other-extensions: BangPatterns, - CPP, - DeriveFunctor, - DeriveGeneric, - DerivingVia, - ExistentialQuantification, - ExplicitNamespaces, - FlexibleContexts, - FlexibleInstances, - GADTSyntax, - GeneralizedNewtypeDeriving, - MultiParamTypeClasses, - NamedFieldPuns, - NumericUnderscores, - RankNTypes, - ScopedTypeVariables, - TypeFamilies - build-depends: base >=4.9 && <4.21, + default-language: GHC2021 + default-extensions: LambdaCase + if impl(ghc < 9.4) + default-extensions: GADTs + build-depends: base >=4.16 && <4.23, io-classes:{io-classes,strict-stm,si-timers} - ^>=1.6, + ^>=1.10, exceptions >=0.10, containers, deepseq, + hashable, nothunks, primitive >=0.7 && <0.11, psqueues >=0.2 && <0.3, - time >=1.9.1 && <1.13, + time >=1.9.1 && <1.16, quiet, QuickCheck, parallel @@ -104,8 +94,10 @@ Test.Control.Monad.Utils Test.Control.Monad.IOSim Test.Control.Monad.IOSimPOR - default-language: Haskell2010 - default-extensions: ImportQualifiedPost + default-language: GHC2021 + default-extensions: LambdaCase + if impl(ghc < 9.4) + default-extensions: GADTs build-depends: base, array, containers, @@ -120,14 +112,18 @@ -rtsopts if impl(ghc >= 9.8) ghc-options: -Wno-x-partial + if impl(ghc >= 9.14) + ghc-options: -Wno-incomplete-record-selectors benchmark bench import: warnings type: exitcode-stdio-1.0 hs-source-dirs: bench main-is: Main.hs - default-language: Haskell2010 - default-extensions: ImportQualifiedPost + default-language: GHC2021 + default-extensions: LambdaCase + if impl(ghc < 9.4) + default-extensions: GADTs build-depends: base, criterion ^>= 1.6, diff --git a/src/Control/Monad/IOSim.hs b/src/Control/Monad/IOSim.hs --- a/src/Control/Monad/IOSim.hs +++ b/src/Control/Monad/IOSim.hs @@ -1,11 +1,7 @@ {-# LANGUAGE ExplicitNamespaces #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TupleSections #-} +{-# LANGUAGE QuantifiedConstraints #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} -{-# LANGUAGE QuantifiedConstraints #-} module Control.Monad.IOSim ( -- * Simulation monad IOSim @@ -22,6 +18,9 @@ , monadicIOSim , runIOSimGen -- ** Explore races using /IOSimPOR/ + , monadicIOSimPOR_ + , monadicIOSimPOR + , runIOSimPORGen -- $iosimpor , exploreSimTrace , controlSimTrace @@ -42,6 +41,7 @@ , unshareClock -- * Simulation trace , type SimTrace + , Time (..) , Trace (Cons, Nil, SimTrace, SimPORTrace, TraceDeadlock, TraceLoop, TraceMainReturn, TraceMainException, TraceRacesFound, TraceInternalError) , traceEvents , traceResult @@ -51,6 +51,7 @@ , ThreadLabel , IOSimThreadId (..) , Labelled (..) + , Unique -- ** Dynamic Tracing , traceM , traceSTM @@ -101,7 +102,7 @@ import Data.List.Trace (Trace (..)) -import Control.Exception (throw) +import Control.Exception (SomeAsyncException (..), throw) import Control.Monad.ST.Lazy @@ -144,11 +145,12 @@ . traceSelectTraceEvents fn -- | Like 'selectTraceEvents', but it returns even if the simulation trace ends --- with 'Failure'. +-- with 'Failure'. It also works with any return type, not only `SimResult` +-- like `selectTraceEvents` does. -- selectTraceEvents' :: (Time -> SimEventType -> Maybe b) - -> SimTrace a + -> Trace a SimEvent -> [b] selectTraceEvents' fn = bifoldr ( \ _ _ -> [] ) @@ -225,20 +227,22 @@ fn t (EventLog dyn) = (t,) <$> fromDynamic dyn fn _ _ = Nothing --- | Like 'selectTraceEventsDynamic' but it returns even if the simulation trace --- ends with 'Failure'. +-- | Like 'selectTraceEventsDynamic' but it returns even if the simulation +-- trace ends with 'Failure'. It also works with any return type, not only +-- `SimResult` like `selectTraceEventsDynamic` does. -- -selectTraceEventsDynamic' :: forall a b. Typeable b => SimTrace a -> [b] +selectTraceEventsDynamic' :: forall a b. Typeable b => Trace a SimEvent -> [b] selectTraceEventsDynamic' = selectTraceEvents' fn where fn :: Time -> SimEventType -> Maybe b fn _ (EventLog dyn) = fromDynamic dyn fn _ _ = Nothing --- | Like `selectTraceEventsDynamic'` but it also captures time of the trace --- event. +-- | Like `selectTraceEventsDynamicWithTime'` but it also captures time of the +-- trace event. It also works with any return type, not only `SimResult` like +-- `selectTraceEventsDynamicWithTime` does. -- -selectTraceEventsDynamicWithTime' :: forall a b. Typeable b => SimTrace a -> [(Time, b)] +selectTraceEventsDynamicWithTime' :: forall a b. Typeable b => Trace a SimEvent -> [(Time, b)] selectTraceEventsDynamicWithTime' = selectTraceEvents' fn where fn :: Time -> SimEventType -> Maybe (Time, b) @@ -266,9 +270,10 @@ fn _ _ = Nothing -- | Like 'selectTraceEventsSay' but it returns even if the simulation trace --- ends with 'Failure'. +-- ends with 'Failure'. It also works with any return type, not only `SimResult` +-- like `selectTraceEventsSay` does. -- -selectTraceEventsSay' :: SimTrace a -> [String] +selectTraceEventsSay' :: Trace a SimEvent -> [String] selectTraceEventsSay' = selectTraceEvents' fn where fn :: Time -> SimEventType -> Maybe String @@ -277,7 +282,7 @@ -- | Like `selectTraceEventsSay'` but it also captures time of the trace event. -- -selectTraceEventsSayWithTime' :: SimTrace a -> [(Time, String)] +selectTraceEventsSayWithTime' :: Trace a SimEvent -> [(Time, String)] selectTraceEventsSayWithTime' = selectTraceEvents' fn where fn :: Time -> SimEventType -> Maybe (Time, String) @@ -361,7 +366,7 @@ deriving Show instance Exception Failure where - displayException (FailureException err) = displayException err + displayException (FailureException err) = displayException err displayException (FailureDeadlock threads) = concat [ "< IO (Either Failure a) eval a = do - r <- try (evaluate a) + -- NOTE: It's fine to let asynchronous exceptions pass through. The only + -- way simulation could raise them is by using `throw` in pure code, while + -- `throwIO` in the simulation will be captured as `FailureException`. So + -- we can safely assume asynchronous exceptions are coming from the + -- environment running the simulation, e.g. `QuickCheck`, as in the case + -- of `within` or `discardAfter` operators. + r <- tryJust (\e -> case fromException @SomeAsyncException e of + Just _ -> Nothing + Nothing -> Just e) + (evaluate a) case r of Left e -> return (Left (FailureEvaluation e)) Right _ -> go a @@ -790,3 +804,77 @@ Capture eval <- capture let trace = runSimTrace (eval sim) return (f trace) + +-- | Like , +-- but evaluates generated simulations using 'exploreSimTrace'. +-- +-- The callback receives the previously passing trace (if any) and the current +-- trace being checked. +-- +-- @since 1.10.0.0 +-- +runIOSimPORGen :: Testable test + => (ExplorationOptions -> ExplorationOptions) + -> (Maybe (SimTrace a) -> SimTrace a -> test) + -> (forall s. Gen (IOSim s a)) + -> Gen Property +runIOSimPORGen optsf k sim = do + Capture eval <- capture + pure $ exploreSimTrace optsf (eval sim) k + +-- | A /IOSimPOR/ variant of 'monadicIOSim_', which: +-- +-- * explores alternative schedules using 'exploreSimTrace'; +-- * allows to run in monad stacks build on top of `IOSim`; +-- * gives more control how to attach debugging information to failed +-- tests. +-- +-- Note, to use this combinator your monad needs to be defined as: +-- +-- > newtype M s a = M { runM :: ReaderT State (IOSim s) a } +-- +-- It's important that `M s` is a monad. For such a monad you'll need to +-- provide a natural transformation: +-- @ +-- -- the state could also be created as an `IOSim` computation. +-- nat :: forall s a. State -> M s a -> 'IOSim' s a +-- nat state m = runStateT (runM m) state +-- @ +-- +-- @since 1.10.0.0 +-- +monadicIOSimPOR :: (Testable a, forall s. Monad (m s)) + => (ExplorationOptions -> ExplorationOptions) + -> (Maybe (SimTrace Property) -> SimTrace Property -> Property) + -> (forall s a. m s a -> IOSim s a) + -> (forall s. PropertyM (m s) a) + -> Property +monadicIOSimPOR optsf f tr sim = + property (runIOSimPORGen optsf f (tr <$> monadic' sim)) + +-- | Like , +-- but using /IOSimPOR/ schedule exploration. +-- +-- Note: it calls `traceResult` in non-strict mode, e.g. leaked threads do not +-- cause failures. +-- +-- > testProperty "example" $ +-- > monadicIOSimPOR_ $ do +-- > x <- run (pure (1 :: Int)) +-- > assert (x == 1) +-- +-- @since 1.10.0.0 +-- +monadicIOSimPOR_ :: Testable a + => (forall s. PropertyM (IOSim s) a) + -> Property +monadicIOSimPOR_ sim = + monadicIOSimPOR + id + (\_ tr -> case traceResult False tr of + Left e -> counterexample (show e) False + Right p -> p) + id + sim diff --git a/src/Control/Monad/IOSim/CommonTypes.hs b/src/Control/Monad/IOSim/CommonTypes.hs --- a/src/Control/Monad/IOSim/CommonTypes.hs +++ b/src/Control/Monad/IOSim/CommonTypes.hs @@ -1,10 +1,7 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE RoleAnnotations #-} -- | Common types shared between `IOSim` and `IOSimPOR`. -- @@ -16,6 +13,7 @@ , childThreadId , setRacyThread , TVarId (..) + , VarId , TimeoutId (..) , ClockId (..) , VectorClock (..) @@ -25,9 +23,13 @@ , TVarLabel , TVar (..) , SomeTVar (..) + , someTVarToLabelled , Deschedule (..) , ThreadStatus (..) , BlockedReason (..) + , Labelled (..) + , ppLabelled + , Unique (..) -- * Utils , ppList ) where @@ -38,6 +40,7 @@ import NoThunks.Class +import Data.Hashable import Data.List (intercalate, intersperse) import Data.Map (Map) import Data.Map qualified as Map @@ -65,6 +68,8 @@ deriving anyclass NFData deriving anyclass NoThunks +instance Hashable IOSimThreadId + ppIOSimThreadId :: IOSimThreadId -> String ppIOSimThreadId (RacyThreadId as) = "Thread {"++ intercalate "," (map show as) ++"}" ppIOSimThreadId (ThreadId as) = "Thread " ++ show as @@ -88,7 +93,24 @@ ppStepId (tid, step) = concat [ppIOSimThreadId tid, ".", show step] -newtype TVarId = TVarId Int deriving (Eq, Ord, Enum, Show) +type VarId = Int +-- | 'TVar's are used to emulate other shared variables. Each one comes with +-- its own id constructor. +data TVarId = + TVarId !VarId + -- ^ a `TVar` + | TMVarId !VarId + -- ^ a `TMVar` simulated by a `TVar`. + | MVarId !VarId + -- ^ an `MVar` simulated by a `TVar`. + | TQueueId !VarId + -- ^ a 'TQueue` simulated by a `TVar`. + | TBQueueId !VarId + -- ^ a 'TBQueue` simulated by a `TVar`. + | TSemId !VarId + -- ^ a 'TSem` simulated by a `TVar`. + -- TODO: `TChan` + deriving (Eq, Ord, Show) newtype TimeoutId = TimeoutId Int deriving (Eq, Ord, Enum, Show) newtype ClockId = ClockId [Int] deriving (Eq, Ord, Show) newtype VectorClock = VectorClock { getVectorClock :: Map IOSimThreadId Int } @@ -135,7 +157,7 @@ tvarVClock :: !(STRef s VectorClock), -- | Callback to construct a trace which will be attached to the dynamic - -- trace. + -- trace each time the `TVar` is committed. tvarTrace :: !(STRef s (Maybe (Maybe a -> a -> ST s TraceValue))) } @@ -145,6 +167,11 @@ data SomeTVar s where SomeTVar :: !(TVar s a) -> SomeTVar s +someTVarToLabelled :: SomeTVar s -> ST s (Labelled (SomeTVar s)) +someTVarToLabelled tv@(SomeTVar var) = do + lbl <- readSTRef (tvarLabel var) + pure (Labelled tv lbl) + data Deschedule = Yield | Interruptable | Blocked BlockedReason @@ -161,6 +188,31 @@ | BlockedOnDelay | BlockedOnThrowTo deriving (Eq, Show) + +-- | A labelled value. +-- +-- For example 'labelThread' or `labelTVar' will insert a label to `IOSimThreadId` +-- (or `TVarId`). +data Labelled a = Labelled { + l_labelled :: !a, + l_label :: !(Maybe String) + } + deriving (Eq, Ord, Generic, Functor) + 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] + +-- | Abstract unique symbols à la "Data.Unique". +newtype Unique s = MkUnique{ unMkUnique :: Integer } + deriving stock (Eq, Ord) + deriving newtype NFData +type role Unique nominal + +instance Hashable (Unique s) where + hash = fromInteger . unMkUnique + hashWithSalt = defaultHashWithSalt -- -- Utils diff --git a/src/Control/Monad/IOSim/Internal.hs b/src/Control/Monad/IOSim/Internal.hs --- a/src/Control/Monad/IOSim/Internal.hs +++ b/src/Control/Monad/IOSim/Internal.hs @@ -1,14 +1,6 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTSyntax #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE TypeFamilies #-} -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') -- and 'reschedule'. @@ -48,22 +40,25 @@ import Prelude hiding (read) +import Data.Coerce import Data.Deque.Strict (Deque) import Data.Deque.Strict qualified as Deque import Data.Dynamic import Data.Foldable (foldlM, toList, traverse_) +import Data.IntPSQ (IntPSQ) +import Data.IntPSQ qualified as PSQ import Data.List qualified as List import Data.List.Trace qualified as Trace import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map import Data.Maybe (mapMaybe) -import Data.OrdPSQ (OrdPSQ) -import Data.OrdPSQ qualified as PSQ import Data.Set (Set) import Data.Set qualified as Set import Data.Time (UTCTime (..), fromGregorian) -import Control.Exception (NonTermination (..), assert, throw) +import Control.DeepSeq (force) +import Control.Exception (NonTermination (..), SomeAsyncException, assert, + throw) import Control.Monad (join, when) import Control.Monad.ST.Lazy import Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST) @@ -134,7 +129,7 @@ -- `TimeoutId` (only used to report in a trace). -type Timeouts s = OrdPSQ TimeoutId Time (TimerCompletionInfo s) +type Timeouts s = IntPSQ Time (TimerCompletionInfo s) -- | Internal state. -- @@ -149,8 +144,9 @@ timers :: !(Timeouts s), -- | list of clocks clocks :: !(Map ClockId UTCTime), - nextVid :: !TVarId, -- ^ next unused 'TVarId' - nextTmid :: !TimeoutId -- ^ next unused 'TimeoutId' + nextVid :: !VarId, -- ^ next unused 'VarId' + nextTmid :: !TimeoutId, -- ^ next unused 'TimeoutId' + nextUniq :: !(Unique s) -- ^ next unused @'Unique' s@ } initialState :: SimState s a @@ -161,8 +157,9 @@ curTime = Time 0, timers = PSQ.empty, clocks = Map.singleton (ClockId []) epoch1970, - nextVid = TVarId 0, - nextTmid = TimeoutId 0 + nextVid = 0, + nextTmid = TimeoutId 0, + nextUniq = MkUnique 0 } where epoch1970 = UTCTime (fromGregorian 1970 1 1) 0 @@ -204,7 +201,7 @@ threads, timers, clocks, - nextVid, nextTmid, + nextVid, nextTmid, nextUniq, curTime = time } = invariant (Just thread) simstate $ @@ -263,7 +260,7 @@ DelayFrame tmid k ctl' -> do let thread' = thread { threadControl = ThreadControl k ctl' } - timers' = PSQ.delete tmid timers + timers' = (PSQ.delete . coerce) tmid timers schedule thread' simstate { timers = timers' } Throw e -> case unwindControlStack e thread timers of @@ -298,26 +295,55 @@ schedule thread' simstate Evaluate expr k -> do - mbWHNF <- unsafeIOToST $ try $ evaluate expr + mbWHNF <- unsafeIOToST $ tryJust (\e -> case fromException @SomeAsyncException e of + Nothing -> Just e + Just {} -> Nothing) + $ evaluate expr case mbWHNF of Left e -> do -- schedule this thread to immediately raise the exception let thread' = thread { threadControl = ThreadControl (Throw e) ctl } - schedule thread' simstate + trace <- schedule thread' simstate + return $ SimTrace time tid tlbl (EventEvaluationError e) + $ trace Right whnf -> do -- continue with the resulting WHNF let thread' = thread { threadControl = ThreadControl (k whnf) ctl } - schedule thread' simstate + trace <- schedule thread' simstate + return $ SimTrace time tid tlbl EventEvaluationSuccess + $ trace Say msg k -> do - let thread' = thread { threadControl = ThreadControl k ctl } - trace <- schedule thread' simstate - return (SimTrace time tid tlbl (EventSay msg) trace) + mbNF <- unsafeIOToST $ tryJust (\e -> case fromException @SomeAsyncException e of + Nothing -> Just e + Just {} -> Nothing) + $ evaluate (force msg) + case mbNF of + Left e -> do + let thread' = thread { threadControl = ThreadControl (Throw e) ctl } + trace <- schedule thread' simstate + return $ SimTrace time tid tlbl (EventSayEvaluationError e) + $ trace + Right msg' -> do + let thread' = thread { threadControl = ThreadControl k ctl } + trace <- schedule thread' simstate + return (SimTrace time tid tlbl (EventSay msg') trace) - Output x k -> do - let thread' = thread { threadControl = ThreadControl k ctl } - trace <- schedule thread' simstate - return (SimTrace time tid tlbl (EventLog x) trace) + Output x@(Dynamic _ x') k -> do + mbWHNF <- unsafeIOToST $ tryJust (\e -> case fromException @SomeAsyncException e of + Nothing -> Just e + Just {} -> Nothing) + $ evaluate x' + case mbWHNF of + Left e -> do + let thread' = thread { threadControl = ThreadControl (Throw e) ctl } + trace <- schedule thread' simstate + return $ SimTrace time tid tlbl (EventLogEvaluationError e) + $ trace + Right {} -> do + let thread' = thread { threadControl = ThreadControl k ctl } + trace <- schedule thread' simstate + return (SimTrace time tid tlbl (EventLog x) trace) LiftST st k -> do x <- strictToLazyST st @@ -358,9 +384,9 @@ error "schedule: StartTimeout: Impossible happened" StartTimeout d action' k -> do - !lock <- TMVar <$> execNewTVar nextVid (Just $! "lock-" ++ show nextTmid) Nothing + !lock <- TMVar <$> execNewTVar (TMVarId nextVid) (Just $! "lock-" ++ show nextTmid) Nothing let !expiry = d `addTime` time - !timers' = PSQ.insert nextTmid expiry (TimerTimeout tid nextTmid lock) timers + !timers' = (PSQ.insert . coerce) nextTmid expiry (TimerTimeout tid nextTmid lock) timers !thread' = thread { threadControl = ThreadControl action' (TimeoutFrame nextTmid lock k ctl) @@ -373,31 +399,31 @@ UnregisterTimeout tmid k -> do let thread' = thread { threadControl = ThreadControl k ctl } - schedule thread' simstate { timers = PSQ.delete tmid timers } + schedule thread' simstate { timers = (PSQ.delete . coerce) tmid timers } RegisterDelay d k | d < 0 -> do - !tvar <- execNewTVar nextVid + !tvar <- execNewTVar (TVarId nextVid) (Just $! "<>") True let !expiry = d `addTime` time !thread' = thread { threadControl = ThreadControl (k tvar) ctl } trace <- schedule thread' simstate { nextVid = succ nextVid } - return (SimTrace time tid tlbl (EventRegisterDelayCreated nextTmid nextVid expiry) $ + return (SimTrace time tid tlbl (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) $ SimTrace time tid tlbl (EventRegisterDelayFired nextTmid) $ trace) RegisterDelay d k -> do - !tvar <- execNewTVar nextVid + !tvar <- execNewTVar (TVarId nextVid) (Just $! "<>") False let !expiry = d `addTime` time - !timers' = PSQ.insert nextTmid expiry (TimerRegisterDelay tvar) timers + !timers' = (PSQ.insert . coerce) nextTmid expiry (TimerRegisterDelay tvar) timers !thread' = thread { threadControl = ThreadControl (k tvar) ctl } trace <- schedule thread' simstate { timers = timers' , nextVid = succ nextVid , nextTmid = succ nextTmid } return (SimTrace time tid tlbl - (EventRegisterDelayCreated nextTmid nextVid expiry) trace) + (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) trace) ThreadDelay d k | d < 0 -> do let !expiry = d `addTime` time @@ -410,7 +436,7 @@ ThreadDelay d k -> do let !expiry = d `addTime` time - !timers' = PSQ.insert nextTmid expiry (TimerThreadDelay tid nextTmid) timers + !timers' = (PSQ.insert . coerce) nextTmid expiry (TimerThreadDelay tid nextTmid) timers !thread' = thread { threadControl = ThreadControl (Return ()) (DelayFrame nextTmid k ctl) } !trace <- deschedule (Blocked BlockedOnDelay) thread' simstate { timers = timers' , nextTmid = succ nextTmid } @@ -424,25 +450,25 @@ !expiry = d `addTime` time !thread' = thread { threadControl = ThreadControl (k t) ctl } trace <- schedule thread' simstate { nextTmid = succ nextTmid } - return (SimTrace time tid tlbl (EventTimerCreated nextTmid nextVid expiry) $ + return (SimTrace time tid tlbl (EventTimerCreated nextTmid (TVarId nextVid) expiry) $ SimTrace time tid tlbl (EventTimerCancelled nextTmid) $ trace) NewTimeout d k -> do - !tvar <- execNewTVar nextVid + !tvar <- execNewTVar (TVarId nextVid) (Just $! "<>") TimeoutPending let !expiry = d `addTime` time !t = Timeout tvar nextTmid - !timers' = PSQ.insert nextTmid expiry (Timer tvar) timers + !timers' = (PSQ.insert . coerce) nextTmid expiry (Timer tvar) timers !thread' = thread { threadControl = ThreadControl (k t) ctl } trace <- schedule thread' simstate { timers = timers' , nextVid = succ nextVid , nextTmid = succ nextTmid } - return (SimTrace time tid tlbl (EventTimerCreated nextTmid nextVid expiry) trace) + return (SimTrace time tid tlbl (EventTimerCreated nextTmid (TVarId nextVid) expiry) trace) CancelTimeout (Timeout tvar tmid) k -> do - let !timers' = PSQ.delete tmid timers + let !timers' = (PSQ.delete . coerce) 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 @@ -547,6 +573,13 @@ , threadLabel = Just l } schedule thread' simstate + GetThreadLabel tid' k -> do + let tlbl' | tid' == tid = tlbl + | otherwise = tid' `Map.lookup` threads + >>= threadLabel + thread' = thread { threadControl = ThreadControl (k tlbl') ctl } + schedule thread' simstate + LabelThread tid' l k -> do let thread' = thread { threadControl = ThreadControl k ctl } threads' = Map.adjust (\t -> t { threadLabel = Just l }) tid' threads @@ -631,7 +664,14 @@ thread' = thread { threadControl = ThreadControl k' ctl } schedule thread' simstate + NewUnique k -> do + let thread' = thread{ threadControl = ThreadControl (k nextUniq) ctl } + n = unMkUnique nextUniq + simstate' = simstate{ nextUniq = MkUnique (n + 1) } + SimTrace time tid tlbl (EventUniqueCreated n) + <$> schedule thread' simstate' + threadInterruptible :: Thread s a -> Bool threadInterruptible thread = case threadMasking thread of @@ -918,8 +958,8 @@ where unwind :: forall s' c. MaskingState -> ControlStack s' c a - -> OrdPSQ TimeoutId Time (TimerCompletionInfo s) - -> (Either Bool (Thread s' a), OrdPSQ TimeoutId Time (TimerCompletionInfo s)) + -> IntPSQ Time (TimerCompletionInfo s) + -> (Either Bool (Thread s' a), IntPSQ Time (TimerCompletionInfo s)) unwind _ MainFrame timers = (Left True, timers) unwind _ ForkFrame timers = (Left False, timers) unwind _ (MaskFrame _k maskst' ctl) timers = unwind maskst' ctl timers @@ -955,13 +995,13 @@ _ -> unwind maskst ctl timers' where -- Remove the timeout associated with the 'TimeoutFrame'. - timers' = PSQ.delete tmid timers + timers' = (PSQ.delete . coerce) tmid timers unwind maskst (DelayFrame tmid _k ctl) timers = unwind maskst ctl timers' where -- Remove the timeout associated with the 'DelayFrame'. - timers' = PSQ.delete tmid timers + timers' = (PSQ.delete . coerce) tmid timers atLeastInterruptibleMask :: MaskingState -> MaskingState @@ -969,10 +1009,10 @@ atLeastInterruptibleMask ms = ms -removeMinimums :: (Ord k, Ord p) - => OrdPSQ k p a - -> Maybe ([k], p, [a], OrdPSQ k p a) -removeMinimums = \psq -> +removeMinimums :: (Coercible k Int, Ord p) + => IntPSQ p a + -> Maybe ([k], p, [a], IntPSQ p a) +removeMinimums = \psq -> coerce $ case PSQ.minView psq of Nothing -> Nothing Just (k, p, x, psq') -> Just (collectAll [k] p [x] psq') @@ -1023,7 +1063,7 @@ Time -> IOSimThreadId -> Maybe ThreadLabel - -> TVarId + -> VarId -> StmA s a -> (StmTxResult s a -> ST s (SimTrace c)) -> ST s (SimTrace c) @@ -1036,7 +1076,7 @@ -> Map TVarId (SomeTVar s) -- set of vars written -> [SomeTVar s] -- vars written in order (no dups) -> [SomeTVar s] -- vars created in order - -> TVarId -- var fresh name supply + -> VarId -- var fresh name supply -> StmA s b -> ST s (SimTrace c) go !ctl !read !written !writtenSeq !createdSeq !nextVid !action = @@ -1085,25 +1125,8 @@ -- Skip the right hand alternative and continue with the k continuation go ctl' read written' writtenSeq' createdSeq' nextVid (k x) - ThrowStm e -> do - -- Rollback `TVar`s written since catch handler was installed - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - case ctl of - AtomicallyFrame -> do - k0 $ StmTxAborted (Map.elems read) (toException e) - - BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - -- Execute the left side in a new frame with an empty written set. - -- but preserve ones that were set prior to it, as specified in the - -- [stm](https://hackage.haskell.org/package/stm/docs/Control-Monad-STM.html#v:catchSTM) package. - let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' - go ctl'' read Map.empty [] [] nextVid (h e) - - BranchFrame (OrElseStmA _r) _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) - - BranchFrame NoOpStmA _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) + ThrowStm e -> + throwStm ctl read written nextVid e CatchStm a h k -> do -- Execute the catch handler with an empty written set. @@ -1138,8 +1161,8 @@ let ctl' = BranchFrame (OrElseStmA b) k written writtenSeq createdSeq ctl go ctl' read Map.empty [] [] nextVid a - NewTVar !mbLabel x k -> do - !v <- execNewTVar nextVid mbLabel x + NewTVar mkId !mbLabel x k -> do + !v <- execNewTVar (mkId nextVid) mbLabel x go ctl read written writtenSeq (SomeTVar v : createdSeq) (succ nextVid) (k v) LabelTVar !label tvar k -> do @@ -1171,12 +1194,32 @@ go ctl read written' (SomeTVar v : writtenSeq) createdSeq nextVid k SayStm msg k -> do - trace <- go ctl read written writtenSeq createdSeq nextVid k - return $ SimTrace time tid tlbl (EventSay msg) trace + mbNF <- unsafeIOToST $ tryJust (\e -> case fromException @SomeAsyncException e of + Nothing -> Just e + Just {} -> Nothing) + $ evaluate (force msg) + case mbNF of + Left e -> do + trace <- throwStm ctl read written nextVid e + return $ SimTrace time tid tlbl (EventSayEvaluationError e) + $ trace + Right msg' -> do + trace <- go ctl read written writtenSeq createdSeq nextVid k + return $ SimTrace time tid tlbl (EventSay msg') trace - OutputStm x k -> do - trace <- go ctl read written writtenSeq createdSeq nextVid k - return $ SimTrace time tid tlbl (EventLog x) trace + OutputStm x@(Dynamic _ x') k -> do + mbWHNF <- unsafeIOToST $ tryJust (\e -> case fromException @SomeAsyncException e of + Nothing -> Just e + Just {} -> Nothing) + $ evaluate x' + case mbWHNF of + Left e -> do + trace <- throwStm ctl read written nextVid e + return $ SimTrace time tid tlbl (EventLogEvaluationError e) + $ trace + Right {} -> do + trace <- go ctl read written writtenSeq createdSeq nextVid k + return $ SimTrace time tid tlbl (EventLog x) trace LiftSTStm st k -> do x <- strictToLazyST st @@ -1194,7 +1237,35 @@ Map.keysSet written == Set.fromList [ tvarId tvar | SomeTVar tvar <- writtenSeq ] + -- throw an exception in an STM transaction + throwStm :: forall b. + StmStack s b a + -> Map TVarId (SomeTVar s) + -> Map TVarId (SomeTVar s) + -> VarId + -> SomeException + -> ST s (SimTrace c) + throwStm ctl read written nextVid e = do + -- Rollback `TVar`s written since catch handler was installed + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + case ctl of + AtomicallyFrame -> do + k0 $ StmTxAborted (Map.elems read) (toException e) + BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + -- Execute the left side in a new frame with an empty written set. + -- but preserve ones that were set prior to it, as specified in the + -- [stm](https://hackage.haskell.org/package/stm/docs/Control-Monad-STM.html#v:catchSTM) package. + let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' + go ctl'' read Map.empty [] [] nextVid (h e) + + BranchFrame (OrElseStmA _r) _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) + + BranchFrame NoOpStmA _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) + + -- | Special case of 'execAtomically' supporting only var reads and writes -- execAtomically' :: StmA s () -> ST s [SomeTVar s] @@ -1222,16 +1293,15 @@ execNewTVar :: TVarId -> Maybe String -> a -> ST s (TVar s a) -execNewTVar nextVid !mbLabel x = do +execNewTVar !tvarId !mbLabel x = do !tvarLabel <- newSTRef mbLabel !tvarCurrent <- newSTRef x !tvarUndo <- newSTRef $! [] !tvarBlocked <- newSTRef ([], Set.empty) !tvarVClock <- newSTRef $! VectorClock Map.empty !tvarTrace <- newSTRef $! Nothing - return TVar {tvarId = nextVid, tvarLabel, - tvarCurrent, tvarUndo, tvarBlocked, tvarVClock, - tvarTrace} + return TVar {tvarId, tvarLabel, tvarCurrent, tvarUndo, tvarBlocked, + tvarVClock, tvarTrace} -- 'execReadTVar' is defined in `Control.Monad.IOSim.Type` and shared with /IOSimPOR/ diff --git a/src/Control/Monad/IOSim/InternalTypes.hs b/src/Control/Monad/IOSim/InternalTypes.hs --- a/src/Control/Monad/IOSim/InternalTypes.hs +++ b/src/Control/Monad/IOSim/InternalTypes.hs @@ -1,6 +1,4 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE GADTs #-} -- | Internal types shared between `IOSim` and `IOSimPOR`. -- diff --git a/src/Control/Monad/IOSim/STM.hs b/src/Control/Monad/IOSim/STM.hs --- a/src/Control/Monad/IOSim/STM.hs +++ b/src/Control/Monad/IOSim/STM.hs @@ -1,7 +1,4 @@ -{-# LANGUAGE BangPatterns #-} {-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -- | 'io-sim' implementation of 'TQueue', 'TBQueue' and 'MVar'. -- @@ -38,7 +35,7 @@ :: MonadTraceSTM m => proxy m -> TQueueDefault m a - -> (Maybe [a] -> [a] -> InspectMonad m TraceValue) + -> (Maybe [a] -> [a] -> InspectMonadSTM m TraceValue) -> STM m () traceTQueueDefault p (TQueue queue) f = traceTVar p queue @@ -122,7 +119,7 @@ :: MonadTraceSTM m => proxy m -> TBQueueDefault m a - -> (Maybe [a] -> [a] -> InspectMonad m TraceValue) + -> (Maybe [a] -> [a] -> InspectMonadSTM m TraceValue) -> STM m () traceTBQueueDefault p (TBQueue queue _size) f = traceTVar p queue (\mas as -> f (g <$> mas) (g as)) @@ -149,12 +146,8 @@ return (Just x) [] -> case reverse ys of - [] -> do - writeTVar queue $! (xs, r', ys, w) - return Nothing + [] -> return Nothing - -- NB. lazy: we want the transaction to be - -- short, otherwise it will conflict (z:zs) -> do writeTVar queue $! (zs, r', [], w) return (Just z) @@ -234,7 +227,7 @@ -- -- /Implementation details:/ -- --- 'STM' does not guarantee fairness, instead it provide compositionally. +-- @STM@ does not guarantee fairness, instead it provides compositionally. -- Fairness of 'putMVarDefault' and 'takeMVarDefault' is provided by tracking -- queue of blocked operation in the 'MVarState', e.g. when a 'putMVarDefault' -- is scheduled on a full 'MVar', the request is put on to the back of the queue @@ -261,13 +254,17 @@ newEmptyMVarDefault :: MonadSTM m => m (MVarDefault m a) newEmptyMVarDefault = MVar <$> newTVarIO (MVarEmpty mempty mempty) +labelMVarDefault + :: MonadLabelledSTM m + => MVarDefault m a -> String -> m () +labelMVarDefault (MVar tvar) = atomically . labelTVar tvar newMVarDefault :: MonadSTM m => a -> m (MVarDefault m a) newMVarDefault a = MVar <$> newTVarIO (MVarFull a mempty) putMVarDefault :: ( MonadMask m - , MonadSTM m + , MonadLabelledSTM m , forall x tvar. tvar ~ TVar m x => Eq tvar ) => MVarDefault m a -> a -> m () @@ -278,6 +275,7 @@ -- It's full, add ourselves to the end of the 'put' blocked queue. MVarFull x' putq -> do putvar <- newTVar False + labelTVar putvar "internal-putvar" writeTVar tv (MVarFull x' (Deque.snoc (x, putvar) putq)) return (Just putvar) @@ -350,7 +348,7 @@ takeMVarDefault :: ( MonadMask m - , MonadSTM m + , MonadLabelledSTM m , forall x tvar. tvar ~ TVar m x => Eq tvar ) => MVarDefault m a @@ -362,6 +360,7 @@ -- It's empty, add ourselves to the end of the 'take' blocked queue. MVarEmpty takeq readq -> do takevar <- newTVar Nothing + labelTVar takevar "internal-takevar" writeTVar tv (MVarEmpty (Deque.snoc takevar takeq) readq) return (Left takevar) @@ -392,8 +391,25 @@ -- takevar; we need to remove it from 'takeq', otherwise we -- will have a space leak. let takeq' = Deque.filter (/= takevar) takeq - writeTVar tv (MVarEmpty takeq' readq) + takevalue <- readTVar takevar + case takevalue of + Nothing -> + writeTVar tv (MVarEmpty takeq' readq) + -- we were given a value before we could read it. Relay it to any + -- new reading threads and possible the next take thread. + Just x -> do + -- notify readers + mapM_ (\readvar -> writeTVar readvar (Just x)) readq + -- notify first `takeMVar` thread + case Deque.uncons takeq' of + Nothing -> + writeTVar tv (MVarFull x mempty) + + Just (takevar', takeq'') -> do + writeTVar takevar' (Just x) + writeTVar tv (MVarEmpty takeq'' mempty) + -- This case is unlikely but possible if another thread ran -- first and modified the mvar. This situation is fine as far as -- space leaks are concerned because it means our wait var is no @@ -433,7 +449,7 @@ -- 'putMVar' value. It will also not block if the 'MVar' is full, even if there -- are other threads attempting to 'putMVar'. -- -readMVarDefault :: ( MonadSTM m +readMVarDefault :: ( MonadLabelledSTM m , MonadMask m , forall x tvar. tvar ~ TVar m x => Eq tvar ) @@ -446,6 +462,7 @@ -- It's empty, add ourselves to the 'read' blocked queue. MVarEmpty takeq readq -> do readvar <- newTVar Nothing + labelTVar readvar "internal-readvar" writeTVar tv (MVarEmpty takeq (Deque.snoc readvar readq)) return (Left readvar) diff --git a/src/Control/Monad/IOSim/Types.hs b/src/Control/Monad/IOSim/Types.hs --- a/src/Control/Monad/IOSim/Types.hs +++ b/src/Control/Monad/IOSim/Types.hs @@ -1,22 +1,14 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTSyntax #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE NumericUnderscores #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} -- Needed for `SimEvent` type. {-# OPTIONS_GHC -Wno-partial-fields #-} +-- `MonadMaskingState` is deprecated in `io-classes`, but we provide an instance +-- for it. +{-# OPTIONS_GHC -Wno-deprecations #-} module Control.Monad.IOSim.Types ( IOSim (..) @@ -58,12 +50,11 @@ , ppTrace_ , ppSimEvent , ppDebug - , Labelled (..) , module Control.Monad.IOSim.CommonTypes , Thrower (..) - , Time (..) - , addTime - , diffTime + , SI.Time (..) + , SI.addTime + , SI.diffTime -- * Internal API , Timeout (..) , newTimeout @@ -75,7 +66,7 @@ ) where import Control.Applicative -import Control.Exception (ErrorCall (..)) +import Control.Exception (ErrorCall (..), SomeAsyncException) import Control.Exception qualified as IO import Control.Monad import Control.Monad.Fix (MonadFix (..)) @@ -91,17 +82,19 @@ import Control.Monad.Class.MonadST import Control.Monad.Class.MonadSTM.Internal (MonadInspectSTM (..), MonadLabelledSTM (..), MonadSTM, MonadTraceSTM (..), TArrayDefault, - TChanDefault, TMVarDefault, TSemDefault, TraceValue, atomically, - retry) + TChanDefault (..), TMVarDefault (..), TSemDefault (..), TraceValue, + atomically, retry) import Control.Monad.Class.MonadSTM.Internal qualified as MonadSTM import Control.Monad.Class.MonadTest import Control.Monad.Class.MonadThrow as MonadThrow hiding (getMaskingState) import Control.Monad.Class.MonadThrow qualified as MonadThrow import Control.Monad.Class.MonadTime -import Control.Monad.Class.MonadTime.SI +import Control.Monad.Class.MonadTime.SI (DiffTime) +import Control.Monad.Class.MonadTime.SI qualified as SI import Control.Monad.Class.MonadTimer import Control.Monad.Class.MonadTimer.SI (TimeoutState (..)) import Control.Monad.Class.MonadTimer.SI qualified as SI +import Control.Monad.Class.MonadUnique import Control.Monad.Primitive qualified as Prim import Control.Monad.ST.Lazy import Control.Monad.ST.Strict qualified as StrictST @@ -113,6 +106,7 @@ import Data.Bifoldable import Data.Bifunctor (bimap) import Data.Dynamic (Dynamic, toDyn) +import Data.Hashable (Hashable (hash)) import Data.List.Trace qualified as Trace import Data.Map.Strict (Map) import Data.Maybe (fromMaybe) @@ -131,12 +125,14 @@ import Quiet (Quiet (..)) import Control.Monad.IOSim.CommonTypes +import Control.Monad.IOSim.CommonTypes qualified as Sim import Control.Monad.IOSim.STM import Control.Monad.IOSimPOR.Types +import Control.DeepSeq (force) import Data.List (intercalate) -import GHC.IO (mkUserError) +import GHC.IO (mkUserError, unsafePerformIO) import System.IO.Error qualified as IO.Error (userError) {-# ANN module "HLint: ignore Use readTVarIO" #-} @@ -149,12 +145,18 @@ -- can then be recovered with `selectTraceEventsDynamic` or -- `selectTraceEventsDynamic'`. -- +-- Note: `traceM` evaluates the `a` to `WHNF`, exceptions are thrown by the +-- current thread and the trace will include `EventLogEvaluationError`. +-- traceM :: Typeable a => a -> IOSim s () -traceM !x = IOSim $ oneShot $ \k -> Output (toDyn x) (k ()) +traceM x = IOSim $ oneShot $ \k -> Output (toDyn x) (k ()) -- | Trace a value, in the same was as `traceM` does, but from the `STM` monad. -- This is primarily useful for debugging. -- +-- Note: `traceSTM` evaluates the `a` to `WHNF`, if exception is thrown, the +-- trace will end with `TraceException`. +-- traceSTM :: Typeable a => a -> STMSim s () traceSTM x = STM $ oneShot $ \k -> OutputStm (toDyn x) (k ()) @@ -168,7 +170,7 @@ LiftST :: StrictST.ST s a -> (a -> SimA s b) -> SimA s b - GetMonoTime :: (Time -> SimA s b) -> SimA s b + GetMonoTime :: (SI.Time -> SimA s b) -> SimA s b GetWallTime :: (UTCTime -> SimA s b) -> SimA s b SetWallTime :: UTCTime -> SimA s b -> SimA s b UnshareClock :: SimA s b -> SimA s b @@ -186,9 +188,10 @@ 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 () -> (IOSimThreadId -> SimA s b) -> SimA s b - GetThreadId :: (IOSimThreadId -> SimA s b) -> SimA s b - LabelThread :: IOSimThreadId -> 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 + GetThreadLabel :: IOSimThreadId -> (Maybe String -> SimA s b) -> SimA s b Atomically :: STM s a -> (a -> SimA s b) -> SimA s b @@ -201,6 +204,7 @@ ExploreRaces :: SimA s b -> SimA s b Fix :: (x -> IOSim s x) -> (x -> SimA s r) -> SimA s r + NewUnique :: (Sim.Unique s -> SimA s r) -> SimA s r newtype STM s a = STM { unSTM :: forall r. (a -> StmA s r) -> StmA s r } @@ -219,7 +223,7 @@ ThrowStm :: SomeException -> StmA s a CatchStm :: StmA s a -> (SomeException -> StmA s a) -> (a -> StmA s b) -> StmA s b - NewTVar :: Maybe String -> x -> (TVar s x -> StmA s b) -> StmA s b + NewTVar :: (VarId -> TVarId) -> Maybe String -> x -> (TVar s x -> StmA s b) -> StmA s b LabelTVar :: String -> TVar s a -> StmA s b -> StmA s b ReadTVar :: TVar s a -> (a -> StmA s b) -> StmA s b WriteTVar :: TVar s a -> a -> StmA s b -> StmA s b @@ -236,8 +240,8 @@ LiftSTStm :: StrictST.ST s a -> (a -> StmA s b) -> StmA s b FixStm :: (x -> STM s x) -> (x -> StmA s r) -> StmA s r --- | `IOSim`'s 'MonadSTM.STM' monad, as 'IOSim' it is parametrised by @s@, e.g. --- @STMSim s a@ is monadic expression of type @a@. +-- | `IOSim`'s 'Control.Monad.Class.MonadSTM.Internal.STM' monad, as 'IOSim' it +-- is parametrised by @s@, e.g. @STMSim s a@ is monadic expression of type @a@. -- type STMSim = STM @@ -335,6 +339,10 @@ instance MonadFix (STM s) where mfix f = STM $ oneShot $ \k -> FixStm f k +-- | `IOSim s` instance is strict: the string will be evaluated to normal form, +-- if an exception is encountered it is thrown in the current thread, and the +-- log will contain `EventSayEvaluationError`. +-- instance MonadSay (IOSim s) where say msg = IOSim $ oneShot $ \k -> Say msg (k ()) @@ -424,7 +432,6 @@ MaskedInterruptible -> blockUninterruptible $ action block MaskedUninterruptible -> action blockUninterruptible -instance MonadMaskingState (IOSim s) where getMaskingState = getMaskingStateImpl interruptible action = do b <- getMaskingStateImpl @@ -433,6 +440,8 @@ MaskedInterruptible -> unblock action MaskedUninterruptible -> action +instance MonadMaskingState (IOSim s) + instance Exceptions.MonadMask (IOSim s) where mask = MonadThrow.mask uninterruptibleMask = MonadThrow.uninterruptibleMask @@ -469,6 +478,7 @@ type ThreadId (IOSim s) = IOSimThreadId myThreadId = IOSim $ oneShot $ \k -> GetThreadId k labelThread t l = IOSim $ oneShot $ \k -> LabelThread t l (k ()) + threadLabel t = IOSim $ oneShot $ \k -> GetThreadLabel t k instance MonadFork (IOSim s) where forkIO task = IOSim $ oneShot $ \k -> Fork task k @@ -478,10 +488,15 @@ forkIO $ try (restore task) >>= k throwTo tid e = IOSim $ oneShot $ \k -> ThrowTo (toException e) tid (k ()) yield = IOSim $ oneShot $ \k -> YieldSim (k ()) + getNumCapabilities = return 1 instance MonadTest (IOSim s) where exploreRaces = IOSim $ oneShot $ \k -> ExploreRaces (k ()) +-- | `STM (IOSim s)` instance is strict: the string will be evaluated to normal +-- form, if an exception is encountered the trace will finish with +-- `TraceException`. +-- instance MonadSay (STMSim s) where say msg = STM $ oneShot $ \k -> SayStm msg (k ()) @@ -507,14 +522,14 @@ atomically action = IOSim $ oneShot $ \k -> Atomically action k - newTVar x = STM $ oneShot $ \k -> NewTVar Nothing x k + newTVar x = STM $ oneShot $ \k -> NewTVar TVarId Nothing x k readTVar tvar = STM $ oneShot $ \k -> ReadTVar tvar k writeTVar tvar x = STM $ oneShot $ \k -> WriteTVar tvar x (k ()) retry = STM $ oneShot $ \_ -> Retry orElse a b = STM $ oneShot $ \k -> OrElse (runSTM a) (runSTM b) k - newTMVar = MonadSTM.newTMVarDefault - newEmptyTMVar = MonadSTM.newEmptyTMVarDefault + newTMVar = \a -> STM $ oneShot $ \k -> NewTVar TMVarId Nothing (Just a) (k . TMVar) + newEmptyTMVar = STM $ oneShot $ \k -> NewTVar TMVarId Nothing Nothing (k . TMVar) takeTMVar = MonadSTM.takeTMVarDefault tryTakeTMVar = MonadSTM.tryTakeTMVarDefault putTMVar = MonadSTM.putTMVarDefault @@ -525,7 +540,7 @@ writeTMVar = MonadSTM.writeTMVarDefault isEmptyTMVar = MonadSTM.isEmptyTMVarDefault - newTQueue = newTQueueDefault + newTQueue = STM $ oneShot $ \k -> NewTVar TQueueId Nothing ([], []) (k . TQueue) readTQueue = readTQueueDefault tryReadTQueue = tryReadTQueueDefault peekTQueue = peekTQueueDefault @@ -535,7 +550,10 @@ isEmptyTQueue = isEmptyTQueueDefault unGetTQueue = unGetTQueueDefault - newTBQueue = newTBQueueDefault + newTBQueue size | size >= fromIntegral (maxBound :: Int) + = error "newTBQueue: size larger than Int" + | otherwise + = STM $ oneShot $ \k -> NewTVar TBQueueId Nothing ([], 0, [], size) (k . (`TBQueue` size )) readTBQueue = readTBQueueDefault tryReadTBQueue = tryReadTBQueueDefault peekTBQueue = peekTBQueueDefault @@ -547,7 +565,7 @@ isFullTBQueue = isFullTBQueueDefault unGetTBQueue = unGetTBQueueDefault - newTSem = MonadSTM.newTSemDefault + newTSem = \i -> STM $ oneShot $ \k -> NewTVar TSemId Nothing i (k . TSem) waitTSem = MonadSTM.waitTSemDefault signalTSem = MonadSTM.signalTSemDefault signalTSemN = MonadSTM.signalTSemNDefault @@ -565,7 +583,7 @@ cloneTChan = MonadSTM.cloneTChanDefault instance MonadInspectSTM (IOSim s) where - type InspectMonad (IOSim s) = ST s + type InspectMonadSTM (IOSim s) = ST s inspectTVar _ TVar { tvarCurrent } = readSTRef tvarCurrent inspectTMVar _ (MonadSTM.TMVar TVar { tvarCurrent }) = readSTRef tvarCurrent @@ -587,8 +605,8 @@ instance MonadMVar (IOSim s) where type MVar (IOSim s) = MVarDefault (IOSim s) - newEmptyMVar = newEmptyMVarDefault - newMVar = newMVarDefault + newEmptyMVar = atomically $ STM $ oneShot $ \k -> NewTVar MVarId Nothing (MVarEmpty mempty mempty) (k . MVar) + newMVar = \a -> atomically $ STM $ oneShot $ \k -> NewTVar MVarId Nothing (MVarFull a mempty) (k . MVar) takeMVar = takeMVarDefault putMVar = putMVarDefault tryTakeMVar = tryTakeMVarDefault @@ -605,6 +623,34 @@ MVarEmpty _ _ -> pure Nothing MVarFull x _ -> pure (Just x) +instance MonadTraceMVar (IOSim s) where + traceMVarIO :: forall proxy a. + proxy + -> MVar (IOSim s) a + -> ( Maybe (Maybe a) + -> Maybe a + -> ST s TraceValue + ) + -> IOSim s () + traceMVarIO _ (MVar mvar) f = traceTVarIO mvar f' + where + f' :: Maybe (MVarState m a) + -> MVarState m a + -> ST s TraceValue + f' mst st = f (g <$> mst) (g st) + + g :: MVarState m a -> Maybe a + g MVarEmpty{} = Nothing + g (MVarFull a _) = Just a + +instance MonadLabelledMVar (IOSim s) where + labelMVar = labelMVarDefault + +instance MonadUnique (IOSim s) where + type Unique (IOSim s) = Sim.Unique s + newUnique = IOSim (oneShot NewUnique) + hashUnique = hash + data Async s a = Async !IOSimThreadId (STM s (Either SomeException a)) instance Eq (Async s a) where @@ -665,10 +711,10 @@ getMonotonicTimeNSec = IOSim $ oneShot $ \k -> GetMonoTime (k . conv) where -- convert time in picoseconds to nanoseconds - conv :: Time -> Word64 - conv (Time d) = fromIntegral (diffTimeToPicoseconds d `div` 1_000) + conv :: SI.Time -> Word64 + conv (SI.Time d) = fromIntegral (diffTimeToPicoseconds d `div` 1_000) -instance MonadMonotonicTime (IOSim s) where +instance SI.MonadMonotonicTime (IOSim s) where getMonotonicTime = IOSim $ oneShot $ \k -> GetMonoTime k instance MonadTime (IOSim s) where @@ -760,8 +806,9 @@ newtype EventlogMarker = EventlogMarker String instance MonadEventlog (IOSim s) where - traceEventIO = traceM . EventlogEvent + traceEventIO = traceM . EventlogEvent traceMarkerIO = traceM . EventlogMarker + flushEventLog = pure () -- | 'Trace' is a recursive data type, it is the trace of a 'IOSim' -- computation. The trace will contain information about thread scheduling, @@ -781,14 +828,14 @@ data SimEvent -- | Used when using `IOSim`. = SimEvent { - seTime :: !Time, + seTime :: !SI.Time, seThreadId :: !IOSimThreadId, seThreadLabel :: !(Maybe ThreadLabel), seType :: !SimEventType } -- | Only used for /IOSimPOR/ | SimPOREvent { - seTime :: !Time, + seTime :: !SI.Time, seThreadId :: !IOSimThreadId, seStep :: !Int, seThreadLabel :: !(Maybe ThreadLabel), @@ -799,7 +846,6 @@ deriving Generic deriving Show via Quiet SimEvent - -- | Pretty print a 'SimEvent'. -- ppSimEvent :: Int -- ^ width of the time @@ -808,29 +854,25 @@ -> SimEvent -> String -ppSimEvent timeWidth tidWidth tLabelWidth SimEvent {seTime = Time time, seThreadId, seThreadLabel, seType} = +ppSimEvent timeWidth tidWidth tLabelWidth SimEvent {seTime = SI.Time time, seThreadId, seThreadLabel, seType} = printf "%-*s - %-*s %-*s - %s" timeWidth (show time) tidWidth (ppIOSimThreadId seThreadId) tLabelWidth - threadLabel + (fromMaybe "" seThreadLabel) (ppSimEventType seType) - where - threadLabel = fromMaybe "" seThreadLabel -ppSimEvent timeWidth tidWidth tLableWidth SimPOREvent {seTime = Time time, seThreadId, seStep, seThreadLabel, seType} = +ppSimEvent timeWidth tidWidth tLableWidth SimPOREvent {seTime = SI.Time time, seThreadId, seStep, seThreadLabel, seType} = printf "%-*s - %-*s %-*s - %s" timeWidth (show time) tidWidth (ppStepId (seThreadId, seStep)) tLableWidth - threadLabel + (fromMaybe "" seThreadLabel) (ppSimEventType seType) - where - threadLabel = fromMaybe "" seThreadLabel ppSimEvent _ _ _ (SimRacesFound controls) = "RacesFound "++show controls @@ -838,11 +880,11 @@ -- | A result type of a simulation. data SimResult a - = MainReturn !Time !(Labelled IOSimThreadId) a ![Labelled IOSimThreadId] + = MainReturn !SI.Time !(Labelled IOSimThreadId) a ![Labelled IOSimThreadId] -- ^ Return value of the main thread. - | MainException !Time !(Labelled IOSimThreadId) SomeException ![Labelled IOSimThreadId] + | MainException !SI.Time !(Labelled IOSimThreadId) SomeException ![Labelled IOSimThreadId] -- ^ Exception thrown by the main thread. - | Deadlock !Time ![Labelled IOSimThreadId] + | Deadlock !SI.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. @@ -860,7 +902,7 @@ -> SimResult a -> String ppSimResult timeWidth tidWidth thLabelWidth r = case r of - MainReturn (Time time) tid a tids -> + MainReturn (SI.Time time) tid a tids -> printf "%-*s - %-*s %-*s - %s %s" timeWidth (show time) @@ -870,7 +912,7 @@ (fromMaybe "" $ l_label tid) ("MainReturn " ++ show a) ("[" ++ intercalate "," (ppLabelled ppIOSimThreadId `map` tids) ++ "]") - MainException (Time time) tid e tids -> + MainException (SI.Time time) tid e tids -> printf "%-*s - %-*s %-*s - %s %s" timeWidth (show time) @@ -880,7 +922,7 @@ (fromMaybe "" $ l_label tid) ("MainException " ++ show e) ("[" ++ intercalate "," (ppLabelled ppIOSimThreadId `map` tids) ++ "]") - Deadlock (Time time) tids -> + Deadlock (SI.Time time) tids -> printf "%-*s - %-*s %-*s - %s %s" timeWidth (show time) @@ -917,12 +959,12 @@ bimaximum . bimap (const (Max 0, Max 0, Max 0)) (\a -> case a of - SimEvent {seTime = Time time, seThreadId, seThreadLabel} -> + SimEvent {seTime = SI.Time time, seThreadId, seThreadLabel} -> ( Max (length (show time)) , Max (length (show (seThreadId))) , Max (length seThreadLabel) ) - SimPOREvent {seTime = Time time, seThreadId, seThreadLabel} -> + SimPOREvent {seTime = SI.Time time, seThreadId, seThreadLabel} -> ( Max (length (show time)) , Max (length (show (seThreadId))) , Max (length seThreadLabel) @@ -935,7 +977,7 @@ -- | Like 'ppTrace' but does not show the result value. -- -ppTrace_ :: SimTrace a -> String +ppTrace_ :: Trace.Trace a SimEvent -> String ppTrace_ tr = Trace.ppTrace (const "") (ppSimEvent timeWidth tidWidth labelWidth) @@ -971,13 +1013,13 @@ . Trace.toList -pattern SimTrace :: Time -> IOSimThreadId -> Maybe ThreadLabel -> SimEventType -> SimTrace a +pattern SimTrace :: SI.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 -> IOSimThreadId -> Int -> Maybe ThreadLabel -> SimEventType -> SimTrace a +pattern SimPORTrace :: SI.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) @@ -989,15 +1031,15 @@ Trace.Cons (SimRacesFound controls) trace -pattern TraceMainReturn :: Time -> Labelled IOSimThreadId -> a -> [Labelled IOSimThreadId] +pattern TraceMainReturn :: SI.Time -> Labelled IOSimThreadId -> a -> [Labelled IOSimThreadId] -> SimTrace a pattern TraceMainReturn time tid a threads = Trace.Nil (MainReturn time tid a threads) -pattern TraceMainException :: Time -> Labelled IOSimThreadId -> SomeException -> [Labelled IOSimThreadId] +pattern TraceMainException :: SI.Time -> Labelled IOSimThreadId -> SomeException -> [Labelled IOSimThreadId] -> SimTrace a pattern TraceMainException time tid err threads = Trace.Nil (MainException time tid err threads) -pattern TraceDeadlock :: Time -> [Labelled IOSimThreadId] +pattern TraceDeadlock :: SI.Time -> [Labelled IOSimThreadId] -> SimTrace a pattern TraceDeadlock time threads = Trace.Nil (Deadlock time threads) @@ -1014,9 +1056,13 @@ -- data SimEventType = EventSay String - -- ^ hold value of `say` + -- ^ holds value of `say` + | EventSayEvaluationError SomeException + -- ^ holds error resulted from evaluation of the expression passed to `say` to NF. | EventLog Dynamic - -- ^ hold a dynamic value of `Control.Monad.IOSim.traceM` + -- ^ holds a dynamic value of `Control.Monad.IOSim.traceM` + | EventLogEvaluationError SomeException + -- ^ holds error resulted from evaluation of the expression passed to `traceM` to WHNF. | EventMask MaskingState -- ^ masking state changed @@ -1031,6 +1077,8 @@ | EventThrowToUnmasked (Labelled IOSimThreadId) -- ^ a target thread of `throwTo` unmasked its exceptions, this is paired -- with `EventThrowToWakeup` for threads which were blocked on `throwTo` + | EventEvaluationError SomeException + | EventEvaluationSuccess | EventThreadForked IOSimThreadId -- ^ forked a thread @@ -1039,6 +1087,9 @@ | EventThreadUnhandled SomeException -- ^ thread terminated by an unhandled exception + | EventUniqueCreated Integer + -- ^ created the n-th 'Unique' + -- -- STM events -- @@ -1063,22 +1114,22 @@ -- Timeouts, Timers & Delays -- - | EventThreadDelay TimeoutId Time + | EventThreadDelay TimeoutId SI.Time -- ^ thread delayed | EventThreadDelayFired TimeoutId -- ^ thread woken up after a delay - | EventTimeoutCreated TimeoutId IOSimThreadId Time + | EventTimeoutCreated TimeoutId IOSimThreadId SI.Time -- ^ new timeout created (via `timeout`) | EventTimeoutFired TimeoutId -- ^ timeout fired - | EventRegisterDelayCreated TimeoutId TVarId Time + | EventRegisterDelayCreated TimeoutId TVarId SI.Time -- ^ registered delay (via `registerDelay`) | EventRegisterDelayFired TimeoutId -- ^ registered delay fired - | EventTimerCreated TimeoutId TVarId Time + | EventTimerCreated TimeoutId TVarId SI.Time -- ^ a new 'Timeout' created (via `newTimeout`) | EventTimerCancelled TimeoutId -- ^ a 'Timeout' was cancelled (via `cancelTimeout`) @@ -1127,18 +1178,33 @@ -- a simulation. Useful for debugging IOSimPOR. deriving Show +unsafeEvaluateString :: String -> String -> String +unsafeEvaluateString name a = unsafePerformIO $ + catchJust + (\e -> case fromException @SomeAsyncException e of + Just{} -> Nothing + Nothing -> Just e + ) + (evaluate (force a)) + (\(e :: SomeException) -> return ("- error evaluating " ++ name ++ ": " ++ show e)) + + ppSimEventType :: SimEventType -> String ppSimEventType = \case EventSay a -> "Say " ++ a + EventSayEvaluationError err -> "SayEvaluationError " ++ show err EventLog a -> "Dynamic " ++ show a + EventLogEvaluationError err -> "DynamicEvaluationError " ++ show err EventMask a -> "Mask " ++ show a - EventThrow a -> "Throw " ++ show a + EventThrow err -> "Throw " ++ unsafeEvaluateString "exception" (show err) EventThrowTo err tid -> concat [ "ThrowTo (", - show err, ") ", + unsafeEvaluateString "exception" (show err), ") ", ppIOSimThreadId tid ] EventThrowToBlocked -> "ThrowToBlocked" EventThrowToWakeup -> "ThrowToWakeup" + EventEvaluationError err -> "EvaluationError " ++ show err + EventEvaluationSuccess -> "EvaluationSuccess" EventThrowToUnmasked a -> "ThrowToUnmasked " ++ ppLabelled ppIOSimThreadId a EventThreadForked a -> @@ -1146,6 +1212,7 @@ EventThreadFinished -> "ThreadFinished" EventThreadUnhandled a -> "ThreadUnhandled " ++ show a + EventUniqueCreated n -> "UniqueCreated " ++ show n EventTxCommitted written created mbEff -> concat [ "TxCommitted ", ppList (ppLabelled show) written, " ", @@ -1209,22 +1276,7 @@ ppEffect eff ] EventRaces a -> show a --- | A labelled value. -- --- For example 'labelThread' or `labelTVar' will insert a label to `IOSimThreadId` --- (or `TVarId`). -data Labelled a = Labelled { - l_labelled :: !a, - l_label :: !(Maybe String) - } - 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 -- @@ -1248,7 +1300,7 @@ ![SomeTVar s] -- ^ created tvars ![Dynamic] ![String] - !TVarId -- updated TVarId name supply + !VarId -- updated TVarId name supply -- | A blocked transaction reports the vars that were read so that the -- scheduler can block the thread on those vars. diff --git a/src/Control/Monad/IOSimPOR/Internal.hs b/src/Control/Monad/IOSimPOR/Internal.hs --- a/src/Control/Monad/IOSimPOR/Internal.hs +++ b/src/Control/Monad/IOSimPOR/Internal.hs @@ -1,1843 +1,1943 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTSyntax #-} -{-# 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 (..) - , runIOSim - , runSimTraceST - , traceM - , traceSTM - , STM - , STMSim - , setCurrentTime - , unshareClock - , TimeoutException (..) - , EventlogEvent (..) - , EventlogMarker (..) - , IOSimThreadId - , ThreadLabel - , Labelled (..) - , SimTrace - , Trace.Trace (SimPORTrace, TraceMainReturn, TraceMainException, TraceDeadlock) - , SimEvent (..) - , SimResult (..) - , SimEventType (..) - , liftST - , execReadTVar - , controlSimTraceST - , ScheduleControl (..) - , ScheduleMod (..) - ) where - -import Prelude hiding (read) - -import Data.Dynamic -import Data.Foldable (foldlM, traverse_) -import Data.List qualified as List -import Data.List.Trace qualified as Trace -import Data.Map.Strict (Map) -import Data.Map.Strict qualified as Map -import Data.Maybe (mapMaybe) -import Data.Ord -import Data.OrdPSQ (OrdPSQ) -import Data.OrdPSQ qualified as PSQ -import Data.Set (Set) -import Data.Set qualified as Set -import Data.Time (UTCTime (..), fromGregorian) - -import Control.Exception (NonTermination (..), assert, throw) -import Control.Monad (join, when) -import Control.Monad.ST.Lazy -import Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST) -import Data.STRef.Lazy - -import Control.Concurrent.Class.MonadSTM.TMVar -import Control.Concurrent.Class.MonadSTM.TVar hiding (TVar) -import Control.Monad.Class.MonadFork (killThread, myThreadId, throwTo) -import Control.Monad.Class.MonadSTM hiding (STM) -import Control.Monad.Class.MonadSTM.Internal (TMVarDefault (TMVar)) -import Control.Monad.Class.MonadThrow as MonadThrow -import Control.Monad.Class.MonadTime -import Control.Monad.Class.MonadTimer.SI (TimeoutState (..)) - -import Control.Monad.IOSim.InternalTypes -import Control.Monad.IOSim.Types hiding (SimEvent (SimEvent), Trace (SimTrace)) -import Control.Monad.IOSim.Types (SimEvent) -import Control.Monad.IOSimPOR.Timeout (unsafeTimeout) -import Control.Monad.IOSimPOR.Types - --- --- Simulation interpreter --- - -data Thread s a = Thread { - 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 IOSimThreadId, VectorClock)], - threadClockId :: !ClockId, - threadLabel :: Maybe ThreadLabel, - threadNextTId :: !Int, - threadStep :: !Int, - threadVClock :: VectorClock, - threadEffect :: Effect, -- in the current step - threadRacy :: !Bool - } - deriving Show - -isThreadBlocked :: Thread s a -> Bool -isThreadBlocked t = case threadStatus t of - ThreadBlocked {} -> True - _ -> False - -isThreadDone :: Thread s a -> Bool -isThreadDone t = case threadStatus t of - ThreadDone -> True - _ -> False - -threadStepId :: Thread s a -> (IOSimThreadId, Int) -threadStepId Thread{ threadId, threadStep } = (threadId, threadStep) - -isRacyThreadId :: IOSimThreadId -> Bool -isRacyThreadId (RacyThreadId _) = True -isRacyThreadId _ = True - -isNotRacyThreadId :: IOSimThreadId -> Bool -isNotRacyThreadId (ThreadId _) = True -isNotRacyThreadId _ = False - -bottomVClock :: VectorClock -bottomVClock = VectorClock Map.empty - -insertVClock :: IOSimThreadId -> Int -> VectorClock -> VectorClock -insertVClock tid !step (VectorClock m) = VectorClock (Map.insert tid step m) - -leastUpperBoundVClock :: VectorClock -> VectorClock -> VectorClock -leastUpperBoundVClock (VectorClock m) (VectorClock m') = - VectorClock (Map.unionWith max m m') - --- hbfVClock :: VectorClock -> VectorClock -> Bool --- hbfVClock (VectorClock m) (VectorClock m') = Map.isSubmapOfBy (<=) m m' - -happensBeforeStep :: Step -- ^ an earlier step - -> Step -- ^ a later step - -> Bool -happensBeforeStep step step' = - Just (stepStep step) - <= Map.lookup (stepThreadId step) - (getVectorClock $ stepVClock step') - -labelledTVarId :: TVar s a -> ST s (Labelled TVarId) -labelledTVarId TVar { tvarId, tvarLabel } = Labelled tvarId <$> readSTRef tvarLabel - -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. - -- TODO: https://github.com/haskell/containers/issues/749 - Map.foldr' - (\Thread { threadId, threadLabel } !acc -> Labelled threadId threadLabel : acc) - [] threadMap - - --- | Timers mutable variables. First one supports 'newTimeout' api, the second --- one 'Control.Monad.Class.MonadTimer.SI.registerDelay', the third one --- 'Control.Monad.Class.MonadTimer.SI.threadDelay'. --- -data TimerCompletionInfo s = - Timer !(TVar s TimeoutState) - -- ^ `newTimeout` timer. - | TimerRegisterDelay !(TVar s Bool) - -- ^ `registerDelay` timer. - | TimerThreadDelay !IOSimThreadId !TimeoutId - -- ^ `threadDelay` timer run by `IOSimThreadId` which was assigned the given - -- `TimeoutId` (only used to report in a trace). - | 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 IOSimThreadId) (Down IOSimThreadId) () -type Timeouts s = OrdPSQ TimeoutId Time (TimerCompletionInfo s) - --- | Internal state. --- -data SimState s a = SimState { - runqueue :: !RunQueue, - -- | All threads other than the currently running thread: both running - -- and blocked threads. - threads :: !(Map IOSimThreadId (Thread s a)), - -- | current time - curTime :: !Time, - -- | ordered list of timers and timeouts - timers :: !(Timeouts s), - -- | timeout locks in order to synchronize the timeout handler and the - -- main thread - clocks :: !(Map ClockId UTCTime), - nextVid :: !TVarId, -- ^ next unused 'TVarId' - nextTmid :: !TimeoutId, -- ^ next unused 'TimeoutId' - -- | previous steps (which we may race with). - -- Note this is *lazy*, so that we don't compute races we will not reverse. - races :: Races, - -- | control the schedule followed, and initial value - control :: !ScheduleControl, - control0 :: !ScheduleControl, - -- | limit on the computation time allowed per scheduling step, for - -- catching infinite loops etc - perStepTimeLimit :: Maybe Int - - } - -initialState :: SimState s a -initialState = - SimState { - runqueue = PSQ.empty, - threads = Map.empty, - curTime = Time 0, - timers = PSQ.empty, - clocks = Map.singleton (ClockId []) epoch1970, - nextVid = TVarId 0, - nextTmid = TimeoutId 0, - races = noRaces, - control = ControlDefault, - control0 = ControlDefault, - perStepTimeLimit = Nothing - } - where - epoch1970 = UTCTime (fromGregorian 1970 1 1) 0 - -invariant :: Maybe (Thread s a) -> SimState s a -> x -> x - -invariant (Just running) simstate@SimState{runqueue,threads,clocks} = - assert (not (isThreadBlocked running)) - . assert (threadId running `Map.notMember` threads) - . assert (not (Down (threadId running) `PSQ.member` runqueue)) - . assert (threadClockId running `Map.member` clocks) - . invariant Nothing simstate - -invariant Nothing SimState{runqueue,threads,clocks} = - assert (PSQ.fold' (\(Down tid) _ _ a -> tid `Map.member` threads && a) True runqueue) - . assert (and [ (isThreadBlocked t || isThreadDone t) == not (Down (threadId t) `PSQ.member` runqueue) - | t <- Map.elems threads ]) - . assert (and (zipWith (\(Down tid, _, _) (Down tid', _, _) -> tid > tid') - (PSQ.toList runqueue) - (drop 1 (PSQ.toList runqueue)))) - . assert (and [ threadClockId t `Map.member` clocks - | t <- Map.elems threads ]) - --- | Interpret the simulation monotonic time as a 'NominalDiffTime' since --- the start. -timeSinceEpoch :: Time -> NominalDiffTime -timeSinceEpoch (Time t) = fromRational (toRational t) - - --- | Insert thread into `runqueue`. --- -insertThread :: Thread s a -> RunQueue -> RunQueue -insertThread Thread { threadId } = PSQ.insert (Down threadId) (Down threadId) () - - --- | Schedule / run a thread. --- -schedule :: forall s a. Thread s a -> SimState s a -> ST s (SimTrace a) -schedule thread@Thread{ - threadId = tid, - threadControl = ThreadControl action ctl, - threadMasking = maskst, - threadLabel = tlbl, - threadStep = tstep, - threadVClock = vClock, - threadEffect = effect - } - simstate@SimState { - runqueue, - threads, - timers, - clocks, - nextVid, nextTmid, - curTime = time, - control, - perStepTimeLimit - } - - | controlTargets (tid,tstep) control = - -- The next step is to be delayed according to the - -- specified schedule. Switch to following the schedule. - SimPORTrace time tid tstep tlbl (EventFollowControl control) <$> - schedule thread simstate{ control = followControl control } - - | not $ controlFollows (tid,tstep) control = - -- the control says this is not the next step to - -- follow. We should be at the beginning of a step; - -- we put the present thread to sleep and reschedule - -- the correct thread. - -- The assertion says that the only effect that may have - -- happened in the start of a thread is us waking up. - ( SimPORTrace time tid tstep tlbl (EventAwaitControl (tid,tstep) control) - . SimPORTrace time tid tstep tlbl (EventDeschedule Sleep) - ) <$> deschedule Sleep thread simstate - - | otherwise = - invariant (Just thread) simstate $ - case control of - ControlFollow (s:_) _ - -> fmap (SimPORTrace time tid tstep tlbl (EventPerformAction (tid,tstep))) - _ -> id - $ - -- The next line forces the evaluation of action, which should be unevaluated up to - -- this point. This is where we actually *run* user code. - case maybe Just unsafeTimeout perStepTimeLimit action of - Nothing -> return TraceLoop - Just _ -> case action of - - Return x -> case ctl of - MainFrame -> - -- the main thread is done, so we're done - -- even if other threads are still running - return $ SimPORTrace time tid tstep tlbl EventThreadFinished - $ traceFinalRacesFound simstate - $ TraceMainReturn time (Labelled tid tlbl) x - ( labelledThreads - . Map.filter (not . isThreadDone) - $ threads - ) - - ForkFrame -> do - -- this thread is done - let thread' = thread - !trace <- deschedule Terminated thread' simstate - return $ SimPORTrace time tid tstep tlbl EventThreadFinished - $ SimPORTrace time tid tstep tlbl (EventDeschedule Terminated) - $ trace - - MaskFrame k maskst' ctl' -> do - -- pop the control stack, restore thread-local state - let thread' = thread { threadControl = ThreadControl (k x) ctl' - , threadMasking = maskst' - } - -- but if we're now unmasked, check for any pending async exceptions - !trace <- deschedule Interruptable thread' simstate - return $ SimPORTrace time tid tstep tlbl (EventMask maskst') - $ SimPORTrace time tid tstep tlbl (EventDeschedule Interruptable) - $ trace - - CatchFrame _handler k ctl' -> do - -- pop the control stack and continue - let thread' = thread { threadControl = ThreadControl (k x) ctl' } - schedule thread' simstate - - TimeoutFrame tmid lock k ctl' -> do - -- It could happen that the timeout action finished at the same time - -- as the timeout expired, this will be a race condition. That's why - -- we have the locks to solve this. - - -- We cannot do `tryPutMVar` in the `treadAction`, because we need to - -- know if the `lock` is empty right now when we still have the frame. - v <- execTryPutTMVar lock undefined - let -- Kill the assassin throwing thread then unmask exceptions and - -- carry on the continuation - threadAction :: IOSim s () - threadAction = - if v then unsafeUnregisterTimeout tmid - else atomically (takeTMVar lock) >>= killThread - - thread' = - thread { threadControl = - ThreadControl (case threadAction of - IOSim k' -> k' (\() -> k (Just x))) - ctl' - } - schedule thread' simstate - - DelayFrame tmid k ctl' -> do - let thread' = thread { threadControl = ThreadControl k ctl' } - timers' = PSQ.delete tmid timers - schedule thread' simstate { timers = timers' } - - Throw e -> case unwindControlStack e thread timers of - -- Found a CatchFrame - (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', 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') $ - 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 - -- have an unhandled exception at the top level of the thread. - | isMain -> do - let thread' = thread { threadStatus = ThreadDone } - -- An unhandled exception in the main thread terminates the program - 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 (Labelled tid tlbl) e (labelledThreads threads)) - - | otherwise -> do - -- An unhandled exception in any other thread terminates the thread - let terminated = Terminated - !trace <- deschedule terminated thread simstate { timers = timers'' } - return $ SimPORTrace time tid tstep tlbl (EventThrow e) - $ SimPORTrace time tid tstep tlbl (EventThreadUnhandled e) - $ SimPORTrace time tid tstep tlbl (EventDeschedule terminated) - $ trace - - Catch action' handler k -> do - -- push the failure and success continuations onto the control stack - let thread' = thread { threadControl = ThreadControl action' - (CatchFrame handler k ctl) - } - schedule thread' simstate - - Evaluate expr k -> do - mbWHNF <- unsafeIOToST $ try $ evaluate expr - case mbWHNF of - Left e -> do - -- schedule this thread to immediately raise the exception - let thread' = thread { threadControl = ThreadControl (Throw e) ctl } - schedule thread' simstate - Right whnf -> do - -- continue with the resulting WHNF - let thread' = thread { threadControl = ThreadControl (k whnf) ctl } - schedule thread' simstate - - Say msg k -> do - let thread' = thread { threadControl = ThreadControl k ctl } - trace <- schedule thread' simstate - return (SimPORTrace time tid tstep tlbl (EventSay msg) trace) - - Output x k -> do - let thread' = thread { threadControl = ThreadControl k ctl } - trace <- schedule thread' simstate - return (SimPORTrace time tid tstep tlbl (EventLog x) trace) - - LiftST st k -> do - x <- strictToLazyST st - let thread' = thread { threadControl = ThreadControl (k x) ctl } - schedule thread' simstate - - GetMonoTime k -> do - let thread' = thread { threadControl = ThreadControl (k time) ctl } - schedule thread' simstate - - GetWallTime k -> do - let clockid = threadClockId thread - clockoff = clocks Map.! clockid - walltime = timeSinceEpoch time `addUTCTime` clockoff - thread' = thread { threadControl = ThreadControl (k walltime) ctl } - schedule thread' simstate - - SetWallTime walltime' k -> do - let clockid = threadClockId thread - clockoff = clocks Map.! clockid - walltime = timeSinceEpoch time `addUTCTime` clockoff - clockoff' = addUTCTime (diffUTCTime walltime' walltime) clockoff - thread' = thread { threadControl = ThreadControl k ctl } - simstate' = simstate { clocks = Map.insert clockid clockoff' clocks } - schedule thread' simstate' - - UnshareClock k -> do - let clockid = threadClockId thread - clockoff = clocks Map.! clockid - clockid' = let ThreadId i = tid in ClockId i -- reuse the thread id - thread' = thread { threadControl = ThreadControl k ctl - , threadClockId = clockid' } - simstate' = simstate { clocks = Map.insert clockid' clockoff clocks } - schedule thread' simstate' - - -- This case is guarded by checks in 'timeout' itself. - StartTimeout d _ _ | d <= 0 -> - error "schedule: StartTimeout: Impossible happened" - - StartTimeout d action' k -> do - lock <- TMVar <$> execNewTVar nextVid (Just $! "lock-" ++ show nextTmid) Nothing - let expiry = d `addTime` time - timers' = PSQ.insert nextTmid expiry (TimerTimeout tid nextTmid lock) timers - thread' = thread { threadControl = - ThreadControl action' - (TimeoutFrame nextTmid lock k ctl) - } - trace <- deschedule Yield thread' simstate { timers = timers' - , nextTmid = succ nextTmid } - return (SimPORTrace time tid tstep tlbl (EventTimeoutCreated nextTmid tid expiry) trace) - - UnregisterTimeout tmid k -> do - let thread' = thread { threadControl = ThreadControl k ctl } - schedule thread' simstate { timers = PSQ.delete tmid timers } - - RegisterDelay d k | d < 0 -> do - tvar <- execNewTVar nextVid - (Just $! "<>") - True - modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) - let !expiry = d `addTime` time - !thread' = thread { threadControl = ThreadControl (k tvar) ctl } - trace <- schedule thread' simstate { nextVid = succ nextVid } - return (SimPORTrace time tid tstep tlbl (EventRegisterDelayCreated nextTmid nextVid expiry) $ - SimPORTrace time tid tstep tlbl (EventRegisterDelayFired nextTmid) $ - trace) - - RegisterDelay d k -> do - tvar <- execNewTVar nextVid - (Just $! "<>") - False - modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) - let !expiry = d `addTime` time - !timers' = PSQ.insert nextTmid expiry (TimerRegisterDelay tvar) timers - !thread' = thread { threadControl = ThreadControl (k tvar) ctl } - trace <- schedule thread' simstate { timers = timers' - , nextVid = succ nextVid - , nextTmid = succ nextTmid } - return (SimPORTrace time tid tstep tlbl - (EventRegisterDelayCreated nextTmid nextVid expiry) trace) - - ThreadDelay d k | d < 0 -> do - let expiry = d `addTime` time - thread' = thread { threadControl = ThreadControl (Return ()) (DelayFrame nextTmid k ctl) } - simstate' = simstate { nextTmid = succ nextTmid } - trace <- schedule thread' simstate' - return (SimPORTrace time tid tstep tlbl (EventThreadDelay nextTmid expiry) $ - SimPORTrace time tid tstep tlbl (EventThreadDelayFired nextTmid) $ - trace) - - ThreadDelay d k -> do - 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 BlockedOnDelay) thread' - simstate { timers = timers', - nextTmid = succ nextTmid } - return (SimPORTrace time tid tstep tlbl (EventThreadDelay nextTmid expiry) trace) - - -- we treat negative timers as cancelled ones; for the record we put - -- `EventTimerCreated` and `EventTimerCancelled` in the trace; This differs - -- from `GHC.Event` behaviour. - NewTimeout d k | d < 0 -> do - let t = NegativeTimeout nextTmid - expiry = d `addTime` time - thread' = thread { threadControl = ThreadControl (k t) ctl } - trace <- schedule thread' simstate { nextTmid = succ nextTmid } - return (SimPORTrace time tid tstep tlbl (EventTimerCreated nextTmid nextVid expiry) $ - SimPORTrace time tid tstep tlbl (EventTimerCancelled nextTmid) $ - trace) - - NewTimeout d k -> do - tvar <- execNewTVar nextVid - (Just $! "<>") - TimeoutPending - modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) - let expiry = d `addTime` time - t = Timeout tvar nextTmid - timers' = PSQ.insert nextTmid expiry (Timer tvar) timers - thread' = thread { threadControl = ThreadControl (k t) ctl } - trace <- schedule thread' simstate { timers = timers' - , nextVid = succ (succ nextVid) - , nextTmid = succ nextTmid } - return (SimPORTrace time tid tstep tlbl (EventTimerCreated nextTmid nextVid expiry) trace) - - CancelTimeout (Timeout tvar tmid) k -> do - let timers' = PSQ.delete tmid timers - written <- execAtomically' (runSTM $ writeTVar tvar TimeoutCancelled) - (wakeup, wokeby) <- threadsUnblockedByWrites written - mapM_ (\(SomeTVar var) -> unblockAllThreadsFromTVar var) written - let effect' = effect - <> writeEffects written - <> wakeupEffects wakeup - thread' = thread { threadControl = ThreadControl k ctl - , threadEffect = effect' - } - (unblocked, - simstate') = unblockThreads False vClock wakeup simstate - modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) - !trace <- deschedule Yield thread' simstate' { timers = timers' } - return $ SimPORTrace time tid tstep tlbl (EventTimerCancelled tmid) - $ traceMany - -- TODO: step - [ (time, tid', (-1), tlbl', EventTxWakeup vids) - | tid' <- unblocked - , let tlbl' = lookupThreadLabel tid' threads - , let Just vids = Set.toList <$> Map.lookup tid' wokeby ] - $ SimPORTrace time tid tstep tlbl (EventDeschedule Yield) - $ trace - - -- cancelling a negative timer is a no-op - CancelTimeout (NegativeTimeout _tmid) k -> do - -- negative timers are promptly removed from the state - let thread' = thread { threadControl = ThreadControl k ctl } - schedule thread' simstate - - Fork a k -> do - let nextTId = threadNextTId thread - tid' | threadRacy thread = setRacyThread $ childThreadId tid nextTId - | otherwise = childThreadId tid nextTId - thread' = thread { threadControl = ThreadControl (k tid') ctl, - threadNextTId = nextTId + 1, - threadEffect = effect - <> forkEffect tid' - } - thread'' = Thread { threadId = tid' - , threadControl = ThreadControl (runIOSim a) - ForkFrame - , threadStatus = ThreadRunning - , threadMasking = threadMasking thread - , threadThrowTo = [] - , threadClockId = threadClockId thread - , threadLabel = Nothing - , threadNextTId = 1 - , threadStep = 0 - , threadVClock = insertVClock tid' 0 - $ vClock - , threadEffect = mempty - , threadRacy = threadRacy thread - } - threads' = Map.insert tid' thread'' threads - -- A newly forked thread may have a higher priority, so we deschedule this one. - !trace <- deschedule Yield thread' - simstate { runqueue = insertThread thread'' runqueue - , threads = threads' } - return $ SimPORTrace time tid tstep tlbl (EventThreadForked tid') - $ SimPORTrace time tid tstep tlbl (EventDeschedule Yield) - $ trace - - Atomically a k -> execAtomically time tid tlbl nextVid (runSTM a) $ \res -> - case res of - StmTxCommitted x written read created - tvarDynamicTraces tvarStringTraces nextVid' -> do - (wakeup, wokeby) <- threadsUnblockedByWrites written - mapM_ (\(SomeTVar tvar) -> unblockAllThreadsFromTVar tvar) written - vClockRead <- leastUpperBoundTVarVClocks read - let vClock' = vClock `leastUpperBoundVClock` vClockRead - effect' = effect - <> readEffects read - <> writeEffects written - <> wakeupEffects unblocked - thread' = thread { threadControl = ThreadControl (k x) ctl, - threadVClock = vClock', - threadEffect = effect' } - (unblocked, - simstate') = unblockThreads True vClock' wakeup simstate - sequence_ [ modifySTRef (tvarVClock r) (leastUpperBoundVClock vClock') - | SomeTVar r <- created ++ written ] - written' <- traverse (\(SomeTVar tvar) -> labelledTVarId tvar) written - created' <- traverse (\(SomeTVar tvar) -> labelledTVarId tvar) created - -- We deschedule a thread after a transaction... another may have woken up. - !trace <- deschedule Yield thread' simstate' { nextVid = nextVid' } - return $ - SimPORTrace time tid tstep tlbl (EventTxCommitted written' created' (Just effect')) $ - traceMany - [ (time, tid', (-1), tlbl', EventTxWakeup vids') - | tid' <- unblocked - , let tlbl' = lookupThreadLabel tid' threads - , let Just vids' = Set.toList <$> Map.lookup tid' wokeby ] $ - traceMany - [ (time, tid, tstep, tlbl, EventLog tr) - | tr <- tvarDynamicTraces - ] $ - traceMany - [ (time, tid, tstep, tlbl, EventSay str) - | str <- tvarStringTraces - ] $ - SimPORTrace time tid tstep tlbl (EventUnblocked unblocked) $ - SimPORTrace time tid tstep tlbl (EventDeschedule Yield) $ - trace - - StmTxAborted read e -> do - -- schedule this thread to immediately raise the exception - vClockRead <- leastUpperBoundTVarVClocks read - let effect' = effect <> readEffects read - thread' = thread { threadControl = ThreadControl (Throw e) ctl, - threadVClock = vClock `leastUpperBoundVClock` vClockRead, - threadEffect = effect' } - trace <- schedule thread' simstate - return $ SimPORTrace time tid tstep tlbl (EventTxAborted (Just effect')) - $ trace - - StmTxBlocked read -> do - mapM_ (\(SomeTVar tvar) -> blockThreadOnTVar tid tvar) read - vids <- traverse (\(SomeTVar tvar) -> labelledTVarId tvar) read - vClockRead <- leastUpperBoundTVarVClocks read - let effect' = effect <> readEffects read - thread' = thread { threadVClock = vClock `leastUpperBoundVClock` vClockRead, - threadEffect = effect' } - !trace <- deschedule (Blocked BlockedOnSTM) thread' simstate - return $ SimPORTrace time tid tstep tlbl (EventTxBlocked vids (Just effect')) - $ SimPORTrace time tid tstep tlbl (EventDeschedule (Blocked BlockedOnSTM)) - $ trace - - GetThreadId k -> do - let thread' = thread { threadControl = ThreadControl (k tid) ctl } - schedule thread' simstate - - LabelThread tid' l k | tid' == tid -> do - let thread' = thread { threadControl = ThreadControl k ctl - , threadLabel = Just l } - schedule thread' simstate - - LabelThread tid' l k -> do - let thread' = thread { threadControl = ThreadControl k ctl } - threads' = Map.adjust (\t -> t { threadLabel = Just l }) tid' threads - schedule thread' simstate { threads = threads' } - - ExploreRaces k -> do - let thread' = thread { threadControl = ThreadControl k ctl - , threadRacy = True } - schedule thread' simstate - - Fix f k -> do - r <- newSTRef (throw NonTermination) - x <- unsafeInterleaveST $ readSTRef r - let k' = unIOSim (f x) $ \x' -> - LiftST (lazyToStrictST (writeSTRef r x')) (\() -> k x') - thread' = thread { threadControl = ThreadControl k' ctl } - schedule thread' simstate - - GetMaskState k -> do - let thread' = thread { threadControl = ThreadControl (k maskst) ctl } - schedule thread' simstate - - SetMaskState maskst' action' k -> do - let thread' = thread { threadControl = ThreadControl - (runIOSim action') - (MaskFrame k maskst ctl) - , threadMasking = maskst' } - trace <- - case maskst' of - -- If we're now unmasked then check for any pending async exceptions - Unmasked -> SimPORTrace time tid tstep tlbl (EventDeschedule Interruptable) - <$> deschedule Interruptable thread' simstate - _ -> schedule thread' simstate - return $ SimPORTrace time tid tstep tlbl (EventMask maskst') - $ trace - - ThrowTo e tid' _ | tid' == tid -> do - -- Throw to ourself is equivalent to a synchronous throw, - -- and works irrespective of masking state since it does not block. - let thread' = thread { threadControl = ThreadControl (Throw e) ctl - , threadEffect = effect - } - trace <- schedule thread' simstate - return (SimPORTrace time tid tstep tlbl (EventThrowTo e tid) trace) - - ThrowTo e tid' k -> do - let thread' = thread { threadControl = ThreadControl k ctl, - threadEffect = effect <> throwToEffect tid' - <> wakeUpEffect, - threadVClock = vClock `leastUpperBoundVClock` vClockTgt - } - (vClockTgt, - wakeUpEffect, - willBlock) = (threadVClock t, - if isThreadBlocked t then wakeupEffects [tid'] else mempty, - not (threadInterruptible t || isThreadDone t)) - where Just t = Map.lookup tid' threads - - if willBlock - then do - -- The target thread has async exceptions masked so we add the - -- exception and the source thread id to the pending async exceptions. - let adjustTarget t = - t { threadThrowTo = (e, Labelled tid tlbl, vClock) : threadThrowTo t } - threads' = Map.adjust adjustTarget tid' 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 BlockedOnThrowTo)) - $ trace - else do - -- The target thread has async exceptions unmasked, or is masked but - -- is blocked (and all blocking operations are interruptible) then we - -- raise the exception in that thread immediately. This will either - -- cause it to terminate or enter an exception handler. - -- In the meantime the thread masks new async exceptions. This will - -- be resolved if the thread terminates or if it leaves the exception - -- handler (when restoring the masking state would trigger the any - -- new pending async exception). - let adjustTarget t@Thread{ threadControl = ThreadControl _ ctl', - threadVClock = vClock' } = - t { threadControl = ThreadControl (Throw e) ctl' - , threadStatus = if isThreadDone t - then threadStatus t - else ThreadRunning - , threadVClock = vClock' `leastUpperBoundVClock` vClock } - (_unblocked, simstate'@SimState { threads = threads' }) = unblockThreads False vClock [tid'] simstate - threads'' = Map.adjust adjustTarget tid' threads' - simstate'' = simstate' { threads = threads'' } - - -- We yield at this point because the target thread may be higher - -- priority, so this should be a step for race detection. - trace <- deschedule Yield thread' simstate'' - return $ SimPORTrace time tid tstep tlbl (EventThrowTo e tid') - $ trace - - -- intentionally a no-op (at least for now) - YieldSim k -> do - let thread' = thread { threadControl = ThreadControl k ctl } - schedule thread' simstate - - -threadInterruptible :: Thread s a -> Bool -threadInterruptible thread = - case threadMasking thread of - Unmasked -> True - MaskedInterruptible - | isThreadBlocked thread -> True -- blocking operations are interruptible - | otherwise -> False - MaskedUninterruptible -> False - -deschedule :: Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a) - -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', 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 = races', - control = control' } - -deschedule Interruptable thread@Thread { - threadId = tid, - threadStep = tstep, - threadControl = ThreadControl _ ctl, - threadMasking = Unmasked, - threadThrowTo = (e, tid', vClock') : etids, - threadLabel = tlbl, - threadVClock = vClock, - threadEffect = effect - } - simstate@SimState{ curTime = time, threads } = do - - 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 (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, - 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', 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 = races', - control = advanceControl (threadStepId thread) control } - -deschedule (Blocked _blockedReason) thread@Thread { threadId = tid - , threadStep = tstep - , threadLabel = tlbl - , threadThrowTo = _ : _ - , threadMasking = maskst - , 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. - SimPORTrace time tid tstep tlbl (EventDeschedule Interruptable) <$> - deschedule Interruptable thread { threadMasking = Unmasked } simstate - -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 = races', - control = advanceControl (threadStepId thread1) control } - -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 wakeup = map (\(_,tid',_) -> l_labelled tid') (reverse (threadThrowTo thread)) - (unblocked, - simstate'@SimState{threads}) = - unblockThreads False vClock wakeup simstate - 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 = races', - control = advanceControl (threadStepId thread) control, - threads = threads' } - return $ traceMany - -- TODO: step - [ (time, tid', (-1), tlbl', EventThrowToWakeup) - | tid' <- unblocked - , let tlbl' = lookupThreadLabel tid' threads ] - $ SimPORTrace time tid tstep tlbl (EventEffect vClock eff) - $ SimPORTrace time tid tstep tlbl (EventRaces races') - trace - -deschedule Sleep thread@Thread { threadId = tid , threadEffect = effect' } - simstate@SimState{runqueue, threads} = - - -- Schedule control says we should run a different thread. Put - -- this one to sleep without recording a step. - - let runqueue' = insertThread thread runqueue - threads' = Map.insert tid thread threads in - reschedule simstate { runqueue = runqueue', threads = threads' } - - --- Choose the next thread to run. -reschedule :: SimState s a -> ST s (SimTrace a) - --- If we are following a controlled schedule, just do that. -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)) $ - invariant Nothing simstate $ - let thread = threads Map.! tid in - assert (threadId thread == tid) $ - --assert (threadStep thread == tstep) $ - if threadStep thread /= tstep then - error $ "Thread step out of sync\n" - ++ " runqueue: "++show runqueue++"\n" - ++ " follows: "++show tid++", step "++show tstep++"\n" - ++ " actual step: "++show (threadStep thread)++"\n" - ++ "Thread:\n" ++ show thread ++ "\n" - else - schedule thread simstate { runqueue = PSQ.delete (Down tid) runqueue - , threads = Map.delete tid threads } - --- When there is no current running thread but the runqueue is non-empty then --- schedule the next one to run. -reschedule simstate@SimState{ runqueue, threads } - | Just (Down !tid, _, _, runqueue') <- PSQ.minView runqueue = - invariant Nothing simstate $ - - let thread = threads Map.! tid in - schedule thread simstate { runqueue = runqueue' - , threads = Map.delete tid threads } - --- But when there are no runnable threads, we advance the time to the next --- timer event, or stop. -reschedule simstate@SimState{ threads, timers, curTime = time, races } = - invariant Nothing simstate $ - - -- time is moving on - --Debug.trace ("Rescheduling at "++show time++", "++ - --show (length (concatMap stepInfoRaces (activeRaces races++completeRaces races)))++" races") $ - - -- important to get all events that expire at this time - case removeMinimums timers of - Nothing -> return (traceFinalRacesFound simstate $ - TraceDeadlock time (labelledThreads threads)) - - Just (tmids, time', fired, timers') -> assert (time' >= time) $ do - - -- 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 - - let wakeupThreadDelay = [ (tid, tmid) | TimerThreadDelay tid tmid <- fired ] - -- TODO: the vector clock below cannot be right, can it? - !simstate' = - snd . unblockThreads False bottomVClock (fst `fmap` wakeupThreadDelay) - . snd . unblockThreads True bottomVClock wakeupSTM - $ simstate - - -- For each 'timeout' action where the timeout has fired, start a - -- new thread to execute throwTo to interrupt the action. - !timeoutExpired = [ (tid, tmid, lock) - | TimerTimeout tid tmid lock <- fired ] - - -- all open races will be completed and reported at this time - !simstate'' <- forkTimeoutInterruptThreads timeoutExpired - simstate' { races = noRaces } - !trace <- reschedule simstate'' { curTime = time' - , timers = timers' } - let traceEntries = - [ ( time', ThreadId [-1], -1, Just "timer" - , EventTimerFired tmid) - | (tmid, Timer _) <- zip tmids fired ] - ++ [ ( 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 - , let Just vids = Set.toList <$> Map.lookup tid' wokeby ] - ++ [ ( time', tid, -1, Just "thread delay timer" - , EventThreadDelayFired tmid) - | (tid, tmid) <- wakeupThreadDelay ] - ++ [ ( time', tid, -1, Just "timeout timer" - , EventTimeoutFired tmid) - | (tid, tmid, _) <- timeoutExpired ] - ++ [ ( time', tid, -1, Just "forked thread" - , EventThreadForked tid) - | (tid, _, _) <- timeoutExpired ] - - return $ - traceFinalRacesFound simstate $ - traceMany traceEntries trace - where - timeoutAction (Timer var) = do - x <- readTVar var - case x of - TimeoutPending -> writeTVar var TimeoutFired - TimeoutFired -> error "MonadTimer(Sim): invariant violation" - TimeoutCancelled -> return () - timeoutAction (TimerRegisterDelay var) = writeTVar var True - timeoutAction (TimerThreadDelay _ _) = return () - timeoutAction (TimerTimeout _ _ _) = return () - -unblockThreads :: forall s a. - Bool -- ^ `True` if we are blocked on STM - -> VectorClock - -> [IOSimThreadId] - -> 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 - ( unblockedIds - , simstate { runqueue = foldr insertThread runqueue unblocked, - threads = threads' - }) - where - -- can only unblock if the thread exists and is blocked (not running) - unblocked :: [Thread s a] - !unblocked = [ thread - | tid <- wakeup - , thread <- - case Map.lookup tid threads of - Just Thread { threadStatus = ThreadRunning } - -> [ ] - Just t@Thread { threadStatus = ThreadBlocked BlockedOnSTM } - -> [t] - Just t@Thread { threadStatus = ThreadBlocked _ } - | onlySTM - -> [ ] - | otherwise - -> [t] - Just Thread { threadStatus = ThreadDone } -> [ ] - Nothing -> [ ] - ] - - unblockedIds :: [IOSimThreadId] - !unblockedIds = map threadId unblocked - - -- and in which case we mark them as now running - !threads' = List.foldl' - (flip (Map.adjust - (\t -> t { threadStatus = ThreadRunning, - threadVClock = vClock `leastUpperBoundVClock` threadVClock t }))) - threads unblockedIds - --- | This function receives a list of TimerTimeout values that represent threads --- for which the timeout expired and kills the running thread if needed. --- --- This function is responsible for the second part of the race condition issue --- and relates to the 'schedule's 'TimeoutFrame' locking explanation (here is --- where the assassin threads are launched. So, as explained previously, at this --- point in code, the timeout expired so we need to interrupt the running --- thread. If the running thread finished at the same time the timeout expired --- we have a race condition. To deal with this race condition what we do is --- look at the lock value. If it is 'Locked' this means that the running thread --- already finished (or won the race) so we can safely do nothing. Otherwise, if --- the lock value is 'NotLocked' we need to acquire the lock and launch an --- assassin thread that is going to interrupt the running one. Note that we --- should run this interrupting thread in an unmasked state since it might --- receive a 'ThreadKilled' exception. --- -forkTimeoutInterruptThreads :: forall s a. - [(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)] - -> SimState s a - -> ST s (SimState s a) -forkTimeoutInterruptThreads timeoutExpired simState = - foldlM (\st@SimState{ runqueue, threads } - (t, TMVar lock) - -> do - v <- execReadTVar lock - return $ case v of - Nothing -> st { runqueue = insertThread t runqueue, - threads = Map.insert (threadId t) t threads - } - Just _ -> st - ) - simState' - throwToThread - - where - -- we launch a thread responsible for throwing an AsyncCancelled exception - -- to the thread which timeout expired - throwToThread :: [(Thread s a, TMVar (IOSim s) IOSimThreadId)] - - (simState', throwToThread) = List.mapAccumR fn simState timeoutExpired - where - fn :: SimState s a - -> (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' - Nothing -> error ("IOSimPOR: internal error: unknown thread " ++ show tid) - nextId = threadNextTId t - tid' = childThreadId tid nextId - in ( state { threads = Map.insert tid t { threadNextTId = succ nextId } threads } - , ( Thread { threadId = tid', - threadControl = - ThreadControl - (runIOSim $ do - mtid <- myThreadId - v2 <- atomically $ tryPutTMVar lock mtid - when v2 $ - throwTo tid (toException (TimeoutException tmid))) - ForkFrame, - threadStatus = ThreadRunning, - threadMasking = Unmasked, - threadThrowTo = [], - threadClockId = threadClockId t, - threadLabel = Just "timeout-forked-thread", - threadNextTId = 1, - threadStep = 0, - threadVClock = insertVClock tid' 0 - $ threadVClock t, - threadEffect = mempty, - threadRacy = threadRacy t - } - , 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. --- --- Also return if it's the main thread or a forked thread since we handle the --- cases differently. --- -unwindControlStack :: forall s a. - SomeException - -> Thread s a - -> Timeouts s - -> ( Either Bool (Thread s a) - , Timeouts s - ) -unwindControlStack e thread = \timeouts -> - case threadControl thread of - ThreadControl _ ctl -> unwind (threadMasking thread) ctl timeouts - where - unwind :: forall s' c. MaskingState - -> ControlStack s' c a - -> Timeouts s - -> (Either Bool (Thread s' a), Timeouts s) - unwind _ MainFrame timers = (Left True, timers) - unwind _ ForkFrame timers = (Left False, timers) - unwind _ (MaskFrame _k maskst' ctl) timers = unwind maskst' ctl timers - - unwind maskst (CatchFrame handler k ctl) timers = - case fromException e of - -- not the right type, unwind to the next containing handler - Nothing -> unwind maskst ctl timers - - -- Ok! We will be able to continue the thread with the handler - -- followed by the continuation after the catch - Just e' -> ( Right thread { - -- As per async exception rules, the handler is run - -- masked - threadControl = ThreadControl (handler e') - (MaskFrame k maskst ctl), - threadMasking = atLeastInterruptibleMask maskst - } - , timers - ) - - -- Either Timeout fired or the action threw an exception. - -- - If Timeout fired, then it was possibly during this thread's execution - -- so we need to run the continuation with a Nothing value. - -- - If the timeout action threw an exception we need to keep unwinding the - -- control stack looking for a handler to this exception. - unwind maskst (TimeoutFrame tmid isLockedRef k ctl) timers = - case fromException e of - -- Exception came from timeout expiring - Just (TimeoutException tmid') | tmid == tmid' -> - (Right thread { threadControl = ThreadControl (k Nothing) ctl }, timers') - -- Exception came from a different exception - _ -> unwind maskst ctl timers' - where - -- Remove the timeout associated with the 'TimeoutFrame'. - timers' = PSQ.delete tmid timers - - unwind maskst (DelayFrame tmid _k ctl) timers = - unwind maskst ctl timers' - where - -- Remove the timeout associated with the 'DelayFrame'. - timers' = PSQ.delete tmid timers - - atLeastInterruptibleMask :: MaskingState -> MaskingState - atLeastInterruptibleMask Unmasked = MaskedInterruptible - atLeastInterruptibleMask ms = ms - - -removeMinimums :: (Ord k, Ord p) - => OrdPSQ k p a - -> Maybe ([k], p, [a], OrdPSQ k p a) -removeMinimums = \psq -> - case PSQ.minView psq of - Nothing -> Nothing - Just (k, p, x, psq') -> Just (collectAll [k] p [x] psq') - where - collectAll ks p xs psq = - case PSQ.minView psq of - Just (k, p', x, psq') - | p == p' -> collectAll (k:ks) p (x:xs) psq' - _ -> (reverse ks, p, reverse xs, psq) - -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 :: IOSimThreadId -> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel -lookupThreadLabel tid threads = join (threadLabel <$> Map.lookup tid threads) - - --- | The most general method of running 'IOSim' is in 'ST' monad. One can --- recover failures or the result from 'SimTrace' with 'traceResult', or access --- 'TraceEvent's generated by the computation with 'traceEvents'. A slightly --- more convenient way is exposed by 'runSimTrace'. --- -runSimTraceST :: forall s a. IOSim s a -> ST s (SimTrace a) -runSimTraceST mainAction = controlSimTraceST Nothing ControlDefault mainAction - -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) - <$> schedule mainThread initialState { control = control, - control0 = control, - perStepTimeLimit = limit - } - where - mainThread = - Thread { - threadId = ThreadId [], - threadControl = ThreadControl (runIOSim mainAction) MainFrame, - threadStatus = ThreadRunning, - threadMasking = Unmasked, - threadThrowTo = [], - threadClockId = ClockId [], - threadLabel = Just "main", - threadNextTId = 1, - threadStep = 0, - threadVClock = insertVClock (ThreadId []) 0 bottomVClock, - threadEffect = mempty, - threadRacy = False - } - - --- --- Executing STM Transactions --- - -execAtomically :: forall s a c. - Time - -> IOSimThreadId - -> Maybe ThreadLabel - -> TVarId - -> StmA s a - -> (StmTxResult s a -> ST s (SimTrace c)) - -> ST s (SimTrace c) -execAtomically !time !tid !tlbl !nextVid0 !action0 !k0 = - go AtomicallyFrame Map.empty Map.empty [] [] nextVid0 action0 - where - go :: forall b. - StmStack s b a - -> Map TVarId (SomeTVar s) -- set of vars read - -> Map TVarId (SomeTVar s) -- set of vars written - -> [SomeTVar s] -- vars written in order (no dups) - -> [SomeTVar s] -- vars created in order - -> TVarId -- var fresh name supply - -> StmA s b - -> ST s (SimTrace c) - go !ctl !read !written !writtenSeq !createdSeq !nextVid !action = - assert localInvariant $ - case action of - ReturnStm x -> - case ctl of - AtomicallyFrame -> do - -- Trace each created TVar - !ds <- traverse (\(SomeTVar tvar) -> traceTVarST tvar True) createdSeq - -- Trace & commit each TVar - !ds' <- Map.elems <$> traverse - (\(SomeTVar tvar) -> do - tr <- traceTVarST tvar False - !_ <- commitTVar tvar - -- Also assert the data invariant that outside a tx - -- the undo stack is empty: - undos <- readTVarUndos tvar - assert (null undos) $ return tr - ) written - - -- Return the vars written, so readers can be unblocked - k0 $ StmTxCommitted x (reverse writtenSeq) - (Map.elems read) - (reverse createdSeq) - (mapMaybe (\TraceValue { traceDynamic } - -> toDyn <$> traceDynamic) - $ ds ++ ds') - (mapMaybe traceString $ ds ++ ds') - nextVid - - BranchFrame _b k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - -- The branch has successfully completed the transaction. Hence, - -- the alternative branch can be ignored. - -- Commit the TVars written in this sub-transaction that are also - -- in the written set of the outer transaction - !_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar) - (Map.intersection written writtenOuter) - -- Merge the written set of the inner with the outer - let written' = Map.union written writtenOuter - writtenSeq' = filter (\(SomeTVar tvar) -> - tvarId tvar `Map.notMember` writtenOuter) - writtenSeq - ++ writtenOuterSeq - createdSeq' = createdSeq ++ createdOuterSeq - -- Skip the orElse right hand and continue with the k continuation - go ctl' read written' writtenSeq' createdSeq' nextVid (k x) - - ThrowStm e -> do - -- Revert all the TVar writes - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - case ctl of - AtomicallyFrame -> do - k0 $ StmTxAborted (Map.elems read) (toException e) - - BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - -- Execute the left side in a new frame with an empty written set. - -- but preserve ones that were set prior to it, as specified in the - -- [stm](https://hackage.haskell.org/package/stm/docs/Control-Monad-STM.html#v:catchSTM) package. - let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' - go ctl'' read Map.empty [] [] nextVid (h e) - - BranchFrame (OrElseStmA _r) _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) - - BranchFrame NoOpStmA _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) - - CatchStm a h k -> do - -- Execute the left side in a new frame with an empty written set - let ctl' = BranchFrame (CatchStmA h) k written writtenSeq createdSeq ctl - go ctl' read Map.empty [] [] nextVid a - - Retry -> do - -- Always revert all the TVar writes for the retry - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - case ctl of - AtomicallyFrame -> do - -- Return vars read, so the thread can block on them - k0 $! StmTxBlocked $! Map.elems read - - BranchFrame (OrElseStmA b) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - -- Execute the orElse right hand with an empty written set - let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' - go ctl'' read Map.empty [] [] nextVid b - - BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - -- Retry makes sense only within a OrElse context. If it is a branch other than - -- OrElse left side, then bubble up the `retry` to the frame above. - -- Skip the continuation and propagate the retry into the outer frame - -- using the written set for the outer frame - go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry - - OrElse a b k -> do - -- Execute the left side in a new frame with an empty written set - let ctl' = BranchFrame (OrElseStmA b) k written writtenSeq createdSeq ctl - go ctl' read Map.empty [] [] nextVid a - - NewTVar !mbLabel x k -> do - !v <- execNewTVar nextVid mbLabel x - -- record a write to the TVar so we know to update its VClock - let written' = Map.insert (tvarId v) (SomeTVar v) written - -- save the value: it will be committed or reverted - !_ <- saveTVar v - go ctl read written' writtenSeq (SomeTVar v : createdSeq) (succ nextVid) (k v) - - LabelTVar !label tvar k -> do - !_ <- writeSTRef (tvarLabel tvar) $! (Just label) - go ctl read written writtenSeq createdSeq nextVid k - - TraceTVar tvar f k -> do - !_ <- writeSTRef (tvarTrace tvar) (Just f) - go ctl read written writtenSeq createdSeq nextVid k - - ReadTVar v k - | tvarId v `Map.member` read -> do - x <- execReadTVar v - go ctl read written writtenSeq createdSeq nextVid (k x) - | otherwise -> do - x <- execReadTVar v - let read' = Map.insert (tvarId v) (SomeTVar v) read - go ctl read' written writtenSeq createdSeq nextVid (k x) - - WriteTVar v x k - | tvarId v `Map.member` written -> do - !_ <- execWriteTVar v x - go ctl read written writtenSeq createdSeq nextVid k - | otherwise -> do - !_ <- saveTVar v - !_ <- execWriteTVar v x - let written' = Map.insert (tvarId v) (SomeTVar v) written - go ctl read written' (SomeTVar v : writtenSeq) createdSeq nextVid k - - SayStm msg k -> do - trace <- go ctl read written writtenSeq createdSeq nextVid k - -- TODO: step - return $ SimPORTrace time tid (-1) tlbl (EventSay msg) trace - - OutputStm x k -> do - trace <- go ctl read written writtenSeq createdSeq nextVid k - -- TODO: step - return $ SimPORTrace time tid (-1) tlbl (EventLog x) trace - - LiftSTStm st k -> do - x <- strictToLazyST st - go ctl read written writtenSeq createdSeq nextVid (k x) - - FixStm f k -> do - r <- newSTRef (throw NonTermination) - x <- unsafeInterleaveST $ readSTRef r - let k' = unSTM (f x) $ \x' -> - LiftSTStm (lazyToStrictST (writeSTRef r x')) (\() -> k x') - go ctl read written writtenSeq createdSeq nextVid k' - - where - localInvariant = - Map.keysSet written - == Set.fromList ([ tvarId tvar | SomeTVar tvar <- writtenSeq ] - ++ [ tvarId tvar | SomeTVar tvar <- createdSeq ]) - - --- | Special case of 'execAtomically' supporting only var reads and writes --- -execAtomically' :: StmA s () -> ST s [SomeTVar s] -execAtomically' = go Map.empty - where - go :: Map TVarId (SomeTVar s) -- set of vars written - -> StmA s () - -> ST s [SomeTVar s] - go !written action = case action of - ReturnStm () -> do - return (Map.elems written) - ReadTVar v k -> do - x <- execReadTVar v - go written (k x) - WriteTVar v x k - | tvarId v `Map.member` written -> do - !_ <- execWriteTVar v x - go written k - | otherwise -> do - !_ <- saveTVar v - !_ <- execWriteTVar v x - let written' = Map.insert (tvarId v) (SomeTVar v) written - go written' k - _ -> error "execAtomically': only for special case of reads and writes" - - -execNewTVar :: TVarId -> Maybe String -> a -> ST s (TVar s a) -execNewTVar nextVid !mbLabel x = do - tvarLabel <- newSTRef mbLabel - tvarCurrent <- newSTRef x - tvarUndo <- newSTRef [] - tvarBlocked <- newSTRef ([], Set.empty) - tvarVClock <- newSTRef bottomVClock - tvarTrace <- newSTRef Nothing - return TVar {tvarId = nextVid, tvarLabel, - tvarCurrent, tvarUndo, tvarBlocked, tvarVClock, - tvarTrace} - --- 'execReadTVar' is defined in `Control.Monad.IOSim.Type` and shared with /IOSim/ - -execWriteTVar :: TVar s a -> a -> ST s () -execWriteTVar TVar{tvarCurrent} = writeSTRef tvarCurrent -{-# INLINE execWriteTVar #-} - -execTryPutTMVar :: TMVar (IOSim s) a -> a -> ST s Bool -execTryPutTMVar (TMVar var) a = do - v <- execReadTVar var - case v of - Nothing -> execWriteTVar var (Just a) - >> return True - Just _ -> return False -{-# INLINE execTryPutTMVar #-} - -saveTVar :: TVar s a -> ST s () -saveTVar TVar{tvarCurrent, tvarUndo} = do - -- push the current value onto the undo stack - v <- readSTRef tvarCurrent - !vs <- readSTRef tvarUndo - writeSTRef tvarUndo $! v:vs - -revertTVar :: TVar s a -> ST s () -revertTVar TVar{tvarCurrent, tvarUndo} = do - -- pop the undo stack, and revert the current value - !vs <- readSTRef tvarUndo - !_ <- writeSTRef tvarCurrent (head vs) - writeSTRef tvarUndo $! tail vs -{-# INLINE revertTVar #-} - -commitTVar :: TVar s a -> ST s () -commitTVar TVar{tvarUndo} = do - !vs <- readSTRef tvarUndo - -- pop the undo stack, leaving the current value unchanged - writeSTRef tvarUndo $! tail vs -{-# INLINE commitTVar #-} - -readTVarUndos :: TVar s a -> ST s [a] -readTVarUndos TVar{tvarUndo} = readSTRef tvarUndo - --- | Trace a 'TVar'. It must be called only on 'TVar's that were new or --- 'written. -traceTVarST :: TVar s a - -> Bool -- true if it's a new 'TVar' - -> ST s TraceValue -traceTVarST TVar{tvarCurrent, tvarUndo, tvarTrace} new = do - mf <- readSTRef tvarTrace - case mf of - Nothing -> return TraceValue { traceDynamic = (Nothing :: Maybe ()), traceString = Nothing } - Just f -> do - !vs <- readSTRef tvarUndo - v <- readSTRef tvarCurrent - case (new, vs) of - (True, _) -> f Nothing v - (_, _:_) -> f (Just $ last vs) v - _ -> error "traceTVarST: unexpected tvar state" - - - -leastUpperBoundTVarVClocks :: [SomeTVar s] -> ST s VectorClock -leastUpperBoundTVarVClocks tvars = - foldr leastUpperBoundVClock bottomVClock <$> - sequence [readSTRef (tvarVClock r) | SomeTVar r <- tvars] - --- --- Blocking and unblocking on TVars --- - -readTVarBlockedThreads :: TVar s a -> ST s [IOSimThreadId] -readTVarBlockedThreads TVar{tvarBlocked} = fst <$> readSTRef tvarBlocked - -blockThreadOnTVar :: IOSimThreadId -> TVar s a -> ST s () -blockThreadOnTVar tid TVar{tvarBlocked} = do - (tids, tidsSet) <- readSTRef tvarBlocked - when (tid `Set.notMember` tidsSet) $ do - let !tids' = tid : tids - !tidsSet' = Set.insert tid tidsSet - writeSTRef tvarBlocked (tids', tidsSet') - -unblockAllThreadsFromTVar :: TVar s a -> ST s () -unblockAllThreadsFromTVar TVar{tvarBlocked} = do - writeSTRef tvarBlocked ([], Set.empty) - --- | For each TVar written to in a transaction (in order) collect the threads --- that blocked on each one (in order). --- --- Also, for logging purposes, return an association between the threads and --- the var writes that woke them. --- -threadsUnblockedByWrites :: [SomeTVar s] - -> ST s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId))) -threadsUnblockedByWrites written = do - tidss <- sequence - [ (,) <$> labelledTVarId tvar <*> readTVarBlockedThreads tvar - | SomeTVar tvar <- written ] - -- Threads to wake up, in wake up order, annotated with the vars written that - -- caused the unblocking. - -- We reverse the individual lists because the tvarBlocked is used as a stack - -- so it is in order of last written, LIFO, and we want FIFO behaviour. - let wakeup = ordNub [ tid | (_vid, tids) <- tidss, tid <- reverse tids ] - wokeby = Map.fromListWith Set.union - [ (tid, Set.singleton vid) - | (vid, tids) <- tidss - , tid <- tids ] - return (wakeup, wokeby) - -ordNub :: Ord a => [a] -> [a] -ordNub = go Set.empty - where - go !_ [] = [] - go !s (x:xs) - | x `Set.member` s = go s xs - | otherwise = x : go (Set.insert x s) xs - --- --- Steps --- - --- | 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' = - -- 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)) - -- 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 = stepThreadId, - threadStep = stepStep, - threadEffect = stepEffect, - threadVClock = stepVClock - } = Step {..} - --- | 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 - }, - threadEffect thread - ) - --- | 'updateRaces' turns a current 'Step' into 'StepInfo', and updates all --- 'activeRaces'. --- --- We take care that steps can only race against threads in their --- 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 :: 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 - - concurrent0 = - Map.keysSet (Map.filter (\t -> not (isThreadDone t) - && threadId t `Set.notMember` - effectForks newEffect - ) threads) - - -- A new step to add to the `activeRaces` list. - newStepInfo :: Maybe StepInfo - !newStepInfo | isNotRacyThreadId tid = Nothing - -- non-racy threads do not race - - | 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 = concurrent Set.\\ effectWakeup newEffect - - -- `step` happened before `newStep` (`newStep` happened after - -- `step`) - happensBefore = step `happensBeforeStep` newStep - - !stepInfoNonDep' - -- `newStep` happened after `step` - | happensBefore = stepInfoNonDep - -- `newStep` did not happen after `step` - | otherwise = newStep : stepInfoNonDep in - - if tid `notElem` concurrent - then let - in stepInfo { stepInfoConcurrent = lessConcurrent - , stepInfoNonDep = stepInfoNonDep' - } - - -- The core of IOSimPOR. Detect if `newStep` is racing with any - -- previous steps and update each `StepInfo`. - else let theseStepsRace = step `racingSteps` newStep - -- `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 - - -- 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 = stepInfoNonDep', - stepInfoRaces = stepInfoRaces' - } - - activeRaces' :: [StepInfo] - !activeRaces' = - case newStepInfo of - Nothing -> updateStepInfo <$> activeRaces - Just si -> si : (updateStepInfo <$> 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' } +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingVia #-} +-- only used to construct records if its clear to do so +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TypeFamilies #-} + +-- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') +-- and 'reschedule'. +{-# OPTIONS_GHC -Wno-incomplete-uni-patterns -Wno-unused-matches #-} +{-# OPTIONS_GHC -Wno-orphans #-} +#if __GLASGOW_HASKELL__ >= 908 +-- We use partial functions from `Data.List`. +{-# OPTIONS_GHC -Wno-x-partial #-} +#endif + +module Control.Monad.IOSimPOR.Internal + ( IOSim (..) + , runIOSim + , runSimTraceST + , traceM + , traceSTM + , STM + , STMSim + , setCurrentTime + , unshareClock + , TimeoutException (..) + , EventlogEvent (..) + , EventlogMarker (..) + , IOSimThreadId + , ThreadLabel + , Labelled (..) + , SimTrace + , Trace.Trace (SimPORTrace, TraceMainReturn, TraceMainException, TraceDeadlock) + , SimEvent (..) + , SimResult (..) + , SimEventType (..) + , liftST + , execReadTVar + , controlSimTraceST + , ScheduleControl (..) + , ScheduleMod (..) + ) where + +import Prelude hiding (read) + +import Data.Dynamic +import Data.Foldable (foldlM, traverse_) +import Data.HashPSQ (HashPSQ) +import Data.HashPSQ qualified as PSQ +import Data.IntPSQ (IntPSQ) +import Data.IntPSQ qualified as IPSQ +import Data.List qualified as List +import Data.List.Trace qualified as Trace +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Maybe (mapMaybe) +import Data.Ord +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Time (UTCTime (..), fromGregorian) + +import Control.DeepSeq (force) +import Control.Exception (NonTermination (..), SomeAsyncException, assert, + throw) +import Control.Monad (join, when) +import Control.Monad.ST.Lazy +import Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST) +import Data.STRef.Lazy + +import Control.Concurrent.Class.MonadSTM.TMVar +import Control.Concurrent.Class.MonadSTM.TVar hiding (TVar) +import Control.Monad.Class.MonadFork (killThread, myThreadId, throwTo) +import Control.Monad.Class.MonadSTM hiding (STM) +import Control.Monad.Class.MonadSTM.Internal (TMVarDefault (TMVar)) +import Control.Monad.Class.MonadThrow as MonadThrow +import Control.Monad.Class.MonadTime (NominalDiffTime) +import Control.Monad.Class.MonadTime qualified as Time +import Control.Monad.Class.MonadTime.SI qualified as SI +import Control.Monad.Class.MonadTimer.SI (TimeoutState (..)) + +import Control.Monad.IOSim.InternalTypes +import Control.Monad.IOSim.Types hiding (SimEvent (SimEvent), Time (..), + Trace (SimTrace)) +import Control.Monad.IOSim.Types (SimEvent) +import Control.Monad.IOSimPOR.Timeout (unsafeTimeout) +import Control.Monad.IOSimPOR.Types +import Data.Coerce (Coercible, coerce) +import Data.Hashable + +-- +-- Simulation interpreter +-- + +data Thread s a = Thread { + 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 IOSimThreadId, VectorClock)], + threadClockId :: !ClockId, + threadLabel :: Maybe ThreadLabel, + threadNextTId :: !Int, + threadStep :: !Int, + threadVClock :: VectorClock, + threadEffect :: Effect, -- in the current step + threadRacy :: !Bool + } + deriving Show + +isThreadBlocked :: Thread s a -> Bool +isThreadBlocked t = case threadStatus t of + ThreadBlocked {} -> True + _ -> False + +isThreadDone :: Thread s a -> Bool +isThreadDone t = case threadStatus t of + ThreadDone -> True + _ -> False + +threadStepId :: Thread s a -> (IOSimThreadId, Int) +threadStepId Thread{ threadId, threadStep } = (threadId, threadStep) + +isRacyThreadId :: IOSimThreadId -> Bool +isRacyThreadId (RacyThreadId _) = True +isRacyThreadId _ = True + +isNotRacyThreadId :: IOSimThreadId -> Bool +isNotRacyThreadId (ThreadId _) = True +isNotRacyThreadId _ = False + +bottomVClock :: VectorClock +bottomVClock = VectorClock Map.empty + +insertVClock :: IOSimThreadId -> Int -> VectorClock -> VectorClock +insertVClock tid !step (VectorClock m) = VectorClock (Map.insert tid step m) + +leastUpperBoundVClock :: VectorClock -> VectorClock -> VectorClock +leastUpperBoundVClock (VectorClock m) (VectorClock m') = + VectorClock (Map.unionWith max m m') + +-- hbfVClock :: VectorClock -> VectorClock -> Bool +-- hbfVClock (VectorClock m) (VectorClock m') = Map.isSubmapOfBy (<=) m m' + +happensBeforeStep :: Step -- ^ an earlier step + -> Step -- ^ a later step + -> Bool +happensBeforeStep step step' = + Just (stepStep step) + <= Map.lookup (stepThreadId step) + (getVectorClock $ stepVClock step') + +labelledTVarId :: TVar s a -> ST s (Labelled TVarId) +labelledTVarId TVar { tvarId, tvarLabel } = Labelled tvarId <$> readSTRef tvarLabel + +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. + -- TODO: https://github.com/haskell/containers/issues/749 + Map.foldr' + (\Thread { threadId, threadLabel } !acc -> Labelled threadId threadLabel : acc) + [] threadMap + + +-- | Timers mutable variables. First one supports 'newTimeout' api, the second +-- one 'Control.Monad.Class.MonadTimer.SI.registerDelay', the third one +-- 'Control.Monad.Class.MonadTimer.SI.threadDelay'. +-- +data TimerCompletionInfo s = + Timer !(TVar s TimeoutState) + -- ^ `newTimeout` timer. + | TimerRegisterDelay !(TVar s Bool) + -- ^ `registerDelay` timer. + | TimerThreadDelay !IOSimThreadId !TimeoutId + -- ^ `threadDelay` timer run by `IOSimThreadId` which was assigned the given + -- `TimeoutId` (only used to report in a trace). + | 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). + +instance Hashable a => Hashable (Down a) + +type RunQueue = HashPSQ (Down IOSimThreadId) (Down IOSimThreadId) () +type Timeouts s = IntPSQ SI.Time (TimerCompletionInfo s) + +-- | Internal state. +-- +data SimState s a = SimState { + runqueue :: !RunQueue, + -- | All threads other than the currently running thread: both running + -- and blocked threads. + threads :: !(Map IOSimThreadId (Thread s a)), + -- | current time + curTime :: !SI.Time, + -- | ordered list of timers and timeouts + timers :: !(Timeouts s), + -- | timeout locks in order to synchronize the timeout handler and the + -- main thread + clocks :: !(Map ClockId UTCTime), + nextVid :: !VarId, -- ^ next unused 'TVarId' + nextTmid :: !TimeoutId, -- ^ next unused 'TimeoutId' + nextUniq :: !(Unique s), -- ^ next unused @'Unique' s@ + -- | previous steps (which we may race with). + -- Note this is *lazy*, so that we don't compute races we will not reverse. + races :: Races, + -- | control the schedule followed, and initial value + control :: !ScheduleControl, + control0 :: !ScheduleControl, + -- | limit on the computation time allowed per scheduling step, for + -- catching infinite loops etc + perStepTimeLimit :: Maybe Int + + } + +initialState :: SimState s a +initialState = + SimState { + runqueue = PSQ.empty, + threads = Map.empty, + curTime = SI.Time 0, + timers = IPSQ.empty, + clocks = Map.singleton (ClockId []) epoch1970, + nextVid = 0, + nextTmid = TimeoutId 0, + nextUniq = MkUnique 0, + races = noRaces, + control = ControlDefault, + control0 = ControlDefault, + perStepTimeLimit = Nothing + } + where + epoch1970 = UTCTime (fromGregorian 1970 1 1) 0 + +invariant :: Maybe (Thread s a) -> SimState s a -> x -> x + +invariant (Just running) simstate@SimState{runqueue,threads,clocks} = + assert (not (isThreadBlocked running)) + . assert (threadId running `Map.notMember` threads) + . assert (not (Down (threadId running) `PSQ.member` runqueue)) + . assert (threadClockId running `Map.member` clocks) + . invariant Nothing simstate + +invariant Nothing SimState{runqueue,threads,clocks} = + assert (PSQ.fold' (\(Down tid) _ _ a -> tid `Map.member` threads && a) True runqueue) + . assert (and [ (isThreadBlocked t || isThreadDone t) == not (Down (threadId t) `PSQ.member` runqueue) + | t <- Map.elems threads ]) + . assert (and [ threadClockId t `Map.member` clocks + | t <- Map.elems threads ]) + +-- | Interpret the simulation monotonic time as a 'NominalDiffTime' since +-- the start. +timeSinceEpoch :: SI.Time -> NominalDiffTime +timeSinceEpoch (SI.Time t) = fromRational (toRational t) + + +-- | Insert thread into `runqueue`. +-- +insertThread :: Thread s a -> RunQueue -> RunQueue +insertThread Thread { threadId } = PSQ.insert (Down threadId) (Down threadId) () + + +-- | Schedule / run a thread. +-- +schedule :: forall s a. Thread s a -> SimState s a -> ST s (SimTrace a) +schedule thread@Thread{ + threadId = tid, + threadControl = ThreadControl action ctl, + threadMasking = maskst, + threadLabel = tlbl, + threadStep = tstep, + threadVClock = vClock, + threadEffect = effect + } + simstate@SimState { + runqueue, + threads, + timers, + clocks, + nextVid, nextTmid, nextUniq, + curTime = time, + control, + perStepTimeLimit + } + + | controlTargets (tid,tstep) control = + -- The next step is to be delayed according to the + -- specified schedule. Switch to following the schedule. + SimPORTrace time tid tstep tlbl (EventFollowControl control) <$> + schedule thread simstate{ control = followControl control } + + | not $ controlFollows (tid,tstep) control = + -- the control says this is not the next step to + -- follow. We should be at the beginning of a step; + -- we put the present thread to sleep and reschedule + -- the correct thread. + -- The assertion says that the only effect that may have + -- happened in the start of a thread is us waking up. + ( SimPORTrace time tid tstep tlbl (EventAwaitControl (tid,tstep) control) + . SimPORTrace time tid tstep tlbl (EventDeschedule Sleep) + ) <$> deschedule Sleep thread simstate + + | otherwise = + invariant (Just thread) simstate $ + case control of + ControlFollow (s:_) _ + -> fmap (SimPORTrace time tid tstep tlbl (EventPerformAction (tid,tstep))) + _ -> id + $ + -- The next line forces the evaluation of action, which should be unevaluated up to + -- this point. This is where we actually *run* user code. + case maybe Just unsafeTimeout perStepTimeLimit action of + Nothing -> return TraceLoop + Just _ -> case action of + + Return x -> case ctl of + MainFrame -> + -- the main thread is done, so we're done + -- even if other threads are still running + return $ SimPORTrace time tid tstep tlbl EventThreadFinished + $ traceFinalRacesFound simstate + $ TraceMainReturn time (Labelled tid tlbl) x + ( labelledThreads + . Map.filter (not . isThreadDone) + $ threads + ) + + ForkFrame -> do + -- this thread is done + let thread' = thread + !trace <- deschedule Terminated thread' simstate + return $ SimPORTrace time tid tstep tlbl EventThreadFinished + $ SimPORTrace time tid tstep tlbl (EventDeschedule Terminated) + $ trace + + MaskFrame k maskst' ctl' -> do + -- pop the control stack, restore thread-local state + let thread' = thread { threadControl = ThreadControl (k x) ctl' + , threadMasking = maskst' + } + -- but if we're now unmasked, check for any pending async exceptions + !trace <- deschedule Interruptable thread' simstate + return $ SimPORTrace time tid tstep tlbl (EventMask maskst') + $ SimPORTrace time tid tstep tlbl (EventDeschedule Interruptable) + $ trace + + CatchFrame _handler k ctl' -> do + -- pop the control stack and continue + let thread' = thread { threadControl = ThreadControl (k x) ctl' } + schedule thread' simstate + + TimeoutFrame tmid lock k ctl' -> do + -- It could happen that the timeout action finished at the same time + -- as the timeout expired, this will be a race condition. That's why + -- we have the locks to solve this. + + -- We cannot do `tryPutMVar` in the `treadAction`, because we need to + -- know if the `lock` is empty right now when we still have the frame. + v <- execTryPutTMVar lock undefined + let -- Kill the assassin throwing thread then unmask exceptions and + -- carry on the continuation + threadAction :: IOSim s () + threadAction = + if v then unsafeUnregisterTimeout tmid + else atomically (takeTMVar lock) >>= killThread + + thread' = + thread { threadControl = + ThreadControl (case threadAction of + IOSim k' -> k' (\() -> k (Just x))) + ctl' + } + schedule thread' simstate + + DelayFrame tmid k ctl' -> do + let thread' = thread { threadControl = ThreadControl k ctl' } + timers' = IPSQ.delete (coerce tmid) timers + schedule thread' simstate { timers = timers' } + + Throw e -> case unwindControlStack e thread timers of + -- Found a CatchFrame + (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', 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') $ + 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 + -- have an unhandled exception at the top level of the thread. + | isMain -> do + let thread' = thread { threadStatus = ThreadDone } + -- An unhandled exception in the main thread terminates the program + 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 (Labelled tid tlbl) e (labelledThreads threads)) + + | otherwise -> do + -- An unhandled exception in any other thread terminates the thread + let terminated = Terminated + !trace <- deschedule terminated thread simstate { timers = timers'' } + return $ SimPORTrace time tid tstep tlbl (EventThrow e) + $ SimPORTrace time tid tstep tlbl (EventThreadUnhandled e) + $ SimPORTrace time tid tstep tlbl (EventDeschedule terminated) + $ trace + + Catch action' handler k -> do + -- push the failure and success continuations onto the control stack + let thread' = thread { threadControl = ThreadControl action' + (CatchFrame handler k ctl) + } + schedule thread' simstate + + Evaluate expr k -> do + mbWHNF <- unsafeIOToST $ tryJust (\e -> case fromException @SomeAsyncException e of + Nothing -> Just e + Just {} -> Nothing) + $ evaluate expr + case mbWHNF of + Left e -> do + -- schedule this thread to immediately raise the exception + let thread' = thread { threadControl = ThreadControl (Throw e) ctl } + trace <- schedule thread' simstate + return $ SimPORTrace time tid tstep tlbl (EventEvaluationError e) + $ trace + Right whnf -> do + -- continue with the resulting WHNF + let thread' = thread { threadControl = ThreadControl (k whnf) ctl } + trace <- schedule thread' simstate + return $ SimPORTrace time tid tstep tlbl EventEvaluationSuccess + $ trace + + Say msg k -> do + mbNF <- unsafeIOToST $ tryJust (\e -> case fromException @SomeAsyncException e of + Nothing -> Just e + Just {} -> Nothing) + $ evaluate (force msg) + case mbNF of + Left e -> do + let thread' = thread { threadControl = ThreadControl (Throw e) ctl } + trace <- schedule thread' simstate + return $ SimPORTrace time tid tstep tlbl (EventSayEvaluationError e) + $ trace + Right msg' -> do + let thread' = thread { threadControl = ThreadControl k ctl } + trace <- schedule thread' simstate + return (SimPORTrace time tid tstep tlbl (EventSay msg') trace) + + Output x@(Dynamic _ x') k -> do + mbWHNF <- unsafeIOToST $ tryJust (\e -> case fromException @SomeAsyncException e of + Nothing -> Just e + Just {} -> Nothing) + $ evaluate x' + case mbWHNF of + Left e -> do + let thread' = thread { threadControl = ThreadControl (Throw e) ctl } + trace <- schedule thread' simstate + return $ SimPORTrace time tid tstep tlbl (EventLogEvaluationError e) + $ trace + Right {} -> do + let thread' = thread { threadControl = ThreadControl k ctl } + trace <- schedule thread' simstate + return (SimPORTrace time tid tstep tlbl (EventLog x) trace) + + LiftST st k -> do + x <- strictToLazyST st + let thread' = thread { threadControl = ThreadControl (k x) ctl } + schedule thread' simstate + + GetMonoTime k -> do + let thread' = thread { threadControl = ThreadControl (k time) ctl } + schedule thread' simstate + + GetWallTime k -> do + let clockid = threadClockId thread + clockoff = clocks Map.! clockid + walltime = timeSinceEpoch time `Time.addUTCTime` clockoff + thread' = thread { threadControl = ThreadControl (k walltime) ctl } + schedule thread' simstate + + SetWallTime walltime' k -> do + let clockid = threadClockId thread + clockoff = clocks Map.! clockid + walltime = timeSinceEpoch time `Time.addUTCTime` clockoff + clockoff' = (walltime' `Time.diffUTCTime` walltime) `Time.addUTCTime` clockoff + thread' = thread { threadControl = ThreadControl k ctl } + simstate' = simstate { clocks = Map.insert clockid clockoff' clocks } + schedule thread' simstate' + + UnshareClock k -> do + let clockid = threadClockId thread + clockoff = clocks Map.! clockid + clockid' = let ThreadId i = tid in ClockId i -- reuse the thread id + thread' = thread { threadControl = ThreadControl k ctl + , threadClockId = clockid' } + simstate' = simstate { clocks = Map.insert clockid' clockoff clocks } + schedule thread' simstate' + + -- This case is guarded by checks in 'timeout' itself. + StartTimeout d _ _ | d <= 0 -> + error "schedule: StartTimeout: Impossible happened" + + StartTimeout d action' k -> do + lock <- TMVar <$> execNewTVar (TMVarId nextVid) (Just $! "lock-" ++ show nextTmid) Nothing + let expiry = d `addTime` time + timers' = IPSQ.insert (coerce nextTmid) expiry (TimerTimeout tid nextTmid lock) timers + thread' = thread { threadControl = + ThreadControl action' + (TimeoutFrame nextTmid lock k ctl) + } + trace <- deschedule Yield thread' simstate { timers = timers' + , nextTmid = succ nextTmid } + return (SimPORTrace time tid tstep tlbl (EventTimeoutCreated nextTmid tid expiry) trace) + + UnregisterTimeout tmid k -> do + let thread' = thread { threadControl = ThreadControl k ctl } + schedule thread' simstate { timers = IPSQ.delete (coerce tmid) timers } + + RegisterDelay d k | d < 0 -> do + tvar <- execNewTVar (TVarId nextVid) + (Just $! "<>") + True + modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) + let !expiry = d `addTime` time + !thread' = thread { threadControl = ThreadControl (k tvar) ctl } + trace <- schedule thread' simstate { nextVid = succ nextVid } + return (SimPORTrace time tid tstep tlbl (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) $ + SimPORTrace time tid tstep tlbl (EventRegisterDelayFired nextTmid) $ + trace) + + RegisterDelay d k -> do + tvar <- execNewTVar (TVarId nextVid) + (Just $! "<>") + False + modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) + let !expiry = d `addTime` time + !timers' = IPSQ.insert (coerce nextTmid) expiry (TimerRegisterDelay tvar) timers + !thread' = thread { threadControl = ThreadControl (k tvar) ctl } + trace <- schedule thread' simstate { timers = timers' + , nextVid = succ nextVid + , nextTmid = succ nextTmid } + return (SimPORTrace time tid tstep tlbl + (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) trace) + + ThreadDelay d k | d < 0 -> do + let expiry = d `addTime` time + thread' = thread { threadControl = ThreadControl (Return ()) (DelayFrame nextTmid k ctl) } + simstate' = simstate { nextTmid = succ nextTmid } + trace <- schedule thread' simstate' + return (SimPORTrace time tid tstep tlbl (EventThreadDelay nextTmid expiry) $ + SimPORTrace time tid tstep tlbl (EventThreadDelayFired nextTmid) $ + trace) + + ThreadDelay d k -> do + let expiry = d `addTime` time + timers' = IPSQ.insert (coerce nextTmid) expiry (TimerThreadDelay tid nextTmid) timers + thread' = thread { threadControl = ThreadControl (Return ()) (DelayFrame nextTmid k ctl) } + trace <- deschedule (Blocked BlockedOnDelay) thread' + simstate { timers = timers', + nextTmid = succ nextTmid } + return (SimPORTrace time tid tstep tlbl (EventThreadDelay nextTmid expiry) trace) + + -- we treat negative timers as cancelled ones; for the record we put + -- `EventTimerCreated` and `EventTimerCancelled` in the trace; This differs + -- from `GHC.Event` behaviour. + NewTimeout d k | d < 0 -> do + let t = NegativeTimeout nextTmid + expiry = d `addTime` time + thread' = thread { threadControl = ThreadControl (k t) ctl } + trace <- schedule thread' simstate { nextTmid = succ nextTmid } + return (SimPORTrace time tid tstep tlbl (EventTimerCreated nextTmid (TVarId nextVid) expiry) $ + SimPORTrace time tid tstep tlbl (EventTimerCancelled nextTmid) $ + trace) + + NewTimeout d k -> do + tvar <- execNewTVar (TVarId nextVid) + (Just $! "<>") + TimeoutPending + modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) + let expiry = d `addTime` time + t = Timeout tvar nextTmid + timers' = IPSQ.insert (coerce nextTmid) expiry (Timer tvar) timers + thread' = thread { threadControl = ThreadControl (k t) ctl } + trace <- schedule thread' simstate { timers = timers' + , nextVid = succ (succ nextVid) + , nextTmid = succ nextTmid } + return (SimPORTrace time tid tstep tlbl (EventTimerCreated nextTmid (TVarId nextVid) expiry) trace) + + CancelTimeout (Timeout tvar tmid) k -> do + let timers' = IPSQ.delete (coerce tmid) timers + written <- execAtomically' (runSTM $ writeTVar tvar TimeoutCancelled) + written' <- mapM someTVarToLabelled written + (wakeup, wokeby) <- threadsUnblockedByWrites written + mapM_ (\(SomeTVar var) -> unblockAllThreadsFromTVar var) written + let effect' = effect + <> writeEffects written' + <> wakeupEffects wakeup + thread' = thread { threadControl = ThreadControl k ctl + , threadEffect = effect' + } + (unblocked, + simstate') = unblockThreads False vClock wakeup simstate + modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) + !trace <- deschedule Yield thread' simstate' { timers = timers' } + return $ SimPORTrace time tid tstep tlbl (EventTimerCancelled tmid) + $ traceMany + -- TODO: step + [ (time, tid', (-1), tlbl', EventTxWakeup vids) + | tid' <- unblocked + , let tlbl' = lookupThreadLabel tid' threads + , let Just vids = Set.toList <$> Map.lookup tid' wokeby ] + $ SimPORTrace time tid tstep tlbl (EventDeschedule Yield) + $ trace + + -- cancelling a negative timer is a no-op + CancelTimeout (NegativeTimeout _tmid) k -> do + -- negative timers are promptly removed from the state + let thread' = thread { threadControl = ThreadControl k ctl } + schedule thread' simstate + + Fork a k -> do + let nextTId = threadNextTId thread + tid' | threadRacy thread = setRacyThread $ childThreadId tid nextTId + | otherwise = childThreadId tid nextTId + thread' = thread { threadControl = ThreadControl (k tid') ctl, + threadNextTId = nextTId + 1, + threadEffect = effect + <> forkEffect tid' + } + thread'' = Thread { threadId = tid' + , threadControl = ThreadControl (runIOSim a) + ForkFrame + , threadStatus = ThreadRunning + , threadMasking = threadMasking thread + , threadThrowTo = [] + , threadClockId = threadClockId thread + , threadLabel = Nothing + , threadNextTId = 1 + , threadStep = 0 + , threadVClock = insertVClock tid' 0 + $ vClock + , threadEffect = mempty + , threadRacy = threadRacy thread + } + threads' = Map.insert tid' thread'' threads + -- A newly forked thread may have a higher priority, so we deschedule this one. + !trace <- deschedule Yield thread' + simstate { runqueue = insertThread thread'' runqueue + , threads = threads' } + return $ SimPORTrace time tid tstep tlbl (EventThreadForked tid') + $ SimPORTrace time tid tstep tlbl (EventDeschedule Yield) + $ trace + + Atomically a k -> execAtomically time tid (labelledThreads threads) tlbl nextVid (runSTM a) $ \res -> + case res of + StmTxCommitted x written read created + tvarDynamicTraces tvarStringTraces nextVid' -> do + (wakeup, wokeby) <- threadsUnblockedByWrites written + mapM_ (\(SomeTVar tvar) -> unblockAllThreadsFromTVar tvar) written + vClockRead <- leastUpperBoundTVarVClocks read + read' <- mapM someTVarToLabelled read + written' <- mapM someTVarToLabelled written + let vClock' = vClock `leastUpperBoundVClock` vClockRead + effect' = effect + <> readEffects read' + <> writeEffects written' + <> wakeupEffects unblocked + thread' = thread { threadControl = ThreadControl (k x) ctl, + threadVClock = vClock', + threadEffect = effect' } + (unblocked, + simstate') = unblockThreads True vClock' wakeup simstate + sequence_ [ modifySTRef (tvarVClock r) (leastUpperBoundVClock vClock') + | SomeTVar r <- created ++ written ] + written'' <- traverse (\(SomeTVar tvar) -> labelledTVarId tvar) written + created' <- traverse (\(SomeTVar tvar) -> labelledTVarId tvar) created + -- We deschedule a thread after a transaction... another may have woken up. + !trace <- deschedule Yield thread' simstate' { nextVid = nextVid' } + return $ + SimPORTrace time tid tstep tlbl (EventTxCommitted written'' created' (Just effect')) $ + traceMany + [ (time, tid', (-1), tlbl', EventTxWakeup vids') + | tid' <- unblocked + , let tlbl' = lookupThreadLabel tid' threads + , let Just vids' = Set.toList <$> Map.lookup tid' wokeby ] $ + traceMany + [ (time, tid, tstep, tlbl, EventLog tr) + | tr <- tvarDynamicTraces + ] $ + traceMany + [ (time, tid, tstep, tlbl, EventSay str) + | str <- tvarStringTraces + ] $ + SimPORTrace time tid tstep tlbl (EventUnblocked unblocked) $ + SimPORTrace time tid tstep tlbl (EventDeschedule Yield) $ + trace + + StmTxAborted read e -> do + -- schedule this thread to immediately raise the exception + vClockRead <- leastUpperBoundTVarVClocks read + read' <- mapM someTVarToLabelled read + let effect' = effect <> readEffects read' + thread' = thread { threadControl = ThreadControl (Throw e) ctl, + threadVClock = vClock `leastUpperBoundVClock` vClockRead, + threadEffect = effect' } + trace <- schedule thread' simstate + return $ SimPORTrace time tid tstep tlbl (EventTxAborted (Just effect')) + $ trace + + StmTxBlocked read -> do + mapM_ (\(SomeTVar tvar) -> blockThreadOnTVar tid tvar) read + vids <- traverse (\(SomeTVar tvar) -> labelledTVarId tvar) read + vClockRead <- leastUpperBoundTVarVClocks read + read' <- mapM someTVarToLabelled read + let effect' = effect <> readEffects read' + thread' = thread { threadVClock = vClock `leastUpperBoundVClock` vClockRead, + threadEffect = effect' } + !trace <- deschedule (Blocked BlockedOnSTM) thread' simstate + return $ SimPORTrace time tid tstep tlbl (EventTxBlocked vids (Just effect')) + $ SimPORTrace time tid tstep tlbl (EventDeschedule (Blocked BlockedOnSTM)) + $ trace + + GetThreadId k -> do + let thread' = thread { threadControl = ThreadControl (k tid) ctl } + schedule thread' simstate + + LabelThread tid' l k | tid' == tid -> do + let thread' = thread { threadControl = ThreadControl k ctl + , threadLabel = Just l } + schedule thread' simstate + + GetThreadLabel tid' k -> do + let tlbl' | tid' == tid = tlbl + | otherwise = tid' `Map.lookup` threads + >>= threadLabel + thread' = thread { threadControl = ThreadControl (k tlbl') ctl } + schedule thread' simstate + + LabelThread tid' l k -> do + let thread' = thread { threadControl = ThreadControl k ctl } + threads' = Map.adjust (\t -> t { threadLabel = Just l }) tid' threads + schedule thread' simstate { threads = threads' } + + ExploreRaces k -> do + let thread' = thread { threadControl = ThreadControl k ctl + , threadRacy = True } + schedule thread' simstate + + Fix f k -> do + r <- newSTRef (throw NonTermination) + x <- unsafeInterleaveST $ readSTRef r + let k' = unIOSim (f x) $ \x' -> + LiftST (lazyToStrictST (writeSTRef r x')) (\() -> k x') + thread' = thread { threadControl = ThreadControl k' ctl } + schedule thread' simstate + + GetMaskState k -> do + let thread' = thread { threadControl = ThreadControl (k maskst) ctl } + schedule thread' simstate + + SetMaskState maskst' action' k -> do + let thread' = thread { threadControl = ThreadControl + (runIOSim action') + (MaskFrame k maskst ctl) + , threadMasking = maskst' } + trace <- + case maskst' of + -- If we're now unmasked then check for any pending async exceptions + Unmasked -> SimPORTrace time tid tstep tlbl (EventDeschedule Interruptable) + <$> deschedule Interruptable thread' simstate + _ -> schedule thread' simstate + return $ SimPORTrace time tid tstep tlbl (EventMask maskst') + $ trace + + ThrowTo e tid' _ | tid' == tid -> do + -- Throw to ourself is equivalent to a synchronous throw, + -- and works irrespective of masking state since it does not block. + let thread' = thread { threadControl = ThreadControl (Throw e) ctl + , threadEffect = effect + } + trace <- schedule thread' simstate + return (SimPORTrace time tid tstep tlbl (EventThrowTo e tid) trace) + + ThrowTo e tid' k -> do + let thread' = thread { threadControl = ThreadControl k ctl, + threadEffect = effect <> throwToEffect tid' + <> wakeUpEffect, + threadVClock = vClock `leastUpperBoundVClock` vClockTgt + } + (vClockTgt, + wakeUpEffect, + willBlock) = (threadVClock t, + if isThreadBlocked t then wakeupEffects [tid'] else mempty, + not (threadInterruptible t || isThreadDone t)) + where Just t = Map.lookup tid' threads + + if willBlock + then do + -- The target thread has async exceptions masked so we add the + -- exception and the source thread id to the pending async exceptions. + let adjustTarget t = + t { threadThrowTo = (e, Labelled tid tlbl, vClock) : threadThrowTo t } + threads' = Map.adjust adjustTarget tid' 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 BlockedOnThrowTo)) + $ trace + else do + -- The target thread has async exceptions unmasked, or is masked but + -- is blocked (and all blocking operations are interruptible) then we + -- raise the exception in that thread immediately. This will either + -- cause it to terminate or enter an exception handler. + -- In the meantime the thread masks new async exceptions. This will + -- be resolved if the thread terminates or if it leaves the exception + -- handler (when restoring the masking state would trigger the any + -- new pending async exception). + let adjustTarget t@Thread{ threadControl = ThreadControl _ ctl', + threadVClock = vClock' } = + t { threadControl = ThreadControl (Throw e) ctl' + , threadStatus = if isThreadDone t + then threadStatus t + else ThreadRunning + , threadVClock = vClock' `leastUpperBoundVClock` vClock } + (_unblocked, simstate'@SimState { threads = threads' }) = unblockThreads False vClock [tid'] simstate + threads'' = Map.adjust adjustTarget tid' threads' + simstate'' = simstate' { threads = threads'' } + + -- We yield at this point because the target thread may be higher + -- priority, so this should be a step for race detection. + trace <- deschedule Yield thread' simstate'' + return $ SimPORTrace time tid tstep tlbl (EventThrowTo e tid') + $ trace + + -- intentionally a no-op (at least for now) + YieldSim k -> do + let thread' = thread { threadControl = ThreadControl k ctl } + schedule thread' simstate + + NewUnique k -> do + let thread' = thread{ threadControl = ThreadControl (k nextUniq) ctl } + n = unMkUnique nextUniq + simstate' = simstate{ nextUniq = MkUnique (n + 1) } + SimPORTrace time tid tstep tlbl (EventUniqueCreated n) + <$> schedule thread' simstate' + + +threadInterruptible :: Thread s a -> Bool +threadInterruptible thread = + case threadMasking thread of + Unmasked -> True + MaskedInterruptible + | isThreadBlocked thread -> True -- blocking operations are interruptible + | otherwise -> False + MaskedUninterruptible -> False + + +-- | Deschedule a thread. +-- +-- A thread is descheduled, which marks a boundary of a `Step` when: +-- +-- * forking a new thread +-- * thread termination +-- * setting the masking state to interruptible +-- * popping masking frame (which resets masking state) +-- * starting or cancelling a timeout +-- * thread delays +-- * on committed or blocked, but not aborted STM transactions +-- * on blocking or non-blocking `throwTo` +-- * unhandled exception in a (non-main) thread +-- +deschedule :: Deschedule -> Thread s a -> SimState s a -> ST s (SimTrace a) + +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', 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 = races', + control = control' } + +deschedule Interruptable thread@Thread { + threadId = tid, + threadStep = tstep, + threadControl = ThreadControl _ ctl, + threadMasking = Unmasked, + threadThrowTo = (e, tid', vClock') : etids, + threadLabel = tlbl, + threadVClock = vClock, + threadEffect = effect + } + simstate@SimState{ curTime = time, threads } = do + + 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 (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, + 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', 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 = races', + control = advanceControl (threadStepId thread) control } + +deschedule (Blocked _blockedReason) thread@Thread { threadId = tid + , threadStep = tstep + , threadLabel = tlbl + , threadThrowTo = _ : _ + , threadMasking = maskst + , 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. + SimPORTrace time tid tstep tlbl (EventDeschedule Interruptable) <$> + deschedule Interruptable thread { threadMasking = Unmasked } simstate + +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 = races', + control = advanceControl (threadStepId thread1) control } + +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 wakeup = map (\(_,tid',_) -> l_labelled tid') (reverse (threadThrowTo thread)) + (unblocked, + simstate'@SimState{threads}) = + unblockThreads False vClock wakeup simstate + 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 = races', + control = advanceControl (threadStepId thread) control, + threads = threads' } + return $ traceMany + -- TODO: step + [ (time, tid', (-1), tlbl', EventThrowToWakeup) + | tid' <- unblocked + , let tlbl' = lookupThreadLabel tid' threads ] + $ SimPORTrace time tid tstep tlbl (EventEffect vClock eff) + $ SimPORTrace time tid tstep tlbl (EventRaces races') + trace + +deschedule Sleep thread@Thread { threadId = tid , threadEffect = effect' } + simstate@SimState{runqueue, threads} = + + -- Schedule control says we should run a different thread. Put + -- this one to sleep without recording a step. + + let runqueue' = insertThread thread runqueue + threads' = Map.insert tid thread threads in + reschedule simstate { runqueue = runqueue', threads = threads' } + + +-- Choose the next thread to run. +reschedule :: SimState s a -> ST s (SimTrace a) + +-- If we are following a controlled schedule, just do that. +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)) $ + invariant Nothing simstate $ + let thread = threads Map.! tid in + assert (threadId thread == tid) $ + --assert (threadStep thread == tstep) $ + if threadStep thread /= tstep then + error $ "Thread step out of sync\n" + ++ " runqueue: "++show runqueue++"\n" + ++ " follows: "++show tid++", step "++show tstep++"\n" + ++ " actual step: "++show (threadStep thread)++"\n" + ++ "Thread:\n" ++ show thread ++ "\n" + else + schedule thread simstate { runqueue = PSQ.delete (Down tid) runqueue + , threads = Map.delete tid threads } + +-- When there is no current running thread but the runqueue is non-empty then +-- schedule the next one to run. +reschedule simstate@SimState{ runqueue, threads } + | Just (Down !tid, _, _, runqueue') <- PSQ.minView runqueue = + invariant Nothing simstate $ + + let thread = threads Map.! tid in + schedule thread simstate { runqueue = runqueue' + , threads = Map.delete tid threads } + +-- But when there are no runnable threads, we advance the time to the next +-- timer event, or stop. +reschedule simstate@SimState{ threads, timers, curTime = time, races } = + invariant Nothing simstate $ + + -- time is moving on + --Debug.trace ("Rescheduling at "++show time++", "++ + --show (length (concatMap stepInfoRaces (activeRaces races++completeRaces races)))++" races") $ + + -- important to get all events that expire at this time + case removeMinimums timers of + Nothing -> return (traceFinalRacesFound simstate $ + TraceDeadlock time (labelledThreads threads)) + + Just (tmids, time', fired, timers') -> assert (time' >= time) $ do + + -- 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 + + let wakeupThreadDelay = [ (tid, tmid) | TimerThreadDelay tid tmid <- fired ] + -- TODO: the vector clock below cannot be right, can it? + !simstate' = + snd . unblockThreads False bottomVClock (fst `fmap` wakeupThreadDelay) + . snd . unblockThreads True bottomVClock wakeupSTM + $ simstate + + -- For each 'timeout' action where the timeout has fired, start a + -- new thread to execute throwTo to interrupt the action. + !timeoutExpired = [ (tid, tmid, lock) + | TimerTimeout tid tmid lock <- fired ] + + -- all open races will be completed and reported at this time + !simstate'' <- forkTimeoutInterruptThreads timeoutExpired + simstate' { races = noRaces } + !trace <- reschedule simstate'' { curTime = time' + , timers = timers' } + let traceEntries = + [ ( time', ThreadId [-1], -1, Just "timer" + , EventTimerFired tmid) + | (tmid, Timer _) <- zip tmids fired ] + ++ [ ( 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 + , let Just vids = Set.toList <$> Map.lookup tid' wokeby ] + ++ [ ( time', tid, -1, Just "thread delay timer" + , EventThreadDelayFired tmid) + | (tid, tmid) <- wakeupThreadDelay ] + ++ [ ( time', tid, -1, Just "timeout timer" + , EventTimeoutFired tmid) + | (tid, tmid, _) <- timeoutExpired ] + ++ [ ( time', tid, -1, Just "forked thread" + , EventThreadForked tid) + | (tid, _, _) <- timeoutExpired ] + + return $ + traceFinalRacesFound simstate $ + traceMany traceEntries trace + where + timeoutAction (Timer var) = do + x <- readTVar var + case x of + TimeoutPending -> writeTVar var TimeoutFired + TimeoutFired -> error "MonadTimer(Sim): invariant violation" + TimeoutCancelled -> return () + timeoutAction (TimerRegisterDelay var) = writeTVar var True + timeoutAction (TimerThreadDelay _ _) = return () + timeoutAction (TimerTimeout _ _ _) = return () + +unblockThreads :: forall s a. + Bool -- ^ `True` if we are blocked on STM + -> VectorClock + -> [IOSimThreadId] + -> 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 + ( unblockedIds + , simstate { runqueue = foldr insertThread runqueue unblocked, + threads = threads' + }) + where + -- can only unblock if the thread exists and is blocked (not running) + unblocked :: [Thread s a] + !unblocked = [ thread + | tid <- wakeup + , thread <- + case Map.lookup tid threads of + Just Thread { threadStatus = ThreadRunning } + -> [ ] + Just t@Thread { threadStatus = ThreadBlocked BlockedOnSTM } + -> [t] + Just t@Thread { threadStatus = ThreadBlocked _ } + | onlySTM + -> [ ] + | otherwise + -> [t] + Just Thread { threadStatus = ThreadDone } -> [ ] + Nothing -> [ ] + ] + + unblockedIds :: [IOSimThreadId] + !unblockedIds = map threadId unblocked + + -- and in which case we mark them as now running + !threads' = List.foldl' + (flip (Map.adjust + (\t -> t { threadStatus = ThreadRunning, + threadVClock = vClock `leastUpperBoundVClock` threadVClock t }))) + threads unblockedIds + +-- | This function receives a list of TimerTimeout values that represent threads +-- for which the timeout expired and kills the running thread if needed. +-- +-- This function is responsible for the second part of the race condition issue +-- and relates to the 'schedule's 'TimeoutFrame' locking explanation (here is +-- where the assassin threads are launched. So, as explained previously, at this +-- point in code, the timeout expired so we need to interrupt the running +-- thread. If the running thread finished at the same time the timeout expired +-- we have a race condition. To deal with this race condition what we do is +-- look at the lock value. If it is 'Locked' this means that the running thread +-- already finished (or won the race) so we can safely do nothing. Otherwise, if +-- the lock value is 'NotLocked' we need to acquire the lock and launch an +-- assassin thread that is going to interrupt the running one. Note that we +-- should run this interrupting thread in an unmasked state since it might +-- receive a 'ThreadKilled' exception. +-- +forkTimeoutInterruptThreads :: forall s a. + [(IOSimThreadId, TimeoutId, TMVar (IOSim s) IOSimThreadId)] + -> SimState s a + -> ST s (SimState s a) +forkTimeoutInterruptThreads timeoutExpired simState = + foldlM (\st@SimState{ runqueue, threads } + (t, TMVar lock) + -> do + v <- execReadTVar lock + return $ case v of + Nothing -> st { runqueue = insertThread t runqueue, + threads = Map.insert (threadId t) t threads + } + Just _ -> st + ) + simState' + throwToThread + + where + -- we launch a thread responsible for throwing an AsyncCancelled exception + -- to the thread which timeout expired + throwToThread :: [(Thread s a, TMVar (IOSim s) IOSimThreadId)] + + (simState', throwToThread) = List.mapAccumR fn simState timeoutExpired + where + fn :: SimState s a + -> (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' + Nothing -> error ("IOSimPOR: internal error: unknown thread " ++ show tid) + nextId = threadNextTId t + tid' = childThreadId tid nextId + in ( state { threads = Map.insert tid t { threadNextTId = succ nextId } threads } + , ( Thread { threadId = tid', + threadControl = + ThreadControl + (runIOSim $ do + mtid <- myThreadId + v2 <- atomically $ tryPutTMVar lock mtid + when v2 $ + throwTo tid (toException (TimeoutException tmid))) + ForkFrame, + threadStatus = ThreadRunning, + threadMasking = Unmasked, + threadThrowTo = [], + threadClockId = threadClockId t, + threadLabel = Just "timeout-forked-thread", + threadNextTId = 1, + threadStep = 0, + threadVClock = insertVClock tid' 0 + $ threadVClock t, + threadEffect = mempty, + threadRacy = threadRacy t + } + , 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. +-- +-- Also return if it's the main thread or a forked thread since we handle the +-- cases differently. +-- +unwindControlStack :: forall s a. + SomeException + -> Thread s a + -> Timeouts s + -> ( Either Bool (Thread s a) + , Timeouts s + ) +unwindControlStack e thread = \timeouts -> + case threadControl thread of + ThreadControl _ ctl -> unwind (threadMasking thread) ctl timeouts + where + unwind :: forall s' c. MaskingState + -> ControlStack s' c a + -> Timeouts s + -> (Either Bool (Thread s' a), Timeouts s) + unwind _ MainFrame timers = (Left True, timers) + unwind _ ForkFrame timers = (Left False, timers) + unwind _ (MaskFrame _k maskst' ctl) timers = unwind maskst' ctl timers + + unwind maskst (CatchFrame handler k ctl) timers = + case fromException e of + -- not the right type, unwind to the next containing handler + Nothing -> unwind maskst ctl timers + + -- Ok! We will be able to continue the thread with the handler + -- followed by the continuation after the catch + Just e' -> ( Right thread { + -- As per async exception rules, the handler is run + -- masked + threadControl = ThreadControl (handler e') + (MaskFrame k maskst ctl), + threadMasking = atLeastInterruptibleMask maskst + } + , timers + ) + + -- Either Timeout fired or the action threw an exception. + -- - If Timeout fired, then it was possibly during this thread's execution + -- so we need to run the continuation with a Nothing value. + -- - If the timeout action threw an exception we need to keep unwinding the + -- control stack looking for a handler to this exception. + unwind maskst (TimeoutFrame tmid isLockedRef k ctl) timers = + case fromException e of + -- Exception came from timeout expiring + Just (TimeoutException tmid') | tmid == tmid' -> + (Right thread { threadControl = ThreadControl (k Nothing) ctl }, timers') + -- Exception came from a different exception + _ -> unwind maskst ctl timers' + where + -- Remove the timeout associated with the 'TimeoutFrame'. + timers' = IPSQ.delete (coerce tmid) timers + + unwind maskst (DelayFrame tmid _k ctl) timers = + unwind maskst ctl timers' + where + -- Remove the timeout associated with the 'DelayFrame'. + timers' = IPSQ.delete (coerce tmid) timers + + atLeastInterruptibleMask :: MaskingState -> MaskingState + atLeastInterruptibleMask Unmasked = MaskedInterruptible + atLeastInterruptibleMask ms = ms + + +removeMinimums :: (Coercible Int k, Ord p) + => IntPSQ p a + -> Maybe ([k], p, [a], IntPSQ p a) +removeMinimums = \psq -> coerce $ + case IPSQ.minView psq of + Nothing -> Nothing + Just (k, p, x, psq') -> Just (collectAll [k] p [x] psq') + where + collectAll ks p xs psq = + case IPSQ.minView psq of + Just (k, p', x, psq') + | p == p' -> collectAll (k:ks) p (x:xs) psq' + _ -> (reverse ks, p, reverse xs, psq) + +traceMany :: [(SI.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 :: IOSimThreadId -> Map IOSimThreadId (Thread s a) -> Maybe ThreadLabel +lookupThreadLabel tid threads = join (threadLabel <$> Map.lookup tid threads) + + +-- | The most general method of running 'IOSim' is in 'ST' monad. One can +-- recover failures or the result from 'SimTrace' with 'traceResult', or access +-- 'TraceEvent's generated by the computation with 'traceEvents'. A slightly +-- more convenient way is exposed by 'runSimTrace'. +-- +runSimTraceST :: forall s a. IOSim s a -> ST s (SimTrace a) +runSimTraceST mainAction = controlSimTraceST Nothing ControlDefault mainAction + +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) + <$> schedule mainThread initialState { control = control, + control0 = control, + perStepTimeLimit = limit + } + where + mainThread = + Thread { + threadId = ThreadId [], + threadControl = ThreadControl (runIOSim mainAction) MainFrame, + threadStatus = ThreadRunning, + threadMasking = Unmasked, + threadThrowTo = [], + threadClockId = ClockId [], + threadLabel = Just "main", + threadNextTId = 1, + threadStep = 0, + threadVClock = insertVClock (ThreadId []) 0 bottomVClock, + threadEffect = mempty, + threadRacy = False + } + + +-- +-- Executing STM Transactions +-- + +execAtomically :: forall s a c. + SI.Time + -> IOSimThreadId + -> [Labelled IOSimThreadId] + -> Maybe ThreadLabel + -> VarId + -> StmA s a + -> (StmTxResult s a -> ST s (SimTrace c)) + -> ST s (SimTrace c) +execAtomically !time !tid threads !tlbl !nextVid0 !action0 !k0 = + go AtomicallyFrame Map.empty Map.empty [] [] nextVid0 action0 + where + go :: forall b. + StmStack s b a + -> Map TVarId (SomeTVar s) -- set of vars read + -> Map TVarId (SomeTVar s) -- set of vars written + -> [SomeTVar s] -- vars written in order (no dups) + -> [SomeTVar s] -- vars created in order + -> VarId -- var fresh name supply + -> StmA s b + -> ST s (SimTrace c) + go !ctl !read !written !writtenSeq !createdSeq !nextVid !action = + assert localInvariant $ + case action of + ReturnStm x -> + case ctl of + AtomicallyFrame -> do + -- Trace each created TVar + !ds <- traverse (\(SomeTVar tvar) -> traceTVarST tvar True) createdSeq + -- Trace & commit each TVar + !ds' <- Map.elems <$> traverse + (\(SomeTVar tvar) -> do + tr <- traceTVarST tvar False + !_ <- commitTVar tvar + -- Also assert the data invariant that outside a tx + -- the undo stack is empty: + undos <- readTVarUndos tvar + assert (null undos) $ return tr + ) written + + -- Return the vars written, so readers can be unblocked + k0 $ StmTxCommitted x (reverse writtenSeq) + (Map.elems read) + (reverse createdSeq) + (mapMaybe (\TraceValue { traceDynamic } + -> toDyn <$> traceDynamic) + $ ds ++ ds') + (mapMaybe traceString $ ds ++ ds') + nextVid + + BranchFrame _b k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + -- The branch has successfully completed the transaction. Hence, + -- the alternative branch can be ignored. + -- Commit the TVars written in this sub-transaction that are also + -- in the written set of the outer transaction + !_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar) + (Map.intersection written writtenOuter) + -- Merge the written set of the inner with the outer + let written' = Map.union written writtenOuter + writtenSeq' = filter (\(SomeTVar tvar) -> + tvarId tvar `Map.notMember` writtenOuter) + writtenSeq + ++ writtenOuterSeq + createdSeq' = createdSeq ++ createdOuterSeq + -- Skip the orElse right hand and continue with the k continuation + go ctl' read written' writtenSeq' createdSeq' nextVid (k x) + + ThrowStm e -> + throwStm ctl read written nextVid e + + CatchStm a h k -> do + -- Execute the left side in a new frame with an empty written set + let ctl' = BranchFrame (CatchStmA h) k written writtenSeq createdSeq ctl + go ctl' read Map.empty [] [] nextVid a + + Retry -> do + -- Always revert all the TVar writes for the retry + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + case ctl of + AtomicallyFrame -> do + -- Return vars read, so the thread can block on them + k0 $! StmTxBlocked $! Map.elems read + + BranchFrame (OrElseStmA b) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + -- Execute the orElse right hand with an empty written set + let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' + go ctl'' read Map.empty [] [] nextVid b + + BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + -- Retry makes sense only within a OrElse context. If it is a branch other than + -- OrElse left side, then bubble up the `retry` to the frame above. + -- Skip the continuation and propagate the retry into the outer frame + -- using the written set for the outer frame + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry + + OrElse a b k -> do + -- Execute the left side in a new frame with an empty written set + let ctl' = BranchFrame (OrElseStmA b) k written writtenSeq createdSeq ctl + go ctl' read Map.empty [] [] nextVid a + + NewTVar mkId !mbLabel x k -> do + !v <- execNewTVar (mkId nextVid) mbLabel x + -- record a write to the TVar so we know to update its VClock + let written' = Map.insert (tvarId v) (SomeTVar v) written + -- save the value: it will be committed or reverted + !_ <- saveTVar v + go ctl read written' writtenSeq (SomeTVar v : createdSeq) (succ nextVid) (k v) + + LabelTVar !label tvar k -> do + !_ <- writeSTRef (tvarLabel tvar) $! (Just label) + go ctl read written writtenSeq createdSeq nextVid k + + TraceTVar tvar f k -> do + !_ <- writeSTRef (tvarTrace tvar) (Just f) + go ctl read written writtenSeq createdSeq nextVid k + + ReadTVar v k + | tvarId v `Map.member` read -> do + x <- execReadTVar v + go ctl read written writtenSeq createdSeq nextVid (k x) + | otherwise -> do + x <- execReadTVar v + let read' = Map.insert (tvarId v) (SomeTVar v) read + go ctl read' written writtenSeq createdSeq nextVid (k x) + + WriteTVar v x k + | tvarId v `Map.member` written -> do + !_ <- execWriteTVar v x + go ctl read written writtenSeq createdSeq nextVid k + | otherwise -> do + !_ <- saveTVar v + !_ <- execWriteTVar v x + let written' = Map.insert (tvarId v) (SomeTVar v) written + go ctl read written' (SomeTVar v : writtenSeq) createdSeq nextVid k + + SayStm msg k -> do + mbNF <- unsafeIOToST $ tryJust (\e -> case fromException @SomeAsyncException e of + Nothing -> Just e + Just {} -> Nothing) + $ evaluate (force msg) + case mbNF of + Left e -> do + trace <- throwStm ctl read written nextVid e + -- TODO: step + return $ SimPORTrace time tid (-1) tlbl (EventSayEvaluationError e) + $ trace + Right msg' -> do + trace <- go ctl read written writtenSeq createdSeq nextVid k + -- TODO: step + return $ SimPORTrace time tid (-1) tlbl (EventSay msg') trace + + OutputStm x@(Dynamic _ x') k -> do + mbWHNF <- unsafeIOToST $ tryJust (\e -> case fromException @SomeAsyncException e of + Nothing -> Just e + Just {} -> Nothing) + $ evaluate x' + case mbWHNF of + Left e -> do + trace <- throwStm ctl read written nextVid e + -- TODO: step + return $ SimPORTrace time tid (-1) tlbl (EventLogEvaluationError e) + $ trace + Right {} -> do + trace <- go ctl read written writtenSeq createdSeq nextVid k + -- TODO: step + return $ SimPORTrace time tid (-1) tlbl (EventLog x) trace + + LiftSTStm st k -> do + x <- strictToLazyST st + go ctl read written writtenSeq createdSeq nextVid (k x) + + FixStm f k -> do + r <- newSTRef (throw NonTermination) + x <- unsafeInterleaveST $ readSTRef r + let k' = unSTM (f x) $ \x' -> + LiftSTStm (lazyToStrictST (writeSTRef r x')) (\() -> k x') + go ctl read written writtenSeq createdSeq nextVid k' + + where + localInvariant = + Map.keysSet written + == Set.fromList ([ tvarId tvar | SomeTVar tvar <- writtenSeq ] + ++ [ tvarId tvar | SomeTVar tvar <- createdSeq ]) + + -- throw an exception in an STM transaction + throwStm :: forall b. + StmStack s b a + -> Map TVarId (SomeTVar s) + -> Map TVarId (SomeTVar s) + -> VarId + -> SomeException + -> ST s (SimTrace c) + throwStm ctl read written nextVid e = do + -- Revert all the TVar writes + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + case ctl of + AtomicallyFrame -> do + k0 $ StmTxAborted (Map.elems read) (toException e) + + BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + -- Execute the left side in a new frame with an empty written set. + -- but preserve ones that were set prior to it, as specified in the + -- [stm](https://hackage.haskell.org/package/stm/docs/Control-Monad-STM.html#v:catchSTM) package. + let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' + go ctl'' read Map.empty [] [] nextVid (h e) + + BranchFrame (OrElseStmA _r) _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) + + BranchFrame NoOpStmA _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) + + +-- | Special case of 'execAtomically' supporting only var reads and writes +-- +execAtomically' :: StmA s () -> ST s [SomeTVar s] +execAtomically' = go Map.empty + where + go :: Map TVarId (SomeTVar s) -- set of vars written + -> StmA s () + -> ST s [SomeTVar s] + go !written action = case action of + ReturnStm () -> do + return (Map.elems written) + ReadTVar v k -> do + x <- execReadTVar v + go written (k x) + WriteTVar v x k + | tvarId v `Map.member` written -> do + !_ <- execWriteTVar v x + go written k + | otherwise -> do + !_ <- saveTVar v + !_ <- execWriteTVar v x + let written' = Map.insert (tvarId v) (SomeTVar v) written + go written' k + _ -> error "execAtomically': only for special case of reads and writes" + + +execNewTVar :: TVarId -> Maybe String -> a -> ST s (TVar s a) +execNewTVar !tvarId !mbLabel x = do + tvarLabel <- newSTRef mbLabel + tvarCurrent <- newSTRef x + tvarUndo <- newSTRef [] + tvarBlocked <- newSTRef ([], Set.empty) + tvarVClock <- newSTRef bottomVClock + tvarTrace <- newSTRef Nothing + return TVar {tvarId, tvarLabel, + tvarCurrent, tvarUndo, tvarBlocked, tvarVClock, + tvarTrace} + +-- 'execReadTVar' is defined in `Control.Monad.IOSim.Type` and shared with /IOSim/ + +execWriteTVar :: TVar s a -> a -> ST s () +execWriteTVar TVar{tvarCurrent} = writeSTRef tvarCurrent +{-# INLINE execWriteTVar #-} + +execTryPutTMVar :: TMVar (IOSim s) a -> a -> ST s Bool +execTryPutTMVar (TMVar var) a = do + v <- execReadTVar var + case v of + Nothing -> execWriteTVar var (Just a) + >> return True + Just _ -> return False +{-# INLINE execTryPutTMVar #-} + +saveTVar :: TVar s a -> ST s () +saveTVar TVar{tvarCurrent, tvarUndo} = do + -- push the current value onto the undo stack + v <- readSTRef tvarCurrent + !vs <- readSTRef tvarUndo + writeSTRef tvarUndo $! v:vs + +revertTVar :: TVar s a -> ST s () +revertTVar TVar{tvarCurrent, tvarUndo} = do + -- pop the undo stack, and revert the current value + !vs <- readSTRef tvarUndo + !_ <- writeSTRef tvarCurrent (head vs) + writeSTRef tvarUndo $! tail vs +{-# INLINE revertTVar #-} + +commitTVar :: TVar s a -> ST s () +commitTVar TVar{tvarUndo} = do + !vs <- readSTRef tvarUndo + -- pop the undo stack, leaving the current value unchanged + writeSTRef tvarUndo $! tail vs +{-# INLINE commitTVar #-} + +readTVarUndos :: TVar s a -> ST s [a] +readTVarUndos TVar{tvarUndo} = readSTRef tvarUndo + +-- | Trace a 'TVar'. It must be called only on 'TVar's that were new or +-- 'written. +traceTVarST :: TVar s a + -> Bool -- true if it's a new 'TVar' + -> ST s TraceValue +traceTVarST TVar{tvarCurrent, tvarUndo, tvarTrace} new = do + mf <- readSTRef tvarTrace + case mf of + Nothing -> return TraceValue { traceDynamic = (Nothing :: Maybe ()), traceString = Nothing } + Just f -> do + !vs <- readSTRef tvarUndo + v <- readSTRef tvarCurrent + case (new, vs) of + (True, _) -> f Nothing v + (_, _:_) -> f (Just $ last vs) v + _ -> error "traceTVarST: unexpected tvar state" + + + +leastUpperBoundTVarVClocks :: [SomeTVar s] -> ST s VectorClock +leastUpperBoundTVarVClocks tvars = + foldr leastUpperBoundVClock bottomVClock <$> + sequence [readSTRef (tvarVClock r) | SomeTVar r <- tvars] + +-- +-- Blocking and unblocking on TVars +-- + +readTVarBlockedThreads :: TVar s a -> ST s [IOSimThreadId] +readTVarBlockedThreads TVar{tvarBlocked} = fst <$> readSTRef tvarBlocked + +blockThreadOnTVar :: IOSimThreadId -> TVar s a -> ST s () +blockThreadOnTVar tid TVar{tvarBlocked} = do + (tids, tidsSet) <- readSTRef tvarBlocked + when (tid `Set.notMember` tidsSet) $ do + let !tids' = tid : tids + !tidsSet' = Set.insert tid tidsSet + writeSTRef tvarBlocked (tids', tidsSet') + +unblockAllThreadsFromTVar :: TVar s a -> ST s () +unblockAllThreadsFromTVar TVar{tvarBlocked} = do + writeSTRef tvarBlocked ([], Set.empty) + +-- | For each TVar written to in a transaction (in order) collect the threads +-- that blocked on each one (in order). +-- +-- Also, for logging purposes, return an association between the threads and +-- the var writes that woke them. +-- +threadsUnblockedByWrites :: [SomeTVar s] + -> ST s ([IOSimThreadId], Map IOSimThreadId (Set (Labelled TVarId))) +threadsUnblockedByWrites written = do + tidss <- sequence + [ (,) <$> labelledTVarId tvar <*> readTVarBlockedThreads tvar + | SomeTVar tvar <- written ] + -- Threads to wake up, in wake up order, annotated with the vars written that + -- caused the unblocking. + -- We reverse the individual lists because the tvarBlocked is used as a stack + -- so it is in order of last written, LIFO, and we want FIFO behaviour. + let wakeup = ordNub [ tid | (_vid, tids) <- tidss, tid <- reverse tids ] + wokeby = Map.fromListWith Set.union + [ (tid, Set.singleton vid) + | (vid, tids) <- tidss + , tid <- tids ] + return (wakeup, wokeby) + +ordNub :: Ord a => [a] -> [a] +ordNub = go Set.empty + where + go !_ [] = [] + go !s (x:xs) + | x `Set.member` s = go s xs + | otherwise = x : go (Set.insert x s) xs + +-- +-- Steps +-- + +-- | 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' = + -- 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)) + -- 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 = stepThreadId, + threadStep = stepStep, + threadEffect = stepEffect, + threadVClock = stepVClock + } = Step {..} + +-- | 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 + }, + threadEffect thread + ) + +-- | 'updateRaces' turns a current 'Step' into 'StepInfo', and updates all +-- 'activeRaces'. +-- +-- We take care that steps can only race against threads in their +-- 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 :: 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 + + concurrent0 = + Map.keysSet (Map.filter (\t -> not (isThreadDone t) + && threadId t `Set.notMember` + effectForks newEffect + ) threads) + + -- A new step to add to the `activeRaces` list. + newStepInfo :: Maybe StepInfo + !newStepInfo | isNotRacyThreadId tid = Nothing + -- non-racy threads do not race + + | 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 = concurrent Set.\\ effectWakeup newEffect + + -- `step` happened before `newStep` (`newStep` happened after + -- `step`) + happensBefore = step `happensBeforeStep` newStep + + !stepInfoNonDep' + -- `newStep` happened after `step` + | happensBefore = stepInfoNonDep + -- `newStep` did not happen after `step` + | otherwise = newStep : stepInfoNonDep in + + if tid `notElem` concurrent + then let + in stepInfo { stepInfoConcurrent = lessConcurrent + , stepInfoNonDep = stepInfoNonDep' + } + + -- The core of IOSimPOR. Detect if `newStep` is racing with any + -- previous steps and update each `StepInfo`. + else let theseStepsRace = step `racingSteps` newStep + -- `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 + + -- 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 = stepInfoNonDep', + stepInfoRaces = stepInfoRaces' + } + + activeRaces' :: [StepInfo] + !activeRaces' = + case newStepInfo of + Nothing -> updateStepInfo <$> activeRaces + Just si -> si : (updateStepInfo <$> 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 diff --git a/src/Control/Monad/IOSimPOR/QuickCheckUtils.hs b/src/Control/Monad/IOSimPOR/QuickCheckUtils.hs --- a/src/Control/Monad/IOSimPOR/QuickCheckUtils.hs +++ b/src/Control/Monad/IOSimPOR/QuickCheckUtils.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE BangPatterns #-} - {-# OPTIONS_GHC -Wno-name-shadowing #-} module Control.Monad.IOSimPOR.QuickCheckUtils where diff --git a/src/Control/Monad/IOSimPOR/Types.hs b/src/Control/Monad/IOSimPOR/Types.hs --- a/src/Control/Monad/IOSimPOR/Types.hs +++ b/src/Control/Monad/IOSimPOR/Types.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE NamedFieldPuns #-} module Control.Monad.IOSimPOR.Types ( -- * Effects Effect (..) @@ -38,8 +37,8 @@ -- execution step. Only used by *IOSimPOR*. -- data Effect = Effect { - effectReads :: !(Set TVarId), - effectWrites :: !(Set TVarId), + effectReads :: !(Set (Labelled TVarId)), + effectWrites :: !(Set (Labelled TVarId)), effectForks :: !(Set IOSimThreadId), effectThrows :: ![IOSimThreadId], effectWakeup :: !(Set IOSimThreadId) @@ -50,11 +49,11 @@ 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) ]) + [ "reads = " ++ ppList (ppLabelled show) (Set.toList effectReads) | not (null effectReads) ] + ++ [ "writes = " ++ ppList (ppLabelled show) (Set.toList 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) ]) ++ " }" @@ -69,17 +68,11 @@ -- Effect smart constructors -- --- readEffect :: SomeTVar s -> Effect --- readEffect r = mempty{effectReads = Set.singleton $ someTvarId r } - -readEffects :: [SomeTVar s] -> Effect -readEffects rs = mempty{effectReads = Set.fromList (map someTvarId rs)} - --- writeEffect :: SomeTVar s -> Effect --- writeEffect r = mempty{effectWrites = Set.singleton $ someTvarId r } +readEffects :: [Labelled (SomeTVar s)] -> Effect +readEffects rs = mempty{effectReads = Set.fromList (map (someTvarId <$>) rs)} -writeEffects :: [SomeTVar s] -> Effect -writeEffects rs = mempty{effectWrites = Set.fromList (map someTvarId rs)} +writeEffects :: [Labelled (SomeTVar s)] -> Effect +writeEffects rs = mempty{effectWrites = Set.fromList (map (someTvarId <$>) rs)} forkEffect :: IOSimThreadId -> Effect forkEffect tid = mempty{effectForks = Set.singleton tid} @@ -171,16 +164,20 @@ showsPrec d (ScheduleMod tgt ctrl insertion) = showParen (d>10) $ showString "ScheduleMod " . - showsPrec 11 tgt . + showParen True (showString (ppStepId tgt)) . showString " " . showsPrec 11 ctrl . - showString " " . - showsPrec 11 insertion + showString " [" . + showString (List.intercalate "," (map ppStepId insertion)) . + showString "]" -- -- Steps -- +-- | A unit of execution. `deschedule` marks a boundary of a `Step`, see it's +-- haddocks. +-- data Step = Step { stepThreadId :: !IOSimThreadId, stepStep :: !Int, @@ -223,11 +220,18 @@ -- Races -- -data Races = Races { -- These steps may still race with future steps - activeRaces :: ![StepInfo], - -- These steps cannot be concurrent with future steps - completeRaces :: ![StepInfo] - } +-- | Information about all discovered races in a simulation categorised as +-- active and complete races. +-- +-- See 'normalizeRaces' how we split `StepInfo` into the two categories. +-- +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 diff --git a/src/Data/Deque/Strict.hs b/src/Data/Deque/Strict.hs --- a/src/Data/Deque/Strict.hs +++ b/src/Data/Deque/Strict.hs @@ -1,6 +1,4 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE LambdaCase #-} - +{-# LANGUAGE CPP #-} -- | A minimal implementation of a strict deque. -- module Data.Deque.Strict where diff --git a/src/Data/List/Trace.hs b/src/Data/List/Trace.hs --- a/src/Data/List/Trace.hs +++ b/src/Data/List/Trace.hs @@ -1,5 +1,4 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE CPP #-} module Data.List.Trace ( Trace (..) @@ -8,6 +7,7 @@ , fromList , head , tail + , last , filter , length , take @@ -16,7 +16,7 @@ , dropWhile ) where -import Prelude hiding (drop, dropWhile, filter, head, length, tail, take, +import Prelude hiding (drop, dropWhile, filter, head, last, length, tail, take, takeWhile) import Control.Applicative (Alternative (..)) @@ -46,6 +46,10 @@ tail :: Trace a b -> Trace a b tail (Cons _ o) = o tail Nil {} = error "Trace.tail: empty" + +last :: Trace a b -> a +last (Cons _ k) = last k +last (Nil a) = a filter :: (b -> Bool) -> Trace a b -> Trace a b filter _fn o@Nil {} = o diff --git a/test/Test/Control/Concurrent/Class/MonadMVar.hs b/test/Test/Control/Concurrent/Class/MonadMVar.hs --- a/test/Test/Control/Concurrent/Class/MonadMVar.hs +++ b/test/Test/Control/Concurrent/Class/MonadMVar.hs @@ -1,13 +1,11 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TupleSections #-} +{-# LANGUAGE GADTs #-} module Test.Control.Concurrent.Class.MonadMVar where import Control.Concurrent.Class.MonadMVar import Control.Monad.Class.MonadAsync import Control.Monad.Class.MonadFork +import Control.Monad.Class.MonadTest import Control.Monad.Class.MonadTime.SI import Control.Monad.Class.MonadTimer.SI import Data.Bifoldable (bifoldMap) @@ -64,6 +62,7 @@ [ testCase "empty MVar is empty" unit_isEmptyMVar_empty_sim , testCase "full MVar is not empty" unit_isEmptyMVar_full_sim ] + , testProperty "takeMVar is exception safe" prop_takeMVar_exception_safe ] @@ -309,6 +308,29 @@ unit_isEmptyMVar_full_sim = assertBool "full mvar must not be empty" $ runSimOrThrow (prop_isEmptyMVar False) + +-- +-- takeMVar is exception safe +-- +prop_takeMVar_exception_safe :: Property +prop_takeMVar_exception_safe = + exploreSimTrace id (do + exploreRaces + mv <- newMVar (0 :: Int) + t1 <- async $ void $ withMVar mv (\v -> pure (v + 1, ())) + t2 <- async $ void $ do + _ <- withMVar mv (\v -> pure (v + 1, ())) + withMVar mv (\v -> pure (v + 1, ())) + t3 <- async $ cancel t1 + wait t3 + wait t2 + wait t1 + ) (\_ trace -> + case traceResult False trace of + Left FailureDeadlock{} -> + counterexample (ppTrace trace) $ property False + _ -> property True + ) -- -- Utils diff --git a/test/Test/Control/Monad/IOSim.hs b/test/Test/Control/Monad/IOSim.hs --- a/test/Test/Control/Monad/IOSim.hs +++ b/test/Test/Control/Monad/IOSim.hs @@ -1,12 +1,9 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE NumericUnderscores #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE CPP #-} {-# OPTIONS_GHC -Wno-orphans #-} +-- `-fno-full-laziness` is needed for `discardAfter` to work correctly, see +-- `unit_discardAfter` below. +{-# OPTIONS_GHC -fno-full-laziness #-} module Test.Control.Monad.IOSim ( tests @@ -20,8 +17,10 @@ , TimeoutDuration , ActionDuration , singleTimeoutExperiment + , TraceBottom (..) ) where +import Data.Bifoldable (bifoldMap) import Data.Either (isLeft) import Data.Fixed (Micro) #if __GLASGOW_HASKELL__ < 910 @@ -30,7 +29,7 @@ import Data.Functor (($>)) import Data.Time.Clock (picosecondsToDiffTime) -import Control.Exception (ArithException (..), AsyncException) +import Control.Exception (ArithException (..), AsyncException, ErrorCall (..)) import Control.Monad import Control.Monad.Fix import System.IO.Error (ioeGetErrorString, isUserError) @@ -49,6 +48,7 @@ import Test.Control.Monad.Utils import Test.QuickCheck +import Test.QuickCheck.Property as QC import Test.Tasty hiding (after) import Test.Tasty.QuickCheck @@ -56,9 +56,9 @@ tests = testGroup "IOSim" [ testProperty "read/write graph (IO)" prop_stm_graph_io - , testProperty "read/write graph (IOSim)" (withMaxSuccess 1000 prop_stm_graph_sim) + , testProperty "read/write graph (IOSim)" (withNumTests 1000 prop_stm_graph_sim) , testGroup "timeouts" - [ testProperty "IOSim" (withMaxSuccess 1000 prop_timers_ST) + [ testProperty "IOSim" (withNumTests 1000 prop_timers_ST) -- fails since we just use `threadDelay` to schedule timers in `IO`. , testProperty "IO" (expectFailure prop_timers_IO) , testProperty "IOSim: no deadlock" prop_timeout_no_deadlock_Sim @@ -72,9 +72,19 @@ , testProperty "threadDelay and STM" unit_threadDelay_and_stm , testProperty "{register,thread}Delay" unit_registerDelay_threadDelay , testProperty "throwTo and STM" unit_throwTo_and_stm + , testGroup "trace bottom" + [ testProperty "say" unit_trace_bottom_say + , testProperty "dynamic" unit_trace_bottom_dynamic + , testProperty "saySTM" unit_trace_bottom_saySTM + , testProperty "dynamicSTM" unit_trace_bottom_dynamicSTM + ] ] - , testProperty "threadId order (IOSim)" (withMaxSuccess 1000 prop_threadId_order_order_Sim) - , testProperty "forkIO order (IOSim)" (withMaxSuccess 1000 prop_fork_order_ST) + , testGroup "QuickCheck" + [ testProperty "timeout: discardAfter" unit_discardAfter + , testProperty "timeout: within" unit_within + ] + , testProperty "threadId order (IOSim)" (withNumTests 1000 prop_threadId_order_order_Sim) + , testProperty "forkIO order (IOSim)" (withNumTests 1000 prop_fork_order_ST) , testProperty "order (IO)" (expectFailure prop_fork_order_IO) , testProperty "STM wakeup order" prop_wakeup_order_ST , testGroup "throw/catch unit tests" @@ -192,6 +202,10 @@ , testProperty "maintains FIFO order IO" prop_flushTBQueueOrder_IO , testProperty "maintains FIFO order IOSim" prop_flushTBQueueOrder_IOSim ] + , testGroup "tryReadTBQueue" + [ testProperty "works correctly when the queue is empty IO" prop_tryReadEmptyTBQueue_IO + , testProperty "works correctly when the queue is empty IOSim" prop_tryReadEmptyTBQueue_IOSim + ] ] ] @@ -419,7 +433,7 @@ :: Property -- unhandled top level exception -unit_catch_0 = +unit_catch_0 = once $ runSimTraceSay example === ["before"] .&&. case traceResult True (runSimTrace example) of Left (FailureException e) -> property (maybe False (==DivideByZero) $ fromException e) @@ -433,7 +447,7 @@ say "after" -- normal execution of a catch frame -unit_catch_1 = +unit_catch_1 = once $ runSimTraceSay (do catch (say "inner") (\(_e :: IOError) -> say "handler") say "after" @@ -443,7 +457,7 @@ -- catching an exception thrown in a catch frame -unit_catch_2 = +unit_catch_2 = once $ runSimTraceSay (do catch (do say "inner1" _ <- throwIO DivideByZero @@ -456,7 +470,7 @@ -- not catching an exception of the wrong type -unit_catch_3 = +unit_catch_3 = once $ runSimTraceSay (do catch (do say "inner" throwIO DivideByZero) @@ -468,7 +482,7 @@ -- catching an exception in an outer handler -unit_catch_4 = +unit_catch_4 = once $ runSimTraceSay (do catch (catch (do say "inner" throwIO DivideByZero) @@ -481,7 +495,7 @@ -- catching an exception in the inner handler -unit_catch_5 = +unit_catch_5 = once $ runSimTraceSay (do catch (catch (do say "inner" throwIO DivideByZero) @@ -494,7 +508,7 @@ -- catching an exception in the inner handler, rethrowing and catching in outer -unit_catch_6 = +unit_catch_6 = once $ runSimTraceSay (do catch (catch (do say "inner" throwIO DivideByZero) @@ -510,14 +524,14 @@ -- evaluate should catch pure errors unit_evaluate_0 :: Property -unit_evaluate_0 = +unit_evaluate_0 = once $ -- This property also fails if the @error@ is not caught by the sim monad -- and instead reaches the QuickCheck driver. property $ isLeft $ runSim $ evaluate (error "boom" :: ()) -- The sim terminates when the main thread terminates -unit_fork_1 = +unit_fork_1 = once $ runSimTraceSay example === ["parent"] .&&. case traceResult True (runSimTrace example) of Left FailureSloppyShutdown{} -> property True @@ -530,7 +544,7 @@ -- Try works and we can pass exceptions back from threads. -- And terminating with an exception is reported properly. -unit_fork_2 = +unit_fork_2 = once $ runSimTraceSay example === ["parent", "user error (oh noes!)"] .&&. case traceResult True (runSimTrace example) of Left (FailureException e) @@ -562,7 +576,7 @@ :: Property -unit_async_1 = +unit_async_1 = once $ runSimTraceSay (do mtid <- myThreadId say ("main " ++ show mtid) @@ -575,7 +589,7 @@ ["main ThreadId []", "parent ThreadId [1]", "child ThreadId [1]"] -unit_async_2 = +unit_async_2 = once $ runSimTraceSay (do tid <- myThreadId say "before" @@ -586,7 +600,7 @@ ["before"] -unit_async_3 = +unit_async_3 = once $ runSimTraceSay (do tid <- myThreadId catch (do say "before" @@ -597,7 +611,7 @@ ["before", "handler"] -unit_async_4 = +unit_async_4 = once $ runSimTraceSay (do tid <- forkIO $ say "child" threadDelay 1 @@ -608,7 +622,7 @@ ["child", "parent done"] -unit_async_5 = +unit_async_5 = once $ runSimTraceSay (do tid <- forkIO $ do say "child" @@ -623,7 +637,7 @@ ["child", "handler", "child done", "parent done"] -unit_async_6 = +unit_async_6 = once $ runSimTraceSay (do tid <- forkIO $ mask_ $ do @@ -643,7 +657,7 @@ ["child", "child masked", "handler", "child done", "parent done"] -unit_async_7 = +unit_async_7 = once $ runSimTraceSay (do tid <- forkIO $ mask $ \restore -> do @@ -663,7 +677,7 @@ ["child", "child masked", "handler", "child done", "parent done"] -unit_async_8 = +unit_async_8 = once $ runSimTraceSay (do tid <- forkIO $ do catch (do mask_ $ do @@ -683,7 +697,7 @@ ["child", "child masked", "handler", "child done", "parent done"] -unit_async_9 = +unit_async_9 = once $ runSimTraceSay (do tid <- forkIO $ mask_ $ do @@ -699,7 +713,7 @@ ["child", "parent done"] -unit_async_10 = +unit_async_10 = once $ runSimTraceSay (do tid1 <- forkIO $ do mask_ $ do @@ -727,7 +741,7 @@ ["child 1", "child 2", "child 1 running", "parent done"] -unit_async_11 = +unit_async_11 = once $ runSimTraceSay (do tid1 <- forkIO $ do mask_ $ do @@ -759,7 +773,7 @@ ["child 1", "child 2", "child 1 running", "parent done"] -unit_async_12 = +unit_async_12 = once $ runSimTraceSay (do tid <- forkIO $ do uninterruptibleMask_ $ do @@ -780,7 +794,7 @@ ["child", "child masked", "child done", "parent done"] -unit_async_13 = +unit_async_13 = once $ case runSim (uninterruptibleMask_ $ do tid <- forkIO $ atomically retry @@ -789,7 +803,7 @@ _ -> property False -unit_async_14 = +unit_async_14 = once $ runSimTraceSay (do tid <- forkIO $ do uninterruptibleMask_ $ do @@ -810,7 +824,7 @@ ["child", "child masked", "child done", "parent done"] -unit_async_15 = +unit_async_15 = once $ runSimTraceSay (do tid <- forkIO $ uninterruptibleMask $ \restore -> do @@ -830,7 +844,7 @@ ["child", "child masked", "handler", "child done", "parent done"] -unit_async_16 = +unit_async_16 = once $ runSimTraceSay (do tid <- forkIO $ do catch (do uninterruptibleMask_ $ do @@ -889,7 +903,6 @@ , MonadMask m , MonadThrow (STM m) , MonadSay m - , MonadMaskingState m ) instance Arbitrary DiffTime where @@ -1076,8 +1089,50 @@ = Just Nothing +-- | Check that `discardAfter` works as expected. +-- +-- NOTE: using `discardAfter` with `IOSim` is more tricky than for `IO` +-- properties, since `IOSim` is a pure computation. One need to wrap the +-- simulation in a lambda and use `-fno-full-laziness` to avoid GHC from +-- moving the thunk outside of the lambda, and evaluating it just once. +-- +unit_discardAfter :: Property +unit_discardAfter = once + . mapTotalResult f + . discardAfter 10 + $ \() -> runSimOrThrow $ True <$ (forever (threadDelay 10)) + where + -- if `discard` kills the computation with the `Timeout` exception, + -- `theException` is `Nothing`, but if `traceResult` wraps it, then it is + -- a `Just`. We mark each test a success if `theException` is `Nothing`, + -- otherwise the test would fail with too many discarded cases, but if we re + -- introduce the bug in `traceResult` then it fails, since then + -- `theException` is a `Just`. + f :: QC.Result -> QC.Result + f r@MkResult { QC.theException = Nothing } + = r { ok = Just True } + f r = r + + +-- | Check that `within` works as expected. +-- +unit_within :: Property +unit_within = once + . mapTotalResult f + . within 10 + $ runSimOrThrow $ True <$ (forever (threadDelay 10)) + where + -- if `within` kills the computation with the `Timeout` exception, + -- `theException` is `Nothing`, but if `traceResult` wraps it, then it is + -- a `Just`. + f :: QC.Result -> QC.Result + f r@MkResult { QC.theException = Nothing } + = r { expect = False } + f r = r + + unit_timeouts_and_async_exceptions_1 :: Property -unit_timeouts_and_async_exceptions_1 = +unit_timeouts_and_async_exceptions_1 = once $ let trace = runSimTrace experiment in counterexample (ppTrace_ trace) . either (\e -> counterexample (show e) False) id @@ -1098,7 +1153,7 @@ unit_timeouts_and_async_exceptions_2 :: Property -unit_timeouts_and_async_exceptions_2 = +unit_timeouts_and_async_exceptions_2 = once $ let trace = runSimTrace experiment in counterexample (ppTrace_ trace) . either (\e -> counterexample (show e) False) id @@ -1119,7 +1174,7 @@ unit_timeouts_and_async_exceptions_3 :: Property -unit_timeouts_and_async_exceptions_3 = +unit_timeouts_and_async_exceptions_3 = once $ let trace = runSimTrace experiment in counterexample (ppTrace_ trace) . either (\e -> counterexample (show e) False) id @@ -1143,7 +1198,7 @@ -- transaction. -- unit_threadDelay_and_stm :: Property -unit_threadDelay_and_stm = +unit_threadDelay_and_stm = once $ let trace = runSimTrace experiment in counterexample (ppTrace_ trace) . either (\e -> counterexample (show e) False) id @@ -1171,7 +1226,7 @@ return (t1 `diffTime` t0 === delay) unit_registerDelay_threadDelay :: Property -unit_registerDelay_threadDelay = +unit_registerDelay_threadDelay = once $ let trace = runSimTrace experiment in counterexample (ppTrace_ trace) . either (\e -> counterexample (show e) False) id @@ -1203,7 +1258,7 @@ -- transaction. -- unit_throwTo_and_stm :: Property -unit_throwTo_and_stm = +unit_throwTo_and_stm = once $ let trace = runSimTrace experiment in counterexample (ppTrace_ trace) . either (\e -> counterexample (show e) False) id @@ -1232,68 +1287,116 @@ return (t1 `diffTime` t0 === delay) + +data TraceBottom = TraceBottomSay + | TraceBottomDynamic + | TraceBottomSaySTM + | TraceBottomDynamicSTM + +prop_trace_bottom :: TraceBottom -> Property +prop_trace_bottom tb = + let trace = runSimTrace sim in + property $ + bifoldMap + (\_ -> Some False) + (\ev -> + case seType ev of + EventSayEvaluationError e + | Just ErrorCall{} <- fromException e + -> Some True + EventLogEvaluationError e + | Just ErrorCall{} <- fromException e + -> Some True + _ -> Some False + ) + trace + where + sim :: IOSim s () + sim = case tb of + TraceBottomSay -> + say (error "bottom") + TraceBottomDynamic -> + traceM (error "bottom" :: String) + TraceBottomSaySTM -> + atomically $ say (error "bottom") + TraceBottomDynamicSTM -> + atomically $ traceSTM (error "bottom" :: String) + +unit_trace_bottom_say :: Property +unit_trace_bottom_say = once (prop_trace_bottom TraceBottomSay) + +unit_trace_bottom_dynamic :: Property +unit_trace_bottom_dynamic = once (prop_trace_bottom TraceBottomDynamic) + +unit_trace_bottom_saySTM :: Property +unit_trace_bottom_saySTM = once (prop_trace_bottom TraceBottomSaySTM) + +unit_trace_bottom_dynamicSTM :: Property +unit_trace_bottom_dynamicSTM = once (prop_trace_bottom TraceBottomDynamicSTM) + + -- -- MonadMask properties -- unit_set_masking_state_IO :: MaskingState -> Property -unit_set_masking_state_IO = +unit_set_masking_state_IO = once . ioProperty . prop_set_masking_state unit_set_masking_state_ST :: MaskingState -> Property -unit_set_masking_state_ST ms = +unit_set_masking_state_ST ms = once $ runSimOrThrow (prop_set_masking_state ms) unit_unmask_IO :: MaskingState -> MaskingState -> Property -unit_unmask_IO ms ms' = ioProperty $ prop_unmask ms ms' +unit_unmask_IO ms ms' = once $ ioProperty $ prop_unmask ms ms' unit_unmask_ST :: MaskingState -> MaskingState -> Property -unit_unmask_ST ms ms' = runSimOrThrow $ prop_unmask ms ms' +unit_unmask_ST ms ms' = once $ runSimOrThrow $ prop_unmask ms ms' unit_fork_masking_state_IO :: MaskingState -> Property -unit_fork_masking_state_IO = +unit_fork_masking_state_IO = once . ioProperty . prop_fork_masking_state unit_fork_masking_state_ST :: MaskingState -> Property -unit_fork_masking_state_ST ms = +unit_fork_masking_state_ST ms = once $ runSimOrThrow (prop_fork_masking_state ms) unit_fork_unmask_IO :: MaskingState -> MaskingState -> Property -unit_fork_unmask_IO ms ms' = ioProperty $ prop_fork_unmask ms ms' +unit_fork_unmask_IO ms ms' = once $ ioProperty $ prop_fork_unmask ms ms' unit_fork_unmask_ST :: MaskingState -> MaskingState -> Property -unit_fork_unmask_ST ms ms' = runSimOrThrow $ prop_fork_unmask ms ms' +unit_fork_unmask_ST ms ms' = once $ runSimOrThrow $ prop_fork_unmask ms ms' unit_catch_throwIO_masking_state_IO :: MaskingState -> Property -unit_catch_throwIO_masking_state_IO ms = +unit_catch_throwIO_masking_state_IO ms = once $ ioProperty $ prop_catch_throwIO_masking_state ms unit_catch_throwIO_masking_state_ST :: MaskingState -> Property -unit_catch_throwIO_masking_state_ST ms = +unit_catch_throwIO_masking_state_ST ms = once $ runSimOrThrow (prop_catch_throwIO_masking_state ms) unit_catch_throwTo_masking_state_IO :: MaskingState -> Property -unit_catch_throwTo_masking_state_IO = +unit_catch_throwTo_masking_state_IO = once . ioProperty . prop_catch_throwTo_masking_state unit_catch_throwTo_masking_state_ST :: MaskingState -> Property -unit_catch_throwTo_masking_state_ST ms = +unit_catch_throwTo_masking_state_ST ms = once $ runSimOrThrow $ prop_catch_throwTo_masking_state ms unit_catch_throwTo_masking_state_async_IO :: MaskingState -> Property -unit_catch_throwTo_masking_state_async_IO = +unit_catch_throwTo_masking_state_async_IO = once . ioProperty . prop_catch_throwTo_masking_state_async unit_catch_throwTo_masking_state_async_ST :: MaskingState -> Property -unit_catch_throwTo_masking_state_async_ST ms = +unit_catch_throwTo_masking_state_async_ST ms = once $ runSimOrThrow (prop_catch_throwTo_masking_state_async ms) unit_catch_throwTo_masking_state_async_mayblock_IO :: MaskingState -> Property -unit_catch_throwTo_masking_state_async_mayblock_IO = +unit_catch_throwTo_masking_state_async_mayblock_IO = once . ioProperty . prop_catch_throwTo_masking_state_async_mayblock unit_catch_throwTo_masking_state_async_mayblock_ST :: MaskingState -> Property -unit_catch_throwTo_masking_state_async_mayblock_ST ms = +unit_catch_throwTo_masking_state_async_mayblock_ST ms = once $ runSimOrThrow (prop_catch_throwTo_masking_state_async_mayblock ms) -- @@ -1463,6 +1566,24 @@ q <- newTBQueue (1 + fromIntegral (length entries)) forM_ entries $ writeTBQueue q flushTBQueue q + +prop_tryReadEmptyTBQueue_IO :: Bool -> Property +prop_tryReadEmptyTBQueue_IO sndRead = + ioProperty $ tryReadEmptyTBQueue sndRead + +prop_tryReadEmptyTBQueue_IOSim :: Bool -> Property +prop_tryReadEmptyTBQueue_IOSim sndRead = + runSimOrThrow $ tryReadEmptyTBQueue sndRead + +tryReadEmptyTBQueue :: MonadSTM m => Bool -> m Property +tryReadEmptyTBQueue sndRead = atomically $ do + q <- newTBQueue 10 + _ <- tryReadTBQueue q + writeTBQueue q () + when sndRead $ void $ tryReadTBQueue q + l <- lengthTBQueue q + + pure $ l === if sndRead then 0 else 1 -- -- Utils diff --git a/test/Test/Control/Monad/IOSimPOR.hs b/test/Test/Control/Monad/IOSimPOR.hs --- a/test/Test/Control/Monad/IOSimPOR.hs +++ b/test/Test/Control/Monad/IOSimPOR.hs @@ -1,16 +1,12 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE PartialTypeSignatures #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveGeneric #-} {-# OPTIONS_GHC -Wno-unused-top-binds #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Test.Control.Monad.IOSimPOR (tests) where +import Data.Bifoldable (bifoldMap) import Data.Fixed (Micro) #if __GLASGOW_HASKELL__ >= 910 import Data.Foldable (traverse_) @@ -25,7 +21,7 @@ import System.Exit import System.IO.Error (ioeGetErrorString, isUserError) -import Control.Exception (ArithException (..), AsyncException) +import Control.Exception (ArithException (..), AsyncException, ErrorCall (..)) import Control.Monad import Control.Monad.Fix @@ -42,13 +38,14 @@ import GHC.Generics import Test.Control.Monad.IOSim (ActionDuration, TimeoutDuration, - WithSanityCheck (..), ignoreSanityCheck, isSanityCheckIgnored, - singleTimeoutExperiment, withSanityCheck) + TraceBottom (..), WithSanityCheck (..), ignoreSanityCheck, + isSanityCheckIgnored, singleTimeoutExperiment, withSanityCheck) import Test.Control.Monad.STM import Test.Control.Monad.Utils import Data.List.Trace qualified as Trace import Test.QuickCheck +import Test.QuickCheck.Monadic (assert, run) import Test.Tasty (TestTree, testGroup) import Test.Tasty.QuickCheck @@ -73,18 +70,24 @@ -- , testProperty "propPermutations" propPermutations ] , testGroup "IO simulator properties" - [ testProperty "read/write graph (IOSim)" (withMaxSuccess 1000 prop_stm_graph_sim) + [ testProperty "read/write graph (IOSim)" (withNumTests 1000 prop_stm_graph_sim) , testGroup "timeouts" - [ testProperty "IOSim" (withMaxSuccess 1000 prop_timers_ST) + [ testProperty "IOSim" (withNumTests 1000 prop_timers_ST) , testProperty "IOSim: no deadlock" prop_timeout_no_deadlock_Sim , testProperty "timeout" prop_timeout , testProperty "timeouts" prop_timeouts , testProperty "stacked timeouts" prop_stacked_timeouts , testProperty "{register,thread}Delay" unit_registerDelay_threadDelay + , testGroup "trace bottom" + [ testProperty "say" unit_trace_bottom_say + , testProperty "dynamic" unit_trace_bottom_dynamic + , testProperty "saySTM" unit_trace_bottom_saySTM + , testProperty "dynamicSTM" unit_trace_bottom_dynamicSTM + ] ] , testProperty "infinite simulation" prop_explore_endless_simulation - , testProperty "threadId order (IOSim)" (withMaxSuccess 1000 prop_threadId_order_order_Sim) - , testProperty "forkIO order (IOSim)" (withMaxSuccess 1000 prop_fork_order_ST) + , testProperty "threadId order (IOSim)" (withNumTests 1000 prop_threadId_order_order_Sim) + , testProperty "forkIO order (IOSim)" (withNumTests 1000 prop_fork_order_ST) , testGroup "throw/catch unit tests" [ testProperty "0" unit_catch_0 , testProperty "1" unit_catch_1 @@ -121,6 +124,11 @@ , testProperty "catch: throwTo async blocking (IOSim)" $ forall_masking_states unit_catch_throwTo_masking_state_async_mayblock_ST ] + , testGroup "PropertyM callbacks" + [ testProperty "happy path" unit_monadicIOSimPOR_0 + , testProperty "failing assert" unit_monadicIOSimPOR_1 + , testProperty "exception" unit_monadicIOSimPOR_2 + ] , testProperty "evaluate unit test" unit_evaluate_0 , testGroup "forkIO unit tests" [ testProperty "1" unit_fork_1 @@ -434,16 +442,32 @@ threadDelay 1 readTVarIO r - -traceNoDuplicates :: (Testable prop1, Show a1) => ((a1 -> a2 -> a2) -> prop1) -> Property -traceNoDuplicates k = r `pseq` (k addTrace .&&. maximum (traceCounts ()) == 1) +traceNoDuplicates :: forall a b. + (Show a) + => ((a -> b -> b) -> Property) + -> Property +-- this NOINLINE pragma is useful for debugging if `r` didn't flow outside of +-- `traceNoDuplicate`. +{-# NOINLINE traceNoDuplicates #-} +traceNoDuplicates k = unsafePerformIO $ do + r <- newIORef (Map.empty :: Map String Int) + return $ r `pseq` + (k (addTrace r) .&&. counterexample "trace counts" (maximum (Map.elems (traceCounts r)) === 1)) where - r = unsafePerformIO $ newIORef (Map.empty :: Map String Int) - addTrace t x = unsafePerformIO $ do - atomicModifyIORef r (\m->(Map.insertWith (+) (show t) 1 m,())) + addTrace :: IORef (Map String Int) -> a -> b -> b + addTrace r t x = unsafePerformIO $ do + let s = show t + atomicModifyIORef r + (\m-> + let m' = Map.insertWith (+) s 1 m + in (m', ()) + ) return x - traceCounts () = unsafePerformIO $ Map.elems <$> readIORef r + traceCounts :: IORef (Map String Int) -> Map String Int + traceCounts r = unsafePerformIO $ readIORef r + + -- | Checks that IOSimPOR is capable of analysing an infinite simulation -- lazily. -- @@ -739,6 +763,30 @@ ) $ \_ trace -> selectTraceSay trace === ["inner", "handler1", "handler2", "after"] +unit_monadicIOSimPOR_0, unit_monadicIOSimPOR_1, unit_monadicIOSimPOR_2 + :: Property + +-- | Basic success case: a PropertyM test can be executed through IOSimPOR. +unit_monadicIOSimPOR_0 = + monadicIOSimPOR_ $ do + x <- run (pure (1 :: Int)) + assert (x == 1) + +-- | Failing assertions inside PropertyM are reported as property failures. +unit_monadicIOSimPOR_1 = + expectFailure $ + monadicIOSimPOR_ $ do + x <- run (pure (1 :: Int)) + assert (x == 2) + +-- | Exceptions thrown by the simulation are turned into failing properties via +-- `traceResult False`, matching the manual workaround from issue #229. +unit_monadicIOSimPOR_2 = + expectFailure $ + monadicIOSimPOR_ $ do + _ <- run $ evaluate (error "boom" :: ()) + assert True + -- evaluate should catch pure errors unit_evaluate_0 :: Property unit_evaluate_0 = @@ -1042,6 +1090,49 @@ t1 <- getMonotonicTime return (t1 `diffTime` t0 === delay) + + +prop_trace_bottom :: TraceBottom -> Property +prop_trace_bottom tb = + exploreSimTrace id sim $ \_ trace -> + property $ + bifoldMap + (\_ -> Some False) + (\ev -> + case seType ev of + EventSayEvaluationError e + | Just ErrorCall{} <- fromException e + -> Some True + EventLogEvaluationError e + | Just ErrorCall{} <- fromException e + -> Some True + _ -> Some False + ) + trace + where + sim :: IOSim s () + sim = case tb of + TraceBottomSay -> + say (error "bottom") + TraceBottomDynamic -> + traceM (error "bottom" :: String) + TraceBottomSaySTM -> + atomically $ say (error "bottom") + TraceBottomDynamicSTM -> + atomically $ traceSTM (error "bottom" :: String) + +unit_trace_bottom_say :: Property +unit_trace_bottom_say = once (prop_trace_bottom TraceBottomSay) + +unit_trace_bottom_dynamic :: Property +unit_trace_bottom_dynamic = once (prop_trace_bottom TraceBottomDynamic) + +unit_trace_bottom_saySTM :: Property +unit_trace_bottom_saySTM = once (prop_trace_bottom TraceBottomSaySTM) + +unit_trace_bottom_dynamicSTM :: Property +unit_trace_bottom_dynamicSTM = once (prop_trace_bottom TraceBottomDynamicSTM) + unit_timeouts_and_async_exceptions_1 :: Property unit_timeouts_and_async_exceptions_1 = diff --git a/test/Test/Control/Monad/STM.hs b/test/Test/Control/Monad/STM.hs --- a/test/Test/Control/Monad/STM.hs +++ b/test/Test/Control/Monad/STM.hs @@ -1,14 +1,7 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-} diff --git a/test/Test/Control/Monad/Utils.hs b/test/Test/Control/Monad/Utils.hs --- a/test/Test/Control/Monad/Utils.hs +++ b/test/Test/Control/Monad/Utils.hs @@ -1,7 +1,4 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} - +{-# LANGUAGE CPP #-} module Test.Control.Monad.Utils where import Data.Array @@ -22,6 +19,11 @@ import Test.QuickCheck +#if !MIN_VERSION_QuickCheck(2,18,0) +withNumTests :: Testable prop => Int -> prop -> Property +withNumTests = withMaxSuccess +#endif + -- -- Read/Write graph -- @@ -340,7 +342,7 @@ -- | Check that setting masking state is effective. -- -prop_set_masking_state :: MonadMaskingState m +prop_set_masking_state :: MonadMask m => MaskingState -> m Property prop_set_masking_state ms = @@ -350,7 +352,7 @@ -- | Check that 'unmask' restores the masking state. -- -prop_unmask :: MonadMaskingState m +prop_unmask :: MonadMask m => MaskingState -> MaskingState -> m Property @@ -362,7 +364,7 @@ -- | Check that masking state is inherited by a forked thread. -- -prop_fork_masking_state :: ( MonadMaskingState m +prop_fork_masking_state :: ( MonadMask m , MonadFork m , MonadSTM m ) @@ -378,7 +380,7 @@ -- Note: unlike 'prop_unmask', 'forkIOWithUnmask's 'unmask' function will -- restore 'Unmasked' state, not the encosing masking state. -- -prop_fork_unmask :: ( MonadMaskingState m +prop_fork_unmask :: ( MonadMask m , MonadFork m , MonadSTM m ) @@ -397,8 +399,9 @@ -- | A unit test which checks the masking state in the context of a catch -- handler. -- -prop_catch_throwIO_masking_state :: forall m. MonadMaskingState m - => MaskingState -> m Property +prop_catch_throwIO_masking_state :: forall m. MonadMask m + => MaskingState + -> m Property prop_catch_throwIO_masking_state ms = setMaskingState_ ms $ do throwIO (userError "error") @@ -409,7 +412,7 @@ -- | Like 'prop_catch_masking_state' but using 'throwTo'. -- prop_catch_throwTo_masking_state :: forall m. - ( MonadMaskingState m + ( MonadMask m , MonadFork m ) => MaskingState -> m Property @@ -425,7 +428,7 @@ -- thread which is in a non-blocking mode. -- prop_catch_throwTo_masking_state_async :: forall m. - ( MonadMaskingState m + ( MonadMask m , MonadFork m , MonadSTM m , MonadDelay m @@ -454,7 +457,7 @@ -- 'willBlock' branch of 'ThrowTo' in 'schedule' is covered. -- prop_catch_throwTo_masking_state_async_mayblock :: forall m. - ( MonadMaskingState m + ( MonadMask m , MonadFork m , MonadSTM m , MonadDelay m @@ -492,7 +495,7 @@ -> Property forall_masking_states prop = -- make sure that the property is executed once! - withMaxSuccess 1 $ + withNumTests 1 $ foldr (\ms p -> counterexample (show ms) (prop ms) .&&. p) (property True) [Unmasked, MaskedInterruptible, MaskedUninterruptible]