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
9 #include <autoconf.h>
10 #include <sel4/functions.h>
11 #include <sel4/sel4_arch/syscalls.h>
12 #include <sel4/types.h>
13
14 #ifdef CONFIG_KERNEL_MCS
15 #define LIBSEL4_MCS_REPLY reply
16 #else
17 #define LIBSEL4_MCS_REPLY 0
18 #endif
19
seL4_Send(seL4_CPtr dest,seL4_MessageInfo_t msgInfo)20 LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
21 {
22 arm_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
23 }
24
seL4_SendWithMRs(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)25 LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
26 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
27 {
28 arm_sys_send(seL4_SysSend, dest, msgInfo.words[0],
29 mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
30 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
31 mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
32 mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
33 );
34 }
35
seL4_NBSend(seL4_CPtr dest,seL4_MessageInfo_t msgInfo)36 LIBSEL4_INLINE_FUNC void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
37 {
38 arm_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
39 }
40
seL4_NBSendWithMRs(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)41 LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
42 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
43 {
44 arm_sys_send(seL4_SysNBSend, dest, msgInfo.words[0],
45 mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
46 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
47 mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
48 mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
49 );
50 }
51
52 #ifndef CONFIG_KERNEL_MCS
seL4_Reply(seL4_MessageInfo_t msgInfo)53 LIBSEL4_INLINE_FUNC void seL4_Reply(seL4_MessageInfo_t msgInfo)
54 {
55 arm_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
56 }
57
seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)58 LIBSEL4_INLINE_FUNC void seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
59 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
60 {
61 arm_sys_reply(seL4_SysReply, msgInfo.words[0],
62 mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
63 mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
64 mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
65 mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
66 );
67 }
68 #endif
69
seL4_Signal(seL4_CPtr dest)70 LIBSEL4_INLINE_FUNC void seL4_Signal(seL4_CPtr dest)
71 {
72 arm_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]);
73 }
74
75
76 #ifdef CONFIG_KERNEL_MCS
seL4_Recv(seL4_CPtr src,seL4_Word * sender,seL4_CPtr reply)77 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
78 #else
79 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender)
80 #endif
81 {
82 seL4_MessageInfo_t info;
83 seL4_Word badge;
84 seL4_Word msg0;
85 seL4_Word msg1;
86 seL4_Word msg2;
87 seL4_Word msg3;
88
89 arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
90
91 seL4_SetMR(0, msg0);
92 seL4_SetMR(1, msg1);
93 seL4_SetMR(2, msg2);
94 seL4_SetMR(3, msg3);
95
96 /* Return back sender and message information. */
97 if (sender) {
98 *sender = badge;
99 }
100 return info;
101 }
102
103 #ifdef CONFIG_KERNEL_MCS
seL4_RecvWithMRs(seL4_CPtr src,seL4_Word * sender,seL4_CPtr reply,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)104 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply,
105 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
106 #else
107 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender,
108 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
109 #endif
110 {
111 seL4_MessageInfo_t info;
112 seL4_Word badge;
113 seL4_Word msg0 = 0;
114 seL4_Word msg1 = 0;
115 seL4_Word msg2 = 0;
116 seL4_Word msg3 = 0;
117
118 arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
119
120 /* Write the message back out to memory. */
121 if (mr0 != seL4_Null) {
122 *mr0 = msg0;
123 }
124 if (mr1 != seL4_Null) {
125 *mr1 = msg1;
126 }
127 if (mr2 != seL4_Null) {
128 *mr2 = msg2;
129 }
130 if (mr3 != seL4_Null) {
131 *mr3 = msg3;
132 }
133
134 /* Return back sender and message information. */
135 if (sender) {
136 *sender = badge;
137 }
138 return info;
139 }
140
141 #ifdef CONFIG_KERNEL_MCS
seL4_NBRecv(seL4_CPtr src,seL4_Word * sender,seL4_CPtr reply)142 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
143 #else
144 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender)
145 #endif
146 {
147 seL4_MessageInfo_t info;
148 seL4_Word badge;
149 seL4_Word msg0;
150 seL4_Word msg1;
151 seL4_Word msg2;
152 seL4_Word msg3;
153
154 arm_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
155
156 seL4_SetMR(0, msg0);
157 seL4_SetMR(1, msg1);
158 seL4_SetMR(2, msg2);
159 seL4_SetMR(3, msg3);
160
161 /* Return back sender and message information. */
162 if (sender) {
163 *sender = badge;
164 }
165 return info;
166 }
167
seL4_Call(seL4_CPtr dest,seL4_MessageInfo_t msgInfo)168 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
169 {
170 seL4_MessageInfo_t info;
171 seL4_Word msg0 = seL4_GetMR(0);
172 seL4_Word msg1 = seL4_GetMR(1);
173 seL4_Word msg2 = seL4_GetMR(2);
174 seL4_Word msg3 = seL4_GetMR(3);
175
176 arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
177
178 /* Write out the data back to memory. */
179 seL4_SetMR(0, msg0);
180 seL4_SetMR(1, msg1);
181 seL4_SetMR(2, msg2);
182 seL4_SetMR(3, msg3);
183
184 return info;
185 }
186
seL4_CallWithMRs(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)187 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
188 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
189 {
190 seL4_MessageInfo_t info;
191 seL4_Word msg0 = 0;
192 seL4_Word msg1 = 0;
193 seL4_Word msg2 = 0;
194 seL4_Word msg3 = 0;
195
196 /* Load beginning of the message into registers. */
197 if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
198 msg0 = *mr0;
199 }
200 if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
201 msg1 = *mr1;
202 }
203 if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
204 msg2 = *mr2;
205 }
206 if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
207 msg3 = *mr3;
208 }
209
210 arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
211
212 /* Write out the data back to memory. */
213 if (mr0 != seL4_Null) {
214 *mr0 = msg0;
215 }
216 if (mr1 != seL4_Null) {
217 *mr1 = msg1;
218 }
219 if (mr2 != seL4_Null) {
220 *mr2 = msg2;
221 }
222 if (mr3 != seL4_Null) {
223 *mr3 = msg3;
224 }
225
226 return info;
227 }
228
229 #ifdef CONFIG_KERNEL_MCS
seL4_ReplyRecv(seL4_CPtr src,seL4_MessageInfo_t msgInfo,seL4_Word * sender,seL4_CPtr reply)230 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
231 seL4_CPtr reply)
232 #else
233 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
234 #endif
235 {
236 seL4_MessageInfo_t info;
237 seL4_Word badge;
238 seL4_Word msg0;
239 seL4_Word msg1;
240 seL4_Word msg2;
241 seL4_Word msg3;
242
243 /* Load beginning of the message into registers. */
244 msg0 = seL4_GetMR(0);
245 msg1 = seL4_GetMR(1);
246 msg2 = seL4_GetMR(2);
247 msg3 = seL4_GetMR(3);
248
249 arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
250 LIBSEL4_MCS_REPLY);
251
252 /* Write the message back out to memory. */
253 seL4_SetMR(0, msg0);
254 seL4_SetMR(1, msg1);
255 seL4_SetMR(2, msg2);
256 seL4_SetMR(3, msg3);
257
258 /* Return back sender and message information. */
259 if (sender) {
260 *sender = badge;
261 }
262
263 return info;
264 }
265
266 #ifdef CONFIG_KERNEL_MCS
seL4_ReplyRecvWithMRs(seL4_CPtr src,seL4_MessageInfo_t msgInfo,seL4_Word * sender,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3,seL4_CPtr reply)267 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo,
268 seL4_Word *sender,
269 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
270 #else
271 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo,
272 seL4_Word *sender,
273 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
274 #endif
275 {
276 seL4_MessageInfo_t info;
277 seL4_Word badge;
278 seL4_Word msg0 = 0;
279 seL4_Word msg1 = 0;
280 seL4_Word msg2 = 0;
281 seL4_Word msg3 = 0;
282
283 if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
284 msg0 = *mr0;
285 }
286 if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
287 msg1 = *mr1;
288 }
289 if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
290 msg2 = *mr2;
291 }
292 if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
293 msg3 = *mr3;
294 }
295
296 arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
297 LIBSEL4_MCS_REPLY);
298
299 /* Write out the data back to memory. */
300 if (mr0 != seL4_Null) {
301 *mr0 = msg0;
302 }
303 if (mr1 != seL4_Null) {
304 *mr1 = msg1;
305 }
306 if (mr2 != seL4_Null) {
307 *mr2 = msg2;
308 }
309 if (mr3 != seL4_Null) {
310 *mr3 = msg3;
311 }
312
313 /* Return back sender and message information. */
314 if (sender) {
315 *sender = badge;
316 }
317
318 return info;
319 }
320
321 #ifdef CONFIG_KERNEL_MCS
seL4_NBSendRecv(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_CPtr src,seL4_Word * sender,seL4_CPtr reply)322 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
323 seL4_Word *sender, seL4_CPtr reply)
324 {
325 seL4_MessageInfo_t info;
326 seL4_Word badge;
327 seL4_Word msg0;
328 seL4_Word msg1;
329 seL4_Word msg2;
330 seL4_Word msg3;
331
332 /* Load beginning of the message into registers. */
333 msg0 = seL4_GetMR(0);
334 msg1 = seL4_GetMR(1);
335 msg2 = seL4_GetMR(2);
336 msg3 = seL4_GetMR(3);
337
338 arm_sys_nbsend_recv(seL4_SysNBSendRecv, dest, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
339 reply);
340
341 /* Write the message back out to memory. */
342 seL4_SetMR(0, msg0);
343 seL4_SetMR(1, msg1);
344 seL4_SetMR(2, msg2);
345 seL4_SetMR(3, msg3);
346
347 /* Return back sender and message information. */
348 if (sender) {
349 *sender = badge;
350 }
351
352 return info;
353 }
354
seL4_NBSendRecvWithMRs(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_CPtr src,seL4_Word * sender,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3,seL4_CPtr reply)355 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
356 seL4_Word *sender,
357 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
358 {
359 seL4_MessageInfo_t info;
360 seL4_Word badge;
361 seL4_Word msg0 = 0;
362 seL4_Word msg1 = 0;
363 seL4_Word msg2 = 0;
364 seL4_Word msg3 = 0;
365
366 if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
367 msg0 = *mr0;
368 }
369 if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
370 msg1 = *mr1;
371 }
372 if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
373 msg2 = *mr2;
374 }
375 if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
376 msg3 = *mr3;
377 }
378
379 arm_sys_nbsend_recv(seL4_SysNBSendRecv, dest, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
380 reply);
381
382 /* Write out the data back to memory. */
383 if (mr0 != seL4_Null) {
384 *mr0 = msg0;
385 }
386 if (mr1 != seL4_Null) {
387 *mr1 = msg1;
388 }
389 if (mr2 != seL4_Null) {
390 *mr2 = msg2;
391 }
392 if (mr3 != seL4_Null) {
393 *mr3 = msg3;
394 }
395
396 /* Return back sender and message information. */
397 if (sender) {
398 *sender = badge;
399 }
400
401 return info;
402 }
403
seL4_NBSendWait(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_CPtr src,seL4_Word * sender)404 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
405 seL4_Word *sender)
406 {
407 seL4_MessageInfo_t info;
408 seL4_Word badge;
409 seL4_Word msg0;
410 seL4_Word msg1;
411 seL4_Word msg2;
412 seL4_Word msg3;
413
414 /* Load beginning of the message into registers. */
415 msg0 = seL4_GetMR(0);
416 msg1 = seL4_GetMR(1);
417 msg2 = seL4_GetMR(2);
418 msg3 = seL4_GetMR(3);
419
420 arm_sys_nbsend_recv(seL4_SysNBSendWait, 0, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
421 dest);
422
423 /* Write the message back out to memory. */
424 seL4_SetMR(0, msg0);
425 seL4_SetMR(1, msg1);
426 seL4_SetMR(2, msg2);
427 seL4_SetMR(3, msg3);
428
429 /* Return back sender and message information. */
430 if (sender) {
431 *sender = badge;
432 }
433
434 return info;
435 }
436
seL4_NBSendWaitWithMRs(seL4_CPtr dest,seL4_MessageInfo_t msgInfo,seL4_CPtr src,seL4_Word * sender,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)437 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
438 seL4_Word *sender,
439 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
440 {
441 seL4_MessageInfo_t info;
442 seL4_Word badge;
443 seL4_Word msg0 = 0;
444 seL4_Word msg1 = 0;
445 seL4_Word msg2 = 0;
446 seL4_Word msg3 = 0;
447
448 if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
449 msg0 = *mr0;
450 }
451 if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
452 msg1 = *mr1;
453 }
454 if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
455 msg2 = *mr2;
456 }
457 if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
458 msg3 = *mr3;
459 }
460
461 arm_sys_nbsend_recv(seL4_SysNBSendRecv, 0, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
462 dest);
463
464 /* Write out the data back to memory. */
465 if (mr0 != seL4_Null) {
466 *mr0 = msg0;
467 }
468 if (mr1 != seL4_Null) {
469 *mr1 = msg1;
470 }
471 if (mr2 != seL4_Null) {
472 *mr2 = msg2;
473 }
474 if (mr3 != seL4_Null) {
475 *mr3 = msg3;
476 }
477
478 /* Return back sender and message information. */
479 if (sender) {
480 *sender = badge;
481 }
482
483 return info;
484 }
485 #endif
486
seL4_Yield(void)487 LIBSEL4_INLINE_FUNC void seL4_Yield(void)
488 {
489 arm_sys_null(seL4_SysYield);
490 asm volatile("" ::: "memory");
491 }
492
493 #ifdef CONFIG_KERNEL_MCS
seL4_Wait(seL4_CPtr src,seL4_Word * sender)494 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Wait(seL4_CPtr src, seL4_Word *sender)
495 {
496 seL4_MessageInfo_t info;
497 seL4_Word badge;
498 seL4_Word msg0;
499 seL4_Word msg1;
500 seL4_Word msg2;
501 seL4_Word msg3;
502
503 arm_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
504
505 seL4_SetMR(0, msg0);
506 seL4_SetMR(1, msg1);
507 seL4_SetMR(2, msg2);
508 seL4_SetMR(3, msg3);
509
510 /* Return back sender and message information. */
511 if (sender) {
512 *sender = badge;
513 }
514 return info;
515 }
516
seL4_WaitWithMRs(seL4_CPtr src,seL4_Word * sender,seL4_Word * mr0,seL4_Word * mr1,seL4_Word * mr2,seL4_Word * mr3)517 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_WaitWithMRs(seL4_CPtr src, seL4_Word *sender,
518 seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
519 {
520 seL4_MessageInfo_t info;
521 seL4_Word badge;
522 seL4_Word msg0 = 0;
523 seL4_Word msg1 = 0;
524 seL4_Word msg2 = 0;
525 seL4_Word msg3 = 0;
526
527 arm_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
528
529 /* Write the message back out to memory. */
530 if (mr0 != seL4_Null) {
531 *mr0 = msg0;
532 }
533 if (mr1 != seL4_Null) {
534 *mr1 = msg1;
535 }
536 if (mr2 != seL4_Null) {
537 *mr2 = msg2;
538 }
539 if (mr3 != seL4_Null) {
540 *mr3 = msg3;
541 }
542
543 /* Return back sender and message information. */
544 if (sender) {
545 *sender = badge;
546 }
547 return info;
548 }
549
seL4_NBWait(seL4_CPtr src,seL4_Word * sender)550 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBWait(seL4_CPtr src, seL4_Word *sender)
551 {
552 seL4_MessageInfo_t info;
553 seL4_Word badge;
554 seL4_Word msg0;
555 seL4_Word msg1;
556 seL4_Word msg2;
557 seL4_Word msg3;
558
559 arm_sys_recv(seL4_SysNBWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
560
561 seL4_SetMR(0, msg0);
562 seL4_SetMR(1, msg1);
563 seL4_SetMR(2, msg2);
564 seL4_SetMR(3, msg3);
565
566 /* Return back sender and message information. */
567 if (sender) {
568 *sender = badge;
569 }
570 return info;
571 }
572 #endif
573
574 #ifdef CONFIG_PRINTING
seL4_DebugPutChar(char c)575 LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
576 {
577 seL4_Word unused0 = 0;
578 seL4_Word unused1 = 0;
579 seL4_Word unused2 = 0;
580 seL4_Word unused3 = 0;
581 seL4_Word unused4 = 0;
582 seL4_Word unused5 = 0;
583
584 arm_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
585 }
586
seL4_DebugPutString(char * str)587 LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str)
588 {
589 for (char *s = str; *s; s++) {
590 seL4_DebugPutChar(*s);
591 }
592 return;
593 }
594
seL4_DebugDumpScheduler(void)595 LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
596 {
597 seL4_Word unused0 = 0;
598 seL4_Word unused1 = 0;
599 seL4_Word unused2 = 0;
600 seL4_Word unused3 = 0;
601 seL4_Word unused4 = 0;
602 seL4_Word unused5 = 0;
603
604 arm_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
605 }
606 #endif
607
608 #if CONFIG_DEBUG_BUILD
seL4_DebugHalt(void)609 LIBSEL4_INLINE_FUNC void seL4_DebugHalt(void)
610 {
611 arm_sys_null(seL4_SysDebugHalt);
612 }
613
seL4_DebugSnapshot(void)614 LIBSEL4_INLINE_FUNC void seL4_DebugSnapshot(void)
615 {
616 arm_sys_null(seL4_SysDebugSnapshot);
617 asm volatile("" ::: "memory");
618 }
619
seL4_DebugCapIdentify(seL4_CPtr cap)620 LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap)
621 {
622 seL4_Word unused0 = 0;
623 seL4_Word unused1 = 0;
624 seL4_Word unused2 = 0;
625 seL4_Word unused3 = 0;
626 seL4_Word unused4 = 0;
627
628 arm_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
629 return (seL4_Uint32)cap;
630 }
631
632 char *strcpy(char *, const char *);
seL4_DebugNameThread(seL4_CPtr tcb,const char * name)633 LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
634 {
635 strcpy((char *)seL4_GetIPCBuffer()->msg, name);
636
637 seL4_Word unused0 = 0;
638 seL4_Word unused1 = 0;
639 seL4_Word unused2 = 0;
640 seL4_Word unused3 = 0;
641 seL4_Word unused4 = 0;
642 seL4_Word unused5 = 0;
643
644 arm_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
645 }
646
647 #if CONFIG_MAX_NUM_NODES > 1
seL4_DebugSendIPI(seL4_Uint8 target,unsigned irq)648 LIBSEL4_INLINE_FUNC void seL4_DebugSendIPI(seL4_Uint8 target, unsigned irq)
649 {
650 arm_sys_send(seL4_SysDebugSendIPI, target, irq, 0, 0, 0, 0);
651 }
652 #endif
653 #endif
654
655 #ifdef CONFIG_DANGEROUS_CODE_INJECTION
seL4_DebugRun(void (* userfn)(void *),void * userarg)656 LIBSEL4_INLINE_FUNC void seL4_DebugRun(void (* userfn)(void *), void *userarg)
657 {
658 arm_sys_send_null(seL4_SysDebugRun, (seL4_Word)userfn, (seL4_Word)userarg);
659 asm volatile("" ::: "memory");
660 }
661 #endif
662
663 #ifdef CONFIG_ENABLE_BENCHMARKS
664 /* set the log index back to 0 */
seL4_BenchmarkResetLog(void)665 LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkResetLog(void)
666 {
667 seL4_Word unused0 = 0;
668 seL4_Word unused1 = 0;
669 seL4_Word unused2 = 0;
670 seL4_Word unused3 = 0;
671 seL4_Word unused4 = 0;
672
673 seL4_Word ret;
674 arm_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
675
676 return (seL4_Error) ret;
677 }
678
seL4_BenchmarkFinalizeLog(void)679 LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkFinalizeLog(void)
680 {
681 seL4_Word unused0 = 0;
682 seL4_Word unused1 = 0;
683 seL4_Word unused2 = 0;
684 seL4_Word unused3 = 0;
685 seL4_Word unused4 = 0;
686
687 seL4_Word index_ret;
688 arm_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
689
690 return (seL4_Word) index_ret;
691 }
692
seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)693 LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
694 {
695 seL4_Word unused0 = 0;
696 seL4_Word unused1 = 0;
697 seL4_Word unused2 = 0;
698 seL4_Word unused3 = 0;
699 seL4_Word unused4 = 0;
700
701 arm_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2, &unused3,
702 &unused4, 0);
703
704 return (seL4_Error) frame_cptr;
705 }
706
seL4_BenchmarkNullSyscall(void)707 LIBSEL4_INLINE_FUNC void seL4_BenchmarkNullSyscall(void)
708 {
709 arm_sys_null(seL4_SysBenchmarkNullSyscall);
710 asm volatile("" ::: "memory");
711 }
712
seL4_BenchmarkFlushCaches(void)713 LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushCaches(void)
714 {
715 arm_sys_send_null(seL4_SysBenchmarkFlushCaches, 0, 0);
716 asm volatile("" ::: "memory");
717 }
718
seL4_BenchmarkFlushL1Caches(seL4_Word cache_type)719 LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushL1Caches(seL4_Word cache_type)
720 {
721 arm_sys_send_null(seL4_SysBenchmarkFlushCaches, 1, cache_type);
722 asm volatile("" ::: "memory");
723 }
724
725 #ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)726 LIBSEL4_INLINE_FUNC void seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
727 {
728 seL4_Word unused0 = 0;
729 seL4_Word unused1 = 0;
730 seL4_Word unused2 = 0;
731 seL4_Word unused3 = 0;
732 seL4_Word unused4 = 0;
733 seL4_Word unused5 = 0;
734
735 arm_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3, &unused4,
736 &unused5, 0);
737 }
738
seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)739 LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
740 {
741 seL4_Word unused0 = 0;
742 seL4_Word unused1 = 0;
743 seL4_Word unused2 = 0;
744 seL4_Word unused3 = 0;
745 seL4_Word unused4 = 0;
746 seL4_Word unused5 = 0;
747
748 arm_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3,
749 &unused4, &unused5, 0);
750 }
751 #ifdef CONFIG_DEBUG_BUILD
seL4_BenchmarkDumpAllThreadsUtilisation(void)752 LIBSEL4_INLINE_FUNC void seL4_BenchmarkDumpAllThreadsUtilisation(void)
753 {
754 seL4_Word unused0 = 0;
755 seL4_Word unused1 = 0;
756 seL4_Word unused2 = 0;
757 seL4_Word unused3 = 0;
758 seL4_Word unused4 = 0;
759 seL4_Word unused5 = 0;
760
761 arm_sys_send_recv(seL4_SysBenchmarkDumpAllThreadsUtilisation, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4,
762 &unused5, 0);
763 }
764
seL4_BenchmarkResetAllThreadsUtilisation(void)765 LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetAllThreadsUtilisation(void)
766 {
767 seL4_Word unused0 = 0;
768 seL4_Word unused1 = 0;
769 seL4_Word unused2 = 0;
770 seL4_Word unused3 = 0;
771 seL4_Word unused4 = 0;
772 seL4_Word unused5 = 0;
773
774 arm_sys_send_recv(seL4_SysBenchmarkResetAllThreadsUtilisation, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4,
775 &unused5, 0);
776 }
777
778 #endif
779 #endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
780 #endif /* CONFIG_ENABLE_BENCHMARKS */
781
782 #ifdef CONFIG_SET_TLS_BASE_SELF
seL4_SetTLSBase(seL4_Word tls_base)783 LIBSEL4_INLINE_FUNC void seL4_SetTLSBase(seL4_Word tls_base)
784 {
785 arm_sys_send_null(seL4_SysSetTLSBase, tls_base, 0);
786 asm volatile("" ::: "memory");
787 }
788 #endif /* CONFIG_SET_TLS_BASE_SELF */
789
790 #ifndef CONFIG_KERNEL_MCS
seL4_Wait(seL4_CPtr src,seL4_Word * sender)791 LIBSEL4_INLINE_FUNC void seL4_Wait(seL4_CPtr src, seL4_Word *sender)
792 {
793 seL4_Recv(src, sender);
794 }
795 #endif
796
seL4_Poll(seL4_CPtr src,seL4_Word * sender)797 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll(seL4_CPtr src, seL4_Word *sender)
798 {
799
800 #ifdef CONFIG_KERNEL_MCS
801 return seL4_NBWait(src, sender);
802 #else
803 return seL4_NBRecv(src, sender);
804 #endif
805 }
806