Crate sel4

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

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§

Structs§

Enums§

Constants§

Traits§

Functions§

Type Aliases§

Attribute Macros§