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