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_SYSCALLS_H 14#define __LIBSEL4_SYSCALLS_H 15#include <autoconf.h> 16 17/** 18 * @defgroup SystemCalls System Calls 19 * @{ 20 * 21 * @defgroup GeneralSystemCalls General System Calls 22 * @{ 23 */ 24 25/** 26 * @xmlonly <manual name="Send" label="sel4_send"/> @endxmlonly 27 * @brief Send to a capability 28 * 29 * @xmlonly 30 * <docref>See <autoref label="sec:sys_send"/></docref> 31 * @endxmlonly 32 * 33 * @param[in] dest The capability to be invoked. 34 * @param[in] msgInfo The messageinfo structure for the IPC. 35 */ 36LIBSEL4_INLINE_FUNC void 37seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo); 38 39/** 40 * @xmlonly <manual name="Recv" label="sel4_recv"/> @endxmlonly 41 * @brief Block until a message is received on an endpoint 42 * 43 * @xmlonly 44 * <docref>See <autoref label="sec:sys_recv"/></docref> 45 * @endxmlonly 46 * 47 * @param[in] src The capability to be invoked. 48 * @param[out] sender The address to write sender information to. 49 * The sender information is the badge of the 50 * endpoint capability that was invoked by the 51 * sender, or the notification word of the 52 * notification object that was signalled. 53 * This parameter is ignored if `NULL`. 54 * 55 * @return A `seL4_MessageInfo_t` structure 56 * @xmlonly 57 * <docref>as described in <autoref label="sec:messageinfo"/></docref> 58 * @endxmlonly 59 */ 60LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 61seL4_Recv(seL4_CPtr src, seL4_Word* sender); 62 63/** 64 * @xmlonly <manual name="Call" label="sel4_call"/> @endxmlonly 65 * @brief Call a capability 66 * 67 * @xmlonly 68 * <docref>See <autoref label="sec:sys_call"/></docref> 69 * @endxmlonly 70 * 71 * @param[in] dest The capability to be invoked. 72 * @param[in] msgInfo The messageinfo structure for the IPC. 73 * 74 * @return A `seL4_MessageInfo_t` structure 75 * @xmlonly 76 * <docref>as described in <autoref label="sec:messageinfo"/></docref> 77 * @endxmlonly 78 */ 79LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 80seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo); 81 82/** 83 * @xmlonly <manual name="Reply" label="sel4_reply"/> @endxmlonly 84 * @brief Perform a send to a one-off reply capability stored when 85 * the thread was last called 86 * 87 * @xmlonly 88 * <docref>See <autoref label="sec:sys_reply"/></docref> 89 * @endxmlonly 90 * 91 * @param[in] msgInfo The messageinfo structure for the IPC. 92 */ 93LIBSEL4_INLINE_FUNC void 94seL4_Reply(seL4_MessageInfo_t msgInfo); 95 96/** 97 * @xmlonly <manual name="Non-Blocking Send" label="sel4_nbsend"/> @endxmlonly 98 * @brief Perform a non-blocking send to a capability 99 * 100 * @xmlonly 101 * <docref>See <autoref label="sec:sys_nbsend"/></docref> 102 * @endxmlonly 103 * 104 * @param[in] dest The capability to be invoked. 105 * @param[in] msgInfo The messageinfo structure for the IPC. 106 */ 107LIBSEL4_INLINE_FUNC void 108seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo); 109 110/** 111 * @xmlonly <manual name="Reply Recv" label="sel4_replyrecv"/> @endxmlonly 112 * @brief Perform a reply followed by a receive in one system call 113 * 114 * @xmlonly 115 * <docref>See <autoref label="sec:sys_replyrecv"/></docref> 116 * @endxmlonly 117 * 118 * @param[in] dest The capability to be invoked. 119 * @param[in] msgInfo The messageinfo structure for the IPC. 120 * @param[out] sender The address to write sender information to. 121 * The sender information is the badge of the 122 * endpoint capability that was invoked by the 123 * sender, or the notification word of the 124 * notification object that was signalled. 125 * This parameter is ignored if `NULL`. 126 * 127 * @return A `seL4_MessageInfo_t` structure 128 * @xmlonly 129 * <docref>as described in <autoref label="sec:messageinfo"/></docref> 130 * @endxmlonly 131 */ 132LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 133seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender); 134 135/** 136 * @xmlonly <manual name="NBRecv" label="sel4_nbrecv"/> @endxmlonly 137 * @brief Receive a message from an endpoint but do not block 138 * in the case that no messages are pending 139 * 140 * @xmlonly 141 * <docref>See <autoref label="sec:sys_nbrecv"/></docref> 142 * @endxmlonly 143 * 144 * @param[in] src The capability to be invoked. 145 * @param[out] sender The address to write sender information to. 146 * The sender information is the badge of the 147 * endpoint capability that was invoked by the 148 * sender, or the notification word of the 149 * notification object that was signalled. 150 * This parameter is ignored if `NULL`. 151 * 152 * @return A `seL4_MessageInfo_t` structure 153 * @xmlonly 154 * <docref>as described in <autoref label="sec:messageinfo"/></docref> 155 * @endxmlonly 156 */ 157LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 158seL4_NBRecv(seL4_CPtr src, seL4_Word* sender); 159 160/** 161 * @xmlonly <manual name="Yield" label="sel4_yield"/> @endxmlonly 162 * @brief Donate the remaining timeslice to a thread of the same priority 163 * 164 * @xmlonly 165 * <docref>See <autoref label="sec:sys_yield"/></docref> 166 * @endxmlonly 167 */ 168LIBSEL4_INLINE_FUNC void 169seL4_Yield(void); 170 171/** 172 * @xmlonly <manual name="Signal" label="sel4_signal"/> @endxmlonly 173 * @brief Signal a notification 174 * 175 * This is not a proper system call known by the kernel. Rather, it is a 176 * convenience wrapper which calls seL4_Send(). 177 * It is useful for signalling a notification. 178 * 179 * @xmlonly 180 * <docref>See the description of <nameref name="seL4_Send"/> in <autoref label="sec:sys_send"/>.</docref> 181 * @endxmlonly 182 * 183 * @param[in] dest The capability to be invoked. 184 */ 185LIBSEL4_INLINE_FUNC void 186seL4_Signal(seL4_CPtr dest); 187 188/** 189 * @xmlonly <manual name="Wait" label="sel4_wait"/> @endxmlonly 190 * @brief Perform a receive on a notification object 191 * 192 * This is not a proper system call known by the kernel. Rather, it is a 193 * convenience wrapper which calls seL4_Recv(). 194 * 195 * @xmlonly 196 * <docref>See the description of <nameref name="seL4_Recv"/> in <autoref label="sec:sys_recv"/>.</docref> 197 * @endxmlonly 198 * 199 * @param[in] src The capability to be invoked. 200 * @param[out] sender The address to write sender information to. 201 * The sender information is the badge of the 202 * endpoint capability that was invoked by the 203 * sender, or the notification word of the 204 * notification object that was signalled. 205 * This parameter is ignored if `NULL`. 206 */ 207LIBSEL4_INLINE_FUNC void 208seL4_Wait(seL4_CPtr src, seL4_Word *sender); 209 210/** 211 * @xmlonly <manual name="Poll" label="sel4_poll"/> @endxmlonly 212 * @brief Perform a non-blocking recv on a notification object 213 * 214 * This is not a proper system call known by the kernel. Rather, it is a 215 * convenience wrapper which calls seL4_NBRecv(). 216 * It is useful for doing a non-blocking wait on a notification. 217 * 218 * @xmlonly 219 * <docref>See the description of <nameref name="seL4_NBRecv"/> in <autoref label="sec:sys_nbrecv"/>.</docref> 220 * @endxmlonly 221 * 222 * @param[in] src The capability to be invoked. 223 * @param[out] sender The address to write sender information to. 224 * The sender information is the badge of the 225 * endpoint capability that was invoked by the 226 * sender, or the notification word of the 227 * notification object that was signalled. 228 * This parameter is ignored if `NULL`. 229 * 230 * @return A `seL4_MessageInfo_t` structure 231 * @xmlonly 232 * <docref>as described in <autoref label="sec:messageinfo"/></docref> 233 * @endxmlonly 234 */ 235LIBSEL4_INLINE_FUNC seL4_MessageInfo_t 236seL4_Poll(seL4_CPtr src, seL4_Word *sender); 237 238/** @} */ 239 240/** 241 * @defgroup DebuggingSystemCalls 242 * This section documents debugging system calls available when the kernel is 243 * build with the `DEBUG_BUILD` configuration. For any system calls that rely 244 * on a kernel serial driver, `PRINTING` must also be enabled. 245 * 246 * @{ 247 */ 248#ifdef CONFIG_PRINTING 249/** 250 * @xmlonly <manual name="Put Char" label="sel4_debugputchar"/> @endxmlonly 251 * @brief Output a single char through the kernel. 252 * 253 * Use the kernel serial driver to output a single character. This is useful for 254 * debugging when a user level serial driver is not available. 255 * 256 * @param c The character to output. 257 * 258 */ 259LIBSEL4_INLINE_FUNC void 260seL4_DebugPutChar(char c); 261 262/** 263 * @xmlonly <manual name="Dump scheduler" label="sel4_dumpscheduler"/> @endxmlonly 264 * @brief Output the contents of the kernel scheduler. 265 * 266 * Dump the state of the all TCB objects to kernel serial output. This system call 267 * will output a table containing: 268 * - Address: the address of the TCB object for that thread, 269 * - Name: the name of the thread (if set), 270 * - IP: the contents of the instruction pointer the thread is at, 271 * - Priority: the priority of that thread, 272 * - State : the state of the thread. 273 */ 274 275LIBSEL4_INLINE_FUNC void 276seL4_DebugDumpScheduler(void); 277#endif 278 279#if CONFIG_DEBUG_BUILD 280/** 281 * @xmlonly <manual name="Halt" label="sel4_debughalt"/> @endxmlonly 282 * @brief Halt the system. 283 * 284 * This debugging system call will cause the kernel immediately cease responding to 285 * system calls. The kernel will switch permanently to the idle thread with 286 * interrupts disabled. Depending on the platform, the kernel may switch 287 * the hardware into a low-power state. 288 * 289 */ 290LIBSEL4_INLINE_FUNC void 291seL4_DebugHalt(void); 292 293/** 294 * @xmlonly <manual name="Snapshot" label="sel4_debugsnapshot"/> @endxmlonly 295 * @brief Output a capDL dump of the current kernel state. 296 * 297 * This debugging system call will output all of the capabilities in the current 298 * kernel using capDL. 299 * 300 */ 301LIBSEL4_INLINE_FUNC void 302seL4_DebugSnapshot(void); 303 304/** 305 * @xmlonly <manual name="Cap Identify" label="sel4_debugcapidentify"/> @endxmlonly 306 * @brief Identify the type of a capability in the current cspace. 307 * 308 * This debugging system call returns the type of capability in a capability 309 * slot in the current cspace. The type returned is not a libsel4 type, but 310 * refers to an internal seL4 type. This can be looked up in a built kernel by 311 * looking for the (generated) `enum cap_tag`, type `cap_tag_t`. 312 * 313 * @param cap A capability slot in the current cspace. 314 * @return The type of capability passed in. 315 * 316 */ 317LIBSEL4_INLINE_FUNC seL4_Uint32 318seL4_DebugCapIdentify(seL4_CPtr cap); 319 320/** 321 * @xmlonly <manual name="Name Thread" label="sel4_debugnamethread"/> @endxmlonly 322 * @brief Name a thread. 323 * 324 * Name a thread. This name will then be output by the kernel in all debugging output. 325 * Note that the max name length that can be passed to this function is limited by the 326 * number of chars that will fit in an IPC message (`seL4_MsgMaxLength` multiplied by the 327 * amount of chars that fit in a word). However the name is also truncated in order to fit into a TCB object. 328 * For some platforms you may need to increase `seL4_TCBBits` by 1 in a debug build in order to 329 * fit a long enough name. 330 * 331 * @param tcb A capability to the tcb object for the thread to name. 332 * @param name The name for the thread. 333 * 334 */ 335LIBSEL4_INLINE_FUNC void 336seL4_DebugNameThread(seL4_CPtr tcb, const char *name); 337#endif 338 339#ifdef CONFIG_DANGEROUS_CODE_INJECTION 340/** 341 * @xmlonly <manual name="Run" label="sel4_debugrun"/> @endxmlonly 342 * @brief Run a user level function in kernel mode. 343 * 344 * This extremely dangerous function is for running benchmarking and debugging code that 345 * needs to be executed in kernel mode from userlevel. It should never be used in a release kernel. 346 * This works because the kernel can access all user mappings of device memory, and does not switch page directories 347 * on kernel entry. 348 * 349 * Unlike the other system calls in this section, `seL4_DebugRun` does not 350 * depend on the `DEBUG_BUILD` configuration option, but its own config 351 * variable `DANGEROUS_CODE_INJECTION`. 352 * 353 * @param userfn The address in userspace of the function to run. 354 * @param userarg A single argument to pass to the function. 355 * 356 */ 357LIBSEL4_INLINE_FUNC void 358seL4_DebugRun(void (* userfn) (void *), void* userarg); 359#endif 360/** @} */ 361 362/** 363 * @defgroup BenchmarkingSystemCalls 364 * This section documents system calls available when the kernel is 365 * configured with benchmarking enabled. 366 * There are several different benchmarking modes which can be configured 367 * when building the kernel: 368 * 1. `BENCHMARK_TRACEPOINTS`: Enable using tracepoints in the kernel and timing code. 369 * 2. `BENCHMARK_TRACK_KERNEL_ENTRIES`: Keep track of information on kernel entries. 370 * 3. `BENCHMARK_TRACK_UTILISATION`: Allow users to get CPU timing info for the system, threads and/or idle thread. 371 * 372 * `BENCHMARK_TRACEPOINTS` and `BENCHMARK_TRACK_KERNEL_ENTRIES` use a log buffer that has to be allocated by the user and mapped 373 * to a fixed location in the kernel window. 374 * All of timing information is output in cycles. 375 * 376 * @{ 377 */ 378#ifdef CONFIG_ENABLE_BENCHMARKS 379/* 380 */ 381 382/** 383 * @xmlonly <manual name="Reset Log" label="sel4_benchmarkresetlog"/> @endxmlonly 384 * @brief Reset benchmark logging. 385 * 386 * The behaviour of this system call depends on benchmarking mode in action while invoking 387 * this system call: 388 * 1. `BENCHMARK_TRACEPOINTS`: resets the log index to 0, 389 * 2. `BENCHMARK_TRACK_KERNEL_ENTRIES`: as above, 390 * 3. `BENCHMARK_TRACK_UTILISATION`: resets benchmark and current thread 391 * start time (to the time of invoking this syscall), resets idle 392 * thread utilisation to 0, and starts tracking utilisation. 393 * 394 * @return A `seL4_Error` error if the user-level log buffer has not been set by the user 395 * (`BENCHMARK_TRACEPOINTS`/`BENCHMARK_TRACK_KERNEL_ENTRIES`). 396 */ 397LIBSEL4_INLINE_FUNC seL4_Error 398seL4_BenchmarkResetLog(void); 399 400/** 401 * @xmlonly <manual name="Finalize Log" label="sel4_benchmarkfinalizelog"/> @endxmlonly 402 * @brief Stop benchmark logging. 403 * 404 * The behaviour of this system call depends on benchmarking mode in action while invoking this system call: 405 * 1. `BENCHMARK_TRACEPOINTS`: Sets the final log buffer index to the current index, 406 * 2. `BENCHMARK_TRACK_KERNEL_ENTRIES`: as above, 407 * 3. `BENCHMARK_TRACK_UTILISATION`: sets benchmark end time to current time, stops tracking utilisation. 408 * 409 * @return The index of the final entry in the log buffer (if `BENCHMARK_TRACEPOINTS`/`BENCHMARK_TRACK_KERNEL_ENTRIES` are enabled). 410 * 411 */ 412LIBSEL4_INLINE_FUNC seL4_Word 413seL4_BenchmarkFinalizeLog(void); 414 415/** 416 * @xmlonly <manual name="Set Log Buffer" label="sel4_benchmarksetlogbuffer"/> @endxmlonly 417 * @brief Set log buffer. 418 * 419 * Provide a large frame object for the kernel to use as a log-buffer. 420 * The object must not be device memory, and must be seL4_LargePageBits in size. 421 * 422 * @param[in] frame_cptr A capability pointer to a user allocated frame of seL4_LargePage size. 423 * @return A `seL4_IllegalOperation` error if `frame_cptr` is not valid and couldn't set the buffer. 424 * 425 */ 426LIBSEL4_INLINE_FUNC seL4_Error 427seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr); 428 429/** 430 * @xmlonly <manual name="Null Syscall" label="sel4_benchmarknullsyscall"/> @endxmlonly 431 * @brief Null system call that enters and exits the kernel immediately, for timing kernel traps in microbenchmarks. 432 * 433 * Used to time kernel traps (in and out). 434 * 435 */ 436LIBSEL4_INLINE_FUNC void 437seL4_BenchmarkNullSyscall(void); 438 439/** 440 * @xmlonly <manual name="Flush Caches" label="sel4_benchmarkflushcaches"/> @endxmlonly 441 * @brief Flush hardware caches. 442 * 443 * Flush all possible hardware caches for this platform. 444 */ 445LIBSEL4_INLINE_FUNC void 446seL4_BenchmarkFlushCaches(void); 447 448#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION 449/** 450 * @xmlonly <manual name="Get Thread Utilisation" label="sel4_benchmarkgetthreadutilisation"/> @endxmlonly 451 * @brief Get utilisation timing information. 452 * 453 * Get timing information for the system, requested thread and idle thread. Such information is written 454 * into the caller's IPC buffer; see the definition of `benchmark_track_util_ipc_index` enum for more 455 * details on the data/format returned on the IPC buffer. 456 * 457 * @param[in] tcb_cptr TCB cap pointer to a thread to get CPU utilisation for. 458 */ 459LIBSEL4_INLINE_FUNC void 460seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr); 461 462/** 463 * @xmlonly <manual name="Reset Thread Utilisation" label="sel4_benchmarkresetthreadutilisation"/> @endxmlonly 464 * @brief Reset utilisation timing for a specific thread. 465 * 466 * Reset the kernel's timing information data (start time and utilisation) for a specific thread. 467 * 468 * @param[in] tcb_cptr TCB cap pointer to a thread to get CPU utilisation for. 469 * 470 */ 471LIBSEL4_INLINE_FUNC void 472seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr); 473#endif 474#endif 475/** @} */ 476 477#ifdef CONFIG_ARCH_X86 478/** 479 * @defgroup X86SystemCalls X86 System Calls 480 * @{ 481 */ 482 483#ifdef CONFIG_VTX 484/** 485 * @xmlonly <manual name="VMEnter" label="sel4_vmenter"/> @endxmlonly 486 * @brief Change current thread to execute from its bound VCPU 487 * 488 * Changes the execution mode of the current thread from normal TCB execution, to 489 * guest execution using its bound VCPU. 490 * @xmlonly 491 * <docref>For details on VCPUs and execution modes see <autoref label="sec:virt"/>.</docref> 492 * @endxmlonly 493 * 494 * Invoking `seL4_VMEnter` is similar to replying to a fault in that updates to the registers 495 * can be given in the message, but unlike a fault no message info 496 * @xmlonly 497 * <docref>(see <autoref label="sec:messageinfo"/>)</docref> 498 * @endxmlonly 499 * is sent as the registers are not optional and the number that must be sent is fixed. 500 * The mapping of hardware register to message register is 501 * - `SEL4_VMENTER_CALL_EIP_MR` Address to start executing instructions at in the guest mode 502 * - `SEL4_VMENTER_CALL_CONTROL_PPC_MR` New value for the Primary Processor Based VM Execution Controls 503 * - `SEL4_VMENTER_CALL_CONTROL_ENTRY_MR` New value for the VM Entry Controls 504 * 505 * On return these same three message registers will be filled with the values at the point 506 * that the privlidged mode ceased executing. If this function returns with `SEL4_VMENTER_RESULT_FAULT` 507 * then the following additional message registers will be filled out 508 * - `SEL4_VMENTER_FAULT_REASON_MR` 509 * - `SEL4_VMENTER_FAULT_QUALIFICATION_MR` 510 * - `SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR` 511 * - `SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR` 512 * - `SEL4_VMENTER_FAULT_RFLAGS_MR` 513 * - `SEL4_VMENTER_FAULT_GUEST_INT_MR` 514 * - `SEL4_VMENTER_FAULT_CR3_MR` 515 * - `SEL4_VMENTER_FAULT_EAX` 516 * - `SEL4_VMENTER_FAULT_EBX` 517 * - `SEL4_VMENTER_FAULT_ECX` 518 * - `SEL4_VMENTER_FAULT_EDX` 519 * - `SEL4_VMENTER_FAULT_ESI` 520 * - `SEL4_VMENTER_FAULT_EDI` 521 * - `SEL4_VMENTER_FAULT_EBP` 522 * 523 * @param[out] sender The address to write sender information to. 524 * If the syscall returns due to receiving a notification 525 * on the bound notification then the sender information 526 * is the badge of the notification capability that was invoked. 527 * This parameter is ignored if `NULL`. 528 * @return `SEL4_VMENTER_RESULT_NOTIF` if a notification was received or `SEL4_VMENTER_RESULT_FAULT` 529 * if the guest mode execution faulted for any reason 530 */ 531LIBSEL4_INLINE_FUNC seL4_Word 532seL4_VMEnter(seL4_Word *sender); 533#endif 534 535/** @} */ 536#endif 537 538/** @} */ 539 540#endif /* __LIBSEL4_SYSCALLS_H */ 541