API Reference

Note: This page is auto-generated from the libsel4 API

System Calls


General System Calls

Send

LIBSEL4_INLINE_FUNC void seL4_Send

Send to a capability.

Type Name Description
seL4_CPtr dest The capability to be invoked.
seL4_MessageInfo_t msgInfo The messageinfo structure for the IPC.

Return value: This method does not return anything.

Recv

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv

Block until a message is received on an endpoint.

Type Name Description
seL4_CPtr src The capability to be invoked.
seL4_Word * 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 value: A seL4_MessageInfo_t structure

Call

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call

Call a capability.

Type Name Description
seL4_CPtr dest The capability to be invoked.
seL4_MessageInfo_t msgInfo The messageinfo structure for the IPC.

Return value: A seL4_MessageInfo_t structure

Reply

LIBSEL4_INLINE_FUNC void seL4_Reply

Perform a send to a one-off reply capability stored when the thread was last called.

Type Name Description
seL4_MessageInfo_t msgInfo The messageinfo structure for the IPC.

Return value: This method does not return anything.

Non-Blocking Send

LIBSEL4_INLINE_FUNC void seL4_NBSend

Perform a non-blocking send to a capability.

Type Name Description
seL4_CPtr dest The capability to be invoked.
seL4_MessageInfo_t msgInfo The messageinfo structure for the IPC.

Return value: This method does not return anything.

Reply Recv

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv

Perform a reply followed by a receive in one system call.

Type Name Description
seL4_CPtr dest The capability to be invoked.
seL4_MessageInfo_t msgInfo The messageinfo structure for the IPC.
seL4_Word * 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 value: A seL4_MessageInfo_t structure

NBRecv

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv

Receive a message from an endpoint but do not block in the case that no messages are pending.

Type Name Description
seL4_CPtr src The capability to be invoked.
seL4_Word * 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 value: A seL4_MessageInfo_t structure

Yield

LIBSEL4_INLINE_FUNC void seL4_Yield

Donate the remaining timeslice to a thread of the same priority.

Return value: This method does not return anything.

Signal

LIBSEL4_INLINE_FUNC void seL4_Signal

Signal a notification.

Type Name Description
seL4_CPtr dest The capability to be invoked.

Return value: This method does not return anything.

Description: 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.

Wait

LIBSEL4_INLINE_FUNC void seL4_Wait

Perform a receive on a notification object.

Type Name Description
seL4_CPtr src The capability to be invoked.
seL4_Word * 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 value: This method does not return anything.

Description: This is not a proper system call known by the kernel. Rather, it is a convenience wrapper which calls seL4_Recv.

Poll

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll

Perform a non-blocking recv on a notification object.

Type Name Description
seL4_CPtr src The capability to be invoked.
seL4_Word * 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 value: A seL4_MessageInfo_t structure

Description: 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.

Debugging System Calls

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.

Put Char

LIBSEL4_INLINE_FUNC void seL4_DebugPutChar

Output a single char through the kernel.

Type Name Description
char c The character to output.

Return value: This method does not return anything.

Description: Use the kernel serial driver to output a single character. This is useful for debugging when a user level serial driver is not available.

Dump scheduler

LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler

Output the contents of the kernel scheduler.

Return value: This method does not return anything.

Description: 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.

Halt

LIBSEL4_INLINE_FUNC void seL4_DebugHalt

Halt the system.

Return value: This method does not return anything.

Description: 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.

Snapshot

LIBSEL4_INLINE_FUNC void seL4_DebugSnapshot

Output a capDL dump of the current kernel state.

Return value: This method does not return anything.

Description: This debugging system call will output all of the capabilities in the current kernel using capDL.

Cap Identify

LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify

Identify the type of a capability in the current cspace.

Type Name Description
seL4_CPtr cap A capability slot in the current cspace.

Return value: The type of capability passed in.

Description: 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.

Name Thread

LIBSEL4_INLINE_FUNC void seL4_DebugNameThread

Name a thread.

Type Name Description
seL4_CPtr tcb A capability to the tcb object for the thread to name.
const char * name The name for the thread.

Return value: This method does not return anything.

Description: 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.

Run

LIBSEL4_INLINE_FUNC void seL4_DebugRun

Run a user level function in kernel mode.

Type Name Description
void(*)(void *) userfn The address in userspace of the function to run.
void * userarg A single argument to pass to the function.

Return value: This method does not return anything.

Description: 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.

Benchmarking System Calls

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.

Reset Log

LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkResetLog

Reset benchmark logging.

Return value: A seL4_Error error if the user-level log buffer has not been set by the user (BENCHMARK_TRACEPOINTS/BENCHMARK_TRACK_KERNEL_ENTRIES).

Description: 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.

Finalize Log

LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkFinalizeLog

Stop benchmark logging.

Return value: The index of the final entry in the log buffer (if BENCHMARK_TRACEPOINTS/BENCHMARK_TRACK_KERNEL_ENTRIES are enabled).

Description: 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.

Set Log Buffer

LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer

Set log buffer.

Type Name Description
seL4_Word frame_cptr A capability pointer to a user allocated frame of seL4_LargePage size.

Return value: A seL4_IllegalOperation error if frame_cptr is not valid and couldn’t set the buffer.

Description: 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.

Null Syscall

LIBSEL4_INLINE_FUNC void seL4_BenchmarkNullSyscall

Null system call that enters and exits the kernel immediately, for timing kernel traps in microbenchmarks.

Return value: This method does not return anything.

Description: Used to time kernel traps (in and out).

Flush Caches

LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushCaches

Flush hardware caches.

Return value: This method does not return anything.

Description: Flush all possible hardware caches for this platform.

Get Thread Utilisation

LIBSEL4_INLINE_FUNC void seL4_BenchmarkGetThreadUtilisation

Get utilisation timing information.

Type Name Description
seL4_Word tcb_cptr TCB cap pointer to a thread to get CPU utilisation for.

Return value: This method does not return anything.

Description: 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.

Reset Thread Utilisation

LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation

Reset utilisation timing for a specific thread.

Type Name Description
seL4_Word tcb_cptr TCB cap pointer to a thread to get CPU utilisation for.

Return value: This method does not return anything.

Description: Reset the kernel’s timing information data (start time and utilisation) for a specific thread.

X86 System Calls

VMEnter

LIBSEL4_INLINE_FUNC seL4_Word seL4_VMEnter

Change current thread to execute from its bound VCPU.

Type Name Description
seL4_Word * 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 value: SEL4_VMENTER_RESULT_NOTIF if a notification was received or SEL4_VMENTER_RESULT_FAULT if the guest mode execution faulted for any reason

Description: Changes the execution mode of the current thread from normal TCB execution, to guest execution using its bound VCPU.

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 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

Architecture-Independent Object Methods


seL4_CNode

Cancel Badged Sends

static inline int seL4_CNode_CancelBadgedSends

The cancel badged sends method is intend to allow for the reuse of badges by an authority. When used with a badged endpoint capability it will cancel any outstanding send operations for that endpoint and badge. This operation has no effect on un-badged or other objects.

Type Name Description
seL4_CNode _service CPTR to the CNode at the root of the CSpace where the capability will be found. Must be at a depth of 32.
seL4_Word index CPTR to the capability. Resolved from the root of the _service parameter.
seL4_Uint8 depth Number of bits of index to resolve to find the capability being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Copy

static inline int seL4_CNode_Copy

Copy a capability, setting its access rights whilst doing so

Type Name Description
seL4_CNode _service CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Word dest_index CPTR to the destination slot. Resolved from the root of the destination CSpace.
seL4_Uint8 dest_depth Number of bits of dest_index to resolve to find the destination slot.
seL4_CNode src_root CPTR to the CNode that forms the root of the source CSpace. Must be at a depth of 32.
seL4_Word src_index CPTR to the source slot. Resolved from the root of the source CSpace.
seL4_Uint8 src_depth Number of bits of src_index to resolve to find the source slot.
seL4_CapRights_t rights The rights inherited by the new capability.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Delete

static inline int seL4_CNode_Delete

Delete a capability

Type Name Description
seL4_CNode _service CPTR to the CNode at the root of the CSpace where the capability will be found. Must be at a depth of 32.
seL4_Word index CPTR to the capability. Resolved from the root of the _service parameter.
seL4_Uint8 depth Number of bits of index to resolve to find the capability being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Mint

static inline int seL4_CNode_Mint

Copy a capability, setting its access rights and badge whilst doing so

Type Name Description
seL4_CNode _service CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Word dest_index CPTR to the destination slot. Resolved from the root of the destination CSpace.
seL4_Uint8 dest_depth Number of bits of dest_index to resolve to find the destination slot.
seL4_CNode src_root CPTR to the CNode that forms the root of the source CSpace. Must be at a depth of 32.
seL4_Word src_index CPTR to the source slot. Resolved from the root of the source CSpace.
seL4_Uint8 src_depth Number of bits of src_index to resolve to find the source slot.
seL4_CapRights_t rights The rights inherited by the new capability.
seL4_Word badge Badge or guard to be applied to the new capability. For badges the high 4 bits are ignored.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Move

static inline int seL4_CNode_Move

Move a capability

Type Name Description
seL4_CNode _service CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Word dest_index CPTR to the destination slot. Resolved from the root of the destination CSpace.
seL4_Uint8 dest_depth Number of bits of dest_index to resolve to find the destination slot.
seL4_CNode src_root CPTR to the CNode that forms the root of the source CSpace. Must be at a depth of 32.
seL4_Word src_index CPTR to the source slot. Resolved from the root of the source CSpace.
seL4_Uint8 src_depth Number of bits of src_index to resolve to find the source slot.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Mutate

static inline int seL4_CNode_Mutate

Move a capability, setting its badge in the process

Type Name Description
seL4_CNode _service CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Word dest_index CPTR to the destination slot. Resolved from the root of the destination CSpace.
seL4_Uint8 dest_depth Number of bits of dest_index to resolve to find the destination slot.
seL4_CNode src_root CPTR to the CNode that forms the root of the source CSpace. Must be at a depth of 32.
seL4_Word src_index CPTR to the source slot. Resolved from the root of the source CSpace.
seL4_Uint8 src_depth Number of bits of src_index to resolve to find the source slot.
seL4_Word badge Badge or guard to be applied to the new capability. For badges the high 4 bits are ignored.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Revoke

static inline int seL4_CNode_Revoke

Delete all child capabilities of a capability

Type Name Description
seL4_CNode _service CPTR to the CNode at the root of the CSpace where the capability will be found. Must be at a depth of 32.
seL4_Word index CPTR to the capability. Resolved from the root of the _service parameter.
seL4_Uint8 depth Number of bits of index to resolve to find the capability being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Rotate

static inline int seL4_CNode_Rotate

Given 3 capability slots - a destination, pivot and source - move the capability in the pivot slot to the destination slot and the capability in the source slot to the pivot slot

Type Name Description
seL4_CNode _service CPTR to the CNode at the root of the CSpace where the destination slot will be found. Must be at a depth of 32.
seL4_Word dest_index CPTR to the destination slot. Resolved relative to _service. Must be empty unless it refers to the same slot as the source slot.
seL4_Uint8 dest_depth Depth to resolve dest_index to.
seL4_Word dest_badge The new capdata for the capability that ends up in the destination slot.
seL4_CNode pivot_root CPTR to the CNode at the root of the CSpace where the pivot slot will be found. Must be at a depth of 32.
seL4_Word pivot_index CPTR to the pivot slot. Resolved relative to pivot_root. The resolved slot must not refer to the source or destination slots.
seL4_Uint8 pivot_depth Depth to resolve pivot_index to.
seL4_Word pivot_badge The new capdata for the capability that ends up in the pivot slot.
seL4_CNode src_root CPTR to the CNode at the root of the CSpace where the source slot will be found. Must be at a depth of 32.
seL4_Word src_index CPTR to the source slot. Resolved relative to src_root.
seL4_Uint8 src_depth Depth to resolve src_index to.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Save Caller

static inline int seL4_CNode_SaveCaller

Save the reply capability from the last time the thread was called in the given CSpace so that it can be invoked later

Type Name Description
seL4_CNode _service CPTR to the CNode at the root of the CSpace where the capability is to be saved. Must be at a depth of 32.
seL4_Word index CPTR to the slot in which to save the capability. Resolved from the root of the _service parameter.
seL4_Uint8 depth Number of bits of index to resolve to find the slot being targeted.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_DomainSet

Set

static inline int seL4_DomainSet_Set

Change the domain of a thread.

Type Name Description
seL4_DomainSet _service Capability allowing domain configuration.
seL4_Uint8 domain The thread’s new domain.
seL4_TCB thread Capability to the TCB which is being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_IRQControl

Get

static inline int seL4_IRQControl_Get

Create an IRQ handler capability

Type Name Description
seL4_IRQControl _service An IRQControl capability. This gives you the authority to make this call.
int irq The IRQ that you want this capability to handle.
seL4_CNode root CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Word index CPTR to the destination slot. Resolved from the root of the destination CSpace.
seL4_Uint8 depth Number of bits of dest_index to resolve to find the destination slot.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_IRQHandler

Acknowledge

static inline int seL4_IRQHandler_Ack

Acknowledge the receipt of an interrupt and re-enable it

Type Name Description
seL4_IRQHandler _service The IRQ handler capability.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Clear

static inline int seL4_IRQHandler_Clear

Clear the handler capability from the IRQ slot

Type Name Description
seL4_IRQHandler _service The IRQ handler capability.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Set Notification

static inline int seL4_IRQHandler_SetNotification

Set the notification which the kernel will signal on interrupts controlled by the supplied IRQ handler capability

Type Name Description
seL4_IRQHandler _service The IRQ handler capability.
seL4_CPtr notification The notification which the IRQs will signal.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_TCB

Bind Notification

static inline int seL4_TCB_BindNotification

Binds a notification object to a TCB

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_CPtr notification Notification to bind.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Configure Single Stepping

static inline seL4_TCB_ConfigureSingleStepping_t seL4_TCB_ConfigureSingleStepping

Set or modify single stepping options for the target TCB. Subsequent calls to this function overwrite previous configuration. Depending on your processor architecture, this may or may not require the consumption of a hardware register.

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_Uint16 bp_num The API-ID of a target breakpoint. This ID will be a positive integer, with values ranging from 0 to seL4_NumHWBreakpoints - 1.
seL4_Word num_instructions Number of instructions to step over before delivering a fault to the target thread’s fault endpoint. Setting this to 0 disables single-stepping.

Return value: A seL4_TCB_ConfigureSingleStepping_t: Struct that contains seL4_Error error, an seL4 API error value, seL4_Bool bp_was_consumed, a boolean which indicates whether or not the bp_num breakpoint ID that was passed to the function, was consumed in the setup of the single-stepping functionality: if this is true, the caller should not attempt to re-use bp_num until it has disabled the single-stepping functionality via a subsequent call to seL4_TCB_ConfigureSingleStepping with an num_instructions argument of 0.

Configure

static inline int seL4_TCB_Configure

Set the parameters of a TCB

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_Word fault_ep CPTR to the endpoint which receives IPCs when this thread faults. This capability is in the CSpace of the thread being configured.
seL4_CNode cspace_root The new CSpace root.
seL4_Word cspace_root_data Optionally set the guard and guard size of the new root CNode. If set to zero, this parameter has no effect.
seL4_CNode vspace_root The new VSpace root.
seL4_Word vspace_root_data Has no effect on x86 or ARM processors.
seL4_Word buffer Location of the thread’s IPC buffer. Must be 512-byte aligned. The IPC buffer may not cross a page boundary.
seL4_CPtr bufferFrame Capability to a page containing the thread’s IPC buffer.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Copy Registers

static inline int seL4_TCB_CopyRegisters

Copy the registers from one thread to another

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on. This is the destination TCB.
seL4_TCB source Cap to the source TCB.
seL4_Bool suspend_source The invocation should also suspend the source thread.
seL4_Bool resume_target The invocation should also resume the destination thread.
seL4_Bool transfer_frame Frame registers should be transferred.
seL4_Bool transfer_integer Integer registers should be transferred.
seL4_Uint8 arch_flags Architecture dependent flags. These have no mearing on either x86 or ARM.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: In the context of this function, frame registers are those that are read, modified or preserved by a system call and integer registers are those that are not. Refer to the seL4 userland library source for specifics.

Get Breakpoint

static inline seL4_TCB_GetBreakpoint_t seL4_TCB_GetBreakpoint

Read a breakpoint or watchpoint’s current configuration.

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_Uint16 bp_num The API-ID of a target breakpoint. This ID will be a positive integer, with values ranging from 0 to seL4_NumHWBreakpoints - 1.

Return value: A seL4_TCB_GetBreakpoint_t: Struct that contains seL4_Error error, an seL4 API error value, seL4_Word vaddr, the virtual address at which the breakpoint will currently be triggered; seL4_Word type, the type of operation which will currently trigger the breakpoint, whether instruction execution, or data access; seL4_Word size, integer value for the span-size of the breakpoint. Usually a power of two (1, 2, 4, etc.); seL4_Word rw, the access direction that will currently trigger the breakpoint, whether read, write, or both and seL4_Bool is_enabled, which indicates whether or not the breakpoint will currently be triggered if the match conditions are met.

Read Registers

static inline int seL4_TCB_ReadRegisters

Read a thread’s registers into the first count fields of a given seL4_UserContext

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_Bool suspend_source The invocation should also suspend the source thread.
seL4_Uint8 arch_flags Architecture dependent flags. These have no mearing on either x86 or ARM.
seL4_Word count The number of registers to read.
seL4_UserContext * regs The structure to read the registers into.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Resume

static inline int seL4_TCB_Resume

Resume a thread

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Set Breakpoint

static inline int seL4_TCB_SetBreakpoint

Set or modify a thread’s breakpoints or watchpoints. Calls to this function overwrite previous configurations for the target breakpoint. Do not use this with seL4_SingleStep: the API will reject the call and return an error. Instead, use seL4_TCB_ConfigureSingleStepping to configure single-stepping.

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_Uint16 bp_num The API-ID of a target breakpoint. This ID will be a positive integer, with values ranging from 0 to seL4_NumHWBreakpoints - 1.
seL4_Word vaddr A virtual address which forms part of the match conditions for the triggering of the breakpoint.
seL4_Word type One of: seL4_InstructionBreakpoint, which specifies that the breakpoint should occur on instruction execution at the specified vaddr or seL4_DataBreakpoint, which states that the breakpoint should occur on data access at the specified vaddr.
seL4_Word size A positive integer indicating the trigger-span of the watchpoint. Must be zero when ‘type’ is seL4_InstructionBreakpoint.
seL4_Word rw One of seL4_BreakOnRead, meaning the breakpoint will only be triggered on read-access; seL4_BreakOnWrite meaning the breakpoint will only be triggered on write-access, and seL4_BreakOnReadWrite meaning the breakpoint will be triggered on any access.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Set CPU Affinity

static inline int seL4_TCB_SetAffinity

Change a thread’s current CPU in multicore machine

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_Word affinity The thread’s new CPU to run.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Set IPC Buffer

static inline int seL4_TCB_SetIPCBuffer

Set a thread’s IPC buffer

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_Word buffer Location of the thread’s IPC buffer. Must be 512-byte aligned. The IPC buffer may not cross a page boundary.
seL4_CPtr bufferFrame Capability to a page containing the thread’s IPC buffer.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: See Sections threads and messageinfo

Set Maximum Controlled Priority

static inline int seL4_TCB_SetMCPriority

Change a thread’s maximum controlled priority

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_CPtr authority Capability to the TCB to use the MCP from when setting the MCP.
seL4_Word mcp The thread’s new maximum controlled priority.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Set Priority

static inline int seL4_TCB_SetPriority

Change a thread’s priority

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_CPtr authority Capability to the TCB to use the MCP from when setting the priority.
seL4_Word priority The thread’s new priority.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Set Sched Params

static inline int seL4_TCB_SetSchedParams

Change a thread’s priority and maximum controlled priority.

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_CPtr authority Capability to the TCB to use the MCP from when setting the priority and MCP.
seL4_Word mcp The thread’s new maximum controlled priority.
seL4_Word priority The thread’s new priority.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Set Space

static inline int seL4_TCB_SetSpace

Set the fault endpoint, CSpace and VSpace of a thread

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_Word fault_ep CPTR to the endpoint which receives IPCs when this thread faults. This capability is in the CSpace of the thread being configured.
seL4_CNode cspace_root The new CSpace root.
seL4_Word cspace_root_data Optionally set the guard and guard size of the new root CNode. If set to zero, this parameter has no effect.
seL4_CNode vspace_root The new VSpace root.
seL4_Word vspace_root_data Has no effect on x86 or ARM processors.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Suspend

static inline int seL4_TCB_Suspend

Suspend a thread

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Unbind Notification

static inline int seL4_TCB_UnbindNotification

Unbinds any notification object from a TCB

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Unset Breakpoint

static inline int seL4_TCB_UnsetBreakpoint

Disables a hardware breakpoint or watchpoint. The caller should assume that the underlying configuration of the hardware registers has also been cleared. Do not use this to clear single-stepping: the API will reject the call and return an error. Instead, use seL4_TCB_ConfigureSingleStepping to disable single-stepping.

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_Uint16 bp_num The API-ID of a target breakpoint. This ID will be a positive integer, with values ranging from 0 to seL4_NumHWBreakpoints - 1.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Write Registers

static inline int seL4_TCB_WriteRegisters

Set a thread’s registers to the first count fields of a given seL4_UserContext

Type Name Description
seL4_TCB _service Capability to the TCB which is being operated on.
seL4_Bool resume_target The invocation should also resume the destination thread.
seL4_Uint8 arch_flags Architecture dependent flags. These have no mearing on either x86 or ARM.
seL4_Word count The number of registers to be set.
seL4_UserContext * regs Data structure containing the new register values.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_Untyped

Retype

static inline int seL4_Untyped_Retype

Retype an untyped object

Type Name Description
seL4_Untyped _service CPTR to an untyped object.
seL4_Word type The seL4 object type that we are retyping to.
seL4_Word size_bits Used to determine the size of variable-sized objects.
seL4_CNode root CPTR to the CNode at the root of the destination CSpace.
seL4_Word node_index CPTR to the destination CNode. Resolved relative to the root parameter.
seL4_Word node_depth Number of bits of node_index to translate when addressing the destination CNode.
seL4_Word node_offset Number of slots into the node at which capabilities start being placed.
seL4_Word num_objects Number of capabilities to create.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Given a capability, _service, to an untyped object, creates num_objects of the requested type. Creates num_objects capabilities to the new objects starting at node_offset in the CNode specified by root, node_index, and node_depth. For variable-sized kernel objects, the size_bits argument is used to determine the size of objects to create. The relationship between size_bits and object size depends on the type of object being created.

x86-Specific Object Methods


General x86 Object Methods

seL4_IRQControl

Get I/O APIC

static inline int seL4_IRQControl_GetIOAPIC

Create an IRQ handler capability for an interrupt from an IOAPIC.

Type Name Description
seL4_IRQControl _service An IRQControl capability. This gives you the authority to make this call.
seL4_CNode root CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Word index CPTR to the destination slot. Resolved from the root of the destination CSpace.
seL4_Uint8 depth Number of bits of index to resolve to find the destination slot.
seL4_Word ioapic Zero based index of IOAPIC to get interrupt from, ordered the same as in ACPI tables
seL4_Word pin IOAPIC pin that generates the interrupt.
seL4_Word level Indicates whether the IOAPIC should be programmed to treat this interrupt as level triggered.
seL4_Word polarity Indicates whether the IOAPIC should be programmed to treat this interrupt as high or low triggered
seL4_Word vector CPU vector to deliver the interrupt to.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Get MSI

static inline int seL4_IRQControl_GetMSI

Create an IRQ handler capability for an interrupt from an MSI.

Type Name Description
seL4_IRQControl _service An IRQControl capability. This gives you the authority to make this call.
seL4_CNode root CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Word index CPTR to the destination slot. Resolved from the root of the destination CSpace.
seL4_Uint8 depth Number of bits of index to resolve to find the destination slot.
seL4_Word pci_bus PCI bus ID of the device that will generate the interrupt.
seL4_Word pci_dev PCI device ID of the device that will generate the interrupt.
seL4_Word pci_func PCI function ID of the device that will generate the interrupt.
seL4_Word handle Value of the handle programmed into the data portion of the MSI.
seL4_Word vector CPU vector to deliver the interrupt to.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_TCB

Set EPT Root

static inline int seL4_TCB_SetEPTRoot

Set the EPT root of a thread

Type Name Description
seL4_TCB _service TODO
seL4_CPtr eptpml4 CPTR to an EPT PML4 object to act as the guest mode vspace root

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_X86_ASIDControl

Make Pool

static inline int seL4_X86_ASIDControl_MakePool

Create an X86 ASID pool.

Type Name Description
seL4_X86_ASIDControl _service The master ASIDControl capability.
seL4_Untyped untyped Capability to an untyped memory object that will become the pool. Must be 4K bytes.
seL4_CNode root CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Word index CPTR to the destination slot. Resolved from the root of the destination CSpace.
seL4_Uint8 depth Number of bits of index to resolve to find the destination slot.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Together with a capability to Untyped Memory, which is passed as an argument, create an ASID Pool. The untyped capability must represent a 4K memory object. This will create an ASID pool with enough space for 1024 VSpaces. ### seL4_X86_ASIDPool

Assign

static inline int seL4_X86_ASIDPool_Assign

Assign an ASID pool.

Type Name Description
seL4_X86_ASIDPool _service The ASID pool which is being assigned to. Must not be full. Each ASID pool can contain 1024 entries.
seL4_CPtr vspace The page directory that is being assigned to an ASID pool. Must not already be assigned to an ASID pool.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Assigns an ASID to the VSpace associated with the Page Directory passed in as an argument. ### seL4_X86_EPTPD

Map

static inline int seL4_X86_EPTPD_Map

Map an EPT page directory.

Type Name Description
seL4_X86_EPTPD _service Capability to the EPT PD being operated on.
seL4_X86_EPTPML4 pml4 Capability to the EPT root which will contain the mapping
seL4_Word gpa Guest physical address to map the page into.
seL4_X86_VMAttributes attr VM attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Unmap

static inline int seL4_X86_EPTPD_Unmap

Unmap an EPT page directory.

Type Name Description
seL4_X86_EPTPD _service Capability to the EPT PD being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_X86_EPTPDPT

Map

static inline int seL4_X86_EPTPDPT_Map

Map an EPT page directory page table.

Type Name Description
seL4_X86_EPTPDPT _service Capability to the EPT PDPT being operated on.
seL4_X86_EPTPML4 pml4 Capability to the EPT root which will contain the mapping
seL4_Word gpa Guest physical address to map the page into.
seL4_X86_VMAttributes attr VM attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Unmap

static inline int seL4_X86_EPTPDPT_Unmap

Unmap an EPT page directory page table.

Type Name Description
seL4_X86_EPTPDPT _service Capability to the EPT PDPT being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_X86_EPTPT

Map

static inline int seL4_X86_EPTPT_Map

Map an EPT page table.

Type Name Description
seL4_X86_EPTPT _service Capability to the EPT PT being operated on.
seL4_X86_EPTPML4 pml4 Capability to the EPT root which will contain the mapping
seL4_Word gpa Guest physical address to map the page into.
seL4_X86_VMAttributes attr VM attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Unmap

static inline int seL4_X86_EPTPT_Unmap

Unmap an EPT page table.

Type Name Description
seL4_X86_EPTPT _service Capability to the EPT PT being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_X86_IOPageTable

Map

static inline int seL4_X86_IOPageTable_Map

Map an IO page table into an IOSpace.

Type Name Description
seL4_X86_IOPageTable _service Capability to the I/O page table being operated on.
seL4_X86_IOSpace iospace The IOSpace to map the page table into.
seL4_Word ioaddr The address to map the page table at.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Unmap

static inline int seL4_X86_IOPageTable_Unmap

Unmap an IO page table from an IOSpace.

Type Name Description
seL4_X86_IOPageTable _service Capability to the I/O page table being operated on.The page table to unmap.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_X86_IOPort

In16

static inline seL4_X86_IOPort_In16_t seL4_X86_IOPort_In16

Read 16 bits from an IO port.

Type Name Description
seL4_X86_IOPort _service An I/O Port capability.
seL4_Uint16 port The port to read from.

Return value: A seL4_X86_IOPort_In16_t structure

In32

static inline seL4_X86_IOPort_In32_t seL4_X86_IOPort_In32

Read 32 bits from an IO port.

Type Name Description
seL4_X86_IOPort _service An I/O Port capability.
seL4_Uint16 port The port to read from.

Return value: A seL4_X86_IOPort_In32_t structure

In8

static inline seL4_X86_IOPort_In8_t seL4_X86_IOPort_In8

Read 8 bits from an IO port.

Type Name Description
seL4_X86_IOPort _service An I/O Port capability.
seL4_Uint16 port The port to read from.

Return value: A seL4_X86_IOPort_In8_t structure

Out16

static inline int seL4_X86_IOPort_Out16

Write 16 bits to an IO port.

Type Name Description
seL4_X86_IOPort _service An I/O Port capability.
seL4_Word port The port to write to.
seL4_Word data Data to write to the IO port.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Out32

static inline int seL4_X86_IOPort_Out32

Write 32 bits to an IO port.

Type Name Description
seL4_X86_IOPort _service An I/O Port capability.
seL4_Word port The port to write to.
seL4_Word data Data to write to the IO port.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Out8

static inline int seL4_X86_IOPort_Out8

Write 8 bits to an IO port.

Type Name Description
seL4_X86_IOPort _service An I/O Port capability.
seL4_Word port The port to write to.
seL4_Word data Data to write to the IO port.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_X86_IOPortControl

Issue

static inline int seL4_X86_IOPortControl_Issue

Issue an IO port sub range.

Type Name Description
seL4_X86_IOPortControl _service Control capability for I/O ports.
seL4_Word first_port First port of the range of the issued capability.
seL4_Word last_port Last port of the range of the issued capability.
seL4_CNode root CPTR to the CNode that forms the root of the destination CSpace.
seL4_Word index CPTR to the destination slot. Resolved from the root of the destination CSpace.
seL4_Uint8 depth Number of bits of dest_index to resolve to find the destination slot.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_X86_Page

Get Address

static inline seL4_X86_Page_GetAddress_t seL4_X86_Page_GetAddress

Get the physical address of the underlying frame.

Type Name Description
seL4_X86_Page _service Capability to the page being operated on.

Return value: A seL4_IA32_Page_GetAddress_t struct that contains a seL4_Word paddr, which holds the physical address of the page, and int error.

Map EPT

static inline int seL4_X86_Page_MapEPT

TODO

Type Name Description
seL4_X86_Page _service Capability to the page being operated on.
seL4_X86_EPTPML4 vspace TODO
seL4_Word vaddr TODO
seL4_CapRights_t rights TODO
seL4_X86_VMAttributes attr TODO

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: TODO

Map I/O

static inline int seL4_X86_Page_MapIO

Map a page into an IOSpace.

Type Name Description
seL4_X86_Page _service Capability to the page being operated on.
seL4_X86_IOSpace iospace The IOSpace that the frame is being mapped into
seL4_CapRights_t rights Rights for the mapping.
seL4_Word ioaddr The address that the frame is being mapped at.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Map

static inline int seL4_X86_Page_Map

Map a page into an address space.

Type Name Description
seL4_X86_Page _service Capability to the page being operated on.
seL4_CPtr vspace Capability to the VSpace which will contain the mapping
seL4_Word vaddr Virtual address to map the page into.
seL4_CapRights_t rights Rights for the mapping.
seL4_X86_VMAttributes attr VM attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Takes a Page Directory capability, which refers to the VSpace, as an argument and installs a reference to the given Page in the lowest-level unmapped paging structure corresponding to the given address. If the required paging structures are not present this operation will fail, returning a seL4_FailedLookup error.

Remap

static inline int seL4_X86_Page_Remap

Remap a page.

Type Name Description
seL4_X86_Page _service Capability to the page being operated on.
seL4_CPtr vspace Capability to the VSpace which will contain the mapping
seL4_CapRights_t rights Rights for the mapping.
seL4_X86_VMAttributes attr VM attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Changes the permissions of an existing mapping.

Unmap

static inline int seL4_X86_Page_Unmap

Unmap a page.

Type Name Description
seL4_X86_Page _service Capability to the page being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Removes an existing mapping. ### seL4_X86_PageDirectory

Get Status Bits

static inline seL4_X86_PageDirectory_GetStatusBits_t seL4_X86_PageDirectory_GetStatusBits

Retrieve the accessed and dirty bits of a page mapped into an address space.

Type Name Description
seL4_X86_PageDirectory _service Capability to the page directory being operated on.Capability to the address space to query.
seL4_Word vaddr Virtual address of the page to query

Return value: A seL4_X86_PageDirectory_GetStatusBits_t structure.

Map

static inline int seL4_X86_PageDirectory_Map

Map a page directory.

Type Name Description
seL4_X86_PageDirectory _service Capability to the page directory being operated on.
seL4_CPtr vspace Capability to the VSpace which will contain the mapping
seL4_Word vaddr Virtual address to map the page into.
seL4_X86_VMAttributes attr VM attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Unmap

static inline int seL4_X86_PageDirectory_Unmap

Unmap a page directory.

Type Name Description
seL4_X86_PageDirectory _service Capability to the page directory being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_X86_PageTable

Map

static inline int seL4_X86_PageTable_Map

Map a page table into an address space.

Type Name Description
seL4_X86_PageTable _service Capability to the page table being operated on.
seL4_CPtr vspace Capability to the VSpace which will contain the mapping
seL4_Word vaddr Virtual address to map the page into.
seL4_X86_VMAttributes attr VM attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Takes a PageDirectory capability as an argument, and installs a reference to the invoked PageTable in a specified slot in the PageDirectory.

Unmap

static inline int seL4_X86_PageTable_Unmap

Unmap a page table from its address space and zero it out.

Type Name Description
seL4_X86_PageTable _service Capability to the page table being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Removes the reference to the invoked PageTable from its containing PageDirectory. ### seL4_X86_VCPU

Disable IO Port

static inline int seL4_X86_VCPU_DisableIOPort

Disable I/O port range in privileged execution

Type Name Description
seL4_X86_VCPU _service VCPU object to operate on
seL4_Word low Start of the I/O port range to disable
seL4_Word high Last I/O port in the range to disable

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Disable a range of I/O ports for direct access by the execution mode in the VCPU.

Enable IO Port

static inline int seL4_X86_VCPU_EnableIOPort

Enable I/O port range in guest execution

Type Name Description
seL4_X86_VCPU _service VCPU object to operate on
seL4_CPtr ioPort I/O port capability whose authority is being delegating
seL4_Word low Start of the I/O port range to enable
seL4_Word high Last I/O port in the range to enable

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Enables a range of I/O ports for direct access by the execution mode in the VCPU. The requested port range must be a sub range of the provided I/O port capability. This also establishes a link between the provided I/O port capability and the VCPU

Read VMCS

static inline seL4_X86_VCPU_ReadVMCS_t seL4_X86_VCPU_ReadVMCS

Read VMCS field from the hardware

Type Name Description
seL4_X86_VCPU _service VCPU object to operate on
seL4_Word field Field to give to vmread instruction

Return value: A seL4_X86_VCPU_ReadVMCS_t struct that contains a seL4_Word value, which holds the return result of the vmread instruction, and int error.

Description: Thin wrapper around the vmread instruction that is performed on the VMCS region that is part of the VCPU object. After validating that a legal field is requested the value of vmread is returned directly in the result.

Set TCB

static inline int seL4_X86_VCPU_SetTCB

Bind TCB to VCPU

Type Name Description
seL4_X86_VCPU _service VCPU object to operate on
seL4_CNode tcb CPTR of the TCB to bind to

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Configures the one-to-one binding of a VCPU and TCB, overwriting any previous binding in both.

Write Registers

static inline int seL4_X86_VCPU_WriteRegisters

Set guest mode registers to the fields of a given seL4_VCPUContext

Type Name Description
seL4_X86_VCPU _service VCPU object to operate on
seL4_VCPUContext * regs Data structure containing the new register values.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Sets the guest mode registers, which is any registers not already part of the VMCS.

Write VMCS

static inline seL4_X86_VCPU_WriteVMCS_t seL4_X86_VCPU_WriteVMCS

Write VMCS field to the hardware

Type Name Description
seL4_X86_VCPU _service VCPU object to operate on
seL4_Word field Field to give to vmwrite instruction
seL4_Word value Value to write using vmwrite instruction

Return value: A seL4_X86_VCPU_WriteVMCS_t struct that contains a seL4_Word writen, which holds the final value written with the vmwrite instruction, and int error.

Description: Thin wrapper around the vmwrite instruction that is performed on the VMCS region that is part of the VCPU object. As well as validating that a legal field is requested, the value may be modified to ensure any bits that are fixed in the hardware are correct, and that any features required for kernel correctness are not disabled . The final value written to the hardware is returned and can be compared to the input parameter to determine what bits the kernel changed.

IA32-Specific Object Methods

No methods.

x86_64-Specific Object Methods

seL4_X86_PDPT

Map

static inline int seL4_X86_PDPT_Map

TODO

Type Name Description
seL4_X86_PDPT _service TODO
seL4_X64_PML4 pml4 TODO
seL4_Word vaddr TODO
seL4_X86_VMAttributes attr TODO

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: TODO

Unmap

static inline int seL4_X86_PDPT_Unmap

TODO

Type Name Description
seL4_X86_PDPT _service TODO

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: TODO

ARM-Specific Object Methods


General ARM Object Methods

seL4_ARM_ASIDControl

Make Pool

static inline int seL4_ARM_ASIDControl_MakePool

Create an ASID Pool.

Type Name Description
seL4_ARM_ASIDControl _service The master ASIDControl capability being operated on.
seL4_Untyped untyped Capability to an untyped memory object that will become the pool. Must be 4K bytes.
seL4_CNode root CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Word index CPTR to the destination slot. Resolved from the root of the destination CSpace.
seL4_Uint8 depth Number of bits of index to resolve to find the destination slot.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Together with a capability to Untyped Memory, which is passed as an argument, create an ASID Pool. The untyped capability must represent a 4K memory object. This will create an ASID pool with enough space for 1024 VSpaces. ### seL4_ARM_ASIDPool

Asid Pool Assign

static inline int seL4_ARM_ASIDPool_Assign

Assign an ASID Pool.

Type Name Description
seL4_ARM_ASIDPool _service The ASID pool which is being assigned to. Must not be full. Each ASID pool can contain 1024 entries.
seL4_CPtr vspace The VSpace that is being assigned to an ASID pool. Must not already be assigned to an ASID pool.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Assigns an ASID to the VSpace passed in as an argument. ### seL4_ARM_IOPageTable

Map

static inline int seL4_ARM_IOPageTable_Map

TODO

Type Name Description
seL4_ARM_IOPageTable _service TODO
seL4_ARM_IOSpace iospace TODO
seL4_Word ioaddr TODO

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: TODO

Unmap

static inline int seL4_ARM_IOPageTable_Unmap

TODO

Type Name Description
seL4_ARM_IOPageTable _service TODO

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: TODO ### seL4_ARM_Page

Clean Data

static inline int seL4_ARM_Page_Clean_Data

Cleans the data cache out to RAM. The start and end are relative to the page being serviced.

Type Name Description
seL4_ARM_Page _service Capability to the page being operated on.
seL4_Word start_offset The offset, relative to the start of the page inclusive.
seL4_Word end_offset The offset, relative to the start of the page exclusive.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Clean and Invalidate Data

static inline int seL4_ARM_Page_CleanInvalidate_Data

Clean and invalidates the cache range within the given page. The range will be flushed out to RAM. The start and end are relative to the page being serviced.

Type Name Description
seL4_ARM_Page _service Capability to the page being operated on.
seL4_Word start_offset The offset, relative to the start of the page inclusive.
seL4_Word end_offset The offset, relative to the start of the page exclusive.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Get Address

static inline seL4_ARM_Page_GetAddress_t seL4_ARM_Page_GetAddress

Get the physical address of the underlying frame.

Type Name Description
seL4_ARM_Page _service Capability to the page being operated on.

Return value: A seL4_ARM_Page_GetAddress_t struct that contains a seL4_Word paddr, which holds the physical address of the page, and int error.

Invalidate Data

static inline int seL4_ARM_Page_Invalidate_Data

Invalidates the cache range within the given page. The start and end are relative to the page being serviced and should be aligned to a cache line boundary where possible. An additional clean is performed on the outer cache lines if the start and end are not aligned, to clean out the bytes between the requested and the cache line boundary.

Type Name Description
seL4_ARM_Page _service Capability to the page being operated on.
seL4_Word start_offset The offset, relative to the start of the page inclusive.
seL4_Word end_offset The offset, relative to the start of the page exclusive.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Map I/O

static inline int seL4_ARM_Page_MapIO

Type Name Description
seL4_ARM_Page _service Capability to the page being operated on.
seL4_ARM_IOSpace iospace TODO
seL4_CapRights_t rights TODO
seL4_Word ioaddr TODO

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: TODO

Map

static inline int seL4_ARM_Page_Map

Map a page into an address space.

Type Name Description
seL4_ARM_Page _service Capability to the page being operated on.
seL4_CPtr vspace Capability to the VSpace which will contain the mapping.
seL4_Word vaddr Virtual address to map the page into.
seL4_CapRights_t rights Rights for the mapping.
seL4_ARM_VMAttributes attr VM Attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Takes a VSpace capability, as an argument and installs a reference to the given Page in the lowest-level unmapped paging structure corresponding to the given address. If the required paging structures are not present this operation will fail, returning a seL4_FailedLookup error.

Remap

static inline int seL4_ARM_Page_Remap

Remap a page.

Type Name Description
seL4_ARM_Page _service Capability to the page being operated on.
seL4_CPtr vspace Capability to the VSpace which will contain the mapping.
seL4_CapRights_t rights Rights for the mapping.
seL4_ARM_VMAttributes attr VM Attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Changes the permissions of an existing mapping.

Unify Instruction

static inline int seL4_ARM_Page_Unify_Instruction

Unify Instruction Cache. Cleans data lines to point of unification, invalidate corresponding instruction lines to point of unification, then invalidates branch predictors. The start and end are relative to the page being serviced.

Type Name Description
seL4_ARM_Page _service Capability to the page being operated on.
seL4_Word start_offset The offset, relative to the start of the page inclusive.
seL4_Word end_offset The offset, relative to the start of the page exclusive.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Unmap

static inline int seL4_ARM_Page_Unmap

Unmap a page.

Type Name Description
seL4_ARM_Page _service Capability to the page being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Removes an existing mapping. ### seL4_ARM_PageTable

Map

static inline int seL4_ARM_PageTable_Map

Map a page table into an address space.

Type Name Description
seL4_ARM_PageTable _service Capability to the page table being operated on.
seL4_CPtr vspace Capability to the VSpace which will contain the mapping.
seL4_Word vaddr Virtual address to map the page into.
seL4_ARM_VMAttributes attr VM Attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Takes a VSpace capability as an argument, and installs a reference to the invoked PageTable in the VSpace according to the provided virtual address.

Unmap

static inline int seL4_ARM_PageTable_Unmap

Unmap a page table from its Page Directory and zero it out.

Type Name Description
seL4_ARM_PageTable _service Capability to the page table being operated on.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Removes the reference to the invoked Page Table from its containing Page Directory. ### seL4_ARM_VCPU

Inject IRQ

static inline int seL4_ARM_VCPU_InjectIRQ

Inject an IRQ to a virtual CPU

Type Name Description
seL4_ARM_VCPU _service TODO
seL4_Uint16 virq Virtual IRQ ID
seL4_Uint8 priority Priority of the IRQ to be injected
seL4_Uint8 group IRQ group
seL4_Uint8 index IRQ index

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: TODO

Read Registers

static inline seL4_ARM_VCPU_ReadRegs_t seL4_ARM_VCPU_ReadRegs

Read a virtual CPU register

Type Name Description
seL4_ARM_VCPU _service TODO
seL4_Word field Register to read from a VCPU

Return value: TODO

Description: TODO

Set TCB

static inline int seL4_ARM_VCPU_SetTCB

Bind a TCB to a virtual CPU

Type Name Description
seL4_ARM_VCPU _service TODO
seL4_TCB tcb Capability to TCB to bind to a virtual CPU

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: There is a 1:1 relationship between a virtual CPU and a TCB. If either (or both) of them is associated with another one, they will be dissociated, and then associated to the ones called in this system calls.

Write Registers

static inline int seL4_ARM_VCPU_WriteRegs

Write a virtual CPU register

Type Name Description
seL4_ARM_VCPU _service TODO
seL4_Word field Register ID to write to a VCPU
seL4_Word value Value to be written to the VCPU register

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: TODO

Aarch32-Specific Object Methods

seL4_ARM_PageDirectory

Clean Data

static inline int seL4_ARM_PageDirectory_Clean_Data

Clean cached pages within a page directory

Type Name Description
seL4_ARM_PageDirectory _service TODO
seL4_Word start Start address
seL4_Word end End address

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Clean and Invalidate Data

static inline int seL4_ARM_PageDirectory_CleanInvalidate_Data

Clean and invalidate cached pages within a page directory

Type Name Description
seL4_ARM_PageDirectory _service TODO
seL4_Word start Start address
seL4_Word end End address

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Invalidate Data

static inline int seL4_ARM_PageDirectory_Invalidate_Data

Invalidate cached pages within a page directory

Type Name Description
seL4_ARM_PageDirectory _service TODO
seL4_Word start Start address
seL4_Word end End address

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Unify Instruction

static inline int seL4_ARM_PageDirectory_Unify_Instruction

Clean and invalidate cached instruction pages to point of unification

Type Name Description
seL4_ARM_PageDirectory _service TODO
seL4_Word start Start address
seL4_Word end End address

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Aarch64-Specific Object Methods

seL4_ARM_PageDirectory

Map

static inline int seL4_ARM_PageDirectory_Map

Map a page directory

Type Name Description
seL4_ARM_PageDirectory _service TODO
seL4_CPtr pud Upper page directory
seL4_Word vaddr Virtual adress
seL4_ARM_VMAttributes attr Memory attributes

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Map a page directory (level 2) to an upper page directory (level 1)

Unmap

static inline int seL4_ARM_PageDirectory_Unmap

Unmap a page directory

Type Name Description
seL4_ARM_PageDirectory _service TODO

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Unmap a page directory (level 2) from an upper page directory (level 1) ### seL4_ARM_PageGlobalDirectory

Clean Data

static inline int seL4_ARM_PageGlobalDirectory_Clean_Data

Clean cached pages within a global page directory

Type Name Description
seL4_ARM_PageGlobalDirectory _service TODO
seL4_Word start Start address
seL4_Word end End address

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Clean and Invalidate Data

static inline int seL4_ARM_PageGlobalDirectory_CleanInvalidate_Data

Clean and invalidate cached pages within a global page directory

Type Name Description
seL4_ARM_PageGlobalDirectory _service TODO
seL4_Word start Start address
seL4_Word end End address

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Invalidate Data

static inline int seL4_ARM_PageGlobalDirectory_Invalidate_Data

Invalidate cached pages within a global page directory

Type Name Description
seL4_ARM_PageGlobalDirectory _service TODO
seL4_Word start Start address
seL4_Word end End address

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Unify Instruction

static inline int seL4_ARM_PageGlobalDirectory_Unify_Instruction

Clean and invalidate cached instruction pages to point of unification

Type Name Description
seL4_ARM_PageGlobalDirectory _service TODO
seL4_Word start TODO
seL4_Word end TODO

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

    ### seL4_ARM_PageUpperDirectory

Map

static inline int seL4_ARM_PageUpperDirectory_Map

Map an upper page directory

Type Name Description
seL4_ARM_PageUpperDirectory _service TODO
seL4_CPtr pgd Global page directory
seL4_Word vaddr Virtual address
seL4_ARM_VMAttributes attr Memory attributes

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Map an upper page directory (level 1) to a global page directory (level 0)

Unmap

static inline int seL4_ARM_PageUpperDirectory_Unmap

TODO

Type Name Description
seL4_ARM_PageUpperDirectory _service TODO

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: TODO

RISCV-Specific Object Methods


seL4_RISCV_ASIDControl

MakePool

static inline int seL4_RISCV_ASIDControl_MakePool

Create an ASID Pool.

Type Name Description
seL4_RISCV_ASIDControl _service The master ASIDControl capability to invoke.
seL4_Untyped untyped Capability to an untyped memory object that will become the pool. Must be 4K bytes.
seL4_CNode root CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Word index CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32.
seL4_Uint8 depth Number of bits of index to resolve to find the destination slot.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Together with a capability to Untyped Memory, which is passed as an argument, create an ASID Pool. The untyped capability must represent a 4K memory object. This will create an ASID pool with enough space for 1024 VSpaces. ### seL4_RISCV_ASIDPool

Assign

static inline int seL4_RISCV_ASIDPool_Assign

Assign an ASID Pool.

Type Name Description
seL4_RISCV_ASIDPool _service The ASID Pool capability to invoke, which must be to an ASID pool that is not full.
seL4_CPtr vspace The top-level PageTable that is being assigned to an ASID pool. Must not already be assigned to an ASID pool.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Assigns an ASID to the VSpace passed in as an argument. ### seL4_RISCV_Page

GetAddress

static inline seL4_RISCV_Page_GetAddress_t seL4_RISCV_Page_GetAddress

Get the physical address of a page.

Type Name Description
seL4_RISCV_Page _service Capability to the page to invoke.

Return value: A seL4_RISCV_Page_GetAddress_t struct that contains a seL4_Word paddr, which holds the physical address of the page, and int error.

Map

static inline int seL4_RISCV_Page_Map

Map a page into a page table.

Type Name Description
seL4_RISCV_Page _service Capability to the page to invoke.
seL4_RISCV_PageTable vspace VSpace to map the page into.
seL4_Word vaddr Virtual address at which to map the page.
seL4_CapRights_t rights Rights for the mapping.
seL4_RISCV_VMAttributes attr VM Attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Takes a VSpace, or top-level Page Table, capability as an argument and installs a reference to the given Page in the page table slot corresponding to the given address. If the required paging structures are not present this operation will fail, returning a seL4_FailedLookup error.

Remap

static inline int seL4_RISCV_Page_Remap

Remap a page.

Type Name Description
seL4_RISCV_Page _service Capability to the page to invoke.
seL4_RISCV_PageTable vspace VSpace to remap the page into.
seL4_CapRights_t rights Rights for the mapping.
seL4_RISCV_VMAttributes attr VM Attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Changes the permissions of an existing mapping.

Unmap

static inline int seL4_RISCV_Page_Unmap

Unmap a page.

Type Name Description
seL4_RISCV_Page _service Capability to the page to invoke.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Removes an existing mapping. ### seL4_RISCV_PageTable

Map

static inline int seL4_RISCV_PageTable_Map

Map a page table at a specific virtual address.

Type Name Description
seL4_RISCV_PageTable _service Capability to the page table to invoke.
seL4_RISCV_PageTable vspace VSpace to map the lower-level page table into.
seL4_Word vaddr Virtual address at which to map the page table.
seL4_RISCV_VMAttributes attr VM Attributes for the mapping.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.

Description: Starting from the VSpace, map the page table object at any unpopulated level for the provided virtual address. If all paging structures and mappings are present for this virtual address, return an seL4_DeleteFirst error.

Unmap

static inline int seL4_RISCV_PageTable_Unmap

Unmap a page table.

Type Name Description
seL4_RISCV_PageTable _service Capability to the page table to invoke.

Return value: A return value of 0 indicates success. A non-zero value indicates that an error occurred.