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