lio-0.1.1: Labeled IO Information Flow Control Library

LIO.Concurrent.LMVar.TCB

Contents

Description

This module provides an implementation for labeled MVars. A labeled MVar, of type LMVar l a, is a mutable location that can be in of of two states; an LMVar can be empty, or it can be full (with a value of tye a). The location is protected by a label of type l. As in the case of LIORefs (see LIO.LIORef), this label is static and does not change according to the content placed into the location.

LMVars can be used to build synchronization primitives and communication channels (LMVars themselves are single-place channels). We refer to Control.Concurrent.MVar for the full documentation on MVars.

Synopsis

Basic Functions

data LMVar l a Source

An LMVar is a labeled synchronization variable (an MVar) that can be used by concurrent threads to communicate.

labelOfLMVar :: Label l => LMVar l a -> lSource

This function returns the label of a labeled MVar.

newEmptyLMVarSource

Arguments

:: LabelState l p s 
=> l

Label of LMVar

-> LIO l p s (LMVar l a)

New mutable location

Create a new labeled MVar, in an empty state. Note that the supplied label must be above the current label and below the current clearance.

newEmptyLMVarP :: LabelState l p s => p -> l -> LIO l p s (LMVar l a)Source

Same as newEmptyLMVar except it takes a set of privileges which are accounted for in comparing the label of the MVar to the current label and clearance.

newLMVarSource

Arguments

:: LabelState l p s 
=> l

Label of LMVar

-> a

Initial value of LMVar

-> LIO l p s (LMVar l a)

New mutable location

Create a new labeled MVar, in an filled state with the supplied value. Note that the supplied label must be above the current label and below the current clearance.

newLMVarP :: LabelState l p s => p -> l -> a -> LIO l p s (LMVar l a)Source

Same as newLMVar except it takes a set of privileges which are accounted for in comparing the label of the MVar to the current label and clearance.

takeLMVar :: LabelState l p s => LMVar l a -> LIO l p s aSource

Return contents of the LMVar. Note that a take consists of a read and a write, since it observes whether or not the LMVar is full, and thus the current label must be the same as that of the LMVar (of course, this is not the case when using privileges). Hence, if the label of the LMVar is below the current clearance, we raise the current label to the join of the current label and the label of the MVar and read the contents of the MVar. If the LMVar is empty, takeLMVar blocks.

takeLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s aSource

Same as takeLMVar except takeLMVarP takes a privilege object which is used when the current label is raised.

putLMVarSource

Arguments

:: LabelState l p s 
=> LMVar l a

Source LMVar

-> a

New value

-> LIO l p s () 

Puts a value into an LMVar. Note that a put consists of a read and a write, since it observes whether or not the LMVar is empty, and so the current label must be the same as that of the LMVar (of course, this is not the case when using privileges). As in the takeLMVar case, if the label of the LMVar is below the current clearance, we raise the current label to the join of the current label and the label of the MVar and put the value into the MVar. If the LMVar is full, putLMVar blocks.

putLMVarP :: LabelState l p s => p -> LMVar l a -> a -> LIO l p s ()Source

Same as putLMVar except putLMVarP takes a privilege object which is used when the current label is raised.

readLMVar :: LabelState l p s => LMVar l a -> LIO l p s aSource

Combination of takeLMVar and putLMVar. Read the value, and just put it back. As specified for readMVar, this operation is atomic iff there is no other thread calling putLMVar for this LMVar.

readLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s aSource

Same as readLMVar except readLMVarP takes a privilege object which is used when the current label is raised.

swapLMVarSource

Arguments

:: LabelState l p s 
=> LMVar l a

Source LMVar

-> a

New value

-> LIO l p s a

Taken value

Takes a value from an LMVar, puts a new value into the LMvar, and returns the taken value. Like the other LMVar operations it is required that the label of the LMVar be above the current label and below the current clearance. Moreover, the current label is raised to accommodate for the observation. This operation is atomic iff there is no other thread calling putLMVar for this LMVar.

swapLMVarP :: LabelState l p s => p -> LMVar l a -> a -> LIO l p s aSource

Same as swapLMVar except swapLMVarP takes a privilege object which is used when the current label is raised.

tryTakeLMVar :: LabelState l p s => LMVar l a -> LIO l p s (Maybe a)Source

Non-blocking version of takeLMVar. It returns Nothing if the LMVar is empty, otherwise it returns Just value, emptying the LMVar.

tryTakeLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s (Maybe a)Source

Same as tryTakeLMVar, but uses priviliges when raising current label.

tryPutLMVar :: LabelState l p s => LMVar l a -> a -> LIO l p s BoolSource

Non-blocking version of putLMVar. It returns True if the LMVar was empty and the put succeeded, otherwise it returns False.

tryPutLMVarP :: LabelState l p s => p -> LMVar l a -> a -> LIO l p s BoolSource

Same as tryPutLMVar, but uses privileges when raising current label.

isEmptyLMVar :: LabelState l p s => LMVar l a -> LIO l p s BoolSource

Check the status of an LMVar, i.e., whether it is empty. The function succeeds if the label of the LMVar is below the current clearance -- the current label is raised to the join of the LMVar label and the current label. Note that this function only returns a snapshot of the state.

isEmptyLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s BoolSource

Same as isEmptyLMVar, but uses privileges when raising current label.

withLMVar :: LabelState l p s => LMVar l a -> (a -> LIO l p s b) -> LIO l p s bSource

Exception-safe wrapper for working with an LMVar. The original contents of the LMVar will be restored if the supplied action throws an exception. The function is atomic only if there is no other thread that performs a putLMVar.

withLMVarP :: LabelState l p s => p -> LMVar l a -> (a -> LIO l p s b) -> LIO l p s bSource

Same as withLMVar, but uses privileges when performing label comparisons/raises.

Unsafe (TCB) Functions

newEmptyLMVarTCB :: LabelState l p s => l -> LIO l p s (LMVar l a)Source

Trusted function used to create an empty LMVar, ignoring IFC.

newLMVarTCB :: LabelState l p s => l -> a -> LIO l p s (LMVar l a)Source

Trusted function used to create an LMVar with the supplied value, ignoring IFC.

takeLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s aSource

Read the contents of an LMVar, ignoring IFC.

putLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s ()Source

Put a value into an LMVar, ignoring IFC.

readLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s aSource

Trusted function used to read (take and put) an LMVar, ignoring IFC.

swapLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s aSource

Trusted function that swaps value of LMVar, ignoring IFC.

tryTakeLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s (Maybe a)Source

Same as tryTakeLMVar, but ignorses IFC.

tryPutLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s BoolSource

Same as tryPutLMVar, but ignorses IFC.

isEmptyLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s BoolSource

Same as isEmptyLMVar, but ignorses IFC.

withLMVarTCB :: LabelState l p s => LMVar l a -> (a -> LIO l p s b) -> LIO l p s bSource

Same as withLMVar, but ignores IFC.