Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Atomic

Description

Wrappers around MVars which provides an atomic modification operation.

Synopsis

Documentation

data Atomic a Source #

A mutable variable which can be read from and *modified*. This provides a modifyAtomic combinator with atomic semantics for modification, unlike modifyMVar.

Instances

Instances details
NFData (Atomic a) Source # 
Instance details

Defined in Agda.Utils.Atomic

Methods

rnf :: Atomic a -> () #

Eq (Atomic a) Source # 
Instance details

Defined in Agda.Utils.Atomic

Methods

(==) :: Atomic a -> Atomic a -> Bool #

(/=) :: Atomic a -> Atomic a -> Bool #

newAtomic :: MonadIO m => a -> m (Atomic a) Source #

Create a new atomic variable with the given initial value.

readAtomic :: MonadIO m => Atomic a -> m a Source #

Read the current state of the atomic variable, waiting if any other thread is modifying it.

Like readMVar, readAtomic is multiple-wakeup, which means that all threads waiting on a modification will be woken up when it finishes.

modifyAtomic :: (MonadIO m, MonadMask m) => Atomic a -> (a -> m (a, b)) -> m b Source #

Modify the contents of an atomic variable. If the continuation fails, or receives an asynchronous exception, the variable is returned to its old state.

No thread, *including the calling thread*, can access the contents of the same Atomic while this function is executing, for reading *or* writing. This means that *any* nested use of the variable, as in

f var = modifyAtomic var old ->
  -- ...
  modifyAtomic var old' -> ... -- (!)
  readAtomic var                -- (!)

will result in a deadlock. The new state of the variable is evaluated (to WHNF).

withAtomic :: (MonadIO m, MonadMask m) => Atomic a -> (a -> m ()) -> m () Source #