dejafu-0.3.2.0: Overloadable primitives for testable, potentially non-deterministic, concurrency.

Copyright (c) 2016 Michael Walker MIT Michael Walker stable portable None Haskell2010

Control.Concurrent.Classy.CRef

Contents

Description

Mutable references in a concurrency monad.

Deviations: There is no Eq instance for MonadConc the CRef type. Furthermore, the mkWeakIORef function is not provided.

Synopsis

# CRefs

newCRef :: MonadConc m => a -> m (CRef m a) Source #

Create a new reference.

newCRef = newCRefN ""

readCRef :: MonadConc m => CRef m a -> m a Source #

Read the current value stored in a reference.

readCRef cref = readForCAS cref >>= peekTicket

writeCRef :: MonadConc m => CRef m a -> a -> m () Source #

Write a new value into an CRef, without imposing a memory barrier. This means that relaxed memory effects can be observed.

modifyCRef :: MonadConc m => CRef m a -> (a -> a) -> m () Source #

Mutate the contents of a CRef.

Be warned that modifyCRef does not apply the function strictly. This means if the program calls modifyCRef many times, but seldomly uses the value, thunks will pile up in memory resulting in a space leak. This is a common mistake made when using a CRef as a counter. For example, the following will likely produce a stack overflow:

ref <- newCRef 0
replicateM_ 1000000 $modifyCRef ref (+1) readCRef ref >>= print To avoid this problem, use modifyCRef' instead. modifyCRef' :: MonadConc m => CRef m a -> (a -> a) -> m () Source # Strict version of modifyCRef atomicModifyCRef :: MonadConc m => CRef m a -> (a -> (a, b)) -> m b Source # Atomically modify the value stored in a reference. This imposes a full memory barrier. atomicModifyCRef' :: MonadConc m => CRef m a -> (a -> (a, b)) -> m b Source # Strict version of atomicModifyCRef. This forces both the value stored in the CRef as well as the value returned. atomicWriteCRef :: MonadConc m => CRef m a -> a -> m () Source # Replace the value stored in a reference, with the barrier-to-reordering property that atomicModifyCRef has. atomicWriteCRef r a = atomicModifyCRef r$ const (a, ())

# Memory Model

In a concurrent program, CRef operations may appear out-of-order to another thread, depending on the memory model of the underlying processor architecture. For example, on x86 (which uses total store order), loads can move ahead of stores. Consider this example:

crefs :: MonadConc m => m (Bool, Bool)
crefs = do
r1 <- newCRef False
r2 <- newCRef False

x <- spawn $writeCRef r1 True >> readCRef r2 y <- spawn$ writeCRef r2 True >> readCRef r1

(,) <\$> readCVar x <*> readCVar y

Under a sequentially consistent memory model the possible results are (True, True), (True, False), and (False, True). Under total or partial store order, (False, False) is also a possible result, even though there is no interleaving of the threads which can lead to this.

We can see this by testing with different memory models:

> autocheck' SequentialConsistency crefs
[pass] No Exceptions (checked: 6)
[fail] Consistent Result (checked: 5)
(False,True) S0-------S1-----S0--S2-----S0---
(True,False) S0-------S1-P2-----S1----S0----
(True,True) S0-------S1--P2-----S1---S0----
(False,True) S0-------S1---P2-----S1--S0----
(True,False) S0-------S2-----S1-----S0----
...
False
> autocheck' TotalStoreOrder crefs
False
Traces for non-sequentially-consistent memory models show where writes to CRefs are committed, which makes a write visible to all threads rather than just the one which performed the write. Only writeCRef is broken up into separate write and commit steps, atomicModifyCRef is still atomic and imposes a memory barrier.