1% 2% Copyright 2014, General Dynamics C4 Systems 3% 4% This software may be distributed and modified according to the terms of 5% the GNU General Public License version 2. Note that NO WARRANTY is provided. 6% See "LICENSE_GPLv2.txt" for details. 7% 8% @TAG(GD_GPL) 9% 10 11This module specifies the behavior of notification objects. 12 13> module SEL4.Object.Notification ( 14> sendSignal, receiveSignal, 15> cancelAllSignals, cancelSignal, completeSignal, 16> getNotification, setNotification, doUnbindNotification, unbindNotification, 17> unbindMaybeNotification, bindNotification, doNBRecvFailedTransfer 18> ) where 19 20\begin{impdetails} 21 22> import Prelude hiding (Word) 23> import SEL4.Machine 24> import SEL4.Model 25> import SEL4.Object.Structures 26> import {-# SOURCE #-} SEL4.Object.Endpoint(cancelIPC) 27> import {-# SOURCE #-} SEL4.Object.TCB(asUser) 28> import SEL4.Object.Instances() 29 30> import {-# SOURCE #-} SEL4.Kernel.Thread 31 32> import Data.Bits 33> import Data.List 34 35\end{impdetails} 36 37\subsection{Sending Signals} 38 39> -- helper function 40> receiveBlocked :: ThreadState -> Bool 41> receiveBlocked st = case st of 42> BlockedOnReceive _ -> True 43> _ -> False 44 45This function performs an signal operation, given a capability to a notification object, and a single machine word of message data (the badge). This operation will never block the signalling thread. 46 47> sendSignal :: PPtr Notification -> Word -> Kernel () 48 49> sendSignal ntfnPtr badge = do 50 51Fetch the notification object object, and select the operation based on its state. 52 53> nTFN <- getNotification ntfnPtr 54> case (ntfnObj nTFN, ntfnBoundTCB nTFN) of 55 56If the notification object is idle, store the badge and the value, and then 57mark the notification object as active. 58 59> (IdleNtfn, Just tcb) -> do 60> state <- getThreadState tcb 61> if (receiveBlocked state) 62> then do 63> cancelIPC tcb 64> setThreadState Running tcb 65> asUser tcb $ setRegister badgeRegister badge 66> possibleSwitchTo tcb 67> else 68> setNotification ntfnPtr $ nTFN { ntfnObj = ActiveNtfn badge } 69> (IdleNtfn, Nothing) -> setNotification ntfnPtr $ nTFN { ntfnObj = ActiveNtfn badge } 70 71If the notification object is waiting, a thread is removed from its queue and the signal is transferred to it. 72 73> (WaitingNtfn (dest:queue), _) -> do 74> setNotification ntfnPtr $ nTFN { 75> ntfnObj = case queue of 76> [] -> IdleNtfn 77> _ -> WaitingNtfn queue 78> } 79> setThreadState Running dest 80> asUser dest $ setRegister badgeRegister badge 81> possibleSwitchTo dest 82> (WaitingNtfn [], _) -> fail "WaitingNtfn Notification must have non-empty queue" 83 84If the notification object is active, new values are calculated and stored in the notification object. The calculation is done by a bitwise OR operation of the currently stored, and the newly sent values. 85 86> (ActiveNtfn badge', _) -> do 87> let newBadge = badge .|. badge' 88> setNotification ntfnPtr $ nTFN { ntfnObj = ActiveNtfn newBadge } 89 90\subsection{Receiving Signals} 91 92This function performs an receive signal operation, given a thread pointer and a capability to a notification object. The receive can be either blocking (the thread will be blocked on the notification until a signal arrives) or non-blocking depending on the isBlocking flag. 93 94> doNBRecvFailedTransfer :: PPtr TCB -> Kernel () 95> doNBRecvFailedTransfer thread = asUser thread $ setRegister badgeRegister 0 96 97 98> receiveSignal :: PPtr TCB -> Capability -> Bool -> Kernel () 99 100> receiveSignal thread cap isBlocking = do 101 102Fetch the notification object, and select the operation based on its state. 103 104> let ntfnPtr = capNtfnPtr cap 105> ntfn <- getNotification ntfnPtr 106> case ntfnObj ntfn of 107 108If the notification object is idle, then it becomes a waiting notification object, with the current thread in its queue. The thread is blocked. 109 110> IdleNtfn -> case isBlocking of 111> True -> do 112> setThreadState (BlockedOnNotification { 113> waitingOnNotification = ntfnPtr } ) thread 114> setNotification ntfnPtr $ ntfn {ntfnObj = WaitingNtfn ([thread]) } 115> False -> doNBRecvFailedTransfer thread 116 117If the notification object is already waiting, the current thread is blocked and added to the queue. Note that this case cannot occur when the notification object is bound, as only the associated thread can wait on it. 118 119> WaitingNtfn queue -> case isBlocking of 120> True -> do 121> setThreadState (BlockedOnNotification { 122> waitingOnNotification = ntfnPtr } ) thread 123> setNotification ntfnPtr $ ntfn {ntfnObj = WaitingNtfn (queue ++ [thread]) } 124> False -> doNBRecvFailedTransfer thread 125 126If the notification object is active, the badge of the invoked notification object capability will be loaded to the badge of the receiving thread and the notification object will be marked as idle. 127 128> ActiveNtfn badge -> do 129> asUser thread $ setRegister badgeRegister badge 130> setNotification ntfnPtr $ ntfn {ntfnObj = IdleNtfn } 131 132\subsection{Delete Operation} 133 134If a notification object is deleted, then pending receive operations must be cancelled. 135 136> cancelAllSignals :: PPtr Notification -> Kernel () 137> cancelAllSignals ntfnPtr = do 138> ntfn <- getNotification ntfnPtr 139> case ntfnObj ntfn of 140> WaitingNtfn queue -> do 141> setNotification ntfnPtr (ntfn { ntfnObj = IdleNtfn }) 142> forM_ queue (\t -> do 143> setThreadState Restart t 144> tcbSchedEnqueue t) 145> rescheduleRequired 146> _ -> return () 147 148The following function will remove the given thread from the queue of the notification object, and replace the thread's IPC block with a fault block (which will retry the operation if the thread is resumed). 149 150> cancelSignal :: PPtr TCB -> PPtr Notification -> Kernel () 151> cancelSignal threadPtr ntfnPtr = do 152> ntfn <- getNotification ntfnPtr 153> assert (isWaiting (ntfnObj ntfn)) 154> "cancelSignal: notification object must be waiting" 155> let queue' = delete threadPtr $ ntfnQueue $ ntfnObj ntfn 156> ntfn' <- case queue' of 157> [] -> return $ IdleNtfn 158> _ -> return $ (ntfnObj ntfn) { ntfnQueue = queue' } 159> setNotification ntfnPtr (ntfn { ntfnObj = ntfn' }) 160> setThreadState Inactive threadPtr 161> where 162> isWaiting ntfn = case ntfn of 163> WaitingNtfn {} -> True 164> _ -> False 165 166> completeSignal :: PPtr Notification -> PPtr TCB -> Kernel () 167> completeSignal ntfnPtr tcb = do 168> ntfn <- getNotification ntfnPtr 169> case ntfnObj ntfn of 170> ActiveNtfn badge -> do 171> asUser tcb $ setRegister badgeRegister badge 172> setNotification ntfnPtr $ ntfn {ntfnObj = IdleNtfn} 173> _ -> fail "tried to complete signal with inactive notification object" 174 175 176\subsection{Accessing Notification Objects} 177 178The following functions are specialisations of the "getObject" and "setObject" for the "Notification" object and pointer type. 179 180> getNotification :: PPtr Notification -> Kernel Notification 181> getNotification = getObject 182 183> setNotification :: PPtr Notification -> Notification -> Kernel () 184> setNotification = setObject 185 186 187\subsection{Miscellaneous} 188 189> bindNotification :: PPtr TCB -> PPtr Notification -> Kernel () 190> bindNotification tcb ntfnPtr = do 191> -- set the bound tcb inside the ntfn 192> ntfn <- getNotification ntfnPtr 193> setNotification ntfnPtr $ ntfn { ntfnBoundTCB = Just tcb } 194> -- set the bound ntfn inside the thread 195> setBoundNotification (Just ntfnPtr) tcb 196 197> doUnbindNotification :: PPtr Notification -> Notification -> PPtr TCB -> Kernel () 198> doUnbindNotification ntfnPtr ntfn tcbptr = do 199> let ntfn' = ntfn { ntfnBoundTCB = Nothing } 200> setNotification ntfnPtr ntfn' 201> setBoundNotification Nothing tcbptr 202 203> unbindNotification :: PPtr TCB -> Kernel () 204> unbindNotification tcb = do 205> ntfnPtr <- getBoundNotification tcb 206> case ntfnPtr of 207> Just ntfnPtr' -> do 208> ntfn <- getNotification ntfnPtr' 209> doUnbindNotification ntfnPtr' ntfn tcb 210> Nothing -> return () 211 212> unbindMaybeNotification :: PPtr Notification -> Kernel () 213> unbindMaybeNotification ntfnPtr = do 214> ntfn <- getNotification ntfnPtr 215> case ntfnBoundTCB ntfn of 216> Just t -> doUnbindNotification ntfnPtr ntfn t 217> Nothing -> return () 218 219 220