Test.DejaFu.Deterministic.Internal.Memory

Operations over CRefs and MVars

Relaxed memory operations over CRefs 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).

Manipulating CRefs

newtype WriteBuffer r

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.

Constructors

WriteBuffer

Fields

buffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite r))

data BufferedWrite r where

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 -> CRef r a -> a -> BufferedWrite r

emptyBuffer :: WriteBuffer r

An empty write buffer.

bufferWrite :: Monad n => Fixed n r s -> WriteBuffer r -> (ThreadId, Maybe CRefId) -> CRef r a -> a -> n (WriteBuffer r)

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)

Commit the write at the head of a buffer.

readCRef :: Monad n => Fixed n r s -> CRef r a -> ThreadId -> n a

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)

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)

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)

Read the local state of a CRef.

writeImmediate :: Monad n => Fixed n r s -> CRef r a -> a -> n ()

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 ()

Flush all writes in the buffer.

addCommitThreads :: WriteBuffer r -> Threads n r s -> Threads n r s

Add phantom threads to the thread list to commit pending writes.

delCommitThreads :: Threads n r s -> Threads n r s

Remove phantom threads.

Manipulating MVars

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])

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])

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])

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])

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])

Try to take from a MVar, not blocking if empty.

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])

Mutate a MVar, in either a blocking or nonblocking way.

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])

Read a MVar, in either a blocking or nonblocking way.