lio-0.9.1.1: Labeled IO Information Flow Control Library

Safe HaskellTrustworthy

LIO.Concurrent

Contents

Description

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.

Synopsis

Documentation

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.

lForkSource

Arguments

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

Constructors

StackOverflow

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.

HeapOverflow

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

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

UserInterrupt

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

lBracketSource

Arguments

:: MonadLIO l m 
=> l

Label of result

-> Int

Duration of computation in microseconds

-> LIO l a

Computation to execute in separate thread

-> m (Labeled l (Maybe a))

Labeled result

Though in most cases using a LabeledResult is sufficient, in certain scenarios it is desirable to produce a pure Labeled value that is the result of other potentially sensitive values. As such, we provide lBracket.

lBracket is like lFork, but rather than returning a LabeledResult, it returns a Labeled value. The key difference between the two is that lBracket takes an additional parameter specifying the number of microseconds the inner computation will take. As such, lBracket will block for the specified duration and the result of the inner computation be forced. That is, if the computation terminated cleanly, i.e., it did not throw an exception and it finished in the time specified, then Just the result is returned, otherwise Nothing is returned.

Note that the original LIO (before version 0.9) included a similar "primitive" called toLabeled. We have chosen to call this lBracket in part because it is a more descriptive name and to avoid confusion with the previous toLabeled where time was not considered.

lBracketPSource

Arguments

:: (MonadLIO l m, Priv l p) 
=> p

Privileges

-> l

Label of result

-> Int

Duration of computation in microseconds

-> LIO l a

Computation to execute in separate thread

-> m (Labeled l (Maybe a))

Labeled result

Same as lBracket, but uses privileges when forking the new thread.