mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-18 19:11:37 +03:00
Unify Ref/CRef/Var/MVar naming.
This was a holdover from old-dejafu, where there were CRefs and CVars, so referring to them as "Ref" and "Var" everywhere made sense as a convenient shorthand. But then "CVar" became "MVar" and the convention made less sense.
This commit is contained in:
Michael Walker
parent
12335e0090
commit
300d1d462a
@ -188,42 +188,42 @@ data ThreadAction =
|
||||
-- ^ Set the number of Haskell threads that can run simultaneously.
|
||||
| Yield
|
||||
-- ^ Yield the current thread.
|
||||
| NewVar MVarId
|
||||
| NewMVar MVarId
|
||||
-- ^ Create a new 'MVar'.
|
||||
| PutVar MVarId [ThreadId]
|
||||
| PutMVar MVarId [ThreadId]
|
||||
-- ^ Put into a 'MVar', possibly waking up some threads.
|
||||
| BlockedPutVar MVarId
|
||||
| BlockedPutMVar MVarId
|
||||
-- ^ Get blocked on a put.
|
||||
| TryPutVar MVarId Bool [ThreadId]
|
||||
| TryPutMVar MVarId Bool [ThreadId]
|
||||
-- ^ Try to put into a 'MVar', possibly waking up some threads.
|
||||
| ReadVar MVarId
|
||||
| ReadMVar MVarId
|
||||
-- ^ Read from a 'MVar'.
|
||||
| TryReadVar MVarId Bool
|
||||
| TryReadMVar MVarId Bool
|
||||
-- ^ Try to read from a 'MVar'.
|
||||
| BlockedReadVar MVarId
|
||||
| BlockedReadMVar MVarId
|
||||
-- ^ Get blocked on a read.
|
||||
| TakeVar MVarId [ThreadId]
|
||||
| TakeMVar MVarId [ThreadId]
|
||||
-- ^ Take from a 'MVar', possibly waking up some threads.
|
||||
| BlockedTakeVar MVarId
|
||||
| BlockedTakeMVar MVarId
|
||||
-- ^ Get blocked on a take.
|
||||
| TryTakeVar MVarId Bool [ThreadId]
|
||||
| TryTakeMVar MVarId Bool [ThreadId]
|
||||
-- ^ Try to take from a 'MVar', possibly waking up some threads.
|
||||
| NewRef CRefId
|
||||
| NewCRef CRefId
|
||||
-- ^ Create a new 'CRef'.
|
||||
| ReadRef CRefId
|
||||
| ReadCRef CRefId
|
||||
-- ^ Read from a 'CRef'.
|
||||
| ReadRefCas CRefId
|
||||
| ReadCRefCas CRefId
|
||||
-- ^ Read from a 'CRef' for a future compare-and-swap.
|
||||
| ModRef CRefId
|
||||
| ModCRef CRefId
|
||||
-- ^ Modify a 'CRef'.
|
||||
| ModRefCas CRefId
|
||||
| ModCRefCas CRefId
|
||||
-- ^ Modify a 'CRef' using a compare-and-swap.
|
||||
| WriteRef CRefId
|
||||
| WriteCRef CRefId
|
||||
-- ^ Write to a 'CRef' without synchronising.
|
||||
| CasRef CRefId Bool
|
||||
| CasCRef CRefId Bool
|
||||
-- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising
|
||||
-- it.
|
||||
| CommitRef ThreadId CRefId
|
||||
| CommitCRef ThreadId CRefId
|
||||
-- ^ Commit the last write to the given 'CRef' by the given thread,
|
||||
-- so that all threads can see the updated value.
|
||||
| STM TTrace [ThreadId]
|
||||
@ -265,9 +265,9 @@ data ThreadAction =
|
||||
-- | Check if a @ThreadAction@ immediately blocks.
|
||||
isBlock :: ThreadAction -> Bool
|
||||
isBlock (BlockedThrowTo _) = True
|
||||
isBlock (BlockedTakeVar _) = True
|
||||
isBlock (BlockedReadVar _) = True
|
||||
isBlock (BlockedPutVar _) = True
|
||||
isBlock (BlockedTakeMVar _) = True
|
||||
isBlock (BlockedReadMVar _) = True
|
||||
isBlock (BlockedPutMVar _) = True
|
||||
isBlock (BlockedSTM _) = True
|
||||
isBlock _ = False
|
||||
|
||||
@ -302,36 +302,36 @@ data Lookahead =
|
||||
-- simultaneously.
|
||||
| WillYield
|
||||
-- ^ Will yield the current thread.
|
||||
| WillNewVar
|
||||
| WillNewMVar
|
||||
-- ^ Will create a new 'MVar'.
|
||||
| WillPutVar MVarId
|
||||
| WillPutMVar MVarId
|
||||
-- ^ Will put into a 'MVar', possibly waking up some threads.
|
||||
| WillTryPutVar MVarId
|
||||
| WillTryPutMVar MVarId
|
||||
-- ^ Will try to put into a 'MVar', possibly waking up some threads.
|
||||
| WillReadVar MVarId
|
||||
| WillReadMVar MVarId
|
||||
-- ^ Will read from a 'MVar'.
|
||||
| WillTryReadVar MVarId
|
||||
| WillTryReadMVar MVarId
|
||||
-- ^ Will try to read from a 'MVar'.
|
||||
| WillTakeVar MVarId
|
||||
| WillTakeMVar MVarId
|
||||
-- ^ Will take from a 'MVar', possibly waking up some threads.
|
||||
| WillTryTakeVar MVarId
|
||||
| WillTryTakeMVar MVarId
|
||||
-- ^ Will try to take from a 'MVar', possibly waking up some threads.
|
||||
| WillNewRef
|
||||
| WillNewCRef
|
||||
-- ^ Will create a new 'CRef'.
|
||||
| WillReadRef CRefId
|
||||
| WillReadCRef CRefId
|
||||
-- ^ Will read from a 'CRef'.
|
||||
| WillReadRefCas CRefId
|
||||
| WillReadCRefCas CRefId
|
||||
-- ^ Will read from a 'CRef' for a future compare-and-swap.
|
||||
| WillModRef CRefId
|
||||
| WillModCRef CRefId
|
||||
-- ^ Will modify a 'CRef'.
|
||||
| WillModRefCas CRefId
|
||||
-- ^ Will nodify a 'CRef' using a compare-and-swap.
|
||||
| WillWriteRef CRefId
|
||||
| WillModCRefCas CRefId
|
||||
-- ^ Will modify a 'CRef' using a compare-and-swap.
|
||||
| WillWriteCRef CRefId
|
||||
-- ^ Will write to a 'CRef' without synchronising.
|
||||
| WillCasRef CRefId
|
||||
| WillCasCRef CRefId
|
||||
-- ^ Will attempt to to a 'CRef' using a compare-and-swap,
|
||||
-- synchronising it.
|
||||
| WillCommitRef ThreadId CRefId
|
||||
| WillCommitCRef ThreadId CRefId
|
||||
-- ^ Will commit the last write by the given thread to the 'CRef'.
|
||||
| WillSTM
|
||||
-- ^ Will execute an STM transaction, possibly waking up some
|
||||
@ -371,24 +371,24 @@ rewind MyThreadId = Just WillMyThreadId
|
||||
rewind (GetNumCapabilities _) = Just WillGetNumCapabilities
|
||||
rewind (SetNumCapabilities i) = Just (WillSetNumCapabilities i)
|
||||
rewind Yield = Just WillYield
|
||||
rewind (NewVar _) = Just WillNewVar
|
||||
rewind (PutVar c _) = Just (WillPutVar c)
|
||||
rewind (BlockedPutVar c) = Just (WillPutVar c)
|
||||
rewind (TryPutVar c _ _) = Just (WillTryPutVar c)
|
||||
rewind (ReadVar c) = Just (WillReadVar c)
|
||||
rewind (BlockedReadVar c) = Just (WillReadVar c)
|
||||
rewind (TryReadVar c _) = Just (WillTryReadVar c)
|
||||
rewind (TakeVar c _) = Just (WillTakeVar c)
|
||||
rewind (BlockedTakeVar c) = Just (WillTakeVar c)
|
||||
rewind (TryTakeVar c _ _) = Just (WillTryTakeVar c)
|
||||
rewind (NewRef _) = Just WillNewRef
|
||||
rewind (ReadRef c) = Just (WillReadRef c)
|
||||
rewind (ReadRefCas c) = Just (WillReadRefCas c)
|
||||
rewind (ModRef c) = Just (WillModRef c)
|
||||
rewind (ModRefCas c) = Just (WillModRefCas c)
|
||||
rewind (WriteRef c) = Just (WillWriteRef c)
|
||||
rewind (CasRef c _) = Just (WillCasRef c)
|
||||
rewind (CommitRef t c) = Just (WillCommitRef t c)
|
||||
rewind (NewMVar _) = Just WillNewMVar
|
||||
rewind (PutMVar c _) = Just (WillPutMVar c)
|
||||
rewind (BlockedPutMVar c) = Just (WillPutMVar c)
|
||||
rewind (TryPutMVar c _ _) = Just (WillTryPutMVar c)
|
||||
rewind (ReadMVar c) = Just (WillReadMVar c)
|
||||
rewind (BlockedReadMVar c) = Just (WillReadMVar c)
|
||||
rewind (TryReadMVar c _) = Just (WillTryReadMVar c)
|
||||
rewind (TakeMVar c _) = Just (WillTakeMVar c)
|
||||
rewind (BlockedTakeMVar c) = Just (WillTakeMVar c)
|
||||
rewind (TryTakeMVar c _ _) = Just (WillTryTakeMVar c)
|
||||
rewind (NewCRef _) = Just WillNewCRef
|
||||
rewind (ReadCRef c) = Just (WillReadCRef c)
|
||||
rewind (ReadCRefCas c) = Just (WillReadCRefCas c)
|
||||
rewind (ModCRef c) = Just (WillModCRef c)
|
||||
rewind (ModCRefCas c) = Just (WillModCRefCas c)
|
||||
rewind (WriteCRef c) = Just (WillWriteCRef c)
|
||||
rewind (CasCRef c _) = Just (WillCasCRef c)
|
||||
rewind (CommitCRef t c) = Just (WillCommitCRef t c)
|
||||
rewind (STM _ _) = Just WillSTM
|
||||
rewind (BlockedSTM _) = Just WillSTM
|
||||
rewind Catching = Just WillCatching
|
||||
@ -408,10 +408,10 @@ rewind Subconcurrency = Just WillSubconcurrency
|
||||
willRelease :: Lookahead -> Bool
|
||||
willRelease WillFork = True
|
||||
willRelease WillYield = True
|
||||
willRelease (WillPutVar _) = True
|
||||
willRelease (WillTryPutVar _) = True
|
||||
willRelease (WillTakeVar _) = True
|
||||
willRelease (WillTryTakeVar _) = True
|
||||
willRelease (WillPutMVar _) = True
|
||||
willRelease (WillTryPutMVar _) = True
|
||||
willRelease (WillTakeMVar _) = True
|
||||
willRelease (WillTryTakeMVar _) = True
|
||||
willRelease WillSTM = True
|
||||
willRelease WillThrow = True
|
||||
willRelease (WillSetMasking _ _) = True
|
||||
@ -493,19 +493,19 @@ simplifyAction = maybe UnsynchronisedOther simplifyLookahead . rewind
|
||||
|
||||
-- | Variant of 'simplifyAction' that takes a 'Lookahead'.
|
||||
simplifyLookahead :: Lookahead -> ActionType
|
||||
simplifyLookahead (WillPutVar c) = SynchronisedWrite c
|
||||
simplifyLookahead (WillTryPutVar c) = SynchronisedWrite c
|
||||
simplifyLookahead (WillReadVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillTryReadVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillTakeVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillTryTakeVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillReadRef r) = UnsynchronisedRead r
|
||||
simplifyLookahead (WillReadRefCas r) = UnsynchronisedRead r
|
||||
simplifyLookahead (WillModRef r) = SynchronisedModify r
|
||||
simplifyLookahead (WillModRefCas r) = PartiallySynchronisedModify r
|
||||
simplifyLookahead (WillWriteRef r) = UnsynchronisedWrite r
|
||||
simplifyLookahead (WillCasRef r) = PartiallySynchronisedWrite r
|
||||
simplifyLookahead (WillCommitRef _ r) = PartiallySynchronisedCommit r
|
||||
simplifyLookahead (WillPutMVar c) = SynchronisedWrite c
|
||||
simplifyLookahead (WillTryPutMVar c) = SynchronisedWrite c
|
||||
simplifyLookahead (WillReadMVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillTakeMVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillTryTakeMVar c) = SynchronisedRead c
|
||||
simplifyLookahead (WillReadCRef r) = UnsynchronisedRead r
|
||||
simplifyLookahead (WillReadCRefCas r) = UnsynchronisedRead r
|
||||
simplifyLookahead (WillModCRef r) = SynchronisedModify r
|
||||
simplifyLookahead (WillModCRefCas r) = PartiallySynchronisedModify r
|
||||
simplifyLookahead (WillWriteCRef r) = UnsynchronisedWrite r
|
||||
simplifyLookahead (WillCasCRef r) = PartiallySynchronisedWrite r
|
||||
simplifyLookahead (WillCommitCRef _ r) = PartiallySynchronisedCommit r
|
||||
simplifyLookahead WillSTM = SynchronisedOther
|
||||
simplifyLookahead (WillThrowTo _) = SynchronisedOther
|
||||
simplifyLookahead _ = UnsynchronisedOther
|
||||
@ -568,7 +568,7 @@ data Decision =
|
||||
-- spaces.
|
||||
showTrace :: Trace -> String
|
||||
showTrace trc = intercalate "\n" $ concatMap go trc : strkey where
|
||||
go (_,_,CommitRef _ _) = "C-"
|
||||
go (_,_,CommitCRef _ _) = "C-"
|
||||
go (Start (ThreadId _ i),_,_) = "S" ++ show i ++ "-"
|
||||
go (SwitchTo (ThreadId _ i),_,_) = "P" ++ show i ++ "-"
|
||||
go (Continue,_,_) = "-"
|
||||
|
||||
@ -121,30 +121,30 @@ instance Monad n => C.MonadConc (Conc n r) where
|
||||
|
||||
-- ----------
|
||||
|
||||
newCRefN n a = toConc (\c -> ANewRef n a c)
|
||||
newCRefN n a = toConc (\c -> ANewCRef n a c)
|
||||
|
||||
readCRef ref = toConc (AReadRef ref)
|
||||
readForCAS ref = toConc (AReadRefCas ref)
|
||||
readCRef ref = toConc (AReadCRef ref)
|
||||
readForCAS ref = toConc (AReadCRefCas ref)
|
||||
|
||||
peekTicket' _ = _ticketVal
|
||||
|
||||
writeCRef ref a = toConc (\c -> AWriteRef ref a (c ()))
|
||||
casCRef ref tick a = toConc (ACasRef ref tick a)
|
||||
writeCRef ref a = toConc (\c -> AWriteCRef ref a (c ()))
|
||||
casCRef ref tick a = toConc (ACasCRef ref tick a)
|
||||
|
||||
atomicModifyCRef ref f = toConc (AModRef ref f)
|
||||
modifyCRefCAS ref f = toConc (AModRefCas ref f)
|
||||
atomicModifyCRef ref f = toConc (AModCRef ref f)
|
||||
modifyCRefCAS ref f = toConc (AModCRefCas ref f)
|
||||
|
||||
-- ----------
|
||||
|
||||
newEmptyMVarN n = toConc (\c -> ANewVar n c)
|
||||
newEmptyMVarN n = toConc (\c -> ANewMVar n c)
|
||||
|
||||
putMVar var a = toConc (\c -> APutVar var a (c ()))
|
||||
readMVar var = toConc (AReadVar var)
|
||||
takeMVar var = toConc (ATakeVar var)
|
||||
putMVar var a = toConc (\c -> APutMVar var a (c ()))
|
||||
readMVar var = toConc (AReadMVar var)
|
||||
takeMVar var = toConc (ATakeMVar var)
|
||||
|
||||
tryPutMVar var a = toConc (ATryPutVar var a)
|
||||
tryReadMVar var = toConc (ATryReadVar var)
|
||||
tryTakeMVar var = toConc (ATryTakeVar var)
|
||||
tryPutMVar var a = toConc (ATryPutMVar var a)
|
||||
tryReadMVar var = toConc (ATryReadMVar var)
|
||||
tryTakeMVar var = toConc (ATryTakeMVar var)
|
||||
|
||||
-- ----------
|
||||
|
||||
|
||||
@ -179,94 +179,94 @@ stepThread sched memtype tid action ctx = case action of
|
||||
AYield c -> simple (goto c tid (cThreads ctx)) Yield
|
||||
|
||||
-- create a new @MVar@, using the next 'MVarId'.
|
||||
ANewVar n c -> do
|
||||
ANewMVar n c -> do
|
||||
let (idSource', newmvid) = nextMVId n (cIdSource ctx)
|
||||
ref <- newRef Nothing
|
||||
let mvar = MVar newmvid ref
|
||||
pure $ Right (ctx { cThreads = goto (c mvar) tid (cThreads ctx), cIdSource = idSource' }, Right (NewVar newmvid))
|
||||
pure $ Right (ctx { cThreads = goto (c mvar) tid (cThreads ctx), cIdSource = idSource' }, Right (NewMVar newmvid))
|
||||
|
||||
-- put a value into a @MVar@, blocking the thread until it's empty.
|
||||
APutVar cvar@(MVar cvid _) a c -> synchronised $ do
|
||||
APutMVar cvar@(MVar cvid _) a c -> synchronised $ do
|
||||
(success, threads', woken) <- putIntoMVar cvar a c tid (cThreads ctx)
|
||||
simple threads' $ if success then PutVar cvid woken else BlockedPutVar cvid
|
||||
simple threads' $ if success then PutMVar cvid woken else BlockedPutMVar cvid
|
||||
|
||||
-- try to put a value into a @MVar@, without blocking.
|
||||
ATryPutVar cvar@(MVar cvid _) a c -> synchronised $ do
|
||||
ATryPutMVar cvar@(MVar cvid _) a c -> synchronised $ do
|
||||
(success, threads', woken) <- tryPutIntoMVar cvar a c tid (cThreads ctx)
|
||||
simple threads' $ TryPutVar cvid success woken
|
||||
simple threads' $ TryPutMVar cvid success woken
|
||||
|
||||
-- get the value from a @MVar@, without emptying, blocking the
|
||||
-- thread until it's full.
|
||||
AReadVar cvar@(MVar cvid _) c -> synchronised $ do
|
||||
AReadMVar cvar@(MVar cvid _) c -> synchronised $ do
|
||||
(success, threads', _) <- readFromMVar cvar c tid (cThreads ctx)
|
||||
simple threads' $ if success then ReadVar cvid else BlockedReadVar cvid
|
||||
simple threads' $ if success then ReadMVar cvid else BlockedReadMVar cvid
|
||||
|
||||
-- try to get the value from a @MVar@, without emptying, without
|
||||
-- blocking.
|
||||
ATryReadVar cvar@(MVar cvid _) c -> synchronised $ do
|
||||
ATryReadMVar cvar@(MVar cvid _) c -> synchronised $ do
|
||||
(success, threads', _) <- tryReadFromMVar cvar c tid (cThreads ctx)
|
||||
simple threads' $ TryReadVar cvid success
|
||||
simple threads' $ TryReadMVar cvid success
|
||||
|
||||
-- take the value from a @MVar@, blocking the thread until it's
|
||||
-- full.
|
||||
ATakeVar cvar@(MVar cvid _) c -> synchronised $ do
|
||||
ATakeMVar cvar@(MVar cvid _) c -> synchronised $ do
|
||||
(success, threads', woken) <- takeFromMVar cvar c tid (cThreads ctx)
|
||||
simple threads' $ if success then TakeVar cvid woken else BlockedTakeVar cvid
|
||||
simple threads' $ if success then TakeMVar cvid woken else BlockedTakeMVar cvid
|
||||
|
||||
-- try to take the value from a @MVar@, without blocking.
|
||||
ATryTakeVar cvar@(MVar cvid _) c -> synchronised $ do
|
||||
ATryTakeMVar cvar@(MVar cvid _) c -> synchronised $ do
|
||||
(success, threads', woken) <- tryTakeFromMVar cvar c tid (cThreads ctx)
|
||||
simple threads' $ TryTakeVar cvid success woken
|
||||
simple threads' $ TryTakeMVar cvid success woken
|
||||
|
||||
-- create a new @CRef@, using the next 'CRefId'.
|
||||
ANewRef n a c -> do
|
||||
ANewCRef n a c -> do
|
||||
let (idSource', newcrid) = nextCRId n (cIdSource ctx)
|
||||
ref <- newRef (M.empty, 0, a)
|
||||
let cref = CRef newcrid ref
|
||||
pure $ Right (ctx { cThreads = goto (c cref) tid (cThreads ctx), cIdSource = idSource' }, Right (NewRef newcrid))
|
||||
pure $ Right (ctx { cThreads = goto (c cref) tid (cThreads ctx), cIdSource = idSource' }, Right (NewCRef newcrid))
|
||||
|
||||
-- read from a @CRef@.
|
||||
AReadRef cref@(CRef crid _) c -> do
|
||||
AReadCRef cref@(CRef crid _) c -> do
|
||||
val <- readCRef cref tid
|
||||
simple (goto (c val) tid (cThreads ctx)) $ ReadRef crid
|
||||
simple (goto (c val) tid (cThreads ctx)) $ ReadCRef crid
|
||||
|
||||
-- read from a @CRef@ for future compare-and-swap operations.
|
||||
AReadRefCas cref@(CRef crid _) c -> do
|
||||
AReadCRefCas cref@(CRef crid _) c -> do
|
||||
tick <- readForTicket cref tid
|
||||
simple (goto (c tick) tid (cThreads ctx)) $ ReadRefCas crid
|
||||
simple (goto (c tick) tid (cThreads ctx)) $ ReadCRefCas crid
|
||||
|
||||
-- modify a @CRef@.
|
||||
AModRef cref@(CRef crid _) f c -> synchronised $ do
|
||||
AModCRef cref@(CRef crid _) f c -> synchronised $ do
|
||||
(new, val) <- f <$> readCRef cref tid
|
||||
writeImmediate cref new
|
||||
simple (goto (c val) tid (cThreads ctx)) $ ModRef crid
|
||||
simple (goto (c val) tid (cThreads ctx)) $ ModCRef crid
|
||||
|
||||
-- modify a @CRef@ using a compare-and-swap.
|
||||
AModRefCas cref@(CRef crid _) f c -> synchronised $ do
|
||||
AModCRefCas cref@(CRef crid _) f c -> synchronised $ do
|
||||
tick@(Ticket _ _ old) <- readForTicket cref tid
|
||||
let (new, val) = f old
|
||||
void $ casCRef cref tid tick new
|
||||
simple (goto (c val) tid (cThreads ctx)) $ ModRefCas crid
|
||||
simple (goto (c val) tid (cThreads ctx)) $ ModCRefCas crid
|
||||
|
||||
-- write to a @CRef@ without synchronising.
|
||||
AWriteRef cref@(CRef crid _) a c -> case memtype of
|
||||
AWriteCRef cref@(CRef crid _) a c -> case memtype of
|
||||
-- write immediately.
|
||||
SequentialConsistency -> do
|
||||
writeImmediate cref a
|
||||
simple (goto c tid (cThreads ctx)) $ WriteRef crid
|
||||
simple (goto c tid (cThreads ctx)) $ WriteCRef crid
|
||||
-- add to buffer using thread id.
|
||||
TotalStoreOrder -> do
|
||||
wb' <- bufferWrite (cWriteBuf ctx) (tid, Nothing) cref a
|
||||
pure $ Right (ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Right (WriteRef crid))
|
||||
pure $ Right (ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Right (WriteCRef crid))
|
||||
-- add to buffer using both thread id and cref id
|
||||
PartialStoreOrder -> do
|
||||
wb' <- bufferWrite (cWriteBuf ctx) (tid, Just crid) cref a
|
||||
pure $ Right (ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Right (WriteRef crid))
|
||||
pure $ Right (ctx { cThreads = goto c tid (cThreads ctx), cWriteBuf = wb' }, Right (WriteCRef crid))
|
||||
|
||||
-- perform a compare-and-swap on a @CRef@.
|
||||
ACasRef cref@(CRef crid _) tick a c -> synchronised $ do
|
||||
ACasCRef cref@(CRef crid _) tick a c -> synchronised $ do
|
||||
(suc, tick') <- casCRef cref tid tick a
|
||||
simple (goto (c (suc, tick')) tid (cThreads ctx)) $ CasRef crid suc
|
||||
simple (goto (c (suc, tick')) tid (cThreads ctx)) $ CasCRef crid suc
|
||||
|
||||
-- commit a @CRef@ write
|
||||
ACommit t c -> do
|
||||
@ -278,7 +278,7 @@ stepThread sched memtype tid action ctx = case action of
|
||||
TotalStoreOrder -> commitWrite (cWriteBuf ctx) (t, Nothing)
|
||||
-- commit using the cref id.
|
||||
PartialStoreOrder -> commitWrite (cWriteBuf ctx) (t, Just c)
|
||||
pure $ Right (ctx { cWriteBuf = wb' }, Right (CommitRef t c))
|
||||
pure $ Right (ctx { cWriteBuf = wb' }, Right (CommitCRef t c))
|
||||
|
||||
-- run a STM transaction atomically.
|
||||
AAtom stm c -> synchronised $ do
|
||||
|
||||
@ -103,21 +103,21 @@ data Action n r =
|
||||
| AGetNumCapabilities (Int -> Action n r)
|
||||
| ASetNumCapabilities Int (Action n r)
|
||||
|
||||
| forall a. ANewVar String (MVar r a -> Action n r)
|
||||
| forall a. APutVar (MVar r a) a (Action n r)
|
||||
| forall a. ATryPutVar (MVar r a) a (Bool -> Action n r)
|
||||
| forall a. AReadVar (MVar r a) (a -> Action n r)
|
||||
| forall a. ATryReadVar (MVar r a) (Maybe a -> Action n r)
|
||||
| forall a. ATakeVar (MVar r a) (a -> Action n r)
|
||||
| forall a. ATryTakeVar (MVar r a) (Maybe a -> Action n r)
|
||||
| forall a. ANewMVar String (MVar r a -> Action n r)
|
||||
| forall a. APutMVar (MVar r a) a (Action n r)
|
||||
| forall a. ATryPutMVar (MVar r a) a (Bool -> Action n r)
|
||||
| forall a. AReadMVar (MVar r a) (a -> Action n r)
|
||||
| forall a. ATryReadMVar (MVar r a) (Maybe a -> Action n r)
|
||||
| forall a. ATakeMVar (MVar r a) (a -> Action n r)
|
||||
| forall a. ATryTakeMVar (MVar r a) (Maybe a -> Action n r)
|
||||
|
||||
| forall a. ANewRef String a (CRef r a -> Action n r)
|
||||
| forall a. AReadRef (CRef r a) (a -> Action n r)
|
||||
| forall a. AReadRefCas (CRef r a) (Ticket a -> Action n r)
|
||||
| forall a b. AModRef (CRef r a) (a -> (a, b)) (b -> Action n r)
|
||||
| forall a b. AModRefCas (CRef r a) (a -> (a, b)) (b -> Action n r)
|
||||
| forall a. AWriteRef (CRef r a) a (Action n r)
|
||||
| forall a. ACasRef (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r)
|
||||
| forall a. ANewCRef String a (CRef r a -> Action n r)
|
||||
| forall a. AReadCRef (CRef r a) (a -> Action n r)
|
||||
| forall a. AReadCRefCas (CRef r a) (Ticket a -> Action n r)
|
||||
| forall a b. AModCRef (CRef r a) (a -> (a, b)) (b -> Action n r)
|
||||
| forall a b. AModCRefCas (CRef r a) (a -> (a, b)) (b -> Action n r)
|
||||
| forall a. AWriteCRef (CRef r a) a (Action n r)
|
||||
| forall a. ACasCRef (CRef r a) (Ticket a) a ((Bool, Ticket a) -> Action n r)
|
||||
|
||||
| forall e. Exception e => AThrow e
|
||||
| forall e. Exception e => AThrowTo ThreadId e (Action n r)
|
||||
@ -145,21 +145,21 @@ lookahead = fromList . lookahead' where
|
||||
lookahead' (AMyTId _) = [WillMyThreadId]
|
||||
lookahead' (AGetNumCapabilities _) = [WillGetNumCapabilities]
|
||||
lookahead' (ASetNumCapabilities i k) = WillSetNumCapabilities i : lookahead' k
|
||||
lookahead' (ANewVar _ _) = [WillNewVar]
|
||||
lookahead' (APutVar (MVar c _) _ k) = WillPutVar c : lookahead' k
|
||||
lookahead' (ATryPutVar (MVar c _) _ _) = [WillTryPutVar c]
|
||||
lookahead' (AReadVar (MVar c _) _) = [WillReadVar c]
|
||||
lookahead' (ATryReadVar (MVar c _) _) = [WillTryReadVar c]
|
||||
lookahead' (ATakeVar (MVar c _) _) = [WillTakeVar c]
|
||||
lookahead' (ATryTakeVar (MVar c _) _) = [WillTryTakeVar c]
|
||||
lookahead' (ANewRef _ _ _) = [WillNewRef]
|
||||
lookahead' (AReadRef (CRef r _) _) = [WillReadRef r]
|
||||
lookahead' (AReadRefCas (CRef r _) _) = [WillReadRefCas r]
|
||||
lookahead' (AModRef (CRef r _) _ _) = [WillModRef r]
|
||||
lookahead' (AModRefCas (CRef r _) _ _) = [WillModRefCas r]
|
||||
lookahead' (AWriteRef (CRef r _) _ k) = WillWriteRef r : lookahead' k
|
||||
lookahead' (ACasRef (CRef r _) _ _ _) = [WillCasRef r]
|
||||
lookahead' (ACommit t c) = [WillCommitRef t c]
|
||||
lookahead' (ANewMVar _ _) = [WillNewMVar]
|
||||
lookahead' (APutMVar (MVar c _) _ k) = WillPutMVar c : lookahead' k
|
||||
lookahead' (ATryPutMVar (MVar c _) _ _) = [WillTryPutMVar c]
|
||||
lookahead' (AReadMVar (MVar c _) _) = [WillReadMVar c]
|
||||
lookahead' (ATryReadMVar (MVar c _) _) = [WillTryReadMVar c]
|
||||
lookahead' (ATakeMVar (MVar c _) _) = [WillTakeMVar c]
|
||||
lookahead' (ATryTakeMVar (MVar c _) _) = [WillTryTakeMVar c]
|
||||
lookahead' (ANewCRef _ _ _) = [WillNewCRef]
|
||||
lookahead' (AReadCRef (CRef r _) _) = [WillReadCRef r]
|
||||
lookahead' (AReadCRefCas (CRef r _) _) = [WillReadCRefCas r]
|
||||
lookahead' (AModCRef (CRef r _) _ _) = [WillModCRef r]
|
||||
lookahead' (AModCRefCas (CRef r _) _ _) = [WillModCRefCas r]
|
||||
lookahead' (AWriteCRef (CRef r _) _ k) = WillWriteCRef r : lookahead' k
|
||||
lookahead' (ACasCRef (CRef r _) _ _ _) = [WillCasCRef r]
|
||||
lookahead' (ACommit t c) = [WillCommitCRef t c]
|
||||
lookahead' (AAtom _ _) = [WillSTM]
|
||||
lookahead' (AThrow _) = [WillThrow]
|
||||
lookahead' (AThrowTo tid _ k) = WillThrowTo tid : lookahead' k
|
||||
|
||||
@ -478,7 +478,7 @@ dependentActions memtype ds a1 a2 = case (a1, a2) of
|
||||
|
||||
-- | Determine if an action is a commit or not.
|
||||
isCommitRef :: ThreadAction -> Bool
|
||||
isCommitRef (CommitRef _ _) = True
|
||||
isCommitRef (CommitCRef _ _) = True
|
||||
isCommitRef _ = False
|
||||
|
||||
-- | Extra threads created in a fork.
|
||||
|
||||
@ -556,8 +556,8 @@ updateDepState depstate tid act = DepState
|
||||
-- | Update the 'CRef' buffer state with the action that has just
|
||||
-- happened.
|
||||
updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool
|
||||
updateCRState (CommitRef _ r) = M.delete r
|
||||
updateCRState (WriteRef r) = M.insert r True
|
||||
updateCRState (CommitCRef _ r) = M.delete r
|
||||
updateCRState (WriteCRef r) = M.insert r True
|
||||
updateCRState ta
|
||||
| isBarrier $ simplifyAction ta = const M.empty
|
||||
| otherwise = id
|
||||
@ -582,9 +582,9 @@ canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool
|
||||
canInterrupt depstate tid act
|
||||
-- If masked interruptible, blocked actions can be interrupted.
|
||||
| isMaskedInterruptible depstate tid = case act of
|
||||
BlockedPutVar _ -> True
|
||||
BlockedReadVar _ -> True
|
||||
BlockedTakeVar _ -> True
|
||||
BlockedPutMVar _ -> True
|
||||
BlockedReadMVar _ -> True
|
||||
BlockedTakeMVar _ -> True
|
||||
BlockedSTM _ -> True
|
||||
BlockedThrowTo _ -> True
|
||||
_ -> False
|
||||
@ -599,9 +599,9 @@ canInterruptL depstate tid lh
|
||||
-- If masked interruptible, actions which can block may be
|
||||
-- interrupted.
|
||||
| isMaskedInterruptible depstate tid = case lh of
|
||||
WillPutVar _ -> True
|
||||
WillReadVar _ -> True
|
||||
WillTakeVar _ -> True
|
||||
WillPutMVar _ -> True
|
||||
WillReadMVar _ -> True
|
||||
WillTakeMVar _ -> True
|
||||
WillSTM -> True
|
||||
WillThrowTo _ -> True
|
||||
_ -> False
|
||||
|
||||
Loading…
Reference in New Issue
Block a user