module Test.DejaFu.Deterministic.Internal.Memory where
import Control.Monad (when)
import Data.Map.Strict (Map)
import Data.Maybe (isJust, fromJust)
import Data.Monoid ((<>))
import Data.Sequence (Seq, ViewL(..), (><), singleton, viewl)
import Test.DejaFu.Deterministic.Internal.Common
import Test.DejaFu.Deterministic.Internal.Threading
import Test.DejaFu.Internal
import qualified Data.Map.Strict as M
newtype WriteBuffer r = WriteBuffer
{ buffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite r)) }
data BufferedWrite r where
BufferedWrite :: ThreadId -> CRef r a -> a -> BufferedWrite r
emptyBuffer :: WriteBuffer r
emptyBuffer = WriteBuffer M.empty
bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> CRef r a -> a -> n (WriteBuffer r)
bufferWrite fixed (WriteBuffer wb) k@(tid, _) cref@(CRef _ ref) new = do
let write = singleton $ BufferedWrite tid cref new
let buffer' = M.insertWith (flip (><)) k write wb
(locals, count, def) <- readRef fixed ref
writeRef fixed ref (M.insert tid new locals, count, def)
return $ WriteBuffer buffer'
commitWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r)
commitWrite fixed w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of
BufferedWrite _ cref a :< rest -> do
writeImmediate fixed cref a
return . WriteBuffer $ M.insert k rest wb
EmptyL -> return w
readCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n a
readCRef fixed cref tid = do
(val, _) <- readCRefPrim fixed cref tid
return val
readForTicket :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (Ticket a)
readForTicket fixed cref@(CRef crid _) tid = do
(val, count) <- readCRefPrim fixed cref tid
return $ Ticket crid count val
casCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a)
casCRef fixed cref tid (Ticket _ cc _) !new = do
tick'@(Ticket _ cc' _) <- readForTicket fixed cref tid
if cc == cc'
then do
writeImmediate fixed cref new
tick'' <- readForTicket fixed cref tid
return (True, tick'')
else return (False, tick')
readCRefPrim :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (a, Integer)
readCRefPrim fixed (CRef _ ref) tid = do
(vals, count, def) <- readRef fixed ref
return (M.findWithDefault def tid vals, count)
writeImmediate :: Monad n => Fixed n r s -> CRef r a -> a -> n ()
writeImmediate fixed (CRef _ ref) a = do
(_, count, _) <- readRef fixed ref
writeRef fixed ref (M.empty, count + 1, a)
writeBarrier :: Monad n => Fixed n r s -> WriteBuffer r -> n ()
writeBarrier fixed (WriteBuffer wb) = mapM_ flush $ M.elems wb where
flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate fixed cref a
addCommitThreads :: WriteBuffer r -> Threads n r s -> Threads n r s
addCommitThreads (WriteBuffer wb) ts = ts <> M.fromList phantoms where
phantoms = [ (ThreadId Nothing $ negate tid, mkthread $ fromJust c)
| ((k, b), tid) <- zip (M.toList wb) [1..]
, let c = go $ viewl b
, isJust c]
go (BufferedWrite tid (CRef crid _) _ :< _) = Just $ ACommit tid crid
go EmptyL = Nothing
delCommitThreads :: Threads n r s -> Threads n r s
delCommitThreads = M.filterWithKey $ \k _ -> k >= initialThread
putIntoMVar :: Monad n => MVar r a -> a -> Action n r s
-> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
putIntoMVar cvar a c = mutMVar True cvar a (const c)
tryPutIntoMVar :: Monad n => MVar r a -> a -> (Bool -> Action n r s)
-> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
tryPutIntoMVar = mutMVar False
readFromMVar :: Monad n => MVar r a -> (a -> Action n r s)
-> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
readFromMVar cvar c = seeMVar False True cvar (c . fromJust)
takeFromMVar :: Monad n => MVar r a -> (a -> Action n r s)
-> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
takeFromMVar cvar c = seeMVar True True cvar (c . fromJust)
tryTakeFromMVar :: Monad n => MVar r a -> (Maybe a -> Action n r s)
-> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
tryTakeFromMVar = seeMVar True False
mutMVar :: Monad n
=> Bool -> MVar r a -> a -> (Bool -> Action n r s)
-> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
mutMVar blocking (MVar cvid ref) a c fixed threadid threads = do
val <- readRef fixed ref
case val of
Just _
| blocking ->
let threads' = block (OnMVarEmpty cvid) threadid threads
in return (False, threads', [])
| otherwise ->
return (False, goto (c False) threadid threads, [])
Nothing -> do
writeRef fixed ref $ Just a
let (threads', woken) = wake (OnMVarFull cvid) threads
return (True, goto (c True) threadid threads', woken)
seeMVar :: Monad n
=> Bool -> Bool -> MVar r a -> (Maybe a -> Action n r s)
-> Fixed n r s -> ThreadId -> Threads n r s -> n (Bool, Threads n r s, [ThreadId])
seeMVar emptying blocking (MVar cvid ref) c fixed threadid threads = do
val <- readRef fixed ref
case val of
Just _ -> do
when emptying $ writeRef fixed ref Nothing
let (threads', woken) = wake (OnMVarEmpty cvid) threads
return (True, goto (c val) threadid threads', woken)
Nothing
| blocking ->
let threads' = block (OnMVarFull cvid) threadid threads
in return (False, threads', [])
| otherwise ->
return (False, goto (c Nothing) threadid threads, [])