Safe Haskell | Trustworthy |
---|
Mutable reference in the LIO
monad. As with other objects in LIO,
mutable references have an associated label that is used to impose
restrictions on its operations. In fact, labeled references
(LIORef
s) are solely labeled IORef
s with read and write access
restricted according to the label. This module is analogous to
Data.IORef, but the operations take place in the LIO
monad.
- data LIORef l a
- newLIORef :: MonadLIO l m => l -> a -> m (LIORef l a)
- newLIORefP :: (MonadLIO l m, Priv l p) => p -> l -> a -> m (LIORef l a)
- readLIORef :: MonadLIO l m => LIORef l a -> m a
- readLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> m a
- writeLIORef :: MonadLIO l m => LIORef l a -> a -> m ()
- writeLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> a -> m ()
- modifyLIORef :: Label l => LIORef l a -> (a -> a) -> LIO l ()
- modifyLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> (a -> a) -> m ()
- atomicModifyLIORef :: MonadLIO l m => LIORef l a -> (a -> (a, b)) -> m b
- atomicModifyLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> (a -> (a, b)) -> m b
Documentation
An LIORef
is an IORef
with an associated, fixed label. The
restriction to an immutable label come from the fact that it is
possible to leak information through the label itself, if we wish to
allow LIORef
to be an instance of LabelOf
. Of course, you can
create an LIORef
of Labeled
to get a limited form of
flow-sensitivity.
Basic Functions
Create labeled IORef
s
To create a new reference the label of the reference must be
below the thread's current clearance and above the current label.
If this is the case, the reference is built. Otherwise an exception
will be thrown by the underlying guardAlloc
guard.
newLIORefP :: (MonadLIO l m, Priv l p) => p -> l -> a -> m (LIORef l a)Source
Same as newLIORef
except newLIORefP
takes a set of
privileges which are accounted for in comparing the label of
the reference to the current label and clearance.
Read LIORef
s
readLIORef :: MonadLIO l m => LIORef l a -> m aSource
Read the value of a labeled reference. A read succeeds only if the
label of the reference is below the current clearance. Moreover,
the current label is raised to the join of the current label and
the reference label. To avoid failures (introduced by the taint
readLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> m aSource
Same as readLIORef
except readLIORefP
takes a privilege object
which is used when the current label is raised.
Write LIORef
s
writeLIORef :: MonadLIO l m => LIORef l a -> a -> m ()Source
Write a new value into a labeled reference. A write succeeds if
the current label can-flow-to the label of the reference, and the
label of the reference can-flow-to the current clearance. Otherwise,
an exception is raised by the underlying guardAlloc
guard.
writeLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> a -> m ()Source
Same as writeLIORef
except writeLIORefP
takes a set of
privileges which are accounted for in comparing the label of
the reference to the current label and clearance.
Modify LIORef
s
Mutate the contents of a labeled reference. For the mutation to
succeed it must be that the current label can flow to the label of the
reference, and the label of the reference can flow to the current
clearance. Note that because a modifier is provided, the reference
contents are not observable by the outer computation and so it is not
required that the current label be raised. It is, however, required
that the label of the reference be bounded by the current label and
clearance (as checked by the underlying guardAlloc
guard).
modifyLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> (a -> a) -> m ()Source
Same as modifyLIORef
except modifyLIORefP
takes a set of
privileges which are accounted for in comparing the label of
the reference to the current label and clearance.
atomicModifyLIORef :: MonadLIO l m => LIORef l a -> (a -> (a, b)) -> m bSource
Atomically modifies the contents of an LIORef
. It is required
that the label of the reference be above the current label, but
below the current clearance. Moreover, since this function can be
used to directly read the value of the stored reference, the
computation is "tainted" by the reference label (i.e., the
current label is raised to the join
of the current and reference
labels). These checks and label raise are done by guardWrite
,
which will raise an exception if any of the IFC conditions cannot
be satisfied.
atomicModifyLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> (a -> (a, b)) -> m bSource
Same as atomicModifyLIORef
except atomicModifyLIORefP
takes
a set of privileges which are accounted for in label comparisons.