From e542235b162029a7a06f17ed072ad4147862ef3e Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Mon, 11 Jul 2022 13:29:21 +0530 Subject: [PATCH 01/11] Add MonadCatch instance for STM WIP - Add MonadCatch Instance - Add CatchStm and CatchStmFrame - Add handler for CatchStmFrame --- .../src/Control/Monad/Class/MonadThrow.hs | 11 ++++++--- io-sim/src/Control/Monad/IOSim/Internal.hs | 23 ++++++++++++++++--- io-sim/src/Control/Monad/IOSim/Types.hs | 21 +++++++++++++++++ 3 files changed, 49 insertions(+), 6 deletions(-) diff --git a/io-classes/src/Control/Monad/Class/MonadThrow.hs b/io-classes/src/Control/Monad/Class/MonadThrow.hs index 541f6b04..2fe79612 100644 --- a/io-classes/src/Control/Monad/Class/MonadThrow.hs +++ b/io-classes/src/Control/Monad/Class/MonadThrow.hs @@ -18,6 +18,7 @@ module Control.Monad.Class.MonadThrow , ExitCase (..) , Handler (..) , catches + , generalBracketSTM -- * Deprecated interfaces , throwM ) where @@ -241,10 +242,9 @@ instance MonadEvaluate IO where instance MonadThrow STM where throwIO = STM.throwSTM -instance MonadCatch STM where - catch = STM.catchSTM - generalBracket acquire release use = do +generalBracketSTM :: MonadCatch m => m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c) +generalBracketSTM acquire release use = do resource <- acquire b <- use resource `catch` \e -> do _ <- release resource (ExitCaseException e) @@ -252,6 +252,11 @@ instance MonadCatch STM where c <- release resource (ExitCaseSuccess b) return (b, c) +instance MonadCatch STM where + catch = STM.catchSTM + + generalBracket = generalBracketSTM + -- -- Instances for ReaderT diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index a3b889e1..c015185b 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -910,11 +910,24 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = -- Continue with the k continuation go ctl' read written' writtenSeq' createdSeq' nextVid (k x) + CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + undefined + ThrowStm e -> {-# SCC "execAtomically.go.ThrowStm" #-} do - -- Revert all the TVar writes - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - k0 $ StmTxAborted [] (toException e) + case (fromException e, ctl) of + (Just e', CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl') | isException exc -> do + -- Use handler to rescue the exception + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (handler e') + (_, _) -> do + -- Revert all the TVar writes + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + k0 $ StmTxAborted [] (toException e) + + CatchStm act handler k -> + {-# SCC "execAtomically.go.CatchStm" #-} do + let ctl' = CatchStmFrame handler k written writtenSeq createdSeq ctl + go ctl' read Map.empty [] [] nextVid act Retry -> {-# SCC "execAtomically.go.Retry" #-} @@ -941,6 +954,10 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = -- using the written set for the outer frame go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry + CatchStmFrame handler _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.catchStmFrame" #-} do + undefined + OrElse a b k -> {-# SCC "execAtomically.go.OrElse" #-} do -- Execute the left side in a new frame with an empty written set diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index 2dc46fc7..ccdc875d 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -175,6 +175,7 @@ runSTM (STM k) = k ReturnStm data StmA s a where ReturnStm :: a -> StmA s a ThrowStm :: SomeException -> StmA s a + CatchStm :: Exception e => StmA s a -> (e -> StmA s a) -> (a -> StmA s b) -> StmA s b NewTVar :: Maybe String -> x -> (TVar s x -> StmA s b) -> StmA s b LabelTVar :: String -> TVar s a -> StmA s b -> StmA s b @@ -313,6 +314,17 @@ instance MonadThrow (STM s) where instance Exceptions.MonadThrow (STM s) where throwM = MonadThrow.throwIO +instance MonadCatch (STM s) where + + catch action handler = STM $ oneShot $ \k -> CatchStm (runSTM action) (runSTM . handler) k + + -- Default implmentation uses mask. For STM, mask is not necessary. + generalBracket = generalBracketSTM + +instance Exceptions.MonadCatch (STM s) where + + catch = MonadThrow.catch + instance MonadCatch (IOSim s) where catch action handler = IOSim $ oneShot $ \k -> Catch (runIOSim action) (runIOSim . handler) k @@ -853,6 +865,15 @@ data StmStack s b a where -> StmStack s b c -> StmStack s a c + -- | Executing in the context of the /action/ part of the 'catch' + CatchStmFrame :: Exception e + => (e -> StmA s a) -- exception handler + -> (a -> StmA s b) -- subsequent continuation + -> Map TVarId (SomeTVar s) -- saved written vars set + -> [SomeTVar s] -- saved written vars set + -> [SomeTVar s] -- created vars list + -> StmStack s b c + -> StmStack s a c --- --- Schedules --- From b5840bc04db4cc2e9c9b9b1aec56941b3aac0eea Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Tue, 12 Jul 2022 12:46:43 +0530 Subject: [PATCH 02/11] Add Catch semantics for Test.STM Handle return, throw and retry cases for Test.STM --- io-sim/TAGS | 1044 ++++++++++++++++++++ io-sim/src/Control/Monad/IOSim/Internal.hs | 11 +- io-sim/test/Test/IOSim.hs | 2 +- io-sim/test/Test/STM.hs | 40 +- 4 files changed, 1089 insertions(+), 8 deletions(-) create mode 100644 io-sim/TAGS diff --git a/io-sim/TAGS b/io-sim/TAGS new file mode 100644 index 00000000..b9167998 --- /dev/null +++ b/io-sim/TAGS @@ -0,0 +1,1044 @@ + +./src/Control/Monad/IOSimPOR/Timeout.hs,381 +module Control.Monad.IOSimPOR.TimeoutControl.Monad.IOSimPOR.Timeout0,1 +newtype Timeout Timeout28,29 +instance Show Show Timeout31,32 + show show32,33 +instance Exception Exception Timeout34,35 + toException toException35,36 + fromException fromException36,37 +timeout timeout38,39 +waitFor waitFor52,53 +getGCTime getGCTime61,62 +unsafeTimeout unsafeTimeout65,66 + +./src/Control/Monad/IOSimPOR/Types.hs,702 +module Control.Monad.IOSimPOR.Types Control.Monad.IOSimPOR.Types0,1 +data Effect Effect15,16 +data Effect = Effect Effect15,16 + effectReads effectReads16,17 + effectWrites effectWrites17,18 + effectForks effectForks18,19 + effectThrows effectThrows19,20 + effectWakeup effectWakeup20,21 +instance Semigroup Semigroup Effect24,25 + Effect Effect25,26 +instance Monoid Monoid Effect28,29 + mempty mempty29,30 +readEffects readEffects34,35 +writeEffects writeEffects40,41 +forkEffect forkEffect43,44 +throwToEffect throwToEffect46,47 +wakeupEffects wakeupEffects49,50 +someTvarId someTvarId52,53 +onlyReadEffect onlyReadEffect55,56 +racingEffects racingEffects58,59 + +./src/Control/Monad/IOSimPOR/QuickCheckUtils.hs,994 +module Control.Monad.IOSimPOR.QuickCheckUtils Control.Monad.IOSimPOR.QuickCheckUtils2,3 +conjoinPar conjoinPar13,14 +conjoinNoCatch conjoinNoCatch29,30 +conjoinSpeculate conjoinSpeculate32,33 +(|(|&&|)75,76 +p p76,77 +(.(.&&|)83,84 +p p84,85 +class TestableNoCatch TestableNoCatch93,94 + propertyNoCatch propertyNoCatch94,95 +instance TestableNoCatch TestableNoCatch Discard96,97 + propertyNoCatch propertyNoCatch97,98 +instance TestableNoCatch TestableNoCatch Bool99,100 + propertyNoCatch propertyNoCatch100,101 +instance TestableNoCatch TestableNoCatch Result102,103 + propertyNoCatch propertyNoCatch103,104 +instance TestableNoCatch TestableNoCatch Prop105,106 + propertyNoCatch propertyNoCatch106,107 +instance TestableNoCatch TestableNoCatch prop => TestableNoCatch (Gen prop)108,109 + propertyNoCatch propertyNoCatch109,110 +instance TestableNoCatch TestableNoCatch Property111,112 + propertyNoCatch propertyNoCatch112,113 +againNoCatch againNoCatch114,115 + +./src/Control/Monad/IOSimPOR/Internal.hs,4347 +module Control.Monad.IOSimPOR.InternalControl.Monad.IOSimPOR.Internal24,25 +data Thread Thread95,96 +data Thread s a = Thread Thread95,96 + threadId threadId96,97 + threadControl threadControl97,98 + threadBlocked threadBlocked98,99 + threadDone threadDone99,100 + threadMasking threadMasking100,101 + threadThrowTo threadThrowTo102,103 + threadClockId threadClockId103,104 + threadLabel threadLabel104,105 + threadNextTId threadNextTId105,106 + threadStep threadStep106,107 + threadVClock threadVClock107,108 + threadEffect threadEffect108,109 + threadRacy threadRacy109,110 +threadStepId threadStepId113,114 +isRacyThreadId isRacyThreadId116,117 +isNotRacyThreadId isNotRacyThreadId120,121 +bottomVClock bottomVClock125,126 +insertVClock insertVClock128,129 +leastUpperBoundVClock leastUpperBoundVClock131,132 +happensBeforeStep happensBeforeStep138,139 +labelledTVarId labelledTVarId146,147 +labelledThreads labelledThreads149,150 +data TimerVars TimerVars162,163 +data TimerVars s = TimerVars TimerVars162,163 +type RunQueue RunQueue164,165 +data SimState SimState168,169 +data SimState s a = SimState SimState168,169 + runqueue runqueue169,170 + threads threads172,173 + curTime curTime174,175 + timers timers176,177 + clocks clocks178,179 + nextVid nextVid179,180 + nextTmid nextTmid180,181 + races races183,184 + control control185,186 + control0 control0186,187 + perStepTimeLimit perStepTimeLimit189,190 +initialState initialState193,194 +invariant invariant211,212 +timeSinceEpoch timeSinceEpoch232,233 +insertThread insertThread238,239 +schedule schedule244,245 +threadInterruptible threadInterruptible707,708 +deschedule deschedule716,717 +reschedule reschedule823,824 +unblockThreads unblockThreads905,906 +unwindControlStack unwindControlStack946,947 +removeMinimums removeMinimums979,980 +traceMany traceMany993,994 +lookupThreadLabel lookupThreadLabel999,1000 +runSimTraceST runSimTraceST1008,1009 +controlSimTraceST controlSimTraceST1011,1012 +execAtomically execAtomically1045,1046 +execAtomically execAtomically1053,1054 +execAtomically' execAtomically'1223,1224 +execNewTVar execNewTVar1248,1249 +execReadTVar execReadTVar1260,1261 +execWriteTVar execWriteTVar1264,1265 +saveTVar saveTVar1268,1269 +revertTVar revertTVar1275,1276 +commitTVar commitTVar1283,1284 +readTVarUndos readTVarUndos1290,1291 +traceTVarST traceTVarST1295,1296 +leastUpperBoundTVarVClocks leastUpperBoundTVarVClocks1312,1313 +readTVarBlockedThreads readTVarBlockedThreads1321,1322 +blockThreadOnTVar blockThreadOnTVar1324,1325 +unblockAllThreadsFromTVar unblockAllThreadsFromTVar1332,1333 +threadsUnblockedByWrites threadsUnblockedByWrites1342,1343 +ordNub ordNub1359,1360 +data Step Step1371,1372 +data Step = Step Step1371,1372 + stepThreadId stepThreadId1372,1373 + stepStep stepStep1373,1374 + stepEffect stepEffect1374,1375 + stepVClock stepVClock1375,1376 +racingSteps racingSteps1380,1381 +currentStep currentStep1393,1394 +stepThread stepThread1405,1406 +data StepInfo StepInfo1415,1416 +data StepInfo = StepInfo StepInfo1415,1416 + stepInfoStep stepInfoStep1416,1417 + stepInfoControl stepInfoControl1418,1419 + stepInfoConcurrent stepInfoConcurrent1420,1421 + stepInfoNonDep stepInfoNonDep1423,1424 + stepInfoRaces stepInfoRaces1425,1426 +data Races Races1433,1434 +data Races = Races Races1433,1434 + activeRaces activeRaces1434,1435 + completeRaces completeRaces1436,1437 +noRaces noRaces1440,1441 +updateRacesInSimState updateRacesInSimState1443,1444 +updateRaces updateRaces1464,1465 +threadTerminatesRaces threadTerminatesRaces1533,1534 +normalizeRaces normalizeRaces1539,1540 +quiescentRaces quiescentRaces1552,1553 +traceRaces traceRaces1560,1561 +controlTargets controlTargets1570,1571 +followControl followControl1576,1577 +controlFollows controlFollows1583,1584 +advanceControl advanceControl1590,1591 +stepStepId stepStepId1616,1617 +stepInfoToScheduleMods stepInfoToScheduleMods1619,1620 +traceFinalRacesFound traceFinalRacesFound1643,1644 +extendScheduleControl' extendScheduleControl'1655,1656 +extendScheduleControl extendScheduleControl1685,1686 + +./src/Control/Monad/IOSim.hs,1400 +module Control.Monad.IOSimControl.Monad.IOSim6,7 +selectTraceEvents selectTraceEvents110,111 +selectTraceEvents' selectTraceEvents'126,127 +selectTraceRaces selectTraceRaces132,133 +detachTraceRaces detachTraceRaces155,156 +selectTraceEventsDynamic selectTraceEventsDynamic173,174 +selectTraceEventsDynamic' selectTraceEventsDynamic'183,184 +selectTraceEventsSay selectTraceEventsSay194,195 +selectTraceEventsSay' selectTraceEventsSay'204,205 +printTraceEventsSay printTraceEventsSay215,216 +traceSelectTraceEvents traceSelectTraceEvents225,226 +traceSelectTraceEventsDynamic traceSelectTraceEventsDynamic242,243 +traceSelectTraceEventsSay traceSelectTraceEventsSay253,254 +data Failure Failure262,263 + FailureException FailureException264,265 + | FailureDeadlock FailureDeadlock267,268 + | FailureSloppyShutdown FailureSloppyShutdown272,273 +instance Exception Exception Failure275,276 + displayException displayException276,277 +runSim runSim290,291 +runSimOrThrow runSimOrThrow296,297 +runSimStrictShutdown runSimStrictShutdown306,307 +traceResult traceResult309,310 +traceEvents traceEvents322,323 +ppEvents ppEvents330,331 +runSimTrace runSimTrace355,356 +controlSimTrace controlSimTrace358,359 +exploreSimTrace exploreSimTrace373,374 +replaySimTrace replaySimTrace444,445 +raceReversals raceReversals455,456 +compareTraces compareTraces470,471 + +./src/Control/Monad/IOSim/CommonTypes.hs,1339 +module Control.Monad.IOSim.CommonTypes Control.Monad.IOSim.CommonTypes7,8 +data ThreadId ThreadId16,17 +data ThreadId = RacyThreadId RacyThreadId16,17 + | ThreadId ThreadId17,18 +childThreadId childThreadId20,21 +setRacyThread setRacyThread24,25 +newtype TVarId TVarId29,30 +newtype TimeoutId TimeoutId30,31 +newtype ClockId ClockId31,32 +newtype VectorClock VectorClock32,33 +newtype VectorClock = VectorClock { getVectorClock getVectorClock32,33 +unTimeoutId unTimeoutId35,36 +type ThreadLabel ThreadLabel38,39 +type TVarLabel TVarLabel39,40 +data TVar TVar41,42 +data TVar s a = TVar TVar41,42 + tvarId tvarId45,46 + tvarLabel tvarLabel48,49 + tvarCurrent tvarCurrent52,53 + tvarUndo tvarUndo57,58 + tvarBlocked tvarBlocked65,66 + tvarVClock tvarVClock69,70 + tvarTrace tvarTrace73,74 +instance Eq Eq (TVar s a)76,77 + TVar TVar77,78 +data SomeTVar SomeTVar79,80 + SomeTVar SomeTVar80,81 +data Deschedule Deschedule82,83 +data Deschedule = Yield Yield82,83 +data Deschedule = Yield | Interruptable Interruptable82,83 +data Deschedule = Yield | Interruptable | Blocked Blocked82,83 +data Deschedule = Yield | Interruptable | Blocked | Terminated Terminated82,83 +data Deschedule = Yield | Interruptable | Blocked | Terminated | SleepSleep82,83 + +./src/Control/Monad/IOSim/Types.hs,12976 +module Control.Monad.IOSim.TypesControl.Monad.IOSim.Types17,18 +newtype IOSim IOSim116,117 +newtype IOSim s a = IOSim { unIOSim unIOSim116,117 +type SimM SimM118,119 +runIOSim runIOSim121,122 +traceM traceM124,125 +traceSTM traceSTM127,128 +data SimA SimA130,131 + Return Return131,132 + Say Say133,134 + Output Output134,135 + LiftST LiftST136,137 + GetMonoTime GetMonoTime138,139 + GetWallTime GetWallTime139,140 + SetWallTime SetWallTime140,141 + UnshareClock UnshareClock141,142 + NewTimeout NewTimeout143,144 + UpdateTimeout:UpdateTimeout144,145 + CancelTimeout:CancelTimeout145,146 + Throw Throw147,148 + Catch Catch148,149 + Evaluate Evaluate150,151 + Fork Fork152,153 + GetThreadId GetThreadId153,154 + LabelThread LabelThread154,155 + Atomically Atomically156,157 + ThrowTo ThrowTo158,159 + SetMaskState SetMaskState159,160 + GetMaskState GetMaskState160,161 + YieldSim YieldSim162,163 + ExploreRaces ExploreRaces164,165 + Fix Fix166,167 +newtype STM STM169,170 +newtype STM s a = STM { unSTM unSTM169,170 +runSTM runSTM171,172 +data StmA StmA174,175 + ReturnStm ReturnStm175,176 + ThrowStm ThrowStm176,177 + CatchStm CatchStm177,178 + NewTVar NewTVar179,180 + LabelTVar LabelTVar180,181 + ReadTVar ReadTVar181,182 + WriteTVar WriteTVar182,183 + Retry Retry183,184 + OrElse OrElse184,185 + SayStm SayStm186,187 + OutputStm OutputStm187,188 + TraceTVar TraceTVar188,189 +type STMSim STMSim194,195 +type SimSTM SimSTM196,197 +instance Functor Functor (IOSim s)203,204 + fmap fmap205,206 +instance Applicative Applicative (IOSim s)207,208 + pure pure209,210 + (<(<*>)212,213 + (*(*>)216,217 +instance Monad Monad (IOSim s)218,219 + return return219,220 + (>(>>=)222,223 + (>(>>)225,226 + fail fail228,229 +instance Semigroup Semigroup a => Semigroup (IOSim s a)231,232 + (<(<>)232,233 +instance Monoid Monoid a => Monoid (IOSim s a)234,235 + mempty mempty235,236 + mappend mappend238,239 +instance Fail.MonadFail Fail-MonadFail (IOSim s)241,242 + fail fail242,243 +instance MonadFix MonadFix (IOSim s)244,245 + mfix mfix245,246 +instance Functor Functor (STM s)248,249 + fmap fmap250,251 +instance Applicative Applicative (STM s)252,253 + pure pure254,255 + (<(<*>)257,258 + (*(*>)261,262 +instance Monad Monad (STM s)263,264 + return return264,265 + (>(>>=)267,268 + (>(>>)270,271 + fail fail273,274 +instance Fail.MonadFail Fail-MonadFail (STM s)276,277 + fail fail277,278 +instance Alternative Alternative (STM s)279,280 + empty empty280,281 + (<(<|>)281,282 +instance MonadPlus MonadPlus (STM s)283,284 +instance MonadSay MonadSay (IOSim s)285,286 + say say286,287 +instance MonadThrow MonadThrow (IOSim s)288,289 + throwIO throwIO289,290 +instance MonadEvaluate MonadEvaluate (IOSim s)291,292 + evaluate evaluate292,293 +instance Exceptions.MonadThrow Exceptions-MonadThrow (IOSim s)294,295 + throwM throwM295,296 +instance MonadThrow MonadThrow (STM s)297,298 + throwIO throwIO298,299 + bracket bracket302,303 + finally finally308,309 +instance Exceptions.MonadThrow Exceptions-MonadThrow (STM s)313,314 + throwM throwM314,315 +instance MonadCatch MonadCatch (STM s)316,317 + catch catch317,318 +instance Exceptions.MonadCatch Exceptions-MonadCatch (STM s)320,321 + catch catch321,322 +instance MonadCatch MonadCatch (IOSim s)323,324 + catch catch324,325 +instance Exceptions.MonadCatch Exceptions-MonadCatch (IOSim s)327,328 + catch catch328,329 +instance MonadMask MonadMask (IOSim s)330,331 + mask mask331,332 + uninterruptibleMask uninterruptibleMask338,339 +instance MonadMaskingState MonadMaskingState (IOSim s)345,346 + getMaskingState getMaskingState346,347 +instance Exceptions.MonadMask Exceptions-MonadMask (IOSim s)348,349 + mask mask349,350 + uninterruptibleMask uninterruptibleMask350,351 + generalBracket generalBracket352,353 +getMaskingStateImpl getMaskingStateImpl362,363 +unblock, block, blockUninterruptible blockUninterruptible363,364 +unblock, block,block363,364 +unblock,unblock363,364 +getMaskingStateImpl getMaskingStateImpl365,366 +unblock unblock366,367 +block block367,368 +blockUninterruptible blockUninterruptible368,369 +instance MonadThread MonadThread (IOSim s)370,371 + type ThreadId ThreadId371,372 + myThreadId myThreadId372,373 + labelThread labelThread373,374 +instance MonadFork MonadFork (IOSim s)375,376 + forkIO forkIO376,377 + forkIOWithUnmask forkIOWithUnmask377,378 + throwTo throwTo378,379 + yield yield379,380 +instance MonadTest MonadTest (IOSim s)381,382 + exploreRaces exploreRaces382,383 +instance MonadSay MonadSay (STMSim s)384,385 + say say385,386 +instance MonadLabelledSTM MonadLabelledSTM (IOSim s)388,389 + labelTVar labelTVar389,390 + labelTMVar labelTMVar390,391 + labelTQueue labelTQueue391,392 + labelTBQueue labelTBQueue392,393 +instance MonadSTM MonadSTM (IOSim s)394,395 + type STM STM395,396 + type TVar TVar396,397 + type TMVar TMVar397,398 + type TQueue TQueue398,399 + type TBQueue TBQueue399,400 + atomically atomically401,402 + newTVar newTVar403,404 + readTVar readTVar404,405 + writeTVar writeTVar405,406 + retry retry406,407 + orElse orElse407,408 + newTMVar newTMVar409,410 + newEmptyTMVar newEmptyTMVar410,411 + takeTMVar takeTMVar411,412 + tryTakeTMVar tryTakeTMVar412,413 + putTMVar putTMVar413,414 + tryPutTMVar tryPutTMVar414,415 + readTMVar readTMVar415,416 + tryReadTMVar tryReadTMVar416,417 + swapTMVar swapTMVar417,418 + isEmptyTMVar isEmptyTMVar418,419 + newTQueue newTQueue420,421 + readTQueue readTQueue421,422 + tryReadTQueue tryReadTQueue422,423 + peekTQueue peekTQueue423,424 + tryPeekTQueue tryPeekTQueue424,425 + writeTQueue writeTQueue425,426 + isEmptyTQueue isEmptyTQueue426,427 + newTBQueue newTBQueue428,429 + readTBQueue readTBQueue429,430 + tryReadTBQueue tryReadTBQueue430,431 + peekTBQueue peekTBQueue431,432 + tryPeekTBQueue tryPeekTBQueue432,433 + flushTBQueue flushTBQueue433,434 + writeTBQueue writeTBQueue434,435 + lengthTBQueue lengthTBQueue435,436 + isEmptyTBQueue isEmptyTBQueue436,437 + isFullTBQueue isFullTBQueue437,438 + newTMVarIO newTMVarIO439,440 + newEmptyTMVarIO newEmptyTMVarIO440,441 +instance MonadInspectSTM MonadInspectSTM (IOSim s)442,443 + type InspectMonad InspectMonad443,444 + inspectTVar inspectTVar444,445 + inspectTMVar inspectTMVar445,446 +instance MonadTraceSTM MonadTraceSTM (IOSim s)453,454 + traceTVar traceTVar454,455 + traceTQueue traceTQueue455,456 + traceTBQueue traceTBQueue456,457 +data Async Async458,459 +data Async s a = Async Async458,459 +instance Eq Eq (Async s a)460,461 + Async Async461,462 +instance Ord Ord (Async s a)463,464 + compare compare464,465 +instance Functor Functor (Async s)466,467 + fmap fmap467,468 +instance MonadAsync MonadAsync (IOSim s)469,470 + type Async Async470,471 + async async472,473 + asyncThreadId asyncThreadId480,481 + waitCatchSTM waitCatchSTM482,483 + pollSTM pollSTM483,484 + cancel cancel485,486 + cancelWith cancelWith486,487 + asyncWithUnmask asyncWithUnmask488,489 +instance MonadST MonadST (IOSim s)490,491 + withLiftST withLiftST491,492 +liftST liftST493,494 +instance MonadMonotonicTime MonadMonotonicTime (IOSim s)496,497 + getMonotonicTime getMonotonicTime497,498 +instance MonadTime MonadTime (IOSim s)499,500 + getCurrentTime getCurrentTime500,501 +setCurrentTime setCurrentTime504,505 +unshareClock unshareClock512,513 +instance MonadDelay MonadDelay (IOSim s)515,516 +instance MonadTimer MonadTimer (IOSim s)518,519 + data Timeout Timeout519,520 + data Timeout (IOSim s) = Timeout Timeout519,520 + | NegativeTimeout NegativeTimeout522,523 + readTimeout readTimeout525,526 + newTimeout newTimeout528,529 + updateTimeout updateTimeout529,530 + cancelTimeout cancelTimeout530,531 + timeout timeout532,533 + registerDelay registerDelay553,554 +newtype TimeoutException TimeoutException555,556 +instance Show Show TimeoutException557,558 + show show558,559 +instance Exception Exception TimeoutException560,561 + toException toException561,562 + fromException fromException562,563 +newtype EventlogEvent EventlogEvent566,567 +newtype EventlogMarker EventlogMarker570,571 +instance MonadEventlog MonadEventlog (IOSim s)572,573 + traceEventIO traceEventIO573,574 + traceMarkerIO traceMarkerIO574,575 +data SimEventSimEvent589,590 + = SimEvent SimEvent590,591 + seTime seTime591,592 + seThreadId seThreadId592,593 + seThreadLabel seThreadLabel593,594 + seType seType594,595 + | SimPOREvent SimPOREvent596,597 + seTime seTime597,598 + seThreadId seThreadId598,599 + seStep seStep599,600 + seThreadLabel seThreadLabel600,601 + seType seType601,602 + | SimRacesFound SimRacesFound603,604 +ppSimEvent ppSimEvent608,609 +data SimResult SimResult638,639 + = MainReturn MainReturn639,640 + | MainException MainException640,641 + | Deadlock Deadlock641,642 + | LoopLoop642,643 +type SimTrace SimTrace646,647 +ppTrace ppTrace650,651 +ppTrace_ ppTrace_678,679 +ppDebug ppDebug706,707 +pattern Trace Trace711,712 +pattern Trace time time713,714 +pattern SimTrace SimTrace719,720 +pattern SimTrace time time721,722 +pattern SimPORTrace SimPORTrace725,726 +pattern SimPORTrace time time727,728 +pattern TraceRacesFound TraceRacesFound731,732 +pattern TraceRacesFound controls controls733,734 +pattern TraceMainReturn TraceMainReturn737,738 +pattern TraceMainReturn time time739,740 +pattern TraceMainException TraceMainException741,742 +pattern TraceMainException time time743,744 +pattern TraceDeadlock TraceDeadlock745,746 +pattern TraceDeadlock time time747,748 +pattern TraceLoop TraceLoop749,750 +data SimEventTypeSimEventType756,757 + = EventSimStart EventSimStart757,758 + | EventSay EventSay758,759 + | EventLog EventLog759,760 + | EventMask EventMask760,761 + | EventThrow EventThrow762,763 + | EventThrowTo EventThrowTo763,764 + | EventThrowToBlocked EventThrowToBlocked764,765 + | EventThrowToWakeup EventThrowToWakeup765,766 + | EventThrowToUnmasked EventThrowToUnmasked766,767 + | EventThreadForked EventThreadForked768,769 + | EventThreadFinished EventThreadFinished769,770 + | EventThreadUnhandled EventThreadUnhandled770,771 + | EventTxCommitted EventTxCommitted772,773 + | EventTxAborted EventTxAborted775,776 + | EventTxBlocked EventTxBlocked776,777 + | EventTxWakeup EventTxWakeup778,779 + | EventTimerCreated EventTimerCreated780,781 + | EventTimerUpdated EventTimerUpdated781,782 + | EventTimerCancelled EventTimerCancelled782,783 + | EventTimerExpired EventTimerExpired783,784 + | EventThreadSleep EventThreadSleep787,788 + | EventThreadWake EventThreadWake789,790 + | EventDeschedule EventDeschedule790,791 + | EventFollowControl EventFollowControl791,792 + | EventAwaitControl EventAwaitControl792,793 + | EventPerformAction EventPerformAction793,794 + | EventReschedule EventReschedule794,795 + | EventUnblocked EventUnblocked795,796 +type TraceEvent TraceEvent798,799 +data Labelled Labelled801,802 +data Labelled a = Labelled Labelled801,802 + l_labelled l_labelled802,803 + l_label l_label803,804 +data StmTxResult StmTxResult812,813 + StmTxCommitted StmTxCommitted825,826 + | StmTxBlocked StmTxBlocked835,836 + | StmTxAborted StmTxAborted840,841 +data StmStack StmStack842,843 + AtomicallyFrame AtomicallyFrame844,845 + OrElseLeftFrame OrElseLeftFrame847,848 + OrElseRightFrame OrElseRightFrame856,857 +data ScheduleControl ScheduleControl867,868 +data ScheduleControl = ControlDefaultControlDefault867,868 + | ControlAwait ControlAwait869,870 + | ControlFollow ControlFollow875,876 +data ScheduleMod ScheduleMod881,882 +data ScheduleMod = ScheduleMod{ScheduleMod{881,882 + scheduleModTarget scheduleModTarget883,884 + scheduleModControl scheduleModControl887,888 + scheduleModInsertion scheduleModInsertion890,891 +type StepId StepId894,895 +instance Show Show ScheduleMod896,897 + showsPrec showsPrec897,898 +data ExplorationOptions ExplorationOptions910,911 +data ExplorationOptions = ExplorationOptions{ExplorationOptions{910,911 + explorationScheduleBound explorationScheduleBound911,912 + explorationBranching explorationBranching912,913 + explorationStepTimelimit explorationStepTimelimit913,914 + explorationReplay explorationReplay914,915 +stdExplorationOptions stdExplorationOptions918,919 +type ExplorationSpec ExplorationSpec926,927 +withScheduleBound withScheduleBound928,929 +withBranching withBranching931,932 +withStepTimelimit withStepTimelimit934,935 +withReplay withReplay937,938 + +./src/Control/Monad/IOSim/STM.hs,1245 +module Control.Monad.IOSim.STM Control.Monad.IOSim.STM7,8 +newtype TQueueDefault TQueueDefault19,20 +newtype TQueueDefault m a = TQueue TQueue19,20 +labelTQueueDefault labelTQueueDefault24,25 +traceTQueueDefault traceTQueueDefault32,33 +newTQueueDefault newTQueueDefault38,39 +writeTQueueDefault writeTQueueDefault41,42 +readTQueueDefault readTQueueDefault46,47 +tryReadTQueueDefault tryReadTQueueDefault49,50 +isEmptyTQueueDefault isEmptyTQueueDefault63,64 +peekTQueueDefault peekTQueueDefault72,73 +tryPeekTQueueDefault tryPeekTQueueDefault79,80 +data TBQueueDefault TBQueueDefault90,91 +data TBQueueDefault m a = TBQueueTBQueue90,91 +labelTBQueueDefault labelTBQueueDefault97,98 +traceTBQueueDefault traceTBQueueDefault105,106 +newTBQueueDefault newTBQueueDefault111,112 +readTBQueueDefault readTBQueueDefault117,118 +tryReadTBQueueDefault tryReadTBQueueDefault120,121 +peekTBQueueDefault peekTBQueueDefault140,141 +tryPeekTBQueueDefault tryPeekTBQueueDefault143,144 +writeTBQueueDefault writeTBQueueDefault150,151 +isEmptyTBQueueDefault isEmptyTBQueueDefault162,163 +isFullTBQueueDefault isFullTBQueueDefault169,170 +lengthTBQueueDefault lengthTBQueueDefault179,180 +flushTBQueueDefault flushTBQueueDefault184,185 + +./src/Control/Monad/IOSim/InternalTypes.hs,621 +module Control.Monad.IOSim.InternalTypesControl.Monad.IOSim.InternalTypes5,6 +data ThreadControl ThreadControl18,19 + ThreadControl ThreadControl19,20 +instance Show Show (ThreadControl s a)23,24 + show show24,25 +data ControlStack ControlStack26,27 + MainFrame MainFrame27,28 + ForkFrame ForkFrame28,29 + MaskFrame MaskFrame29,30 + CatchFrame CatchFrame33,34 +instance Show Show (ControlStack s b a)39,40 + show show40,41 +data ControlStackDash ControlStackDash47,48 + MainFrame'MainFrame'48,49 + | ForkFrame'ForkFrame'49,50 + | MaskFrame' MaskFrame'50,51 + | CatchFrame' CatchFrame'51,52 + +./src/Control/Monad/IOSim/Internal.hs,2038 +module Control.Monad.IOSim.InternalControl.Monad.IOSim.Internal22,23 +data Thread Thread94,95 +data Thread s a = Thread Thread94,95 + threadId threadId95,96 + threadControl threadControl96,97 + threadBlocked threadBlocked97,98 + threadMasking threadMasking98,99 + threadThrowTo threadThrowTo100,101 + threadClockId threadClockId101,102 + threadLabel threadLabel102,103 + threadNextTId threadNextTId103,104 +labelledTVarId labelledTVarId106,107 +labelledThreads labelledThreads109,110 +data TimerVars TimerVars122,123 +data TimerVars s = TimerVars TimerVars122,123 +data SimState SimState127,128 +data SimState s a = SimState SimState127,128 + runqueue runqueue128,129 + threads threads131,132 + curTime curTime133,134 + timers timers135,136 + clocks clocks137,138 + nextVid nextVid138,139 + nextTmid nextTmid139,140 +initialState initialState142,143 +invariant invariant156,157 +timeSinceEpoch timeSinceEpoch175,176 +schedule schedule181,182 +threadInterruptible threadInterruptible582,583 +deschedule deschedule591,592 +reschedule reschedule675,676 +unblockThreads unblockThreads724,725 +unwindControlStack unwindControlStack752,753 +removeMinimums removeMinimums785,786 +traceMany traceMany799,800 +lookupThreadLabel lookupThreadLabel805,806 +runSimTraceST runSimTraceST814,815 +execAtomically execAtomically834,835 +execAtomically execAtomically842,843 +execAtomically' execAtomically'1005,1006 +execNewTVar execNewTVar1030,1031 +execReadTVar execReadTVar1042,1043 +execWriteTVar execWriteTVar1046,1047 +saveTVar saveTVar1050,1051 +revertTVar revertTVar1058,1059 +commitTVar commitTVar1067,1068 +readTVarUndos readTVarUndos1075,1076 +traceTVarST traceTVarST1080,1081 +readTVarBlockedThreads readTVarBlockedThreads1102,1103 +blockThreadOnTVar blockThreadOnTVar1105,1106 +unblockAllThreadsFromTVar unblockAllThreadsFromTVar1114,1115 +threadsUnblockedByWrites threadsUnblockedByWrites1125,1126 +ordNub ordNub1142,1143 + +./src/Data/List/Trace.hs,1572 +module Data.List.TraceData.List.Trace2,3 +data Trace Trace30,31 + = Cons Cons31,32 + | Nil Nil32,33 +head head35,36 +tail tail39,40 +filter filter43,44 +length length50,51 +toList toList54,55 +fromList fromList57,58 +ppTrace ppTrace62,63 +instance Bifunctor Bifunctor Trace66,67 + bimap bimap67,68 +instance Bifoldable Bifoldable Trace70,71 + bifoldMap bifoldMap71,72 + bifoldr bifoldr74,75 + bifoldl bifoldl80,81 +instance Bitraversable Bitraversable Trace86,87 + bitraverse bitraverse87,88 +instance Semigroup Semigroup a => Semigroup (Trace a b)90,91 + Cons Cons91,92 + o@Nil o@Nil92,93 + Nil Nil93,94 +instance Monoid Monoid a => Monoid (Trace a b)95,96 + mempty mempty96,97 +instance Monoid Monoid a => Applicative (Trace a)98,99 + pure pure99,100 + Cons Cons100,101 + Nil Nil101,102 +instance Monoid Monoid a => Monad (Trace a)103,104 + return return104,105 + o o106,107 +instance Monoid Monoid a => MonadFail (Trace a)108,109 + fail fail109,110 +instance Monoid Monoid a => Alternative (Trace a)111,112 + empty empty112,113 + (<(<|>)113,114 +instance Monoid Monoid a => MonadPlus (Trace a)115,116 + mzero mzero116,117 + mplus mplus117,118 +instance Monoid Monoid a => MonadFix (Trace a)119,120 + mfix mfix120,121 +instance Eq Eq a => Eq1 (Trace a)124,125 + liftEq liftEq125,126 +instance Ord Ord a => Ord1 (Trace a)130,131 + liftCompare liftCompare131,132 +instance Show Show a => Show1 (Trace a)136,137 + liftShowsPrec liftShowsPrec137,138 + +./bench/Main.hs,312 +module Main Main3,4 +prop_channel prop_channel32,33 +prop_threadDelay prop_threadDelay57,58 +prop_registerDelay prop_registerDelay60,61 +prop_timeout_fail prop_timeout_fail63,64 +prop_timeout_succeed prop_timeout_succeed66,67 +prop_threads prop_threads74,75 +prop_async prop_async83,84 +main main91,92 + +./test/Main.hs,55 +module Main Main0,1 +main main6,7 +tests tests9,10 + +./test/Test/Control/Monad/IOSimPOR.hs,1477 +module Test.Control.Monad.IOSimPOR Test.Control.Monad.IOSimPOR8,9 +data Step Step30,31 + WhenSet WhenSet31,32 + | ThrowTo ThrowTo32,33 + | Delay Delay33,34 + | Timeout Timeout34,35 +data TimeoutStep TimeoutStep37,38 + NewTimeout NewTimeout38,39 + | UpdateTimeout UpdateTimeout39,40 + | CancelTimeoutCancelTimeout40,41 + | AwaitTimeoutAwaitTimeout41,42 +instance Arbitrary Arbitrary Step44,45 + arbitrary arbitrary45,46 + shrink shrink54,55 +instance Arbitrary Arbitrary TimeoutStep60,61 + arbitrary arbitrary61,62 + shrink shrink68,69 +newtype Task Task71,72 +instance Arbitrary Arbitrary Task74,75 + arbitrary arbitrary75,76 + shrink shrink78,79 +normalize normalize82,83 +compressSteps compressSteps90,91 +newtype Tasks Tasks96,97 +instance Arbitrary Arbitrary Tasks99,100 + arbitrary arbitrary100,101 + shrink shrink101,102 +fixThrowTos fixThrowTos108,109 +shrinkDelays shrinkDelays111,112 +removeTask removeTask126,127 +advanceThrowTo advanceThrowTo134,135 +mapThrowTos mapThrowTos144,145 +sortTasks sortTasks150,151 +interpret interpret155,156 +runTasks runTasks179,180 +maxTaskValue maxTaskValue191,192 +propSimulates propSimulates196,197 +propExploration propExploration202,203 +propPermutations propPermutations217,218 +doit doit226,227 +ordered ordered234,235 +noExceptions noExceptions237,238 +splitTrace splitTrace243,244 +traceCounter traceCounter249,250 +traceNoDuplicates traceNoDuplicates259,260 + +./test/Test/IOSim.hs,4560 +module Test.IOSimTest.IOSim5,6 +tests tests42,43 +prop_stm_graph_io prop_stm_graph_io153,154 +prop_stm_graph_sim prop_stm_graph_sim158,159 +prop_stm_graph prop_stm_graph167,168 +newtype TestThreadGraph TestThreadGraph198,199 +instance Arbitrary Arbitrary TestThreadGraph201,202 + arbitrary arbitrary202,203 +arbitraryAcyclicGraph arbitraryAcyclicGraph209,210 +newtype TestMicro TestMicro235,236 +instance Arbitrary Arbitrary TestMicro241,242 + arbitrary arbitrary242,243 + shrink shrink259,260 +test_timers test_timers261,262 +prop_timers_ST prop_timers_ST309,310 +prop_timers_IO prop_timers_IO314,315 +test_fork_order test_fork_order325,326 +prop_fork_order_ST prop_fork_order_ST350,351 +prop_fork_order_IO prop_fork_order_IO353,354 +test_threadId_order test_threadId_order357,358 +prop_threadId_order_order_Sim prop_threadId_order_order_Sim380,381 +prop_wakeup_order_ST prop_wakeup_order_ST384,385 +test_wakeup_order test_wakeup_order394,395 +prop_mfix_purity prop_mfix_purity422,423 +prop_mfix_purity_2 prop_mfix_purity_2432,433 +prop_mfix_left_shrinking prop_mfix_left_shrinking469,470 +prop_mfix_lazy prop_mfix_lazy491,492 +prop_mfix_recdata prop_mfix_recdata540,541 +type Probe Probe573,574 +withProbe withProbe575,576 +probeOutput probeOutput581,582 +unit_catch_0 unit_catch_0595,596 +unit_catch_1 unit_catch_1609,610 +unit_catch_2 unit_catch_2619,620 +unit_catch_3 unit_catch_3632,633 +unit_catch_4 unit_catch_4644,645 +unit_catch_5 unit_catch_5657,658 +unit_catch_6 unit_catch_6670,671 +unit_evaluate_0 unit_evaluate_0685,686 +unit_fork_1 unit_fork_1693,694 +unit_fork_2 unit_fork_2706,707 +unit_async_1 unit_async_1738,739 +unit_async_2 unit_async_2751,752 +unit_async_3 unit_async_3762,763 +unit_async_4 unit_async_4773,774 +unit_async_5 unit_async_5784,785 +unit_async_6 unit_async_6799,800 +unit_async_7 unit_async_7819,820 +unit_async_8 unit_async_8839,840 +unit_async_9 unit_async_9859,860 +unit_async_10 unit_async_10875,876 +unit_async_11 unit_async_11903,904 +unit_async_12 unit_async_12935,936 +unit_async_13 unit_async_13956,957 +unit_async_14 unit_async_14965,966 +unit_async_15 unit_async_15986,987 +unit_async_16 unit_async_161006,1007 +prop_stm_referenceIO prop_stm_referenceIO1033,1034 +prop_stm_referenceSim prop_stm_referenceSim1040,1041 +prop_stm_referenceM prop_stm_referenceM1051,1052 +prop_timeout_no_deadlockM prop_timeout_no_deadlockM1062,1063 +prop_timeout_no_deadlock_Sim prop_timeout_no_deadlock_Sim1084,1085 +prop_timeout_no_deadlock_IO prop_timeout_no_deadlock_IO1087,1088 +setMaskingState_ setMaskingState_1095,1096 +setMaskingState setMaskingState1100,1101 +maxMS maxMS1106,1107 +forall_masking_states forall_masking_states1114,1115 +prop_set_masking_state prop_set_masking_state1125,1126 +unit_set_masking_state_IO unit_set_masking_state_IO1133,1134 +unit_set_masking_state_ST unit_set_masking_state_ST1137,1138 +prop_unmask prop_unmask1144,1145 +unit_unmask_IO unit_unmask_IO1154,1155 +unit_unmask_ST unit_unmask_ST1157,1158 +prop_fork_masking_state prop_fork_masking_state1163,1164 +unit_fork_masking_state_IO unit_fork_masking_state_IO1174,1175 +unit_fork_masking_state_ST unit_fork_masking_state_ST1178,1179 +prop_fork_unmask prop_fork_unmask1188,1189 +unit_fork_unmask_IO unit_fork_unmask_IO1204,1205 +unit_fork_unmask_ST unit_fork_unmask_ST1207,1208 +prop_catch_throwIO_masking_state prop_catch_throwIO_masking_state1214,1215 +unit_catch_throwIO_masking_state_IO unit_catch_throwIO_masking_state_IO1223,1224 +unit_catch_throwIO_masking_state_ST unit_catch_throwIO_masking_state_ST1227,1228 +prop_catch_throwTo_masking_state prop_catch_throwTo_masking_state1234,1235 +unit_catch_throwTo_masking_state_IO unit_catch_throwTo_masking_state_IO1247,1248 +unit_catch_throwTo_masking_state_ST unit_catch_throwTo_masking_state_ST1251,1252 +prop_catch_throwTo_masking_state_async prop_catch_throwTo_masking_state_async1259,1260 +unit_catch_throwTo_masking_state_async_IO unit_catch_throwTo_masking_state_async_IO1285,1286 +unit_catch_throwTo_masking_state_async_ST unit_catch_throwTo_masking_state_async_ST1289,1290 +prop_catch_throwTo_masking_state_async_mayblock prop_catch_throwTo_masking_state_async_mayblock1298,1299 +unit_catch_throwTo_masking_state_async_mayblock_IO unit_catch_throwTo_masking_state_async_mayblock_IO1329,1330 +unit_catch_throwTo_masking_state_async_mayblock_ST unit_catch_throwTo_masking_state_async_mayblock_ST1333,1334 +runSimTraceSay runSimTraceSay1341,1342 +selectTraceSay selectTraceSay1344,1345 + +./test/Test/STM.hs,4426 +module Test.STM Test.STM22,23 +data Type Type41,42 + TyUnit TyUnit42,43 + TyInt TyInt43,44 + TyVar TyVar44,45 + TyUnit TyUnit42,43 + TyInt TyInt43,44 + TyVar TyVar44,45 +data TyRep TyRep49,50 +data TyRep (t t49,50 + TyRepUnit TyRepUnit50,51 + TyRepInt TyRepInt51,52 + TyRepVar TyRepVar52,53 +data TyRep (t t49,50 +data Term Term65,66 +data Term (t t65,66 + Return Return67,68 + Throw Throw68,69 + Retry Retry69,70 + ReadTVar ReadTVar71,72 + WriteTVar WriteTVar72,73 + NewTVar NewTVar73,74 + Bind Bind76,77 + OrElse OrElse77,78 +data Term (t t65,66 +data Expr Expr84,85 +data Expr (t t84,85 + ExprUnit ExprUnit86,87 + ExprInt ExprInt87,88 + ExprName ExprName88,89 +data Expr (t t84,85 +data Value Value95,96 +data Value (t t95,96 + ValUnit ValUnit97,98 + ValInt ValInt98,99 + ValVar ValVar99,100 +data Value (t t95,96 +data Name Name114,115 +data Name (t :: Type) = Name Name114,115 +newtype NameId NameId117,118 +data Var Var125,126 +data Var (t :: Type) = Var Var125,126 +newtype VarId VarId128,129 +eqTyRep eqTyRep137,138 +nameTyRep nameTyRep145,146 +varTyRep varTyRep148,149 +tyRepExpr tyRepExpr151,152 +tyRepValue tyRepValue156,157 +data SomeName SomeName166,167 + SomeName SomeName167,168 +data SomeValue SomeValue169,170 + SomeValue SomeValue170,171 +newtype Env Env178,179 +lookupEnv lookupEnv183,184 +extendEnv extendEnv190,191 +data SomeVar SomeVar199,200 + SomeVar SomeVar200,201 +newtype Heap Heap204,205 +type Allocs Allocs208,209 +readVar readVar211,212 +writeVar writeVar218,219 +extendHeap extendHeap227,228 +data TxResult TxResult249,250 + TxComitted TxComitted250,251 + | TxBlockedTxBlocked251,252 + | TxAborted TxAborted252,253 +data ImmValue ImmValue261,262 + ImmValUnit ImmValUnit263,264 + ImmValInt ImmValInt264,265 + ImmValVar ImmValVar265,266 + ImmValUnit ImmValUnit263,264 +instance Exception Exception ImmValue271,272 +evalExpr evalExpr279,280 +data NfTerm NfTerm286,287 +data NfTerm (t t286,287 + NfReturn NfReturn288,289 + NfThrow NfThrow289,290 + NfRetry NfRetry290,291 +data NfTerm (t t286,287 +evalTerm evalTerm300,301 +evalAtomically evalAtomically361,362 +snapshotValue snapshotValue388,389 +data ExecValue ExecValue398,399 +data ExecValue m (t t398,399 + ExecValUnit ExecValUnit400,401 + ExecValInt ExecValInt401,402 + ExecValVar ExecValVar402,403 +instance Show Show (ExecValue m t)405,406 + show show406,407 +data SomeExecValue SomeExecValue411,412 + SomeExecValue SomeExecValue412,413 +newtype ExecEnv ExecEnv417,418 +tyRepExecValue tyRepExecValue420,421 +lookupExecEnv lookupExecEnv425,426 +extendExecEnv extendExecEnv432,433 +execTerm execTerm439,440 +execExpr execExpr482,483 +snapshotExecValue snapshotExecValue487,488 +execAtomically execAtomically493,494 +instance Arbitrary Arbitrary SomeTerm513,514 + arbitrary arbitrary514,515 + shrink shrink516,517 +data SomeTerm SomeTerm519,520 + SomeTerm SomeTerm520,521 +data SomeExpr SomeExpr522,523 + SomeExpr SomeExpr523,524 +data GenEnv GenEnv532,533 +data GenEnv = GenEnv GenEnv532,533 + envNames envNames534,535 + envNextName envNextName537,538 +data TyTrie TyTrie540,541 + TyTrieEmptyTyTrieEmpty541,542 + | TyTrieNode TyTrieNode542,543 + trieUnit trieUnit543,544 + trieInt trieInt544,545 + trieVar trieVar545,546 +lookupTyTrie lookupTyTrie549,550 +insertTyTrie insertTyTrie555,556 +emptyGenEnv emptyGenEnv568,569 +lookupNames lookupNames571,572 +freshName freshName577,578 +pickName pickName587,588 +data SomeVarName SomeVarName591,592 + SomeVarName SomeVarName592,593 +lookupVarNames lookupVarNames595,596 +deep deep607,608 +genSomeTerm genSomeTerm614,615 +genTerm genTerm630,631 +genSomeExpr genSomeExpr677,678 +genExpr genExpr686,687 +elements' elements'701,702 +oneof' oneof'704,705 +frequency' frequency'707,708 +shrinkTerm shrinkTerm710,711 +shrinkExpr shrinkExpr730,731 +freeNamesTerm freeNamesTerm737,738 +freeNamesExpr freeNamesExpr748,749 +nameId nameId753,754 +prop_genSomeTerm prop_genSomeTerm756,757 +termSize termSize767,768 +termDepth termDepth777,778 +showTerm showTerm787,788 +showExpr showExpr808,809 +showName showName813,814 +showNameTyped showNameTyped816,817 +showTyRep showTyRep821,822 diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index c015185b..d6ad7fef 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -911,15 +911,16 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = go ctl' read written' writtenSeq' createdSeq' nextVid (k x) CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - undefined + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid undefined ThrowStm e -> {-# SCC "execAtomically.go.ThrowStm" #-} do - case (fromException e, ctl) of - (Just e', CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl') | isException exc -> do + case ctl of + CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do -- Use handler to rescue the exception - go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (handler e') - (_, _) -> do + -- go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (handler e') + undefined + _ -> do -- Revert all the TVar writes !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written k0 $ StmTxAborted [] (toException e) diff --git a/io-sim/test/Test/IOSim.hs b/io-sim/test/Test/IOSim.hs index 53b817ac..576f0446 100644 --- a/io-sim/test/Test/IOSim.hs +++ b/io-sim/test/Test/IOSim.hs @@ -1049,7 +1049,7 @@ prop_stm_referenceSim t = -- | Compare the behaviour of the STM reference operational semantics with -- the behaviour of any 'MonadSTM' STM implementation. -- -prop_stm_referenceM :: (MonadSTM m, MonadThrow (STM m), MonadCatch m) +prop_stm_referenceM :: (MonadSTM m, MonadThrow (STM m), MonadCatch m, LazySTM.MonadSTM m, MonadCatch (LazySTM.STM m)) => SomeTerm -> m Property prop_stm_referenceM (SomeTerm _tyrep t) = do let (r1, _heap) = evalAtomically t diff --git a/io-sim/test/Test/STM.hs b/io-sim/test/Test/STM.hs index 27b5d5a5..1df40207 100644 --- a/io-sim/test/Test/STM.hs +++ b/io-sim/test/Test/STM.hs @@ -67,6 +67,7 @@ data Term (t :: Type) where Return :: Expr t -> Term t Throw :: Expr a -> Term t + Catch :: Term t -> Term t -> Term t Retry :: Term t ReadTVar :: Name (TyVar t) -> Term t @@ -309,6 +310,30 @@ evalTerm !env !heap !allocs term = case term of where e' = evalExpr env e + -- Exception semantics are detailed in "Appendix A Exception semantics" p 12-13 of + -- + Catch t1 t2 -> + let (nf1, heap', allocs') = evalTerm env heap mempty t1 in case nf1 of + + -- Rule XSTM1 + -- M; heap, {} => return P; heap', allocs' + -- -------------------------------------------------------- + -- S[catch M N]; heap, allocs => S[N P]; heap, allocs + NfReturn v -> (NfReturn v, heap', allocs `mappend` allocs') + + -- Rule XSTM2 + -- M; heap, {} => throw P; heap', allocs' + -- -------------------------------------------------------- + -- S[catch M N]; heap, allocs => S[N P]; heap, allocs + NfThrow _ -> evalTerm env (heap `mappend` allocs') (allocs `mappend` allocs') t2 + + -- Rule XSTM3 + -- M; heap, {} => retry; heap', allocs' + -- -------------------------------------------------------- + -- S[catch M N]; heap, allocs => S[retry]; heap, allocs + NfRetry -> (NfRetry, heap, allocs) + + Retry -> (NfRetry, heap, allocs) -- Rule READ @@ -437,7 +462,7 @@ extendExecEnv (Name name _tyrep) v (ExecEnv env) = -- | Execute an STM 'Term' in the 'STM' monad. -- -execTerm :: (MonadSTM m, MonadThrow (STM m)) +execTerm :: (MonadSTM m, MonadThrow (STM m), MonadCatch (STM m)) => ExecEnv m -> Term t -> STM m (ExecValue m t) @@ -451,6 +476,8 @@ execTerm env t = let e' = execExpr env e throwSTM =<< snapshotExecValue e' + Catch t1 t2 -> execTerm env t1 `catch` \(_ :: ImmValue) -> execTerm env t2 + Retry -> retry ReadTVar n -> do @@ -491,7 +518,7 @@ snapshotExecValue (ExecValInt x) = return (ImmValInt x) snapshotExecValue (ExecValVar v _) = fmap ImmValVar (snapshotExecValue =<< readTVar v) -execAtomically :: forall m t. (MonadSTM m, MonadThrow (STM m), MonadCatch m) +execAtomically :: forall m t. (MonadSTM m, MonadThrow (STM m), MonadCatch m, MonadCatch (STM m)) => Term t -> m TxResult execAtomically t = toTxResult <$> try (atomically action') @@ -713,6 +740,9 @@ shrinkTerm t = case t of Return e -> [Return e' | e' <- shrinkExpr e] Throw e -> [Throw e' | e' <- shrinkExpr e] + Catch t1 t2 -> [t1, t2] + ++ [Catch t1' t2 | t1' <- shrinkTerm t1 ] + ++ [Catch t1 t2' | t2' <- shrinkTerm t2 ] Retry -> [] ReadTVar _ -> [] @@ -738,6 +768,7 @@ shrinkExpr (ExprName (Name _ (TyRepVar _))) = [] freeNamesTerm :: Term t -> Set NameId freeNamesTerm (Return e) = freeNamesExpr e freeNamesTerm (Throw e) = freeNamesExpr e +freeNamesTerm (Catch t1 t2) = freeNamesTerm t1 <> freeNamesTerm t2 freeNamesTerm Retry = Set.empty freeNamesTerm (ReadTVar n) = Set.singleton (nameId n) freeNamesTerm (WriteTVar n e) = Set.singleton (nameId n) <> freeNamesExpr e @@ -768,6 +799,7 @@ prop_genSomeTerm (SomeTerm tyrep term) = termSize :: Term a -> Int termSize Return{} = 1 termSize Throw{} = 1 +termSize (Catch a b) = 1 + termSize a + termSize b termSize Retry{} = 1 termSize ReadTVar{} = 1 termSize WriteTVar{} = 1 @@ -778,6 +810,7 @@ termSize (OrElse a b) = 1 + termSize a + termSize b termDepth :: Term a -> Int termDepth Return{} = 1 termDepth Throw{} = 1 +termDepth (Catch a b) = 1 + max (termDepth a) (termDepth b) termDepth Retry{} = 1 termDepth ReadTVar{} = 1 termDepth WriteTVar{} = 1 @@ -790,6 +823,9 @@ showTerm p (Return e) = showParen (p > 10) $ showString "return " . showExpr 11 e showTerm p (Throw e) = showParen (p > 10) $ showString "throwSTM " . showExpr 11 e +showTerm p (Catch t1 t2) = showParen (p > 9) $ + showTerm 10 t1 . showString " `catch` " + . showTerm 10 t2 showTerm _ Retry = showString "retry" showTerm p (ReadTVar n) = showParen (p > 10) $ showString "readTVar " . showName n From 7fdec2fe633bd7524ccfb70c89f0ba179d11d702 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Tue, 12 Jul 2022 13:46:40 +0530 Subject: [PATCH 03/11] CAD-4738 Remove extra files --- io-sim/TAGS | 1044 --------------------------------------------------- 1 file changed, 1044 deletions(-) delete mode 100644 io-sim/TAGS diff --git a/io-sim/TAGS b/io-sim/TAGS deleted file mode 100644 index b9167998..00000000 --- a/io-sim/TAGS +++ /dev/null @@ -1,1044 +0,0 @@ - -./src/Control/Monad/IOSimPOR/Timeout.hs,381 -module Control.Monad.IOSimPOR.TimeoutControl.Monad.IOSimPOR.Timeout0,1 -newtype Timeout Timeout28,29 -instance Show Show Timeout31,32 - show show32,33 -instance Exception Exception Timeout34,35 - toException toException35,36 - fromException fromException36,37 -timeout timeout38,39 -waitFor waitFor52,53 -getGCTime getGCTime61,62 -unsafeTimeout unsafeTimeout65,66 - -./src/Control/Monad/IOSimPOR/Types.hs,702 -module Control.Monad.IOSimPOR.Types Control.Monad.IOSimPOR.Types0,1 -data Effect Effect15,16 -data Effect = Effect Effect15,16 - effectReads effectReads16,17 - effectWrites effectWrites17,18 - effectForks effectForks18,19 - effectThrows effectThrows19,20 - effectWakeup effectWakeup20,21 -instance Semigroup Semigroup Effect24,25 - Effect Effect25,26 -instance Monoid Monoid Effect28,29 - mempty mempty29,30 -readEffects readEffects34,35 -writeEffects writeEffects40,41 -forkEffect forkEffect43,44 -throwToEffect throwToEffect46,47 -wakeupEffects wakeupEffects49,50 -someTvarId someTvarId52,53 -onlyReadEffect onlyReadEffect55,56 -racingEffects racingEffects58,59 - -./src/Control/Monad/IOSimPOR/QuickCheckUtils.hs,994 -module Control.Monad.IOSimPOR.QuickCheckUtils Control.Monad.IOSimPOR.QuickCheckUtils2,3 -conjoinPar conjoinPar13,14 -conjoinNoCatch conjoinNoCatch29,30 -conjoinSpeculate conjoinSpeculate32,33 -(|(|&&|)75,76 -p p76,77 -(.(.&&|)83,84 -p p84,85 -class TestableNoCatch TestableNoCatch93,94 - propertyNoCatch propertyNoCatch94,95 -instance TestableNoCatch TestableNoCatch Discard96,97 - propertyNoCatch propertyNoCatch97,98 -instance TestableNoCatch TestableNoCatch Bool99,100 - propertyNoCatch propertyNoCatch100,101 -instance TestableNoCatch TestableNoCatch Result102,103 - propertyNoCatch propertyNoCatch103,104 -instance TestableNoCatch TestableNoCatch Prop105,106 - propertyNoCatch propertyNoCatch106,107 -instance TestableNoCatch TestableNoCatch prop => TestableNoCatch (Gen prop)108,109 - propertyNoCatch propertyNoCatch109,110 -instance TestableNoCatch TestableNoCatch Property111,112 - propertyNoCatch propertyNoCatch112,113 -againNoCatch againNoCatch114,115 - -./src/Control/Monad/IOSimPOR/Internal.hs,4347 -module Control.Monad.IOSimPOR.InternalControl.Monad.IOSimPOR.Internal24,25 -data Thread Thread95,96 -data Thread s a = Thread Thread95,96 - threadId threadId96,97 - threadControl threadControl97,98 - threadBlocked threadBlocked98,99 - threadDone threadDone99,100 - threadMasking threadMasking100,101 - threadThrowTo threadThrowTo102,103 - threadClockId threadClockId103,104 - threadLabel threadLabel104,105 - threadNextTId threadNextTId105,106 - threadStep threadStep106,107 - threadVClock threadVClock107,108 - threadEffect threadEffect108,109 - threadRacy threadRacy109,110 -threadStepId threadStepId113,114 -isRacyThreadId isRacyThreadId116,117 -isNotRacyThreadId isNotRacyThreadId120,121 -bottomVClock bottomVClock125,126 -insertVClock insertVClock128,129 -leastUpperBoundVClock leastUpperBoundVClock131,132 -happensBeforeStep happensBeforeStep138,139 -labelledTVarId labelledTVarId146,147 -labelledThreads labelledThreads149,150 -data TimerVars TimerVars162,163 -data TimerVars s = TimerVars TimerVars162,163 -type RunQueue RunQueue164,165 -data SimState SimState168,169 -data SimState s a = SimState SimState168,169 - runqueue runqueue169,170 - threads threads172,173 - curTime curTime174,175 - timers timers176,177 - clocks clocks178,179 - nextVid nextVid179,180 - nextTmid nextTmid180,181 - races races183,184 - control control185,186 - control0 control0186,187 - perStepTimeLimit perStepTimeLimit189,190 -initialState initialState193,194 -invariant invariant211,212 -timeSinceEpoch timeSinceEpoch232,233 -insertThread insertThread238,239 -schedule schedule244,245 -threadInterruptible threadInterruptible707,708 -deschedule deschedule716,717 -reschedule reschedule823,824 -unblockThreads unblockThreads905,906 -unwindControlStack unwindControlStack946,947 -removeMinimums removeMinimums979,980 -traceMany traceMany993,994 -lookupThreadLabel lookupThreadLabel999,1000 -runSimTraceST runSimTraceST1008,1009 -controlSimTraceST controlSimTraceST1011,1012 -execAtomically execAtomically1045,1046 -execAtomically execAtomically1053,1054 -execAtomically' execAtomically'1223,1224 -execNewTVar execNewTVar1248,1249 -execReadTVar execReadTVar1260,1261 -execWriteTVar execWriteTVar1264,1265 -saveTVar saveTVar1268,1269 -revertTVar revertTVar1275,1276 -commitTVar commitTVar1283,1284 -readTVarUndos readTVarUndos1290,1291 -traceTVarST traceTVarST1295,1296 -leastUpperBoundTVarVClocks leastUpperBoundTVarVClocks1312,1313 -readTVarBlockedThreads readTVarBlockedThreads1321,1322 -blockThreadOnTVar blockThreadOnTVar1324,1325 -unblockAllThreadsFromTVar unblockAllThreadsFromTVar1332,1333 -threadsUnblockedByWrites threadsUnblockedByWrites1342,1343 -ordNub ordNub1359,1360 -data Step Step1371,1372 -data Step = Step Step1371,1372 - stepThreadId stepThreadId1372,1373 - stepStep stepStep1373,1374 - stepEffect stepEffect1374,1375 - stepVClock stepVClock1375,1376 -racingSteps racingSteps1380,1381 -currentStep currentStep1393,1394 -stepThread stepThread1405,1406 -data StepInfo StepInfo1415,1416 -data StepInfo = StepInfo StepInfo1415,1416 - stepInfoStep stepInfoStep1416,1417 - stepInfoControl stepInfoControl1418,1419 - stepInfoConcurrent stepInfoConcurrent1420,1421 - stepInfoNonDep stepInfoNonDep1423,1424 - stepInfoRaces stepInfoRaces1425,1426 -data Races Races1433,1434 -data Races = Races Races1433,1434 - activeRaces activeRaces1434,1435 - completeRaces completeRaces1436,1437 -noRaces noRaces1440,1441 -updateRacesInSimState updateRacesInSimState1443,1444 -updateRaces updateRaces1464,1465 -threadTerminatesRaces threadTerminatesRaces1533,1534 -normalizeRaces normalizeRaces1539,1540 -quiescentRaces quiescentRaces1552,1553 -traceRaces traceRaces1560,1561 -controlTargets controlTargets1570,1571 -followControl followControl1576,1577 -controlFollows controlFollows1583,1584 -advanceControl advanceControl1590,1591 -stepStepId stepStepId1616,1617 -stepInfoToScheduleMods stepInfoToScheduleMods1619,1620 -traceFinalRacesFound traceFinalRacesFound1643,1644 -extendScheduleControl' extendScheduleControl'1655,1656 -extendScheduleControl extendScheduleControl1685,1686 - -./src/Control/Monad/IOSim.hs,1400 -module Control.Monad.IOSimControl.Monad.IOSim6,7 -selectTraceEvents selectTraceEvents110,111 -selectTraceEvents' selectTraceEvents'126,127 -selectTraceRaces selectTraceRaces132,133 -detachTraceRaces detachTraceRaces155,156 -selectTraceEventsDynamic selectTraceEventsDynamic173,174 -selectTraceEventsDynamic' selectTraceEventsDynamic'183,184 -selectTraceEventsSay selectTraceEventsSay194,195 -selectTraceEventsSay' selectTraceEventsSay'204,205 -printTraceEventsSay printTraceEventsSay215,216 -traceSelectTraceEvents traceSelectTraceEvents225,226 -traceSelectTraceEventsDynamic traceSelectTraceEventsDynamic242,243 -traceSelectTraceEventsSay traceSelectTraceEventsSay253,254 -data Failure Failure262,263 - FailureException FailureException264,265 - | FailureDeadlock FailureDeadlock267,268 - | FailureSloppyShutdown FailureSloppyShutdown272,273 -instance Exception Exception Failure275,276 - displayException displayException276,277 -runSim runSim290,291 -runSimOrThrow runSimOrThrow296,297 -runSimStrictShutdown runSimStrictShutdown306,307 -traceResult traceResult309,310 -traceEvents traceEvents322,323 -ppEvents ppEvents330,331 -runSimTrace runSimTrace355,356 -controlSimTrace controlSimTrace358,359 -exploreSimTrace exploreSimTrace373,374 -replaySimTrace replaySimTrace444,445 -raceReversals raceReversals455,456 -compareTraces compareTraces470,471 - -./src/Control/Monad/IOSim/CommonTypes.hs,1339 -module Control.Monad.IOSim.CommonTypes Control.Monad.IOSim.CommonTypes7,8 -data ThreadId ThreadId16,17 -data ThreadId = RacyThreadId RacyThreadId16,17 - | ThreadId ThreadId17,18 -childThreadId childThreadId20,21 -setRacyThread setRacyThread24,25 -newtype TVarId TVarId29,30 -newtype TimeoutId TimeoutId30,31 -newtype ClockId ClockId31,32 -newtype VectorClock VectorClock32,33 -newtype VectorClock = VectorClock { getVectorClock getVectorClock32,33 -unTimeoutId unTimeoutId35,36 -type ThreadLabel ThreadLabel38,39 -type TVarLabel TVarLabel39,40 -data TVar TVar41,42 -data TVar s a = TVar TVar41,42 - tvarId tvarId45,46 - tvarLabel tvarLabel48,49 - tvarCurrent tvarCurrent52,53 - tvarUndo tvarUndo57,58 - tvarBlocked tvarBlocked65,66 - tvarVClock tvarVClock69,70 - tvarTrace tvarTrace73,74 -instance Eq Eq (TVar s a)76,77 - TVar TVar77,78 -data SomeTVar SomeTVar79,80 - SomeTVar SomeTVar80,81 -data Deschedule Deschedule82,83 -data Deschedule = Yield Yield82,83 -data Deschedule = Yield | Interruptable Interruptable82,83 -data Deschedule = Yield | Interruptable | Blocked Blocked82,83 -data Deschedule = Yield | Interruptable | Blocked | Terminated Terminated82,83 -data Deschedule = Yield | Interruptable | Blocked | Terminated | SleepSleep82,83 - -./src/Control/Monad/IOSim/Types.hs,12976 -module Control.Monad.IOSim.TypesControl.Monad.IOSim.Types17,18 -newtype IOSim IOSim116,117 -newtype IOSim s a = IOSim { unIOSim unIOSim116,117 -type SimM SimM118,119 -runIOSim runIOSim121,122 -traceM traceM124,125 -traceSTM traceSTM127,128 -data SimA SimA130,131 - Return Return131,132 - Say Say133,134 - Output Output134,135 - LiftST LiftST136,137 - GetMonoTime GetMonoTime138,139 - GetWallTime GetWallTime139,140 - SetWallTime SetWallTime140,141 - UnshareClock UnshareClock141,142 - NewTimeout NewTimeout143,144 - UpdateTimeout:UpdateTimeout144,145 - CancelTimeout:CancelTimeout145,146 - Throw Throw147,148 - Catch Catch148,149 - Evaluate Evaluate150,151 - Fork Fork152,153 - GetThreadId GetThreadId153,154 - LabelThread LabelThread154,155 - Atomically Atomically156,157 - ThrowTo ThrowTo158,159 - SetMaskState SetMaskState159,160 - GetMaskState GetMaskState160,161 - YieldSim YieldSim162,163 - ExploreRaces ExploreRaces164,165 - Fix Fix166,167 -newtype STM STM169,170 -newtype STM s a = STM { unSTM unSTM169,170 -runSTM runSTM171,172 -data StmA StmA174,175 - ReturnStm ReturnStm175,176 - ThrowStm ThrowStm176,177 - CatchStm CatchStm177,178 - NewTVar NewTVar179,180 - LabelTVar LabelTVar180,181 - ReadTVar ReadTVar181,182 - WriteTVar WriteTVar182,183 - Retry Retry183,184 - OrElse OrElse184,185 - SayStm SayStm186,187 - OutputStm OutputStm187,188 - TraceTVar TraceTVar188,189 -type STMSim STMSim194,195 -type SimSTM SimSTM196,197 -instance Functor Functor (IOSim s)203,204 - fmap fmap205,206 -instance Applicative Applicative (IOSim s)207,208 - pure pure209,210 - (<(<*>)212,213 - (*(*>)216,217 -instance Monad Monad (IOSim s)218,219 - return return219,220 - (>(>>=)222,223 - (>(>>)225,226 - fail fail228,229 -instance Semigroup Semigroup a => Semigroup (IOSim s a)231,232 - (<(<>)232,233 -instance Monoid Monoid a => Monoid (IOSim s a)234,235 - mempty mempty235,236 - mappend mappend238,239 -instance Fail.MonadFail Fail-MonadFail (IOSim s)241,242 - fail fail242,243 -instance MonadFix MonadFix (IOSim s)244,245 - mfix mfix245,246 -instance Functor Functor (STM s)248,249 - fmap fmap250,251 -instance Applicative Applicative (STM s)252,253 - pure pure254,255 - (<(<*>)257,258 - (*(*>)261,262 -instance Monad Monad (STM s)263,264 - return return264,265 - (>(>>=)267,268 - (>(>>)270,271 - fail fail273,274 -instance Fail.MonadFail Fail-MonadFail (STM s)276,277 - fail fail277,278 -instance Alternative Alternative (STM s)279,280 - empty empty280,281 - (<(<|>)281,282 -instance MonadPlus MonadPlus (STM s)283,284 -instance MonadSay MonadSay (IOSim s)285,286 - say say286,287 -instance MonadThrow MonadThrow (IOSim s)288,289 - throwIO throwIO289,290 -instance MonadEvaluate MonadEvaluate (IOSim s)291,292 - evaluate evaluate292,293 -instance Exceptions.MonadThrow Exceptions-MonadThrow (IOSim s)294,295 - throwM throwM295,296 -instance MonadThrow MonadThrow (STM s)297,298 - throwIO throwIO298,299 - bracket bracket302,303 - finally finally308,309 -instance Exceptions.MonadThrow Exceptions-MonadThrow (STM s)313,314 - throwM throwM314,315 -instance MonadCatch MonadCatch (STM s)316,317 - catch catch317,318 -instance Exceptions.MonadCatch Exceptions-MonadCatch (STM s)320,321 - catch catch321,322 -instance MonadCatch MonadCatch (IOSim s)323,324 - catch catch324,325 -instance Exceptions.MonadCatch Exceptions-MonadCatch (IOSim s)327,328 - catch catch328,329 -instance MonadMask MonadMask (IOSim s)330,331 - mask mask331,332 - uninterruptibleMask uninterruptibleMask338,339 -instance MonadMaskingState MonadMaskingState (IOSim s)345,346 - getMaskingState getMaskingState346,347 -instance Exceptions.MonadMask Exceptions-MonadMask (IOSim s)348,349 - mask mask349,350 - uninterruptibleMask uninterruptibleMask350,351 - generalBracket generalBracket352,353 -getMaskingStateImpl getMaskingStateImpl362,363 -unblock, block, blockUninterruptible blockUninterruptible363,364 -unblock, block,block363,364 -unblock,unblock363,364 -getMaskingStateImpl getMaskingStateImpl365,366 -unblock unblock366,367 -block block367,368 -blockUninterruptible blockUninterruptible368,369 -instance MonadThread MonadThread (IOSim s)370,371 - type ThreadId ThreadId371,372 - myThreadId myThreadId372,373 - labelThread labelThread373,374 -instance MonadFork MonadFork (IOSim s)375,376 - forkIO forkIO376,377 - forkIOWithUnmask forkIOWithUnmask377,378 - throwTo throwTo378,379 - yield yield379,380 -instance MonadTest MonadTest (IOSim s)381,382 - exploreRaces exploreRaces382,383 -instance MonadSay MonadSay (STMSim s)384,385 - say say385,386 -instance MonadLabelledSTM MonadLabelledSTM (IOSim s)388,389 - labelTVar labelTVar389,390 - labelTMVar labelTMVar390,391 - labelTQueue labelTQueue391,392 - labelTBQueue labelTBQueue392,393 -instance MonadSTM MonadSTM (IOSim s)394,395 - type STM STM395,396 - type TVar TVar396,397 - type TMVar TMVar397,398 - type TQueue TQueue398,399 - type TBQueue TBQueue399,400 - atomically atomically401,402 - newTVar newTVar403,404 - readTVar readTVar404,405 - writeTVar writeTVar405,406 - retry retry406,407 - orElse orElse407,408 - newTMVar newTMVar409,410 - newEmptyTMVar newEmptyTMVar410,411 - takeTMVar takeTMVar411,412 - tryTakeTMVar tryTakeTMVar412,413 - putTMVar putTMVar413,414 - tryPutTMVar tryPutTMVar414,415 - readTMVar readTMVar415,416 - tryReadTMVar tryReadTMVar416,417 - swapTMVar swapTMVar417,418 - isEmptyTMVar isEmptyTMVar418,419 - newTQueue newTQueue420,421 - readTQueue readTQueue421,422 - tryReadTQueue tryReadTQueue422,423 - peekTQueue peekTQueue423,424 - tryPeekTQueue tryPeekTQueue424,425 - writeTQueue writeTQueue425,426 - isEmptyTQueue isEmptyTQueue426,427 - newTBQueue newTBQueue428,429 - readTBQueue readTBQueue429,430 - tryReadTBQueue tryReadTBQueue430,431 - peekTBQueue peekTBQueue431,432 - tryPeekTBQueue tryPeekTBQueue432,433 - flushTBQueue flushTBQueue433,434 - writeTBQueue writeTBQueue434,435 - lengthTBQueue lengthTBQueue435,436 - isEmptyTBQueue isEmptyTBQueue436,437 - isFullTBQueue isFullTBQueue437,438 - newTMVarIO newTMVarIO439,440 - newEmptyTMVarIO newEmptyTMVarIO440,441 -instance MonadInspectSTM MonadInspectSTM (IOSim s)442,443 - type InspectMonad InspectMonad443,444 - inspectTVar inspectTVar444,445 - inspectTMVar inspectTMVar445,446 -instance MonadTraceSTM MonadTraceSTM (IOSim s)453,454 - traceTVar traceTVar454,455 - traceTQueue traceTQueue455,456 - traceTBQueue traceTBQueue456,457 -data Async Async458,459 -data Async s a = Async Async458,459 -instance Eq Eq (Async s a)460,461 - Async Async461,462 -instance Ord Ord (Async s a)463,464 - compare compare464,465 -instance Functor Functor (Async s)466,467 - fmap fmap467,468 -instance MonadAsync MonadAsync (IOSim s)469,470 - type Async Async470,471 - async async472,473 - asyncThreadId asyncThreadId480,481 - waitCatchSTM waitCatchSTM482,483 - pollSTM pollSTM483,484 - cancel cancel485,486 - cancelWith cancelWith486,487 - asyncWithUnmask asyncWithUnmask488,489 -instance MonadST MonadST (IOSim s)490,491 - withLiftST withLiftST491,492 -liftST liftST493,494 -instance MonadMonotonicTime MonadMonotonicTime (IOSim s)496,497 - getMonotonicTime getMonotonicTime497,498 -instance MonadTime MonadTime (IOSim s)499,500 - getCurrentTime getCurrentTime500,501 -setCurrentTime setCurrentTime504,505 -unshareClock unshareClock512,513 -instance MonadDelay MonadDelay (IOSim s)515,516 -instance MonadTimer MonadTimer (IOSim s)518,519 - data Timeout Timeout519,520 - data Timeout (IOSim s) = Timeout Timeout519,520 - | NegativeTimeout NegativeTimeout522,523 - readTimeout readTimeout525,526 - newTimeout newTimeout528,529 - updateTimeout updateTimeout529,530 - cancelTimeout cancelTimeout530,531 - timeout timeout532,533 - registerDelay registerDelay553,554 -newtype TimeoutException TimeoutException555,556 -instance Show Show TimeoutException557,558 - show show558,559 -instance Exception Exception TimeoutException560,561 - toException toException561,562 - fromException fromException562,563 -newtype EventlogEvent EventlogEvent566,567 -newtype EventlogMarker EventlogMarker570,571 -instance MonadEventlog MonadEventlog (IOSim s)572,573 - traceEventIO traceEventIO573,574 - traceMarkerIO traceMarkerIO574,575 -data SimEventSimEvent589,590 - = SimEvent SimEvent590,591 - seTime seTime591,592 - seThreadId seThreadId592,593 - seThreadLabel seThreadLabel593,594 - seType seType594,595 - | SimPOREvent SimPOREvent596,597 - seTime seTime597,598 - seThreadId seThreadId598,599 - seStep seStep599,600 - seThreadLabel seThreadLabel600,601 - seType seType601,602 - | SimRacesFound SimRacesFound603,604 -ppSimEvent ppSimEvent608,609 -data SimResult SimResult638,639 - = MainReturn MainReturn639,640 - | MainException MainException640,641 - | Deadlock Deadlock641,642 - | LoopLoop642,643 -type SimTrace SimTrace646,647 -ppTrace ppTrace650,651 -ppTrace_ ppTrace_678,679 -ppDebug ppDebug706,707 -pattern Trace Trace711,712 -pattern Trace time time713,714 -pattern SimTrace SimTrace719,720 -pattern SimTrace time time721,722 -pattern SimPORTrace SimPORTrace725,726 -pattern SimPORTrace time time727,728 -pattern TraceRacesFound TraceRacesFound731,732 -pattern TraceRacesFound controls controls733,734 -pattern TraceMainReturn TraceMainReturn737,738 -pattern TraceMainReturn time time739,740 -pattern TraceMainException TraceMainException741,742 -pattern TraceMainException time time743,744 -pattern TraceDeadlock TraceDeadlock745,746 -pattern TraceDeadlock time time747,748 -pattern TraceLoop TraceLoop749,750 -data SimEventTypeSimEventType756,757 - = EventSimStart EventSimStart757,758 - | EventSay EventSay758,759 - | EventLog EventLog759,760 - | EventMask EventMask760,761 - | EventThrow EventThrow762,763 - | EventThrowTo EventThrowTo763,764 - | EventThrowToBlocked EventThrowToBlocked764,765 - | EventThrowToWakeup EventThrowToWakeup765,766 - | EventThrowToUnmasked EventThrowToUnmasked766,767 - | EventThreadForked EventThreadForked768,769 - | EventThreadFinished EventThreadFinished769,770 - | EventThreadUnhandled EventThreadUnhandled770,771 - | EventTxCommitted EventTxCommitted772,773 - | EventTxAborted EventTxAborted775,776 - | EventTxBlocked EventTxBlocked776,777 - | EventTxWakeup EventTxWakeup778,779 - | EventTimerCreated EventTimerCreated780,781 - | EventTimerUpdated EventTimerUpdated781,782 - | EventTimerCancelled EventTimerCancelled782,783 - | EventTimerExpired EventTimerExpired783,784 - | EventThreadSleep EventThreadSleep787,788 - | EventThreadWake EventThreadWake789,790 - | EventDeschedule EventDeschedule790,791 - | EventFollowControl EventFollowControl791,792 - | EventAwaitControl EventAwaitControl792,793 - | EventPerformAction EventPerformAction793,794 - | EventReschedule EventReschedule794,795 - | EventUnblocked EventUnblocked795,796 -type TraceEvent TraceEvent798,799 -data Labelled Labelled801,802 -data Labelled a = Labelled Labelled801,802 - l_labelled l_labelled802,803 - l_label l_label803,804 -data StmTxResult StmTxResult812,813 - StmTxCommitted StmTxCommitted825,826 - | StmTxBlocked StmTxBlocked835,836 - | StmTxAborted StmTxAborted840,841 -data StmStack StmStack842,843 - AtomicallyFrame AtomicallyFrame844,845 - OrElseLeftFrame OrElseLeftFrame847,848 - OrElseRightFrame OrElseRightFrame856,857 -data ScheduleControl ScheduleControl867,868 -data ScheduleControl = ControlDefaultControlDefault867,868 - | ControlAwait ControlAwait869,870 - | ControlFollow ControlFollow875,876 -data ScheduleMod ScheduleMod881,882 -data ScheduleMod = ScheduleMod{ScheduleMod{881,882 - scheduleModTarget scheduleModTarget883,884 - scheduleModControl scheduleModControl887,888 - scheduleModInsertion scheduleModInsertion890,891 -type StepId StepId894,895 -instance Show Show ScheduleMod896,897 - showsPrec showsPrec897,898 -data ExplorationOptions ExplorationOptions910,911 -data ExplorationOptions = ExplorationOptions{ExplorationOptions{910,911 - explorationScheduleBound explorationScheduleBound911,912 - explorationBranching explorationBranching912,913 - explorationStepTimelimit explorationStepTimelimit913,914 - explorationReplay explorationReplay914,915 -stdExplorationOptions stdExplorationOptions918,919 -type ExplorationSpec ExplorationSpec926,927 -withScheduleBound withScheduleBound928,929 -withBranching withBranching931,932 -withStepTimelimit withStepTimelimit934,935 -withReplay withReplay937,938 - -./src/Control/Monad/IOSim/STM.hs,1245 -module Control.Monad.IOSim.STM Control.Monad.IOSim.STM7,8 -newtype TQueueDefault TQueueDefault19,20 -newtype TQueueDefault m a = TQueue TQueue19,20 -labelTQueueDefault labelTQueueDefault24,25 -traceTQueueDefault traceTQueueDefault32,33 -newTQueueDefault newTQueueDefault38,39 -writeTQueueDefault writeTQueueDefault41,42 -readTQueueDefault readTQueueDefault46,47 -tryReadTQueueDefault tryReadTQueueDefault49,50 -isEmptyTQueueDefault isEmptyTQueueDefault63,64 -peekTQueueDefault peekTQueueDefault72,73 -tryPeekTQueueDefault tryPeekTQueueDefault79,80 -data TBQueueDefault TBQueueDefault90,91 -data TBQueueDefault m a = TBQueueTBQueue90,91 -labelTBQueueDefault labelTBQueueDefault97,98 -traceTBQueueDefault traceTBQueueDefault105,106 -newTBQueueDefault newTBQueueDefault111,112 -readTBQueueDefault readTBQueueDefault117,118 -tryReadTBQueueDefault tryReadTBQueueDefault120,121 -peekTBQueueDefault peekTBQueueDefault140,141 -tryPeekTBQueueDefault tryPeekTBQueueDefault143,144 -writeTBQueueDefault writeTBQueueDefault150,151 -isEmptyTBQueueDefault isEmptyTBQueueDefault162,163 -isFullTBQueueDefault isFullTBQueueDefault169,170 -lengthTBQueueDefault lengthTBQueueDefault179,180 -flushTBQueueDefault flushTBQueueDefault184,185 - -./src/Control/Monad/IOSim/InternalTypes.hs,621 -module Control.Monad.IOSim.InternalTypesControl.Monad.IOSim.InternalTypes5,6 -data ThreadControl ThreadControl18,19 - ThreadControl ThreadControl19,20 -instance Show Show (ThreadControl s a)23,24 - show show24,25 -data ControlStack ControlStack26,27 - MainFrame MainFrame27,28 - ForkFrame ForkFrame28,29 - MaskFrame MaskFrame29,30 - CatchFrame CatchFrame33,34 -instance Show Show (ControlStack s b a)39,40 - show show40,41 -data ControlStackDash ControlStackDash47,48 - MainFrame'MainFrame'48,49 - | ForkFrame'ForkFrame'49,50 - | MaskFrame' MaskFrame'50,51 - | CatchFrame' CatchFrame'51,52 - -./src/Control/Monad/IOSim/Internal.hs,2038 -module Control.Monad.IOSim.InternalControl.Monad.IOSim.Internal22,23 -data Thread Thread94,95 -data Thread s a = Thread Thread94,95 - threadId threadId95,96 - threadControl threadControl96,97 - threadBlocked threadBlocked97,98 - threadMasking threadMasking98,99 - threadThrowTo threadThrowTo100,101 - threadClockId threadClockId101,102 - threadLabel threadLabel102,103 - threadNextTId threadNextTId103,104 -labelledTVarId labelledTVarId106,107 -labelledThreads labelledThreads109,110 -data TimerVars TimerVars122,123 -data TimerVars s = TimerVars TimerVars122,123 -data SimState SimState127,128 -data SimState s a = SimState SimState127,128 - runqueue runqueue128,129 - threads threads131,132 - curTime curTime133,134 - timers timers135,136 - clocks clocks137,138 - nextVid nextVid138,139 - nextTmid nextTmid139,140 -initialState initialState142,143 -invariant invariant156,157 -timeSinceEpoch timeSinceEpoch175,176 -schedule schedule181,182 -threadInterruptible threadInterruptible582,583 -deschedule deschedule591,592 -reschedule reschedule675,676 -unblockThreads unblockThreads724,725 -unwindControlStack unwindControlStack752,753 -removeMinimums removeMinimums785,786 -traceMany traceMany799,800 -lookupThreadLabel lookupThreadLabel805,806 -runSimTraceST runSimTraceST814,815 -execAtomically execAtomically834,835 -execAtomically execAtomically842,843 -execAtomically' execAtomically'1005,1006 -execNewTVar execNewTVar1030,1031 -execReadTVar execReadTVar1042,1043 -execWriteTVar execWriteTVar1046,1047 -saveTVar saveTVar1050,1051 -revertTVar revertTVar1058,1059 -commitTVar commitTVar1067,1068 -readTVarUndos readTVarUndos1075,1076 -traceTVarST traceTVarST1080,1081 -readTVarBlockedThreads readTVarBlockedThreads1102,1103 -blockThreadOnTVar blockThreadOnTVar1105,1106 -unblockAllThreadsFromTVar unblockAllThreadsFromTVar1114,1115 -threadsUnblockedByWrites threadsUnblockedByWrites1125,1126 -ordNub ordNub1142,1143 - -./src/Data/List/Trace.hs,1572 -module Data.List.TraceData.List.Trace2,3 -data Trace Trace30,31 - = Cons Cons31,32 - | Nil Nil32,33 -head head35,36 -tail tail39,40 -filter filter43,44 -length length50,51 -toList toList54,55 -fromList fromList57,58 -ppTrace ppTrace62,63 -instance Bifunctor Bifunctor Trace66,67 - bimap bimap67,68 -instance Bifoldable Bifoldable Trace70,71 - bifoldMap bifoldMap71,72 - bifoldr bifoldr74,75 - bifoldl bifoldl80,81 -instance Bitraversable Bitraversable Trace86,87 - bitraverse bitraverse87,88 -instance Semigroup Semigroup a => Semigroup (Trace a b)90,91 - Cons Cons91,92 - o@Nil o@Nil92,93 - Nil Nil93,94 -instance Monoid Monoid a => Monoid (Trace a b)95,96 - mempty mempty96,97 -instance Monoid Monoid a => Applicative (Trace a)98,99 - pure pure99,100 - Cons Cons100,101 - Nil Nil101,102 -instance Monoid Monoid a => Monad (Trace a)103,104 - return return104,105 - o o106,107 -instance Monoid Monoid a => MonadFail (Trace a)108,109 - fail fail109,110 -instance Monoid Monoid a => Alternative (Trace a)111,112 - empty empty112,113 - (<(<|>)113,114 -instance Monoid Monoid a => MonadPlus (Trace a)115,116 - mzero mzero116,117 - mplus mplus117,118 -instance Monoid Monoid a => MonadFix (Trace a)119,120 - mfix mfix120,121 -instance Eq Eq a => Eq1 (Trace a)124,125 - liftEq liftEq125,126 -instance Ord Ord a => Ord1 (Trace a)130,131 - liftCompare liftCompare131,132 -instance Show Show a => Show1 (Trace a)136,137 - liftShowsPrec liftShowsPrec137,138 - -./bench/Main.hs,312 -module Main Main3,4 -prop_channel prop_channel32,33 -prop_threadDelay prop_threadDelay57,58 -prop_registerDelay prop_registerDelay60,61 -prop_timeout_fail prop_timeout_fail63,64 -prop_timeout_succeed prop_timeout_succeed66,67 -prop_threads prop_threads74,75 -prop_async prop_async83,84 -main main91,92 - -./test/Main.hs,55 -module Main Main0,1 -main main6,7 -tests tests9,10 - -./test/Test/Control/Monad/IOSimPOR.hs,1477 -module Test.Control.Monad.IOSimPOR Test.Control.Monad.IOSimPOR8,9 -data Step Step30,31 - WhenSet WhenSet31,32 - | ThrowTo ThrowTo32,33 - | Delay Delay33,34 - | Timeout Timeout34,35 -data TimeoutStep TimeoutStep37,38 - NewTimeout NewTimeout38,39 - | UpdateTimeout UpdateTimeout39,40 - | CancelTimeoutCancelTimeout40,41 - | AwaitTimeoutAwaitTimeout41,42 -instance Arbitrary Arbitrary Step44,45 - arbitrary arbitrary45,46 - shrink shrink54,55 -instance Arbitrary Arbitrary TimeoutStep60,61 - arbitrary arbitrary61,62 - shrink shrink68,69 -newtype Task Task71,72 -instance Arbitrary Arbitrary Task74,75 - arbitrary arbitrary75,76 - shrink shrink78,79 -normalize normalize82,83 -compressSteps compressSteps90,91 -newtype Tasks Tasks96,97 -instance Arbitrary Arbitrary Tasks99,100 - arbitrary arbitrary100,101 - shrink shrink101,102 -fixThrowTos fixThrowTos108,109 -shrinkDelays shrinkDelays111,112 -removeTask removeTask126,127 -advanceThrowTo advanceThrowTo134,135 -mapThrowTos mapThrowTos144,145 -sortTasks sortTasks150,151 -interpret interpret155,156 -runTasks runTasks179,180 -maxTaskValue maxTaskValue191,192 -propSimulates propSimulates196,197 -propExploration propExploration202,203 -propPermutations propPermutations217,218 -doit doit226,227 -ordered ordered234,235 -noExceptions noExceptions237,238 -splitTrace splitTrace243,244 -traceCounter traceCounter249,250 -traceNoDuplicates traceNoDuplicates259,260 - -./test/Test/IOSim.hs,4560 -module Test.IOSimTest.IOSim5,6 -tests tests42,43 -prop_stm_graph_io prop_stm_graph_io153,154 -prop_stm_graph_sim prop_stm_graph_sim158,159 -prop_stm_graph prop_stm_graph167,168 -newtype TestThreadGraph TestThreadGraph198,199 -instance Arbitrary Arbitrary TestThreadGraph201,202 - arbitrary arbitrary202,203 -arbitraryAcyclicGraph arbitraryAcyclicGraph209,210 -newtype TestMicro TestMicro235,236 -instance Arbitrary Arbitrary TestMicro241,242 - arbitrary arbitrary242,243 - shrink shrink259,260 -test_timers test_timers261,262 -prop_timers_ST prop_timers_ST309,310 -prop_timers_IO prop_timers_IO314,315 -test_fork_order test_fork_order325,326 -prop_fork_order_ST prop_fork_order_ST350,351 -prop_fork_order_IO prop_fork_order_IO353,354 -test_threadId_order test_threadId_order357,358 -prop_threadId_order_order_Sim prop_threadId_order_order_Sim380,381 -prop_wakeup_order_ST prop_wakeup_order_ST384,385 -test_wakeup_order test_wakeup_order394,395 -prop_mfix_purity prop_mfix_purity422,423 -prop_mfix_purity_2 prop_mfix_purity_2432,433 -prop_mfix_left_shrinking prop_mfix_left_shrinking469,470 -prop_mfix_lazy prop_mfix_lazy491,492 -prop_mfix_recdata prop_mfix_recdata540,541 -type Probe Probe573,574 -withProbe withProbe575,576 -probeOutput probeOutput581,582 -unit_catch_0 unit_catch_0595,596 -unit_catch_1 unit_catch_1609,610 -unit_catch_2 unit_catch_2619,620 -unit_catch_3 unit_catch_3632,633 -unit_catch_4 unit_catch_4644,645 -unit_catch_5 unit_catch_5657,658 -unit_catch_6 unit_catch_6670,671 -unit_evaluate_0 unit_evaluate_0685,686 -unit_fork_1 unit_fork_1693,694 -unit_fork_2 unit_fork_2706,707 -unit_async_1 unit_async_1738,739 -unit_async_2 unit_async_2751,752 -unit_async_3 unit_async_3762,763 -unit_async_4 unit_async_4773,774 -unit_async_5 unit_async_5784,785 -unit_async_6 unit_async_6799,800 -unit_async_7 unit_async_7819,820 -unit_async_8 unit_async_8839,840 -unit_async_9 unit_async_9859,860 -unit_async_10 unit_async_10875,876 -unit_async_11 unit_async_11903,904 -unit_async_12 unit_async_12935,936 -unit_async_13 unit_async_13956,957 -unit_async_14 unit_async_14965,966 -unit_async_15 unit_async_15986,987 -unit_async_16 unit_async_161006,1007 -prop_stm_referenceIO prop_stm_referenceIO1033,1034 -prop_stm_referenceSim prop_stm_referenceSim1040,1041 -prop_stm_referenceM prop_stm_referenceM1051,1052 -prop_timeout_no_deadlockM prop_timeout_no_deadlockM1062,1063 -prop_timeout_no_deadlock_Sim prop_timeout_no_deadlock_Sim1084,1085 -prop_timeout_no_deadlock_IO prop_timeout_no_deadlock_IO1087,1088 -setMaskingState_ setMaskingState_1095,1096 -setMaskingState setMaskingState1100,1101 -maxMS maxMS1106,1107 -forall_masking_states forall_masking_states1114,1115 -prop_set_masking_state prop_set_masking_state1125,1126 -unit_set_masking_state_IO unit_set_masking_state_IO1133,1134 -unit_set_masking_state_ST unit_set_masking_state_ST1137,1138 -prop_unmask prop_unmask1144,1145 -unit_unmask_IO unit_unmask_IO1154,1155 -unit_unmask_ST unit_unmask_ST1157,1158 -prop_fork_masking_state prop_fork_masking_state1163,1164 -unit_fork_masking_state_IO unit_fork_masking_state_IO1174,1175 -unit_fork_masking_state_ST unit_fork_masking_state_ST1178,1179 -prop_fork_unmask prop_fork_unmask1188,1189 -unit_fork_unmask_IO unit_fork_unmask_IO1204,1205 -unit_fork_unmask_ST unit_fork_unmask_ST1207,1208 -prop_catch_throwIO_masking_state prop_catch_throwIO_masking_state1214,1215 -unit_catch_throwIO_masking_state_IO unit_catch_throwIO_masking_state_IO1223,1224 -unit_catch_throwIO_masking_state_ST unit_catch_throwIO_masking_state_ST1227,1228 -prop_catch_throwTo_masking_state prop_catch_throwTo_masking_state1234,1235 -unit_catch_throwTo_masking_state_IO unit_catch_throwTo_masking_state_IO1247,1248 -unit_catch_throwTo_masking_state_ST unit_catch_throwTo_masking_state_ST1251,1252 -prop_catch_throwTo_masking_state_async prop_catch_throwTo_masking_state_async1259,1260 -unit_catch_throwTo_masking_state_async_IO unit_catch_throwTo_masking_state_async_IO1285,1286 -unit_catch_throwTo_masking_state_async_ST unit_catch_throwTo_masking_state_async_ST1289,1290 -prop_catch_throwTo_masking_state_async_mayblock prop_catch_throwTo_masking_state_async_mayblock1298,1299 -unit_catch_throwTo_masking_state_async_mayblock_IO unit_catch_throwTo_masking_state_async_mayblock_IO1329,1330 -unit_catch_throwTo_masking_state_async_mayblock_ST unit_catch_throwTo_masking_state_async_mayblock_ST1333,1334 -runSimTraceSay runSimTraceSay1341,1342 -selectTraceSay selectTraceSay1344,1345 - -./test/Test/STM.hs,4426 -module Test.STM Test.STM22,23 -data Type Type41,42 - TyUnit TyUnit42,43 - TyInt TyInt43,44 - TyVar TyVar44,45 - TyUnit TyUnit42,43 - TyInt TyInt43,44 - TyVar TyVar44,45 -data TyRep TyRep49,50 -data TyRep (t t49,50 - TyRepUnit TyRepUnit50,51 - TyRepInt TyRepInt51,52 - TyRepVar TyRepVar52,53 -data TyRep (t t49,50 -data Term Term65,66 -data Term (t t65,66 - Return Return67,68 - Throw Throw68,69 - Retry Retry69,70 - ReadTVar ReadTVar71,72 - WriteTVar WriteTVar72,73 - NewTVar NewTVar73,74 - Bind Bind76,77 - OrElse OrElse77,78 -data Term (t t65,66 -data Expr Expr84,85 -data Expr (t t84,85 - ExprUnit ExprUnit86,87 - ExprInt ExprInt87,88 - ExprName ExprName88,89 -data Expr (t t84,85 -data Value Value95,96 -data Value (t t95,96 - ValUnit ValUnit97,98 - ValInt ValInt98,99 - ValVar ValVar99,100 -data Value (t t95,96 -data Name Name114,115 -data Name (t :: Type) = Name Name114,115 -newtype NameId NameId117,118 -data Var Var125,126 -data Var (t :: Type) = Var Var125,126 -newtype VarId VarId128,129 -eqTyRep eqTyRep137,138 -nameTyRep nameTyRep145,146 -varTyRep varTyRep148,149 -tyRepExpr tyRepExpr151,152 -tyRepValue tyRepValue156,157 -data SomeName SomeName166,167 - SomeName SomeName167,168 -data SomeValue SomeValue169,170 - SomeValue SomeValue170,171 -newtype Env Env178,179 -lookupEnv lookupEnv183,184 -extendEnv extendEnv190,191 -data SomeVar SomeVar199,200 - SomeVar SomeVar200,201 -newtype Heap Heap204,205 -type Allocs Allocs208,209 -readVar readVar211,212 -writeVar writeVar218,219 -extendHeap extendHeap227,228 -data TxResult TxResult249,250 - TxComitted TxComitted250,251 - | TxBlockedTxBlocked251,252 - | TxAborted TxAborted252,253 -data ImmValue ImmValue261,262 - ImmValUnit ImmValUnit263,264 - ImmValInt ImmValInt264,265 - ImmValVar ImmValVar265,266 - ImmValUnit ImmValUnit263,264 -instance Exception Exception ImmValue271,272 -evalExpr evalExpr279,280 -data NfTerm NfTerm286,287 -data NfTerm (t t286,287 - NfReturn NfReturn288,289 - NfThrow NfThrow289,290 - NfRetry NfRetry290,291 -data NfTerm (t t286,287 -evalTerm evalTerm300,301 -evalAtomically evalAtomically361,362 -snapshotValue snapshotValue388,389 -data ExecValue ExecValue398,399 -data ExecValue m (t t398,399 - ExecValUnit ExecValUnit400,401 - ExecValInt ExecValInt401,402 - ExecValVar ExecValVar402,403 -instance Show Show (ExecValue m t)405,406 - show show406,407 -data SomeExecValue SomeExecValue411,412 - SomeExecValue SomeExecValue412,413 -newtype ExecEnv ExecEnv417,418 -tyRepExecValue tyRepExecValue420,421 -lookupExecEnv lookupExecEnv425,426 -extendExecEnv extendExecEnv432,433 -execTerm execTerm439,440 -execExpr execExpr482,483 -snapshotExecValue snapshotExecValue487,488 -execAtomically execAtomically493,494 -instance Arbitrary Arbitrary SomeTerm513,514 - arbitrary arbitrary514,515 - shrink shrink516,517 -data SomeTerm SomeTerm519,520 - SomeTerm SomeTerm520,521 -data SomeExpr SomeExpr522,523 - SomeExpr SomeExpr523,524 -data GenEnv GenEnv532,533 -data GenEnv = GenEnv GenEnv532,533 - envNames envNames534,535 - envNextName envNextName537,538 -data TyTrie TyTrie540,541 - TyTrieEmptyTyTrieEmpty541,542 - | TyTrieNode TyTrieNode542,543 - trieUnit trieUnit543,544 - trieInt trieInt544,545 - trieVar trieVar545,546 -lookupTyTrie lookupTyTrie549,550 -insertTyTrie insertTyTrie555,556 -emptyGenEnv emptyGenEnv568,569 -lookupNames lookupNames571,572 -freshName freshName577,578 -pickName pickName587,588 -data SomeVarName SomeVarName591,592 - SomeVarName SomeVarName592,593 -lookupVarNames lookupVarNames595,596 -deep deep607,608 -genSomeTerm genSomeTerm614,615 -genTerm genTerm630,631 -genSomeExpr genSomeExpr677,678 -genExpr genExpr686,687 -elements' elements'701,702 -oneof' oneof'704,705 -frequency' frequency'707,708 -shrinkTerm shrinkTerm710,711 -shrinkExpr shrinkExpr730,731 -freeNamesTerm freeNamesTerm737,738 -freeNamesExpr freeNamesExpr748,749 -nameId nameId753,754 -prop_genSomeTerm prop_genSomeTerm756,757 -termSize termSize767,768 -termDepth termDepth777,778 -showTerm showTerm787,788 -showExpr showExpr808,809 -showName showName813,814 -showNameTyped showNameTyped816,817 -showTyRep showTyRep821,822 From 07e448a3abf2e6aee878968ce1e705b4eb41a631 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Wed, 13 Jul 2022 14:01:34 +0530 Subject: [PATCH 04/11] WIP Handling throw and catch semantics --- io-sim/src/Control/Monad/IOSim/Internal.hs | 55 ++++++++++++++++------ io-sim/src/Control/Monad/IOSim/Types.hs | 47 ++++++++++-------- io-sim/test/Main.hs | 5 +- io-sim/test/Test/IOSim.hs | 2 +- io-sim/test/Test/STM.hs | 11 ++++- 5 files changed, 82 insertions(+), 38 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index d6ad7fef..0a6c4cfd 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -19,6 +19,8 @@ -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') -- and 'reschedule'. {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} module Control.Monad.IOSim.Internal ( IOSim (..) @@ -70,7 +72,7 @@ import qualified Deque.Strict as Deque import GHC.Exts (fromList) -import Control.Exception (NonTermination (..), assert, throw) +import Control.Exception (NonTermination (..), assert, throw, SomeException (SomeException)) import Control.Monad (join) import Control.Monad (when) @@ -828,6 +830,7 @@ runSimTraceST mainAction = schedule mainThread initialState } + -- -- Executing STM Transactions -- @@ -843,6 +846,22 @@ execAtomically :: forall s a c. execAtomically !time !tid !tlbl !nextVid0 action0 k0 = go AtomicallyFrame Map.empty Map.empty [] [] nextVid0 action0 where + catchStackFrameOrAbort :: forall b. + StmStack s b a + -> Map TVarId (SomeTVar s) + -> SomeException + -> TVarId + -> ST s (SimTrace c) + -> ST s (SimTrace c) + catchStackFrameOrAbort ctl read exc nextVid abort = + case ctl of + AtomicallyFrame -> abort + OrElseLeftFrame _ _ _ _ _ ctl' -> catchStackFrameOrAbort ctl' read exc nextVid abort + OrElseRightFrame _ _ _ _ ctl' -> catchStackFrameOrAbort ctl' read exc nextVid abort + CatchStmFrame handler _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (handler exc) + + go :: forall b. StmStack s b a -> Map TVarId (SomeTVar s) -- set of vars read @@ -910,20 +929,23 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = -- Continue with the k continuation go ctl' read written' writtenSeq' createdSeq' nextVid (k x) - CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid undefined + CatchStmFrame _handler k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + -- Merge allocations with outer sequence + let written' = Map.union written writtenOuter + writtenSeq' = filter (\(SomeTVar tvar) -> + tvarId tvar `Map.notMember` writtenOuter) + writtenSeq + ++ writtenOuterSeq + createdSeq' = createdSeq ++ createdOuterSeq + go ctl' read written' writtenSeq' createdSeq' nextVid (k x) ThrowStm e -> - {-# SCC "execAtomically.go.ThrowStm" #-} do - case ctl of - CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - -- Use handler to rescue the exception - -- go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (handler e') - undefined - _ -> do - -- Revert all the TVar writes - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - k0 $ StmTxAborted [] (toException e) + {-# SCC "execAtomically.go.ThrowStm" #-} + let abort = do + -- Revert all the TVar writes + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + k0 $ StmTxAborted [] (toException e) + in catchStackFrameOrAbort ctl read (toException e) nextVid abort CatchStm act handler k -> {-# SCC "execAtomically.go.CatchStm" #-} do @@ -955,9 +977,12 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = -- using the written set for the outer frame go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry - CatchStmFrame handler _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + CatchStmFrame _handler _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.catchStmFrame" #-} do - undefined + -- This is XSTM3 test case from the STM paper. + -- Revert all the TVar writes within this catch action branch + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry OrElse a b k -> {-# SCC "execAtomically.go.OrElse" #-} do diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index ccdc875d..a22e9d5a 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -14,6 +14,7 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {-# OPTIONS_GHC -Wno-partial-fields #-} +{-# LANGUAGE MultiWayIf #-} module Control.Monad.IOSim.Types ( IOSim (..) @@ -175,7 +176,8 @@ runSTM (STM k) = k ReturnStm data StmA s a where ReturnStm :: a -> StmA s a ThrowStm :: SomeException -> StmA s a - CatchStm :: Exception e => StmA s a -> (e -> StmA s a) -> (a -> StmA s b) -> StmA s b + -- Catch with continuation + 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 LabelTVar :: String -> TVar s a -> StmA s b -> StmA s b @@ -225,9 +227,9 @@ instance Monad (IOSim s) where {-# INLINE (>>) #-} (>>) = (*>) -#if !(MIN_VERSION_base(4,13,0)) - fail = Fail.fail -#endif + + + instance Semigroup a => Semigroup (IOSim s a) where (<>) = liftA2 (<>) @@ -235,9 +237,9 @@ instance Semigroup a => Semigroup (IOSim s a) where instance Monoid a => Monoid (IOSim s a) where mempty = pure mempty -#if !(MIN_VERSION_base(4,11,0)) - mappend = liftA2 mappend -#endif + + + instance Fail.MonadFail (IOSim s) where fail msg = IOSim $ oneShot $ \_ -> Throw (toException (IO.Error.userError msg)) @@ -270,9 +272,9 @@ instance Monad (STM s) where {-# INLINE (>>) #-} (>>) = (*>) -#if !(MIN_VERSION_base(4,13,0)) - fail = Fail.fail -#endif + + + instance Fail.MonadFail (STM s) where fail msg = STM $ oneShot $ \_ -> ThrowStm (toException (ErrorCall msg)) @@ -314,14 +316,20 @@ instance MonadThrow (STM s) where instance Exceptions.MonadThrow (STM s) where throwM = MonadThrow.throwIO -instance MonadCatch (STM s) where +instance MonadCatch (STM s) where - catch action handler = STM $ oneShot $ \k -> CatchStm (runSTM action) (runSTM . handler) k + catch action handler = STM $ oneShot $ \k -> CatchStm (runSTM action) (runSTM . handler') k + where + handler' :: SomeException -> STM s a + handler' exc = + if + | Just exc' <- fromException exc -> handler exc' + | otherwise -> throwIO exc -- Default implmentation uses mask. For STM, mask is not necessary. - generalBracket = generalBracketSTM + generalBracket = generalBracketSTM -instance Exceptions.MonadCatch (STM s) where +instance Exceptions.MonadCatch (STM s) where catch = MonadThrow.catch @@ -866,14 +874,13 @@ data StmStack s b a where -> StmStack s a c -- | Executing in the context of the /action/ part of the 'catch' - CatchStmFrame :: Exception e - => (e -> StmA s a) -- exception handler + CatchStmFrame :: (SomeException -> StmA s a) -- exception handler -> (a -> StmA s b) -- subsequent continuation -> Map TVarId (SomeTVar s) -- saved written vars set - -> [SomeTVar s] -- saved written vars set - -> [SomeTVar s] -- created vars list - -> StmStack s b c - -> StmStack s a c + -> [SomeTVar s] -- saved written vars list + -> [SomeTVar s] -- created vars list (allocations) + -> StmStack s b c + -> StmStack s a c --- --- Schedules --- diff --git a/io-sim/test/Main.hs b/io-sim/test/Main.hs index 87db2244..8d31a082 100644 --- a/io-sim/test/Main.hs +++ b/io-sim/test/Main.hs @@ -3,6 +3,7 @@ module Main (main) where import Test.Tasty import qualified Test.IOSim (tests) +import qualified Test.STM (tests) main :: IO () main = defaultMain tests @@ -10,5 +11,7 @@ main = defaultMain tests tests :: TestTree tests = testGroup "IO Sim" - [ Test.IOSim.tests + [ + Test.IOSim.tests + , Test.STM.tests ] diff --git a/io-sim/test/Test/IOSim.hs b/io-sim/test/Test/IOSim.hs index 576f0446..44e331dd 100644 --- a/io-sim/test/Test/IOSim.hs +++ b/io-sim/test/Test/IOSim.hs @@ -33,7 +33,7 @@ import Control.Monad.Class.MonadTime import Control.Monad.Class.MonadTimer import Control.Monad.IOSim -import Test.STM +import Test.STM hiding (tests) import Test.QuickCheck import Test.Tasty diff --git a/io-sim/test/Test/STM.hs b/io-sim/test/Test/STM.hs index 1df40207..c4e105d0 100644 --- a/io-sim/test/Test/STM.hs +++ b/io-sim/test/Test/STM.hs @@ -34,6 +34,8 @@ import Control.Monad.Class.MonadSTM as STM import Control.Monad.Class.MonadThrow import Test.QuickCheck +import Test.Tasty (testGroup, TestTree) +import Test.Tasty.QuickCheck (testProperty) -- | The type level structure of types in our STM 'Term's. This is kept simple, @@ -318,7 +320,7 @@ evalTerm !env !heap !allocs term = case term of -- Rule XSTM1 -- M; heap, {} => return P; heap', allocs' -- -------------------------------------------------------- - -- S[catch M N]; heap, allocs => S[N P]; heap, allocs + -- S[catch M N]; heap, allocs => S[return P]; heap, allocs NfReturn v -> (NfReturn v, heap', allocs `mappend` allocs') -- Rule XSTM2 @@ -860,3 +862,10 @@ showTyRep _ TyRepUnit = showString "()" showTyRep _ TyRepInt = showString "Int" showTyRep p (TyRepVar t) = showParen (p > 10) $ showString "TVar " . showTyRep 11 t + +tests :: TestTree +tests = + testGroup "Test STM" + [ + testProperty "Term generation" prop_genSomeTerm + ] From c637d59423b5914b72f247eb3aecb1d29725b672 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Thu, 14 Jul 2022 13:27:15 +0530 Subject: [PATCH 05/11] Add `Catch` support for generator --- .../src/Control/Monad/Class/MonadThrow.hs | 12 +++----- io-sim/src/Control/Monad/IOSim/Internal.hs | 29 ++++++++++--------- io-sim/src/Control/Monad/IOSim/Types.hs | 21 +++++++------- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 24 +++++++++++++++ io-sim/test/Test/STM.hs | 11 +++++-- 5 files changed, 62 insertions(+), 35 deletions(-) diff --git a/io-classes/src/Control/Monad/Class/MonadThrow.hs b/io-classes/src/Control/Monad/Class/MonadThrow.hs index 2fe79612..ad655fed 100644 --- a/io-classes/src/Control/Monad/Class/MonadThrow.hs +++ b/io-classes/src/Control/Monad/Class/MonadThrow.hs @@ -18,7 +18,6 @@ module Control.Monad.Class.MonadThrow , ExitCase (..) , Handler (..) , catches - , generalBracketSTM -- * Deprecated interfaces , throwM ) where @@ -243,8 +242,10 @@ instance MonadThrow STM where throwIO = STM.throwSTM -generalBracketSTM :: MonadCatch m => m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c) -generalBracketSTM acquire release use = do +instance MonadCatch STM where + catch = STM.catchSTM + + generalBracket acquire release use = do resource <- acquire b <- use resource `catch` \e -> do _ <- release resource (ExitCaseException e) @@ -252,11 +253,6 @@ generalBracketSTM acquire release use = do c <- release resource (ExitCaseSuccess b) return (b, c) -instance MonadCatch STM where - catch = STM.catchSTM - - generalBracket = generalBracketSTM - -- -- Instances for ReaderT diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 0a6c4cfd..343166fc 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -19,8 +19,8 @@ -- incomplete uni patterns in 'schedule' (when interpreting 'StmTxCommitted') -- and 'reschedule'. {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} module Control.Monad.IOSim.Internal ( IOSim (..) @@ -72,7 +72,8 @@ import qualified Deque.Strict as Deque import GHC.Exts (fromList) -import Control.Exception (NonTermination (..), assert, throw, SomeException (SomeException)) +import Control.Exception (NonTermination (..), + SomeException (SomeException), assert, throw) import Control.Monad (join) import Control.Monad (when) @@ -829,8 +830,6 @@ runSimTraceST mainAction = schedule mainThread initialState threadNextTId = 1 } - - -- -- Executing STM Transactions -- @@ -849,17 +848,19 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = catchStackFrameOrAbort :: forall b. StmStack s b a -> Map TVarId (SomeTVar s) - -> SomeException + -> SomeException -> TVarId -> ST s (SimTrace c) -> ST s (SimTrace c) catchStackFrameOrAbort ctl read exc nextVid abort = - case ctl of + case ctl of AtomicallyFrame -> abort - OrElseLeftFrame _ _ _ _ _ ctl' -> catchStackFrameOrAbort ctl' read exc nextVid abort - OrElseRightFrame _ _ _ _ ctl' -> catchStackFrameOrAbort ctl' read exc nextVid abort + OrElseLeftFrame _ _ _ _ _ ctl' -> catchStackFrameOrAbort ctl' read exc nextVid abort + OrElseRightFrame _ _ _ _ ctl' -> catchStackFrameOrAbort ctl' read exc nextVid abort CatchStmFrame handler _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> - go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (handler exc) + case fromException exc of + Nothing -> catchStackFrameOrAbort ctl' read exc nextVid abort + Just e' -> go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (handler e') go :: forall b. @@ -940,14 +941,14 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = go ctl' read written' writtenSeq' createdSeq' nextVid (k x) ThrowStm e -> - {-# SCC "execAtomically.go.ThrowStm" #-} + {-# SCC "execAtomically.go.ThrowStm" #-} let abort = do -- Revert all the TVar writes !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written k0 $ StmTxAborted [] (toException e) - in catchStackFrameOrAbort ctl read (toException e) nextVid abort + in catchStackFrameOrAbort ctl read (toException e) nextVid abort - CatchStm act handler k -> + CatchStm act handler k -> {-# SCC "execAtomically.go.CatchStm" #-} do let ctl' = CatchStmFrame handler k written writtenSeq createdSeq ctl go ctl' read Map.empty [] [] nextVid act @@ -979,7 +980,7 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = CatchStmFrame _handler _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.catchStmFrame" #-} do - -- This is XSTM3 test case from the STM paper. + -- This is XSTM3 test case from the STM paper. -- Revert all the TVar writes within this catch action branch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index a22e9d5a..5b3818f8 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -177,7 +177,7 @@ data StmA s a where ReturnStm :: a -> StmA s a ThrowStm :: SomeException -> StmA s a -- Catch with continuation - CatchStm :: StmA s a -> (SomeException -> StmA s a) -> (a -> StmA s b) -> StmA s b + CatchStm :: Exception e => StmA s a -> (e -> StmA s a) -> (a -> StmA s b) -> StmA s b NewTVar :: Maybe String -> x -> (TVar s x -> StmA s b) -> StmA s b LabelTVar :: String -> TVar s a -> StmA s b -> StmA s b @@ -318,16 +318,16 @@ instance Exceptions.MonadThrow (STM s) where instance MonadCatch (STM s) where - catch action handler = STM $ oneShot $ \k -> CatchStm (runSTM action) (runSTM . handler') k - where - handler' :: SomeException -> STM s a - handler' exc = - if - | Just exc' <- fromException exc -> handler exc' - | otherwise -> throwIO exc + catch action handler = STM $ oneShot $ \k -> CatchStm (runSTM action) (runSTM . handler) k -- Default implmentation uses mask. For STM, mask is not necessary. - generalBracket = generalBracketSTM + generalBracket acquire release use = do + resource <- acquire + b <- use resource `catch` \e -> do + _ <- release resource (ExitCaseException e) + throwIO e + c <- release resource (ExitCaseSuccess b) + return (b, c) instance Exceptions.MonadCatch (STM s) where @@ -874,7 +874,8 @@ data StmStack s b a where -> StmStack s a c -- | Executing in the context of the /action/ part of the 'catch' - CatchStmFrame :: (SomeException -> StmA s a) -- exception handler + CatchStmFrame :: Exception e + => (e -> StmA s a) -- exception handler -> (a -> StmA s b) -- subsequent continuation -> Map TVarId (SomeTVar s) -- saved written vars set -> [SomeTVar s] -- saved written vars list diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index e0deae98..01d30270 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1121,12 +1121,28 @@ execAtomically time tid tlbl nextVid0 action0 k0 = -- Continue with the k continuation go ctl' read written' writtenSeq' createdSeq' nextVid (k x) + CatchStmFrame _handler k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + let written' = Map.union written writtenOuter + writtenSeq' = filter (\(SomeTVar tvar) -> + tvarId tvar `Map.notMember` writtenOuter) + writtenSeq + ++ writtenOuterSeq + createdSeq' = createdSeq ++ createdOuterSeq + go ctl' read written' writtenSeq' createdSeq' nextVid (k x) + + ThrowStm e -> {-# SCC "execAtomically.go.ThrowStm" #-} do -- Revert all the TVar writes + -- TODO: Add unwind support !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written k0 $ StmTxAborted (Map.elems read) (toException e) + CatchStm act handler k -> + {-# SCC "execAtomically.go.ThrowStm" #-} do + let ctl' = CatchStmFrame handler k written writtenSeq createdSeq ctl + go ctl' read Map.empty [] [] nextVid act + Retry -> {-# SCC "execAtomically.go.Retry" #-} case ctl of @@ -1152,6 +1168,14 @@ execAtomically time tid tlbl nextVid0 action0 k0 = -- using the written set for the outer frame go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry + CatchStmFrame _handler _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.catchStmFrame" #-} do + -- This is XSTM3 test case from the STM paper. + -- Revert all the TVar writes within this catch action branch + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry + + OrElse a b k -> {-# SCC "execAtomically.go.OrElse" #-} do -- Execute the left side in a new frame with an empty written set diff --git a/io-sim/test/Test/STM.hs b/io-sim/test/Test/STM.hs index c4e105d0..556f18e5 100644 --- a/io-sim/test/Test/STM.hs +++ b/io-sim/test/Test/STM.hs @@ -320,13 +320,13 @@ evalTerm !env !heap !allocs term = case term of -- Rule XSTM1 -- M; heap, {} => return P; heap', allocs' -- -------------------------------------------------------- - -- S[catch M N]; heap, allocs => S[return P]; heap, allocs + -- S[catch M N]; heap, allocs => S[return P]; heap', allocs' NfReturn v -> (NfReturn v, heap', allocs `mappend` allocs') -- Rule XSTM2 -- M; heap, {} => throw P; heap', allocs' -- -------------------------------------------------------- - -- S[catch M N]; heap, allocs => S[N P]; heap, allocs + -- S[catch M N]; heap, allocs => S[N P]; heap U allocs', allocs U allocs' NfThrow _ -> evalTerm env (heap `mappend` allocs') (allocs `mappend` allocs') t2 -- Rule XSTM3 @@ -686,7 +686,7 @@ genTerm env tyrep = Nothing) ] - binTerm = frequency [ (2, bindTerm), (1, orElseTerm)] + binTerm = frequency [ (2, bindTerm), (1, orElseTerm), (1, catchTerm)] bindTerm = sized $ \sz -> do @@ -704,6 +704,11 @@ genTerm env tyrep = OrElse <$> genTerm env tyrep <*> genTerm env tyrep + catchTerm = + sized $ \sz -> resize (sz `div` 2) $ + Catch <$> genTerm env tyrep + <*> genTerm env tyrep + genSomeExpr :: GenEnv -> Gen SomeExpr genSomeExpr env = oneof' From 1ae2f72ffaeb28d69c295d7ec5c215ee50410c0a Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Thu, 14 Jul 2022 21:08:28 +0530 Subject: [PATCH 06/11] Add exception semantics - Add Catch handler frame `CatchHandlerStmFrame` for handling catch handler - Add unwind support for handling matching exceptions --- io-sim/src/Control/Monad/IOSim/Internal.hs | 81 +++++++++++++++------- io-sim/src/Control/Monad/IOSim/Types.hs | 8 +++ 2 files changed, 65 insertions(+), 24 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 343166fc..d3b2cb0b 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -72,11 +72,8 @@ import qualified Deque.Strict as Deque import GHC.Exts (fromList) -import Control.Exception (NonTermination (..), - SomeException (SomeException), assert, throw) -import Control.Monad (join) - -import Control.Monad (when) +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 @@ -830,6 +827,33 @@ runSimTraceST mainAction = schedule mainThread initialState threadNextTId = 1 } + +data StmControl s a where + StmControl :: StmA s b -> !(StmStack s b a) -> StmControl s a + + +-- Unwind the STM control stack till the matching exception +unwindControlStmStack :: forall s a. + SomeException + -> StmControl s a + -> Either Bool (StmControl s a) +unwindControlStmStack e (StmControl _ frame) = unwindFrame frame + + where + unwindFrame :: forall s' b. StmStack s' b a -> Either Bool (StmControl s' a) + unwindFrame AtomicallyFrame = Left True + unwindFrame (OrElseLeftFrame _ _ _ _ _ ctl) = unwindFrame ctl + unwindFrame (OrElseRightFrame _ _ _ _ ctl) = unwindFrame ctl + unwindFrame (CatchHandlerStmFrame _ _ _ _ ctl) = unwindFrame ctl + unwindFrame (CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl) = + case fromException e of + -- Continue to unwind till we find a handler which can handle this exception. + Nothing -> unwindFrame ctl + Just e' -> + let action' = handler e' + ctl' = CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl + in Right $ StmControl action' ctl' + -- -- Executing STM Transactions -- @@ -845,24 +869,6 @@ execAtomically :: forall s a c. execAtomically !time !tid !tlbl !nextVid0 action0 k0 = go AtomicallyFrame Map.empty Map.empty [] [] nextVid0 action0 where - catchStackFrameOrAbort :: forall b. - StmStack s b a - -> Map TVarId (SomeTVar s) - -> SomeException - -> TVarId - -> ST s (SimTrace c) - -> ST s (SimTrace c) - catchStackFrameOrAbort ctl read exc nextVid abort = - case ctl of - AtomicallyFrame -> abort - OrElseLeftFrame _ _ _ _ _ ctl' -> catchStackFrameOrAbort ctl' read exc nextVid abort - OrElseRightFrame _ _ _ _ ctl' -> catchStackFrameOrAbort ctl' read exc nextVid abort - CatchStmFrame handler _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> - case fromException exc of - Nothing -> catchStackFrameOrAbort ctl' read exc nextVid abort - Just e' -> go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (handler e') - - go :: forall b. StmStack s b a -> Map TVarId (SomeTVar s) -- set of vars read @@ -931,6 +937,20 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = go ctl' read written' writtenSeq' createdSeq' nextVid (k x) CatchStmFrame _handler k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + -- Successful main catch action + -- Merge allocations with outer sequence + let written' = Map.union written writtenOuter + writtenSeq' = filter (\(SomeTVar tvar) -> + tvarId tvar `Map.notMember` writtenOuter) + writtenSeq + ++ writtenOuterSeq + createdSeq' = createdSeq ++ createdOuterSeq + go ctl' read written' writtenSeq' createdSeq' nextVid (k x) + + CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + -- Successful completion of catch handler + !_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar) + (Map.intersection written writtenOuter) -- Merge allocations with outer sequence let written' = Map.union written writtenOuter writtenSeq' = filter (\(SomeTVar tvar) -> @@ -942,11 +962,16 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = ThrowStm e -> {-# SCC "execAtomically.go.ThrowStm" #-} + -- Abort if no matching exception is found let abort = do -- Revert all the TVar writes !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written k0 $ StmTxAborted [] (toException e) - in catchStackFrameOrAbort ctl read (toException e) nextVid abort + + -- Unwind to the nearest matching exception + in case unwindControlStmStack e (StmControl action ctl) of + Left _ -> abort + Right (StmControl action' ctl') -> go ctl' read written writtenSeq createdSeq nextVid action' CatchStm act handler k -> {-# SCC "execAtomically.go.CatchStm" #-} do @@ -985,6 +1010,14 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry + CatchHandlerStmFrame _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.catchStmFrame" #-} do + -- This is XSTM3 test case from the STM paper. + -- Revert all the TVar writes within this catch action branch + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry + + OrElse a b k -> {-# SCC "execAtomically.go.OrElse" #-} do -- Execute the left side in a new frame with an empty written set diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index 5b3818f8..0da0df80 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -882,6 +882,14 @@ data StmStack s b a where -> [SomeTVar s] -- created vars list (allocations) -> StmStack s b c -> StmStack s a c + + -- | A continuation frame + CatchHandlerStmFrame :: (b -> StmA s c) -- subsequent continuation + -> Map TVarId (SomeTVar s) -- saved written vars set + -> [SomeTVar s] -- saved written vars list + -> [SomeTVar s] -- created vars list (allocations) + -> !(StmStack s c a) + -> StmStack s b a --- --- Schedules --- From 1f74a5a7c2f0748576f75a8c144360e1779ea8bc Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Thu, 14 Jul 2022 21:51:08 +0530 Subject: [PATCH 07/11] Add unwind support to IOSimPOR --- io-sim/src/Control/Monad/IOSim/Internal.hs | 2 +- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 60 +++++++++++++++++-- 2 files changed, 55 insertions(+), 7 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index d3b2cb0b..7f3a0a42 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -832,7 +832,7 @@ data StmControl s a where StmControl :: StmA s b -> !(StmStack s b a) -> StmControl s a --- Unwind the STM control stack till the matching exception +-- Unwind the STM control stack till the matching exception is found unwindControlStmStack :: forall s a. SomeException -> StmControl s a diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 01d30270..10d71634 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1039,6 +1039,32 @@ controlSimTraceST limit control mainAction = } +data StmControl s a where + StmControl :: StmA s b -> !(StmStack s b a) -> StmControl s a + + +-- Unwind the STM control stack till the matching exception is found +unwindControlStmStack :: forall s a. + SomeException + -> StmControl s a + -> Either Bool (StmControl s a) +unwindControlStmStack e (StmControl _ frame) = unwindFrame frame + + where + unwindFrame :: forall s' b. StmStack s' b a -> Either Bool (StmControl s' a) + unwindFrame AtomicallyFrame = Left True + unwindFrame (OrElseLeftFrame _ _ _ _ _ ctl) = unwindFrame ctl + unwindFrame (OrElseRightFrame _ _ _ _ ctl) = unwindFrame ctl + unwindFrame (CatchHandlerStmFrame _ _ _ _ ctl) = unwindFrame ctl + unwindFrame (CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl) = + case fromException e of + -- Continue to unwind till we find a handler which can handle this exception. + Nothing -> unwindFrame ctl + Just e' -> + let action' = handler e' + ctl' = CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl + in Right $ StmControl action' ctl' + -- -- Executing STM Transactions -- @@ -1130,13 +1156,30 @@ execAtomically time tid tlbl nextVid0 action0 k0 = createdSeq' = createdSeq ++ createdOuterSeq go ctl' read written' writtenSeq' createdSeq' nextVid (k x) + CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + !_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar) + (Map.intersection written writtenOuter) + let written' = Map.union written writtenOuter + writtenSeq' = filter (\(SomeTVar tvar) -> + tvarId tvar `Map.notMember` writtenOuter) + writtenSeq + ++ writtenOuterSeq + createdSeq' = createdSeq ++ createdOuterSeq + go ctl' read written' writtenSeq' createdSeq' nextVid (k x) + + ThrowStm e -> - {-# SCC "execAtomically.go.ThrowStm" #-} do - -- Revert all the TVar writes - -- TODO: Add unwind support - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - k0 $ StmTxAborted (Map.elems read) (toException e) + {-# SCC "execAtomically.go.ThrowStm" #-} + + let abort = do + -- Revert all the TVar writes + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + k0 $ StmTxAborted (Map.elems read) (toException e) + + in case unwindControlStmStack e (StmControl action ctl) of + Left _ -> abort + Right (StmControl action' ctl') -> go ctl' read written writtenSeq createdSeq nextVid action' CatchStm act handler k -> {-# SCC "execAtomically.go.ThrowStm" #-} do @@ -1170,7 +1213,12 @@ execAtomically time tid tlbl nextVid0 action0 k0 = CatchStmFrame _handler _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.catchStmFrame" #-} do - -- This is XSTM3 test case from the STM paper. + -- Revert all the TVar writes within this catch action branch + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry + + CatchHandlerStmFrame _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.catchHandlerStmFrame" #-} do -- Revert all the TVar writes within this catch action branch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry From 5868e9c721f4ae62f2c39740c5eaf647e9991ea2 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Tue, 19 Jul 2022 12:13:39 +0530 Subject: [PATCH 08/11] Add more tests to reproduce the error --- io-sim/test/Test/IOSim.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/io-sim/test/Test/IOSim.hs b/io-sim/test/Test/IOSim.hs index 44e331dd..8adce19d 100644 --- a/io-sim/test/Test/IOSim.hs +++ b/io-sim/test/Test/IOSim.hs @@ -134,8 +134,8 @@ tests = , testProperty "16" unit_async_16 ] , testGroup "STM reference semantics" - [ testProperty "Reference vs IO" prop_stm_referenceIO - , testProperty "Reference vs Sim" prop_stm_referenceSim + [ testProperty "Reference vs IO" (withMaxSuccess 10000 prop_stm_referenceIO) + , testProperty "Reference vs Sim" (withMaxSuccess 10000 prop_stm_referenceSim) ] , testGroup "MonadFix instance" [ testProperty "purity" prop_mfix_purity From 4d6d6eca0bbfa4b38a174931aae46f330169bdd7 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Tue, 19 Jul 2022 13:03:03 +0530 Subject: [PATCH 09/11] Add style changes --- io-sim/src/Control/Monad/IOSim/Types.hs | 4 ++-- io-sim/test/Main.hs | 2 +- io-sim/test/Test/STM.hs | 10 +++++----- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index 0da0df80..ed9d8b7b 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -14,7 +14,7 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {-# OPTIONS_GHC -Wno-partial-fields #-} -{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE MultiWayIf #-} module Control.Monad.IOSim.Types ( IOSim (..) @@ -874,7 +874,7 @@ data StmStack s b a where -> StmStack s a c -- | Executing in the context of the /action/ part of the 'catch' - CatchStmFrame :: Exception e + CatchStmFrame :: Exception e => (e -> StmA s a) -- exception handler -> (a -> StmA s b) -- subsequent continuation -> Map TVarId (SomeTVar s) -- saved written vars set diff --git a/io-sim/test/Main.hs b/io-sim/test/Main.hs index 8d31a082..eb170f08 100644 --- a/io-sim/test/Main.hs +++ b/io-sim/test/Main.hs @@ -11,7 +11,7 @@ main = defaultMain tests tests :: TestTree tests = testGroup "IO Sim" - [ + [ Test.IOSim.tests , Test.STM.tests ] diff --git a/io-sim/test/Test/STM.hs b/io-sim/test/Test/STM.hs index 556f18e5..6765a3b5 100644 --- a/io-sim/test/Test/STM.hs +++ b/io-sim/test/Test/STM.hs @@ -34,8 +34,8 @@ import Control.Monad.Class.MonadSTM as STM import Control.Monad.Class.MonadThrow import Test.QuickCheck -import Test.Tasty (testGroup, TestTree) -import Test.Tasty.QuickCheck (testProperty) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck (testProperty) -- | The type level structure of types in our STM 'Term's. This is kept simple, @@ -704,9 +704,9 @@ genTerm env tyrep = OrElse <$> genTerm env tyrep <*> genTerm env tyrep - catchTerm = + catchTerm = sized $ \sz -> resize (sz `div` 2) $ - Catch <$> genTerm env tyrep + Catch <$> genTerm env tyrep <*> genTerm env tyrep genSomeExpr :: GenEnv -> Gen SomeExpr @@ -869,7 +869,7 @@ showTyRep p (TyRepVar t) = showParen (p > 10) $ showString "TVar " . showTyRep 11 t tests :: TestTree -tests = +tests = testGroup "Test STM" [ testProperty "Term generation" prop_genSomeTerm From 6afd94fe0edc9db5c59f4200cfc4bc17373558d7 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Thu, 21 Jul 2022 22:16:19 +0530 Subject: [PATCH 10/11] Unwind the stack on exception --- io-sim/src/Control/Monad/IOSim/Internal.hs | 55 +++++++++---------- io-sim/src/Control/Monad/IOSim/Types.hs | 22 +++++--- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 14 ++--- 3 files changed, 47 insertions(+), 44 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 7f3a0a42..a4507da8 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -73,7 +73,7 @@ import qualified Deque.Strict as Deque import GHC.Exts (fromList) import Control.Exception (NonTermination (..), assert, throw) -import Control.Monad (join, when) +import Control.Monad (join, when, forM_) import Control.Monad.ST.Lazy import Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST) import Data.STRef.Lazy @@ -837,21 +837,21 @@ unwindControlStmStack :: forall s a. SomeException -> StmControl s a -> Either Bool (StmControl s a) -unwindControlStmStack e (StmControl _ frame) = unwindFrame frame +unwindControlStmStack e (StmControl _ frame) = unwindFrame [] frame where - unwindFrame :: forall s' b. StmStack s' b a -> Either Bool (StmControl s' a) - unwindFrame AtomicallyFrame = Left True - unwindFrame (OrElseLeftFrame _ _ _ _ _ ctl) = unwindFrame ctl - unwindFrame (OrElseRightFrame _ _ _ _ ctl) = unwindFrame ctl - unwindFrame (CatchHandlerStmFrame _ _ _ _ ctl) = unwindFrame ctl - unwindFrame (CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl) = + unwindFrame :: forall s' b. [Map TVarId (SomeTVar s')] -> StmStack s' b a -> Either Bool (StmControl s' a) + unwindFrame _ AtomicallyFrame = Left True + unwindFrame ws (OrElseLeftFrame _ _ w _ _ ctl) = unwindFrame (w:ws) ctl + unwindFrame ws (OrElseRightFrame _ w _ _ ctl) = unwindFrame (w:ws) ctl + unwindFrame ws (CatchHandlerStmFrame _ _ws' _w _ _ ctl) = unwindFrame ws ctl -- Should not happen + unwindFrame ws (CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl) = case fromException e of -- Continue to unwind till we find a handler which can handle this exception. - Nothing -> unwindFrame ctl + Nothing -> unwindFrame (writtenOuter:ws) ctl Just e' -> let action' = handler e' - ctl' = CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl + ctl' = CatchHandlerStmFrame k (reverse ws) writtenOuter writtenOuterSeq createdOuterSeq ctl in Right $ StmControl action' ctl' -- @@ -939,26 +939,23 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = CatchStmFrame _handler k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do -- Successful main catch action -- Merge allocations with outer sequence - let written' = Map.union written writtenOuter - writtenSeq' = filter (\(SomeTVar tvar) -> - tvarId tvar `Map.notMember` writtenOuter) - writtenSeq - ++ writtenOuterSeq - createdSeq' = createdSeq ++ createdOuterSeq - go ctl' read written' writtenSeq' createdSeq' nextVid (k x) - - CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do - -- Successful completion of catch handler !_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar) (Map.intersection written writtenOuter) - -- Merge allocations with outer sequence + -- 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 - go ctl' read written' writtenSeq' createdSeq' nextVid (k x) + -- Skip the orElse right hand and continue with the k continuation + go ctl' read written' writtenSeq' createdOuterSeq nextVid (k x) + + CatchHandlerStmFrame k ws writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + -- Undo all written tvars + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + -- And all the ones till the catch frame + forM_ ws $ traverse_ (\(SomeTVar tvar) -> revertTVar tvar) + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (k x) ThrowStm e -> {-# SCC "execAtomically.go.ThrowStm" #-} @@ -970,8 +967,8 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = -- Unwind to the nearest matching exception in case unwindControlStmStack e (StmControl action ctl) of - Left _ -> abort Right (StmControl action' ctl') -> go ctl' read written writtenSeq createdSeq nextVid action' + _ -> abort CatchStm act handler k -> {-# SCC "execAtomically.go.CatchStm" #-} do @@ -1010,14 +1007,14 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry - CatchHandlerStmFrame _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> - {-# SCC "execAtomically.go.catchStmFrame" #-} do - -- This is XSTM3 test case from the STM paper. - -- Revert all the TVar writes within this catch action branch + CatchHandlerStmFrame _k ws writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.catchHandlerStmFrame" #-} do + -- Undo all written tvars !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + -- And all the ones till the catch frame + forM_ ws $ traverse_ (\(SomeTVar tvar) -> revertTVar tvar) go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry - OrElse a b k -> {-# SCC "execAtomically.go.OrElse" #-} do -- Execute the left side in a new frame with an empty written set diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index ed9d8b7b..dd59c649 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -14,7 +14,6 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {-# OPTIONS_GHC -Wno-partial-fields #-} -{-# LANGUAGE MultiWayIf #-} module Control.Monad.IOSim.Types ( IOSim (..) @@ -227,7 +226,9 @@ instance Monad (IOSim s) where {-# INLINE (>>) #-} (>>) = (*>) - +#if !(MIN_VERSION_base(4,13,0)) + fail = Fail.fail +#endif @@ -237,7 +238,9 @@ instance Semigroup a => Semigroup (IOSim s a) where instance Monoid a => Monoid (IOSim s a) where mempty = pure mempty - +#if !(MIN_VERSION_base(4,11,0)) + mappend = liftA2 mappend +#endif @@ -272,7 +275,9 @@ instance Monad (STM s) where {-# INLINE (>>) #-} (>>) = (*>) - +#if !(MIN_VERSION_base(4,13,0)) + fail = Fail.fail +#endif @@ -884,10 +889,11 @@ data StmStack s b a where -> StmStack s a c -- | A continuation frame - CatchHandlerStmFrame :: (b -> StmA s c) -- subsequent continuation - -> Map TVarId (SomeTVar s) -- saved written vars set - -> [SomeTVar s] -- saved written vars list - -> [SomeTVar s] -- created vars list (allocations) + CatchHandlerStmFrame :: (b -> StmA s c) -- subsequent continuation + -> [Map TVarId (SomeTVar s)] -- All written vars between `throw` and `catch` + -> Map TVarId (SomeTVar s) -- saved written vars set + -> [SomeTVar s] -- saved written vars list + -> [SomeTVar s] -- created vars list (allocations) -> !(StmStack s c a) -> StmStack s b a --- diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 10d71634..7b5ea847 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1052,17 +1052,17 @@ unwindControlStmStack e (StmControl _ frame) = unwindFrame frame where unwindFrame :: forall s' b. StmStack s' b a -> Either Bool (StmControl s' a) - unwindFrame AtomicallyFrame = Left True - unwindFrame (OrElseLeftFrame _ _ _ _ _ ctl) = unwindFrame ctl - unwindFrame (OrElseRightFrame _ _ _ _ ctl) = unwindFrame ctl - unwindFrame (CatchHandlerStmFrame _ _ _ _ ctl) = unwindFrame ctl + unwindFrame AtomicallyFrame = Left True + unwindFrame (OrElseLeftFrame _ _ _ _ _ ctl) = unwindFrame ctl + unwindFrame (OrElseRightFrame _ _ _ _ ctl) = unwindFrame ctl + unwindFrame (CatchHandlerStmFrame _ _ _ _ _ ctl) = unwindFrame ctl unwindFrame (CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl) = case fromException e of -- Continue to unwind till we find a handler which can handle this exception. Nothing -> unwindFrame ctl Just e' -> let action' = handler e' - ctl' = CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl + ctl' = CatchHandlerStmFrame k [] writtenOuter writtenOuterSeq createdOuterSeq ctl in Right $ StmControl action' ctl' -- @@ -1156,7 +1156,7 @@ execAtomically time tid tlbl nextVid0 action0 k0 = createdSeq' = createdSeq ++ createdOuterSeq go ctl' read written' writtenSeq' createdSeq' nextVid (k x) - CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + CatchHandlerStmFrame k [] writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do !_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar) (Map.intersection written writtenOuter) let written' = Map.union written writtenOuter @@ -1217,7 +1217,7 @@ execAtomically time tid tlbl nextVid0 action0 k0 = !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry - CatchHandlerStmFrame _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + CatchHandlerStmFrame _k [] writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.catchHandlerStmFrame" #-} do -- Revert all the TVar writes within this catch action branch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written From 7db68cabdc512614fa67f35a89fb489744ad2f99 Mon Sep 17 00:00:00 2001 From: Nicolas Frisby Date: Thu, 21 Jul 2022 10:00:45 -0700 Subject: [PATCH 11/11] WIP remove accumulator from CatchHandlerStmFrame --- io-sim/src/Control/Monad/IOSim/Internal.hs | 50 ++++++++++--------- io-sim/src/Control/Monad/IOSim/Types.hs | 1 - io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 8 +-- 3 files changed, 31 insertions(+), 28 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index a4507da8..17e425f5 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -73,7 +73,7 @@ import qualified Deque.Strict as Deque import GHC.Exts (fromList) import Control.Exception (NonTermination (..), assert, throw) -import Control.Monad (join, when, forM_) +import Control.Monad (join, when) import Control.Monad.ST.Lazy import Control.Monad.ST.Lazy.Unsafe (unsafeIOToST, unsafeInterleaveST) import Data.STRef.Lazy @@ -836,23 +836,26 @@ data StmControl s a where unwindControlStmStack :: forall s a. SomeException -> StmControl s a - -> Either Bool (StmControl s a) + -> Either Bool + ( StmControl s a + , [Map TVarId (SomeTVar s)] + ) unwindControlStmStack e (StmControl _ frame) = unwindFrame [] frame where - unwindFrame :: forall s' b. [Map TVarId (SomeTVar s')] -> StmStack s' b a -> Either Bool (StmControl s' a) + unwindFrame :: forall s' b. [Map TVarId (SomeTVar s')] -> StmStack s' b a -> Either Bool (StmControl s' a, [Map TVarId (SomeTVar s')]) unwindFrame _ AtomicallyFrame = Left True unwindFrame ws (OrElseLeftFrame _ _ w _ _ ctl) = unwindFrame (w:ws) ctl unwindFrame ws (OrElseRightFrame _ w _ _ ctl) = unwindFrame (w:ws) ctl - unwindFrame ws (CatchHandlerStmFrame _ _ws' _w _ _ ctl) = unwindFrame ws ctl -- Should not happen + unwindFrame ws (CatchHandlerStmFrame _ _w _ _ ctl) = unwindFrame ws ctl -- Should not happen unwindFrame ws (CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl) = case fromException e of -- Continue to unwind till we find a handler which can handle this exception. Nothing -> unwindFrame (writtenOuter:ws) ctl Just e' -> let action' = handler e' - ctl' = CatchHandlerStmFrame k (reverse ws) writtenOuter writtenOuterSeq createdOuterSeq ctl - in Right $ StmControl action' ctl' + ctl' = CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl + in Right $ (StmControl action' ctl', reverse ws) -- -- Executing STM Transactions @@ -950,25 +953,28 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = -- Skip the orElse right hand and continue with the k continuation go ctl' read written' writtenSeq' createdOuterSeq nextVid (k x) - CatchHandlerStmFrame k ws writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do -- Undo all written tvars !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - -- And all the ones till the catch frame - forM_ ws $ traverse_ (\(SomeTVar tvar) -> revertTVar tvar) go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (k x) - ThrowStm e -> - {-# SCC "execAtomically.go.ThrowStm" #-} - -- Abort if no matching exception is found - let abort = do - -- Revert all the TVar writes - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - k0 $ StmTxAborted [] (toException e) + ThrowStm e -> {-# SCC "execAtomically.go.ThrowStm" #-} do + revertThem written + case unwindControlStmStack e (StmControl action ctl) of - -- Unwind to the nearest matching exception - in case unwindControlStmStack e (StmControl action ctl) of - Right (StmControl action' ctl') -> go ctl' read written writtenSeq createdSeq nextVid action' - _ -> abort + -- Unwind to the nearest matching exception + Right (StmControl action' ctl', ws) -> do + mapM_ revertThem ws + go ctl' read written writtenSeq createdSeq nextVid action' + + -- Abort if no matching exception is found + Left{} -> + k0 $ StmTxAborted [] (toException e) + + -- Revert all the TVar writes + where + revertThem x = + traverse_ (\(SomeTVar tvar) -> revertTVar tvar) x CatchStm act handler k -> {-# SCC "execAtomically.go.CatchStm" #-} do @@ -1007,12 +1013,10 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry - CatchHandlerStmFrame _k ws writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + CatchHandlerStmFrame _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.catchHandlerStmFrame" #-} do -- Undo all written tvars !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - -- And all the ones till the catch frame - forM_ ws $ traverse_ (\(SomeTVar tvar) -> revertTVar tvar) go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry OrElse a b k -> diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index dd59c649..91f2d935 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -890,7 +890,6 @@ data StmStack s b a where -- | A continuation frame CatchHandlerStmFrame :: (b -> StmA s c) -- subsequent continuation - -> [Map TVarId (SomeTVar s)] -- All written vars between `throw` and `catch` -> Map TVarId (SomeTVar s) -- saved written vars set -> [SomeTVar s] -- saved written vars list -> [SomeTVar s] -- created vars list (allocations) diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 7b5ea847..22d4efa3 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1055,14 +1055,14 @@ unwindControlStmStack e (StmControl _ frame) = unwindFrame frame unwindFrame AtomicallyFrame = Left True unwindFrame (OrElseLeftFrame _ _ _ _ _ ctl) = unwindFrame ctl unwindFrame (OrElseRightFrame _ _ _ _ ctl) = unwindFrame ctl - unwindFrame (CatchHandlerStmFrame _ _ _ _ _ ctl) = unwindFrame ctl + unwindFrame (CatchHandlerStmFrame _ _ _ _ ctl) = unwindFrame ctl unwindFrame (CatchStmFrame handler k writtenOuter writtenOuterSeq createdOuterSeq ctl) = case fromException e of -- Continue to unwind till we find a handler which can handle this exception. Nothing -> unwindFrame ctl Just e' -> let action' = handler e' - ctl' = CatchHandlerStmFrame k [] writtenOuter writtenOuterSeq createdOuterSeq ctl + ctl' = CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl in Right $ StmControl action' ctl' -- @@ -1156,7 +1156,7 @@ execAtomically time tid tlbl nextVid0 action0 k0 = createdSeq' = createdSeq ++ createdOuterSeq go ctl' read written' writtenSeq' createdSeq' nextVid (k x) - CatchHandlerStmFrame k [] writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do + CatchHandlerStmFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do !_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar) (Map.intersection written writtenOuter) let written' = Map.union written writtenOuter @@ -1217,7 +1217,7 @@ execAtomically time tid tlbl nextVid0 action0 k0 = !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry - CatchHandlerStmFrame _k [] writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + CatchHandlerStmFrame _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.catchHandlerStmFrame" #-} do -- Revert all the TVar writes within this catch action branch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written