Copyright | (c) 2016 Michael Walker |
---|---|

License | MIT |

Maintainer | Michael Walker <mike@barrucadu.co.uk> |

Stability | experimental |

Portability | BangPatterns, GADTs |

Safe Haskell | None |

Language | Haskell2010 |

Operations over `CRef`

s and `MVar`

s. This module is NOT considered
to form part of the public interface of this library.

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.