Safe Haskell | None |
---|---|
Language | Haskell2010 |
Operations over CRef
s and MVar
s
Relaxed memory operations over CRef
s are implemented with an
explicit write buffer: one per thread for TSO, and one per
thread/variable combination for PSO. Unsynchronised writes append
to this buffer, and periodically separate threads commit from these
buffers to the "actual" CRef
.
This model comes from /Dynamic Partial Order Reduction for Relaxed Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015).
- newtype WriteBuffer r = WriteBuffer {}
- data BufferedWrite r where
- BufferedWrite :: ThreadId -> CRef r a -> a -> BufferedWrite r
- emptyBuffer :: WriteBuffer r
- bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> CRef r a -> a -> n (WriteBuffer r)
- commitWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r)
- readCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n a
- readForTicket :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (Ticket a)
- casCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a)
- readCRefPrim :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (a, Integer)
- writeImmediate :: Monad n => Fixed n r s -> CRef r a -> a -> n ()
- writeBarrier :: Monad n => Fixed n r s -> WriteBuffer r -> n ()
- addCommitThreads :: WriteBuffer r -> Threads n r s -> Threads n r s
- delCommitThreads :: Threads n r s -> Threads n r s
- 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])
- 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])
- 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])
- 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])
- 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])
- 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])
- 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])
Manipulating CRef
s
newtype WriteBuffer r Source
In non-sequentially-consistent memory models, non-synchronised writes get buffered.
The CRefId
parameter is only used under PSO. Under TSO each
thread has a single buffer.
data BufferedWrite r where Source
A buffered write is a reference to the variable, and the value to write. Universally quantified over the value type so that the only thing which can be done with it is to write it to the reference.
BufferedWrite :: ThreadId -> CRef r a -> a -> BufferedWrite r |
emptyBuffer :: WriteBuffer r Source
An empty write buffer.
bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> CRef r a -> a -> n (WriteBuffer r) Source
Add a new write to the end of a buffer.
commitWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r) Source
Commit the write at the head of a buffer.
readCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n a Source
Read from a CRef
, returning a newer thread-local non-committed
write if there is one.
readForTicket :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (Ticket a) Source
Read from a CRef
, returning a Ticket
representing the current
view of the thread.
casCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a) Source
Perform a compare-and-swap on a CRef
if the ticket is still
valid. This is strict in the "new" value argument.
readCRefPrim :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n (a, Integer) Source
Read the local state of a CRef
.
writeImmediate :: Monad n => Fixed n r s -> CRef r a -> a -> n () Source
Write and commit to a CRef
immediately, clearing the update map
and incrementing the write count.
writeBarrier :: Monad n => Fixed n r s -> WriteBuffer r -> n () Source
Flush all writes in the buffer.
addCommitThreads :: WriteBuffer r -> Threads n r s -> Threads n r s Source
Add phantom threads to the thread list to commit pending writes.
delCommitThreads :: Threads n r s -> Threads n r s Source
Remove phantom threads.
Manipulating MVar
s
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]) Source
Put into a MVar
, blocking if full.
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]) Source
Try to put into a MVar
, not blocking if full.
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]) Source
Read from a MVar
, blocking if empty.
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]) Source
Take from a MVar
, blocking if empty.
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]) Source
Try to take from a MVar
, not blocking if empty.