dejafu-2.3.0.1: A library for unit-testing concurrent programs.

Copyright(c) 2016--2019 Michael Walker
LicenseMIT
MaintainerMichael Walker <mike@barrucadu.co.uk>
Stabilityexperimental
PortabilityBangPatterns, GADTs, FlexibleContexts, LambdaCase, RecordWildCards
Safe HaskellNone
LanguageHaskell2010

Test.DejaFu.Conc.Internal.Memory

Contents

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

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.

commitThreadId :: ThreadId -> Maybe IORefId -> ThreadId Source #

The ID of a commit thread.

delCommitThreads :: Threads n -> Threads n Source #

Remove phantom threads.

Manipulating MVars

data Blocking Source #

Constructors

Blocking 
NonBlocking 

data Emptying Source #

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.

mutMVar :: MonadDejaFu n => Blocking -> ModelMVar n a -> a -> (Bool -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ()) Source #

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

seeMVar :: MonadDejaFu n => Emptying -> Blocking -> ModelMVar n a -> (Maybe a -> Action n) -> ThreadId -> Threads n -> n (Bool, Threads n, [ThreadId], n ()) Source #

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