LIO.LIORef.TCB

This module implements labeled IORefs. The interface is analogous to Data.IORef, but the operations take place in the LIO monad.

Basic Functions

data LIORef l a

An LIORef is an IORef with an associated, static label. The restriction of an immutable label come from the fact that it is possible to leak information through the label itself. Hence, LIO is flow-insensitive. Of course, you can create an LIORef of Labeled to get a limited form of flow-sensitivity.

newLIORef

Arguments

:: LabelState l p s

=> l

Label of reference

-> a

Initial value

-> LIO l p s (LIORef l a)

Mutable reference

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.

labelOfLIORef :: Label l => LIORef l a -> l

Get the label of a reference.

readLIORef :: LabelState l p s => LIORef l a -> LIO l p s a

Read the value of a labeled refernce. 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 use labelOfLIORef to check that a read will suceed.

writeLIORef :: LabelState l p s => LIORef l a -> a -> LIO l p s ()

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.

modifyLIORef

Arguments

:: LabelState l p s

=> LIORef l a

Labeled reference

-> (a -> a)

Modifier

-> LIO l p 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 modifer is provided, the reference contents are not observable by the outer computation and so it is not required that the current label be raised.

atomicModifyLIORef :: LabelState l p s => LIORef l a -> (a -> (a, b)) -> LIO l p s 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.

Privileged Functions

newLIORefP :: LabelState l p s => p -> l -> a -> LIO l p s (LIORef l a)

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.

readLIORefP :: LabelState l p s => p -> LIORef l a -> LIO l p s a

Same as readLIORef except readLIORefP takes a privilege object which is used when the current label is raised.

writeLIORefP :: LabelState l p s => p -> LIORef l a -> a -> LIO l p s ()

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.

modifyLIORefP :: LabelState l p s => p -> LIORef l a -> (a -> a) -> LIO l p s ()

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.

atomicModifyLIORefP :: LabelState l p s => p -> LIORef l a -> (a -> (a, b)) -> LIO l p s b

Same as atomicModifyLIORef except atomicModifyLIORefP takes a set of privileges which are accounted for in label comparisons.

Unsafe (TCB) Functions

newLIORefTCB :: LabelState l p s => l -> a -> LIO l p s (LIORef l a)

Trusted constructor that creates labeled references.

readLIORefTCB :: LabelState l p s => LIORef l a -> LIO l p s a

Trusted function used to read the value of a reference without raising the current label.

writeLIORefTCB :: LabelState l p s => LIORef l a -> a -> LIO l p s ()

Trusted function used to write a new value into a labeled reference, ignoring IFC.

modifyLIORefTCB :: LabelState l p s => LIORef l a -> (a -> a) -> LIO l p s ()

Trusted function that mutates the contents on an LIORef, ignoring IFC.

atomicModifyLIORefTCB :: LabelState l p s => LIORef l a -> (a -> (a, b)) -> LIO l p s b

Trusted function used to atomically modify the contents of a labeled reference, ignoring IFC.