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_SEL4_ARCH_SYSCALLS_H
14#define __LIBSEL4_SEL4_ARCH_SYSCALLS_H
15
16#include <autoconf.h>
17#include <sel4/arch/functions.h>
18#include <sel4/types.h>
19
20/*
21 * A general description of the x86_sys_ functions and what they do can be found in
22 * the ARM aarch32 syscalls.h file (substituting ARM for x86)
23 *
24 * Further there are two version of every function, one that supports Position
25 * Independent Code, and one that does not. The PIC variant works to preserve
26 * EBX, which is used by the compiler, and has to do additional work to save/restore
27 * and juggle the contents of EBX as the kernel ABI uses EBX
28 */
29
30#if defined(__pic__)
31
32static inline void
33x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word mr1, seL4_Word mr2)
34{
35    asm volatile (
36        "pushl %%ebp       \n"
37        "pushl %%ebx       \n"
38        "movl %%ecx, %%ebp \n"
39        "movl %%esp, %%ecx \n"
40        "movl %%edx, %%ebx \n"
41        "leal 1f, %%edx    \n"
42        "1:                \n"
43        "sysenter          \n"
44        "popl %%ebx        \n"
45        "popl %%ebp        \n"
46        : "+d" (dest)
47        : "a" (sys),
48        "S" (info),
49        "D" (mr1),
50        "c" (mr2)
51    );
52}
53
54static inline void
55x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, seL4_Word mr2)
56{
57    asm volatile (
58        "pushl %%ebp       \n"
59        "pushl %%ebx       \n"
60        "movl %%ecx, %%ebp \n"
61        "movl %%esp, %%ecx \n"
62        "leal 1f, %%edx    \n"
63        "1:                \n"
64        "sysenter          \n"
65        "popl %%ebx        \n"
66        "popl %%ebp        \n"
67        :
68        : "a" (sys),
69        "S" (info),
70        "D" (mr1),
71        "c" (mr2)
72        : "%edx"
73    );
74}
75
76static inline void
77x86_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info)
78{
79    asm volatile (
80        "pushl %%ebp       \n"
81        "pushl %%ebx       \n"
82        "movl %%esp, %%ecx \n"
83        "movl %%edx, %%ebx \n"
84        "leal 1f, %%edx    \n"
85        "1:                \n"
86        "sysenter          \n"
87        "popl %%ebx        \n"
88        "popl %%ebp        \n"
89        : "+d" (src)
90        : "a" (sys),
91        "S" (info)
92        : "%ecx"
93    );
94}
95
96static inline void
97x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr1, seL4_Word *out_mr2)
98{
99    asm volatile (
100        "pushl %%ebp       \n"
101        "pushl %%ebx       \n"
102        "movl %%esp, %%ecx \n"
103        "movl %%edx, %%ebx \n"
104        "leal 1f, %%edx    \n"
105        "1:                \n"
106        "sysenter          \n"
107        "movl %%ebx, %%edx \n"
108        "popl %%ebx        \n"
109        "movl %%ebp, %%ecx \n"
110        "popl %%ebp        \n"
111        :
112        "=d" (*out_badge),
113        "=S" (*out_info),
114        "=D" (*out_mr1),
115        "=c" (*out_mr2)
116        : "a" (sys),
117        "d" (src)
118        : "memory"
119    );
120}
121
122static inline void
123x86_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2)
124{
125    asm volatile(
126        "pushl %%ebp       \n"
127        "pushl %%ebx       \n"
128        "movl %%ecx, %%ebp \n"
129        "movl %%esp, %%ecx \n"
130        "movl %%edx, %%ebx \n"
131        "leal 1f, %%edx    \n"
132        "1:                \n"
133        "sysenter          \n"
134        "movl %%ebx, %%edx \n"
135        "popl %%ebx        \n"
136        "movl %%ebp, %%ecx \n"
137        "popl %%ebp        \n"
138        :
139        "=S" (*out_info),
140        "=D" (*in_out_mr1),
141        "=c" (*in_out_mr2),
142        "=d" (*out_badge)
143        : "a" (sys),
144        "S" (info),
145        "D" (*in_out_mr1),
146        "c" (*in_out_mr2),
147        "d" (dest)
148        : "memory"
149    );
150}
151
152static inline void
153x86_sys_null(seL4_Word sys)
154{
155    asm volatile (
156        "pushl %%ebp       \n"
157        "pushl %%ebx       \n"
158        "movl %%esp, %%ecx \n"
159        "leal 1f, %%edx    \n"
160        "1:                \n"
161        "sysenter          \n"
162        "popl %%ebx        \n"
163        "popl %%ebp        \n"
164        :
165        : "a" (sys)
166        : "%ecx", "%edx"
167    );
168}
169
170#else
171
172static inline void
173x86_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info, seL4_Word mr1, seL4_Word mr2)
174{
175    asm volatile (
176        "pushl %%ebp       \n"
177        "movl %%ecx, %%ebp \n"
178        "movl %%esp, %%ecx \n"
179        "leal 1f, %%edx    \n"
180        "1:                \n"
181        "sysenter          \n"
182        "popl %%ebp        \n"
183        :
184        : "a" (sys),
185        "b" (dest),
186        "S" (info),
187        "D" (mr1),
188        "c" (mr2)
189        : "%edx"
190    );
191}
192
193static inline void
194x86_sys_reply(seL4_Word sys, seL4_Word info, seL4_Word mr1, seL4_Word mr2)
195{
196    asm volatile(
197        "pushl %%ebp       \n"
198        "movl %%ecx, %%ebp \n"
199        "movl %%esp, %%ecx \n"
200        "leal 1f, %%edx    \n"
201        "1:                \n"
202        "sysenter          \n"
203        "popl %%ebp        \n"
204        :
205        : "a" (sys),
206        "S" (info),
207        "D" (mr1),
208        "c" (mr2)
209        : "%ebx", "%edx"
210    );
211}
212
213static inline void
214x86_sys_send_null(seL4_Word sys, seL4_Word dest, seL4_Word info)
215{
216    asm volatile ( \
217                   "pushl %%ebp       \n"
218                   "movl %%esp, %%ecx \n"
219                   "leal 1f, %%edx    \n"
220                   "1:                \n"
221                   "sysenter          \n"
222                   "popl %%ebp        \n"
223                   :
224                   : "a" (sys),
225                   "b" (dest),
226                   "S" (info)
227                   : "%ecx", "edx"
228                 );
229}
230
231static inline void
232x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr1, seL4_Word *out_mr2)
233{
234    asm volatile ( \
235                   "pushl %%ebp       \n"
236                   "movl %%esp, %%ecx \n"
237                   "leal 1f, %%edx    \n"
238                   "1:                \n"
239                   "sysenter          \n"
240                   "movl %%ebp, %%ecx \n"
241                   "popl %%ebp        \n"
242                   : "=b" (*out_badge),
243                   "=S" (*out_info),
244                   "=D" (*out_mr1),
245                   "=c" (*out_mr2)
246                   : "a" (sys),
247                   "b" (src)
248                   : "%edx", "memory"
249                 );
250}
251
252static inline void
253x86_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info, seL4_Word *out_info, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2)
254{
255    asm volatile (
256        "pushl %%ebp       \n"
257        "movl %%ecx, %%ebp \n"
258        "movl %%esp, %%ecx \n"
259        "leal 1f, %%edx    \n"
260        "1:                \n"
261        "sysenter          \n"
262        "movl %%ebp, %%ecx \n"
263        "popl %%ebp        \n"
264        : "=S" (*out_info),
265        "=D" (*in_out_mr1),
266        "=c" (*in_out_mr2),
267        "=b" (*out_badge)
268        : "a" (sys),
269        "S" (info),
270        "D" (*in_out_mr1),
271        "c" (*in_out_mr2),
272        "b" (dest)
273        : "%edx", "memory"
274    );
275}
276
277static inline void
278x86_sys_null(seL4_Word sys)
279{
280    asm volatile (
281        "pushl %%ebp       \n"
282        "movl %%esp, %%ecx \n"
283        "leal 1f, %%edx    \n"
284        "1:                \n"
285        "sysenter          \n"
286        "popl %%ebp        \n"
287        :
288        : "a" (sys)
289        : "%ebx", "%ecx", "%edx"
290    );
291}
292
293#endif /* defined(__pic__) */
294
295LIBSEL4_INLINE_FUNC void
296seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
297{
298    x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1));
299}
300
301LIBSEL4_INLINE_FUNC void
302seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
303                 seL4_Word *mr0, seL4_Word *mr1)
304{
305    x86_sys_send(seL4_SysSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0);
306}
307
308LIBSEL4_INLINE_FUNC void
309seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
310{
311    x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1));
312}
313
314LIBSEL4_INLINE_FUNC void
315seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
316                   seL4_Word *mr0, seL4_Word *mr1)
317{
318    x86_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0);
319}
320
321LIBSEL4_INLINE_FUNC void
322seL4_Reply(seL4_MessageInfo_t msgInfo)
323{
324    x86_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1));
325}
326
327LIBSEL4_INLINE_FUNC void
328seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
329                  seL4_Word *mr0, seL4_Word *mr1)
330{
331    x86_sys_reply(seL4_SysReply, msgInfo.words[0], mr0 != seL4_Null ? *mr0 : 0, mr1 != seL4_Null ? *mr1 : 0);
332}
333
334LIBSEL4_INLINE_FUNC void
335seL4_Signal(seL4_CPtr dest)
336{
337    x86_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]);
338}
339
340LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
341seL4_Recv(seL4_CPtr src, seL4_Word* sender)
342{
343    seL4_MessageInfo_t info;
344    seL4_Word badge;
345    seL4_Word mr0;
346    seL4_Word mr1;
347
348    x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, &mr1);
349
350    seL4_SetMR(0, mr0);
351    seL4_SetMR(1, mr1);
352
353    if (sender) {
354        *sender = badge;
355    }
356
357    return info;
358}
359
360LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
361seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender,
362                 seL4_Word *mr0, seL4_Word *mr1)
363{
364    seL4_MessageInfo_t info;
365    seL4_Word badge;
366    seL4_Word msg0 = 0;
367    seL4_Word msg1 = 0;
368
369    x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1);
370
371    if (mr0 != seL4_Null) {
372        *mr0 = msg0;
373    }
374    if (mr1 != seL4_Null) {
375        *mr1 = msg1;
376    }
377
378    if (sender) {
379        *sender = badge;
380    }
381
382    return info;
383}
384
385LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
386seL4_NBRecv(seL4_CPtr src, seL4_Word* sender)
387{
388    seL4_MessageInfo_t info;
389    seL4_Word badge;
390    seL4_Word mr0;
391    seL4_Word mr1;
392
393    x86_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &mr0, &mr1);
394
395    seL4_SetMR(0, mr0);
396    seL4_SetMR(1, mr1);
397
398    if (sender) {
399        *sender = badge;
400    }
401
402    return info;
403}
404
405LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
406seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
407{
408    seL4_MessageInfo_t info;
409    seL4_Word mr0 = seL4_GetMR(0);
410    seL4_Word mr1 = seL4_GetMR(1);
411
412    x86_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &mr0, &mr1);
413
414    seL4_SetMR(0, mr0);
415    seL4_SetMR(1, mr1);
416
417    return info;
418}
419
420LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
421seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
422                 seL4_Word *mr0, seL4_Word *mr1)
423{
424    seL4_MessageInfo_t info;
425    seL4_Word msg0 = 0;
426    seL4_Word msg1 = 0;
427
428    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
429        msg0 = *mr0;
430    }
431    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
432        msg1 = *mr1;
433    }
434
435    x86_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1);
436
437    if (mr0 != seL4_Null) {
438        *mr0 = msg0;
439    }
440    if (mr1 != seL4_Null) {
441        *mr1 = msg1;
442    }
443
444    return info;
445}
446
447LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
448seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
449{
450    seL4_MessageInfo_t info;
451    seL4_Word badge;
452    seL4_Word mr0 = seL4_GetMR(0);
453    seL4_Word mr1 = seL4_GetMR(1);
454
455    x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &mr0, &mr1);
456
457    seL4_SetMR(0, mr0);
458    seL4_SetMR(1, mr1);
459
460    if (sender) {
461        *sender = badge;
462    }
463
464    return info;
465}
466
467LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
468seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
469                      seL4_Word *mr0, seL4_Word *mr1)
470{
471    seL4_MessageInfo_t info;
472    seL4_Word badge;
473    seL4_Word msg0 = 0;
474    seL4_Word msg1 = 0;
475
476    if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
477        msg0 = *mr0;
478    }
479    if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
480        msg1 = *mr1;
481    }
482
483    x86_sys_send_recv(seL4_SysReplyRecv, dest, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1);
484
485    if (mr0 != seL4_Null) {
486        *mr0 = msg0;
487    }
488    if (mr1 != seL4_Null) {
489        *mr1 = msg1;
490    }
491
492    if (sender) {
493        *sender = badge;
494    }
495
496    return info;
497}
498
499LIBSEL4_INLINE_FUNC void
500seL4_Yield(void)
501{
502    x86_sys_null(seL4_SysYield);
503    asm volatile("" :::"%esi", "%edi", "memory");
504}
505
506#ifdef CONFIG_VTX
507LIBSEL4_INLINE_FUNC seL4_Word
508seL4_VMEnter(seL4_Word *sender)
509{
510    seL4_Word fault;
511    seL4_Word badge;
512    seL4_Word mr0 = seL4_GetMR(0);
513    seL4_Word mr1 = seL4_GetMR(1);
514
515    x86_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, &mr1);
516
517    seL4_SetMR(0, mr0);
518    seL4_SetMR(1, mr1);
519    if (!fault && sender) {
520        *sender = badge;
521    }
522    return fault;
523}
524#endif
525
526#ifdef CONFIG_PRINTING
527LIBSEL4_INLINE_FUNC void
528seL4_DebugPutChar(char c)
529{
530    seL4_Word unused0 = 0;
531    seL4_Word unused1 = 0;
532    seL4_Word unused2 = 0;
533    seL4_Word unused3 = 0;
534
535    x86_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3);
536}
537
538LIBSEL4_INLINE_FUNC void
539seL4_DebugDumpScheduler(void)
540{
541    seL4_Word unused0 = 0;
542    seL4_Word unused1 = 0;
543    seL4_Word unused2 = 0;
544    seL4_Word unused3 = 0;
545
546    x86_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3);
547}
548#endif
549
550#ifdef CONFIG_DEBUG_BUILD
551LIBSEL4_INLINE_FUNC void
552seL4_DebugHalt(void)
553{
554    x86_sys_null(seL4_SysDebugHalt);
555    asm volatile("" :::"%esi", "%edi", "memory");
556}
557#endif
558
559#if defined(CONFIG_DEBUG_BUILD)
560LIBSEL4_INLINE_FUNC void
561seL4_DebugSnapshot(void)
562{
563    x86_sys_null(seL4_SysDebugSnapshot);
564    asm volatile("" :::"%esi", "%edi", "memory");
565}
566#endif
567
568#ifdef CONFIG_DEBUG_BUILD
569LIBSEL4_INLINE_FUNC seL4_Uint32
570seL4_DebugCapIdentify(seL4_CPtr cap)
571{
572    seL4_Word unused0 = 0;
573    seL4_Word unused1 = 0;
574    seL4_Word unused2 = 0;
575
576    x86_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2);
577    return (seL4_Uint32)cap;
578}
579
580char *strcpy(char *, const char *);
581LIBSEL4_INLINE_FUNC void
582seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
583{
584    strcpy((char*)seL4_GetIPCBuffer()->msg, name);
585
586    seL4_Word unused0 = 0;
587    seL4_Word unused1 = 0;
588    seL4_Word unused2 = 0;
589    seL4_Word unused3 = 0;
590
591    x86_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3);
592}
593#endif
594
595#if defined(CONFIG_DANGEROUS_CODE_INJECTION)
596LIBSEL4_INLINE_FUNC void
597seL4_DebugRun(void (*userfn) (void *), void* userarg)
598{
599    x86_sys_send_null(seL4_SysDebugRun, (seL4_Word)userfn, (seL4_Word)userarg);
600    asm volatile("" ::: "%edi", "memory");
601}
602#endif
603
604#if defined(CONFIG_KERNEL_X86_DANGEROUS_MSR)
605LIBSEL4_INLINE_FUNC void
606seL4_X86DangerousWRMSR(seL4_Uint32 msr, seL4_Uint64 value)
607{
608    seL4_Uint32 value_low = value & 0xffffffff;
609    seL4_Uint32 value_high = value >> 32;
610    x86_sys_send(seL4_SysX86DangerousWRMSR, msr, 0, value_low, value_high);
611}
612LIBSEL4_INLINE_FUNC seL4_Uint64
613seL4_X86DangerousRDMSR(seL4_Word msr)
614{
615    seL4_Word unused0 = 0;
616    seL4_Word unused1 = 0;
617    seL4_Word low, high;
618    x86_sys_recv(seL4_SysX86DangerousRDMSR, msr, &unused0, &unused1, &low, &high);
619    return ((seL4_Uint64)low) | ((seL4_Uint64)high << 32);
620}
621#endif
622
623#ifdef CONFIG_ENABLE_BENCHMARKS
624LIBSEL4_INLINE_FUNC seL4_Error
625seL4_BenchmarkResetLog(void)
626{
627    seL4_Word unused0 = 0;
628    seL4_Word unused1 = 0;
629    seL4_Word unused2 = 0;
630
631    seL4_Word ret;
632
633    x86_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2);
634
635    return (seL4_Error)ret;
636}
637
638LIBSEL4_INLINE_FUNC seL4_Word
639seL4_BenchmarkFinalizeLog(void)
640{
641    seL4_Word unused0 = 0;
642    seL4_Word unused1 = 0;
643    seL4_Word unused2 = 0;
644    seL4_Word index_ret;
645    x86_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2);
646
647    return (seL4_Word)index_ret;
648}
649
650LIBSEL4_INLINE_FUNC seL4_Error
651seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
652{
653    seL4_Word unused0 = 0;
654    seL4_Word unused1 = 0;
655    seL4_Word unused2 = 0;
656
657    x86_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2);
658
659    return (seL4_Error) frame_cptr;
660}
661
662
663LIBSEL4_INLINE_FUNC void
664seL4_BenchmarkNullSyscall(void)
665{
666    x86_sys_null(seL4_SysBenchmarkNullSyscall);
667    asm volatile("" :::"%esi", "%edi", "memory");
668}
669
670LIBSEL4_INLINE_FUNC void
671seL4_BenchmarkFlushCaches(void)
672{
673    x86_sys_null(seL4_SysBenchmarkFlushCaches);
674    asm volatile("" :::"%esi", "%edi", "memory");
675}
676
677#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
678LIBSEL4_INLINE_FUNC void
679seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
680{
681    seL4_Word unused0 = 0;
682    seL4_Word unused1 = 0;
683    seL4_Word unused2 = 0;
684    seL4_Word unused3 = 0;
685
686    x86_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3);
687}
688
689LIBSEL4_INLINE_FUNC void
690seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
691{
692    seL4_Word unused0 = 0;
693    seL4_Word unused1 = 0;
694    seL4_Word unused2 = 0;
695    seL4_Word unused3 = 0;
696
697    x86_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3);
698}
699#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
700#endif /* CONFIG_ENABLE_BENCHMARKS */
701
702#endif
703