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. Does nothing if there is no reply capability which can happen if the blocked thread was unblocked via an operation such as destroying it.

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

Non-Blocking Recv

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

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.

Send SGI 0-15

LIBSEL4_INLINE_FUNC void seL4_DebugSendIPI

Sends arbitrary SGI.

Type	Name	Description
seL4_Uint8	target	The target core ID.
unsigned	irq	The SGI number (0-15).

Return value: This method does not return anything.

Description: Send an arbitrary SGI (core-specific interrupt 0-15) to the specified target core.

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

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.

Flush L1 Caches

LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushL1Caches

Flush L1 caches.

Type	Name	Description
seL4_Word	cache_type	L1 Cache Type to be flushed

Return value: This method does not return anything.

Description: Flush L1 caches for this platform (currently only support for ARM). Allow to specify the cache type to be flushed (i.e. instruction cache only, data cache only and both instruction cache and data cache).

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.

Dump All Threads Utilisation

LIBSEL4_INLINE_FUNC void seL4_BenchmarkDumpAllThreadsUtilisation

Print the current accumulated cycle count for every thread on the current node.

Return value: This method does not return anything.

Description: Uses kernel’s printf to print number of cycles on each line in the following format: thread_name,thread_cycles

Reset All Threads Utilisation

LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetAllThreadsUtilisation

Reset the accumulated cycle count for every thread on the current node.

Return value: This method does not return anything.

Description: Reset the cycle count for each thread to 0.

X86 System Calls

VM Enter

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 privileged 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 intended 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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_FailedLookup	The index or depth is invalid .
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, the capability does not have full rights to the Endpoint .
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The depth is invalid .

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 equivalent to the wordsize.
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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth of the source or destination is invalid . Or, src_root is a CPtr to a capability of the wrong type. Or, the source slot is empty.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, the source capability cannot be derived .
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The dest_depth or src_depth is invalid .
seL4_RevokeFirst	The source capability cannot be derived .

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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_FailedLookup	The index or depth is invalid .
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The depth is invalid .

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 equivalent to the wordsize.
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 equivalent to the wordsize.
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 on 32-bit platforms, the high 4 bits are ignored.

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

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth of the source or destination is invalid . Or, src_root is a CPtr to a capability of the wrong type. Or, the source slot is empty.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, the source capability cannot be derived . Or, the badge or guard value is invalid.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The dest_depth or src_depth is invalid .
seL4_RevokeFirst	The source capability cannot be derived .

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 equivalent to the wordsize.
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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth of the source or destination is invalid . Or, src_root is a CPtr to a capability of the wrong type. Or, the source slot is empty.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The dest_depth or src_depth is invalid .

Mutate

static inline int seL4_CNode_Mutate

Move a capability, setting its guard in the process. This operation is mostly useful for setting the guard of a CNode capability without losing revokability of that CNode capability. All other uses can be replaced by a combination of Mint and Delete.

Type	Name	Description
seL4_CNode	_service	CPtr to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize.
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 equivalent to the wordsize.
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	Guard to be applied to the new capability.

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

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth of the source or destination is invalid . Or, src_root is a CPtr to a capability of the wrong type. Or, the source slot is empty.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, the guard value is invalid.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The dest_depth or src_depth is invalid .

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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_FailedLookup	The index or depth is invalid .
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The depth is invalid .

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 equivalent to the wordsize.
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 equivalent to the wordsize.
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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	If the destination is not the same slot as the source and the destination slot contains a capability.
seL4_FailedLookup	The index or depth of the source, destination, or pivot is invalid . Or, src_root or pivot_root is a CPtr to a capability of the wrong type. Or, the source or pivot slot is empty.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, the pivot is the same slot as the source or destination. Or, the guard value on the destination or pivot is invalid.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The dest_depth, src_depth, or pivot_depth is invalid .

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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth is invalid .
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The depth is invalid .

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The domain is greater than CONFIG_NUM_DOMAINS. Or, thread is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

seL4_IRQControl

Get IRQ Handler

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.
seL4_Word	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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The root, index, or depth is invalid .
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, on x86, an IOAPIC is being used.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The irq is invalid for the target architecture. Or, on x86, irq is not in the ISA IRQ range. Or, depth is invalid .
seL4_RevokeFirst	An IRQ handler capability for irq has already been created.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or notification is a CPtr to a capability of the wrong type. Or, notification does not have the Write right .

seL4_SchedContext (MCS)

Bind

static inline int seL4_SchedContext_Bind

Bind an object to a scheduling context. The object can be a notification object or a thread.

If the object is a thread and the thread is in a runnable state and the scheduling context has available budget, this will start the thread running.

If the object is a notification, when passive threads wait on the notification object and a signal arrives, the passive thread will receive the scheduling context and possess it until it waits on the notification object again.

This operation will fail for notification objects if the scheduling context is already bound to a notification object, and for thread objects if the scheduling context is already bound to a thread.

Type	Name	Description
seL4_SchedContext	_service	Capability to the scheduling context which is being operated on.
seL4_CPtr	cap	Capability to a TCB or a notification object

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service or cap is already bound to the same type of object. Or, cap is a TCB in the blocked state and _service is not schedulable.
seL4_InvalidCapability	The _service or cap is a CPtr to a capability of the wrong type.

Consumed

static inline seL4_SchedContext_Consumed_t seL4_SchedContext_Consumed

Return the amount of time used by this scheduling context since this function was last called or a timeout exception triggered.

Type	Name	Description
seL4_SchedContext	_service	Capability to the scheduling context which is being operated on.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Unbind Object

static inline int seL4_SchedContext_UnbindObject

Unbind an object from a scheduling context. The object can be either a thread or a notification.

If the thread being unbound is the thread that is bound to this scheduling context, this will render the thread passive. However if the thread being unbound received the scheduling context via scheduling context donation over IPC, the scheduling context will be returned to the thread that it was originally bound to.

If the object is a notification and it is bound to the scheduling context, unbind it.

Type	Name	Description
seL4_SchedContext	_service	Capability to the scheduling context which is being operated on.
seL4_CPtr	cap	Capability to a notification that is bound to the scheduling context or capability to a TCB that is bound to this scheduling context or has received it through scheduling context donation.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, cap is not bound to _service. Or, cap is the current thread’s TCB.
seL4_InvalidCapability	The _service or cap is a CPtr to a capability of the wrong type.

Unbind

static inline int seL4_SchedContext_Unbind

Unbind any objects (threads or notification objects) from a scheduling context. This will render the bound thread passive, see Section 6.1.5.

Type	Name	Description
seL4_SchedContext	_service	Capability to the scheduling context which is being operated on.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, the current thread’s TCB is bound to _service.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Yield To

static inline seL4_SchedContext_YieldTo_t seL4_SchedContext_YieldTo

If a thread is currently runnable and running on this scheduling context and the scheduling context has available budget, place it at the head of the scheduling queue. If the caller is at an equal priority to the thread this will result in the thread being scheduled. If the caller is at a higher priority the thread will not run until the threads priority is the highest priority in the system. The caller must have a maximum control priority greater than or equal to the threads priority.

Type	Name	Description
seL4_SchedContext	_service	Capability to the scheduling context which is being operated on.

Return value:

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is not bound to a TCB or is bound to the current thread’s TCB. Or, the target thread’s priority is greater than the current thread’s maximum controlled priority .
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Description: Capability to the scheduling context which is being operated on.

seL4_SchedControl (MCS)

Configure Flags

static inline int seL4_SchedControl_ConfigureFlags

Set the parameters of a scheduling context by invoking the scheduling control capability. If the scheduling context is bound to a currently running thread, the parameters will take effect immediately: that is the current budget will be increased or reduced by the difference between the new and previous budget and the replenishment time will be updated according to any difference in the period. This can result in active threads being post-poned or released depending on the nature of the parameter change and the state of the thread. Additionally, if the scheduling context was previously empty (no budget) but bound to a runnable thread, this can result in a thread running for the first time since it now has access to CPU time. This call will return seL4 Invalid Argument if the parameters are too small (smaller than the kernel WCET for this platform) or too large (will overflow the timer).

Type	Name	Description
seL4_SchedControl	_service	Capability to a scheduling control object.
seL4_SchedContext	schedcontext	Capability to the scheduling context which is being operated on.
seL4_Time	budget	Timeslice in microseconds, when the budget expires the thread will be pre-empted.
seL4_Time	period	Period in microseconds, if equal to budget, this thread will be treated as a round-robin thread. Otherwise, sporadic servers will be used to assure the scheduling context does not exceed the budget over the specified period.
seL4_Word	extra_refills	Number of extra sporadic replenishments this scheduling context should use. Ignored for round-robin threads.
seL4_Word	badge	Identifier for this scheduling context. Delivered to timeout exception handler. Can be used to determine which scheduling context triggered the timeout.
seL4_Word	flags	Bitwise OR’d set of seL4_SchedContextFlag.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or schedcontext is a CPtr to a capability of the wrong type.
seL4_RangeError	The budget or period or extra_refills is too big or too small. Or, budget is greater than period.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service or notification is a CPtr to a capability of the wrong type. Or, _service or notification is already bound. Or, notification does not have Read rights to the Notification .
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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. This value is unused on AARCH64
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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, the argument values are inappropriate for the target architecture.
seL4_InvalidArgument	The argument values are inappropriate for the target architecture.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service, bufferFrame, cspace_root, or vspace_root is a CPtr to a capability of the wrong type. Or, vspace_root is not assigned to an ASID pool. Or, cspace_root_data is invalid. Or, buffer is not aligned. Or, bufferFrame is retyped from a device untyped .
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	The bufferFrame, cspace_root, or vspace_root is a CPtr to a capability of the wrong type.

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 meaning on x86, ARM, and RISC-V.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or source is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The argument values are inappropriate for the target architecture.

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 meaning on x86, ARM, and RISC-V.
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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is the current thread’s TCB.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The count requested too few or too many registers.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_AlignmentError	The vaddr is not aligned to size bytes.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The bp_num, size, or rw is not valid for the given type. Or, argument values are inappropriate for the target architecture. Or, vaddr is in the kernel virtual address range.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The argument values are inappropriate for the target architecture.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, affinity is not a valid CPU number.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_AlignmentError	The buffer is not aligned.
seL4_IllegalOperation	The _service or bufferFrame is a CPtr to a capability of the wrong type. Or, bufferFrame is retyped from a device untyped .
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	The bufferFrame is a CPtr to a capability of the wrong type.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or authority is a CPtr to a capability of the wrong type.
seL4_RangeError	The mcp is greater than the maximum controlled priority of authority.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or authority is a CPtr to a capability of the wrong type.
seL4_RangeError	The priority is greater than the maximum controlled priority of authority.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or authority is a CPtr to a capability of the wrong type.
seL4_RangeError	The mcp is greater than the maximum controlled priority of authority. Or, priority is greater than the maximum controlled priority of authority.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service, cspace_root, or vspace_root is a CPtr to a capability of the wrong type. Or, vspace_root is not assigned to an ASID pool. Or, cspace_root_data is invalid.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	The cspace_root or vspace_root is a CPtr to a capability of the wrong type.

Set TLS Base

static inline int seL4_TCB_SetTLSBase

Set the TLS base of the target TCB.

Type	Name	Description
seL4_TCB	_service	Capability to the TCB which is being operated on.
seL4_Word	tls_base	The TLS base to set.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Description: An invocation for setting the Thread Local Storage (TLS) base address. This ensures that across all platforms, the TLSBase register is viewed as being completely mutable, just like all of the general purpose registers, even on platforms where modification is a privileged operation.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is not bound to a notification.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, the argument values are inappropriate for the target architecture.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The argument values are inappropriate for the target architecture.

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 meaning on x86, ARM, and RISC-V.
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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is the current thread’s TCB.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

seL4_TCB (MCS)

Configure (MCS)

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_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_CPtr	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.

Error Code	Possible Cause
seL4_AlignmentError	The buffer is not aligned.
seL4_IllegalOperation	The _service, bufferFrame, cspace_root, or vspace_root is a CPtr to a capability of the wrong type. Or, vspace_root is not assigned to an ASID pool. Or, cspace_root_data is invalid. Or, bufferFrame is retyped from a device untyped .
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	The bufferFrame, cspace_root, or vspace_root is a CPtr to a capability of the wrong type.

Set Sched Params (MCS)

static inline int seL4_TCB_SetSchedParams

Change a thread’s priority, maximum controlled priority, scheduling context and fault handler.

Type	Name	Description
seL4_TCB	_service	Capability to the TCB which is being operated on.
seL4_TCB	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.
seL4_CPtr	sched_context	Capability to the scheduling context that the TCB should run on. If the scheduling context is already bound to a notification or TCB that is not this TCB this operation will fail. Similarly, if this TCB is already bound to a scheduling context that is not this scheduling context, this will also fail.
seL4_CPtr	fault_ep	CPtr to the endpoint which receives IPCs when this thread faults.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service or sched_context is already bound. Or, _service is the current thread’s TCB. Or, _service is a TCB in the blocked state and sched_context is not schedulable.
seL4_InvalidCapability	The _service, authority, sched_context, or fault_ep is a CPtr to a capability of the wrong type. Or, fault_ep does not have both Write rights and either Grant or GrantReply rights to the Endpoint .
seL4_RangeError	The mcp is greater than the maximum controlled priority of authority. Or, priority is greater than the maximum controlled priority of authority.

Set Space (MCS)

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_CPtr	fault_ep	CPtr to the endpoint which receives IPCs when this thread faults. On MCS this cap gets copied into the TCB.
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_CPtr	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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service, cspace_root, or vspace_root is a CPtr to a capability of the wrong type. Or, vspace_root is not assigned to an ASID pool. Or, cspace_root_data is invalid.
seL4_InvalidCapability	The _service or fault_ep is a CPtr to a capability of the wrong type. Or, fault_ep does not have both Write rights and either Grant or GrantReply rights to the Endpoint .
seL4_RevokeFirst	The cspace_root or vspace_root is a CPtr to a capability of the wrong type.

Set Timeout Endpoint

static inline int seL4_TCB_SetTimeoutEndpoint

Set a thread’s timeout endpoint.

Type	Name	Description
seL4_TCB	_service	Capability to the TCB which is being operated on.
seL4_CPtr	timeout_fault_ep	CPtr to the endpoint which receives IPCs when this thread triggers timeout faults. Can be null.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or timeout_fault_ep is a CPtr to a capability of the wrong type. Or, timeout_fault_ep does not have both Write rights and either Grant or GrantReply rights to the Endpoint .

Description: Timeout exception messages will be delivered to this endpoint if it is not a null capability.

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.

Error Code	Possible Cause
seL4_DeleteFirst	A capability exists in the destination window of the CNode.
seL4_FailedLookup	The root, node_index, or node_depth is invalid .
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The size_bits is too big or too small for the requested object type. Or, type cannot be created from a device untyped . Or, the requested object type does not exist.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_NotEnoughMemory	The total size of the new objects exceeds the space available.
seL4_RangeError	The num_objects do not fit in the destination CNode at node_offset. Or, num_objects is greater than CONFIG_RETYPE_FAN_OUT_LIMIT. Or, size_bits is too large.

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 Handler

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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, an IOAPIC is not in use.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The vector, ioapic, or pin is invalid. Or, level or polarity is not 0 or 1. Or, depth is invalid .
seL4_RevokeFirst	An IRQ handler capability for vector has already been created.

Get MSI Handler

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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, an IOAPIC is not in use.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The vector, pic_bus, pci_dev, or pci_func is invalid. Or, the depth is invalid .
seL4_RevokeFirst	An IRQ handler capability for vector has already been created.

seL4_TCB

Set EPT Root

static inline int seL4_TCB_SetEPTRoot

Set the EPT root of a thread

Type	Name	Description
seL4_TCB	_service	Capability to the TCB which is being operated on.
seL4_X86_EPTPML4	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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service or eptpml4 is a CPtr to a capability of the wrong type. Or, eptpml4 is not assigned to an ASID pool.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability. Or, there are no more ASID pools available.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or untyped is a CPtr to a capability of the wrong type. Or, untyped is not the exact size of an ASID pool object. Or, untyped is a device untyped .
seL4_RangeError	The depth is invalid .
seL4_RevokeFirst	The untyped has been used to retype an object. Or, a copy of the untyped capability exists.

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.

Error Code	Possible Cause
seL4_DeleteFirst	There are no more ASIDs available in _service.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is already assigned to an ASID pool.

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

Error Code	Possible Cause
seL4_DeleteFirst	A mapping already exists for this level in eptpml4 at gpa.
seL4_FailedLookup	The eptpml4 is not assigned to an ASID pool. Or, eptpml4 does not have an EPTPDPT mapped at gpa.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or eptpml4 is a CPtr to a capability of the wrong type. Or, _service is already mapped in a VSpace. Or, eptpml4 is not assigned to an ASID pool.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	A copy of the _service capability exists.

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

Error Code	Possible Cause
seL4_DeleteFirst	A mapping already exists for this level in eptpml4 at gpa.
seL4_FailedLookup	The eptpml4 is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or eptpml4 is a CPtr to a capability of the wrong type. Or, _service is already mapped in a VSpace. Or, eptpml4 is not assigned to an ASID pool.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	A copy of the _service capability exists.

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

Error Code	Possible Cause
seL4_DeleteFirst	A mapping already exists for this level in eptpml4 at gpa.
seL4_FailedLookup	The eptpml4 is not assigned to an ASID pool. Or, eptpml4 does not have an EPTPD mapped at gpa.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or eptpml4 is a CPtr to a capability of the wrong type. Or, _service is already mapped in a VSpace. Or, eptpml4 is not assigned to an ASID pool.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	A copy of the _service capability exists.

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.

Error Code	Possible Cause
seL4_DeleteFirst	All required page tables are already mapped in iospace at ioaddr.
seL4_FailedLookup	The iospace does not have a paging structure at the required level mapped at ioaddr.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or iospace is a CPtr to a capability of the wrong type. Or, iospace is not assigned to a PCI device. Or, _service is already mapped in an IOSpace.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, reading from port and port+1 is not authorized by the capability.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, reading from ports port through port+3 is not authorized by the capability.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, reading from port is not authorized by the capability.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, writing to port and port+1 is not authorized by the capability.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, writing to ports port through port+3 is not authorized by the capability.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, writing to port is not authorized by the capability.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The last_port is less than first_port.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The depth is invalid .
seL4_RevokeFirst	One or more ports in the requested range have already been issued.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Map EPT

static inline int seL4_X86_Page_MapEPT

Map an extended page table.

Type	Name	Description
seL4_X86_Page	_service	Capability to the page being operated on.
seL4_X86_EPTPML4	vspace	Capability to the VSpace which will contain the mapping
seL4_Word	vaddr	Virtual address at which to map page.
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.

Error Code	Possible Cause
seL4_AlignmentError	The vaddr is not aligned to the page size of _service.
seL4_DeleteFirst	A mapping already exists in vspace at vaddr.
seL4_FailedLookup	The vspace does not have a paging structure at the required level mapped at vaddr. Or, vspace is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is not assigned to an ASID pool. Or, _service is already mapped. Or, _service has an unsupported page size.

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.

Error Code	Possible Cause
seL4_DeleteFirst	A mapping already exists in iospace at ioaddr.
seL4_FailedLookup	The iospace does not have a sufficient number of IO Page Tables mapped at ioaddr.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	No rights were specified in rights. Or, the rights in the _service capability do not include rights.
seL4_InvalidCapability	The _service or iospace is a CPtr to a capability of the wrong type. Or, _service is already mapped. Or, _service is not a page of size 4 KiB. Or, iospace is not assigned to a PCI device.

Map

static inline int seL4_X86_Page_Map

Map a page into an address space or update the mapping attributes.

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.

Error Code	Possible Cause
seL4_AlignmentError	The vaddr is not aligned to the page size of _service.
seL4_DeleteFirst	A mapping already exists in vspace at vaddr.
seL4_FailedLookup	The vspace does not have a paging structure at the required level mapped at vaddr. Or, vspace is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is already mapped in an IOSpace.
seL4_InvalidArgument	The _service is already mapped in vspace at a different virtual address. Or, vaddr is in the kernel virtual address range.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is not assigned to an ASID pool. Or, _service is already mapped in a different VSpace.

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, or updates the mapping attributes if the page is already mapped at this address. If the required paging structures are not present this operation will fail, returning a seL4_FailedLookup error.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The _service does not have a mapping at vaddr. Or, vaddr is in the kernel virtual address range.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_DeleteFirst	A mapping already exists for this level in vspace at vaddr.
seL4_FailedLookup	The vspace does not have a PDPT mapped at vaddr. Or, vspace is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The vaddr is in the kernel virtual address range.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is not assigned to an ASID pool. Or, _service is already mapped in a VSpace.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	A copy of the _service capability exists.

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.

Error Code	Possible Cause
seL4_DeleteFirst	A mapping already exists for this level in vspace at vaddr.
seL4_FailedLookup	The vspace does not have a Page Directory mapped at vaddr. Or, vspace is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The vaddr is in the kernel virtual address range.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is not assigned to an ASID pool. Or, _service is already mapped in a VSpace.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	A copy of the _service capability exists.

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

seL4_X86_VCPU

Disable I/O 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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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

Enable I/O 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_X86_IOPort	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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service or ioPort is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The low or high IO port exceeds the range authorized by ioPort.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, field is invalid or unsupported.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service or tcb is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, field is invalid or unsupported.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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

Map a page directory page table.

Type	Name	Description
seL4_X86_PDPT	_service	Capability to the PDPT being operated on.
seL4_X64_PML4	pml4	Capability to the VSpace which will contain the mapping.
seL4_Word	vaddr	Virtual address at which to map page.
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.

Error Code	Possible Cause
seL4_DeleteFirst	A mapping already exists for this level in vspace at vaddr.
seL4_FailedLookup	The pml4 is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The vaddr is in the kernel virtual address range.
seL4_InvalidCapability	The _service or pml4 is a CPtr to a capability of the wrong type. Or, pml4 is not assigned to an ASID pool. Or, _service is already mapped in a VSpace.

Unmap

static inline int seL4_X86_PDPT_Unmap

Unmap a page directory page table.

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

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	A copy of the _service capability exists.

seL4_X86_VCPU

Read MSR

static inline seL4_X86_VCPU_ReadMSR_t seL4_X86_VCPU_ReadMSR

Read 64-bit specific MSR field from the hardware

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

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

Description: Thin wrapper around the rdmsr instruction that is performed on specific, needed registers. Certain registers might simply be cached and restored later.

Write MSR

static inline seL4_X86_VCPU_WriteMSR_t seL4_X86_VCPU_WriteMSR

Write 64-bit specific MSR field to the hardware

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

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

Description: Thin wrapper around the wrmsr instruction that is performed on specific, needed registers. 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.

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 equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability. Or, there are no more ASID pools available.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or untyped is a CPtr to a capability of the wrong type. Or, untyped is not the exact size of an ASID pool object. Or, untyped is a device untyped .
seL4_RangeError	The depth is invalid .
seL4_RevokeFirst	The untyped has been used to retype an object. Or, a copy of the untyped capability exists.

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.

Error Code	Possible Cause
seL4_DeleteFirst	There are no more ASIDs available in _service.
seL4_FailedLookup	The ASID pool of _service is no longer assigned.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is already assigned to an ASID pool.

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

seL4_ARM_CB

Assign VSpace

static inline int seL4_ARM_CB_AssignVspace

Assigning a VSpace to a context bank.

Type	Name	Description
seL4_ARM_CB	_service	A CB capability. This gives you the authority to make this call.
seL4_CPtr	vspace	The VSpace that is being assigned to a context bank. Must already has an assigned ASID.

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

Error Code	Possible Cause
seL4_DeleteFirst	The _service is already assigned to a VSpace.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is not assigned to an ASID pool.

CB Clear Fault

static inline int seL4_ARM_CB_CBClearFault

Clear the fault status of the context bank.

Type	Name	Description
seL4_ARM_CB	_service	A CB capability. This gives you the authority to make this call.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

CB Get Fault

static inline seL4_ARM_CB_CBGetFault_t seL4_ARM_CB_CBGetFault

Get the fault status of the context bank.

Type	Name	Description
seL4_ARM_CB	_service	A CB capability. This gives you the authority to make this call.

Return value: A seL4_ARM_SMMU_CB_GetFault_t struct that contains a seL4_Word status, which holds the fault status of the context bank, seL4_Word address, which holds the faulty address, and int error.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

TLB Invalidate

static inline int seL4_ARM_CB_TLBInvalidate

Invalidating TLB entries used by the current ASID in this context bank.

Type	Name	Description
seL4_ARM_CB	_service	A CB capability. This gives you the authority to make this call.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is not assigned to a VSpace.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Unassign VSpace

static inline int seL4_ARM_CB_UnassignVspace

Unassigning a VSpace to a context bank.

Type	Name	Description
seL4_ARM_CB	_service	A CB capability. This gives you the authority to make this call.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is not assigned to a VSpace.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

seL4_ARM_CBControl

Get CB

static inline int seL4_ARM_CBControl_GetCB

Create a CB capability.

Type	Name	Description
seL4_ARM_CBControl	_service	A CBControl capability. This gives you the authority to make this call.
seL4_Word	cb	The CB that you want this capability to manage.
seL4_CNode	root	CPtr to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The depth is invalid . Or, cb is invalid.
seL4_RevokeFirst	A CB capability for cb has already been created.

TLB Invalidate All

static inline int seL4_ARM_CBControl_TLBInvalidateAll

Invalidate all TLB entries.

Type	Name	Description
seL4_ARM_CBControl	_service	A CBControl capability. This gives you the authority to make this call.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

seL4_ARM_IOPageTable

Map

static inline int seL4_ARM_IOPageTable_Map

Map an IO page table into an IOSpace.

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

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

Error Code	Possible Cause
seL4_DeleteFirst	All required page tables are already mapped in iospace at ioaddr.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or iospace is a CPtr to a capability of the wrong type. Or, _service is already mapped in an IOSpace.

Unmap

static inline int seL4_ARM_IOPageTable_Unmap

Unmap an IO page table from an IOSpace.

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

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_FailedLookup	The VSpace of _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is not mapped in a VSpace. Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
seL4_InvalidArgument	The start_offset is greater than or equal to end_offset. Or, start_offset or end_offset exceeds the page size of _service.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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

Error Code	Possible Cause
seL4_FailedLookup	The VSpace of _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is not mapped in a VSpace. Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
seL4_InvalidArgument	The start_offset is greater than or equal to end_offset. Or, start_offset or end_offset exceeds the page size of _service.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Invalidate Data

static inline int seL4_ARM_Page_Invalidate_Data

Invalidates the cache range within the given page. The start and end offsets 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.

Error Code	Possible Cause
seL4_FailedLookup	The VSpace of _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is not mapped in a VSpace. Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
seL4_InvalidArgument	The start_offset is greater than or equal to end_offset. Or, start_offset or end_offset exceeds the page size of _service.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Map I/O

static inline int seL4_ARM_Page_MapIO

Map a page into an IOSpace.

Type	Name	Description
seL4_ARM_Page	_service	Capability to the page being operated on.
seL4_ARM_IOSpace	iospace	The IOSpace to map the page into.
seL4_CapRights_t	rights	Rights for the mapping.
seL4_Word	ioaddr	Virtual address at which to map page.

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

Error Code	Possible Cause
seL4_DeleteFirst	A mapping already exists in iospace at ioaddr.
seL4_FailedLookup	The iospace does not have a sufficient number of IO Page Tables mapped at ioaddr.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	No rights were specified in rights. Or, the rights in the _service capability do not include rights.
seL4_InvalidCapability	The _service or iospace is a CPtr to a capability of the wrong type. Or, _service is already mapped. Or, _service is not a page of size 4 KiB.

Map

static inline int seL4_ARM_Page_Map

Map a page into an address space or update the mapping attributes.

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. Must be assigned to an ASID pool.
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.

Error Code	Possible Cause
seL4_AlignmentError	The vaddr is not aligned to the page size of _service.
seL4_DeleteFirst	A mapping already exists in vspace at vaddr.
seL4_FailedLookup	The vspace does not have a paging structure at the required level mapped at vaddr. Or, vspace is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The _service is already mapped in vspace at a different virtual address. Or, vaddr is in the kernel virtual address range.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is not assigned to an ASID pool. Or, _service is already mapped in a different VSpace.

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, or updates the mapping attributes if the page is already mapped at this address. The page must not already be mapped through this capability in a different VSpace or at a different address; the page may be mapped in multiple VSpaces by copying the capability.

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

Error Code	Possible Cause
seL4_FailedLookup	The VSpace of _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is not mapped in a VSpace. Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
seL4_InvalidArgument	The start_offset is greater than or equal to end_offset. Or, start_offset or end_offset exceeds the page size of _service.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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. Must be assigned to an ASID pool.
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.

Error Code	Possible Cause
seL4_DeleteFirst	A mapping already exists for this level in vspace at vaddr.
seL4_FailedLookup	On aarch64, vspace does not have a Page Directory mapped at vaddr. Or, vspace is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The vaddr is in the kernel virtual address range.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is not assigned to an ASID pool. Or, _service is already mapped in a VSpace.

Description: Takes a VSpace capability as an argument, and installs a reference to the page table in the VSpace at 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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	A copy of the _service capability exists.

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

seL4_ARM_SID

Bind CB

static inline int seL4_ARM_SID_BindCB

Binding a context bank to a stream ID.

Type	Name	Description
seL4_ARM_SID	_service	A SID capability. This gives you the authority to make this call.
seL4_CPtr	cb	The CB that is being binded to a stream ID. Must already has an assigned vspace.

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

Error Code	Possible Cause
seL4_DeleteFirst	The _service is already bound to a context bank.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or cb is a CPtr to a capability of the wrong type. Or, cb is not assigned to a VSpace.

Unbind CB

static inline int seL4_ARM_SID_UnbindCB

Unbinding a context bank from a stream ID.

Type	Name	Description
seL4_ARM_SID	_service	A SID capability. This gives you the authority to make this call.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, _service is not bound to a context block.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

seL4_ARM_SIDControl

Clear Fault

static inline int seL4_ARM_SIDControl_ClearFault

Clear the fault status of the SMMU.

Type	Name	Description
seL4_ARM_SIDControl	_service	A SIDControl capability. This gives you the authority to make this call.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Get Fault

static inline seL4_ARM_SIDControl_GetFault_t seL4_ARM_SIDControl_GetFault

Get the fault status of the SMMU.

Type	Name	Description
seL4_ARM_SIDControl	_service	A SIDControl capability. This gives you the authority to make this call.

Return value: A seL4_ARM_SMMU_GetFault_t struct that contains a seL4_Word status, which holds the global fault status of the SMMU, seL4_Word syndrome_0, which holds the global fault syndrome 0 of the SMMU, seL4_Word syndrome_1, which holds the global fault syndrome 1 of the SMMU, and int error.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Get SID

static inline int seL4_ARM_SIDControl_GetSID

Create a SID capability.

Type	Name	Description
seL4_ARM_SIDControl	_service	A SIDControl capability. This gives you the authority to make this call.
seL4_Word	sid	The SID that you want this capability to manage.
seL4_CNode	root	CPtr to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The depth is invalid . Or, sid is invalid.
seL4_RevokeFirst	An SID capability for sid has already been created.

seL4_ARM_VCPU

Acknowledge Virtual PPI IRQ

static inline int seL4_ARM_VCPU_AckVPPI

Acknowledge a PPI IRQ previously forwarded from a VPPIEvent fault.

Type	Name	Description
seL4_ARM_VCPU	_service	Capability to the VCPU being operated on.
seL4_Word	irq	irq to ack.

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

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The irq is invalid.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Description: Acknowledge and unmask the PPI interrupt so that further interrupts can be forwarded through VPPIEvent faults.

Inject IRQ

static inline int seL4_ARM_VCPU_InjectIRQ

Inject an IRQ to a virtual CPU.

Type	Name	Description
seL4_ARM_VCPU	_service	Capability to the VCPU being operated on.
seL4_Uint16	virq	Virtual IRQ ID
seL4_Uint8	priority	Priority of the IRQ to be injected
seL4_Uint8	group	IRQ group
seL4_Uint8	index	VGIC list register

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

Error Code	Possible Cause
seL4_DeleteFirst	The index is in use and not yet handled by the guest.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The virq, priority, group, or index is invalid.

Description: Used to queue IRQs towards the VCPU. Writes ICH_LRn_EL2 for GICv3 or LRn for GICv2, where n is determined by index. The list register becomes available again when the guest acknowledges the injected interrupt.

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	Capability to the VCPU being operated on.
seL4_VCPUReg	field	Register to read from a VCPU

Return value: A seL4_ARM_VCPU_ReadRegs_t struct that contains a seL4_Word value, which holds the value of the system register, and int error, which will be non-zero when an error occurred.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The field is invalid.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Description: Provides a way to read EL1 system registers, as well as VMPIDR_EL2.

Set TCB

static inline int seL4_ARM_VCPU_SetTCB

Bind a TCB to a virtual CPU.

Type	Name	Description
seL4_ARM_VCPU	_service	Capability to the VCPU being operated on.
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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service or tcb is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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	Capability to the VCPU being operated on.
seL4_VCPUReg	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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The field is invalid.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

Description: Provides a way to write EL1 system registers, as well as VMPIDR_EL2.

seL4_IRQControl

Get IRQ Handler (SMP)

static inline int seL4_IRQControl_GetTriggerCore

Create an IRQ handler capability and specify the trigger method (edge or level) and the target core.

Type	Name	Description
seL4_IRQControl	_service	An IRQControl capability. This gives you the authority to make this call.
seL4_Word	irq	The IRQ that you want this capability to handle.
seL4_Word	trigger	Indicates whether this IRQ is edge (1) or level (0) triggered.
seL4_CNode	root	CPtr to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize.
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	target	Indicates the target core ID to which this IRQ will be sent.

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

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, SMP support is not enabled.
seL4_InvalidArgument	The target is invalid.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The depth is invalid .
seL4_RevokeFirst	An IRQ handler capability for irq has already been created.

Get IRQ Handler with Trigger Type

static inline int seL4_IRQControl_GetTrigger

Create an IRQ handler capability and specify the trigger method (edge or level).

Type	Name	Description
seL4_IRQControl	_service	An IRQControl capability. This gives you the authority to make this call.
seL4_Word	irq	The IRQ that you want this capability to handle.
seL4_Word	trigger	Indicates whether this IRQ is edge (1) or level (0) triggered.
seL4_CNode	root	CPtr to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, the platform does not support setting the IRQ trigger.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The irq is invalid. Or, depth is invalid .
seL4_RevokeFirst	An IRQ handler capability for irq has already been created.

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	Capability to the page directory being operated on.
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.

Error Code	Possible Cause
seL4_FailedLookup	The _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, start or end is in the kernel virtual address range.
seL4_InvalidArgument	The start is greater than or equal to end.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type. Or, _service is not assigned to an ASID pool.
seL4_RangeError	The specified range crosses a page boundary.

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	Capability to the page directory being operated on.
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.

Error Code	Possible Cause
seL4_FailedLookup	The _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, start or end is in the kernel virtual address range.
seL4_InvalidArgument	The start is greater than or equal to end.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type. Or, _service is not assigned to an ASID pool.
seL4_RangeError	The specified range crosses a page boundary.

Invalidate Data

static inline int seL4_ARM_PageDirectory_Invalidate_Data

Invalidate cached pages within a page directory

Type	Name	Description
seL4_ARM_PageDirectory	_service	Capability to the page directory being operated on.
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.

Error Code	Possible Cause
seL4_FailedLookup	The _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, start or end is in the kernel virtual address range.
seL4_InvalidArgument	The start is greater than or equal to end.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type. Or, _service is not assigned to an ASID pool.
seL4_RangeError	The specified range crosses a page boundary.

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	Capability to the page directory being operated on.
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.

Error Code	Possible Cause
seL4_FailedLookup	The _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, start or end is in the kernel virtual address range.
seL4_InvalidArgument	The start is greater than or equal to end.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type. Or, _service is not assigned to an ASID pool.
seL4_RangeError	The specified range crosses a page boundary.

Aarch64-Specific Object Methods

seL4_ARM_SMC

SMC Call

static inline int seL4_ARM_SMC_Call

Tell the kernel to make the real SMC call.

Type	Name	Description
seL4_ARM_SMC	_service	Capability to allow threads to make Secure Monitor Calls.
seL4_ARM_SMCContext *	smc_args	The structure that has the provided arguments.
seL4_ARM_SMCContext *	smc_response	The structure to capture the responses.

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

Description: Takes x0-x7 as arguments to an SMC call which are defined as a seL4_ARM_SMCContext struct. The kernel makes the SMC call and then returns the results as a new seL4_ARM_SMCContext.

seL4_ARM_VSpace

Clean Data

static inline int seL4_ARM_VSpace_Clean_Data

Clean cached pages within a top level translation table

Type	Name	Description
seL4_ARM_VSpace	_service	Capability to the top level translation table being operated on.
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.

Error Code	Possible Cause
seL4_FailedLookup	The _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, end is in the kernel virtual address range.
seL4_InvalidArgument	The start is greater than or equal to end.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type. Or, _service is not assigned to an ASID pool.
seL4_RangeError	The specified range crosses a page boundary.

Clean and Invalidate Data

static inline int seL4_ARM_VSpace_CleanInvalidate_Data

Clean and invalidate cached pages within a top level translation table

Type	Name	Description
seL4_ARM_VSpace	_service	Capability to the top level translation table being operated on.
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.

Error Code	Possible Cause
seL4_FailedLookup	The _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, end is in the kernel virtual address range.
seL4_InvalidArgument	The start is greater than or equal to end.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type. Or, _service is not assigned to an ASID pool.
seL4_RangeError	The specified range crosses a page boundary.

Invalidate Data

static inline int seL4_ARM_VSpace_Invalidate_Data

Invalidate cached pages within a top level translation table

Type	Name	Description
seL4_ARM_VSpace	_service	Capability to the top level translation table being operated on.
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.

Error Code	Possible Cause
seL4_FailedLookup	The _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, end is in the kernel virtual address range.
seL4_InvalidArgument	The start is greater than or equal to end.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type. Or, _service is not assigned to an ASID pool.
seL4_RangeError	The specified range crosses a page boundary.

Unify Instruction

static inline int seL4_ARM_VSpace_Unify_Instruction

Clean and invalidate cached instruction pages to point of unification

Type	Name	Description
seL4_ARM_VSpace	_service	Capability to the top level translation table being operated on.
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.

Error Code	Possible Cause
seL4_FailedLookup	The _service is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, end is in the kernel virtual address range.
seL4_InvalidArgument	The start is greater than or equal to end.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type. Or, _service is not assigned to an ASID pool.
seL4_RangeError	The specified range crosses a page boundary.

RISCV-Specific Object Methods

---

seL4_IRQControl

Get IRQ Handler with Trigger Type

static inline int seL4_IRQControl_GetTrigger

Create an IRQ handler capability and specify the trigger method (edge or level).

Type	Name	Description
seL4_IRQControl	_service	An IRQControl capability. This gives you the authority to make this call.
seL4_Word	irq	The IRQ that you want this capability to handle.
seL4_Word	trigger	Indicates whether this IRQ is edge (1) or level (0) triggered.
seL4_CNode	root	CPtr to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize.
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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type. Or, the platform does not support setting the IRQ trigger.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RangeError	The irq is invalid. Or, depth is invalid .
seL4_RevokeFirst	An IRQ handler capability for irq has already been created.

seL4_RISCV_ASIDControl

Make Pool

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.

Error Code	Possible Cause
seL4_DeleteFirst	The destination slot contains a capability. Or, there are no more ASID pools available.
seL4_FailedLookup	The index or depth is invalid . Or, root is a CPtr to a capability of the wrong type.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or untyped is a CPtr to a capability of the wrong type. Or, untyped is not the exact size of an ASID pool object. Or, untyped is a device untyped .
seL4_RangeError	The depth is invalid .
seL4_RevokeFirst	The untyped has been used to retype an object. Or, a copy of the untyped capability exists.

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.

Error Code	Possible Cause
seL4_DeleteFirst	There are no more ASIDs available in _service.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is already assigned to an ASID pool. Or, vspace is mapped in a VSpace.

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

seL4_RISCV_Page

Get Address

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_AlignmentError	The vaddr is not aligned to the page size of _service.
seL4_DeleteFirst	A mapping already exists in vspace at vaddr.
seL4_FailedLookup	The vspace does not have a paging structure at the required level mapped at vaddr. Or, vspace is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The _service is already mapped in vspace at a different virtual address. Or, vaddr is in the kernel virtual address range.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is not the root of a VSpace. Or, vspace is not assigned to an ASID pool. Or, _service is already mapped in a different VSpace.

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 a page is already mapped at the same virtual address, update the mapping attributes. If the required paging structures are not present this operation will fail, returning a seL4_FailedLookup error.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.

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.

Error Code	Possible Cause
seL4_DeleteFirst	A page is mapped in vspace at vaddr. Or, all required page tables are already mapped in vspace at vaddr.
seL4_FailedLookup	The vspace is not assigned to an ASID pool.
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidArgument	The vaddr is in the kernel virtual address range.
seL4_InvalidCapability	The _service or vspace is a CPtr to a capability of the wrong type. Or, vspace is not assigned to an ASID pool. Or, _service is already mapped in a VSpace.

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.

Error Code	Possible Cause
seL4_IllegalOperation	The _service is a CPtr to a capability of the wrong type.
seL4_InvalidCapability	The _service is a CPtr to a capability of the wrong type.
seL4_RevokeFirst	The _service is the root of a VSpace. Or, a copy of the _service capability exists.