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