Improve docs

README.md

@@ -22,7 +22,7 @@ This repository contains crates for supporting the use of Rust in
 The [./hacking](./hacking) directory contains scripts for developing and testing these crates using
 Nix and, optionally, Docker.
 
-This work is funded by the [seL4 Foundation](https://sel4.systems/Foundation/home.pml).
+This work is funded by the [seL4 Foundation](https://sel4.systems/Foundation/).
 
 ### Rendered rustdoc
 
@@ -38,11 +38,11 @@ following versions of those related projects:
   [`cd6d3b8c25d49be2b100b0608cf0613483a6fffa`](https://github.com/seL4/seL4/tree/cd6d3b8c25d49be2b100b0608cf0613483a6fffa)
   (version 13.0.0, on [github.com/seL4/seL4:master](https://github.com/seL4/seL4/tree/master))
 - seL4, when used with Microkit:
-  [`0cdbffec9cf6b4c7c9c57971cbee5a24a70c8fd0`](https://github.com/seL4/seL4/tree/0cdbffec9cf6b4c7c9c57971cbee5a24a70c8fd0)
+  [`4cae30a6ef166a378d4d23697b00106ce7e4e76f`](https://github.com/seL4/seL4/tree/4cae30a6ef166a378d4d23697b00106ce7e4e76f)
   (on [github.com/seL4/seL4:microkit](https://github.com/seL4/seL4/tree/microkit))
 - seL4 Microkit:
-  [`1ccdfcb3b224533c965fd6508de3dd56657f959c`](https://github.com/seL4/microkit/tree/1ccdfcb3b224533c965fd6508de3dd56657f959c)
-  (version 1.3.0, on [github.com/seL4/microkit:main](https://github.com/seL4/microkit/tree/main))
+  [`395cf0e5be489bbd7586b012188fc1f712cd1a57`](https://github.com/seL4/microkit/tree/395cf0e5be489bbd7586b012188fc1f712cd1a57)
+  (version 1.4.1, on [github.com/seL4/microkit:main](https://github.com/seL4/microkit/tree/main))
 
 ### Demos
 

crates/private/meta/Cargo.nix

@@ -25,16 +25,33 @@ mk {
       sel4-async-unsync
       sel4-atomic-ptr
       sel4-bounce-buffer-allocator
+      sel4-dlmalloc
+      sel4-driver-interfaces
+      sel4-elf-header
       sel4-immediate-sync-once-cell
       sel4-immutable-cell
+      sel4-initialize-tls
       sel4-logging
+      sel4-newlib
       sel4-one-ref-cell
+      sel4-panicking
+      sel4-panicking-env
       sel4-shared-ring-buffer
       sel4-shared-ring-buffer-block-io
       sel4-shared-ring-buffer-block-io-types
       sel4-shared-ring-buffer-bookkeeping
       sel4-shared-ring-buffer-smoltcp
+      sel4-stack
       sel4-sync
+      sel4-sync-trivial
+
+      sel4-bcm2835-aux-uart-driver
+      sel4-pl011-driver
+      sel4-pl031-driver
+      sel4-sp804-driver
+      sel4-virtio-blk
+      sel4-virtio-hal-impl
+      sel4-virtio-net
     ;
 
     sel4-externally-shared = localCrates.sel4-externally-shared // { features = [ "unstable" ]; };
@@ -46,6 +63,11 @@ mk {
   target."cfg(not(target_thread_local))".dependencies = {
     sel4 = localCrates.sel4 // { features = [ "single-threaded" ]; };
   };
+  target."cfg(target_arch = \"aarch64\")".dependencies = {
+    inherit (localCrates)
+      sel4-reset
+    ;
+  };
   target."cfg(not(target_arch = \"x86_64\"))".dependencies = {
     sel4-platform-info = localCrates.sel4-platform-info  // { optional = true; };
   };

crates/private/meta/Cargo.toml

@@ -32,27 +32,46 @@ sel4-async-single-threaded-executor = { path = "../../sel4-async/single-threaded
 sel4-async-time = { path = "../../sel4-async/time" }
 sel4-async-unsync = { path = "../../sel4-async/unsync" }
 sel4-atomic-ptr = { path = "../../sel4-atomic-ptr" }
+sel4-bcm2835-aux-uart-driver = { path = "../../drivers/bcm2835-aux-uart" }
 sel4-bounce-buffer-allocator = { path = "../../sel4-bounce-buffer-allocator" }
 sel4-config = { path = "../../sel4/config" }
+sel4-dlmalloc = { path = "../../sel4-dlmalloc" }
+sel4-driver-interfaces = { path = "../../sel4-driver-interfaces" }
+sel4-elf-header = { path = "../../sel4-elf-header" }
 sel4-externally-shared = { path = "../../sel4-externally-shared", features = ["unstable"] }
 sel4-immediate-sync-once-cell = { path = "../../sel4-immediate-sync-once-cell" }
 sel4-immutable-cell = { path = "../../sel4-immutable-cell" }
+sel4-initialize-tls = { path = "../../sel4-initialize-tls" }
 sel4-logging = { path = "../../sel4-logging" }
 sel4-microkit = { path = "../../sel4-microkit", features = ["full"], optional = true }
 sel4-microkit-message = { path = "../../sel4-microkit/message", optional = true }
 sel4-microkit-message-types = { path = "../../sel4-microkit/message/types", optional = true }
+sel4-newlib = { path = "../../sel4-newlib" }
 sel4-one-ref-cell = { path = "../../sel4-one-ref-cell" }
+sel4-panicking = { path = "../../sel4-panicking" }
+sel4-panicking-env = { path = "../../sel4-panicking/env" }
+sel4-pl011-driver = { path = "../../drivers/pl011" }
+sel4-pl031-driver = { path = "../../drivers/pl031" }
 sel4-root-task = { path = "../../sel4-root-task", features = ["full"], optional = true }
 sel4-shared-ring-buffer = { path = "../../sel4-shared-ring-buffer" }
 sel4-shared-ring-buffer-block-io = { path = "../../sel4-shared-ring-buffer/block-io" }
 sel4-shared-ring-buffer-block-io-types = { path = "../../sel4-shared-ring-buffer/block-io/types" }
 sel4-shared-ring-buffer-bookkeeping = { path = "../../sel4-shared-ring-buffer/bookkeeping" }
 sel4-shared-ring-buffer-smoltcp = { path = "../../sel4-shared-ring-buffer/smoltcp" }
+sel4-sp804-driver = { path = "../../drivers/sp804" }
+sel4-stack = { path = "../../sel4-stack" }
 sel4-sync = { path = "../../sel4-sync" }
+sel4-sync-trivial = { path = "../../sel4-sync/trivial" }
 sel4-sys = { path = "../../sel4/sys" }
+sel4-virtio-blk = { path = "../../drivers/virtio/blk" }
+sel4-virtio-hal-impl = { path = "../../drivers/virtio/hal-impl" }
+sel4-virtio-net = { path = "../../drivers/virtio/net" }
 
 [target."cfg(not(target_arch = \"x86_64\"))".dependencies]
 sel4-platform-info = { path = "../../sel4-platform-info", optional = true }
 
 [target."cfg(not(target_thread_local))".dependencies]
 sel4 = { path = "../../sel4", features = ["single-threaded"] }
+
+[target."cfg(target_arch = \"aarch64\")".dependencies]
+sel4-reset = { path = "../../sel4-reset" }

crates/private/meta/src/lib.rs

@@ -23,9 +23,11 @@
 //!   notification-based mutexes.
 //! - [`sel4_logging`]: [`Log`](log::Log) implementation for the [`log`] crate.
 //! - [`sel4_externally_shared`]: Abstractions for interacting with data in shared memory.
-//! - [`sel4_shared_ring_buffer`]: Implementation of shared data structures used in the [seL4 Device
+//! - [`sel4_shared_ring_buffer`] and `sel4_shared_ring_buffer_*`: Implementation of shared data structures used in the [seL4 Device
 //!   Driver Framework](https://github.com/au-ts/sddf).
 //! - `sel4_async_*`: Crates for leveraging async Rust in seL4 userspace.
+//! - `sel4_*_driver`: Crates implementing drivers for use with `sel4_shared_ring_buffer_*` and the orthogonal [`sel4_driver_interfaces`].
+//! - ...and many more, including lower-level crates for implementing additional runtimes.
 //!
 //! ### Runtime crates
 //!
@@ -79,6 +81,10 @@ pub mod absent {}
 
 definitely! {
     sel4
+    sel4_sys
+    sel4_config
+
+    // sel4_abstract_rc
     sel4_async_block_io
     sel4_async_block_io_fat
     sel4_async_io
@@ -88,19 +94,42 @@ definitely! {
     sel4_async_unsync
     sel4_atomic_ptr
     sel4_bounce_buffer_allocator
-    sel4_config
+    sel4_dlmalloc
+    sel4_driver_interfaces
+    sel4_elf_header
     sel4_externally_shared
     sel4_immediate_sync_once_cell
     sel4_immutable_cell
+    sel4_initialize_tls
     sel4_logging
+    sel4_newlib
     sel4_one_ref_cell
+    sel4_panicking
+    sel4_panicking_env
+}
+
+maybe! {
+    #[cfg(target_arch = "aarch64")]
+    sel4_reset
+}
+
+definitely! {
     sel4_shared_ring_buffer
     sel4_shared_ring_buffer_block_io
     sel4_shared_ring_buffer_block_io_types
     sel4_shared_ring_buffer_bookkeeping
     sel4_shared_ring_buffer_smoltcp
+    sel4_stack
     sel4_sync
-    sel4_sys
+    sel4_sync_trivial
+
+    sel4_bcm2835_aux_uart_driver
+    sel4_pl011_driver
+    sel4_pl031_driver
+    sel4_sp804_driver
+    sel4_virtio_net
+    sel4_virtio_blk
+    sel4_virtio_hal_impl
 }
 
 maybe! {

crates/sel4-microkit/base/src/defer.rs

@@ -91,6 +91,7 @@ impl PreparedDeferredAction {
     }
 }
 
+/// Utility type for implementing [`Handler::take_deferred_action`].
 // TODO maybe excessive. remove?
 pub struct DeferredActionSlot {
     inner: Option<DeferredAction>,

crates/sel4-microkit/base/src/handler.rs

@@ -37,6 +37,9 @@ pub trait Handler {
         panic!("unexpected protected procedure call from channel {channel:?} with msg_info={msg_info:?}")
     }
 
+    /// This method has the same meaning and type as its analog in `libmicrokit`.
+    ///
+    /// The default implementation just panics.
     fn fault(
         &mut self,
         child: Child,

crates/sel4-microkit/base/src/message.rs

@@ -4,9 +4,13 @@
 // SPDX-License-Identifier: BSD-2-Clause
 //
 
+/// Type alias for [`MessageInfo`] labels.
 pub type MessageLabel = sel4::Word;
+
+/// Type alias for message register values.
 pub type MessageRegisterValue = sel4::Word;
 
+/// Corresponds to `microkit_msginfo`.
 #[derive(Debug, Clone)]
 pub struct MessageInfo {
     inner: sel4::MessageInfo,
@@ -32,18 +36,22 @@ impl MessageInfo {
         Self::from_inner(sel4::MessageInfo::new(label, 0, 0, count))
     }
 
+    /// The label associated with this message.
     pub fn label(&self) -> MessageLabel {
         self.inner.label()
     }
 
+    /// The number of meaningful bits in `MessageLabel`.
     pub const fn label_width() -> usize {
         sel4::MessageInfo::label_width()
     }
 
+    /// The number of filled message registers associated with this message.
     pub fn count(&self) -> usize {
         self.inner.length()
     }
 
+    /// Interpret this message as a [`sel4::Fault`].
     pub fn fault(&self) -> sel4::Fault {
         sel4::with_ipc_buffer(|ipc_buffer| sel4::Fault::new(ipc_buffer, self.inner()))
     }
@@ -55,26 +63,33 @@ impl Default for MessageInfo {
     }
 }
 
+/// Provides access to the protection domain's message registers.
 pub fn with_msg_regs<T>(f: impl FnOnce(&[MessageRegisterValue]) -> T) -> T {
     sel4::with_ipc_buffer(|ipc_buffer| f(ipc_buffer.msg_regs()))
 }
 
+/// Provides mutable access to the protection domain's message registers.
 pub fn with_msg_regs_mut<T>(f: impl FnOnce(&mut [MessageRegisterValue]) -> T) -> T {
     sel4::with_ipc_buffer_mut(|ipc_buffer| f(ipc_buffer.msg_regs_mut()))
 }
 
+/// Provides access to the protection domain's message registers, viewed as an array of bytes.
 pub fn with_msg_bytes<T>(f: impl FnOnce(&[u8]) -> T) -> T {
     sel4::with_ipc_buffer(|ipc_buffer| f(ipc_buffer.msg_bytes()))
 }
 
+/// Provides mutable access to the protection domain's message registers, viewed as an array of
+/// bytes.
 pub fn with_msg_bytes_mut<T>(f: impl FnOnce(&mut [u8]) -> T) -> T {
     sel4::with_ipc_buffer_mut(|ipc_buffer| f(ipc_buffer.msg_bytes_mut()))
 }
 
+/// Corresponds to `microkit_mr_set`.
 pub fn set_mr(i: usize, value: MessageRegisterValue) {
     with_msg_regs_mut(|regs| regs[i] = value)
 }
 
+/// Corresponds to `microkit_mr_get`.
 pub fn get_mr(i: usize) -> MessageRegisterValue {
     with_msg_regs(|regs| regs[i])
 }