1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7#pragma once
8#include <autoconf.h>
9
10/**
11 * @defgroup MCSSystemCalls MCS System Calls
12 * @{
13 */
14
15/**
16 * @xmlonly <manual name="Send" label="sel4_mcs_send"/> @endxmlonly
17 * @brief Send to a capability
18 *
19 * @xmlonly
20 * <docref>See <autoref label="sec:sys_send"/></docref>
21 * @endxmlonly
22 *
23 * @param[in] dest The capability to be invoked.
24 * @param[in] msgInfo The messageinfo structure for the IPC.
25 */
26LIBSEL4_INLINE_FUNC void
27seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
28
29/**
30 * @xmlonly <manual name="Recv" label="sel4_mcs_recv"/> @endxmlonly
31 * @brief Block until a message is received on an endpoint
32 *
33 * @xmlonly
34 * <docref>See <autoref label="sec:sys_recv"/></docref>
35 * @endxmlonly
36 *
37 * @param[in] src The capability to be invoked.
38 * @param[out] sender The address to write sender information to.
39 *               The sender information is the badge of the
40 *               endpoint capability that was invoked by the
41 *               sender, or the notification word of the
42 *               notification object that was signalled.
43 *               This parameter is ignored if `NULL`.
44 * @param[in] reply The capability to the reply object to use on a call (only used on MCS).
45 *
46 * @return A `seL4_MessageInfo_t` structure
47 * @xmlonly
48 * <docref>as described in <autoref label="sec:messageinfo"/></docref>
49 * @endxmlonly
50 */
51LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
52seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply);
53
54/**
55 * @xmlonly <manual name="Call" label="sel4_mcs_call"/> @endxmlonly
56 * @brief  Call a capability
57 *
58 * @xmlonly
59 * <docref>See <autoref label="sec:sys_call"/></docref>
60 * @endxmlonly
61 *
62 * @param[in] dest The capability to be invoked.
63 * @param[in] msgInfo The messageinfo structure for the IPC.
64 *
65 * @return A `seL4_MessageInfo_t` structure
66 * @xmlonly
67 * <docref>as described in <autoref label="sec:messageinfo"/></docref>
68 * @endxmlonly
69 */
70LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
71seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
72
73
74/**
75 * @xmlonly <manual name="Non-Blocking Send" label="sel4_mcs_nbsend"/> @endxmlonly
76 * @brief Perform a non-blocking send to a capability
77 *
78 * @xmlonly
79 * <docref>See <autoref label="sec:sys_nbsend"/></docref>
80 * @endxmlonly
81 *
82 * @param[in] dest The capability to be invoked.
83 * @param[in] msgInfo The messageinfo structure for the IPC.
84 */
85LIBSEL4_INLINE_FUNC void
86seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
87
88
89/**
90 * @xmlonly <manual name="Reply Recv" label="sel4_mcs_replyrecv"/> @endxmlonly
91 * @brief Perform a reply followed by a receive in one system call
92 *
93 * @xmlonly
94 * <docref>See <autoref label="sec:sys_replyrecv"/></docref>
95 * @endxmlonly
96 *
97 * @param[in] src The capability to perform the receive on.
98 * @param[in] msgInfo The messageinfo structure for the IPC.
99 * @param[out] sender The address to write sender information to.
100 *               The sender information is the badge of the
101 *               endpoint capability that was invoked by the
102 *               sender, or the notification word of the
103 *               notification object that was signalled.
104 *               This parameter is ignored if `NULL`.
105 *
106 * @param[in] reply The capability to the reply object, which is first invoked and then used
107 *                  for the recv phase to store a new reply capability.
108 * @return A `seL4_MessageInfo_t` structure
109 * @xmlonly
110 * <docref>as described in <autoref label="sec:messageinfo"/></docref>
111 * @endxmlonly
112 */
113LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
114seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_CPtr reply);
115
116/**
117 * @xmlonly <manual name="NBRecv" label="sel4_mcs_nbrecv"/> @endxmlonly
118 * @brief Receive a message from an endpoint but do not block
119 *        in the case that no messages are pending
120 *
121 * @xmlonly
122 * <docref>See <autoref label="sec:sys_nbrecv"/></docref>
123 * @endxmlonly
124 *
125 * @param[in] src The capability to receive on.
126 * @param[out] sender The address to write sender information to.
127 *                    The sender information is the badge of the
128 *                    endpoint capability that was invoked by the
129 *                    sender, or the notification word of the
130 *                    notification object that was signalled.
131 *                    This parameter is ignored if `NULL`.
132 * @param[in] reply The capability to the reply object to use on a call.
133 *
134 * @return A `seL4_MessageInfo_t` structure
135 * @xmlonly
136 * <docref>as described in <autoref label="sec:messageinfo"/></docref>
137 * @endxmlonly
138 */
139LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
140seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply);
141
142/**
143 * @xmlonly <manual name="NBSend Recv" label="sel4_nbsendrecv"/> @endxmlonly
144 * @brief Non-blocking send on one capability, and a blocking recieve on another in a single
145 *        system call.
146 *
147 * @xmlonly
148 * <docref>See <autoref label="sec:sys_nbsendrecv"/></docref>
149 * @endxmlonly
150 *
151 * @param[in] dest The capability to be invoked.
152 * @param[in] msgInfo The messageinfo structure for the IPC.
153 * @param[out] sender The address to write sender information to.
154 *               The sender information is the badge of the
155 *               endpoint capability that was invoked by the
156 *               sender, or the notification word of the
157 *               notification object that was signalled.
158 *               This parameter is ignored if `NULL`.
159 * @param[in] src The capability to receive on.
160 * @param[in] reply The capability to the reply object, which is first invoked and then used
161 *                  for the recv phase to store a new reply capability.
162 * @return A `seL4_MessageInfo_t` structure
163 * @xmlonly
164 * as described in <autoref label="sec:messageinfo"/>
165 * @endxmlonly
166 */
167LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
168seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply);
169
170/**
171 * @xmlonly <manual name="NBSend Wait" label="sel4_nbsendwait"/> @endxmlonly
172 * @brief Non-blocking invoke of a capability and wait on another in one system call
173 *
174 * @xmlonly
175 * <docref>See <autoref label="sec:sys_nbsendwait"/></docref>
176 * @endxmlonly
177 *
178 * @param[in] dest The capability to be invoked.
179 * @param[in] msgInfo The messageinfo structure for the IPC.
180 * @param[out] sender The address to write sender information to.
181 *               The sender information is the badge of the
182 *               endpoint capability that was invoked by the
183 *               sender, or the notification word of the
184 *               notification object that was signalled.
185 *               This parameter is ignored if `NULL`.
186 * @param[in] src The capability to receive on.
187 * @return A `seL4_MessageInfo_t` structure
188 * @xmlonly
189 * as described in <autoref label="sec:messageinfo"/>
190 * @endxmlonly
191 */
192LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
193seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender);
194
195/**
196 * @xmlonly <manual name="Yield" label="sel4_mcs_yield"/> @endxmlonly
197 * @brief Yield the remaining timeslice. Periodic threads will not be scheduled again until their
198 *        next sporadic replenishment.
199 *
200 * @xmlonly
201 * <docref>See <autoref label="sec:sys_yield"/></docref>
202 * @endxmlonly
203 */
204LIBSEL4_INLINE_FUNC void
205seL4_Yield(void);
206
207/**
208 * @xmlonly <manual name="Wait" label="sel4_mcs_wait"/> @endxmlonly
209 * @brief Perform a wait on an endpoint or notification object
210 *
211 * Block on a notification or endpoint waiting for a message. No reply object is
212 * required for a Wait. Wait should not be paired with Call, as it does not provide
213 * a reply object. If Wait is paired with a Call the waiter will block after recieving
214 * the message.
215 *
216 * @xmlonly
217 * <docref>See the description of <nameref name="seL4_Wait"/> in <autoref label="sec:sys_wait"/>.</docref>
218 * @endxmlonly
219 *
220 * @param[in] src The capability to be invoked.
221 * @param[out] sender The address to write sender information to.
222 *               The sender information is the badge of the
223 *               endpoint capability that was invoked by the
224 *               sender, or the notification word of the
225 *               notification object that was signalled.
226 *               This parameter is ignored if `NULL`.
227 */
228LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
229seL4_Wait(seL4_CPtr src, seL4_Word *sender);
230
231/**
232 * @xmlonly <manual name="NBWait" label="sel4_nbwait"/> @endxmlonly
233 * @brief Perform a polling wait on an endpoint or notification object
234 *
235 * Poll a notification or endpoint waiting for a message. No reply object is
236 * required for a Wait. Wait should not be paired with Call.
237 *
238 * @xmlonly
239 * <docref>See the description of <nameref name="seL4_NBWait"/> in <autoref label="sec:sys_nbwait"/>.</docref>
240 * @endxmlonly
241 *
242 * @param[in] src The capability to be invoked.
243 * @param[out] sender The address to write sender information to.
244 *               The sender information is the badge of the
245 *               endpoint capability that was invoked by the
246 *               sender, or the notification word of the
247 *               notification object that was signalled.
248 *               This parameter is ignored if `NULL`.
249 */
250LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
251seL4_NBWait(seL4_CPtr src, seL4_Word *sender);
252
253/**
254 * @xmlonly <manual name="Poll" label="sel4_mcs_poll"/> @endxmlonly
255 * @brief Perform a non-blocking recv on a notification object
256 *
257 * This is not a proper system call known by the kernel. Rather, it is a
258 * convenience wrapper which calls seL4_NBWait().
259 * It is useful for doing a non-blocking wait on a notification.
260 *
261 * @xmlonly
262 * <docref>See the description of <nameref name="seL4_NBWait"/> in <autoref label="sec:sys_nbwait"/>.</docref>
263 * @endxmlonly
264 *
265 * @param[in] src The capability to be invoked.
266 * @param[out] sender The address to write sender information to.
267 *               The sender information is the badge of the
268 *               endpoint capability that was invoked by the
269 *               sender, or the notification word of the
270 *               notification object that was signalled.
271 *               This parameter is ignored if `NULL`.
272 *
273 * @return A `seL4_MessageInfo_t` structure
274 * @xmlonly
275 * <docref>as described in <autoref label="sec:messageinfo"/></docref>
276 * @endxmlonly
277 */
278LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
279seL4_Poll(seL4_CPtr src, seL4_Word *sender);
280
281/**
282 * @xmlonly <manual name="Signal" label="sel4_mcs_signal"/> @endxmlonly
283 * @brief Signal a notification
284 *
285 * This is not a proper system call known by the kernel. Rather, it is a
286 * convenience wrapper which calls seL4_Send().
287 * It is useful for signalling a notification.
288 *
289 * @xmlonly
290 * <docref>See the description of <nameref name="seL4_Send"/> in <autoref label="sec:sys_send"/>.</docref>
291 * @endxmlonly
292 *
293 * @param[in] dest The capability to be invoked.
294 */
295LIBSEL4_INLINE_FUNC void
296seL4_Signal(seL4_CPtr dest);
297
298/** @} */
299
300