Enable mapping extra TCB and SC caps into PD's

docs/manual.md

@@ -984,6 +984,13 @@ virtual CPU with ID `vcpu`.
 Write the registers of a given virtual CPU with ID `vcpu`. The `regs` argument is the pointer to
 the struct of registers `seL4_VCPUContext` that are written from.
 
+## `seL4_CPtr microkit_cspace_slot_to_cptr(seL4_Word slot)` {#libmicrokit_cspace_slot_to_cptr}
+
+Converts the slot identifier of the `<cspace>`'s capability element into an
+`seL4_CPtr` value to be used in `libsel4` calls by the PD.
+
+If the slot exceeds the valid range of inputs (`0 <= slot < MICROKIT_MAX_USER_CAPS`), it returns the value `seL4_CapNull`.
+
 # System Description File {#sysdesc}
 
 This section describes the format of the System Description File (SDF).
@@ -1025,6 +1032,7 @@ Additionally, it supports the following child elements:
 * `protection_domain`: (zero or more) Describes a child protection domain.
 * `virtual_machine`: (zero or one) Describes a child virtual machine.
 * `ioport`: (zero or more) Describes an I/O port, x86-64 only.
+* `cspace`: (zero or one) Describes ["extra" capabilities](#sdf-cspace) in the microkit-provided CSpace.
 
 The `program_image` element has the following attributes:
 
@@ -1125,6 +1133,29 @@ It supports the following attributes:
 
 The `memory_region` element does not support any child elements.
 
+## `cspace` {#sdf-cspace}
+
+The `cspace` element represents the *Capability Space* of each protection domain.
+This is an advanced feature designed for users of Microkit who want more complex runtime behaviour than the system description file allows.
+For more details on how CSpaces and capabilities work, please see the ['Capability Spaces' section of the seL4 reference manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf#chapter.3).
+
+It supports no attributes, but supports the following elements as children:
+
+* `cap_tcb`: A capability to a protection domain's Thread Control Block (TCB).
+* `cap_sc`: A capability to a protection domain's Scheduling Context (SC).
+  If the protection domain is passive, this is a capability to the notification's scheduling context.
+* `cap_vspace`: A capability to a protection domain's VSpace.
+* `cap_cspace`: A capability to a protection domain's CSpace.
+
+All of the elements support the `slot` attribute, which is is an opaque identifier used to address the capability at runtime.
+To convert the `slot` to an `seL4_CPtr`, use the [`seL4_CPtr microkit_cspace_slot_to_cptr(seL4_Word slot)`](#libmicrokit_cspace_slot_to_cptr) function.
+
+See the 'cap_sharing' example packaged in your SDK or [on GitHub](https://github.com/seL4/microkit/tree/main/example/cap_sharing).
+
+All capability elements (currently) all support the `pd` attribute, the name of the protection domain that the capability is from.
+For instance, `<cap_tcb slot="1" pd="alpha">` will place the TCB of PD 'alpha' in the CSpace of the current PD.
+
+
 ### Page sizes by architecture
 
 Below are the available page sizes for each architecture that Microkit supports.

example/cap_sharing/Makefile

@@ -0,0 +1,71 @@
+#
+# Copyright 2026, UNSW
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+ifeq ($(strip $(BUILD_DIR)),)
+$(error BUILD_DIR must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_SDK)),)
+$(error MICROKIT_SDK must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_BOARD)),)
+$(error MICROKIT_BOARD must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_CONFIG)),)
+$(error MICROKIT_CONFIG must be specified)
+endif
+
+BOARD_DIR := $(MICROKIT_SDK)/board/$(MICROKIT_BOARD)/$(MICROKIT_CONFIG)
+
+ARCH := ${shell grep 'CONFIG_SEL4_ARCH  ' $(BOARD_DIR)/include/kernel/gen_config.h | cut -d' ' -f4}
+
+ifeq ($(ARCH),aarch64)
+  TARGET_TRIPLE := aarch64-none-elf
+  CFLAGS_ARCH := -mstrict-align
+else ifeq ($(ARCH),riscv64)
+  TARGET_TRIPLE := riscv64-unknown-elf
+  CFLAGS_ARCH := -march=rv64imafdc_zicsr_zifencei -mabi=lp64d
+else ifeq ($(ARCH),x86_64)
+	TARGET_TRIPLE := x86_64-linux-gnu
+	CFLAGS_ARCH := -march=x86-64 -mtune=generic
+else
+$(error Unsupported ARCH)
+endif
+
+ifeq ($(strip $(LLVM)),True)
+  CC := clang -target $(TARGET_TRIPLE)
+  AS := clang -target $(TARGET_TRIPLE)
+  LD := ld.lld
+else
+  CC := $(TARGET_TRIPLE)-gcc
+  LD := $(TARGET_TRIPLE)-ld
+  AS := $(TARGET_TRIPLE)-as
+endif
+
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
+
+IMAGES := cap_sharing.elf secondary.elf
+CFLAGS := -nostdlib -ffreestanding -g -O3 -Wall  -Wno-unused-function -Werror -I$(BOARD_DIR)/include $(CFLAGS_ARCH)
+LDFLAGS := -L$(BOARD_DIR)/lib
+LIBS := -lmicrokit -Tmicrokit.ld
+
+IMAGE_FILE = $(BUILD_DIR)/loader.img
+REPORT_FILE = $(BUILD_DIR)/report.txt
+
+all: $(IMAGE_FILE)
+
+$(BUILD_DIR):
+	mkdir -p $@
+
+$(BUILD_DIR)/%.o: %.c Makefile | $(BUILD_DIR)
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.elf: $(BUILD_DIR)/%.o
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) cap_sharing.system
+	$(MICROKIT_TOOL) cap_sharing.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)

example/cap_sharing/README.md

@@ -0,0 +1,44 @@
+<!--
+     Copyright 2026, UNSW
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+# Example - Cap Sharing
+
+This is a basic example that demonstrates how one can use the `<cspace>` element
+of a PD to give delegated access of specific capabilities associated with other
+(or its own) protection domain.
+
+See `cap_sharing.system` for some comments on the internal setup of this system.
+The idea behind this example is that we have two PDs, one of which has control
+over the TCB and scheduling context of the other; this could be the basis of
+(e.g.) a user space scheduler.
+
+All supported platforms are supported in this example.
+
+## Building
+
+```sh
+mkdir build
+make BUILD_DIR=build MICROKIT_BOARD=<board> MICROKIT_CONFIG=<debug/release/benchmark> MICROKIT_SDK=/path/to/sdk
+```
+
+## Running
+
+See instructions for your board in the manual.
+
+You should see the following output:
+
+```
+INFO  [sel4_capdl_initializer::initialize] Starting CapDL initializer
+INFO  [sel4_capdl_initializer::initialize] Starting threads
+MON|INFO: Microkit Monitor started!
+|secondary| hello, world
+|primary  | hello, world
+|primary  | notifying secondary
+|secondary| notified
+|primary  | suspending secondary
+|primary  | notifying secondary (it should not print)
+|primary  | resuming secondary (it should then print)
+|secondary| notified
+|primary  | halting (success)...
+```

example/cap_sharing/cap_sharing.c

@@ -0,0 +1,63 @@
+/*
+ * Copyright 2026, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stdint.h>
+#include <microkit.h>
+
+#define CH_SECONDARY ((microkit_channel)0)
+
+// As per cap_sharing.system
+#define CAP_SECONDARY_SC  (microkit_cspace_slot_to_cptr(1))
+#define CAP_SECONDARY_TCB (microkit_cspace_slot_to_cptr(2))
+#define CAP_MY_SC         (microkit_cspace_slot_to_cptr(3))
+#define CAP_MY_TCB        (microkit_cspace_slot_to_cptr(4))
+
+static void halt(void)
+{
+    seL4_Error error = seL4_TCB_Suspend(CAP_MY_TCB);
+    if (error != seL4_NoError) {
+        microkit_dbg_puts("|primary  | error suspending TCB\n");
+    }
+
+    microkit_dbg_puts("|primary  | error: should not reach this point! we should have suspended ourself!\n");
+    while (1) { }
+}
+
+void init(void)
+{
+    seL4_Error err;
+
+    microkit_dbg_puts("|primary  | hello, world\n");
+
+    /* Notify the secondary. This will print output from secondary as it is
+       higher priority. */
+    microkit_dbg_puts("|primary  | notifying secondary\n");
+    microkit_notify(CH_SECONDARY);
+
+    microkit_dbg_puts("|primary  | suspending secondary\n");
+    err = seL4_TCB_Suspend(CAP_SECONDARY_TCB);
+    if (err != seL4_NoError) {
+        microkit_dbg_puts("|primary  | error suspending TCB\n");
+        halt();
+    }
+
+    /* Notify the secondary. It is suspended so it will not print. */
+    microkit_dbg_puts("|primary  | notifying secondary (it should not print)\n");
+    microkit_notify(CH_SECONDARY);
+
+    microkit_dbg_puts("|primary  | resuming secondary (it should then print)\n");
+    err = seL4_TCB_Resume(CAP_SECONDARY_TCB);
+    if (err != seL4_NoError) {
+        microkit_dbg_puts("|primary  | error resuming TCB\n");
+        halt();
+    }
+
+    microkit_dbg_puts("|primary  | halting (success)...\n");
+    halt();
+}
+
+void notified(microkit_channel ch)
+{
+}

example/cap_sharing/cap_sharing.system

@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="primary" priority="1">
+        <program_image path="cap_sharing.elf" />
+
+        <cspace>
+            <!-- You can have the SC or TCB of another PD -->
+            <cap_sc  slot="1" pd="secondary" />
+            <cap_tcb slot="2" pd="secondary" />
+
+            <!-- You can also have it of yourself -->
+            <cap_sc  slot="3" pd="primary" />
+            <cap_tcb slot="4" pd="primary" />
+        </cspace>
+    </protection_domain>
+
+    <protection_domain name="secondary" priority="2">
+        <program_image path="secondary.elf" />
+    </protection_domain>
+
+    <channel>
+        <end pd="primary" id="0" />
+        <end pd="secondary" id="0" />
+    </channel>
+</system>

example/cap_sharing/secondary.c

@@ -0,0 +1,18 @@
+/*
+ * Copyright 2026, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stdint.h>
+#include <microkit.h>
+
+void init(void)
+{
+    microkit_dbg_puts("|secondary| hello, world\n");
+}
+
+void notified(microkit_channel ch)
+{
+    microkit_dbg_puts("|secondary| notified\n");
+    microkit_notify(ch);
+}

libmicrokit/include/microkit.h

@@ -28,7 +28,9 @@ typedef seL4_MessageInfo_t microkit_msginfo;
 #define BASE_VM_TCB_CAP 266
 #define BASE_VCPU_CAP 330
 #define BASE_IOPORT_CAP 394
+#define BASE_USER_CAPS 458
 
+#define MICROKIT_MAX_USER_CAPS 128
 #define MICROKIT_MAX_CHANNELS 62
 #define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1)
 #define MICROKIT_MAX_IOPORT_ID MICROKIT_MAX_CHANNELS
@@ -506,3 +508,19 @@ static inline void microkit_deferred_irq_ack(microkit_channel ch)
     microkit_signal_msg = seL4_MessageInfo_new(IRQAckIRQ, 0, 0, 0);
     microkit_signal_cap = (BASE_IRQ_CAP + ch);
 }
+
+/**
+ * Convert the "slot" identifier from the system file for the extra user caps
+ * <cspace> element into the seL4_CPtr at runtime.
+ *
+ * If the slot exceeds the valid range of inputs (0 <= slot < MICROKIT_MAX_USER_CAPS),
+ * it returns the value `seL4_CapNull`.
+ **/
+static inline seL4_CPtr microkit_cspace_slot_to_cptr(seL4_Word slot)
+{
+    if (slot > MICROKIT_MAX_USER_CAPS) {
+        return seL4_CapNull;
+    }
+
+    return BASE_USER_CAPS + slot;
+}