Crate sel4

Help

Expand description

This crate provides straightforward, pure-Rust bindings to the seL4 API.

Most items in this crate correspond to types, constants, and functions in libsel4. See the seL4 manual for more information about the seL4 concepts and libsel4 items references in this crate’s documentation.

This crate’s implementation is based on the lower-level sel4-sys crate, which is generated from the libsel4 headers and interface definition files.

§Features

§`"state"`

Functions in the C libsel4 use the thread-local variable __sel4_ipc_buffer to obtain a pointer to the current thread’s IPC buffer:

extern __thread seL4_IPCBuffer *__sel4_ipc_buffer;

libmicrokit, which does not support thread-local storage uses the following snippet to force __sel4_ipc_buffer to global rather than thread-local:

#define __thread
#include <sel4/sel4.h>

For the sake of flexibility and applicability, this crate can be configured to use no state at all. Users can opt out of state and explicitly pass around references to the active IPC buffer instead of relying on the implementation to obtain such a reference using thread-local or global state. Such a paradigm is useful in certain uncommon circumstances, but most users will benefit from the convenience of an implicit IPC buffer. The "state" feature, enabled by default, uses state to allow one to make seL4 API calls without having to explicitly specify an IPC buffer.

For the sake of interoperability with C, the state looks something like: static mut __sel4_ipc_buffer: *mut IpcBuffer. If the "state-exposed" feature is enabled, it is exposed with #![no_mangle]. If the "state-extern" feature is enabled, it is wrapped in an extern "C" block. Whether it is thread-local is determined by the following pseudocode:

cfg_if! {
    if #[cfg(all(any(target_thread_local, feature = "tls"), not(feature = "non-thread-local-state")))] {
        // thread-local
    } else if #[cfg(not(feature = "thread-local-state"))] {
        // not thread-local
    } else {
        compile_error!(r#"invalid configuration"#);
    }
}

The non-thread-local configuration should only be used in cases where the language runtime does not support thread-local storage. In those cases without thread-local storage where this crate will only ever run in a single thread, use the "single-threaded" feature to enable a more efficient implementation. Note that enabling the "single-threaded" feature in a case where this crate runs in more than one thread is unsafe.

At the API level, the "state" feature causes NoExplicitInvocationContext to be an alias for ImplicitInvocationContext, which implements InvocationContext by accessing the thread-local pointer to an IPC buffer. When the "state" feature is not enabled, NoExplicitInvocationContext is an alias for NoInvocationContext, which does not implement InvocationContext. The thread-local IPC buffer pointer is modified and accessed by set_ipc_buffer, with_ipc_buffer, and with_ipc_buffer_mut. The lower-level try_with_ipc_buffer_slot and try_with_ipc_buffer_slot_mut are provided as well.

§Building

This crate and its dependencies depend, at build time, on the libsel4 headers. The location of these headers is provided to this crate at build time by environment variables. If SEL4_INCLUDE_DIRS is set, then its value is interpreted as a colon-separated list of include paths for the libsel4 headers. Otherwise, if SEL4_PREFIX is set, then $SEL4_PREFIX/libsel4/include is used.

Re-exports§

pub use sel4_config as config;
pub use sel4_sys as sys;

Modules§

cap: Marked aliases of Cap.
cap_type: Markers corresponding to capability types and classes of capability types.
init_thread: Items that are applicable within the context of the root task’s initial thread’s CSpace.
vspace_levels: Items describing the layout of address translation structures for this kernel configuration.

Macros§

debug_print: Like std::debug_print!, except backed by seL4_DebugPutChar.
debug_println: Like std::debug_println!, except backed by seL4_DebugPutChar.
sel4_cfg_bool: Like core::cfg!, except using the seL4 kernel configuration.
sel4_cfg_if: Like cfg_if::cfg_if!, except with sel4_cfg instead of #[cfg].
sel4_cfg_str: Like core::cfg!, except using the seL4 kernel configuration.
sel4_cfg_usize: Like core::cfg!, except using the seL4 kernel configuration.
sel4_cfg_word: Like core::cfg!, except using the seL4 kernel configuration.
sel4_cfg_wrap_match: Like sel4_cfg_match, except it works on stable, at the expense of not being an attribute macro.

Structs§

AbsoluteCPtr: A CPtrWithDepth to be resolved in the context of a particular CNode.
BootInfo: Corresponds to seL4_BootInfo.
BootInfoExtra: An extra bootinfo chunk along with its ID.
BootInfoExtraIter: An iterator for accessing the BootInfoExtra entires associated with a BootInfoPtr.
BootInfoPtr: A wrapped pointer to a BootInfo block.
CNodeCapData: Corresponds to seL4_CNode_CapData.
CPtr: A capability pointer.
CPtrWithDepth: A capability pointer with a number of bits to resolve.
CallWithMRs: The result of cap::Endpoint::call_with_mrs.
Cap: A capability pointer to be resolved in the current CSpace.
CapFault: Corresponds to seL4_Fault_CapFault.
CapRights: Corresponds to seL4_CapRights_t.
CapRightsBuilder: Helper for constructing CapRights.
DebugWrite: Implements core::fmt::Write using debug_put_char.
ImplicitInvocationContext: The strategy for discovering the current thread’s IPC buffer which uses thread-local state.
ImplicitReplyAuthority: Under this configuration, no reply authority is required.
IpcBuffer: Corresponds to seL4_IPCBuffer.
MessageInfo: Corresponds to seL4_MessageInfo_t.
MessageInfoBuilder: Helper for constructing MessageInfo.
NoInvocationContext: The absence of a strategy for discovering the current thread’s IPC buffer.
NullFault: Corresponds to seL4_Fault_NullFault.
RecvWithMRs: The result of cap::Endpoint::recv_with_mrs.
UnknownSyscall: Corresponds to seL4_Fault_UnknownSyscall.
UntypedDesc: Corresponds to seL4_UntypedDesc.
UserContext: Corresponds to seL4_UserContext.
UserException: Corresponds to seL4_Fault_UserException.
VmAttributes: Corresponds to seL4_ARM_VMAttributes.
VmFault: Corresponds to seL4_Fault_VMFault.

Enums§

BootInfoExtraId: Corresponds to seL4_BootInfoID.
Error: Corresponds to seL4_Error.
Fault: Corresponds to seL4_Fault.
FrameObjectType: Frame object types for this kernel configuration.
ObjectBlueprint: An object description for Untyped::untyped_retype.
ObjectBlueprintAArch32: AArch32-specific variants of ObjectBlueprint.
ObjectBlueprintArm: Arm-specific variants of ObjectBlueprint.
ObjectType: Corresponds to seL4_ObjectType.
ObjectTypeAArch32: Corresponds to seL4_ModeObjectType.
ObjectTypeArm: Corresponds to seL4_ArchObjectType.
TranslationTableObjectType: Translation table object types for this kernel configuration.

Constants§

NUM_FAST_MESSAGE_REGISTERS: The number of message registers which are passed in architectural registers.
NUM_MESSAGE_REGISTERS: Number of message registers in the IPC buffer.
WORD_SIZE: The size of Word in bits.

Traits§

CapType: Trait for marker types corresponding to capability types in the seL4 API.
CapTypeForFrameObject: Trait for CapTypes which correspond to frame objects.
CapTypeForFrameObjectOfFixedSize: Trait for CapTypes which correspond to frame objects of fixed size.
CapTypeForObject: Trait for CapTypes which correspond to kernel objects.
CapTypeForObjectOfFixedSize: Trait for CapTypes which correspond to kernel objects of fixed size.
CapTypeForObjectOfVariableSize: Trait for CapTypes which correspond to kernel objects of variable size.
CapTypeForTranslationTableObject: Trait for CapTypes which correspond to translation table objects.
ConveysReplyAuthority: Trait for types from which ReplyAuthority can be derived.
FastMessages: Trait for types which can hold the contents of a set of inline message registers.
HasCPtrWithDepth: Trait for types whose members which logically contain a CPtrWithDepth.
InvocationContext: A strategy for discovering the current thread’s IPC buffer.
IpcCapType: Trait for CapTypes which are used as targets of IPC syscalls.

Functions§

debug_put_char: Corresponds to seL4_DebugPutChar.
debug_snapshot: Corresponds to seL4_DebugSnapshot.
ipc_buffer_is_thread_local: Returns whether this crate’s IPC buffer slot is thread-local.
reply: Corresponds to seL4_Reply.
set_ipc_buffer: Sets the IPC buffer that this crate will use for this thread.
try_with_ipc_buffer_slot: Provides low-level access to this thread’s IPC buffer.
try_with_ipc_buffer_slot_mut: Provides low-level mutable access to this thread’s IPC buffer.
with_ipc_buffer: Provides access to this thread’s IPC buffer.
with_ipc_buffer_mut: Provides mutable access to this thread’s IPC buffer.
yield: Corresponds to seL4_Yield.

Type Aliases§

Badge: A capability badge.
CPtrBits: The raw bits of a capability pointer.
NoExplicitInvocationContext: The default strategy for discovering the current thread’s IPC buffer.
ObjectBlueprintArch: Alias for ObjectBlueprintArm.
ObjectBlueprintSeL4Arch: Alias for ObjectBlueprintAArch32.
ObjectTypeArch: Alias for ObjectTypeArm.
ObjectTypeSeL4Arch: Alias for ObjectTypeAArch32.
ReplyAuthority: Configuration-dependant alias for conveying reply authority to syscalls.
Result: Alias for Result<_, Error>.
Word: Corresponds to seL4_Word.

Attribute Macros§

sel4_cfg: Make the attached code conditional on a seL4 kernel configuration expression.
sel4_cfg_attr: Make the associated attribute expression conditional on a seL4 kernel configuration expression.
sel4_cfg_enum: Allows an enum’s variants to use the sel4_cfg attribute.
sel4_cfg_match: Allows a match expression’s variants to use the sel4_cfg attribute.
sel4_cfg_struct: Allows a struct’s fields to use the sel4_cfg attribute.

Crate sel4Copy item path