This module provides an implementation for labeled MVars. A labeled
MVar, of type
, is a mutable location that can be in
of of two states; an LMVar
l aLMVar
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 LIORef
s (see LIO.LIORef), this label
is static and does not change according to the content placed into
the location.
LMVar
s can be used to build synchronization primitives and
communication channels (LMVar
s themselves are single-place
channels). We refer to Control.Concurrent.MVar for the full
documentation on MVars.
- data LMVar l a
- labelOfLMVar :: Label l => LMVar l a -> l
- newEmptyLMVar :: LabelState l p s => l -> LIO l p s (LMVar l a)
- newEmptyLMVarP :: LabelState l p s => p -> l -> LIO l p s (LMVar l a)
- newLMVar :: LabelState l p s => l -> a -> LIO l p s (LMVar l a)
- newLMVarP :: LabelState l p s => p -> l -> a -> LIO l p s (LMVar l a)
- takeLMVar :: LabelState l p s => LMVar l a -> LIO l p s a
- takeLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s a
- putLMVar :: LabelState l p s => LMVar l a -> a -> LIO l p s ()
- putLMVarP :: LabelState l p s => p -> LMVar l a -> a -> LIO l p s ()
- readLMVar :: LabelState l p s => LMVar l a -> LIO l p s a
- readLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s a
- swapLMVar :: LabelState l p s => LMVar l a -> a -> LIO l p s a
- swapLMVarP :: LabelState l p s => p -> LMVar l a -> a -> LIO l p s a
- tryTakeLMVar :: LabelState l p s => LMVar l a -> LIO l p s (Maybe a)
- tryTakeLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s (Maybe a)
- tryPutLMVar :: LabelState l p s => LMVar l a -> a -> LIO l p s Bool
- tryPutLMVarP :: LabelState l p s => p -> LMVar l a -> a -> LIO l p s Bool
- isEmptyLMVar :: LabelState l p s => LMVar l a -> LIO l p s Bool
- isEmptyLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s Bool
- withLMVar :: LabelState l p s => LMVar l a -> (a -> LIO l p s b) -> LIO l p s b
- withLMVarP :: LabelState l p s => p -> LMVar l a -> (a -> LIO l p s b) -> LIO l p s b
- newEmptyLMVarTCB :: LabelState l p s => l -> LIO l p s (LMVar l a)
- newLMVarTCB :: LabelState l p s => l -> a -> LIO l p s (LMVar l a)
- takeLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s a
- putLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s ()
- readLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s a
- swapLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s a
- tryTakeLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s (Maybe a)
- tryPutLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s Bool
- isEmptyLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s Bool
- withLMVarTCB :: LabelState l p s => LMVar l a -> (a -> LIO l p s b) -> LIO l p s b
Basic Functions
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.
:: LabelState l p s | |
=> l | Label of |
-> 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.
:: LabelState l p s | |
=> l | Label of |
-> a | Initial value of |
-> 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.
:: LabelState l p s | |
=> LMVar l a | Source |
-> 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
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.
:: LabelState l p s | |
=> LMVar l a | Source |
-> 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
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
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
isEmptyLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s BoolSource
Same as isEmptyLMVar
, but uses privileges when raising current label.
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.