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 20LIBSEL4_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 25LIBSEL4_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 36LIBSEL4_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 41LIBSEL4_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 53LIBSEL4_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 58LIBSEL4_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 70LIBSEL4_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 77LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply) 78#else 79LIBSEL4_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 104LIBSEL4_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 107LIBSEL4_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 142LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply) 143#else 144LIBSEL4_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 168LIBSEL4_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 187LIBSEL4_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 230LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, 231 seL4_CPtr reply) 232#else 233LIBSEL4_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 267LIBSEL4_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 271LIBSEL4_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 322LIBSEL4_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 355LIBSEL4_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 404LIBSEL4_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 437LIBSEL4_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 487LIBSEL4_INLINE_FUNC void seL4_Yield(void) 488{ 489 arm_sys_null(seL4_SysYield); 490 asm volatile("" ::: "memory"); 491} 492 493#ifdef CONFIG_KERNEL_MCS 494LIBSEL4_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 517LIBSEL4_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 550LIBSEL4_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 575LIBSEL4_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 587LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str) 588{ 589 for (char *s = str; *s; s++) { 590 seL4_DebugPutChar(*s); 591 } 592 return; 593} 594 595LIBSEL4_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 609LIBSEL4_INLINE_FUNC void seL4_DebugHalt(void) 610{ 611 arm_sys_null(seL4_SysDebugHalt); 612} 613 614LIBSEL4_INLINE_FUNC void seL4_DebugSnapshot(void) 615{ 616 arm_sys_null(seL4_SysDebugSnapshot); 617 asm volatile("" ::: "memory"); 618} 619 620LIBSEL4_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 632char *strcpy(char *, const char *); 633LIBSEL4_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 648LIBSEL4_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 656LIBSEL4_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 */ 665LIBSEL4_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 679LIBSEL4_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 693LIBSEL4_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 707LIBSEL4_INLINE_FUNC void seL4_BenchmarkNullSyscall(void) 708{ 709 arm_sys_null(seL4_SysBenchmarkNullSyscall); 710 asm volatile("" ::: "memory"); 711} 712 713LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushCaches(void) 714{ 715 arm_sys_send_null(seL4_SysBenchmarkFlushCaches, 0, 0); 716 asm volatile("" ::: "memory"); 717} 718 719LIBSEL4_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 726LIBSEL4_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 739LIBSEL4_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 752LIBSEL4_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 765LIBSEL4_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 783LIBSEL4_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 791LIBSEL4_INLINE_FUNC void seL4_Wait(seL4_CPtr src, seL4_Word *sender) 792{ 793 seL4_Recv(src, sender); 794} 795#endif 796 797LIBSEL4_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