| Copyright | (c) 2016--2019 Michael Walker |
|---|---|
| License | MIT |
| Maintainer | Michael Walker <mike@barrucadu.co.uk> |
| Stability | experimental |
| Portability | BangPatterns, GADTs, FlexibleContexts, LambdaCase, RecordWildCards |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Test.DejaFu.Conc.Internal.Memory
Description
Operations over IORefs and MVars. This module is NOT considered
to form part of the public interface of this library.
Relaxed memory operations over IORefs 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" IORef.
This model comes from /Dynamic Partial Order Reduction for Relaxed Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015).
Synopsis
- newtype WriteBuffer n = WriteBuffer {}
- data BufferedWrite n where
- BufferedWrite :: ThreadId -> ModelIORef n a -> a -> BufferedWrite n
- emptyBuffer :: WriteBuffer n
- bufferWrite :: MonadDejaFu n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> ModelIORef n a -> a -> n (WriteBuffer n)
- commitWrite :: MonadDejaFu n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n)
- readIORef :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n a
- readForTicket :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n (ModelTicket a)
- casIORef :: MonadDejaFu n => ModelIORef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())
- readIORefPrim :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n (a, Integer)
- readIORefGlobal :: MonadDejaFu n => ModelIORef n a -> n a
- writeImmediate :: MonadDejaFu n => ModelIORef n a -> a -> n (n ())
- writeBarrier :: MonadDejaFu n => WriteBuffer n -> n ()
- addCommitThreads :: WriteBuffer n -> Threads n -> Threads n
- commitThreadId :: ThreadId -> Maybe IORefId -> ThreadId
- delCommitThreads :: Threads n -> Threads n
- data Blocking
- data Emptying
- putIntoMVar :: MonadDejaFu n => ModelMVar n a -> a -> Action n -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ())
- tryPutIntoMVar :: MonadDejaFu n => ModelMVar n a -> a -> (Bool -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ())
- readFromMVar :: (MonadDejaFu n, HasCallStack) => ModelMVar n a -> (a -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ())
- tryReadFromMVar :: MonadDejaFu n => ModelMVar n a -> (Maybe a -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ())
- takeFromMVar :: (MonadDejaFu n, HasCallStack) => ModelMVar n a -> (a -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ())
- tryTakeFromMVar :: MonadDejaFu n => ModelMVar n a -> (Maybe a -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ())
- mutMVar :: MonadDejaFu n => Blocking -> ModelMVar n a -> a -> (Bool -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ())
- seeMVar :: MonadDejaFu n => Emptying -> Blocking -> ModelMVar n a -> (Maybe a -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ())
Manipulating IORefs
newtype WriteBuffer n Source #
In non-sequentially-consistent memory models, non-synchronised writes get buffered.
The IORefId parameter is only used under PSO. Under TSO each
thread has a single buffer.
Constructors
| WriteBuffer | |
data BufferedWrite n 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.
Constructors
| BufferedWrite :: ThreadId -> ModelIORef n a -> a -> BufferedWrite n |
emptyBuffer :: WriteBuffer n Source #
An empty write buffer.
bufferWrite :: MonadDejaFu n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> ModelIORef n a -> a -> n (WriteBuffer n) Source #
Add a new write to the end of a buffer.
commitWrite :: MonadDejaFu n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n) Source #
Commit the write at the head of a buffer.
readIORef :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n a Source #
Read from a IORef, returning a newer thread-local non-committed
write if there is one.
readForTicket :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n (ModelTicket a) Source #
Read from a IORef, returning a Ticket representing the current
view of the thread.
casIORef :: MonadDejaFu n => ModelIORef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ()) Source #
Perform a compare-and-swap on a IORef if the ticket is still
valid. This is strict in the "new" value argument.
readIORefPrim :: MonadDejaFu n => ModelIORef n a -> ThreadId -> n (a, Integer) Source #
Read the local state of a IORef.
readIORefGlobal :: MonadDejaFu n => ModelIORef n a -> n a Source #
Read the global state of a IORef.
writeImmediate :: MonadDejaFu n => ModelIORef n a -> a -> n (n ()) Source #
Write and commit to a IORef immediately, clearing the update map
and incrementing the write count.
writeBarrier :: MonadDejaFu n => WriteBuffer n -> n () Source #
Flush all writes in the buffer.
addCommitThreads :: WriteBuffer n -> Threads n -> Threads n Source #
Add phantom threads to the thread list to commit pending writes.
delCommitThreads :: Threads n -> Threads n Source #
Remove phantom threads.
Manipulating MVars
Constructors
| Blocking | |
| NonBlocking |
Constructors
| Emptying | |
| NonEmptying |
putIntoMVar :: MonadDejaFu n => ModelMVar n a -> a -> Action n -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ()) Source #
Put into a MVar, blocking if full.
tryPutIntoMVar :: MonadDejaFu n => ModelMVar n a -> a -> (Bool -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ()) Source #
Try to put into a MVar, not blocking if full.
readFromMVar :: (MonadDejaFu n, HasCallStack) => ModelMVar n a -> (a -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ()) Source #
Read from a MVar, blocking if empty.
tryReadFromMVar :: MonadDejaFu n => ModelMVar n a -> (Maybe a -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ()) Source #
Try to read from a MVar, not blocking if empty.
takeFromMVar :: (MonadDejaFu n, HasCallStack) => ModelMVar n a -> (a -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ()) Source #
Take from a MVar, blocking if empty.
tryTakeFromMVar :: MonadDejaFu n => ModelMVar n a -> (Maybe a -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ()) Source #
Try to take from a MVar, not blocking if empty.