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 contents and behaviour of a synchronous IPC endpoint. 12 13> module SEL4.Object.Endpoint ( 14> sendIPC, receiveIPC, 15> replyFromKernel, 16> cancelIPC, cancelAllIPC, cancelBadgedSends 17> ) where 18 19\begin{impdetails} 20 21% {-# BOOT-IMPORTS: SEL4.Machine SEL4.Model SEL4.Object.Structures #-} 22% {-# BOOT-EXPORTS: cancelIPC #-} 23 24> import Prelude hiding (Word) 25> import SEL4.API.Types 26> import SEL4.Machine 27> import SEL4.Model 28> import SEL4.Object.Structures 29> import SEL4.Object.Instances() 30> import SEL4.Object.Notification 31> import {-# SOURCE #-} SEL4.Object.CNode 32> import {-# SOURCE #-} SEL4.Object.TCB 33> import {-# SOURCE #-} SEL4.Kernel.Thread 34> import {-# SOURCE #-} SEL4.Kernel.VSpace 35 36> import Data.List 37> import Data.Maybe 38 39\end{impdetails} 40 41\subsection{Sending IPC} 42 43This function performs an IPC send operation, given a pointer to the sending thread, a capability to an endpoint, and possibly a fault that should be sent instead of a message from the thread. 44 45> sendIPC :: Bool -> Bool -> Word -> Bool -> PPtr TCB -> 46> PPtr Endpoint -> Kernel () 47 48The normal (blocking) version of the send operation will remove a recipient from the endpoint's queue if one is available, or otherwise add the sender to the queue. 49 50> sendIPC blocking call badge canGrant thread epptr = do 51> ep <- getEndpoint epptr 52> case ep of 53 54If the endpoint is idle, and this is a blocking IPC operation, then the current thread is queued in the endpoint, which changes to the sending state. The thread will block until a receive operation is performed on the endpoint. 55 56> IdleEP | blocking -> do 57> setThreadState (BlockedOnSend { 58> blockingObject = epptr, 59> blockingIPCBadge = badge, 60> blockingIPCCanGrant = canGrant, 61> blockingIPCIsCall = call }) thread 62> setEndpoint epptr $ SendEP [thread] 63 64If the endpoint is already in the sending state, and this is a blocking IPC operation, then the current thread is blocked and added to the queue. 65 66> SendEP queue | blocking -> do 67> setThreadState (BlockedOnSend { 68> blockingObject = epptr, 69> blockingIPCBadge = badge, 70> blockingIPCCanGrant = canGrant, 71> blockingIPCIsCall = call }) thread 72> setEndpoint epptr $ SendEP $ queue ++ [thread] 73 74A non-blocking IPC to an idle or sending endpoint will be silently dropped. 75 76> IdleEP -> return () 77> SendEP _ -> return () 78 79If the endpoint is receiving, then a thread is removed from its queue, and an IPC transfer is performed. If the recipient is the last thread in the endpoint's queue, the endpoint becomes idle. 80 81> RecvEP (dest:queue) -> do 82> setEndpoint epptr $ case queue of 83> [] -> IdleEP 84> _ -> RecvEP queue 85> recvState <- getThreadState dest 86> assert (isReceive recvState) 87> "TCB in receive endpoint queue must be blocked on send" 88> doIPCTransfer thread (Just epptr) badge canGrant 89> dest 90 91The receiving thread has now completed its blocking operation and can run. If the receiving thread has higher priority than the current thread, the scheduler is instructed to switch to it immediately. 92 93> setThreadState Running dest 94> possibleSwitchTo dest 95 96If the sender is performing a call or has faulted, set up the reply capability. 97 98> fault <- threadGet tcbFault thread 99> case (call, fault, canGrant) of 100> (False, Nothing, _) -> return () 101> (_, _, True) -> setupCallerCap thread dest 102> _ -> setThreadState Inactive thread 103 104Empty receive endpoints are invalid. 105 106> RecvEP [] -> fail "Receive endpoint queue must not be empty" 107 108\subsection{Receiving IPC} 109 110The IPC receive operation is essentially the same as the send operation, but with the send and receive states swapped. There are a few other differences: the badge must be retrieved from the TCB when completing an operation, and is not set when adding a TCB to the queue; also, the operation always blocks if no partner is immediately available; lastly, the receivers thread state does not need updating to Running however the senders state may. 111 112> isActive :: Notification -> Bool 113> isActive (NTFN (ActiveNtfn _) _) = True 114> isActive _ = False 115 116> receiveIPC :: PPtr TCB -> Capability -> Bool -> Kernel () 117> receiveIPC thread cap@(EndpointCap {}) isBlocking = do 118> let epptr = capEPPtr cap 119> ep <- getEndpoint epptr 120> -- check if anything is waiting on bound ntfn 121> ntfnPtr <- getBoundNotification thread 122> ntfn <- maybe (return $ NTFN IdleNtfn Nothing) (getNotification) ntfnPtr 123> if (isJust ntfnPtr && isActive ntfn) 124> then completeSignal (fromJust ntfnPtr) thread 125> else case ep of 126> IdleEP -> case isBlocking of 127> True -> do 128> setThreadState (BlockedOnReceive { 129> blockingObject = epptr }) thread 130> setEndpoint epptr $ RecvEP [thread] 131> False -> doNBRecvFailedTransfer thread 132> RecvEP queue -> case isBlocking of 133> True -> do 134> setThreadState (BlockedOnReceive { 135> blockingObject = epptr }) thread 136> setEndpoint epptr $ RecvEP $ queue ++ [thread] 137> False -> doNBRecvFailedTransfer thread 138> SendEP (sender:queue) -> do 139> setEndpoint epptr $ case queue of 140> [] -> IdleEP 141> _ -> SendEP queue 142> senderState <- getThreadState sender 143> assert (isSend senderState) 144> "TCB in send endpoint queue must be blocked on send" 145> let badge = blockingIPCBadge senderState 146> let canGrant = blockingIPCCanGrant senderState 147> doIPCTransfer sender (Just epptr) badge canGrant 148> thread 149> let call = blockingIPCIsCall senderState 150> fault <- threadGet tcbFault sender 151> case (call, fault, canGrant) of 152> (False, Nothing, _) -> do 153> setThreadState Running sender 154> possibleSwitchTo sender 155> (_, _, True) -> setupCallerCap sender thread 156> _ -> setThreadState Inactive sender 157> SendEP [] -> fail "Send endpoint queue must not be empty" 158 159> receiveIPC _ _ _ = fail "receiveIPC: invalid cap" 160 161\subsection{Kernel Invocation Replies} 162 163A system call reply from the kernel is an IPC transfer with no badge and no additional capabilities. The message registers are explicitly specified rather than coming from the sender's context. 164 165> replyFromKernel :: PPtr TCB -> (Word, [Word]) -> Kernel () 166> replyFromKernel thread (resultLabel, resultData) = do 167> destIPCBuffer <- lookupIPCBuffer True thread 168> asUser thread $ setRegister badgeRegister 0 169> len <- setMRs thread destIPCBuffer resultData 170> let msgInfo = MI { 171> msgLength = len, 172> msgExtraCaps = 0, 173> msgCapsUnwrapped = 0, 174> msgLabel = resultLabel } 175> setMessageInfo thread msgInfo 176 177\subsection{Cancelling IPC} 178 179If a thread is waiting for an IPC operation, it may be necessary to move the thread into a state where it is no longer waiting; for example if the thread is deleted. The following function, given a pointer to a thread, cancels any IPC that thread is involved in. 180 181> cancelIPC :: PPtr TCB -> Kernel () 182> cancelIPC tptr = do 183> state <- getThreadState tptr 184> case state of 185 186Threads blocked waiting for endpoints will simply be removed from the endpoint queue. 187 188> BlockedOnSend {} -> blockedIPCCancel state 189> BlockedOnReceive {} -> blockedIPCCancel state 190> BlockedOnNotification {} -> cancelSignal tptr (waitingOnNotification state) 191 192Threads that are waiting for an ipc reply or a fault response must have their reply capability revoked. 193 194> BlockedOnReply {} -> replyIPCCancel 195> _ -> return () 196> where 197 198If the thread is blocking on an endpoint, then the endpoint is fetched and the thread removed from its queue. 199 200> replyIPCCancel = do 201> threadSet (\tcb -> tcb {tcbFault = Nothing}) tptr 202> slot <- getThreadReplySlot tptr 203> callerCap <- liftM (mdbNext . cteMDBNode) $ getCTE slot 204> when (callerCap /= nullPointer) $ do 205> stateAssert (capHasProperty callerCap (\cap -> isReplyCap cap && 206> not (capReplyMaster cap))) 207> "replyIPCCancel: expected a reply cap" 208> cteDeleteOne callerCap 209> blockedIPCCancel state = do 210> let epptr = blockingObject state 211> ep <- getEndpoint epptr 212> assert (not $ isIdle ep) 213> "blockedIPCCancel: endpoint must not be idle" 214> let queue' = delete tptr $ epQueue ep 215> ep' <- case queue' of 216> [] -> return IdleEP 217> _ -> return $ ep { epQueue = queue' } 218> setEndpoint epptr ep' 219 220Finally, replace the IPC block with a fault block (which will retry the operation if the thread is resumed). 221 222> setThreadState Inactive tptr 223> isIdle ep = case ep of 224> IdleEP -> True 225> _ -> False 226 227If an endpoint is deleted, then every pending IPC operation using it must be cancelled. 228 229> cancelAllIPC :: PPtr Endpoint -> Kernel () 230> cancelAllIPC epptr = do 231> ep <- getEndpoint epptr 232> case ep of 233> IdleEP -> 234> return () 235> _ -> do 236> setEndpoint epptr IdleEP 237> forM_ (epQueue ep) (\t -> do 238> setThreadState Restart t 239> tcbSchedEnqueue t) 240> rescheduleRequired 241 242If a badged endpoint is recycled, then cancel every pending send operation using a badge equal to the recycled capability's badge. Receive operations are not affected. 243 244> cancelBadgedSends :: PPtr Endpoint -> Word -> Kernel () 245> cancelBadgedSends epptr badge = do 246> ep <- getEndpoint epptr 247> case ep of 248> IdleEP -> return () 249> RecvEP {} -> return () 250> SendEP queue -> do 251> setEndpoint epptr IdleEP 252> queue' <- (flip filterM queue) $ \t -> do 253> st <- getThreadState t 254> if blockingIPCBadge st == badge 255> then do 256> setThreadState Restart t 257> tcbSchedEnqueue t 258> return False 259> else return True 260> ep' <- case queue' of 261> [] -> return IdleEP 262> _ -> return $ SendEP { epQueue = queue' } 263> setEndpoint epptr ep' 264> rescheduleRequired 265 266\subsection{Accessing Endpoints} 267 268The following two functions are specialisations of "getObject" and 269"setObject" for the endpoint object and pointer types. 270 271> getEndpoint :: PPtr Endpoint -> Kernel Endpoint 272> getEndpoint = getObject 273 274> setEndpoint :: PPtr Endpoint -> Endpoint -> Kernel () 275> setEndpoint = setObject 276 277 278