This module exposes useful concurrency abstrations for
module is, in part, analogous to Control.Concurrent. Specifically,
LIO provides a means for spawning
LIO computations in a new thread
forkLIO. LIO relies on the lightweight threads managed by
Haskell's runtime system; we do not provide a way to fork OS-level
In addition to this, LIO also provides
lWait which allow
forking of a computation that is restricted from reading data more
sensitive than a given upper bound. This limit is different from
clearance in that it allows the computation to spawn additional
threads with an upper bound above said upper bound label, but below
the clearance. The
lFork function should be used whenever an LIO
computation wishes to execute a sub-computation that may raise the
current label (up to the supplied upper bound). To this end, the
current label only needs to be raised when the computation is
interested in reading the result of the sub-computation. The role of
lWait is precisely this: raise the current label and return the
result of such a sub-computation.
- data LabeledResult l a
- data ThreadId
- myThreadId :: MonadLIO l m => m ThreadId
- forkLIO :: Label l => LIO l () -> LIO l ThreadId
- lForkP :: Priv l p => p -> l -> LIO l a -> LIO l (LabeledResult l a)
- lFork :: Label l => l -> LIO l a -> LIO l (LabeledResult l a)
- lWaitP :: (MonadLIO l m, Priv l p) => p -> LabeledResult l a -> m a
- lWait :: MonadLIO l m => LabeledResult l a -> m a
- trylWaitP :: (MonadLIO l m, Priv l p) => p -> LabeledResult l a -> m (Maybe a)
- trylWait :: MonadLIO l m => LabeledResult l a -> m (Maybe a)
- threadDelay :: MonadLIO l m => Int -> m ()
- data AsyncException
- lForce :: MonadLIO l m => LabeledResult l a -> m (Labeled l (Maybe a))
- lForceP :: (MonadLIO l m, Priv l p) => p -> LabeledResult l a -> m (Labeled l (Maybe a))
A labeled thread result is simply a wrapper for a
LMVar. A thread
can observe the result of another thread, only after raising its label
to the label of the result.
ThreadId is an abstract type representing a handle to a thread.
ThreadId is an instance of
Ord instance implements an arbitrary total ordering over
Show instance lets you convert an arbitrary-valued
ThreadId to string form; showing a
ThreadId value is occasionally
useful when debugging or diagnosing the behaviour of a concurrent
Note: in GHC, if you have a
ThreadId, you essentially have
a pointer to the thread itself. This means the thread itself can't be
garbage collected until you drop the
This misfeature will hopefully be corrected at a later date.
Note: Hugs does not provide any operations on other threads;
ThreadId as a synonym for ().
Forking new threads
lFork, but the supplied set of priviliges are accounted
for when performing label comparisons.
|:: Label l|
Label of result
|-> LIO l a|
Computation to execute in separate thread
|-> LIO l (LabeledResult l a)|
lFork allows one to invoke computations that
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, 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 as enforced by the underlying
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.
lFork immediately returns a
LabeledResult, which is
essentially a "future", or "promise". This prevents
timing/termination attacks in which the duration of the forked
computation affects the duration of the
To guarantee that the computation has completed, it is important that
some thread actually touch the future, i.e., perform an
Waiting on threads
lWait, but uses priviliges in label checks and raises.
LabeledResult (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
clearance. Moreover, before block-reading,
lWait raises the current
label to the join of the current label and label of result. An
exception is thrown by the underlying
guardWrite if this is not the
case. Additionally, if the thread terminates with an exception (for
example if it violates clearance), the exception is rethrown by
lWait. Similarly, if the thread reads values above the result label,
an exception is thrown in place of the result.
trylWait, but uses priviliges in label checks and raises.
lWait, but does not block waiting for result.
Suspend current thread for a given number of microseconds.
Forcing computations (EXPERIMENTAL)
The current thread's stack exceeded its limit. Since an exception has been raised, the thread's stack will certainly be below its limit again, but the programmer should take remedial action immediately.
The program's heap is reaching its limit, and the program should take action to reduce the amount of live data it has. Notes:
This exception is raised by another thread
This exception is raised by default in the main thread of the program when the user requests to terminate the program via the usual mechanism(s) (e.g. Control-C in the console).
Force execution of a thread spawned with
If the computation completed without raising an exception, then the
result is wrapped in a
Just, otherwise this function returns
Nothing. Note that the current computation must be able to read
and write at the security level of the labeled result.