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