Skip to content

CAD-4750 generalise OrElse frame #15

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Aug 24, 2022
Merged

CAD-4750 generalise OrElse frame #15

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
63 changes: 25 additions & 38 deletions io-sim/src/Control/Monad/IOSim/Internal.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -881,21 +881,9 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 =
(mapMaybe traceString $ ds ++ ds')
nextVid

OrElseLeftFrame _b k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do
-- Commit the TVars written in this sub-transaction that are also
-- in the written set of the outer transaction
!_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar)
(Map.intersection written writtenOuter)
-- Merge the written set of the inner with the outer
let written' = Map.union written writtenOuter
writtenSeq' = filter (\(SomeTVar tvar) ->
tvarId tvar `Map.notMember` writtenOuter)
writtenSeq
++ writtenOuterSeq
-- Skip the orElse right hand and continue with the k continuation
go ctl' read written' writtenSeq' createdOuterSeq nextVid (k x)

OrElseRightFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do
BranchFrame _b k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do
-- The branch has successfully completed the transaction. Hence,
-- the alternative branch can be ignored.
-- Commit the TVars written in this sub-transaction that are also
-- in the written set of the outer transaction
!_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar)
Expand All @@ -907,7 +895,7 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 =
writtenSeq
++ writtenOuterSeq
createdSeq' = createdSeq ++ createdOuterSeq
-- Continue with the k continuation
-- Skip the right hand alternative and continue with the k continuation
go ctl' read written' writtenSeq' createdSeq' nextVid (k x)

ThrowStm e ->
Expand All @@ -918,33 +906,32 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 =

Retry ->
{-# SCC "execAtomically.go.Retry" #-}
case ctl of
AtomicallyFrame -> do
-- Revert all the TVar writes
!_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written
-- Return vars read, so the thread can block on them
k0 $! StmTxBlocked $! (Map.elems read)

OrElseLeftFrame b k writtenOuter writtenOuterSeq createdOuterSeq ctl' ->
{-# SCC "execAtomically.go.OrElseLeftFrame" #-} do
-- Revert all the TVar writes within this orElse
!_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written
-- Execute the orElse right hand with an empty written set
let ctl'' = OrElseRightFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl'
go ctl'' read Map.empty [] [] nextVid b

OrElseRightFrame _k writtenOuter writtenOuterSeq createdOuterSeq ctl' ->
{-# SCC "execAtomically.go.OrElseRightFrame" #-} do
-- Revert all the TVar writes within this orElse branch
do
-- Always revert all the TVar writes for the retry
!_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written
-- 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
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
-- Execute the left side in a new frame with an empty written set
let ctl' = OrElseLeftFrame b k written writtenSeq createdSeq ctl
let ctl' = BranchFrame (OrElseStmA b) k written writtenSeq createdSeq ctl
go ctl' read Map.empty [] [] nextVid a

NewTVar !mbLabel x k ->
Expand Down
18 changes: 9 additions & 9 deletions io-sim/src/Control/Monad/IOSim/Types.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ module Control.Monad.IOSim.Types
, runSTM
, StmA (..)
, StmTxResult (..)
, BranchStmA (..)
, StmStack (..)
, Timeout (..)
, TimeoutException (..)
Expand Down Expand Up @@ -844,26 +845,25 @@ 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

data StmStack s b a where
-- | Executing in the context of a top level 'atomically'.
AtomicallyFrame :: StmStack s a a

-- | Executing in the context of the /left/ hand side of an 'orElse'
OrElseLeftFrame :: StmA s a -- orElse right alternative
-- | Executing in the context of the /left/ hand side of a branch.
-- A right branch is represented by a frame containing empty statement.
BranchFrame :: !(BranchStmA s a) -- right alternative, can be empty
-> (a -> StmA s b) -- subsequent continuation
-> Map TVarId (SomeTVar s) -- saved written vars set
-> [SomeTVar s] -- saved written vars list
-> [SomeTVar s] -- created vars list
-> StmStack s b c
-> StmStack s a c

-- | Executing in the context of the /right/ hand side of an 'orElse'
OrElseRightFrame :: (a -> StmA s b) -- subsequent continuation
-> Map TVarId (SomeTVar s) -- saved written vars set
-> [SomeTVar s] -- saved written vars list
-> [SomeTVar s] -- created vars list
-> StmStack s b c
-> StmStack s a c

---
--- Schedules
Expand Down
64 changes: 26 additions & 38 deletions io-sim/src/Control/Monad/IOSimPOR/Internal.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1092,21 +1092,9 @@ execAtomically time tid tlbl nextVid0 action0 k0 =
(mapMaybe traceString $ ds ++ ds')
nextVid

OrElseLeftFrame _b k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do
-- Commit the TVars written in this sub-transaction that are also
-- in the written set of the outer transaction
!_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar)
(Map.intersection written writtenOuter)
-- Merge the written set of the inner with the outer
let written' = Map.union written writtenOuter
writtenSeq' = filter (\(SomeTVar tvar) ->
tvarId tvar `Map.notMember` writtenOuter)
writtenSeq
++ writtenOuterSeq
-- Skip the orElse right hand and continue with the k continuation
go ctl' read written' writtenSeq' createdOuterSeq nextVid (k x)

OrElseRightFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do
BranchFrame _b k writtenOuter writtenOuterSeq createdOuterSeq ctl' -> do
-- The branch has successfully completed the transaction. Hence,
-- the alternative branch can be ignored.
-- Commit the TVars written in this sub-transaction that are also
-- in the written set of the outer transaction
!_ <- traverse_ (\(SomeTVar tvar) -> commitTVar tvar)
Expand All @@ -1118,7 +1106,7 @@ execAtomically time tid tlbl nextVid0 action0 k0 =
writtenSeq
++ writtenOuterSeq
createdSeq' = createdSeq ++ createdOuterSeq
-- Continue with the k continuation
-- Skip the orElse right hand and continue with the k continuation
go ctl' read written' writtenSeq' createdSeq' nextVid (k x)

ThrowStm e ->
Expand All @@ -1129,33 +1117,33 @@ execAtomically time tid tlbl nextVid0 action0 k0 =

Retry ->
{-# SCC "execAtomically.go.Retry" #-}
case ctl of
AtomicallyFrame -> do
-- Revert all the TVar writes
!_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written
-- Return vars read, so the thread can block on them
k0 $! StmTxBlocked $! Map.elems read

OrElseLeftFrame b k writtenOuter writtenOuterSeq createdOuterSeq ctl' ->
{-# SCC "execAtomically.go.OrElseLeftFrame" #-} do
-- Revert all the TVar writes within this orElse
!_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written
-- Execute the orElse right hand with an empty written set
let ctl'' = OrElseRightFrame k writtenOuter writtenOuterSeq createdOuterSeq ctl'
go ctl'' read Map.empty [] [] nextVid b

OrElseRightFrame _k writtenOuter writtenOuterSeq createdOuterSeq ctl' ->
{-# SCC "execAtomically.go.OrElseRightFrame" #-} do
-- Revert all the TVar writes within this orElse branch
do
-- Always revert all the TVar writes for the retry
!_ <- traverse_ (\(SomeTVar tvar) -> revertTVar tvar) written
-- 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
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

OrElse a b k ->
{-# SCC "execAtomically.go.OrElse" #-} do
-- Execute the left side in a new frame with an empty written set
let ctl' = OrElseLeftFrame b k written writtenSeq createdSeq ctl
let ctl' = BranchFrame (OrElseStmA b) k written writtenSeq createdSeq ctl
go ctl' read Map.empty [] [] nextVid a

NewTVar !mbLabel x k ->
Expand Down