lio- Labeled IO Information Flow Control Library

Safe HaskellTrustworthy




This module exposes useful concurrency abstrations for LIO. This module is, in part, analogous to Control.Concurrent. Specifically, LIO provides a means for spawning LIO computations in a new thread with forkLIO. LIO relies on the lightweight threads managed by Haskell's runtime system; we do not provide a way to fork OS-level threads.

In addition to this, LIO also provides lFork and 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 Source

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.

data ThreadId

A ThreadId is an abstract type representing a handle to a thread. ThreadId is an instance of Eq, Ord and Show, where the Ord instance implements an arbitrary total ordering over ThreadIds. The 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 program.

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 ThreadId. This misfeature will hopefully be corrected at a later date.

Note: Hugs does not provide any operations on other threads; it defines ThreadId as a synonym for ().

myThreadId :: MonadLIO l m => m ThreadIdSource

Get the ThreadId of the calling thread.

Forking new threads

forkLIO :: Label l => LIO l () -> LIO l ThreadIdSource

Execute an LIO computation in a new lightweight thread. The ThreadId of the newly created thread is returned.

lForkP :: Priv l p => p -> l -> LIO l a -> LIO l (LabeledResult l a)Source

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



:: Label l 
=> l

Label of result

-> LIO l a

Computation to execute in separate thread

-> LIO l (LabeledResult l a)

Labeled result

Labeled fork. 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 lWait and 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 guardAlloc. 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.

Note that 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 lFork.

To guarantee that the computation has completed, it is important that some thread actually touch the future, i.e., perform an lWait.

Waiting on threads

lWaitP :: (MonadLIO l m, Priv l p) => p -> LabeledResult l a -> m aSource

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

lWait :: MonadLIO l m => LabeledResult l a -> m aSource

Given a 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.

trylWaitP :: (MonadLIO l m, Priv l p) => p -> LabeledResult l a -> m (Maybe a)Source

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

trylWait :: MonadLIO l m => LabeledResult l a -> m (Maybe a)Source

Same as lWait, but does not block waiting for result.

threadDelay :: MonadLIO l m => Int -> m ()Source

Suspend current thread for a given number of microseconds.

Forcing computations (EXPERIMENTAL)

data AsyncException

Asynchronous exceptions.



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:

  • It is undefined which thread receives this exception.
  • GHC currently does not throw HeapOverflow exceptions.

This exception is raised by another thread calling killThread, or by the system if it needs to terminate the thread for some reason.


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).

lForce :: MonadLIO l m => LabeledResult l a -> m (Labeled l (Maybe a))Source

Force execution of a thread spawned with lFork or lForkP. 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.

lForceP :: (MonadLIO l m, Priv l p) => p -> LabeledResult l a -> m (Labeled l (Maybe a))Source

Same as lForce, but uses privileges when raising current label to the join of the current label and result label.