diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,40 @@ # Revision history of io-sim +## next release + +### Breaking changes + +### Non-breaking changes + +## 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.8.0.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 } flag asserts description: Enable assertions @@ -56,31 +60,15 @@ 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 + build-depends: base >=4.9 && <4.22, io-classes:{io-classes,strict-stm,si-timers} - ^>=1.6, + ^>=1.6 || ^>= 1.7 || ^>= 1.8, exceptions >=0.10, containers, deepseq, + hashable, nothunks, primitive >=0.7 && <0.11, psqueues >=0.2 && <0.3, @@ -104,8 +92,8 @@ Test.Control.Monad.Utils Test.Control.Monad.IOSim Test.Control.Monad.IOSimPOR - default-language: Haskell2010 - default-extensions: ImportQualifiedPost + default-language: GHC2021 + default-extensions: LambdaCase build-depends: base, array, containers, @@ -126,8 +114,8 @@ 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 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 @@ -42,6 +38,7 @@ , unshareClock -- * Simulation trace , type SimTrace + , Time (..) , Trace (Cons, Nil, SimTrace, SimPORTrace, TraceDeadlock, TraceLoop, TraceMainReturn, TraceMainException, TraceRacesFound, TraceInternalError) , traceEvents , traceResult @@ -144,11 +141,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 +223,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 +266,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 +278,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) 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,6 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE DerivingVia #-} -- | Common types shared between `IOSim` and `IOSimPOR`. -- @@ -16,6 +12,7 @@ , childThreadId , setRacyThread , TVarId (..) + , VarId , TimeoutId (..) , ClockId (..) , VectorClock (..) @@ -25,9 +22,12 @@ , TVarLabel , TVar (..) , SomeTVar (..) + , someTVarToLabelled , Deschedule (..) , ThreadStatus (..) , BlockedReason (..) + , Labelled (..) + , ppLabelled -- * Utils , ppList ) where @@ -38,6 +38,7 @@ import NoThunks.Class +import Data.Hashable import Data.List (intercalate, intersperse) import Data.Map (Map) import Data.Map qualified as Map @@ -65,6 +66,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 +91,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 +155,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 +165,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 +186,21 @@ | 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] -- -- 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,17 +40,18 @@ 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) @@ -134,7 +127,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,7 +142,7 @@ timers :: !(Timeouts s), -- | list of clocks clocks :: !(Map ClockId UTCTime), - nextVid :: !TVarId, -- ^ next unused 'TVarId' + nextVid :: !VarId, -- ^ next unused 'VarId' nextTmid :: !TimeoutId -- ^ next unused 'TimeoutId' } @@ -161,7 +154,7 @@ curTime = Time 0, timers = PSQ.empty, clocks = Map.singleton (ClockId []) epoch1970, - nextVid = TVarId 0, + nextVid = 0, nextTmid = TimeoutId 0 } where @@ -263,7 +256,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 @@ -358,9 +351,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 +366,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 +403,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 +417,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 +540,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 @@ -918,8 +918,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 +955,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 +969,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 +1023,7 @@ Time -> IOSimThreadId -> Maybe ThreadLabel - -> TVarId + -> VarId -> StmA s a -> (StmTxResult s a -> ST s (SimTrace c)) -> ST s (SimTrace c) @@ -1036,7 +1036,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 = @@ -1138,8 +1138,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 @@ -1222,16 +1222,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,9 +146,7 @@ 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 @@ -234,7 +229,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 +256,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 +277,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 +350,7 @@ takeMVarDefault :: ( MonadMask m - , MonadSTM m + , MonadLabelledSTM m , forall x tvar. tvar ~ TVar m x => Eq tvar ) => MVarDefault m a @@ -362,6 +362,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 +393,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 +451,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 +464,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,13 @@ -{-# 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 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 +49,11 @@ , ppTrace_ , ppSimEvent , ppDebug - , Labelled (..) , module Control.Monad.IOSim.CommonTypes , Thrower (..) - , Time (..) - , addTime - , diffTime + , SI.Time (..) + , SI.addTime + , SI.diffTime -- * Internal API , Timeout (..) , newTimeout @@ -91,14 +81,15 @@ 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 @@ -168,7 +159,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 +177,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 @@ -219,7 +211,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 +228,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 @@ -424,7 +416,6 @@ MaskedInterruptible -> blockUninterruptible $ action block MaskedUninterruptible -> action blockUninterruptible -instance MonadMaskingState (IOSim s) where getMaskingState = getMaskingStateImpl interruptible action = do b <- getMaskingStateImpl @@ -433,6 +424,8 @@ MaskedInterruptible -> unblock action MaskedUninterruptible -> action +instance MonadMaskingState (IOSim s) + instance Exceptions.MonadMask (IOSim s) where mask = MonadThrow.mask uninterruptibleMask = MonadThrow.uninterruptibleMask @@ -469,6 +462,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,6 +472,7 @@ 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 ()) @@ -507,14 +502,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 +520,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 +530,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 +545,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 +563,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 +585,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 +603,29 @@ 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 + data Async s a = Async !IOSimThreadId (STM s (Either SomeException a)) instance Eq (Async s a) where @@ -665,10 +686,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 @@ -781,14 +802,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), @@ -808,29 +829,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 +855,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 +877,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 +887,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 +897,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 +934,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 +952,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 +988,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 +1006,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) @@ -1063,22 +1080,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`) @@ -1209,22 +1226,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 +1250,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,21 +1,13 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE CPP #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTSyntax #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingVia #-} -- only used to construct records if its clear to do so -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} +{-# 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 #-} @@ -53,14 +45,16 @@ 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.OrdPSQ (OrdPSQ) -import Data.OrdPSQ qualified as PSQ import Data.Set (Set) import Data.Set qualified as Set import Data.Time (UTCTime (..), fromGregorian) @@ -77,14 +71,19 @@ 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.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), Trace (SimTrace)) +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 @@ -178,9 +177,11 @@ -- ^ `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) +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 { @@ -189,13 +190,13 @@ -- and blocked threads. threads :: !(Map IOSimThreadId (Thread s a)), -- | current time - curTime :: !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 :: !TVarId, -- ^ next unused 'TVarId' + nextVid :: !VarId, -- ^ 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. @@ -214,10 +215,10 @@ SimState { runqueue = PSQ.empty, threads = Map.empty, - curTime = Time 0, - timers = PSQ.empty, + curTime = SI.Time 0, + timers = IPSQ.empty, clocks = Map.singleton (ClockId []) epoch1970, - nextVid = TVarId 0, + nextVid = 0, nextTmid = TimeoutId 0, races = noRaces, control = ControlDefault, @@ -240,16 +241,13 @@ 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) +timeSinceEpoch :: SI.Time -> NominalDiffTime +timeSinceEpoch (SI.Time t) = fromRational (toRational t) -- | Insert thread into `runqueue`. @@ -372,7 +370,7 @@ DelayFrame tmid k ctl' -> do let thread' = thread { threadControl = ThreadControl k ctl' } - timers' = PSQ.delete tmid timers + timers' = IPSQ.delete (coerce tmid) timers schedule thread' simstate { timers = timers' } Throw e -> case unwindControlStack e thread timers of @@ -453,15 +451,15 @@ GetWallTime k -> do let clockid = threadClockId thread clockoff = clocks Map.! clockid - walltime = timeSinceEpoch time `addUTCTime` clockoff + 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 `addUTCTime` clockoff - clockoff' = addUTCTime (diffUTCTime walltime' walltime) clockoff + 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' @@ -480,9 +478,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' = IPSQ.insert (coerce nextTmid) expiry (TimerTimeout tid nextTmid lock) timers thread' = thread { threadControl = ThreadControl action' (TimeoutFrame nextTmid lock k ctl) @@ -493,33 +491,33 @@ UnregisterTimeout tmid k -> do let thread' = thread { threadControl = ThreadControl k ctl } - schedule thread' simstate { timers = PSQ.delete tmid timers } + schedule thread' simstate { timers = IPSQ.delete (coerce tmid) timers } RegisterDelay d k | d < 0 -> do - tvar <- execNewTVar nextVid + 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 nextVid expiry) $ + 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 nextVid + tvar <- execNewTVar (TVarId nextVid) (Just $! "<>") False modifySTRef (tvarVClock tvar) (leastUpperBoundVClock vClock) let !expiry = d `addTime` time - !timers' = PSQ.insert nextTmid expiry (TimerRegisterDelay tvar) timers + !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 nextVid expiry) trace) + (EventRegisterDelayCreated nextTmid (TVarId nextVid) expiry) trace) ThreadDelay d k | d < 0 -> do let expiry = d `addTime` time @@ -532,7 +530,7 @@ ThreadDelay d k -> do let expiry = d `addTime` time - timers' = PSQ.insert nextTmid expiry (TimerThreadDelay tid nextTmid) timers + 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', @@ -547,31 +545,32 @@ 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) $ + 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 nextVid + tvar <- execNewTVar (TVarId 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 + 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 nextVid expiry) trace) + , 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' = PSQ.delete tmid timers + 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 + <> writeEffects written' <> wakeupEffects wakeup thread' = thread { threadControl = ThreadControl k ctl , threadEffect = effect' @@ -636,10 +635,12 @@ (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 + <> readEffects read' + <> writeEffects written' <> wakeupEffects unblocked thread' = thread { threadControl = ThreadControl (k x) ctl, threadVClock = vClock', @@ -648,12 +649,12 @@ simstate') = unblockThreads True vClock' wakeup simstate sequence_ [ modifySTRef (tvarVClock r) (leastUpperBoundVClock vClock') | SomeTVar r <- created ++ written ] - written' <- traverse (\(SomeTVar tvar) -> labelledTVarId tvar) 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')) $ + SimPORTrace time tid tstep tlbl (EventTxCommitted written'' created' (Just effect')) $ traceMany [ (time, tid', (-1), tlbl', EventTxWakeup vids') | tid' <- unblocked @@ -674,7 +675,8 @@ StmTxAborted read e -> do -- schedule this thread to immediately raise the exception vClockRead <- leastUpperBoundTVarVClocks read - let effect' = effect <> readEffects read + read' <- mapM someTVarToLabelled read + let effect' = effect <> readEffects read' thread' = thread { threadControl = ThreadControl (Throw e) ctl, threadVClock = vClock `leastUpperBoundVClock` vClockRead, threadEffect = effect' } @@ -686,7 +688,8 @@ mapM_ (\(SomeTVar tvar) -> blockThreadOnTVar tid tvar) read vids <- traverse (\(SomeTVar tvar) -> labelledTVarId tvar) read vClockRead <- leastUpperBoundTVarVClocks read - let effect' = effect <> readEffects read + read' <- mapM someTVarToLabelled read + let effect' = effect <> readEffects read' thread' = thread { threadVClock = vClock `leastUpperBoundVClock` vClockRead, threadEffect = effect' } !trace <- deschedule (Blocked BlockedOnSTM) thread' simstate @@ -703,6 +706,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 @@ -814,6 +824,21 @@ | 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, @@ -1264,34 +1289,34 @@ _ -> unwind maskst ctl timers' where -- Remove the timeout associated with the 'TimeoutFrame'. - timers' = PSQ.delete tmid timers + 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' = PSQ.delete tmid timers + timers' = IPSQ.delete (coerce 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 +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 PSQ.minView psq of + 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 :: [(Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)] +traceMany :: [(SI.Time, IOSimThreadId, Int, Maybe ThreadLabel, SimEventType)] -> SimTrace a -> SimTrace a traceMany [] trace = trace traceMany ((time, tid, tstep, tlbl, event):ts) trace = @@ -1343,10 +1368,10 @@ -- execAtomically :: forall s a c. - Time + SI.Time -> IOSimThreadId -> Maybe ThreadLabel - -> TVarId + -> VarId -> StmA s a -> (StmTxResult s a -> ST s (SimTrace c)) -> ST s (SimTrace c) @@ -1359,7 +1384,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 = @@ -1458,8 +1483,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 -- 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 @@ -1548,14 +1573,14 @@ 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 bottomVClock tvarTrace <- newSTRef Nothing - return TVar {tvarId = nextVid, tvarLabel, + return TVar {tvarId, tvarLabel, tvarCurrent, tvarUndo, tvarBlocked, tvarVClock, tvarTrace} @@ -1837,7 +1862,8 @@ $ activeRaces ) ++ completeRaces - in Races{ activeRaces = activeRaces', completeRaces = 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 (..) 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,10 +1,4 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE NumericUnderscores #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE CPP #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -192,6 +186,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 + ] ] ] @@ -889,7 +887,6 @@ , MonadMask m , MonadThrow (STM m) , MonadSay m - , MonadMaskingState m ) instance Arbitrary DiffTime where @@ -1463,6 +1460,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,10 +1,5 @@ -{-# 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 #-} @@ -434,15 +429,31 @@ 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. 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,3 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} - module Test.Control.Monad.Utils where import Data.Array @@ -340,7 +336,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 +346,7 @@ -- | Check that 'unmask' restores the masking state. -- -prop_unmask :: MonadMaskingState m +prop_unmask :: MonadMask m => MaskingState -> MaskingState -> m Property @@ -362,7 +358,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 +374,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 +393,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 +406,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 +422,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 +451,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