From 7c22a2ac765e4e62c02ea1b7f9e33796e039c5ef Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Mon, 29 Aug 2022 10:58:39 +0530 Subject: [PATCH 01/11] Add catch semantics to STM Add catch handler as branch to support catch --- io-sim/src/Control/Monad/IOSim/Internal.hs | 29 +++++++++++++++++-- io-sim/src/Control/Monad/IOSim/Types.hs | 28 ++++++++++++++++-- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 28 ++++++++++++++++-- io-sim/test/Test/STM.hs | 1 + 4 files changed, 77 insertions(+), 9 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index f5c684be..76e1c331 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -899,10 +899,33 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = go ctl' read written' writtenSeq' createdSeq' nextVid (k x) ThrowStm e -> + {-# SCC "execAtomically.go.ThrowStm" #-} + case ctl of + AtomicallyFrame -> do + -- Revert all the TVar writes + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + k0 $ StmTxAborted [] (toException e) + + BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.branchFrame" #-} do + -- Revert all the TVar writes within this orElse + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + -- Execute the catch handler with an empty written set + let ctl'' = BranchFrame EmptyStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' + go ctl'' read Map.empty [] [] nextVid (h e) + -- + BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.branchFrame" #-} do + -- Revert all the TVar writes within this orElse + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) + + CatchStm a h k -> {-# SCC "execAtomically.go.ThrowStm" #-} do - -- Revert all the TVar writes - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - k0 $ StmTxAborted [] (toException e) + -- Execute the left side in a new frame with an empty written set + let ctl' = BranchFrame (CatchStmA h) k written writtenSeq createdSeq ctl + go ctl' read Map.empty [] [] nextVid a + Retry -> {-# SCC "execAtomically.go.Retry" #-} diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index 951bb681..48a690b4 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -177,6 +177,7 @@ runSTM (STM k) = k ReturnStm data StmA s a where ReturnStm :: a -> StmA s a ThrowStm :: SomeException -> StmA s a + CatchStm :: StmA s a -> (SomeException -> StmA s a) -> (a -> StmA s b) -> StmA s b NewTVar :: Maybe String -> x -> (TVar s x -> StmA s b) -> StmA s b LabelTVar :: String -> TVar s a -> StmA s b -> StmA s b @@ -315,6 +316,25 @@ 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 + where + handler' e = case fromException e of + Nothing -> throwIO e -- Rethrow the exception if handler does not handle it. + Just e' -> handler e' + + 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 + catch = MonadThrow.catch + instance MonadCatch (IOSim s) where catch action handler = IOSim $ oneShot $ \k -> Catch (runIOSim action) (runIOSim . handler) k @@ -846,9 +866,11 @@ data StmTxResult s a = | StmTxAborted [SomeTVar s] SomeException --- | OrElse/Catch give rise to an alternate right hand side branch. A right branch --- can be a NoOp -data BranchStmA s a = OrElseStmA (StmA s a) | NoOpStmA +-- | OrElse/Catch give rise to an alternate branch. A branch of a branch is an +-- empty one. +data BranchStmA s a = OrElseStmA (StmA s a) + | CatchStmA (SomeException -> StmA s a) + | NoOpStmA data StmStack s b a where -- | Executing in the context of a top level 'atomically'. diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 18894af2..fda67156 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1110,10 +1110,32 @@ execAtomically time tid tlbl nextVid0 action0 k0 = go ctl' read written' writtenSeq' createdSeq' nextVid (k x) ThrowStm e -> + {-# SCC "execAtomically.go.ThrowStm" #-} + case ctl of + AtomicallyFrame -> do + -- Revert all the TVar writes + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + k0 $ StmTxAborted [] (toException e) + + BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.branchFrame" #-} do + -- Revert all the TVar writes within this orElse + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + -- Execute the catch handler with an empty written set + let ctl'' = BranchFrame EmptyStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' + go ctl'' read Map.empty [] [] nextVid (h e) + -- + BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.branchFrame" #-} do + -- Revert all the TVar writes within this orElse + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) + + CatchStm a h k -> {-# SCC "execAtomically.go.ThrowStm" #-} do - -- Revert all the TVar writes - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - k0 $ StmTxAborted (Map.elems read) (toException e) + -- Execute the left side in a new frame with an empty written set + let ctl' = BranchFrame (CatchStmA h) k written writtenSeq createdSeq ctl + go ctl' read Map.empty [] [] nextVid a Retry -> {-# SCC "execAtomically.go.Retry" #-} diff --git a/io-sim/test/Test/STM.hs b/io-sim/test/Test/STM.hs index 27b5d5a5..3121ffb9 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 -> Expr a -> Term t -> Term t Retry :: Term t ReadTVar :: Name (TyVar t) -> Term t From ba46a954cf99476fd577e50f914dc85d6e837c5c Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Tue, 2 Aug 2022 12:02:12 +0530 Subject: [PATCH 02/11] Add Catch term to reference STM evaluation --- io-sim/test/Test/IOSim.hs | 2 +- io-sim/test/Test/STM.hs | 48 +++++++++++++++++++++++++++++++++++---- 2 files changed, 45 insertions(+), 5 deletions(-) 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 3121ffb9..a3dcef88 100644 --- a/io-sim/test/Test/STM.hs +++ b/io-sim/test/Test/STM.hs @@ -67,7 +67,7 @@ data Term (t :: Type) where Return :: Expr t -> Term t Throw :: Expr a -> Term t - Catch :: Term t -> Expr a -> Term t -> Term t + Catch :: Term t -> Term t -> Term t Retry :: Term t ReadTVar :: Name (TyVar t) -> Term t @@ -310,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[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 U allocs', allocs U 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 @@ -438,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) @@ -452,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 @@ -492,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') @@ -658,7 +684,7 @@ genTerm env tyrep = Nothing) ] - binTerm = frequency [ (2, bindTerm), (1, orElseTerm)] + binTerm = frequency [ (2, bindTerm), (1, orElseTerm), (1, catchTerm)] bindTerm = sized $ \sz -> do @@ -676,6 +702,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' @@ -714,6 +745,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 _ -> [] @@ -739,6 +773,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 @@ -769,6 +804,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 @@ -779,6 +815,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 @@ -791,6 +828,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 36ea45ff1a37302dcdeefd1a56ecbf44894f1348 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Tue, 2 Aug 2022 15:19:55 +0530 Subject: [PATCH 03/11] Stylish-Haskell formatting fix --- io-sim/src/Control/Monad/IOSim/Internal.hs | 8 ++++---- io-sim/src/Control/Monad/IOSim/Types.hs | 2 +- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 6 +++--- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 76e1c331..2dd9d763 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -900,7 +900,7 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = ThrowStm e -> {-# SCC "execAtomically.go.ThrowStm" #-} - case ctl of + case ctl of AtomicallyFrame -> do -- Revert all the TVar writes !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written @@ -913,19 +913,19 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = -- Execute the catch handler with an empty written set let ctl'' = BranchFrame EmptyStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' go ctl'' read Map.empty [] [] nextVid (h e) - -- + -- BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.branchFrame" #-} do -- Revert all the TVar writes within this orElse !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) - CatchStm a h k -> + CatchStm a h k -> {-# SCC "execAtomically.go.ThrowStm" #-} do -- Execute the left side in a new frame with an empty written set let ctl' = BranchFrame (CatchStmA h) k written writtenSeq createdSeq ctl go ctl' read Map.empty [] [] nextVid a - + Retry -> {-# SCC "execAtomically.go.Retry" #-} diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index 48a690b4..5972641c 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -319,7 +319,7 @@ instance Exceptions.MonadThrow (STM s) where instance MonadCatch (STM s) where catch action handler = STM $ oneShot $ \k -> CatchStm (runSTM action) (runSTM . handler') k - where + where handler' e = case fromException e of Nothing -> throwIO e -- Rethrow the exception if handler does not handle it. Just e' -> handler e' diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index fda67156..c9a3198b 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1111,7 +1111,7 @@ execAtomically time tid tlbl nextVid0 action0 k0 = ThrowStm e -> {-# SCC "execAtomically.go.ThrowStm" #-} - case ctl of + case ctl of AtomicallyFrame -> do -- Revert all the TVar writes !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written @@ -1124,14 +1124,14 @@ execAtomically time tid tlbl nextVid0 action0 k0 = -- Execute the catch handler with an empty written set let ctl'' = BranchFrame EmptyStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' go ctl'' read Map.empty [] [] nextVid (h e) - -- + -- BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.branchFrame" #-} do -- Revert all the TVar writes within this orElse !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) - CatchStm a h k -> + CatchStm a h k -> {-# SCC "execAtomically.go.ThrowStm" #-} do -- Execute the left side in a new frame with an empty written set let ctl' = BranchFrame (CatchStmA h) k written writtenSeq createdSeq ctl From a69e4ac37506329b907e353178741439266982a5 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Mon, 29 Aug 2022 11:02:28 +0530 Subject: [PATCH 04/11] Add a correct cost center name, and comments. --- io-sim/src/Control/Monad/IOSim/Internal.hs | 8 ++++---- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 2dd9d763..0a0bf2b5 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -907,16 +907,16 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = k0 $ StmTxAborted [] (toException e) BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> - {-# SCC "execAtomically.go.branchFrame" #-} do - -- Revert all the TVar writes within this orElse + {-# SCC "execAtomically.go.BranchFrame" #-} do + -- Revert all the TVar writes within this catch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written -- Execute the catch handler with an empty written set let ctl'' = BranchFrame EmptyStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' go ctl'' read Map.empty [] [] nextVid (h e) -- BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> - {-# SCC "execAtomically.go.branchFrame" #-} do - -- Revert all the TVar writes within this orElse + {-# SCC "execAtomically.go.BranchFrame" #-} do + -- Revert all the TVar writes within this branch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index c9a3198b..4d0a8da2 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1118,16 +1118,16 @@ execAtomically time tid tlbl nextVid0 action0 k0 = k0 $ StmTxAborted [] (toException e) BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> - {-# SCC "execAtomically.go.branchFrame" #-} do - -- Revert all the TVar writes within this orElse + {-# SCC "execAtomically.go.BranchFrame" #-} do + -- Revert all the TVar writes within this catch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written -- Execute the catch handler with an empty written set let ctl'' = BranchFrame EmptyStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' go ctl'' read Map.empty [] [] nextVid (h e) -- BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> - {-# SCC "execAtomically.go.branchFrame" #-} do - -- Revert all the TVar writes within this orElse + {-# SCC "execAtomically.go.BranchFrame" #-} do + -- Revert all the TVar writes within this branch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) From 06b61ea595e22a08e7de0cb79dd794b02c40b59c Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Mon, 29 Aug 2022 11:26:53 +0530 Subject: [PATCH 05/11] Fix builder errors --- io-sim/src/Control/Monad/IOSim/Internal.hs | 2 +- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 0a0bf2b5..8ac04123 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -911,7 +911,7 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = -- Revert all the TVar writes within this catch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written -- Execute the catch handler with an empty written set - let ctl'' = BranchFrame EmptyStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' + let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' go ctl'' read Map.empty [] [] nextVid (h e) -- BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 4d0a8da2..e1e7abb1 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1122,7 +1122,7 @@ execAtomically time tid tlbl nextVid0 action0 k0 = -- Revert all the TVar writes within this catch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written -- Execute the catch handler with an empty written set - let ctl'' = BranchFrame EmptyStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' + let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' go ctl'' read Map.empty [] [] nextVid (h e) -- BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> From 0b1cb71e2a996eef0bd64a1c3de0c038f85b7c41 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Mon, 29 Aug 2022 19:13:30 +0530 Subject: [PATCH 06/11] Update comments - Pass read to IOSim --- io-sim/src/Control/Monad/IOSim/Internal.hs | 8 +++++--- io-sim/src/Control/Monad/IOSim/Types.hs | 10 +++++++--- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 3 +-- io-sim/test/Test/IOSim.hs | 2 +- io-sim/test/Test/STM.hs | 14 +++++++------- 5 files changed, 21 insertions(+), 16 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 8ac04123..5f5325bb 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -904,13 +904,15 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = AtomicallyFrame -> do -- Revert all the TVar writes !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - k0 $ StmTxAborted [] (toException e) + k0 $ StmTxAborted (Map.elems read) (toException e) BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.BranchFrame" #-} do - -- Revert all the TVar writes within this catch + -- Execute the catch handler with an empty written set. + -- Rollback `TVar`s written since catch handler was installed + -- but preserve ones that were set prior to it, as specified in the + -- [stm](https://hackage.haskell.org/package/stm/docs/Control-Monad-STM.html#v:catchSTM) package. !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - -- Execute the catch handler with an empty written set let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' go ctl'' read Map.empty [] [] nextVid (h e) -- diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index 5972641c..7263a64a 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -316,14 +316,18 @@ 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 + catch action handler = STM $ oneShot $ \k -> CatchStm (runSTM action) (runSTM . fromHandler handler) k where - handler' e = case fromException e of + -- Get a total handler from the given handler + fromHandler :: Exception e => (e -> STM s a) -> SomeException -> STM s a + fromHandler h e = case fromException e of Nothing -> throwIO e -- Rethrow the exception if handler does not handle it. - Just e' -> handler e' + Just e' -> h e' + -- No need to consider masking for STM generalBracket acquire release use = do resource <- acquire b <- use resource `catch` \e -> do diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index e1e7abb1..89b1e73e 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1115,13 +1115,12 @@ execAtomically time tid tlbl nextVid0 action0 k0 = AtomicallyFrame -> do -- Revert all the TVar writes !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - k0 $ StmTxAborted [] (toException e) + k0 $ StmTxAborted (Map.elems read) (toException e) BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.BranchFrame" #-} do -- Revert all the TVar writes within this catch !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - -- Execute the catch handler with an empty written set let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' go ctl'' read Map.empty [] [] nextVid (h e) -- diff --git a/io-sim/test/Test/IOSim.hs b/io-sim/test/Test/IOSim.hs index 576f0446..f31cee73 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, LazySTM.MonadSTM m, MonadCatch (LazySTM.STM m)) +prop_stm_referenceM :: (MonadSTM m, MonadCatch (STM m), MonadCatch 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 a3dcef88..d8e4c692 100644 --- a/io-sim/test/Test/STM.hs +++ b/io-sim/test/Test/STM.hs @@ -297,7 +297,7 @@ deriving instance Show (NfTerm t) -- | The STM transition rules. They reduce a 'Term' to a normal-form 'NfTerm'. -- -- Compare the implementation of this against the operational semantics in --- Figure 4 in the paper. Note that @catch@ is not included. +-- Figure 4 in the paper including the `Catch` semantics from the Appendix A. -- evalTerm :: Env -> Heap -> Allocs -> Term t -> (NfTerm t, Heap, Allocs) evalTerm !env !heap !allocs term = case term of @@ -319,13 +319,13 @@ evalTerm !env !heap !allocs term = case term of -- M; heap, {} => return P; heap', allocs' -- -------------------------------------------------------- -- S[catch M N]; heap, allocs => S[return P]; heap', allocs' - NfReturn v -> (NfReturn v, heap', allocs `mappend` allocs') + NfReturn v -> (NfReturn v, heap', allocs <> allocs') -- Rule XSTM2 -- M; heap, {} => throw 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 + NfThrow _ -> evalTerm env (heap <> allocs') (allocs <> allocs') t2 -- Rule XSTM3 -- M; heap, {} => retry; heap', allocs' @@ -462,7 +462,7 @@ extendExecEnv (Name name _tyrep) v (ExecEnv env) = -- | Execute an STM 'Term' in the 'STM' monad. -- -execTerm :: (MonadSTM m, MonadThrow (STM m), MonadCatch (STM m)) +execTerm :: (MonadSTM m, MonadCatch (STM m)) => ExecEnv m -> Term t -> STM m (ExecValue m t) @@ -518,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, MonadCatch (STM m)) +execAtomically :: forall m t. (MonadSTM m, MonadCatch (STM m), MonadCatch m) => Term t -> m TxResult execAtomically t = toTxResult <$> try (atomically action') @@ -698,12 +698,12 @@ genTerm env tyrep = return (Bind t1 name t2) orElseTerm = - sized $ \sz -> resize (sz `div` 2) $ + scale (`div` 2) $ OrElse <$> genTerm env tyrep <*> genTerm env tyrep catchTerm = - sized $ \sz -> resize (sz `div` 2) $ + scale (`div` 2) $ Catch <$> genTerm env tyrep <*> genTerm env tyrep From 5925b6a908094bac3442d4511108d32f80db5c03 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Mon, 29 Aug 2022 19:38:49 +0530 Subject: [PATCH 07/11] Prefer generic liftShrink2 --- io-sim/test/Test/STM.hs | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/io-sim/test/Test/STM.hs b/io-sim/test/Test/STM.hs index d8e4c692..047a7b64 100644 --- a/io-sim/test/Test/STM.hs +++ b/io-sim/test/Test/STM.hs @@ -746,8 +746,7 @@ shrinkTerm t = 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 ] + ++ [Catch t1' t2' | (t1', t2') <- liftShrink2 shrinkTerm shrinkTerm (t1, t2)] Retry -> [] ReadTVar _ -> [] @@ -756,12 +755,10 @@ shrinkTerm t = NewTVar e -> [NewTVar e' | e' <- shrinkExpr e] Bind t1 n t2 -> [ t2 | nameId n `Set.notMember` freeNamesTerm t2 ] - ++ [ Bind t1' n t2 | t1' <- shrinkTerm t1 ] - ++ [ Bind t1 n t2' | t2' <- shrinkTerm t2 ] + ++ [ Bind t1' n t2' | (t1', t2') <- liftShrink2 shrinkTerm shrinkTerm (t1, t2) ] OrElse t1 t2 -> [t1, t2] - ++ [ OrElse t1' t2 | t1' <- shrinkTerm t1 ] - ++ [ OrElse t1 t2' | t2' <- shrinkTerm t2 ] + ++ [ OrElse t1' t2' | (t1', t2') <- liftShrink2 shrinkTerm shrinkTerm (t1, t2) ] shrinkExpr :: Expr t -> [Expr t] shrinkExpr ExprUnit = [] From 04554576849ca9d0b7bb48d3ee9cb0a2ae3f5c2c Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Tue, 30 Aug 2022 10:27:03 +0530 Subject: [PATCH 08/11] Fix stylish haskell error --- io-sim/test/Test/STM.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/io-sim/test/Test/STM.hs b/io-sim/test/Test/STM.hs index 047a7b64..60c3e901 100644 --- a/io-sim/test/Test/STM.hs +++ b/io-sim/test/Test/STM.hs @@ -325,13 +325,13 @@ evalTerm !env !heap !allocs term = case term of -- M; heap, {} => throw P; heap', allocs' -- -------------------------------------------------------- -- S[catch M N]; heap, allocs => S[N P]; heap U allocs', allocs U allocs' - NfThrow _ -> evalTerm env (heap <> allocs') (allocs <> allocs') t2 + NfThrow _ -> evalTerm env (heap <> allocs') (allocs <> allocs') t2 -- Rule XSTM3 -- M; heap, {} => retry; heap', allocs' -- -------------------------------------------------------- -- S[catch M N]; heap, allocs => S[retry]; heap, allocs - NfRetry -> (NfRetry, heap, allocs) + NfRetry -> (NfRetry, heap, allocs) Retry -> (NfRetry, heap, allocs) From 0d1760454f9312fcd7b603aafc54d5ea43998577 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Mon, 12 Sep 2022 16:54:36 +0530 Subject: [PATCH 09/11] Refactor and add comments - De-duplicate source code - Add comments refering to STM semantics reference --- io-sim/src/Control/Monad/IOSim/Internal.hs | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index 5015c71d..de655fe3 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -899,32 +899,28 @@ 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" #-} do + -- Rollback `TVar`s written since catch handler was installed + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written case ctl of AtomicallyFrame -> do - -- Revert all the TVar writes - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written k0 $ StmTxAborted (Map.elems read) (toException e) BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.BranchFrame" #-} do - -- Execute the catch handler with an empty written set. - -- Rollback `TVar`s written since catch handler was installed - -- but preserve ones that were set prior to it, as specified in the - -- [stm](https://hackage.haskell.org/package/stm/docs/Control-Monad-STM.html#v:catchSTM) package. - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + -- Execute the left side in a new frame with an empty written set let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' go ctl'' read Map.empty [] [] nextVid (h e) -- BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.BranchFrame" #-} do - -- Revert all the TVar writes within this branch - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) CatchStm a h k -> {-# SCC "execAtomically.go.ThrowStm" #-} do - -- Execute the left side in a new frame with an empty written set + -- Execute the catch handler with an empty written set. + -- but preserve ones that were set prior to it, as specified in the + -- [stm](https://hackage.haskell.org/package/stm/docs/Control-Monad-STM.html#v:catchSTM) package. let ctl' = BranchFrame (CatchStmA h) k written writtenSeq createdSeq ctl go ctl' read Map.empty [] [] nextVid a From 5c283339694145a05f70631098702d41a8436e16 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Thu, 6 Oct 2022 14:29:34 +0530 Subject: [PATCH 10/11] Refactor code - Remove redundancy between subbranches --- io-sim/src/Control/Monad/IOSim/Internal.hs | 3 +- io-sim/src/Control/Monad/IOSim/Types.hs | 4 +- io-sim/src/Control/Monad/IOSimPOR/Internal.hs | 54 +++++++++---------- 3 files changed, 27 insertions(+), 34 deletions(-) diff --git a/io-sim/src/Control/Monad/IOSim/Internal.hs b/io-sim/src/Control/Monad/IOSim/Internal.hs index bfb7b3ec..2ae72dd6 100644 --- a/io-sim/src/Control/Monad/IOSim/Internal.hs +++ b/io-sim/src/Control/Monad/IOSim/Internal.hs @@ -952,8 +952,7 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 = Retry -> - {-# SCC "execAtomically.go.Retry" #-} - do + {-# SCC "execAtomically.go.Retry" #-} do -- Always revert all the TVar writes for the retry !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written case ctl of diff --git a/io-sim/src/Control/Monad/IOSim/Types.hs b/io-sim/src/Control/Monad/IOSim/Types.hs index 01f00e50..916ce0cb 100644 --- a/io-sim/src/Control/Monad/IOSim/Types.hs +++ b/io-sim/src/Control/Monad/IOSim/Types.hs @@ -881,8 +881,8 @@ data StmTxResult s a = | StmTxAborted [SomeTVar s] SomeException --- | OrElse/Catch give rise to an alternate branch. A branch of a branch is an --- empty one. +-- | OrElse/Catch give rise to an alternate branch. +-- A branch of a branch is an empty one. data BranchStmA s a = OrElseStmA (StmA s a) | CatchStmA (SomeException -> StmA s a) | NoOpStmA diff --git a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs index 40d91455..c913bda1 100644 --- a/io-sim/src/Control/Monad/IOSimPOR/Internal.hs +++ b/io-sim/src/Control/Monad/IOSimPOR/Internal.hs @@ -1171,24 +1171,20 @@ 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" #-} do + -- Revert all the TVar writes + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written case ctl of AtomicallyFrame -> do - -- Revert all the TVar writes - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written k0 $ StmTxAborted (Map.elems read) (toException e) BranchFrame (CatchStmA h) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.BranchFrame" #-} do - -- Revert all the TVar writes within this catch - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' go ctl'' read Map.empty [] [] nextVid (h e) -- BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> {-# SCC "execAtomically.go.BranchFrame" #-} do - -- Revert all the TVar writes within this branch - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid (ThrowStm e) CatchStm a h k -> @@ -1198,29 +1194,27 @@ execAtomically time tid tlbl nextVid0 action0 k0 = go ctl' read Map.empty [] [] nextVid a Retry -> - {-# SCC "execAtomically.go.Retry" #-} - do - -- Always revert all the TVar writes for the retry - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - case ctl of - AtomicallyFrame -> do - -- Return vars read, so the thread can block on them - k0 $! StmTxBlocked $! Map.elems read - - BranchFrame (OrElseStmA b) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> - {-# SCC "execAtomically.go.BranchFrame.OrElseStmA" #-} do - !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written - -- Execute the orElse right hand with an empty written set - let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' - go ctl'' read Map.empty [] [] nextVid b - - BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> - {-# SCC "execAtomically.go.BranchFrame" #-} do - -- Retry makes sense only within a OrElse context. If it is a branch other than - -- OrElse left side, then bubble up the `retry` to the frame above. - -- Skip the continuation and propagate the retry into the outer frame - -- using the written set for the outer frame - go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry + {-# SCC "execAtomically.go.Retry" #-} do + -- Always revert all the TVar writes for the retry + !_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written + case ctl of + AtomicallyFrame -> do + -- Return vars read, so the thread can block on them + k0 $! StmTxBlocked $! Map.elems read + + BranchFrame (OrElseStmA b) k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.BranchFrame.OrElseStmA" #-} do + -- Execute the orElse right hand with an empty written set + let ctl'' = BranchFrame NoOpStmA k writtenOuter writtenOuterSeq createdOuterSeq ctl' + go ctl'' read Map.empty [] [] nextVid b + + BranchFrame _ _k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> + {-# SCC "execAtomically.go.BranchFrame" #-} do + -- Retry makes sense only within a OrElse context. If it is a branch other than + -- OrElse left side, then bubble up the `retry` to the frame above. + -- Skip the continuation and propagate the retry into the outer frame + -- using the written set for the outer frame + go ctl' read writtenOuter writtenOuterSeq createdOuterSeq nextVid Retry OrElse a b k -> {-# SCC "execAtomically.go.OrElse" #-} do From 20837e04cf00f5223fde7c1b69bccaa8bc8c4002 Mon Sep 17 00:00:00 2001 From: Yogesh Sajanikar Date: Thu, 6 Oct 2022 15:25:14 +0530 Subject: [PATCH 11/11] Add exception handler for evaluator/exec - ImmValInt 0 is treated as an exception, and is the only value handled as an exception. Otherwise the exception is rethrown. --- io-sim/test/Test/STM.hs | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) diff --git a/io-sim/test/Test/STM.hs b/io-sim/test/Test/STM.hs index ccf4d6dc..b9afd6df 100644 --- a/io-sim/test/Test/STM.hs +++ b/io-sim/test/Test/STM.hs @@ -24,7 +24,7 @@ module Test.STM where import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map -import Data.Maybe (fromMaybe, maybeToList) +import Data.Maybe import Data.Set (Set) import qualified Data.Set as Set import Data.Type.Equality @@ -68,7 +68,7 @@ data Term (t :: Type) where Return :: Expr t -> Term t Throw :: Expr a -> Term t - Catch :: Term t -> Term t -> Term t + Catch :: Term t -> SomeException -> Term t -> Term t Retry :: Term t ReadTVar :: Name (TyVar t) -> Term t @@ -268,6 +268,7 @@ data ImmValue where ImmValVar :: ImmValue -> ImmValue deriving (Eq, Show) + -- | In the execution in real STM transactions are aborted by throwing an -- exception. -- @@ -313,7 +314,7 @@ evalTerm !env !heap !allocs term = case term of -- Exception semantics are detailed in "Appendix A Exception semantics" p 12-13 of -- - Catch t1 t2 -> + Catch t1 exc t2 -> let (nf1, heap', allocs') = evalTerm env heap mempty t1 in case nf1 of -- Rule XSTM1 @@ -326,7 +327,14 @@ evalTerm !env !heap !allocs term = case term of -- M; heap, {} => throw P; heap', allocs' -- -------------------------------------------------------- -- S[catch M N]; heap, allocs => S[N P]; heap U allocs', allocs U allocs' - NfThrow _ -> evalTerm env (heap <> allocs') (allocs <> allocs') t2 + NfThrow v -> + -- v should be compared to exception + case fromException exc of + -- TODO: Add eqValue for value + Just (ImmValInt 0) -> + evalTerm env (heap <> allocs') (allocs <> allocs') t2 + -- Exception is not handled, bubble it up + _otherwise -> (NfThrow v, heap, allocs) -- Rule XSTM3 -- M; heap, {} => retry; heap', allocs' @@ -477,7 +485,7 @@ execTerm env t = let e' = execExpr env e throwSTM =<< snapshotExecValue e' - Catch t1 t2 -> execTerm env t1 `catch` \(_ :: ImmValue) -> execTerm env t2 + Catch t1 _ t2 -> execTerm env t1 `catch` \(_ :: ImmValue) -> execTerm env t2 Retry -> retry @@ -706,6 +714,7 @@ genTerm env tyrep = catchTerm = scale (`div` 2) $ Catch <$> genTerm env tyrep + <*> pure (toException $ ImmValInt 0) -- TODO: 0 is treated as an exception value, generalize it later <*> genTerm env tyrep genSomeExpr :: GenEnv -> Gen SomeExpr @@ -746,8 +755,8 @@ 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', t2') <- liftShrink2 shrinkTerm shrinkTerm (t1, t2)] + Catch t1 exc t2 -> [t1, t2] + ++ [Catch t1' exc t2' | (t1', t2') <- liftShrink2 shrinkTerm shrinkTerm (t1, t2)] Retry -> [] ReadTVar _ -> [] @@ -771,7 +780,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 (Catch t1 exc 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 @@ -802,7 +811,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 (Catch a _ b) = 1 + termSize a + termSize b termSize Retry{} = 1 termSize ReadTVar{} = 1 termSize WriteTVar{} = 1 @@ -813,7 +822,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 (Catch a _ b) = 1 + max (termDepth a) (termDepth b) termDepth Retry{} = 1 termDepth ReadTVar{} = 1 termDepth WriteTVar{} = 1 @@ -826,7 +835,7 @@ 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 p (Catch t1 _ t2) = showParen (p > 9) $ showTerm 10 t1 . showString " `catch` " . showTerm 10 t2 showTerm _ Retry = showString "retry"