lio-0.1.2: Labeled IO Information Flow Control Library

Safe HaskellTrustworthy



This module exposes the concurrent interface to LIO. Specifically, it implements labeled fork (lFork) and wait (lWait). We strongly suggest these primitives over toLabeled as they are termination-senstivie.



lForkP :: LabelState l p s => p -> l -> LIO l p s a -> LIO l p s (LRes l a)Source

Same as lFork, but the supplied set of priviliges are accounted for when performing label comparisons.



:: LabelState l p s 
=> l

Label of result

-> LIO l p s a

Computation to execute in separate thread

-> LIO l p s (LRes l a)

Labeled result

Labeled fork. lFork allows one to invoke computations taht would otherwise raise the current label, but without actually raising the label. The computation is executed in a separate thread and writes its result into a labeled result (whose label is supplied). To observe the result of the computation, or if the computation has terminated, one will have to call lWait and raise the current label. Of couse, as in toLabeled, this can be postponed until the result is needed.

lFork takes a label, which corresponds to the label of the result. It is require that this label is above the current label, and below the current clearance. Moreover, the supplied computation must not read anything more sensitive, i.e., with a label above the supplied label --- doing so will result in an exception (whose label will reflect this observation) being thrown.

If an exception is thrown in the inner computation, the exception label will be raised to the join of the result label and original exception label.

Not that, compared to toLabeled, lFork immediately returns a labeled result of type LRes, which is essentially a "future", or "promise". Moreover, to guarantee that the computation has completed, it is important that some thread actually touch the future, i.e., perform an lWait.

lWaitP :: LabelState l p s => p -> LRes l a -> LIO l p s aSource

Same as lWait, but uses priviliges in label checks and raises.

lWait :: LabelState l p s => LRes l a -> LIO l p s aSource

Given a labeled result (a future), lWait returns the unwrapped result (blocks, if necessary). For lWait to succeed, the label of the result must be above the current label and below the current clearnce. Moreover, before block-reading, lWait raises the current label to the join of the current label and label of result. If the thread lWait is terminates with an exception (for example if it violates clearance), the exceptin is rethrown. Similarly, if the thread reads values above the result label, an exception is thrown in place of the result.