LIO.LIORef

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 (LIORefs) are simply labeled IORefs 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.

Documentation

type LIORef l a = LObj l (IORef a)

An LIORef is an IORef with an associated, fixed label. The restriction to an immutable label comes from the fact that it is possible to leak information through the label itself, since 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 IORefs

newLIORef

Arguments

:: Label l

=> l

Label of reference

-> a

Initial value

-> LIO l (LIORef l a)

Mutable reference

Create a new reference with a particularlabel. The label specified must be between the thread's current label and clearance, as enforced by guardAlloc.

newLIORefP :: PrivDesc l p => Priv p -> l -> a -> LIO l (LIORef l a)

Same as newLIORef except newLIORefP takes privileges which make the comparison to the current label more permissive, as enforced by guardAllocP.

Read LIORefs

readLIORef :: Label l => LIORef l a -> LIO l a

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 lub of the current label and the reference label. To avoid failures (introduced by the taint guard) use labelOf to check that a read will succeed.

readLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> LIO l a

Same as readLIORef, except readLIORefP takes a privilege object which is used when the current label is raised (using taintP instead of taint).

Write LIORefs

writeLIORef :: Label l => LIORef l a -> a -> LIO l ()

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 :: PrivDesc l p => Priv p -> LIORef l a -> a -> LIO l ()

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.

Modify LIORefs

modifyLIORef

Arguments

:: Label l

=> LIORef l a

Labeled reference

-> (a -> a)

Modifier

-> LIO l ()

Mutate the contents of a labeled reference. The mutation is performed by a a pure function, which, because of laziness, is not actually evaluated until such point as a (possibly higher-labeled) thread actually reads the LIORef. The caller of modifyLIORef learns no information about the previous contents the LIORef. For that reason, there is no need to raise the current label. The LIORef's label must still lie between the current label and clearance, however (as enforced by guardAlloc).

modifyLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> (a -> a) -> LIO l ()

Like modifyLIORef, but takes a privilege argument and guards execution with guardAllocP instead of guardAlloc.

atomicModifyLIORef :: Label l => LIORef l a -> (a -> (a, b)) -> LIO l b

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 a LabelError exception if any of the IFC conditions cannot be satisfied.

atomicModifyLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> (a -> (a, b)) -> LIO l b

Same as atomicModifyLIORef except atomicModifyLIORefP takes a set of privileges and uses guardWriteP instead of guardWrite.