lio 0.11.4.2 → 0.11.5.0
raw patch · 6 files changed
+155/−25 lines, 6 files
Files
- LIO/Concurrent/LChan.hs +85/−0
- LIO/Concurrent/LMVar.hs +3/−8
- LIO/LIORef.hs +6/−15
- LIO/TCB/LObj.hs +35/−1
- examples/channel.hs +23/−0
- lio.cabal +3/−1
+ LIO/Concurrent/LChan.hs view
@@ -0,0 +1,85 @@+{-# LANGUAGE Trustworthy #-}++{- |++Unbounded FIFO channels in the 'LIO' monad. As with other objects in+LIO, a channel has an associated label that is used to impose+restrictions on its operations. In fact, labeled channels ('LChan's)+are simply labeled 'Chan's with read and write access restricted+according to the label. This module is analogous to+"Control.Concurrent.Chan", but the operations take place in the 'LIO'+monad.++-}++module LIO.Concurrent.LChan (+ LChan+ -- * Basic Functions+ -- ** Create labeled 'IORef's+ , newLChan, newLChanP+ -- ** Read 'LChan's+ , readLChan, readLChanP+ -- ** Write 'LChan's+ , writeLChan, writeLChanP+ -- ** Dupicate 'LChan's+ , dupLChan, dupLChanP+ ) where++import safe Control.Concurrent.Chan++import safe LIO.Core+import safe LIO.Error+import safe LIO.Label+import LIO.TCB.LObj++-- | A @LChan@ is a labeled channel, i.e., an unbounded FIFO channel.+type LChan l a = LObj l (Chan a)+++-- | Create a new labeled channel. Note that the supplied label must+-- be above the current label and below the current clearance. An+-- exception will be thrown by the underlying 'guardAlloc' if this is+-- not the case.+newLChan :: Label l => l -> LIO l (LChan l a)+newLChan l = guardIOTCB (withContext "newLChan" $ guardAlloc l) $+ LObjTCB l `fmap` newChan++-- | Same as 'newLChan' except it takes a set of privileges which are+-- accounted for in comparing the label of the Chan to the current label.+newLChanP :: PrivDesc l p => Priv p -> l -> LIO l (LChan l a)+newLChanP p l = guardIOTCB (withContext "newLChanP" $ guardAllocP p l) $+ LObjTCB l `fmap` newChan++-- | Write value to the labeled channel. The label of the channel must+-- be bounded by the current label and clearance.+writeLChan :: Label l => LChan l a -> a -> LIO l ()+writeLChan = blessWriteOnlyTCB "writeLChan" writeChan++-- | Same as 'writeLChan', but uses privileges when comparing the+-- current label to the label of the channel.+writeLChanP :: PrivDesc l p => Priv p -> LChan l a -> a -> LIO l ()+writeLChanP = blessWriteOnlyPTCB "writeLChanP" writeChan++-- | Read the next value from the channel. The current label is+-- raised to join of the channel label and current label. Howerver,+-- the label of the channel must be below the current clearance.+readLChan :: Label l => LChan l a -> LIO l a+readLChan = blessReadOnlyTCB "readLChan" readChan++-- | Same as 'readLChan', but takes a privilege object which is used+-- when the current label is raised to avoid over-taining the context.+readLChanP :: PrivDesc l p => Priv p -> LChan l a -> LIO l a+readLChanP = blessReadOnlyPTCB "readLChanP" readChan++-- | Duplicate labeled channel. The label of the channel must be+-- bounded by the current label and clearance.+dupLChan :: Label l => LChan l a -> LIO l (LChan l a)+dupLChan (LObjTCB l ch)= guardIOTCB (withContext "dupLChan" $ guardAlloc l) $+ LObjTCB l `fmap` dupChan ch++-- | Same as 'dupLChan', but uses privileges when comparing the+-- current label to the label of the channel.+dupLChanP :: PrivDesc l p => Priv p -> LChan l a -> LIO l (LChan l a)+dupLChanP p (LObjTCB l ch) = + guardIOTCB (withContext "dupLChanP" $ guardAllocP p l) $+ LObjTCB l `fmap` dupChan ch
LIO/Concurrent/LMVar.hs view
@@ -84,8 +84,7 @@ LObjTCB l `fmap` newMVar a -- | 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.+-- accounted for in comparing the label of the MVar to the current label. newLMVarP :: PrivDesc l p => Priv p -> l -> a -> LIO l (LMVar l a) newLMVarP p l a = guardIOTCB (withContext "newLMVarP" $ guardAllocP p l) $ LObjTCB l `fmap` newMVar a@@ -204,12 +203,8 @@ -- clearance -- the current label is raised to the join of the 'LMVar' -- label and the current label. isEmptyLMVar :: Label l => LMVar l a -> LIO l Bool-isEmptyLMVar (LObjTCB l m) =- guardIOTCB (withContext "isEmptyLMVar" $ taint l) $- isEmptyMVar m+isEmptyLMVar = blessReadOnlyTCB "isEmptyLMVar" isEmptyMVar -- | Same as 'isEmptyLMVar', but uses privileges when raising current label. isEmptyLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l Bool-isEmptyLMVarP p (LObjTCB l m) =- guardIOTCB (withContext "isEmptyLMVarP" $ taintP p l) $- isEmptyMVar m+isEmptyLMVarP = blessReadOnlyPTCB "isEmptyLMVarP" isEmptyMVar
LIO/LIORef.hs view
@@ -75,15 +75,13 @@ -- (introduced by the 'taint' guard) use 'labelOf' to check that a -- read will succeed. readLIORef :: Label l => LIORef l a -> LIO l a-readLIORef (LObjTCB l r) =- guardIOTCB (withContext "readLIORef" $ taint l) $ readIORef r+readLIORef = blessReadOnlyTCB "readLIORef" readIORef -- | Same as 'readLIORef', except @readLIORefP@ takes a privilege -- object which is used when the current label is raised (using -- 'taintP' instead of 'taint'). readLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> LIO l a-readLIORefP p (LObjTCB l r) =- guardIOTCB (withContext "readLIORefP" $ taintP p l) $ readIORef r+readLIORefP = blessReadOnlyPTCB "readLIORefP" readIORef -- -- Write 'LIORef's@@ -94,16 +92,13 @@ -- label of the reference can-flow-to the current clearance. Otherwise, -- an exception is raised by the underlying 'guardAlloc' guard. writeLIORef :: Label l => LIORef l a -> a -> LIO l ()-writeLIORef (LObjTCB l r) a =- guardIOTCB (withContext "writeLIORef" $ guardAlloc l) $ writeIORef r a+writeLIORef = blessWriteOnlyTCB "writeLIORef" writeIORef -- | Same as 'writeLIORef' except @writeLIORefP@ takes a set of -- privileges which are accounted for in comparing the label of the -- reference to the current label. writeLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> a -> LIO l ()-writeLIORefP p (LObjTCB l r) a =- guardIOTCB (withContext "writeLIORefP" $ guardAllocP p l) $- writeIORef r a+writeLIORefP = blessWriteOnlyPTCB "writeLIORefP" writeIORef -- -- Modify 'LIORef's@@ -121,17 +116,13 @@ => LIORef l a -- ^ Labeled reference -> (a -> a) -- ^ Modifier -> LIO l ()-modifyLIORef (LObjTCB l r) f =- guardIOTCB (withContext "modifyLIORef" $ guardAlloc l)- modifyIORef r f+modifyLIORef = blessWriteOnlyTCB "modifyLIORef" modifyIORef -- | Like 'modifyLIORef', but takes a privilege argument and guards -- execution with 'guardAllocP' instead of 'guardAlloc'. modifyLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> (a -> a) -> LIO l ()-modifyLIORefP p (LObjTCB l r) f =- guardIOTCB (withContext "modifyLIORefP" $ guardAllocP p l) $- modifyIORef r f+modifyLIORefP = blessWriteOnlyPTCB "modifyLIORefP" modifyIORef -- | Atomically modifies the contents of an 'LIORef'. It is required -- that the label of the reference be above the current label, but
LIO/TCB/LObj.hs view
@@ -28,7 +28,13 @@ -- -- Then application-specific trusted code can wrap a specific label -- around each 'Handle' using the 'LObjTCB' constructor.-module LIO.TCB.LObj (LObj(..), blessTCB, blessPTCB, GuardIO(..)) where+module LIO.TCB.LObj (+ LObj(..)+ , blessTCB, blessPTCB+ , blessWriteOnlyTCB, blessWriteOnlyPTCB+ , blessReadOnlyTCB, blessReadOnlyPTCB+ , GuardIO(..)+ ) where import safe Data.Typeable @@ -116,3 +122,31 @@ {-# INLINE blessPTCB #-} blessPTCB name io p (LObjTCB l a) = guardIOTCB (withContext name $ guardWriteP p l) (io a)++-- | Similar to 'blessTCB', but enforces the weaker restriction that the+-- action is write-only. When in doubt use 'blessTCB'.+blessWriteOnlyTCB :: (GuardIO l io lio, Label l) =>+ String -> (a -> io) -> (LObj l a) -> lio+{-# INLINE blessWriteOnlyTCB #-}+blessWriteOnlyTCB name io (LObjTCB l a) =+ guardIOTCB (withContext name $ guardAlloc l) (io a)++blessWriteOnlyPTCB :: (GuardIO l io lio, PrivDesc l p) =>+ String -> (a -> io) -> Priv p -> (LObj l a) -> lio+{-# INLINE blessWriteOnlyPTCB #-}+blessWriteOnlyPTCB name io p (LObjTCB l a) =+ guardIOTCB (withContext name $ guardAllocP p l) (io a)++-- | Similar to 'blessTCB', but enforces the weaker restriction that+-- the action is read-only. When in doubt use 'blessTCB'.+blessReadOnlyTCB :: (GuardIO l io lio, Label l) =>+ String -> (a -> io) -> (LObj l a) -> lio+{-# INLINE blessReadOnlyTCB #-}+blessReadOnlyTCB name io (LObjTCB l a) =+ guardIOTCB (withContext name $ taint l) (io a)++blessReadOnlyPTCB :: (GuardIO l io lio, PrivDesc l p) =>+ String -> (a -> io) -> Priv p -> (LObj l a) -> lio+{-# INLINE blessReadOnlyPTCB #-}+blessReadOnlyPTCB name io p (LObjTCB l a) =+ guardIOTCB (withContext name $ taintP p l) (io a)
+ examples/channel.hs view
@@ -0,0 +1,23 @@+module Main where ++import LIO+import LIO.DCLabel+import LIO.Concurrent+import LIO.Concurrent.LChan++import Control.Monad++import LIO.TCB (ioTCB)++main = evalDC $ do+ log <- newLChan ("Logger" %% True)+ forkLIO $ forever $ do+ msg <- readLChan log+ lcur <- getLabel+ ioTCB $ putStrLn $ show lcur ++ " > " ++ msg+ forkLIO $ do+ writeLChan log "in them alternate threads"+ forkLIO $ do+ taint ("Alice" %% True)+ writeLChan log "i has failed"+ forM_ [1..10] $ \i -> writeLChan log $ "yo "++ show i
lio.cabal view
@@ -1,5 +1,5 @@ Name: lio-Version: 0.11.4.2+Version: 0.11.5.0 Cabal-Version: >= 1.8 Build-type: Simple License: GPL@@ -56,6 +56,7 @@ examples/dclabel.hs examples/gate.hs examples/waitAndCatch.hs+ examples/channel.hs Source-repository head Type: git@@ -90,6 +91,7 @@ -- * Concurrency LIO.Concurrent LIO.Concurrent.LMVar+ LIO.Concurrent.LChan -- * DCLabels LIO.DCLabel -- * Privileged internals