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