From 3631766fc860edf7e150da0f42605e4f3e8f2325 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Thu, 16 Jul 2026 15:58:00 +1000
Subject: [PATCH 1/8] tool: rename domain_ids -> iommu_domain_ids

This is confusing with seL4 domains.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 tool/microkit/src/sdf.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs
index 191b0da54..985097906 100644
--- a/tool/microkit/src/sdf.rs
+++ b/tool/microkit/src/sdf.rs
@@ -2437,7 +2437,7 @@ pub fn parse(
     let mut mrs = vec![];
     let mut iomaps = vec![];
     let mut device_names = HashSet::new();
-    let mut domain_ids = HashSet::new();
+    let mut iommu_domain_ids = HashSet::new();
     let mut iommu_device_identifiers = HashSet::new();
     let mut channels = vec![];
     let system = doc
@@ -2478,7 +2478,7 @@ pub fn parse(
                         &xml_sdf,
                         &child,
                         &mut device_names,
-                        &mut domain_ids,
+                        &mut iommu_domain_ids,
                         &mut iommu_device_identifiers,
                     )?
                     .iomaps,

From 72e1ab15e6346fa519bcf6ee59d2dec4410b931f Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Thu, 16 Jul 2026 12:52:30 +1000
Subject: [PATCH 2/8] domains: enable on non-smp configs by default

Having a domain scheduler causes no issues if the domain
scheduler is unused, so we can turn it on on non-smp
configurations. (seL4 does not support SMP domain-scheduler).

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 build_sdk.py | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/build_sdk.py b/build_sdk.py
index 7ec4e3178..8a3056908 100644
--- a/build_sdk.py
+++ b/build_sdk.py
@@ -53,6 +53,18 @@
     # 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).
+    "KernelNumDomains": 16,
+    # This is the current default value used by seL4.
+    "KernelNumDomainSchedules": 100,
 }
 
 DEFAULT_KERNEL_OPTIONS_AARCH64: KERNEL_OPTIONS = {
@@ -523,6 +535,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)
 

From d27e038746806577adebf8c816b7037d6f0901ba Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Thu, 16 Jul 2026 15:04:19 +1000
Subject: [PATCH 3/8] domains: gather relevant kernel constants

These will be useful later.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 tool/microkit/src/main.rs   | 4 ++++
 tool/microkit/src/sel4.rs   | 2 ++
 tool/microkit/tests/test.rs | 4 ++++
 3 files changed, 10 insertions(+)

diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs
index dd6934e64..daaaefeb3 100644
--- a/tool/microkit/src/main.rs
+++ b/tool/microkit/src/main.rs
@@ -279,6 +279,10 @@ fn main() -> Result<(), String> {
         } else {
             1
         },
+        num_domains: json_str_as_u64(&kernel_config_json, "NUM_DOMAINS")?
+            .try_into()
+            .unwrap(),
+        num_domain_schedules: json_str_as_u64(&kernel_config_json, "NUM_DOMAIN_SCHEDULES")?,
         fpu: json_str_as_bool(&kernel_config_json, "HAVE_FPU")?,
         arm_pa_size_bits,
         arm_smc,
diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs
index 83d66bac5..d95084a74 100644
--- a/tool/microkit/src/sel4.rs
+++ b/tool/microkit/src/sel4.rs
@@ -308,6 +308,8 @@ pub struct Config {
     pub hypervisor: bool,
     pub benchmark: bool,
     pub num_cores: u8,
+    pub num_domains: u8,
+    pub num_domain_schedules: u64,
     pub fpu: bool,
     /// ARM-specific, number of physical address bits
     pub arm_pa_size_bits: Option<usize>,
diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs
index 30f509452..3e46377da 100644
--- a/tool/microkit/tests/test.rs
+++ b/tool/microkit/tests/test.rs
@@ -40,6 +40,8 @@ const DEFAULT_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config {
     iommu: true,
     benchmark: false,
     num_cores: 1,
+    num_domains: 16,
+    num_domain_schedules: 100,
     fpu: true,
     arm_pa_size_bits: Some(40),
     arm_smc: None,
@@ -71,6 +73,8 @@ const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config {
     iommu: true,
     benchmark: false,
     num_cores: 1,
+    num_domains: 16,
+    num_domain_schedules: 100,
     fpu: true,
     arm_pa_size_bits: None,
     arm_smc: None,

From 129d60cdb68585e3f4e9395aaccbb1e76555c0c4 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Thu, 16 Jul 2026 17:49:43 +1000
Subject: [PATCH 4/8] domains: support defining a domain schedule

This adds a new syntax which looks like this:

    <domains>
        <domain name="monitor" id="0" />
        <domain name="emitter" id="1" />
        <domain name="collector" />

        <domain_schedule start_index="3" index_shift="0" >
            <schedule_entry domain="monitor" duration="3000 us" />
            <schedule_entry domain="emitter" duration="8000 us" />
            <schedule_entry domain="collector" duration="2000 us" />
            <schedule_entry domain="monitor" duration="3000 us" />
        </domain_schedule>
    </domains>

Co-authored-by: Krishnan Winter <krishnan.winter@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 tool/microkit/src/capdl/builder.rs |  19 +-
 tool/microkit/src/sdf.rs           | 290 ++++++++++++++++++++++++++++-
 2 files changed, 302 insertions(+), 7 deletions(-)

diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs
index 9b928f767..f653a2a56 100644
--- a/tool/microkit/src/capdl/builder.rs
+++ b/tool/microkit/src/capdl/builder.rs
@@ -1278,7 +1278,16 @@ pub fn build_capdl_spec(
     }
 
     // *********************************
-    // Step 7. Sort the root objects
+    // Step 7. Emit a domain schedule
+    // *********************************
+    if system.domains.has_domains() {
+        spec_container.spec.domain_schedule = Some(system.domains.schedule.clone());
+        spec_container.spec.domain_set_start = system.domains.schedule_start_index.map(Word);
+        spec_container.spec.domain_idx_shift = system.domains.schedule_index_shift.map(Word);
+    }
+
+    // *********************************
+    // Step 8. Sort the root objects
     // *********************************
     // The CapDL initialiser expects objects with paddr to come first, then sorted by size so that the
     // allocation algorithm at run-time can run more efficiently.
@@ -1289,13 +1298,13 @@ pub fn build_capdl_spec(
     // 3. Record all of the root objects new index.
     // 4. Recurse through every cap, for any cap bearing the original object ID, write the new object ID.
 
-    // Step 6-1
+    // Step 8-1
     let mut obj_name_to_old_id: HashMap<String, ObjectId> = HashMap::new();
     for (id, obj) in spec_container.spec.objects.iter().enumerate() {
         obj_name_to_old_id.insert(obj.name.as_ref().unwrap().clone(), id.into());
     }
 
-    // Step 6-2
+    // Step 8-2
     spec_container.spec.objects.sort_by(|a, b| {
         // Objects with paddrs always come first.
         if a.object.paddr().is_none() && b.object.paddr().is_some() {
@@ -1334,7 +1343,7 @@ pub fn build_capdl_spec(
         }
     });
 
-    // Step 6-3
+    // Step 8-3
     let mut obj_old_id_to_new_id: HashMap<ObjectId, ObjectId> = HashMap::new();
     for (new_id, obj) in spec_container.spec.objects.iter().enumerate() {
         obj_old_id_to_new_id.insert(
@@ -1343,7 +1352,7 @@ pub fn build_capdl_spec(
         );
     }
 
-    // Step 6-4
+    // Step 8-4
     for obj in spec_container.spec.objects.iter_mut() {
         match obj.object.slots_mut() {
             Some(caps) => {
diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs
index 985097906..6205ff82c 100644
--- a/tool/microkit/src/sdf.rs
+++ b/tool/microkit/src/sdf.rs
@@ -22,11 +22,14 @@ use crate::sel4::{
 
 use crate::util::{get_full_path, ranges_overlap, round_up, str_to_bool};
 use crate::MAX_PDS;
-use sel4_capdl_initializer_types::{object, x86_io_address_space, FillEntryContentBootInfoId};
-use std::collections::{HashMap, HashSet};
+use sel4_capdl_initializer_types::{
+    object, x86_io_address_space, DomainSchedDuration, DomainSchedEntry, FillEntryContentBootInfoId,
+};
+use std::collections::{hash_map, HashMap, HashSet};
 use std::fmt;
 use std::fs;
 use std::hash::{Hash, Hasher};
+use std::num::NonZero;
 use std::ops::Deref;
 use std::path::{Path, PathBuf};
 use std::str::FromStr;
@@ -2124,6 +2127,275 @@ impl Channel {
     }
 }
 
+#[derive(Debug, Default)]
+pub struct Domains {
+    pub name_to_id_map: HashMap<String, u8>,
+    pub schedule_start_index: Option<u64>,
+    pub schedule_index_shift: Option<u64>,
+    pub schedule: Vec<DomainSchedEntry>,
+}
+
+impl Domains {
+    fn from_xml(
+        config: &Config,
+        xml_sdf: &XmlSystemDescription,
+        node: &roxmltree::Node,
+    ) -> Result<Self, String> {
+        check_attributes(xml_sdf, node, &[])?;
+
+        let mut name_to_id_map = HashMap::<String, Option<u8>>::new();
+        let mut id_to_name_map = HashMap::<u8, String>::new();
+        let mut domain_schedule_element = None;
+
+        for child in node.children().filter(|child| child.is_element()) {
+            match child.tag_name().name() {
+                "domain" => {
+                    let (dom_name, dom_id) = Self::domain_from_xml(config, xml_sdf, &child)?;
+
+                    if let Some(existing_dom) = name_to_id_map.insert(dom_name.clone(), dom_id) {
+                        return Err(value_error(
+                            xml_sdf,
+                            &child,
+                            format!(
+                                "Each <domain>'s name element must be unique \
+                                 found existing domain '{dom_name}' with id '{existing_dom:?}'"
+                            ),
+                        ));
+                    }
+
+                    if let Some(dom_id) = dom_id {
+                        if let Some(existing_dom) = id_to_name_map.insert(dom_id, dom_name.clone())
+                        {
+                            return Err(value_error(
+                                xml_sdf,
+                                &child,
+                                format!(
+                                    "Each <domain>'s id element must be unique \
+                                     found existing domain '{existing_dom}' with id '{dom_id}'"
+                                ),
+                            ));
+                        }
+                    }
+                }
+                "domain_schedule" => {
+                    if domain_schedule_element.is_some() {
+                        return Err(value_error(
+                            xml_sdf,
+                            &child,
+                            "The <domain_schedule> element can only appear once".to_string(),
+                        ));
+                    }
+
+                    domain_schedule_element = Some(child);
+                }
+                _ => {
+                    let pos = xml_sdf.doc.text_pos_at(child.range().start);
+                    return Err(format!(
+                        "Error: invalid XML element as child of <domains> '{}': {}",
+                        child.tag_name().name(),
+                        loc_string(xml_sdf, pos)
+                    ));
+                }
+            }
+        }
+
+        let Some(domain_schedule_element) = domain_schedule_element else {
+            return Err(value_error(
+                xml_sdf,
+                node,
+                "The <domain_schedule> element must appear once".to_string(),
+            ));
+        };
+
+        let name_to_id_map = name_to_id_map
+            .into_iter()
+            .map(|(name, dom)| match dom {
+                Some(dom) => Ok((name, dom)),
+                None => {
+                    // TODO: We could be more efficient here. However, for a
+                    // maximum of 256 possible domains, iterating over the
+                    // valid possible domain IDs is actually OK.
+
+                    let mut dom = None;
+                    for i in 0..=config.num_domains {
+                        if let hash_map::Entry::Vacant(e) = id_to_name_map.entry(i) {
+                            e.insert(name.clone());
+                            dom = Some(i);
+                            break;
+                        }
+                    }
+
+                    let Some(dom) = dom else {
+                        return Err(value_error(
+                            xml_sdf,
+                            node,
+                            format!("Number of domains exceeds {}", config.num_domains),
+                        ));
+                    };
+
+                    Ok((name, dom))
+                }
+            })
+            .collect::<Result<_, _>>()?;
+
+        Self::domain_schedule_from_xml(config, xml_sdf, &domain_schedule_element, name_to_id_map)
+    }
+
+    fn domain_from_xml(
+        config: &Config,
+        xml_sdf: &XmlSystemDescription,
+        node: &roxmltree::Node,
+    ) -> Result<(String, Option<u8>), String> {
+        check_attributes(xml_sdf, node, &["name", "id"])?;
+
+        let name = checked_lookup(xml_sdf, node, "name")?.to_string();
+
+        let domain_id = node
+            .attribute("id")
+            .map(|s| sdf_parse_number(s, node))
+            .transpose()?
+            .map(|n| {
+                if n >= config.num_domains.into() {
+                    Err(value_error(
+                        xml_sdf,
+                        node,
+                        format!(
+                            "domain id {n} should be less than the \
+                             configured KernelNumDomains value of {}",
+                            config.num_domains
+                        ),
+                    ))
+                } else {
+                    Ok(n.try_into()
+                        .expect("num_domains is u8 so by if above this is OK"))
+                }
+            })
+            .transpose()?;
+
+        Ok((name, domain_id))
+    }
+
+    fn domain_schedule_from_xml(
+        config: &Config,
+        xml_sdf: &XmlSystemDescription,
+        node: &roxmltree::Node,
+        name_to_id_map: HashMap<String, u8>,
+    ) -> Result<Domains, String> {
+        check_attributes(xml_sdf, node, &["index_shift", "start_index"])?;
+
+        let schedule_start_index = node
+            .attribute("start_index")
+            .map(|s| sdf_parse_number(s, node))
+            .transpose()?
+            // The domain schedule is only started when the start index is Some(...)
+            // so even when not specified we default to a start index of zero.
+            .unwrap_or(0);
+
+        let schedule_index_shift = node
+            .attribute("index_shift")
+            .map(|s| sdf_parse_number(s, node))
+            .transpose()?;
+
+        let mut schedule = vec![];
+
+        for child in node.children().filter(|c| c.is_element()) {
+            match child.tag_name().name() {
+                "schedule_entry" => {
+                    schedule.push(Self::schedule_entry_from_xml(
+                        xml_sdf,
+                        &child,
+                        &name_to_id_map,
+                    )?);
+                }
+                "schedule_end_marker" => {
+                    check_attributes(xml_sdf, &child, &[])?;
+
+                    schedule.push(DomainSchedEntry {
+                        domain: 0,
+                        duration: DomainSchedDuration::EndMarker,
+                    });
+                }
+                name => {
+                    let pos = xml_sdf.doc.text_pos_at(child.range().start);
+                    return Err(format!(
+                        "Error: invalid XML element as child of <domain_schedule> '{name}': {}",
+                        loc_string(xml_sdf, pos)
+                    ));
+                }
+            }
+        }
+
+        if schedule.len() >= config.num_domain_schedules as usize {
+            return Err(format!(
+                "More than configured KernelNumDomainSchedules {} \
+                number of <schedule_entry> elements found",
+                config.num_domain_schedules
+            ));
+        }
+
+        Ok(Domains {
+            name_to_id_map,
+            schedule_start_index: Some(schedule_start_index),
+            schedule_index_shift,
+            schedule,
+        })
+    }
+
+    fn schedule_entry_from_xml(
+        xml_sdf: &XmlSystemDescription,
+        node: &roxmltree::Node,
+        name_to_id_map: &HashMap<String, u8>,
+    ) -> Result<DomainSchedEntry, String> {
+        check_attributes(xml_sdf, node, &["domain", "duration"])?;
+
+        let domain_name = checked_lookup(xml_sdf, node, "domain")?;
+        let duration_str = checked_lookup(xml_sdf, node, "duration")?;
+
+        let &domain = name_to_id_map.get(domain_name).ok_or_else(|| {
+            value_error(
+                xml_sdf,
+                node,
+                format!("domain '{domain_name}' does not exist,"),
+            )
+        })?;
+
+        let (duration_raw, duration_unit) = duration_str.split_once(" ").ok_or_else(|| {
+            value_error(
+                xml_sdf,
+                node,
+                format!(
+                    "The duration '{duration_str}' must contain a value and a unit, e.g. '1000 us'"
+                ),
+            )
+        })?;
+
+        let duration_int = sdf_parse_number(duration_raw, node)?;
+        let duration = NonZero::new(duration_int).ok_or_else(|| {
+            value_error(
+                xml_sdf,
+                node,
+                format!("The duration '{duration_str}' must be non-zero"),
+            )
+        })?;
+
+        let duration = match duration_unit {
+            "us" => Ok(DomainSchedDuration::Us(duration)),
+            "ticks" => Ok(DomainSchedDuration::Ticks(duration)),
+            _ => Err(value_error(
+                xml_sdf,
+                node,
+                format!("The duration '{duration_str}' must be in either 'ticks' or 'us'"),
+            )),
+        }?;
+
+        Ok(DomainSchedEntry { domain, duration })
+    }
+
+    pub fn has_domains(&self) -> bool {
+        !self.name_to_id_map.is_empty()
+    }
+}
+
 struct XmlSystemDescription<'a> {
     filename: &'a Path,
     doc: &'a roxmltree::Document<'a>,
@@ -2135,6 +2407,7 @@ pub struct SystemDescription {
     pub memory_regions: Vec<SysMemoryRegion>,
     pub iomaps: Vec<SysIOMap>,
     pub channels: Vec<Channel>,
+    pub domains: Domains,
 }
 
 fn location_suffix_format(
@@ -2440,6 +2713,7 @@ pub fn parse(
     let mut iommu_domain_ids = HashSet::new();
     let mut iommu_device_identifiers = HashSet::new();
     let mut channels = vec![];
+    let mut domains = Domains::default();
     let system = doc
         .root()
         .children()
@@ -2491,6 +2765,17 @@ pub fn parse(
                     loc_string(&xml_sdf, pos)
                 ));
             }
+            "domains" => {
+                if domains.has_domains() {
+                    return Err(value_error(
+                        &xml_sdf,
+                        &child,
+                        "domains must only be specified once".to_string(),
+                    ));
+                }
+
+                domains = Domains::from_xml(config, &xml_sdf, &child)?;
+            }
             _ => {
                 let pos = xml_sdf.doc.text_pos_at(child.range().start);
                 return Err(format!(
@@ -2964,6 +3249,7 @@ pub fn parse(
         memory_regions: mrs,
         iomaps,
         channels,
+        domains,
     })
 }
 

From 069b6e4d7fc382200abbb0d318db14f9226ebcdb Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Thu, 16 Jul 2026 18:14:18 +1000
Subject: [PATCH 5/8] domains: support specifying domains for each PD

When we have a domain schedule specified, this is also
required.

Co-authored-by: Krishnan Winter <krishnan.winter@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 tool/microkit/src/capdl/builder.rs |  4 +++-
 tool/microkit/src/sdf.rs           | 36 ++++++++++++++++++++++++++----
 2 files changed, 35 insertions(+), 5 deletions(-)

diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs
index f653a2a56..b5f8b71b6 100644
--- a/tool/microkit/src/capdl/builder.rs
+++ b/tool/microkit/src/capdl/builder.rs
@@ -25,7 +25,7 @@ use crate::{
     elf::ElfFile,
     sdf::{
         CapMapType, CpuCore, IommuDeviceIdentifier, Map, SystemDescription, BUDGET_DEFAULT,
-        MONITOR_PD_NAME, MONITOR_PRIORITY,
+        MONITOR_DOMAIN, MONITOR_PD_NAME, MONITOR_PRIORITY,
     },
     sel4::{Arch, Config, PageSize},
     util::{ranges_overlap, round_down, round_up},
@@ -509,6 +509,7 @@ pub fn build_capdl_spec(
         monitor_tcb.extra.prio = MONITOR_PRIORITY;
         monitor_tcb.extra.max_prio = MONITOR_PRIORITY;
         monitor_tcb.extra.resume = true;
+        monitor_tcb.extra.domain = Some(MONITOR_DOMAIN);
 
         monitor_tcb.slots.push(capdl_util_make_cte(
             TcbBoundSlot::IpcBuffer as u32,
@@ -1102,6 +1103,7 @@ pub fn build_capdl_spec(
             pd_tcb.extra.max_prio = pd.priority();
             pd_tcb.extra.fpu_disabled = !pd.fpu;
             pd_tcb.extra.resume = true;
+            pd_tcb.extra.domain = pd.domain;
 
             pd_tcb.slots.extend(caps_to_bind_to_tcb);
             // Stylistic purposes only
diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs
index 6205ff82c..4b6edbc43 100644
--- a/tool/microkit/src/sdf.rs
+++ b/tool/microkit/src/sdf.rs
@@ -56,6 +56,7 @@ const PD_MAX_PRIORITY: u8 = 254;
 pub const BUDGET_DEFAULT: u64 = 1000;
 
 pub const MONITOR_PD_NAME: &str = "monitor";
+pub const MONITOR_DOMAIN: u8 = 0;
 
 /// Default to a stack size of 8KiB
 pub const PD_DEFAULT_STACK_SIZE: u64 = 0x2000;
@@ -612,6 +613,7 @@ pub struct ProtectionDomain {
     pub stack_size: u64,
     pub smc: bool,
     pub cpu: CpuCore,
+    pub domain: Option<u8>,
     pub program_image: PathBuf,
     pub program_image_for_symbols: Option<PathBuf>,
     /// Enable FPU for this PD.
@@ -957,6 +959,7 @@ impl ProtectionDomain {
         xml_sdf: &XmlSystemDescription,
         node: &roxmltree::Node,
         is_child: bool,
+        domains: &Domains,
     ) -> Result<ProtectionDomain, String> {
         let mut attrs = vec![
             "name",
@@ -969,6 +972,7 @@ impl ProtectionDomain {
             // but we do the error-checking further down.
             "smc",
             "cpu",
+            "domain",
             "fpu",
         ];
         if is_child {
@@ -1075,6 +1079,28 @@ impl ProtectionDomain {
             ));
         }
 
+        let domain = if domains.has_domains() {
+            let domain_s = checked_lookup(xml_sdf, node, "domain")?;
+            Some(*domains.name_to_id_map.get(domain_s).ok_or_else(|| {
+                value_error(
+                    xml_sdf,
+                    node,
+                    format!("domain '{domain_s}' not declared in <domains>:"),
+                )
+            })?)
+        } else {
+            if let Some(name) = node.attribute("domain") {
+                return Err(value_error(
+                    xml_sdf,
+                    node,
+                    format!("Specifying a domain '{name}' without declaring a \
+                             domain schedule is not allowed:"),
+                ));
+            }
+
+            None
+        };
+
         #[allow(clippy::manual_range_contains)]
         if stack_size < PD_MIN_STACK_SIZE || stack_size > PD_MAX_STACK_SIZE {
             return Err(value_error(
@@ -1493,7 +1519,8 @@ impl ProtectionDomain {
                     checked_add_setvar(&mut setvars, setvar, xml_sdf, &child)?;
                 }
                 "protection_domain" => {
-                    let child_pd = ProtectionDomain::from_xml(config, xml_sdf, &child, true)?;
+                    let child_pd =
+                        ProtectionDomain::from_xml(config, xml_sdf, &child, true, domains)?;
 
                     if let Some(setvar_id) = &child_pd.setvar_id {
                         let setvar = SysSetVar {
@@ -1581,6 +1608,7 @@ impl ProtectionDomain {
             stack_size,
             smc,
             cpu,
+            domain,
             program_image: program_image.unwrap(),
             program_image_for_symbols,
             fpu,
@@ -2735,9 +2763,9 @@ pub fn parse(
 
         let child_name = child.tag_name().name();
         match child_name {
-            "protection_domain" => {
-                root_pds.push(ProtectionDomain::from_xml(config, &xml_sdf, &child, false)?)
-            }
+            "protection_domain" => root_pds.push(ProtectionDomain::from_xml(
+                config, &xml_sdf, &child, false, &domains,
+            )?),
             "channel" => channel_nodes.push(child),
             "memory_region" => mrs.push(SysMemoryRegion::from_xml(
                 config,

From e8c65e3036804c82c045e25f52c8f0b36e9bf948 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Thu, 16 Jul 2026 15:32:56 +1000
Subject: [PATCH 6/8] domains: add basic example

This is equivalent to the CAmkES domains example which
has an emitter and collector.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 build_sdk.py                   |  1 +
 example/domains/Makefile       | 72 ++++++++++++++++++++++++++++++
 example/domains/README.md      | 81 ++++++++++++++++++++++++++++++++++
 example/domains/collector.c    | 17 +++++++
 example/domains/domains.system | 45 +++++++++++++++++++
 example/domains/emitter.c      | 27 ++++++++++++
 6 files changed, 243 insertions(+)
 create mode 100644 example/domains/Makefile
 create mode 100644 example/domains/README.md
 create mode 100644 example/domains/collector.c
 create mode 100644 example/domains/domains.system
 create mode 100644 example/domains/emitter.c

diff --git a/build_sdk.py b/build_sdk.py
index 8a3056908..de6af64c9 100644
--- a/build_sdk.py
+++ b/build_sdk.py
@@ -519,6 +519,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"),
diff --git a/example/domains/Makefile b/example/domains/Makefile
new file mode 100644
index 000000000..d0b1a671f
--- /dev/null
+++ b/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)
diff --git a/example/domains/README.md b/example/domains/README.md
new file mode 100644
index 000000000..98035835b
--- /dev/null
+++ b/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.
diff --git a/example/domains/collector.c b/example/domains/collector.c
new file mode 100644
index 000000000..a8a6dd82c
--- /dev/null
+++ b/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");
+}
diff --git a/example/domains/domains.system b/example/domains/domains.system
new file mode 100644
index 000000000..6f486e346
--- /dev/null
+++ b/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>
diff --git a/example/domains/emitter.c b/example/domains/emitter.c
new file mode 100644
index 000000000..d2d0e927f
--- /dev/null
+++ b/example/domains/emitter.c
@@ -0,0 +1,27 @@
+/*
+ * Copyright 2026, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stdint.h>
+#include <microkit.h>
+
+void init(void)
+{
+    int i;
+
+    microkit_dbg_puts("emitter: starting to emit events...\n");
+    i = 0;
+    while (i < 100000) {
+        i++;
+        microkit_notify(0);
+
+        if (i % 10000 == 0) {
+            microkit_dbg_puts("emitter: still emitting events...\n");
+        }
+    }
+
+    microkit_dbg_puts("emitter: done emitting events\n");
+}
+
+void notified(microkit_channel ch) { }

From d452725ab6ee21c73e7ff25aa7f306a7b281ee74 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Fri, 17 Jul 2026 11:18:05 +1000
Subject: [PATCH 7/8] domains: add tests for errors cases

Mostly just error cases :)

Plus some extra cases in the code.

Co-authored-by: Krishnan Winter <krishnan.winter@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 tool/microkit/src/sdf.rs                      |  43 +++++++-
 .../domain_assign_pd_to_invalid_domain.system |  19 ++++
 .../sdf/domain_exceed_max_domains.system      |  36 ++++++
 .../tests/sdf/domain_invalid_shift.system     |  19 ++++
 .../sdf/domain_invalid_start_index.system     |  19 ++++
 .../tests/sdf/domain_invalid_timeslice.system |  19 ++++
 .../tests/sdf/domain_no_pd_domain.system      |  18 +++
 .../tests/sdf/domain_no_schedule.system       |  11 ++
 .../sdf/domain_out_of_bounds_shift.system     |  19 ++++
 .../domain_out_of_bounds_start_index.system   |  19 ++++
 tool/microkit/tests/sdf/domain_smp.system     |  19 ++++
 tool/microkit/tests/test.rs                   | 103 ++++++++++++++++++
 12 files changed, 341 insertions(+), 3 deletions(-)
 create mode 100644 tool/microkit/tests/sdf/domain_assign_pd_to_invalid_domain.system
 create mode 100644 tool/microkit/tests/sdf/domain_exceed_max_domains.system
 create mode 100644 tool/microkit/tests/sdf/domain_invalid_shift.system
 create mode 100644 tool/microkit/tests/sdf/domain_invalid_start_index.system
 create mode 100644 tool/microkit/tests/sdf/domain_invalid_timeslice.system
 create mode 100644 tool/microkit/tests/sdf/domain_no_pd_domain.system
 create mode 100644 tool/microkit/tests/sdf/domain_no_schedule.system
 create mode 100644 tool/microkit/tests/sdf/domain_out_of_bounds_shift.system
 create mode 100644 tool/microkit/tests/sdf/domain_out_of_bounds_start_index.system
 create mode 100644 tool/microkit/tests/sdf/domain_smp.system

diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs
index 4b6edbc43..7750cb6bf 100644
--- a/tool/microkit/src/sdf.rs
+++ b/tool/microkit/src/sdf.rs
@@ -1093,8 +1093,10 @@ impl ProtectionDomain {
                 return Err(value_error(
                     xml_sdf,
                     node,
-                    format!("Specifying a domain '{name}' without declaring a \
-                             domain schedule is not allowed:"),
+                    format!(
+                        "Specifying a domain '{name}' without declaring a \
+                             domain schedule is not allowed:"
+                    ),
                 ));
             }
 
@@ -2171,6 +2173,13 @@ impl Domains {
     ) -> Result<Self, String> {
         check_attributes(xml_sdf, node, &[])?;
 
+        if config.num_cores != 1 {
+            return Err(
+                "Error: The domain scheduler is not supported in multicore builds of seL4"
+                    .to_string(),
+            );
+        }
+
         let mut name_to_id_map = HashMap::<String, Option<u8>>::new();
         let mut id_to_name_map = HashMap::<u8, String>::new();
         let mut domain_schedule_element = None;
@@ -2353,7 +2362,7 @@ impl Domains {
             }
         }
 
-        if schedule.len() >= config.num_domain_schedules as usize {
+        if schedule.len() >= config.num_domain_schedules.try_into().unwrap() {
             return Err(format!(
                 "More than configured KernelNumDomainSchedules {} \
                 number of <schedule_entry> elements found",
@@ -2361,6 +2370,34 @@ impl Domains {
             ));
         }
 
+        if schedule_start_index >= schedule.len().try_into().unwrap() {
+            return Err(value_error(
+                xml_sdf,
+                node,
+                format!(
+                    "schedule_start_index '{schedule_start_index}' is \
+                     greater than the length of the schedule '{}'",
+                    schedule.len()
+                ),
+            ));
+        }
+
+        if let Some(shift) = schedule_index_shift {
+            if shift + u64::try_from(schedule.len()).unwrap() >= config.num_domain_schedules {
+                return Err(value_error(
+                    xml_sdf,
+                    node,
+                    format!(
+                        "schedule_index_shift '{schedule_start_index}' on top of \
+                         the schedule length '{}' would exceed than the configured \
+                         KernelNumDomainSchedules {}",
+                        schedule.len(),
+                        config.num_domain_schedules
+                    ),
+                ));
+            }
+        }
+
         Ok(Domains {
             name_to_id_map,
             schedule_start_index: Some(schedule_start_index),
diff --git a/tool/microkit/tests/sdf/domain_assign_pd_to_invalid_domain.system b/tool/microkit/tests/sdf/domain_assign_pd_to_invalid_domain.system
new file mode 100644
index 000000000..6dbf6ccd8
--- /dev/null
+++ b/tool/microkit/tests/sdf/domain_assign_pd_to_invalid_domain.system
@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <domains>
+        <domain name="domain_1" />
+
+        <domain_schedule>
+            <schedule_entry domain="domain_1" duration="1000 us" />
+        </domain_schedule>
+    </domains>
+
+    <protection_domain name="test1" domain="domain_2">
+        <program_image path="test" />
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/domain_exceed_max_domains.system b/tool/microkit/tests/sdf/domain_exceed_max_domains.system
new file mode 100644
index 000000000..f8edf0d0c
--- /dev/null
+++ b/tool/microkit/tests/sdf/domain_exceed_max_domains.system
@@ -0,0 +1,36 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <domains>
+        <domain name="domain_1" />
+        <domain name="domain_2" />
+        <domain name="domain_3" />
+        <domain name="domain_4" />
+        <domain name="domain_5" />
+        <domain name="domain_6" />
+        <domain name="domain_7" />
+        <domain name="domain_8" />
+        <domain name="domain_9" />
+        <domain name="domain_10" />
+        <domain name="domain_12" />
+        <domain name="domain_13" />
+        <domain name="domain_14" />
+        <domain name="domain_15" />
+        <domain name="domain_16" />
+        <domain name="domain_17" />
+        <domain name="domain_18" />
+        <domain name="domain_19" />
+
+        <domain_schedule>
+            <schedule_entry domain="domain_1" duration="1000 us" />
+        </domain_schedule>
+    </domains>
+
+    <protection_domain name="test1" domain="domain_1">
+        <program_image path="test" />
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/domain_invalid_shift.system b/tool/microkit/tests/sdf/domain_invalid_shift.system
new file mode 100644
index 000000000..789f559a5
--- /dev/null
+++ b/tool/microkit/tests/sdf/domain_invalid_shift.system
@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <domains>
+        <domain name="domain_1" />
+
+        <domain_schedule index_shift="zzzz">
+            <schedule_entry domain="domain_1" duration="1000 us" />
+        </domain_schedule>
+    </domains>
+
+    <protection_domain name="test1" domain="domain_1">
+        <program_image path="test" />
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/domain_invalid_start_index.system b/tool/microkit/tests/sdf/domain_invalid_start_index.system
new file mode 100644
index 000000000..3569fe767
--- /dev/null
+++ b/tool/microkit/tests/sdf/domain_invalid_start_index.system
@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <domains>
+        <domain name="domain_1" />
+
+        <domain_schedule start_index="zzzz">
+            <schedule_entry domain="domain_1" duration="1000 us" />
+        </domain_schedule>
+    </domains>
+
+    <protection_domain name="test1" domain="domain_1">
+        <program_image path="test" />
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/domain_invalid_timeslice.system b/tool/microkit/tests/sdf/domain_invalid_timeslice.system
new file mode 100644
index 000000000..284679e86
--- /dev/null
+++ b/tool/microkit/tests/sdf/domain_invalid_timeslice.system
@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <domains>
+        <domain name="domain_1" />
+
+        <domain_schedule>
+            <schedule_entry domain="domain_1" duration="1000 kilometres" />
+        </domain_schedule>
+    </domains>
+
+    <protection_domain name="test1" domain="domain_1">
+        <program_image path="test" />
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/domain_no_pd_domain.system b/tool/microkit/tests/sdf/domain_no_pd_domain.system
new file mode 100644
index 000000000..8af63abbd
--- /dev/null
+++ b/tool/microkit/tests/sdf/domain_no_pd_domain.system
@@ -0,0 +1,18 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <domains>
+        <domain name="domain_1" />
+        <domain_schedule>
+            <schedule_entry domain="domain_1" duration="1000 us" />
+        </domain_schedule>
+    </domains>
+
+    <protection_domain name="test1" >
+        <program_image path="test" />
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/domain_no_schedule.system b/tool/microkit/tests/sdf/domain_no_schedule.system
new file mode 100644
index 000000000..694073a72
--- /dev/null
+++ b/tool/microkit/tests/sdf/domain_no_schedule.system
@@ -0,0 +1,11 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="test1" domain="domain_1">
+        <program_image path="test" />
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/domain_out_of_bounds_shift.system b/tool/microkit/tests/sdf/domain_out_of_bounds_shift.system
new file mode 100644
index 000000000..fc7cbea0b
--- /dev/null
+++ b/tool/microkit/tests/sdf/domain_out_of_bounds_shift.system
@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <domains>
+        <domain name="domain_1" />
+
+        <domain_schedule index_shift="1000">
+            <schedule_entry domain="domain_1" duration="1000 us" />
+        </domain_schedule>
+    </domains>
+
+    <protection_domain name="test1" domain="domain_1">
+        <program_image path="test" />
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/domain_out_of_bounds_start_index.system b/tool/microkit/tests/sdf/domain_out_of_bounds_start_index.system
new file mode 100644
index 000000000..1f862c72e
--- /dev/null
+++ b/tool/microkit/tests/sdf/domain_out_of_bounds_start_index.system
@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <domains>
+        <domain name="domain_1" />
+
+        <domain_schedule start_index="1">
+            <schedule_entry domain="domain_1" duration="1000 us" />
+        </domain_schedule>
+    </domains>
+
+    <protection_domain name="test1" domain="domain_1">
+        <program_image path="test" />
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/domain_smp.system b/tool/microkit/tests/sdf/domain_smp.system
new file mode 100644
index 000000000..43fd59edf
--- /dev/null
+++ b/tool/microkit/tests/sdf/domain_smp.system
@@ -0,0 +1,19 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <domains>
+        <domain name="domain_1" />
+
+        <domain_schedule>
+            <schedule_entry domain="domain_1" duration="1000 us" />
+        </domain_schedule>
+    </domains>
+
+    <protection_domain name="test1" domain="domain_1">
+        <program_image path="test" />
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs
index 3e46377da..96e9d11f7 100644
--- a/tool/microkit/tests/test.rs
+++ b/tool/microkit/tests/test.rs
@@ -59,6 +59,11 @@ const DEFAULT_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config {
     },
 };
 
+const SMP_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config {
+    num_cores: 4,
+    ..DEFAULT_AARCH64_KERNEL_CONFIG
+};
+
 const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config {
     arch: sel4::Arch::X86_64,
     word_size: 64,
@@ -1227,6 +1232,104 @@ mod channel {
     }
 }
 
+#[cfg(test)]
+mod domains {
+    use super::*;
+
+    #[test]
+    fn test_domain_smp() {
+        check_error(
+            &SMP_AARCH64_KERNEL_CONFIG,
+            "domain_smp.system",
+            "Error: The domain scheduler is not supported in multicore builds of seL4",
+        )
+    }
+
+    #[test]
+    fn test_domain_too_many_domains() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "domain_exceed_max_domains.system",
+            "Error: Number of domains exceeds 16 on element 'domains': domain_exceed_max_domains.system:8:5",
+        )
+    }
+
+    #[test]
+    fn test_domain_assign_pd_to_invalid_domain() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "domain_assign_pd_to_invalid_domain.system",
+            "Error: domain 'domain_2' not declared in <domains>: on element 'protection_domain': domain_assign_pd_to_invalid_domain.system:16:5",
+        )
+    }
+
+    #[test]
+    fn test_domain_invalid_timeslice() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "domain_invalid_timeslice.system",
+            "Error: The duration '1000 kilometres' must be in either 'ticks' or 'us' on element 'schedule_entry': domain_invalid_timeslice.system:12:13"
+        )
+    }
+
+    #[test]
+    fn test_domain_no_schedule() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "domain_no_schedule.system",
+            "Error: Specifying a domain 'domain_1' without declaring a domain schedule is not allowed: on element 'protection_domain': domain_no_schedule.system:8:5",
+        )
+    }
+
+    #[test]
+    fn test_domain_pd_no_domain() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "domain_no_pd_domain.system",
+            "Error: Missing required attribute 'domain' on element 'protection_domain': domain_no_pd_domain.system:15:5",
+        )
+    }
+
+    #[test]
+    fn test_domain_invalid_start_index() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "domain_invalid_start_index.system",
+            "Error: failed to parse integer 'zzzz' on element 'domain_schedule': invalid digit found in string",
+        )
+    }
+
+    #[test]
+    fn test_domain_out_of_bounds_start_index() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "domain_out_of_bounds_start_index.system",
+            "Error: schedule_start_index '1' is greater than the length of the schedule '1' \
+             on element 'domain_schedule': domain_out_of_bounds_start_index.system:11:9",
+        )
+    }
+
+    #[test]
+    fn test_domain_invalid_shift() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "domain_invalid_shift.system",
+            "Error: failed to parse integer 'zzzz' on element 'domain_schedule': invalid digit found in string",
+        )
+    }
+
+    #[test]
+    fn test_domain_out_of_bounds_shift() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "domain_out_of_bounds_shift.system",
+            "Error: schedule_index_shift '0' on top of the schedule length '1' would \
+             exceed than the configured KernelNumDomainSchedules 100 \
+             on element 'domain_schedule': domain_out_of_bounds_shift.system:11:9",
+        )
+    }
+}
+
 #[cfg(test)]
 mod system {
     use super::*;

From 54c94761e9458b7aa1a2d7b1a95f9504f532940c Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Fri, 17 Jul 2026 13:07:44 +1000
Subject: [PATCH 8/8] domains: document the feature in the manual

We describe the syntax and the reference separately.

Co-authored-by: Krishnan Winter <krishnan.winter@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 build_sdk.py   |  1 +
 docs/manual.md | 82 ++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 83 insertions(+)

diff --git a/build_sdk.py b/build_sdk.py
index de6af64c9..3ae49ac25 100644
--- a/build_sdk.py
+++ b/build_sdk.py
@@ -62,6 +62,7 @@
     # 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,
diff --git a/docs/manual.md b/docs/manual.md
index 914c3f024..ce25ff3a7 100644
--- a/docs/manual.md
+++ b/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.