lFork, but the supplied set of priviliges are accounted
for when performing label comparisons.
|:: LabelState l p s|
Label of result
|-> LIO l p s a|
Computation to execute in separate thread
|-> LIO l p s (LRes l a)|
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
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
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, but uses priviliges in label checks and raises.
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.