This provides documentation for kernel design of the x86 virtualisation, the additional syscall and object invocations. The ARM design is not fully expanded.
540 lines
19 KiB
C
540 lines
19 KiB
C
/*
|
|
* Copyright 2017, Data61
|
|
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
|
|
* ABN 41 687 119 230.
|
|
*
|
|
* This software may be distributed and modified according to the terms of
|
|
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
|
* See "LICENSE_BSD2.txt" for details.
|
|
*
|
|
* @TAG(DATA61_BSD)
|
|
*/
|
|
|
|
#ifndef __LIBSEL4_SYSCALLS_H
|
|
#define __LIBSEL4_SYSCALLS_H
|
|
#include <autoconf.h>
|
|
|
|
/**
|
|
* @defgroup SystemCalls System Calls
|
|
* @{
|
|
*
|
|
* @defgroup GeneralSystemCalls General System Calls
|
|
* @{
|
|
*/
|
|
|
|
/**
|
|
* @xmlonly <manual name="Send" label="sel4_send"/> @endxmlonly
|
|
* @brief Send to a capability
|
|
*
|
|
* @xmlonly
|
|
* See <autoref label="sec:sys_send"/>
|
|
* @endxmlonly
|
|
*
|
|
* @param[in] dest The capability to be invoked.
|
|
* @param[in] msgInfo The messageinfo structure for the IPC.
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Recv" label="sel4_recv"/> @endxmlonly
|
|
* @brief Block until a message is received on an endpoint
|
|
*
|
|
* @xmlonly
|
|
* See <autoref label="sec:sys_recv"/>
|
|
* @endxmlonly
|
|
*
|
|
* @param[in] src The capability to be invoked.
|
|
* @param[out] sender The address to write sender information to.
|
|
* The sender information is the badge of the
|
|
* endpoint capability that was invoked by the
|
|
* sender, or the notification word of the
|
|
* notification object that was signalled.
|
|
* This parameter is ignored if `NULL`.
|
|
*
|
|
* @return A `seL4_MessageInfo_t` structure
|
|
* @xmlonly
|
|
* as described in <autoref label="sec:messageinfo"/>
|
|
* @endxmlonly
|
|
*/
|
|
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
|
|
seL4_Recv(seL4_CPtr src, seL4_Word* sender);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Call" label="sel4_call"/> @endxmlonly
|
|
* @brief Call a capability
|
|
*
|
|
* @xmlonly
|
|
* See <autoref label="sec:sys_call"/>
|
|
* @endxmlonly
|
|
*
|
|
* @param[in] dest The capability to be invoked.
|
|
* @param[in] msgInfo The messageinfo structure for the IPC.
|
|
*
|
|
* @return A `seL4_MessageInfo_t` structure
|
|
* @xmlonly
|
|
* as described in <autoref label="sec:messageinfo"/>
|
|
* @endxmlonly
|
|
*/
|
|
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
|
|
seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Reply" label="sel4_reply"/> @endxmlonly
|
|
* @brief Perform a send to a one-off reply capability stored when
|
|
* the thread was last called
|
|
*
|
|
* @xmlonly
|
|
* See <autoref label="sec:sys_reply"/>
|
|
* @endxmlonly
|
|
*
|
|
* @param[in] msgInfo The messageinfo structure for the IPC.
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_Reply(seL4_MessageInfo_t msgInfo);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Polling Send" label="sel4_nbsend"/> @endxmlonly
|
|
* @brief Perform a polling send to a capability
|
|
*
|
|
* @xmlonly
|
|
* See <autoref label="sec:sys_nbsend"/>
|
|
* @endxmlonly
|
|
*
|
|
* @param[in] dest The capability to be invoked.
|
|
* @param[in] msgInfo The messageinfo structure for the IPC.
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Reply Recv" label="sel4_replyrecv"/> @endxmlonly
|
|
* @brief Perform a reply followed by a receive in one system call
|
|
*
|
|
* @xmlonly
|
|
* See <autoref label="sec:sys_replyrecv"/>
|
|
* @endxmlonly
|
|
*
|
|
* @param[in] dest The capability to be invoked.
|
|
* @param[in] msgInfo The messageinfo structure for the IPC.
|
|
* @param[out] sender The address to write sender information to.
|
|
* The sender information is the badge of the
|
|
* endpoint capability that was invoked by the
|
|
* sender, or the notification word of the
|
|
* notification object that was signalled.
|
|
* This parameter is ignored if `NULL`.
|
|
*
|
|
* @return A `seL4_MessageInfo_t` structure
|
|
* @xmlonly
|
|
* as described in <autoref label="sec:messageinfo"/>
|
|
* @endxmlonly
|
|
*/
|
|
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
|
|
seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender);
|
|
|
|
/**
|
|
* @xmlonly <manual name="NBRecv" label="sel4_nbrecv"/> @endxmlonly
|
|
* @brief Receive a message from an endpoint but do not block
|
|
* in the case that no messages are pending
|
|
*
|
|
* @xmlonly
|
|
* See <autoref label="sec:sys_nbrecv"/>
|
|
* @endxmlonly
|
|
*
|
|
* @param[in] src The capability to be invoked.
|
|
* @param[out] sender The address to write sender information to.
|
|
* The sender information is the badge of the
|
|
* endpoint capability that was invoked by the
|
|
* sender, or the notification word of the
|
|
* notification object that was signalled.
|
|
* This parameter is ignored if `NULL`.
|
|
*
|
|
* @return A `seL4_MessageInfo_t` structure
|
|
* @xmlonly
|
|
* as described in <autoref label="sec:messageinfo"/>
|
|
* @endxmlonly
|
|
*/
|
|
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
|
|
seL4_NBRecv(seL4_CPtr src, seL4_Word* sender);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Yield" label="sel4_yield"/> @endxmlonly
|
|
* @brief Donate the remaining timeslice to a thread of the same priority
|
|
*
|
|
* @xmlonly
|
|
* See <autoref label="sec:sys_yield"/>
|
|
* @endxmlonly
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_Yield(void);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Signal" label="sel4_signal"/> @endxmlonly
|
|
* @brief Signal a notification
|
|
*
|
|
* This is not a proper system call known by the kernel. Rather, it is a
|
|
* convenience wrapper which calls seL4_Send().
|
|
* It is useful for signalling a notification.
|
|
*
|
|
* @xmlonly
|
|
* See the description of <nameref name="seL4_Send"/> in <autoref label="sec:sys_send"/>.
|
|
* @endxmlonly
|
|
*
|
|
* @param[in] dest The capability to be invoked.
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_Signal(seL4_CPtr dest);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Wait" label="sel4_wait"/> @endxmlonly
|
|
* @brief Perform a receive on a notification object
|
|
*
|
|
* This is not a proper system call known by the kernel. Rather, it is a
|
|
* convenience wrapper which calls seL4_Recv().
|
|
*
|
|
* @xmlonly
|
|
* See the description of <nameref name="seL4_Recv"/> in <autoref label="sec:sys_recv"/>.
|
|
* @endxmlonly
|
|
*
|
|
* @param[in] src The capability to be invoked.
|
|
* @param[out] sender The address to write sender information to.
|
|
* The sender information is the badge of the
|
|
* endpoint capability that was invoked by the
|
|
* sender, or the notification word of the
|
|
* notification object that was signalled.
|
|
* This parameter is ignored if `NULL`.
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_Wait(seL4_CPtr src, seL4_Word *sender);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Poll" label="sel4_poll"/> @endxmlonly
|
|
* @brief Perform a non-blocking recv on a notification object
|
|
*
|
|
* This is not a proper system call known by the kernel. Rather, it is a
|
|
* convenience wrapper which calls seL4_NBRecv().
|
|
* It is useful for doing a non-blocking wait on a notification.
|
|
*
|
|
* @xmlonly
|
|
* See the description of <nameref name="seL4_NBRecv"/> in <autoref label="sec:sys_nbrecv"/>.
|
|
* @endxmlonly
|
|
*
|
|
* @param[in] src The capability to be invoked.
|
|
* @param[out] sender The address to write sender information to.
|
|
* The sender information is the badge of the
|
|
* endpoint capability that was invoked by the
|
|
* sender, or the notification word of the
|
|
* notification object that was signalled.
|
|
* This parameter is ignored if `NULL`.
|
|
*
|
|
* @return A `seL4_MessageInfo_t` structure
|
|
* @xmlonly
|
|
* as described in <autoref label="sec:messageinfo"/>
|
|
* @endxmlonly
|
|
*/
|
|
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
|
|
seL4_Poll(seL4_CPtr src, seL4_Word *sender);
|
|
|
|
/** @} */
|
|
|
|
/**
|
|
* @defgroup DebuggingSystemCalls
|
|
* This section documents debugging system calls available when the kernel is
|
|
* build with the `DEBUG_BUILD` configuration. For any system calls that rely
|
|
* on a kernel serial driver, `PRINTING` must also be enabled.
|
|
*
|
|
* @{
|
|
*/
|
|
#ifdef CONFIG_PRINTING
|
|
/**
|
|
* @xmlonly <manual name="Put Char" label="sel4_debugputchar"/> @endxmlonly
|
|
* @brief Output a single char through the kernel.
|
|
*
|
|
* Use the kernel serial driver to output a single character. This is useful for
|
|
* debugging when a user level serial driver is not available.
|
|
*
|
|
* @param c The character to output.
|
|
*
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_DebugPutChar(char c);
|
|
#endif
|
|
|
|
#if CONFIG_DEBUG_BUILD
|
|
/**
|
|
* @xmlonly <manual name="Halt" label="sel4_debughalt"/> @endxmlonly
|
|
* @brief Halt the system.
|
|
*
|
|
* This debugging system call will cause the kernel immediately cease responding to
|
|
* system calls. The kernel will switch permanently to the idle thread with
|
|
* interrupts disabled. Depending on the platform, the kernel may switch
|
|
* the hardware into a low-power state.
|
|
*
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_DebugHalt(void);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Snapshot" label="sel4_debugsnapshot"/> @endxmlonly
|
|
* @brief Output a capDL dump of the current kernel state.
|
|
*
|
|
* This debugging system call will output all of the capabilities in the current
|
|
* kernel using capDL.
|
|
*
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_DebugSnapshot(void);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Cap Identify" label="sel4_debugcapidentify"/> @endxmlonly
|
|
* @brief Identify the type of a capability in the current cspace.
|
|
*
|
|
* This debugging system call returns the type of capability in a capability
|
|
* slot in the current cspace. The type returned is not a libsel4 type, but
|
|
* refers to an internal seL4 type. This can be looked up in a built kernel by
|
|
* looking for the (generated) `enum cap_tag`, type `cap_tag_t`.
|
|
*
|
|
* @param cap A capability slot in the current cspace.
|
|
* @return The type of capability passed in.
|
|
*
|
|
*/
|
|
LIBSEL4_INLINE_FUNC seL4_Uint32
|
|
seL4_DebugCapIdentify(seL4_CPtr cap);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Name Thread" label="sel4_debugnamethread"/> @endxmlonly
|
|
* @brief Name a thread.
|
|
*
|
|
* Name a thread. This name will then be output by the kernel in all debugging output.
|
|
* Note that the max name length that can be passed to this function is limited by the
|
|
* number of chars that will fit in an IPC message (`seL4_MsgMaxLength` multiplied by the
|
|
* amount of chars that fit in a word). However the name is also truncated in order to fit into a TCB object.
|
|
* For some platforms you may need to increase `seL4_TCBBits` by 1 in a debug build in order to
|
|
* fit a long enough name.
|
|
*
|
|
* @param tcb A capability to the tcb object for the thread to name.
|
|
* @param name The name for the thread.
|
|
*
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_DebugNameThread(seL4_CPtr tcb, const char *name);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Dump scheduler" label="sel4_dumpscheduler"/> @endxmlonly
|
|
* @brief Output the contents of the kernel scheduler.
|
|
*
|
|
* Dump the state of the all TCB objects to kernel serial output. This system call
|
|
* will output a table containing:
|
|
* - Address: the address of the TCB object for that thread,
|
|
* - Name: the name of the thread (if set),
|
|
* - IP: the contents of the instruction pointer the thread is at,
|
|
* - Priority: the priority of that thread,
|
|
* - State : the state of the thread.
|
|
*/
|
|
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_DebugDumpScheduler(void);
|
|
#endif
|
|
|
|
#ifdef CONFIG_DANGEROUS_CODE_INJECTION
|
|
/**
|
|
* @xmlonly <manual name="Run" label="sel4_debugrun"/> @endxmlonly
|
|
* @brief Run a user level function in kernel mode.
|
|
*
|
|
* This extremely dangerous function is for running benchmarking and debugging code that
|
|
* needs to be executed in kernel mode from userlevel. It should never be used in a release kernel.
|
|
* This works because the kernel can access all user mappings of device memory, and does not switch page directories
|
|
* on kernel entry.
|
|
*
|
|
* Unlike the other system calls in this section, `seL4_DebugRun` does not
|
|
* depend on the `DEBUG_BUILD` configuration option, but its own config
|
|
* variable `DANGEROUS_CODE_INJECTION`.
|
|
*
|
|
* @param userfn The address in userspace of the function to run.
|
|
* @param userarg A single argument to pass to the function.
|
|
*
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_DebugRun(void (* userfn) (void *), void* userarg);
|
|
#endif
|
|
/** @} */
|
|
|
|
/**
|
|
* @defgroup BenchmarkingSystemCalls
|
|
* This section documents system calls available when the kernel is
|
|
* configured with benchmarking enabled.
|
|
* There are several different benchmarking modes which can be configured
|
|
* when building the kernel:
|
|
* 1. `BENCHMARK_TRACEPOINTS`: Enable using tracepoints in the kernel and timing code.
|
|
* 2. `BENCHMARK_TRACK_KERNEL_ENTRIES`: Keep track of information on kernel entries.
|
|
* 3. `BENCHMARK_TRACK_UTILISATION`: Allow users to get CPU timing info for the system, threads and/or idle thread.
|
|
*
|
|
* `BENCHMARK_TRACEPOINTS` and `BENCHMARK_TRACK_KERNEL_ENTRIES` use a log buffer that has to be allocated by the user and mapped
|
|
* to a fixed location in the kernel window.
|
|
* All of timing information is output in cycles.
|
|
*
|
|
* @{
|
|
*/
|
|
#ifdef CONFIG_ENABLE_BENCHMARKS
|
|
/*
|
|
*/
|
|
|
|
/**
|
|
* @xmlonly <manual name="Reset Log" label="sel4_benchmarkresetlog"/> @endxmlonly
|
|
* @brief Reset benchmark logging.
|
|
*
|
|
* The behaviour of this system call depends on benchmarking mode in action while invoking
|
|
* this system call:
|
|
* 1. `BENCHMARK_TRACEPOINTS`: resets the log index to 0,
|
|
* 2. `BENCHMARK_TRACK_KERNEL_ENTRIES`: as above,
|
|
* 3. `BENCHMARK_TRACK_UTILISATION`: resets benchmark and current thread
|
|
* start time (to the time of invoking this syscall), resets idle
|
|
* thread utilisation to 0, and starts tracking utilisation.
|
|
*
|
|
* @return A `seL4_Error` error if the user-level log buffer has not been set by the user
|
|
* (`BENCHMARK_TRACEPOINTS`/`BENCHMARK_TRACK_KERNEL_ENTRIES`).
|
|
*/
|
|
LIBSEL4_INLINE_FUNC seL4_Error
|
|
seL4_BenchmarkResetLog(void);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Finalize Log" label="sel4_benchmarkfinalizelog"/> @endxmlonly
|
|
* @brief Stop benchmark logging.
|
|
*
|
|
* The behaviour of this system call depends on benchmarking mode in action while invoking this system call:
|
|
* 1. `BENCHMARK_TRACEPOINTS`: Sets the final log buffer index to the current index,
|
|
* 2. `BENCHMARK_TRACK_KERNEL_ENTRIES`: as above,
|
|
* 3. `BENCHMARK_TRACK_UTILISATION`: sets benchmark end time to current time, stops tracking utilisation.
|
|
*
|
|
* @return The index of the final entry in the log buffer (if `BENCHMARK_TRACEPOINTS`/`BENCHMARK_TRACK_KERNEL_ENTRIES` are enabled).
|
|
*
|
|
*/
|
|
LIBSEL4_INLINE_FUNC seL4_Word
|
|
seL4_BenchmarkFinalizeLog(void);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Set Log Buffer" label="sel4_benchmarksetlogbuffer"/> @endxmlonly
|
|
* @brief Set log buffer.
|
|
*
|
|
* Provide a large frame object for the kernel to use as a log-buffer.
|
|
* The object must not be device memory, and must be seL4_LargePageBits in size.
|
|
*
|
|
* @param[in] frame_cptr A capability pointer to a user allocated frame of seL4_LargePage size.
|
|
* @return A `seL4_IllegalOperation` error if `frame_cptr` is not valid and couldn't set the buffer.
|
|
*
|
|
*/
|
|
LIBSEL4_INLINE_FUNC seL4_Error
|
|
seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Null Syscall" label="sel4_benchmarknullsyscall"/> @endxmlonly
|
|
* @brief Null system call that enters and exits the kernel immediately, for timing kernel traps in microbenchmarks.
|
|
*
|
|
* Used to time kernel traps (in and out).
|
|
*
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_BenchmarkNullSyscall(void);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Flush Caches" label="sel4_benchmarkflushcaches"/> @endxmlonly
|
|
* @brief Flush hardware caches.
|
|
*
|
|
* Flush all possible hardware caches for this platform.
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_BenchmarkFlushCaches(void);
|
|
|
|
#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
|
|
/**
|
|
* @xmlonly <manual name="Get Thread Utilisation" label="sel4_benchmarkgetthreadutilisation"/> @endxmlonly
|
|
* @brief Get utilisation timing information.
|
|
*
|
|
* Get timing information for the system, requested thread and idle thread. Such information is written
|
|
* into the caller's IPC buffer; see the definition of `benchmark_track_util_ipc_index` enum for more
|
|
* details on the data/format returned on the IPC buffer.
|
|
*
|
|
* @param[in] tcb_cptr TCB cap pointer to a thread to get CPU utilisation for.
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr);
|
|
|
|
/**
|
|
* @xmlonly <manual name="Reset Thread Utilisation" label="sel4_benchmarkresetthreadutilisation"/> @endxmlonly
|
|
* @brief Reset utilisation timing for a specific thread.
|
|
*
|
|
* Reset the kernel's timing information data (start time and utilisation) for a specific thread.
|
|
*
|
|
* @param[in] tcb_cptr TCB cap pointer to a thread to get CPU utilisation for.
|
|
*
|
|
*/
|
|
LIBSEL4_INLINE_FUNC void
|
|
seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr);
|
|
#endif
|
|
#endif
|
|
/** @} */
|
|
|
|
#ifdef CONFIG_ARCH_X86
|
|
/**
|
|
* @defgroup X86SystemCalls X86 System Calls
|
|
* @{
|
|
*/
|
|
|
|
#ifdef CONFIG_VTX
|
|
/**
|
|
* @xmlonly <manual name="VMEnter" label="sel4_vmenter"/> @endxmlonly
|
|
* @brief Change current thread to execute from its bound VCPU
|
|
*
|
|
* Changes the execution mode of the current thread from normal TCB execution, to
|
|
* guest execution using its bound VCPU.
|
|
* @xmlonly
|
|
* For details on VCPUs and execution modes see <autoref label="sec:virt"/>.
|
|
* @endxmlonly
|
|
*
|
|
* Invoking `seL4_VMEnter` is similar to replying to a fault in that updates to the registers
|
|
* can be given in the message, but unlike a fault no message info
|
|
* @xmlonly
|
|
* (see <autoref label="sec:messageinfo"/>)
|
|
* @endxmlonly
|
|
* is sent as the registers are not optional and the number that must be sent is fixed.
|
|
* The mapping of hardware register to message register is
|
|
* - `SEL4_VMENTER_CALL_EIP_MR` Address to start executing instructions at in the guest mode
|
|
* - `SEL4_VMENTER_CALL_CONTROL_PPC_MR` New value for the Primary Processor Based VM Execution Controls
|
|
* - `SEL4_VMENTER_CALL_CONTROL_ENTRY_MR` New value for the VM Entry Controls
|
|
*
|
|
* On return these same three message registers will be filled with the values at the point
|
|
* that the privlidged mode ceased executing. If this function returns with `SEL4_VMENTER_RESULT_FAULT`
|
|
* then the following additional message registers will be filled out
|
|
* - `SEL4_VMENTER_FAULT_REASON_MR`
|
|
* - `SEL4_VMENTER_FAULT_QUALIFICATION_MR`
|
|
* - `SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR`
|
|
* - `SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR`
|
|
* - `SEL4_VMENTER_FAULT_RFLAGS_MR`
|
|
* - `SEL4_VMENTER_FAULT_GUEST_INT_MR`
|
|
* - `SEL4_VMENTER_FAULT_CR3_MR`
|
|
* - `SEL4_VMENTER_FAULT_EAX`
|
|
* - `SEL4_VMENTER_FAULT_EBX`
|
|
* - `SEL4_VMENTER_FAULT_ECX`
|
|
* - `SEL4_VMENTER_FAULT_EDX`
|
|
* - `SEL4_VMENTER_FAULT_ESI`
|
|
* - `SEL4_VMENTER_FAULT_EDI`
|
|
* - `SEL4_VMENTER_FAULT_EBP`
|
|
*
|
|
* @param[out] sender The address to write sender information to.
|
|
* If the syscall returns due to receiving a notification
|
|
* on the bound notification then the sender information
|
|
* is the badge of the notification capability that was invoked.
|
|
* This parameter is ignored if `NULL`.
|
|
* @return `SEL4_VMENTER_RESULT_NOTIF` if a notification was received or `SEL4_VMENTER_RESULT_FAULT`
|
|
* if the guest mode execution faulted for any reason
|
|
*/
|
|
LIBSEL4_INLINE_FUNC seL4_Word
|
|
seL4_VMEnter(seL4_Word *sender);
|
|
#endif
|
|
|
|
/** @} */
|
|
#endif
|
|
|
|
/** @} */
|
|
|
|
#endif /* __LIBSEL4_SYSCALLS_H */
|