LIO.Concurrent

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.

Documentation

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

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

lFork

Arguments

:: 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 being thrown.

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 a

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

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

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.