Domain schedules

build_sdk.py

@@ -53,6 +53,19 @@
     # Turning off this feature removes the __thread attribute on
     # __sel4_ipc_buffer and makes it a true global.
     "LibSel4UseThreadLocals": False,
+
+    # The domain scheduler is turned on by default with 16 domains and 100
+    # schedules. This represent the maximums imposed by the static build of
+    # the kernel; we can easily have less domains or schedules.
+    # Both of these are arbitrary values; increasing them has a memory cost
+    # for seL4.
+    # Having the domain scheduler enabled in the kernel has no impact if we
+    # only have one domain schedule (the non-domain kernel build has NumDomains = 1,
+    # and the same code is run).
+    # NOTE: If updating make sure to update the manual too.
+    "KernelNumDomains": 16,
+    # This is the current default value used by seL4.
+    "KernelNumDomainSchedules": 100,
 }
 
 DEFAULT_KERNEL_OPTIONS_AARCH64: KERNEL_OPTIONS = {
@@ -507,6 +520,7 @@ class KernelPath:
 
 EXAMPLES = {
     "hello": Path("example/hello"),
+    "domains": Path("example/domains"),
     "ethernet": Path("example/ethernet"),
     "passive_server": Path("example/passive_server"),
     "hierarchy": Path("example/hierarchy"),
@@ -523,6 +537,8 @@ def elaborate_all_board_configs(board: BoardInfo) -> list[ConfigInfo]:
             config.name = f"smp-{config.name}"
             config.kernel_options |= {
                 "KernelMaxNumNodes": str(board.smp_cores),
+                # SMP configurations of seL4 do not support the domain scheduler
+                "KernelNumDomains": 1,
             }
             elaborated_configs.append(config)
 

docs/manual.md

@@ -110,6 +110,7 @@ This document attempts to clearly describe all of these terms, however as the co
 * [fault](#fault)
 * [ioport](#ioport)
 * [IO address space](#io_address_space)
+* [domain scheduling](#domains)
 
 ## System {#system}
 
@@ -381,6 +382,40 @@ IO Address Spaces provide a way to isolate device memory accesses within a fixed
 
 IO Address Spaces allow *memory regions* to be mapped to a provided base IO virtual address. These IO virtual addresses will be translated by the hardware IOMMU or SMMU to the underlying physical memory that backs the memory region.
 
+## Domain Scheduling {#domains}
+
+seL4, and by extension, Microkit, supports a domain scheduler.
+Domains are used to isolate independent subsystems (sets of protection domains)
+and limit information flow between them.
+
+seL4 switches between the domains according to a cyclical schedule where each
+domain runs for a static duration. Protection domains belong to exactly one
+domain each, and only will run when that domain is active.
+
+The default system fault handler (aka the monitor) lives in domain 0.
+
+Below we describe the behaviour of the domain scheduler and its relevance to
+the Microkit system with reference to the [SDF syntax for Domains](#sdf-domains).
+
+The list of `<schedule_entry>` within the `<domain_schedule>` element defines
+the domain schedule. The kernel steps through each schedule entry, starting
+from the `start_index`, until reaching an `<schedule_end_marker>`. Upon reaching
+the "end marker", it restarts at `start_index` once again. This allows one to
+use the domain schedule to setup multiple schedules that can be atomically
+switched between, though at this time Microkit does not expose this feature.
+
+The scheduler duration at the seL4 kernel level is specified in terms of
+platform-specific timer ticks. When specifying a duration in microseconds,
+the capDL initialiser must convert these to timer ticks. It guarantees that
+either it will be the nearest tick value, or that it will fail to boot. If you
+want platform-specific guarantees of certain tick values, you can still specify
+ticks.
+
+There is always an implicit `<schedule_end_marker>` at the end of the schedule.
+
+For more details on the domain schedule, please see [RFC-20: Runtime domain
+schedules](https://sel4.github.io/rfcs/implemented/0200-domain-schedules.html).
+
 # SDK {#sdk}
 
 Microkit is distributed as a software development kit (SDK).
@@ -939,6 +974,7 @@ Within the `system` root element the following child elements are supported:
 * `protection_domain`
 * `memory_region`
 * `channel`
+* `domains`
 
 ## `protection_domain`
 
@@ -956,6 +992,8 @@ It supports the following attributes:
 * `cpu`: (optional) set the physical CPU core this PD will run on. Defaults to zero.
 * `smc`: (optional, only on ARM) Allow the PD to give an SMC call for the kernel to perform.. Defaults to false.
 * `fpu`: (optional) whether this PD can access the FPU. Defaults to true.
+* `domain`: (conditionally required) the name of the domain that this PD belongs to.
+            If a domain schedule is specified, this is mandatory, else it is disallowed.
 
 Additionally, it supports the following child elements:
 
@@ -1118,6 +1156,50 @@ The `iomap` element supports the following attributes:
 * `perms`: Identifies the permissions with which to map the memory region. Can be a combination of `r` (read), and `w` (write).
            Defaults to read-write.
 
+## `domains` {#sdf-domains}
+
+The `domains` element describes the (security) domains and their schedule within
+a microkit system. seL4 only supports the domain scheduler on non-SMP (unicore)
+configurations. There is a fixed upper limit on the number of domains and the
+number of schedule entries, determined by the kernel configurations `KernelNumDomains`
+and `KernelNumDomainSchedules`. In the default SDK build, we support 16 domains and
+100 schedule entries.
+
+<!-- If updating make sure to update build_sdk.py -->
+
+The SDK includes a 'Domains' example which contains a basic example and commented
+example of a valid SDF containing a domain schedule.
+
+It supports no attributes, but supports the following elements as children:
+
+* `domain`: (one or more) Provides a human-readable name for a domain ID.
+* `domain_schedule`: (exactly one) Contains the list of scheduler entries.
+
+The `domain` element has no children, but supports the following attributes:
+
+* `name`: A unique name for the domain.
+* `id`: (optional) The domain ID.
+
+The `domain_schedule` element specifies the domain schedule.
+Please see the [Domains](#domains) reference for details on these.
+It has the following attributes:
+
+* `start_index` (optional, defaults to 0) defines the 'start index' of the schedule
+* `index_shift` (optional) the offset of the Microkit domain schedule within
+                the kernel's domain schedule array.
+
+It supports two types of child element, the `<schedule_entry>` and the
+`<schedule_end_marker>`.
+
+The `<schedule_entry>` requires the following attributes:
+
+* `domain`: The name of the domain to be scheduled.
+* `duration`: The duration for which the domain should be active.
+              This contains a value and a unit, i.e. `1000 us`.
+              The unit can either be 'us' or 'ticks'.
+
+The `<schedule_end_marker>` has no attributes or children.
+
 ### Page sizes by architecture
 
 Below are the available page sizes for each architecture that Microkit supports.

example/domains/Makefile

@@ -0,0 +1,72 @@
+#
+# Copyright 2026, UNSW
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+BUILD_DIR ?= build
+
+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 := emitter.elf collector.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
+SPEC_FILE = $(BUILD_DIR)/capdl_spec.json
+
+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)) domains.system
+	$(MICROKIT_TOOL) domains.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) \
+		--viper-output ${BUILD_DIR}/viper -r $(REPORT_FILE) --capdl-json $(SPEC_FILE)

example/domains/README.md

@@ -0,0 +1,81 @@
+<!--
+     Copyright 2026, UNSW
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+
+# Example - Domains
+
+This is a basic example that uses the seL4 domain scheduler.
+
+It is similar to the [CAmkES](https://github.com/seL4/camkes/tree/camkes-3.12.x-compatible/apps/domains)
+example application 'Domains'.
+
+It uses three domains: monitor (0), emitter (1), and collector (2).
+Domain 0 runs the Microkit monitor. Domain 1 contains the emitter PD, and
+Domain 2 the collector PD.
+
+The emitter will be able to do a large number of notifies before the collector
+has time to run. Because notifications are coalesced by seL4, one should not see the
+100,000 notifies that the emitter produces, but only a smaller number, once
+per time the collector runs. A shorter duration for the domain 1 (emitter)
+will cause domain 2 (collector) to see more events.
+
+Look at the `domains.system` file for a commented example of the syntax.
+
+## Example Output
+
+```
+INFO  [sel4_capdl_initializer::initialize] Starting threads
+MON|INFO: Microkit Monitor started!
+emitter: starting to emit events...
+collector: Waiting for an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+emitter: still emitting collector: Got an event
+collector: Got an event
+events...
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+emitter: still emitting events...
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+emitter: still emitting events...
+...
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+collector: Got an event
+emitter: still emitting events...
+emitter: done emitting events
+collector: Got an event
+collector: Got an event
+```
+
+## Building
+
+```sh
+make MICROKIT_BOARD=<board> MICROKIT_CONFIG=debug MICROKIT_SDK=/path/to/sdk
+```
+
+## Running
+
+See instructions for your board in the manual.

example/domains/collector.c

@@ -0,0 +1,17 @@
+/*
+ * Copyright 2026, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stdint.h>
+#include <microkit.h>
+
+void init(void)
+{
+    microkit_dbg_puts("collector: Waiting for an event\n");
+}
+
+void notified(microkit_channel ch)
+{
+    microkit_dbg_puts("collector: Got an event\n");
+}

example/domains/domains.system

@@ -0,0 +1,45 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+    Copyright 2026, UNSW
+
+    SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <!-- This element is used to declare the list of domains, to give
+         each domain a human-readable name. -->
+    <domains>
+        <!-- The first domain contains the Microkit Monitor PD, but can contain others. -->
+        <domain name="monitor" id="0" />
+        <!-- You give each domain a name and its domain id. -->
+        <domain name="emitter" id="1" />
+        <!-- The domain ID is optional and can be auto-assigned if desired.
+             It will be assigned to the smallest unused ID, and must be less
+             than KernelNumDomains. -->
+        <domain name="collector" />
+
+        <!-- This is a domain schedule. Note that the same domain can appear twice
+             in the schedule.
+             Also supports optional attributes "start_index" and "index_shift".
+         -->
+        <domain_schedule>
+            <schedule_entry domain="monitor" duration="6000 us" />
+            <schedule_entry domain="emitter" duration="8000 us" />
+            <schedule_entry domain="collector" duration="2000 us" />
+            <!-- This element is optional, and is implicitly there anyway. -->
+            <schedule_end_marker />
+        </domain_schedule>
+    </domains>
+
+    <protection_domain name="emitter" domain="emitter">
+        <program_image path="emitter.elf" />
+    </protection_domain>
+
+    <protection_domain name="collector" domain="collector">
+        <program_image path="collector.elf" />
+    </protection_domain>
+
+    <channel>
+        <end pd="emitter" id="0" />
+        <end pd="collector" id="0" notify="false" />
+    </channel>
+</system>