From 2bc9d0f67e925d35f561fa777ca77d1275aec066 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Fri, 20 Mar 2026 16:24:43 +1100 Subject: [PATCH 01/21] Add experimental run-time domain scheduler support Signed-off-by: Krishnan Winter --- build_sdk.py | 23 +++++ tool/microkit/src/capdl/builder.rs | 29 +++++- tool/microkit/src/capdl/packaging.rs | 4 +- tool/microkit/src/capdl/spec.rs | 1 + tool/microkit/src/main.rs | 1 + tool/microkit/src/sdf.rs | 130 ++++++++++++++++++++++++++- tool/microkit/src/sel4.rs | 8 ++ tool/microkit/tests/test.rs | 2 + 8 files changed, 192 insertions(+), 6 deletions(-) diff --git a/build_sdk.py b/build_sdk.py index ac8cd1b77..7e7bb8c60 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -465,6 +465,29 @@ class KernelPath: } }, ), + # TODO: This is experimental for now, do this in a better way + ConfigInfo( + name="release_domains", + debug=False, + kernel_options={ + "KernelNumDomains": 256, + "KernelNumDomainSchedules": 256, + }, + kernel_options_arch={}, + ), + ConfigInfo( + name="debug_domains", + debug=True, + kernel_options={ + "KernelDebugBuild": True, + "KernelPrinting": True, + "KernelVerificationBuild": False, + "KernelNumDomains": 256, + "KernelNumDomainSchedules": 256, + }, + kernel_options_arch={}, + ), + ) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 4173a2feb..45e6c6ce9 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -12,7 +12,7 @@ use std::{ use sel4_capdl_initializer_types::{ object, CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId, Spec, - Word, + Word, DomainSchedEntry, }; use crate::{ @@ -130,6 +130,7 @@ impl CapDLSpecContainer { spec: Spec { objects: Vec::new(), irqs: Vec::new(), + domain_schedule: None, asid_slots: Vec::new(), root_objects: Range { start: 0.into(), @@ -322,6 +323,7 @@ impl CapDLSpecContainer { prio: 0, max_prio: 0, resume: false, + domain: 0, ip: entry_point.into(), sp: 0.into(), gprs: Vec::new(), @@ -485,6 +487,9 @@ pub fn build_capdl_spec( monitor_tcb.extra.max_prio = MONITOR_PRIORITY; monitor_tcb.extra.resume = true; + // @kwinter: What domain should the monitor be in? + monitor_tcb.extra.domain = 0; + monitor_tcb.slots.push(capdl_util_make_cte( TcbBoundSlot::CSpace as u32, mon_cnode_cap, @@ -904,6 +909,7 @@ pub fn build_capdl_spec( )); // Finally create TCB, unlike PDs, VMs are suspended by default until resume'd by their parent. + // @kwinter: Is it fair to assign the VM the same domain as the parent? let vm_vcpu_tcb_inner_obj = object::Tcb { slots: caps_to_bind_to_vm_tcbs, extra: Box::new(object::TcbExtraInfo { @@ -912,6 +918,7 @@ pub fn build_capdl_spec( prio: virtual_machine.priority, max_prio: virtual_machine.priority, resume: false, + domain: pd.domain_id.expect("No domain ID specified for vm"), // VMs do not have program images associated with them so these are always zero. ip: Word(0), sp: Word(0), @@ -980,6 +987,7 @@ pub fn build_capdl_spec( pd_tcb.extra.prio = pd.priority; pd_tcb.extra.max_prio = pd.priority; pd_tcb.extra.resume = true; + pd_tcb.extra.domain = pd.domain_id.expect("No domain ID specified for PD"); pd_tcb.slots.extend(caps_to_bind_to_tcb); // Stylistic purposes only @@ -1079,7 +1087,24 @@ pub fn build_capdl_spec( } // ********************************* - // Step 5. Sort the root objects + // Step 5. Pass domain schedule + // ********************************* + + if system.domain_schedule.is_some() { + let mut domain_schedule: Vec = Vec::new(); + + for sched_entry in system.domain_schedule.as_ref().unwrap().schedule.iter() { + domain_schedule.push(DomainSchedEntry{ + id: sched_entry.id, + time: sched_entry.length, + }) + } + + spec_container.spec.domain_schedule = Some(domain_schedule); + } + + // ********************************* + // Step 6. 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. diff --git a/tool/microkit/src/capdl/packaging.rs b/tool/microkit/src/capdl/packaging.rs index 5a18ad248..ab1e65547 100644 --- a/tool/microkit/src/capdl/packaging.rs +++ b/tool/microkit/src/capdl/packaging.rs @@ -38,9 +38,9 @@ pub fn pack_spec_into_initial_task( for named_obj in output_spec.objects.iter_mut() { match build_config { - "smp-debug" | "debug" => {} + "smp-debug" | "debug" | "debug_domains" => {} // We don't copy over the object names as there is no debug printing in these configuration to save memory. - "release" | "benchmark" | "smp-release" | "smp-benchmark" => named_obj.name = None, + "release" | "release_domains" | "benchmark" | "smp-release" | "smp-benchmark" => named_obj.name = None, _ => panic!("unknown configuration {build_config}"), }; } diff --git a/tool/microkit/src/capdl/spec.rs b/tool/microkit/src/capdl/spec.rs index 8d9bca61c..a78d1c377 100644 --- a/tool/microkit/src/capdl/spec.rs +++ b/tool/microkit/src/capdl/spec.rs @@ -74,6 +74,7 @@ pub fn capdl_obj_human_name(obj: &Object, sel4_config: &Config) -> &' Object::ArmSmc => "ARM SMC", Object::Untyped(_) => "Untyped", Object::Irq(_) => "IRQ", + Object::DomainSet => "Domain Set", } } diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index ae6a188ef..f0a86e563 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -538,6 +538,7 @@ fn main() -> Result<(), String> { invocations_labels, device_regions, normal_regions, + num_domain_schedules: json_str_as_u64(&kernel_config_json, "ROOT_CNODE_SIZE_BITS")?, }; if kernel_config.arch != Arch::X86_64 && !loader_elf_path.exists() { diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index e8093b7e1..cbbd3f0de 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -22,6 +22,7 @@ use crate::sel4::{ use crate::util::{ranges_overlap, str_to_bool}; use crate::MAX_PDS; use std::collections::HashSet; +use std::collections::HashMap; use std::fmt::Display; use std::path::{Path, PathBuf}; @@ -273,6 +274,20 @@ pub struct ProtectionDomain { pub setvar_id: Option, /// Location in the parsed SDF file text_pos: Option, + /// Index into the domain schedule vector if the system is using domain scheduling + pub domain_id: Option, +} + +#[derive(Debug, PartialEq, Eq, Hash, Copy, Clone)] +pub struct DomainTimeslice { + pub id: u8, + pub length: u64, +} + +#[derive(Debug, PartialEq, Eq)] +pub struct DomainSchedule { + pub domain_ids: HashMap, + pub schedule: Vec, } #[derive(Debug, PartialEq, Eq)] @@ -444,6 +459,7 @@ impl ProtectionDomain { xml_sdf: &XmlSystemDescription, node: &roxmltree::Node, is_child: bool, + domain_schedule: &Option, ) -> Result { let mut attrs = vec![ "name", @@ -455,6 +471,7 @@ impl ProtectionDomain { // The SMC field is only available in certain configurations // but we do the error-checking further down. "smc", + "domain", "cpu", ]; if is_child { @@ -583,6 +600,27 @@ impl ProtectionDomain { )); } + let mut domain_id = None; + match (domain_schedule, checked_lookup(xml_sdf, node, "domain")) { + (Some(domain_schedule), Ok(domain_name)) => { + domain_id = domain_schedule.domain_ids.get(domain_name); + if domain_id.is_none() { + return Err(format!("Protection domain {} specifies a domain {} that is not in the domain schedule", name, domain_name)); + } + } + (Some(_), _) => { + return Err(format!("System specifies a domain schedule but protection domain {} does not specify a domain", name)) + } + (_, Ok(domain)) => { + if config.num_domain_schedules > 1 { + return Err(format!("Protection domain {} specifies a domain {} but system does not specify a domain schedule", name, domain)); + } else { + return Err("Assigning PDs to domains is only supported if SDK is built with --experimental-domain-support".to_string()); + } + } + (_, _) => {} + } + let mut maps = Vec::new(); let mut irqs = Vec::new(); let mut ioports = Vec::new(); @@ -987,7 +1025,7 @@ 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, domain_schedule)?; if let Some(setvar_id) = &child_pd.setvar_id { let setvar = SysSetVar { @@ -1073,6 +1111,76 @@ impl ProtectionDomain { parent: None, setvar_id, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), + domain_id: domain_id.copied(), + }) + } +} + +impl DomainSchedule { + fn from_xml( + xml_sdf: &XmlSystemDescription, + config: &Config, + node: &roxmltree::Node, + ) -> Result { + let pos = xml_sdf.doc.text_pos_at(node.range().start); + + check_attributes(xml_sdf, node, &[])?; + + let mut next_domain_id = 0; + let mut domain_ids = HashMap::new(); + let mut schedule = Vec::new(); + for child in node.children() { + if !child.is_element() { + continue; + } + + let child_name = child.tag_name().name(); + if child_name != "domain" { + return Err(format!( + "Error: invalid XML element '{}': {}", + child_name, + loc_string(xml_sdf, pos) + )); + } + + if schedule.len() == config.num_domain_schedules as usize { + return Err(format!( + "Error: length of domain schedule exceeds maximum of {}: {}", + config.num_domain_schedules as usize, + loc_string(xml_sdf, pos) + )); + } + + check_attributes(xml_sdf, &child, &["name", "length"])?; + let name = checked_lookup(xml_sdf, &child, "name")?; + let length = checked_lookup(xml_sdf, &child, "length")?.parse::(); + if length.is_err() { + return Err(format!( + "Error: invalid domain timeslice length '{}': {}", + name, + loc_string(xml_sdf, pos) + )); + } + + let id = match domain_ids.get(name) { + Some(&id) => id, + None => { + let id = next_domain_id; + next_domain_id += 1; + domain_ids.insert(name.to_string(), id); + id + } + }; + + schedule.push(DomainTimeslice { + id, + length: length.unwrap(), + }); + } + + Ok(DomainSchedule { + domain_ids, + schedule, }) } } @@ -1391,6 +1499,7 @@ pub struct SystemDescription { pub protection_domains: Vec, pub memory_regions: Vec, pub channels: Vec, + pub domain_schedule: Option, } fn check_maps( @@ -1616,6 +1725,7 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Result { - root_pds.push(ProtectionDomain::from_xml(config, &xml_sdf, &child, false)?) + root_pds.push(ProtectionDomain::from_xml(config, &xml_sdf, &child, false, &domain_schedule)?) } "channel" => channel_nodes.push(child), "memory_region" => mrs.push(SysMemoryRegion::from_xml(config, &xml_sdf, &child)?), @@ -1652,6 +1762,21 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result { + if config.num_domain_schedules > 1 { + println!("NUM DOMAINS IS GREATER THAN 1: {}", config.num_domain_schedules); + if let Some(domain_schedule_node) = system + .children() + .filter(|&child| child.is_element()) + .find(|&child| child.tag_name().name() == "domain_schedule") + { + println!("Doing the domain schedule!\n"); + domain_schedule = Some(DomainSchedule::from_xml(&xml_sdf, &config, &domain_schedule_node)?); + } + } else { + println!("NUM DOMAINS SCHEDULE IS 1 OR NONE"); + } } _ => { let pos = xml_sdf.doc.text_pos_at(child.range().start); @@ -2015,6 +2140,7 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result>, pub normal_regions: Option>, + /// Flag to enable experimental domain scheduler support + pub num_domain_schedules: u64, } impl Config { diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 02263798c..956b112d0 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -32,6 +32,7 @@ const DEFAULT_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config { invocations_labels: json!(null), device_regions: None, normal_regions: None, + num_domain_schedules: 1, }; const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config { @@ -56,6 +57,7 @@ const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config { invocations_labels: json!(null), device_regions: None, normal_regions: None, + num_domain_schedules: 1, }; fn check_success(kernel_config: &sel4::Config, test_name: &str) { From 937ea6e61783469f5d945a771bde438807e7614f Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Wed, 11 Mar 2026 13:29:06 +1100 Subject: [PATCH 02/21] domains: Convert milliseconds to kernel ticks Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 8 ++++++-- tool/microkit/src/main.rs | 6 ++++++ tool/microkit/src/sdf.rs | 2 -- tool/microkit/src/sel4.rs | 2 ++ tool/microkit/tests/test.rs | 2 ++ 5 files changed, 16 insertions(+), 4 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 45e6c6ce9..95dcc2d57 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -1090,13 +1090,17 @@ pub fn build_capdl_spec( // Step 5. Pass domain schedule // ********************************* + + if system.domain_schedule.is_some() { let mut domain_schedule: Vec = Vec::new(); - + // We need to convert from the milliseconds that the user defines in the + // sdf to the kernel scheduler ticks. + let ticks_in_ms = kernel_config.timer_freq.unwrap() / 1000; for sched_entry in system.domain_schedule.as_ref().unwrap().schedule.iter() { domain_schedule.push(DomainSchedEntry{ id: sched_entry.id, - time: sched_entry.length, + time: sched_entry.length * ticks_in_ms, }) } diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index f0a86e563..a28a9130d 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -502,6 +502,11 @@ fn main() -> Result<(), String> { _ => None, }; + let timer_freq = match arch { + Arch::Aarch64 => Some(json_str_as_u64(&kernel_config_json, "TIMER_FREQUENCY")? as u64), + _ => None, + }; + let kernel_frame_size = match arch { Arch::Aarch64 => 1 << 12, Arch::Riscv64 => 1 << 21, @@ -531,6 +536,7 @@ fn main() -> Result<(), String> { 1 }, fpu: json_str_as_bool(&kernel_config_json, "HAVE_FPU")?, + timer_freq, arm_pa_size_bits, arm_smc, riscv_pt_levels: Some(RiscvVirtualMemory::Sv39), diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index cbbd3f0de..36af6ee57 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -1765,13 +1765,11 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result { if config.num_domain_schedules > 1 { - println!("NUM DOMAINS IS GREATER THAN 1: {}", config.num_domain_schedules); if let Some(domain_schedule_node) = system .children() .filter(|&child| child.is_element()) .find(|&child| child.tag_name().name() == "domain_schedule") { - println!("Doing the domain schedule!\n"); domain_schedule = Some(DomainSchedule::from_xml(&xml_sdf, &config, &domain_schedule_node)?); } } else { diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index d9212fe73..9a9a69d87 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -281,6 +281,8 @@ pub struct Config { pub benchmark: bool, pub num_cores: u8, pub fpu: bool, + /// Not used on x86 configs as timer freq is not defined + pub timer_freq: Option, /// ARM-specific, number of physical address bits pub arm_pa_size_bits: Option, /// ARM-specific, where or not SMC forwarding is allowed diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 956b112d0..90f634208 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -24,6 +24,7 @@ const DEFAULT_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config { benchmark: false, num_cores: 1, fpu: true, + timer_freq: None, arm_pa_size_bits: Some(40), arm_smc: None, riscv_pt_levels: None, @@ -49,6 +50,7 @@ const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config { benchmark: false, num_cores: 1, fpu: true, + timer_freq: None, arm_pa_size_bits: None, arm_smc: None, riscv_pt_levels: None, From 0aab2bc92eea8dd2ab6f44bc4df04ed0ffd846ba Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Mon, 9 Mar 2026 15:22:47 +1100 Subject: [PATCH 03/21] domains: Add docs Signed-off-by: Krishnan Winter --- docs/manual.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/docs/manual.md b/docs/manual.md index 462d5a0d0..c3231eb26 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -109,6 +109,7 @@ This document attempts to clearly describe all of these terms, however as the co * [interrupt](#irq) * [fault](#fault) * [ioport](#ioport) +* [domain scheduling](#domain) ## System {#system} @@ -186,6 +187,10 @@ Runnable PDs of the same priority are scheduled in a round-robin manner. **Passive** determines whether the PD is passive. A passive PD will have its scheduling context revoked after initialisation and then bound instead to the PD's notification object. This means the PD will be scheduled on receiving a notification, whereby it will run on the notification's scheduling context. When the PD receives a *protected procedure* by another PD or a *fault* caused by a child PD, the passive PD will run on the scheduling context of the callee. +#### Domain scheduling (experimental) + +If the SDK is built with a domain support config, the PD can be assigned to a scheduling **domain** in the system description. If a PD is assigned to a domain, then the PD will only be allowed to execute when that domain is active. Which domain is active at any given point in time is determined by the [domain schedule](#domain). + ## Virtual Machines {#vm} A *virtual machine* (VM) is a runtime abstraction for running guest operating systems in Microkit. It is similar @@ -346,6 +351,10 @@ delivered to another PD, the fault being handled depends on when the parent PD i I/O ports are x86 mechanisms to access certain physical devices (e.g. PC serial ports or PCI) using the `in` and `out` CPU instructions. The system description specifies if a protection domain have access to certain port address ranges. These accesses will be executed by seL4 and the result returned to protection domains. +# Domain Scheduling (experimental) {#domain} + +Microkit can be built with experimental support for a method of temporally isolating different groups of PDs called domain scheduling. On a Microkit system, only one domain is active at a time, and the kernel alternates between domains according to a round-robin schedule. A domain schedule consists of an ordered list of domains, each with an associated length of time to run. The kernel will then activate a domain for the specified length of time; after that time has passed, it will deactivate that domain and activate the next domain for its length of time, and so on, proceeding through the list until it wraps back to the first domain. PDs are assigned to domains, such that when a certain domain is active, only PDs belonging to that domain will be scheduled to run. + # SDK {#sdk} Microkit is distributed as a software development kit (SDK). @@ -984,6 +993,7 @@ Within the `system` root element the following child elements are supported: * `protection_domain` * `memory_region` * `channel` +* `domain_schedule` (If using one of the domain configs) ## `protection_domain` @@ -1000,6 +1010,7 @@ It supports the following attributes: Must be be between 4KiB and 16MiB and be 4K page-aligned. Defaults to 8KiB. * `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. +* `domain`: (optional, experimental) Specifies the name of the scheduling domain the PD belongs to. Additionally, it supports the following child elements: @@ -1135,6 +1146,19 @@ The `end` element has the following attributes: The `id` is passed to the PD in the `notified` and `protected` entry points. The `id` should be passed to the `microkit_notify` and `microkit_ppcall` functions. +## `domain_schedule` (experimental) + +The `domain_schedule` element has has a list of up to 256 `domain` child elements. Each child specifies a particular timeslice in the domain schedule and the order of the child elements specifies the order in which the timeslices will be scheduled. A domain may be named more than once in the schedule, in which case the domain will have multiple timeslices in the schedule. + +The `domain` element has the following attributes: + +* `name`: Name of the domain. +* `length`: Length of time the domain will run each time it is active, in milliseconds. + +The `name` attribute of each `domain` element can be referenced in the `domain` attribute of a `protection_domain` element. + +The `domain_schedule` element is only valid if the using one of the domain configs (`release_domains`, `debug_domains`). + # Board Support Packages {#bsps} This chapter describes the board support packages that are available in the SDK. From 76f63cd51454803c13d934d492bd90e82b3b4f42 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Mon, 9 Mar 2026 15:51:34 +1100 Subject: [PATCH 04/21] domains: Update rust-sel4 branch Signed-off-by: Krishnan Winter --- Cargo.toml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index f9e7a481f..b53d9c53b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,12 +12,12 @@ members = [ ] [workspace.dependencies.sel4-capdl-initializer] -git = "https://github.com/seL4/rust-sel4" -rev = "cf43f5d0a97854e9916cc999fdd97ff3b5fbea7b" +git = "https://github.com/au-ts/rust-sel4" +branch = "domain_set" [workspace.dependencies.sel4-capdl-initializer-types] -git = "https://github.com/seL4/rust-sel4" -rev = "cf43f5d0a97854e9916cc999fdd97ff3b5fbea7b" +git = "https://github.com/au-ts/rust-sel4" +branch = "domain_set" [profile.release.package.microkit-tool] strip = true From 3803b2fb6fb6267ee145c781f44422bb9dae7900 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Tue, 10 Mar 2026 13:06:57 +1100 Subject: [PATCH 05/21] domains: Custom start idx Signed-off-by: Krishnan Winter --- docs/manual.md | 7 +- tool/microkit/src/capdl/builder.rs | 9 ++- tool/microkit/src/sdf.rs | 109 +++++++++++++++++++---------- 3 files changed, 84 insertions(+), 41 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index c3231eb26..3d944f6a7 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -189,7 +189,7 @@ Runnable PDs of the same priority are scheduled in a round-robin manner. #### Domain scheduling (experimental) -If the SDK is built with a domain support config, the PD can be assigned to a scheduling **domain** in the system description. If a PD is assigned to a domain, then the PD will only be allowed to execute when that domain is active. Which domain is active at any given point in time is determined by the [domain schedule](#domain). +If a Microkit system is built with a domain supported (`release_domain, debug_domain`) config, the PD can be assigned to a scheduling **domain** in the system description. If a PD is assigned to a domain, then the PD will only be allowed to execute when that domain is active. By default, PDs are assigned to domain 0. Which domain is active at any given point in time is determined by the [domain schedule](#domain). ## Virtual Machines {#vm} @@ -1148,7 +1148,7 @@ The `id` should be passed to the `microkit_notify` and `microkit_ppcall` functio ## `domain_schedule` (experimental) -The `domain_schedule` element has has a list of up to 256 `domain` child elements. Each child specifies a particular timeslice in the domain schedule and the order of the child elements specifies the order in which the timeslices will be scheduled. A domain may be named more than once in the schedule, in which case the domain will have multiple timeslices in the schedule. +The `domain_schedule` element, by default, has a list of up to 256 `domain` child elements. This can be configured by changing the number of schedule entries defined in the `release_domains` and `debug_domains` configs in `build_sdk.py`. Each child specifies a particular timeslice in the domain schedule and the order of the child elements specifies the order in which the timeslices will be scheduled. A domain may be named more than once in the schedule, in which case the domain will have multiple timeslices in the schedule. The `domain` element has the following attributes: @@ -1157,6 +1157,9 @@ The `domain` element has the following attributes: The `name` attribute of each `domain` element can be referenced in the `domain` attribute of a `protection_domain` element. +The `domain_start` element has the following attribute: +* `index`: This is the start index of the domain schedule. When the kernel reaches the end of the domain schedule, it will wrap around to this index again. + The `domain_schedule` element is only valid if the using one of the domain configs (`release_domains`, `debug_domains`). # Board Support Packages {#bsps} diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 95dcc2d57..34eeae107 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -131,6 +131,7 @@ impl CapDLSpecContainer { objects: Vec::new(), irqs: Vec::new(), domain_schedule: None, + domain_start_idx: None, asid_slots: Vec::new(), root_objects: Range { start: 0.into(), @@ -1087,11 +1088,9 @@ pub fn build_capdl_spec( } // ********************************* - // Step 5. Pass domain schedule + // Step 5. Parse domain schedule // ********************************* - - if system.domain_schedule.is_some() { let mut domain_schedule: Vec = Vec::new(); // We need to convert from the milliseconds that the user defines in the @@ -1105,6 +1104,10 @@ pub fn build_capdl_spec( } spec_container.spec.domain_schedule = Some(domain_schedule); + spec_container.spec.domain_start_idx = system.domain_schedule + .as_ref() + .unwrap() + .domain_start_idx.map(|idx| Word(idx)); } // ********************************* diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 36af6ee57..9596183ab 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -288,6 +288,7 @@ pub struct DomainTimeslice { pub struct DomainSchedule { pub domain_ids: HashMap, pub schedule: Vec, + pub domain_start_idx: Option, } #[derive(Debug, PartialEq, Eq)] @@ -1129,58 +1130,80 @@ impl DomainSchedule { let mut next_domain_id = 0; let mut domain_ids = HashMap::new(); let mut schedule = Vec::new(); + let mut domain_start_idx: Option = None; for child in node.children() { if !child.is_element() { continue; } let child_name = child.tag_name().name(); - if child_name != "domain" { - return Err(format!( - "Error: invalid XML element '{}': {}", - child_name, - loc_string(xml_sdf, pos) - )); - } + match child_name { + "domain" => { + if schedule.len() == config.num_domain_schedules as usize { + return Err(format!( + "Error: length of domain schedule exceeds maximum of {}: {}", + config.num_domain_schedules as usize, + loc_string(xml_sdf, pos) + )); + } - if schedule.len() == config.num_domain_schedules as usize { - return Err(format!( - "Error: length of domain schedule exceeds maximum of {}: {}", - config.num_domain_schedules as usize, - loc_string(xml_sdf, pos) - )); - } + check_attributes(xml_sdf, &child, &["name", "length"])?; + let name = checked_lookup(xml_sdf, &child, "name")?; + let length = checked_lookup(xml_sdf, &child, "length")?.parse::(); + if length.is_err() { + return Err(format!( + "Error: invalid domain timeslice length '{}': {}", + name, + loc_string(xml_sdf, pos) + )); + } - check_attributes(xml_sdf, &child, &["name", "length"])?; - let name = checked_lookup(xml_sdf, &child, "name")?; - let length = checked_lookup(xml_sdf, &child, "length")?.parse::(); - if length.is_err() { - return Err(format!( - "Error: invalid domain timeslice length '{}': {}", - name, - loc_string(xml_sdf, pos) - )); - } + let id = match domain_ids.get(name) { + Some(&id) => id, + None => { + let id = next_domain_id; + next_domain_id += 1; + domain_ids.insert(name.to_string(), id); + id + } + }; - let id = match domain_ids.get(name) { - Some(&id) => id, - None => { - let id = next_domain_id; - next_domain_id += 1; - domain_ids.insert(name.to_string(), id); - id + schedule.push(DomainTimeslice { + id, + length: length.unwrap(), + }); + } + "domain_start" => { + if domain_start_idx.is_some() { + return Err(format!( + "Error: Duplicate setting of domain start index, already set to '{}'", + domain_start_idx.unwrap() + )) + } + check_attributes(xml_sdf, &child, &["index"])?; + let start_index = checked_lookup(xml_sdf, &child, "index")?.parse::(); + if start_index.is_err() { + return Err(format!( + "Error: invalid domain start index", + )) + } + domain_start_idx = Some(start_index.unwrap()); + } + _ => { + return Err(format!( + "Error: invalid XML element '{}': {}", + child_name, + loc_string(xml_sdf, pos) + )); } - }; - schedule.push(DomainTimeslice { - id, - length: length.unwrap(), - }); + } } Ok(DomainSchedule { domain_ids, schedule, + domain_start_idx, }) } } @@ -2134,6 +2157,20 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result= dom_sched.schedule.len() as u64 + { + return Err(format!( + "Error: Setting domain start index to '{}' when schedule is of length '{}'. Note that the domain start is 0 indexed.", + dom_sched.domain_start_idx.unwrap(), + dom_sched.schedule.len() + )) + } + } + Ok(SystemDescription { protection_domains: pds, memory_regions: mrs, From cd95bf0d4d0f3d53c1e77f36414203b8d4cde81f Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Tue, 24 Mar 2026 14:32:51 +1100 Subject: [PATCH 06/21] domains: Build one monitor per domain Signed-off-by: Krishnan Winter --- monitor/src/main.c | 5 +- tool/microkit/src/capdl/builder.rs | 260 ++++++++++++++------------- tool/microkit/src/capdl/packaging.rs | 18 +- tool/microkit/src/capdl/spec.rs | 8 +- tool/microkit/src/main.rs | 22 ++- tool/microkit/src/sdf.rs | 16 +- tool/microkit/src/sel4.rs | 8 +- tool/microkit/src/symbols.rs | 121 +++++++------ 8 files changed, 259 insertions(+), 199 deletions(-) diff --git a/monitor/src/main.c b/monitor/src/main.c index bd8c3288e..38e6c2a08 100644 --- a/monitor/src/main.c +++ b/monitor/src/main.c @@ -32,6 +32,7 @@ extern seL4_IPCBuffer __sel4_ipc_buffer_obj; seL4_IPCBuffer *__sel4_ipc_buffer = &__sel4_ipc_buffer_obj; +char monitor_name[MAX_NAME_LEN]; char pd_names[MAX_PDS][MAX_NAME_LEN]; seL4_Word pd_names_len; char vm_names[MAX_VMS][MAX_NAME_LEN] __attribute__((unused)); @@ -897,7 +898,9 @@ void main(void) } #endif - puts("MON|INFO: Microkit Monitor started!\n"); + puts("MON|INFO: Microkit Monitor started: '"); + puts(monitor_name); + puts("'\n"); monitor(); } diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 34eeae107..469236c87 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -19,7 +19,7 @@ use crate::{ capdl::{ irq::create_irq_handler_cap, memory::{create_vspace, create_vspace_ept, map_page}, - spec::{capdl_obj_physical_size_bits, ElfContent}, + spec::{capdl_obj_physical_size_bits, ElfContent, ElfIndex}, util::*, }, elf::ElfFile, @@ -183,7 +183,7 @@ impl CapDLSpecContainer { sel4_config: &Config, pd_name: &str, pd_cpu: CpuCore, - elf_id: usize, + elf_id: ElfIndex, elf: &ElfFile, ) -> Result { // We assumes that ELFs and PDs have a one-to-one relationship. So for each ELF we create a VSpace. @@ -233,7 +233,7 @@ impl CapDLSpecContainer { end: dest_offset + len_to_cpy, }, content: FillEntryContent::Data(ElfContent { - elf_id, + elf_id: elf_id.clone(), elf_seg_idx: seg_idx, elf_seg_data_range: (section_offset as usize ..((section_offset + len_to_cpy) as usize)), @@ -388,6 +388,7 @@ fn map_memory_region( pub fn build_capdl_spec( kernel_config: &Config, elfs: &mut [ElfFile], + monitor_elfs: &mut [ElfFile], system: &SystemDescription, ) -> Result { let mut spec_container = CapDLSpecContainer::new(); @@ -396,112 +397,119 @@ pub fn build_capdl_spec( // Step 1. Create the monitor's spec. // ********************************* // Parse ELF, create VSpace, map in all ELF loadable frames and IPC buffer, and create TCB. - // We expect the PD ELFs to be first and the monitor ELF last in the list of ELFs. - let mon_elf_id = elfs.len() - 1; - assert!(elfs.len() == system.protection_domains.len() + 1); - let monitor_tcb_obj_id = { - let monitor_elf = &elfs[mon_elf_id]; - spec_container - .add_elf_to_spec( - kernel_config, - MONITOR_PD_NAME, - CpuCore(0), - mon_elf_id, - monitor_elf, - ) - .unwrap() - }; + let mut mon_fault_ep_id_by_dom = Vec::with_capacity(monitor_elfs.len()); + let mut mon_cnode_id_by_dom = Vec::with_capacity(monitor_elfs.len()); + let mut mon_pd_idx_by_dom: Vec = vec![0; monitor_elfs.len()]; + + for (monitor_idx, monitor_elf) in monitor_elfs.iter().enumerate() { + let monitor_name = format!("{MONITOR_PD_NAME}_{monitor_idx}"); + let monitor_name_str = monitor_name.as_str(); + let monitor_tcb_obj_id = { + spec_container + .add_elf_to_spec( + kernel_config, + monitor_name_str, + CpuCore(0), + ElfIndex::MonitorElf(monitor_idx), + monitor_elf, + ) + .unwrap() + }; - // Create monitor fault endpoint object + cap - let mon_fault_ep_obj_id = - capdl_util_make_endpoint_obj(&mut spec_container, MONITOR_PD_NAME, true); - let mon_fault_ep_cap = capdl_util_make_endpoint_cap(mon_fault_ep_obj_id, true, true, true, 0); - - // Create monitor reply object object + cap - let mon_reply_obj_id = capdl_util_make_reply_obj(&mut spec_container, MONITOR_PD_NAME); - let mon_reply_cap = capdl_util_make_reply_cap(mon_reply_obj_id); - - // Create monitor scheduling context object + cap - let mon_sc_obj_id = capdl_util_make_sc_obj( - &mut spec_container, - MONITOR_PD_NAME, - PD_SCHEDCONTEXT_EXTRA_SIZE_BITS as u8, - BUDGET_DEFAULT, - BUDGET_DEFAULT, - 0, - ); - let mon_sc_cap = capdl_util_make_sc_cap(mon_sc_obj_id); - - // Create monitor CSpace and pre-insert the fault EP and reply caps into the correct slots in CSpace. - let mon_cnode_obj_id = capdl_util_make_cnode_obj( - &mut spec_container, - MONITOR_PD_NAME, - PD_CAP_BITS, - [ - capdl_util_make_cte(MON_FAULT_EP_CAP_IDX as u32, mon_fault_ep_cap), - capdl_util_make_cte(MON_REPLY_CAP_IDX as u32, mon_reply_cap), - ] - .to_vec(), - ); - let mon_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; - let mon_cnode_cap = capdl_util_make_cnode_cap(mon_cnode_obj_id, 0, mon_guard_size as u8); - - // Create monitor stack frame - let mon_stack_frame_obj_id = capdl_util_make_frame_obj( - &mut spec_container, - Fill { - entries: [].to_vec(), - }, - &format!("{MONITOR_PD_NAME}_stack"), - None, - PageSize::Small.fixed_size_bits(kernel_config) as u8, - ); - let mon_stack_frame_cap = - capdl_util_make_frame_cap(mon_stack_frame_obj_id, true, true, false, true); - let mon_vspace_obj_id = - capdl_util_get_vspace_id_from_tcb_id(&spec_container, monitor_tcb_obj_id); - map_page( - &mut spec_container, - kernel_config, - MONITOR_PD_NAME, - mon_vspace_obj_id, - mon_stack_frame_cap, - PageSize::Small as u64, - kernel_config.pd_stack_bottom(MON_STACK_SIZE), - ) - .unwrap(); - - // At this point, all of the required objects for the monitor have been created and it caps inserted into - // the correct slot in the CSpace. We need to bind those objects into the TCB for the monitor to use them. - // In addition, `add_elf_to_spec()` doesn't fill most the details in the TCB. - // Now fill them in: stack ptr, priority, ipc buf vaddr, etc. - if let Object::Tcb(monitor_tcb) = &mut spec_container - .get_root_object_mut(monitor_tcb_obj_id) - .unwrap() - .object - { - // Special case, monitor has its stack statically allocated. - monitor_tcb.extra.sp = Word(kernel_config.pd_stack_top()); - // While there is nothing stopping us from running the monitor at the highest priority alongside the - // CapDL initialiser, the debug kernel serial output can get garbled when the monitor TCB is resumed. - monitor_tcb.extra.prio = MONITOR_PRIORITY; - monitor_tcb.extra.max_prio = MONITOR_PRIORITY; - monitor_tcb.extra.resume = true; - - // @kwinter: What domain should the monitor be in? - monitor_tcb.extra.domain = 0; - - monitor_tcb.slots.push(capdl_util_make_cte( - TcbBoundSlot::CSpace as u32, - mon_cnode_cap, - )); + // Create monitor fault endpoint object + cap + let mon_fault_ep_obj_id = + capdl_util_make_endpoint_obj(&mut spec_container, monitor_name_str, true); + let mon_fault_ep_cap = capdl_util_make_endpoint_cap(mon_fault_ep_obj_id, true, true, true, 0); - monitor_tcb.slots.push(capdl_util_make_cte( - TcbBoundSlot::SchedContext as u32, - mon_sc_cap, - )); - } else { - unreachable!("internal bug: build_capdl_spec() got a non TCB object ID when trying to set TCB parameters for the monitor."); + mon_fault_ep_id_by_dom.push(mon_fault_ep_obj_id); + + // Create monitor reply object object + cap + let mon_reply_obj_id = capdl_util_make_reply_obj(&mut spec_container, monitor_name_str); + let mon_reply_cap = capdl_util_make_reply_cap(mon_reply_obj_id); + + // Create monitor scheduling context object + cap + let mon_sc_obj_id = capdl_util_make_sc_obj( + &mut spec_container, + monitor_name_str, + PD_SCHEDCONTEXT_EXTRA_SIZE_BITS as u8, + BUDGET_DEFAULT, + BUDGET_DEFAULT, + 0, + ); + let mon_sc_cap = capdl_util_make_sc_cap(mon_sc_obj_id); + + // Create monitor CSpace and pre-insert the fault EP and reply caps into the correct slots in CSpace. + let mon_cnode_obj_id = capdl_util_make_cnode_obj( + &mut spec_container, + monitor_name_str, + PD_CAP_BITS, + [ + capdl_util_make_cte(MON_FAULT_EP_CAP_IDX as u32, mon_fault_ep_cap), + capdl_util_make_cte(MON_REPLY_CAP_IDX as u32, mon_reply_cap), + ] + .to_vec(), + ); + let mon_guard_size = kernel_config.cap_address_bits - PD_CAP_BITS as u64; + let mon_cnode_cap = capdl_util_make_cnode_cap(mon_cnode_obj_id, 0, mon_guard_size as u8); + + mon_cnode_id_by_dom.push(mon_cnode_obj_id); + + // Create monitor stack frame + let mon_stack_frame_obj_id = capdl_util_make_frame_obj( + &mut spec_container, + Fill { + entries: [].to_vec(), + }, + &format!("{monitor_name_str}_stack"), + None, + PageSize::Small.fixed_size_bits(kernel_config) as u8, + ); + let mon_stack_frame_cap = + capdl_util_make_frame_cap(mon_stack_frame_obj_id, true, true, false, true); + let mon_vspace_obj_id = + capdl_util_get_vspace_id_from_tcb_id(&spec_container, monitor_tcb_obj_id); + map_page( + &mut spec_container, + kernel_config, + monitor_name_str, + mon_vspace_obj_id, + mon_stack_frame_cap, + PageSize::Small as u64, + kernel_config.pd_stack_bottom(MON_STACK_SIZE), + ) + .unwrap(); + + // At this point, all of the required objects for the monitor have been created and it caps inserted into + // the correct slot in the CSpace. We need to bind those objects into the TCB for the monitor to use them. + // In addition, `add_elf_to_spec()` doesn't fill most the details in the TCB. + // Now fill them in: stack ptr, priority, ipc buf vaddr, etc. + if let Object::Tcb(monitor_tcb) = &mut spec_container + .get_root_object_mut(monitor_tcb_obj_id) + .unwrap() + .object + { + // Special case, monitor has its stack statically allocated. + monitor_tcb.extra.sp = Word(kernel_config.pd_stack_top()); + // While there is nothing stopping us from running the monitor at the highest priority alongside the + // CapDL initialiser, the debug kernel serial output can get garbled when the monitor TCB is resumed. + monitor_tcb.extra.prio = MONITOR_PRIORITY; + monitor_tcb.extra.max_prio = MONITOR_PRIORITY; + monitor_tcb.extra.resume = true; + + monitor_tcb.extra.domain = monitor_idx as u8; + + monitor_tcb.slots.push(capdl_util_make_cte( + TcbBoundSlot::CSpace as u32, + mon_cnode_cap, + )); + + monitor_tcb.slots.push(capdl_util_make_cte( + TcbBoundSlot::SchedContext as u32, + mon_sc_cap, + )); + } else { + unreachable!("internal bug: build_capdl_spec() got a non TCB object ID when trying to set TCB parameters for the monitor."); + } } // ********************************* @@ -560,13 +568,18 @@ pub fn build_capdl_spec( for (pd_global_idx, pd) in system.protection_domains.iter().enumerate() { let elf_obj = &elfs[pd_global_idx]; + let mon_pd_idx = mon_pd_idx_by_dom[pd.domain_id as usize]; + + // Get this PD's monitor info + let mon_cnode_obj_id = *mon_cnode_id_by_dom.get(pd.domain_id as usize).unwrap(); + let mon_fault_ep_obj_id = *mon_fault_ep_id_by_dom.get(pd.domain_id as usize).unwrap(); let mut caps_to_bind_to_tcb: Vec = Vec::new(); let mut caps_to_insert_to_pd_cspace: Vec = Vec::new(); // Step 3-1: Create TCB and VSpace with all ELF loadable frames mapped in. let pd_tcb_obj_id = spec_container - .add_elf_to_spec(kernel_config, &pd.name, pd.cpu, pd_global_idx, elf_obj) + .add_elf_to_spec(kernel_config, &pd.name, pd.cpu, ElfIndex::SystemElf(pd_global_idx), elf_obj) .unwrap(); let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id); @@ -667,15 +680,19 @@ pub fn build_capdl_spec( )); // Step 3-5 Create fault Endpoint cap to parent/monitor - let pd_fault_ep_cap = if let Some(pd_parent) = pd.parent { - assert!(pd_global_idx > pd_parent); + let pd_fault_ep_cap = if pd.parent.is_none() { + let badge: u64 = mon_pd_idx as u64 + 1; + capdl_util_make_endpoint_cap(mon_fault_ep_obj_id, true, true, true, badge) + } else { + // @kwinter: Should we enforce domain boundaries here? + assert!(pd_global_idx > pd.parent.unwrap()); let badge: u64 = FAULT_BADGE | pd.id.unwrap(); - let parent_ep_obj_id = &pd_id_to_ep_id[&pd_parent]; + let parent_ep_obj_id = &pd_id_to_ep_id[&pd.parent.unwrap()]; let fault_ep_cap = capdl_util_make_endpoint_cap(*parent_ep_obj_id, true, true, true, badge); // Allow the parent PD to access the child's TCB: - let parent_cspace_obj_id = &pd_id_to_cspace_id[&pd_parent]; + let parent_cspace_obj_id = &pd_id_to_cspace_id[&pd.parent.unwrap()]; capdl_util_insert_cap_into_cspace( &mut spec_container, *parent_cspace_obj_id, @@ -684,10 +701,6 @@ pub fn build_capdl_spec( ); fault_ep_cap - } else { - // badge = pd_global_idx + 1 because seL4 considers badge = 0 as no badge. - let badge: u64 = pd_global_idx as u64 + 1; - capdl_util_make_endpoint_cap(mon_fault_ep_obj_id, true, true, true, badge) }; caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( PD_FAULT_EP_CAP_IDX as u32, @@ -705,7 +718,7 @@ pub fn build_capdl_spec( true, true, true, - pd_global_idx as u64 + 1, + mon_pd_idx as u64 + 1, ); caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( PD_MONITOR_EP_CAP_IDX as u32, @@ -910,7 +923,6 @@ pub fn build_capdl_spec( )); // Finally create TCB, unlike PDs, VMs are suspended by default until resume'd by their parent. - // @kwinter: Is it fair to assign the VM the same domain as the parent? let vm_vcpu_tcb_inner_obj = object::Tcb { slots: caps_to_bind_to_vm_tcbs, extra: Box::new(object::TcbExtraInfo { @@ -919,7 +931,7 @@ pub fn build_capdl_spec( prio: virtual_machine.priority, max_prio: virtual_machine.priority, resume: false, - domain: pd.domain_id.expect("No domain ID specified for vm"), + domain: pd.domain_id, // VMs do not have program images associated with them so these are always zero. ip: Word(0), sp: Word(0), @@ -988,7 +1000,7 @@ pub fn build_capdl_spec( pd_tcb.extra.prio = pd.priority; pd_tcb.extra.max_prio = pd.priority; pd_tcb.extra.resume = true; - pd_tcb.extra.domain = pd.domain_id.expect("No domain ID specified for PD"); + pd_tcb.extra.domain = pd.domain_id; pd_tcb.slots.extend(caps_to_bind_to_tcb); // Stylistic purposes only @@ -1003,7 +1015,7 @@ pub fn build_capdl_spec( capdl_util_insert_cap_into_cspace( &mut spec_container, mon_cnode_obj_id, - (MON_BASE_PD_TCB_CAP as usize + pd_global_idx) as u32, + (MON_BASE_PD_TCB_CAP as usize + mon_pd_idx) as u32, capdl_util_make_tcb_cap(pd_tcb_obj_id), ); if pd.passive { @@ -1012,16 +1024,18 @@ pub fn build_capdl_spec( capdl_util_insert_cap_into_cspace( &mut spec_container, mon_cnode_obj_id, - (MON_BASE_SCHED_CONTEXT_CAP as usize + pd_global_idx) as u32, + (MON_BASE_SCHED_CONTEXT_CAP as usize + mon_pd_idx) as u32, capdl_util_make_sc_cap(pd_sc_obj_id), ); capdl_util_insert_cap_into_cspace( &mut spec_container, mon_cnode_obj_id, - (MON_BASE_NOTIFICATION_CAP as usize + pd_global_idx) as u32, + (MON_BASE_NOTIFICATION_CAP as usize + mon_pd_idx) as u32, capdl_util_make_ntfn_cap(pd_ntfn_obj_id, true, true, 0), ); } + + mon_pd_idx_by_dom[pd.domain_id as usize] = mon_pd_idx + 1; } // ********************************* diff --git a/tool/microkit/src/capdl/packaging.rs b/tool/microkit/src/capdl/packaging.rs index ab1e65547..a319d0c1b 100644 --- a/tool/microkit/src/capdl/packaging.rs +++ b/tool/microkit/src/capdl/packaging.rs @@ -8,6 +8,7 @@ use crate::{ capdl::{initialiser::CapDLInitialiser, CapDLSpecContainer}, elf::ElfFile, sel4::{Config, PageSize}, + capdl::spec::{ElfIndex}, }; pub fn pack_spec_into_initial_task( @@ -15,6 +16,7 @@ pub fn pack_spec_into_initial_task( build_config: &str, spec_container: &CapDLSpecContainer, system_elfs: &[ElfFile], + monitor_elfs: &[ElfFile], capdl_initialiser: &mut CapDLInitialiser, ) { let compress_frames = true; @@ -24,9 +26,19 @@ pub fn pack_spec_into_initial_task( PageSize::Small.fixed_size_bits(sel4_config) as u8, |_| embed_frames, |d, buf| { - buf.copy_from_slice( - &system_elfs[d.elf_id].segments[d.elf_seg_idx].data()[d.elf_seg_data_range.clone()], - ); + match d.elf_id { + ElfIndex::SystemElf(elf_id) => { + buf.copy_from_slice( + &system_elfs[elf_id].segments[d.elf_seg_idx].data()[d.elf_seg_data_range.clone()], + ); + } + ElfIndex::MonitorElf(elf_id) => { + buf.copy_from_slice( + &monitor_elfs[elf_id].segments[d.elf_seg_idx].data()[d.elf_seg_data_range.clone()], + ); + } + } + compress_frames }, ); diff --git a/tool/microkit/src/capdl/spec.rs b/tool/microkit/src/capdl/spec.rs index a78d1c377..88ed79ee8 100644 --- a/tool/microkit/src/capdl/spec.rs +++ b/tool/microkit/src/capdl/spec.rs @@ -14,9 +14,15 @@ use crate::{ sel4::{Config, ObjectType, PageSize}, }; +#[derive(Clone, Serialize)] +pub enum ElfIndex { + MonitorElf(usize), + SystemElf(usize), +} + #[derive(Clone, Serialize)] pub struct ElfContent { - pub elf_id: usize, + pub elf_id: ElfIndex, pub elf_seg_idx: usize, pub elf_seg_data_range: Range, } diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index a28a9130d..45685c64a 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -513,6 +513,8 @@ fn main() -> Result<(), String> { Arch::X86_64 => 1 << 12, }; + let num_domain_schedules = json_str_as_u64(&kernel_config_json, "NUM_DOMAIN_SCHEDULES")?; + let kernel_config = Config { arch, word_size: json_str_as_u64(&kernel_config_json, "WORD_SIZE")?, @@ -544,7 +546,7 @@ fn main() -> Result<(), String> { invocations_labels, device_regions, normal_regions, - num_domain_schedules: json_str_as_u64(&kernel_config_json, "ROOT_CNODE_SIZE_BITS")?, + num_domain_schedules, }; if kernel_config.arch != Arch::X86_64 && !loader_elf_path.exists() { @@ -657,8 +659,17 @@ fn main() -> Result<(), String> { } } - // The monitor is just a special PD - system_elfs.push(monitor_elf); + // Create a copy of the monitor elf for every domain in the system + let mut num_domains = 1; + if system.domain_schedule.is_some() { + num_domains = system.domain_schedule.clone().unwrap().domain_ids.len(); + } + + let mut monitor_elfs = Vec::with_capacity(num_domains); + + for _ in 0..num_domains { + monitor_elfs.push(monitor_elf.clone()); + } let mut capdl_initialiser = CapDLInitialiser::new(capdl_initialiser_elf); @@ -671,17 +682,18 @@ fn main() -> Result<(), String> { spec_need_refinement = false; // Patch all the required symbols in the Monitor and PDs according to the Microkit's requirements - if let Err(err) = patch_symbols(&kernel_config, &mut system_elfs, &system) { + if let Err(err) = patch_symbols(&kernel_config, &mut system_elfs, &mut monitor_elfs, &system) { eprintln!("ERROR: {err}"); std::process::exit(1); } - let mut spec_container = build_capdl_spec(&kernel_config, &mut system_elfs, &system)?; + let mut spec_container = build_capdl_spec(&kernel_config, &mut system_elfs, &mut monitor_elfs, &system)?; pack_spec_into_initial_task( &kernel_config, args.config, &spec_container, &system_elfs, + &monitor_elfs, &mut capdl_initialiser, ); diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 9596183ab..a75536558 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -275,7 +275,8 @@ pub struct ProtectionDomain { /// Location in the parsed SDF file text_pos: Option, /// Index into the domain schedule vector if the system is using domain scheduling - pub domain_id: Option, + /// Defaults to domain 0 if not set. + pub domain_id: u8, } #[derive(Debug, PartialEq, Eq, Hash, Copy, Clone)] @@ -284,7 +285,7 @@ pub struct DomainTimeslice { pub length: u64, } -#[derive(Debug, PartialEq, Eq)] +#[derive(Debug, PartialEq, Eq, Clone)] pub struct DomainSchedule { pub domain_ids: HashMap, pub schedule: Vec, @@ -601,13 +602,14 @@ impl ProtectionDomain { )); } - let mut domain_id = None; + let mut domain_id: u8 = 0; match (domain_schedule, checked_lookup(xml_sdf, node, "domain")) { (Some(domain_schedule), Ok(domain_name)) => { - domain_id = domain_schedule.domain_ids.get(domain_name); - if domain_id.is_none() { + let domain_id_get = domain_schedule.domain_ids.get(domain_name); + if domain_id_get.is_none() { return Err(format!("Protection domain {} specifies a domain {} that is not in the domain schedule", name, domain_name)); } + domain_id = *domain_id_get.unwrap(); } (Some(_), _) => { return Err(format!("System specifies a domain schedule but protection domain {} does not specify a domain", name)) @@ -1112,7 +1114,7 @@ impl ProtectionDomain { parent: None, setvar_id, text_pos: Some(xml_sdf.doc.text_pos_at(node.range().start)), - domain_id: domain_id.copied(), + domain_id, }) } } @@ -1856,6 +1858,8 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result>, pub normal_regions: Option>, - /// Flag to enable experimental domain scheduler support + /// Number of domain schedules the kernel is configure for pub num_domain_schedules: u64, } diff --git a/tool/microkit/src/symbols.rs b/tool/microkit/src/symbols.rs index 6136cf145..314e23dc4 100644 --- a/tool/microkit/src/symbols.rs +++ b/tool/microkit/src/symbols.rs @@ -8,7 +8,7 @@ use std::{cmp::min, collections::HashMap}; use crate::{ elf::ElfFile, - sdf::{self, SysMemoryRegion, SystemDescription}, + sdf::{self, SysMemoryRegion, SystemDescription, ProtectionDomain}, sel4::{Arch, Config}, util::{monitor_serialise_names, monitor_serialise_u64_vec}, MAX_PDS, MAX_VMS, PD_MAX_NAME_LENGTH, VM_MAX_NAME_LENGTH, @@ -19,68 +19,83 @@ use crate::{ pub fn patch_symbols( kernel_config: &Config, pd_elf_files: &mut [ElfFile], + monitor_elf_files: &mut [ElfFile], system: &SystemDescription, ) -> Result<(), String> { // ********************************* // Step 1. Write ELF symbols in the monitor. // ********************************* - let monitor_elf = pd_elf_files.last_mut().unwrap(); + // There is a one to one mapping between monitors and domains + for (mon_idx, monitor_elf) in monitor_elf_files.iter_mut().enumerate() { + // Filter a subset of the pd's that belong to this monitor's + // domain + let filtered_pds: Vec<&ProtectionDomain> = system + .protection_domains + .iter() + .filter(|pd| pd.domain_id == mon_idx as u8) + .collect(); - let pd_names: Vec = system - .protection_domains - .iter() - .map(|pd| pd.name.clone()) - .collect(); - monitor_elf - .write_symbol( - "pd_names_len", - &system.protection_domains.len().to_le_bytes(), - ) - .unwrap(); - monitor_elf - .write_symbol( - "pd_names", - &monitor_serialise_names(&pd_names, MAX_PDS, PD_MAX_NAME_LENGTH), - ) - .unwrap(); + let pd_names: Vec = filtered_pds + .iter() + .map(|pd| pd.name.clone()) + .collect(); + monitor_elf + .write_symbol( + "pd_names_len", + &filtered_pds.len().to_le_bytes(), + ) + .unwrap(); + monitor_elf + .write_symbol( + "pd_names", + &monitor_serialise_names(&pd_names, MAX_PDS, PD_MAX_NAME_LENGTH), + ) + .unwrap(); - let vm_names: Vec = system - .protection_domains - .iter() - .filter(|pd| pd.virtual_machine.is_some()) - .flat_map(|pd_with_vm| { - let vm = pd_with_vm.virtual_machine.as_ref().unwrap(); - let num_vcpus = vm.vcpus.len(); - std::iter::repeat_n(vm.name.clone(), num_vcpus) - }) - .collect(); + let vm_names: Vec = filtered_pds + .iter() + .filter(|pd| pd.virtual_machine.is_some()) + .flat_map(|pd_with_vm| { + let vm = pd_with_vm.virtual_machine.as_ref().unwrap(); + let num_vcpus = vm.vcpus.len(); + std::iter::repeat_n(vm.name.clone(), num_vcpus) + }) + .collect(); + + let vm_names_len = match kernel_config.arch { + Arch::Aarch64 | Arch::Riscv64 => vm_names.len(), + // VM on x86 doesn't have a separate TCB. + Arch::X86_64 => 0, + }; + monitor_elf + .write_symbol("vm_names_len", &vm_names_len.to_le_bytes()) + .unwrap(); + monitor_elf + .write_symbol( + "vm_names", + &monitor_serialise_names(&vm_names, MAX_VMS, VM_MAX_NAME_LENGTH), + ) + .unwrap(); - let vm_names_len = match kernel_config.arch { - Arch::Aarch64 | Arch::Riscv64 => vm_names.len(), - // VM on x86 doesn't have a separate TCB. - Arch::X86_64 => 0, - }; - monitor_elf - .write_symbol("vm_names_len", &vm_names_len.to_le_bytes()) - .unwrap(); - monitor_elf - .write_symbol( - "vm_names", - &monitor_serialise_names(&vm_names, MAX_VMS, VM_MAX_NAME_LENGTH), - ) - .unwrap(); + let mut pd_stack_bottoms: Vec = Vec::new(); + for pd in filtered_pds.iter() { + let cur_stack_vaddr = kernel_config.pd_stack_bottom(pd.stack_size); + pd_stack_bottoms.push(cur_stack_vaddr); + } + monitor_elf + .write_symbol( + "pd_stack_bottom_addrs", + &monitor_serialise_u64_vec(&pd_stack_bottoms), + ) + .unwrap(); - let mut pd_stack_bottoms: Vec = Vec::new(); - for pd in system.protection_domains.iter() { - let cur_stack_vaddr = kernel_config.pd_stack_bottom(pd.stack_size); - pd_stack_bottoms.push(cur_stack_vaddr); + monitor_elf + .write_symbol( + "monitor_name", + format!("monitor_{}", mon_idx).as_bytes() + ) + .unwrap(); } - monitor_elf - .write_symbol( - "pd_stack_bottom_addrs", - &monitor_serialise_u64_vec(&pd_stack_bottoms), - ) - .unwrap(); // ********************************* // Step 2. Write ELF symbols for each PD From adb42bc9319344c02e4f7b1805900cf9f4ab2a3f Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Tue, 17 Mar 2026 15:29:23 +1100 Subject: [PATCH 07/21] domains: Add index shift Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 9 +++++- tool/microkit/src/sdf.rs | 51 ++++++++++++++++++++++++++++-- 2 files changed, 57 insertions(+), 3 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 469236c87..ddfe30074 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -132,6 +132,7 @@ impl CapDLSpecContainer { irqs: Vec::new(), domain_schedule: None, domain_start_idx: None, + domain_idx_shift: None, asid_slots: Vec::new(), root_objects: Range { start: 0.into(), @@ -1114,14 +1115,20 @@ pub fn build_capdl_spec( domain_schedule.push(DomainSchedEntry{ id: sched_entry.id, time: sched_entry.length * ticks_in_ms, - }) + }); } + println!("This is the domain schedule: {:?}", domain_schedule); + spec_container.spec.domain_schedule = Some(domain_schedule); spec_container.spec.domain_start_idx = system.domain_schedule .as_ref() .unwrap() .domain_start_idx.map(|idx| Word(idx)); + spec_container.spec.domain_idx_shift = system.domain_schedule + .as_ref() + .unwrap() + .domain_idx_shift.map(|shift| Word(shift)); } // ********************************* diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index a75536558..c2caea67f 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -290,6 +290,7 @@ pub struct DomainSchedule { pub domain_ids: HashMap, pub schedule: Vec, pub domain_start_idx: Option, + pub domain_idx_shift: Option, } #[derive(Debug, PartialEq, Eq)] @@ -1133,6 +1134,7 @@ impl DomainSchedule { let mut domain_ids = HashMap::new(); let mut schedule = Vec::new(); let mut domain_start_idx: Option = None; + let mut domain_idx_shift: Option = None; for child in node.children() { if !child.is_element() { continue; @@ -1190,6 +1192,24 @@ impl DomainSchedule { )) } domain_start_idx = Some(start_index.unwrap()); + + } + "domain_idx_shift" => { + if domain_idx_shift.is_some() { + return Err(format!( + "Error: Duplicate setting of domain index shift, already set to '{}'", + domain_idx_shift.unwrap() + )) + } + check_attributes(xml_sdf, &child, &["shift"])?; + let index_shift = checked_lookup(xml_sdf, &child, "shift")?.parse::(); + if index_shift.is_err() { + return Err(format!( + "Error: invalid domain index shift", + )) + } + domain_idx_shift = Some(index_shift.unwrap()); + } _ => { return Err(format!( @@ -1206,6 +1226,7 @@ impl DomainSchedule { domain_ids, schedule, domain_start_idx, + domain_idx_shift, }) } } @@ -2164,15 +2185,41 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result= dom_sched.schedule.len() as u64 + dom_sched.domain_start_idx.unwrap() >= dom_sched.schedule.len() as u64 { + return Err(format!( + "Error: Domain index of '{}' exceeds domain schedule length '{}'. NOTE: Domain start index starts at 0.", + dom_sched.domain_start_idx.unwrap(), + dom_sched.schedule.len(), + )) + } + + if dom_sched.domain_start_idx.is_some() && + dom_sched.domain_start_idx.unwrap() + dom_shift >= config.num_domain_schedules { return Err(format!( - "Error: Setting domain start index to '{}' when schedule is of length '{}'. Note that the domain start is 0 indexed.", + "Error: Setting domain start index to '{}' when max schedule length is '{}'.", dom_sched.domain_start_idx.unwrap(), dom_sched.schedule.len() )) } + + let schedule_len: u64 = dom_sched.schedule.len() as u64; + if schedule_len + dom_shift > config.num_domain_schedules { + return Err(format!( + "Error: Schedule length '{}' exceeds max schedule length '{}'.", + schedule_len, + config.num_domain_schedules, + )) + } } Ok(SystemDescription { From 959ae68e50f00e437a0c42a4114dab9c2459a5d4 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Tue, 17 Mar 2026 16:12:55 +1100 Subject: [PATCH 08/21] domains: Error checking domain kernel config Signed-off-by: Krishnan Winter --- docs/manual.md | 8 +++++++- tool/microkit/src/main.rs | 2 ++ tool/microkit/src/sdf.rs | 6 ++++++ tool/microkit/src/sel4.rs | 3 ++- tool/microkit/tests/test.rs | 2 ++ 5 files changed, 19 insertions(+), 2 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index 3d944f6a7..9a3e250b3 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -1157,8 +1157,12 @@ The `domain` element has the following attributes: The `name` attribute of each `domain` element can be referenced in the `domain` attribute of a `protection_domain` element. +The `domain_idx_shift` element has the following attribute: +* `shift`: This is the start index of where we will construct our schedule. So if we shift by 5, we will begin constructing +the domain schedule from index 5 onwards. + The `domain_start` element has the following attribute: -* `index`: This is the start index of the domain schedule. When the kernel reaches the end of the domain schedule, it will wrap around to this index again. +* `index`: This is the start index of the domain schedule. When the kernel reaches the end of the domain schedule, it will wrap around to this index again. This index is an offset into the user defined schedule, and not an absolute index. The `domain_schedule` element is only valid if the using one of the domain configs (`release_domains`, `debug_domains`). @@ -1845,6 +1849,8 @@ which PD caused an exception and details on the PD's state at the time of the fa Other than printing fault details, the monitor does not do anything to handle the fault, it will simply go back to sleep waiting for any other faults. +When domains are enabled, we will build one monitor for each domain. + ## libmicrokit {#libmicrokit_internals} Unlike the previous sections, libmicrokit is not its own program but it is worth diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index 45685c64a..fc4d753a7 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -513,6 +513,7 @@ fn main() -> Result<(), String> { Arch::X86_64 => 1 << 12, }; + let num_domains = json_str_as_u64(&kernel_config_json, "NUM_DOMAINS")?; let num_domain_schedules = json_str_as_u64(&kernel_config_json, "NUM_DOMAIN_SCHEDULES")?; let kernel_config = Config { @@ -546,6 +547,7 @@ fn main() -> Result<(), String> { invocations_labels, device_regions, normal_regions, + num_domains, num_domain_schedules, }; diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index c2caea67f..3ca6062ed 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -1126,6 +1126,12 @@ impl DomainSchedule { config: &Config, node: &roxmltree::Node, ) -> Result { + if config.num_domains <= 1 { + return Err(format!( + "Error: Attempting to set a domain schedule when kernel config does not support more than 1 domain", + )); + } + let pos = xml_sdf.doc.text_pos_at(node.range().start); check_attributes(xml_sdf, node, &[])?; diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs index 5f2f329d8..e4b54acc4 100644 --- a/tool/microkit/src/sel4.rs +++ b/tool/microkit/src/sel4.rs @@ -291,7 +291,8 @@ pub struct Config { /// The two remaining fields are only valid on ARM and RISC-V pub device_regions: Option>, pub normal_regions: Option>, - /// Number of domain schedules the kernel is configure for + /// Number of domain and domain schedules the kernel is configure for + pub num_domains: u64, pub num_domain_schedules: u64, } diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 90f634208..b01dd0909 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -33,6 +33,7 @@ const DEFAULT_AARCH64_KERNEL_CONFIG: sel4::Config = sel4::Config { invocations_labels: json!(null), device_regions: None, normal_regions: None, + num_domains: 1, num_domain_schedules: 1, }; @@ -59,6 +60,7 @@ const DEFAULT_X86_64_KERNEL_CONFIG: sel4::Config = sel4::Config { invocations_labels: json!(null), device_regions: None, normal_regions: None, + num_domains: 1, num_domain_schedules: 1, }; From 35e92f7642fbe8fccb3dff954d4e4457aaa09a10 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Fri, 20 Mar 2026 15:00:30 +1100 Subject: [PATCH 09/21] domain: rename start idx to set start Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index ddfe30074..b02d346ad 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -131,7 +131,7 @@ impl CapDLSpecContainer { objects: Vec::new(), irqs: Vec::new(), domain_schedule: None, - domain_start_idx: None, + domain_set_start: None, domain_idx_shift: None, asid_slots: Vec::new(), root_objects: Range { @@ -1121,7 +1121,7 @@ pub fn build_capdl_spec( println!("This is the domain schedule: {:?}", domain_schedule); spec_container.spec.domain_schedule = Some(domain_schedule); - spec_container.spec.domain_start_idx = system.domain_schedule + spec_container.spec.domain_set_start = system.domain_schedule .as_ref() .unwrap() .domain_start_idx.map(|idx| Word(idx)); From 4a5d5954b117ad9f1805385fa5d47468e07cc78f Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Fri, 20 Mar 2026 15:58:46 +1100 Subject: [PATCH 10/21] domain set start: Default to 0 if not set Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 2 -- tool/microkit/src/sdf.rs | 5 +++++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index b02d346ad..b6a0de3a6 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -1118,8 +1118,6 @@ pub fn build_capdl_spec( }); } - println!("This is the domain schedule: {:?}", domain_schedule); - spec_container.spec.domain_schedule = Some(domain_schedule); spec_container.spec.domain_set_start = system.domain_schedule .as_ref() diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 3ca6062ed..21d4dd19a 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -1228,6 +1228,11 @@ impl DomainSchedule { } } + // We are defaulting the set start to 0 if none has been specified. + if domain_start_idx.is_none() { + domain_start_idx = Some(0); + } + Ok(DomainSchedule { domain_ids, schedule, From c62d0b5ef20fd4cb6334f479130efd16f5ff33df Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Fri, 20 Mar 2026 16:19:20 +1100 Subject: [PATCH 11/21] pd domain: Make optional Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 13 +++++++------ tool/microkit/src/sdf.rs | 6 +++--- tool/microkit/src/symbols.rs | 2 +- 3 files changed, 11 insertions(+), 10 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index b6a0de3a6..30ffbe062 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -325,7 +325,7 @@ impl CapDLSpecContainer { prio: 0, max_prio: 0, resume: false, - domain: 0, + domain: None, ip: entry_point.into(), sp: 0.into(), gprs: Vec::new(), @@ -497,7 +497,7 @@ pub fn build_capdl_spec( monitor_tcb.extra.max_prio = MONITOR_PRIORITY; monitor_tcb.extra.resume = true; - monitor_tcb.extra.domain = monitor_idx as u8; + monitor_tcb.extra.domain = Some(monitor_idx as u8); monitor_tcb.slots.push(capdl_util_make_cte( TcbBoundSlot::CSpace as u32, @@ -569,11 +569,12 @@ pub fn build_capdl_spec( for (pd_global_idx, pd) in system.protection_domains.iter().enumerate() { let elf_obj = &elfs[pd_global_idx]; - let mon_pd_idx = mon_pd_idx_by_dom[pd.domain_id as usize]; + let pd_domain_id = pd.domain_id.unwrap_or(0); + let mon_pd_idx = mon_pd_idx_by_dom[pd_domain_id as usize]; // Get this PD's monitor info - let mon_cnode_obj_id = *mon_cnode_id_by_dom.get(pd.domain_id as usize).unwrap(); - let mon_fault_ep_obj_id = *mon_fault_ep_id_by_dom.get(pd.domain_id as usize).unwrap(); + let mon_cnode_obj_id = *mon_cnode_id_by_dom.get(pd_domain_id as usize).unwrap(); + let mon_fault_ep_obj_id = *mon_fault_ep_id_by_dom.get(pd_domain_id as usize).unwrap(); let mut caps_to_bind_to_tcb: Vec = Vec::new(); let mut caps_to_insert_to_pd_cspace: Vec = Vec::new(); @@ -1036,7 +1037,7 @@ pub fn build_capdl_spec( ); } - mon_pd_idx_by_dom[pd.domain_id as usize] = mon_pd_idx + 1; + mon_pd_idx_by_dom[pd_domain_id as usize] = mon_pd_idx + 1; } // ********************************* diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 21d4dd19a..7743d0ef5 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -276,7 +276,7 @@ pub struct ProtectionDomain { text_pos: Option, /// Index into the domain schedule vector if the system is using domain scheduling /// Defaults to domain 0 if not set. - pub domain_id: u8, + pub domain_id: Option, } #[derive(Debug, PartialEq, Eq, Hash, Copy, Clone)] @@ -603,14 +603,14 @@ impl ProtectionDomain { )); } - let mut domain_id: u8 = 0; + let mut domain_id: Option = None; match (domain_schedule, checked_lookup(xml_sdf, node, "domain")) { (Some(domain_schedule), Ok(domain_name)) => { let domain_id_get = domain_schedule.domain_ids.get(domain_name); if domain_id_get.is_none() { return Err(format!("Protection domain {} specifies a domain {} that is not in the domain schedule", name, domain_name)); } - domain_id = *domain_id_get.unwrap(); + domain_id = Some(*domain_id_get.unwrap()); } (Some(_), _) => { return Err(format!("System specifies a domain schedule but protection domain {} does not specify a domain", name)) diff --git a/tool/microkit/src/symbols.rs b/tool/microkit/src/symbols.rs index 314e23dc4..c77297673 100644 --- a/tool/microkit/src/symbols.rs +++ b/tool/microkit/src/symbols.rs @@ -32,7 +32,7 @@ pub fn patch_symbols( let filtered_pds: Vec<&ProtectionDomain> = system .protection_domains .iter() - .filter(|pd| pd.domain_id == mon_idx as u8) + .filter(|pd| pd.domain_id.unwrap_or(0) == mon_idx as u8) .collect(); let pd_names: Vec = filtered_pds From e56f90e888516fca3004f5db7414133e341aaa44 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Fri, 20 Mar 2026 16:22:24 +1100 Subject: [PATCH 12/21] domain: update manual Signed-off-by: Krishnan Winter --- docs/manual.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index 9a3e250b3..85085f0d8 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -189,7 +189,7 @@ Runnable PDs of the same priority are scheduled in a round-robin manner. #### Domain scheduling (experimental) -If a Microkit system is built with a domain supported (`release_domain, debug_domain`) config, the PD can be assigned to a scheduling **domain** in the system description. If a PD is assigned to a domain, then the PD will only be allowed to execute when that domain is active. By default, PDs are assigned to domain 0. Which domain is active at any given point in time is determined by the [domain schedule](#domain). +If a Microkit system is built with a domain supported (`release_domain, debug_domain`) config, the PD can be assigned to a scheduling **domain** in the system description. If a PD is assigned to a domain, then the PD will only be allowed to execute when that domain is active. Which domain is active at any given point in time is determined by the [domain schedule](#domain). ## Virtual Machines {#vm} @@ -1158,11 +1158,11 @@ The `domain` element has the following attributes: The `name` attribute of each `domain` element can be referenced in the `domain` attribute of a `protection_domain` element. The `domain_idx_shift` element has the following attribute: -* `shift`: This is the start index of where we will construct our schedule. So if we shift by 5, we will begin constructing -the domain schedule from index 5 onwards. +* `shift`: This is the start index of where we will construct our schedule. So if we shift by 5, we will begin constructing the domain schedule from index 5 onwards. If not specified, no shift will be applied, and we will start constructing the schedule from index 0. + The `domain_start` element has the following attribute: -* `index`: This is the start index of the domain schedule. When the kernel reaches the end of the domain schedule, it will wrap around to this index again. This index is an offset into the user defined schedule, and not an absolute index. +* `index`: This is the start index of the domain schedule. When the kernel reaches the end of the domain schedule, it will wrap around to this index again. This index is an offset into the user defined schedule, and not an absolute index. If no domain start index is set, then the Microkit tool will set this to 0 by default. The `domain_schedule` element is only valid if the using one of the domain configs (`release_domains`, `debug_domains`). From a02c8e583e81666985d5cb860ab474eedb58d202 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Fri, 20 Mar 2026 16:27:39 +1100 Subject: [PATCH 13/21] example: Add hello domain example Signed-off-by: Krishnan Winter --- example/hello_domains/Makefile | 70 ++++++++++++++++++++++++++++++ example/hello_domains/README.md | 22 ++++++++++ example/hello_domains/hello.c | 26 +++++++++++ example/hello_domains/hello.system | 25 +++++++++++ 4 files changed, 143 insertions(+) create mode 100644 example/hello_domains/Makefile create mode 100644 example/hello_domains/README.md create mode 100644 example/hello_domains/hello.c create mode 100644 example/hello_domains/hello.system diff --git a/example/hello_domains/Makefile b/example/hello_domains/Makefile new file mode 100644 index 000000000..0773536c1 --- /dev/null +++ b/example/hello_domains/Makefile @@ -0,0 +1,70 @@ +# +# Copyright 2021, Breakaway Consulting Pty. Ltd. +# +# 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 + +HELLO_OBJS := hello.o + +IMAGES := hello.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)/%.o: %.c Makefile + $(CC) -c $(CFLAGS) $< -o $@ + +$(BUILD_DIR)/hello.elf: $(addprefix $(BUILD_DIR)/, $(HELLO_OBJS)) + $(LD) $(LDFLAGS) $^ $(LIBS) -o $@ + +$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) hello.system + $(MICROKIT_TOOL) hello.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) diff --git a/example/hello_domains/README.md b/example/hello_domains/README.md new file mode 100644 index 000000000..b2d456c86 --- /dev/null +++ b/example/hello_domains/README.md @@ -0,0 +1,22 @@ + +# Example - Hello World + +This is a basic hello world example with domains. There are three protection +domains, all with the same source ELF. Each protection domain is assigned to +its own domain. The domain schedule will infinitely cycle through these domains. + +All supported platforms are supported in this example. + +## Building + +```sh +mkdir build +make BUILD_DIR=build MICROKIT_BOARD= MICROKIT_CONFIG= MICROKIT_SDK=/path/to/sdk +``` + +## Running + +See instructions for your board in the manual. diff --git a/example/hello_domains/hello.c b/example/hello_domains/hello.c new file mode 100644 index 000000000..cfa88574c --- /dev/null +++ b/example/hello_domains/hello.c @@ -0,0 +1,26 @@ +/* + * Copyright 2021, Breakaway Consulting Pty. Ltd. + * + * SPDX-License-Identifier: BSD-2-Clause + */ +#include +#include + +void init(void) +{ + for (uint64_t i = 0; i < 99999999; i++) { + if (i == 99999998) { + microkit_dbg_puts("hello, world from "); + microkit_dbg_puts(microkit_name); + microkit_dbg_puts("\n"); + i = 0; + } else { + asm("nop"); + } + } + +} + +void notified(microkit_channel ch) +{ +} diff --git a/example/hello_domains/hello.system b/example/hello_domains/hello.system new file mode 100644 index 000000000..d02c5c9fe --- /dev/null +++ b/example/hello_domains/hello.system @@ -0,0 +1,25 @@ + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file From b9b0b30f6b50f79c567fa6ebd32f42f180b7edb5 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Tue, 24 Mar 2026 12:39:52 +1100 Subject: [PATCH 14/21] domains: Timer freq and monitor name checking Signed-off-by: Krishnan Winter --- docs/manual.md | 2 +- tool/microkit/src/capdl/builder.rs | 25 ++++++++++++++++++++++--- tool/microkit/src/main.rs | 3 +++ tool/microkit/src/sdf.rs | 11 +---------- tool/microkit/src/sel4.rs | 3 ++- 5 files changed, 29 insertions(+), 15 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index 85085f0d8..2073357a6 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -1153,7 +1153,7 @@ The `domain_schedule` element, by default, has a list of up to 256 `domain` chil The `domain` element has the following attributes: * `name`: Name of the domain. -* `length`: Length of time the domain will run each time it is active, in milliseconds. +* `length`: Length of time the domain will run each time it is active, in milliseconds on Aarch64 and Riscv64. On x86 this length is currently defined in ticks as we don't have a static definition of the timer frequency. The `name` attribute of each `domain` element can be referenced in the `domain` attribute of a `protection_domain` element. diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 30ffbe062..97d601a31 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -107,6 +107,8 @@ pub const SLOT_SIZE: u64 = 1 << SLOT_BITS; pub type FrameFill = Fill; pub type CapDLNamedObject = NamedObject; +const MS_IN_S: u64 = 1000; + pub struct ExpectedAllocation { pub ut_idx: usize, pub paddr: u64, @@ -404,6 +406,16 @@ pub fn build_capdl_spec( for (monitor_idx, monitor_elf) in monitor_elfs.iter().enumerate() { let monitor_name = format!("{MONITOR_PD_NAME}_{monitor_idx}"); + // Make sure that no other PD has the same name as this monitor + for pd in system.protection_domains.iter() { + if pd.name == monitor_name { + return Err(format!( + "Error: User defined PD name clashes with monitor name '{}'", + monitor_name, + )); + } + } + let monitor_name_str = monitor_name.as_str(); let monitor_tcb_obj_id = { spec_container @@ -1109,9 +1121,16 @@ pub fn build_capdl_spec( if system.domain_schedule.is_some() { let mut domain_schedule: Vec = Vec::new(); - // We need to convert from the milliseconds that the user defines in the - // sdf to the kernel scheduler ticks. - let ticks_in_ms = kernel_config.timer_freq.unwrap() / 1000; + // We want to convert from the milliseconds that the user defines in the + // sdf to the kernel scheduler ticks. If we are on x86, we won't necessarily + // have a static definition of the timer frequency. We will express the + // domain timeslices in ticks. + let ticks_in_ms = if kernel_config.timer_freq.is_some() { + kernel_config.timer_freq.unwrap() / MS_IN_S + } else { + 1 + }; + for sched_entry in system.domain_schedule.as_ref().unwrap().schedule.iter() { domain_schedule.push(DomainSchedEntry{ id: sched_entry.id, diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index fc4d753a7..82587bb17 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -502,8 +502,11 @@ fn main() -> Result<(), String> { _ => None, }; + // TODO - x86 builds do not have to statically define PC99_TSC_FREQUENCY, so we are + // defaulting to using timer ticks. Need to have a better solution for this problem let timer_freq = match arch { Arch::Aarch64 => Some(json_str_as_u64(&kernel_config_json, "TIMER_FREQUENCY")? as u64), + Arch::Riscv64 => Some(json_str_as_u64(&kernel_config_json, "TIMER_FREQUENCY")? as u64), _ => None, }; diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 7743d0ef5..5d4745119 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -619,7 +619,7 @@ impl ProtectionDomain { if config.num_domain_schedules > 1 { return Err(format!("Protection domain {} specifies a domain {} but system does not specify a domain schedule", name, domain)); } else { - return Err("Assigning PDs to domains is only supported if SDK is built with --experimental-domain-support".to_string()); + return Err("Assigning PDs to domains is only supported built with a config that supports domains".to_string()); } } (_, _) => {} @@ -1829,8 +1829,6 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result { @@ -1890,13 +1888,6 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result, /// ARM-specific, number of physical address bits pub arm_pa_size_bits: Option, From 18da0655edddc7392373ebd69ff0e095d3503ace Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Tue, 24 Mar 2026 14:37:17 +1100 Subject: [PATCH 15/21] builder: use [] not get for monitor info Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 97d601a31..57e8eb4e8 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -585,8 +585,8 @@ pub fn build_capdl_spec( let mon_pd_idx = mon_pd_idx_by_dom[pd_domain_id as usize]; // Get this PD's monitor info - let mon_cnode_obj_id = *mon_cnode_id_by_dom.get(pd_domain_id as usize).unwrap(); - let mon_fault_ep_obj_id = *mon_fault_ep_id_by_dom.get(pd_domain_id as usize).unwrap(); + let mon_cnode_obj_id = mon_cnode_id_by_dom[pd_domain_id as usize]; + let mon_fault_ep_obj_id = mon_fault_ep_id_by_dom[pd_domain_id as usize]; let mut caps_to_bind_to_tcb: Vec = Vec::new(); let mut caps_to_insert_to_pd_cspace: Vec = Vec::new(); From 329cd2559a493fa4f99c13086539ed1c0639f1da Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Tue, 24 Mar 2026 14:57:07 +1100 Subject: [PATCH 16/21] domains: clean up error checking Signed-off-by: Krishnan Winter --- tool/microkit/src/sdf.rs | 33 ++++++++++++--------------------- 1 file changed, 12 insertions(+), 21 deletions(-) diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 5d4745119..f4f778a11 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -2190,35 +2190,26 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result= dom_sched.schedule.len() as u64 { - return Err(format!( - "Error: Domain index of '{}' exceeds domain schedule length '{}'. NOTE: Domain start index starts at 0.", - dom_sched.domain_start_idx.unwrap(), - dom_sched.schedule.len(), - )) - } - - if dom_sched.domain_start_idx.is_some() && - dom_sched.domain_start_idx.unwrap() + dom_shift >= config.num_domain_schedules - { + // Checking start index against the length of the user defined schedule + if dom_start_idx >= schedule_len { return Err(format!( - "Error: Setting domain start index to '{}' when max schedule length is '{}'.", + "Error: Domain index of '{}' is out of bounds for domain schedule length '{}'. Note that the schedule is 0 indexed.", dom_sched.domain_start_idx.unwrap(), - dom_sched.schedule.len() + schedule_len )) } - let schedule_len: u64 = dom_sched.schedule.len() as u64; - if schedule_len + dom_shift > config.num_domain_schedules { + // Make sure our schedule length, including the shift, is in bounds of + // the kernel configured max number of schedules. + if schedule_len + dom_shift >= config.num_domain_schedules { return Err(format!( - "Error: Schedule length '{}' exceeds max schedule length '{}'.", + "Error: Schedule length '{}' with shift of '{}' exceeds max schedule length '{}'.", schedule_len, + dom_shift, config.num_domain_schedules, )) } From 0fa19718add42514cd4c145c81fd3a0f74d205f9 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Tue, 24 Mar 2026 15:41:29 +1100 Subject: [PATCH 17/21] run rust-fmt and clippy fix Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 40 ++++++++++++-------- tool/microkit/src/capdl/packaging.rs | 14 ++++--- tool/microkit/src/main.rs | 7 +++- tool/microkit/src/sdf.rs | 56 ++++++++++++++-------------- tool/microkit/src/symbols.rs | 17 ++------- 5 files changed, 70 insertions(+), 64 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 57e8eb4e8..626d0c626 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -11,8 +11,8 @@ use std::{ }; use sel4_capdl_initializer_types::{ - object, CapTableEntry, Fill, FillEntry, FillEntryContent, NamedObject, Object, ObjectId, Spec, - Word, DomainSchedEntry, + object, CapTableEntry, DomainSchedEntry, Fill, FillEntry, FillEntryContent, NamedObject, + Object, ObjectId, Spec, Word, }; use crate::{ @@ -410,8 +410,7 @@ pub fn build_capdl_spec( for pd in system.protection_domains.iter() { if pd.name == monitor_name { return Err(format!( - "Error: User defined PD name clashes with monitor name '{}'", - monitor_name, + "Error: User defined PD name clashes with monitor name '{monitor_name}'", )); } } @@ -432,7 +431,8 @@ pub fn build_capdl_spec( // Create monitor fault endpoint object + cap let mon_fault_ep_obj_id = capdl_util_make_endpoint_obj(&mut spec_container, monitor_name_str, true); - let mon_fault_ep_cap = capdl_util_make_endpoint_cap(mon_fault_ep_obj_id, true, true, true, 0); + let mon_fault_ep_cap = + capdl_util_make_endpoint_cap(mon_fault_ep_obj_id, true, true, true, 0); mon_fault_ep_id_by_dom.push(mon_fault_ep_obj_id); @@ -593,7 +593,13 @@ pub fn build_capdl_spec( // Step 3-1: Create TCB and VSpace with all ELF loadable frames mapped in. let pd_tcb_obj_id = spec_container - .add_elf_to_spec(kernel_config, &pd.name, pd.cpu, ElfIndex::SystemElf(pd_global_idx), elf_obj) + .add_elf_to_spec( + kernel_config, + &pd.name, + pd.cpu, + ElfIndex::SystemElf(pd_global_idx), + elf_obj, + ) .unwrap(); let pd_vspace_obj_id = capdl_util_get_vspace_id_from_tcb_id(&spec_container, pd_tcb_obj_id); @@ -1132,21 +1138,25 @@ pub fn build_capdl_spec( }; for sched_entry in system.domain_schedule.as_ref().unwrap().schedule.iter() { - domain_schedule.push(DomainSchedEntry{ + domain_schedule.push(DomainSchedEntry { id: sched_entry.id, time: sched_entry.length * ticks_in_ms, }); } spec_container.spec.domain_schedule = Some(domain_schedule); - spec_container.spec.domain_set_start = system.domain_schedule - .as_ref() - .unwrap() - .domain_start_idx.map(|idx| Word(idx)); - spec_container.spec.domain_idx_shift = system.domain_schedule - .as_ref() - .unwrap() - .domain_idx_shift.map(|shift| Word(shift)); + spec_container.spec.domain_set_start = system + .domain_schedule + .as_ref() + .unwrap() + .domain_start_idx + .map(Word); + spec_container.spec.domain_idx_shift = system + .domain_schedule + .as_ref() + .unwrap() + .domain_idx_shift + .map(Word); } // ********************************* diff --git a/tool/microkit/src/capdl/packaging.rs b/tool/microkit/src/capdl/packaging.rs index a319d0c1b..83ed7ea19 100644 --- a/tool/microkit/src/capdl/packaging.rs +++ b/tool/microkit/src/capdl/packaging.rs @@ -5,10 +5,10 @@ // use crate::{ + capdl::spec::ElfIndex, capdl::{initialiser::CapDLInitialiser, CapDLSpecContainer}, elf::ElfFile, sel4::{Config, PageSize}, - capdl::spec::{ElfIndex}, }; pub fn pack_spec_into_initial_task( @@ -29,16 +29,18 @@ pub fn pack_spec_into_initial_task( match d.elf_id { ElfIndex::SystemElf(elf_id) => { buf.copy_from_slice( - &system_elfs[elf_id].segments[d.elf_seg_idx].data()[d.elf_seg_data_range.clone()], + &system_elfs[elf_id].segments[d.elf_seg_idx].data() + [d.elf_seg_data_range.clone()], ); } ElfIndex::MonitorElf(elf_id) => { buf.copy_from_slice( - &monitor_elfs[elf_id].segments[d.elf_seg_idx].data()[d.elf_seg_data_range.clone()], + &monitor_elfs[elf_id].segments[d.elf_seg_idx].data() + [d.elf_seg_data_range.clone()], ); } } - + compress_frames }, ); @@ -52,7 +54,9 @@ pub fn pack_spec_into_initial_task( match build_config { "smp-debug" | "debug" | "debug_domains" => {} // We don't copy over the object names as there is no debug printing in these configuration to save memory. - "release" | "release_domains" | "benchmark" | "smp-release" | "smp-benchmark" => named_obj.name = None, + "release" | "release_domains" | "benchmark" | "smp-release" | "smp-benchmark" => { + named_obj.name = None + } _ => panic!("unknown configuration {build_config}"), }; } diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index 82587bb17..8eb10bbc8 100644 --- a/tool/microkit/src/main.rs +++ b/tool/microkit/src/main.rs @@ -687,12 +687,15 @@ fn main() -> Result<(), String> { spec_need_refinement = false; // Patch all the required symbols in the Monitor and PDs according to the Microkit's requirements - if let Err(err) = patch_symbols(&kernel_config, &mut system_elfs, &mut monitor_elfs, &system) { + if let Err(err) = + patch_symbols(&kernel_config, &mut system_elfs, &mut monitor_elfs, &system) + { eprintln!("ERROR: {err}"); std::process::exit(1); } - let mut spec_container = build_capdl_spec(&kernel_config, &mut system_elfs, &mut monitor_elfs, &system)?; + let mut spec_container = + build_capdl_spec(&kernel_config, &mut system_elfs, &mut monitor_elfs, &system)?; pack_spec_into_initial_task( &kernel_config, args.config, diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index f4f778a11..a1dc9f453 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -21,8 +21,8 @@ use crate::sel4::{ }; use crate::util::{ranges_overlap, str_to_bool}; use crate::MAX_PDS; -use std::collections::HashSet; use std::collections::HashMap; +use std::collections::HashSet; use std::fmt::Display; use std::path::{Path, PathBuf}; @@ -608,16 +608,16 @@ impl ProtectionDomain { (Some(domain_schedule), Ok(domain_name)) => { let domain_id_get = domain_schedule.domain_ids.get(domain_name); if domain_id_get.is_none() { - return Err(format!("Protection domain {} specifies a domain {} that is not in the domain schedule", name, domain_name)); + return Err(format!("Protection domain {name} specifies a domain {domain_name} that is not in the domain schedule")); } domain_id = Some(*domain_id_get.unwrap()); } (Some(_), _) => { - return Err(format!("System specifies a domain schedule but protection domain {} does not specify a domain", name)) + return Err(format!("System specifies a domain schedule but protection domain {name} does not specify a domain")) } (_, Ok(domain)) => { if config.num_domain_schedules > 1 { - return Err(format!("Protection domain {} specifies a domain {} but system does not specify a domain schedule", name, domain)); + return Err(format!("Protection domain {name} specifies a domain {domain} but system does not specify a domain schedule")); } else { return Err("Assigning PDs to domains is only supported built with a config that supports domains".to_string()); } @@ -1029,7 +1029,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, domain_schedule)?; + let child_pd = + ProtectionDomain::from_xml(config, xml_sdf, &child, true, domain_schedule)?; if let Some(setvar_id) = &child_pd.setvar_id { let setvar = SysSetVar { @@ -1127,9 +1128,7 @@ impl DomainSchedule { node: &roxmltree::Node, ) -> Result { if config.num_domains <= 1 { - return Err(format!( - "Error: Attempting to set a domain schedule when kernel config does not support more than 1 domain", - )); + return Err("Error: Attempting to set a domain schedule when kernel config does not support more than 1 domain".to_string()); } let pos = xml_sdf.doc.text_pos_at(node.range().start); @@ -1188,34 +1187,28 @@ impl DomainSchedule { return Err(format!( "Error: Duplicate setting of domain start index, already set to '{}'", domain_start_idx.unwrap() - )) + )); } check_attributes(xml_sdf, &child, &["index"])?; let start_index = checked_lookup(xml_sdf, &child, "index")?.parse::(); if start_index.is_err() { - return Err(format!( - "Error: invalid domain start index", - )) + return Err("Error: invalid domain start index".to_string()); } domain_start_idx = Some(start_index.unwrap()); - } "domain_idx_shift" => { if domain_idx_shift.is_some() { return Err(format!( "Error: Duplicate setting of domain index shift, already set to '{}'", domain_idx_shift.unwrap() - )) + )); } check_attributes(xml_sdf, &child, &["shift"])?; let index_shift = checked_lookup(xml_sdf, &child, "shift")?.parse::(); if index_shift.is_err() { - return Err(format!( - "Error: invalid domain index shift", - )) + return Err("Error: invalid domain index shift".to_string()); } domain_idx_shift = Some(index_shift.unwrap()); - } _ => { return Err(format!( @@ -1224,7 +1217,6 @@ impl DomainSchedule { loc_string(xml_sdf, pos) )); } - } } @@ -1808,9 +1800,13 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result { - root_pds.push(ProtectionDomain::from_xml(config, &xml_sdf, &child, false, &domain_schedule)?) - } + "protection_domain" => root_pds.push(ProtectionDomain::from_xml( + config, + &xml_sdf, + &child, + false, + &domain_schedule, + )?), "channel" => channel_nodes.push(child), "memory_region" => mrs.push(SysMemoryRegion::from_xml(config, &xml_sdf, &child)?), "virtual_machine" => { @@ -1819,7 +1815,7 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result { if config.num_domain_schedules > 1 { if let Some(domain_schedule_node) = system @@ -1827,7 +1823,11 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result Result Result= config.num_domain_schedules { return Err(format!( "Error: Schedule length '{}' with shift of '{}' exceeds max schedule length '{}'.", - schedule_len, - dom_shift, - config.num_domain_schedules, - )) + schedule_len, dom_shift, config.num_domain_schedules, + )); } } diff --git a/tool/microkit/src/symbols.rs b/tool/microkit/src/symbols.rs index c77297673..7377add49 100644 --- a/tool/microkit/src/symbols.rs +++ b/tool/microkit/src/symbols.rs @@ -8,7 +8,7 @@ use std::{cmp::min, collections::HashMap}; use crate::{ elf::ElfFile, - sdf::{self, SysMemoryRegion, SystemDescription, ProtectionDomain}, + sdf::{self, ProtectionDomain, SysMemoryRegion, SystemDescription}, sel4::{Arch, Config}, util::{monitor_serialise_names, monitor_serialise_u64_vec}, MAX_PDS, MAX_VMS, PD_MAX_NAME_LENGTH, VM_MAX_NAME_LENGTH, @@ -35,15 +35,9 @@ pub fn patch_symbols( .filter(|pd| pd.domain_id.unwrap_or(0) == mon_idx as u8) .collect(); - let pd_names: Vec = filtered_pds - .iter() - .map(|pd| pd.name.clone()) - .collect(); + let pd_names: Vec = filtered_pds.iter().map(|pd| pd.name.clone()).collect(); monitor_elf - .write_symbol( - "pd_names_len", - &filtered_pds.len().to_le_bytes(), - ) + .write_symbol("pd_names_len", &filtered_pds.len().to_le_bytes()) .unwrap(); monitor_elf .write_symbol( @@ -90,10 +84,7 @@ pub fn patch_symbols( .unwrap(); monitor_elf - .write_symbol( - "monitor_name", - format!("monitor_{}", mon_idx).as_bytes() - ) + .write_symbol("monitor_name", format!("monitor_{mon_idx}").as_bytes()) .unwrap(); } From 9f7fad19423a2aa55df096b4a05199eb0e56176c Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Thu, 26 Mar 2026 11:24:12 +1100 Subject: [PATCH 18/21] domains: Move domain configs to elaborate configs Signed-off-by: Krishnan Winter --- build_sdk.py | 32 ++++++++-------------------- docs/manual.md | 12 ++++++----- tool/microkit/src/capdl/packaging.rs | 4 ++-- 3 files changed, 18 insertions(+), 30 deletions(-) diff --git a/build_sdk.py b/build_sdk.py index 7e7bb8c60..32d235e52 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -465,29 +465,6 @@ class KernelPath: } }, ), - # TODO: This is experimental for now, do this in a better way - ConfigInfo( - name="release_domains", - debug=False, - kernel_options={ - "KernelNumDomains": 256, - "KernelNumDomainSchedules": 256, - }, - kernel_options_arch={}, - ), - ConfigInfo( - name="debug_domains", - debug=True, - kernel_options={ - "KernelDebugBuild": True, - "KernelPrinting": True, - "KernelVerificationBuild": False, - "KernelNumDomains": 256, - "KernelNumDomainSchedules": 256, - }, - kernel_options_arch={}, - ), - ) @@ -512,6 +489,15 @@ def elaborate_all_board_configs(board: BoardInfo) -> list[ConfigInfo]: } elaborated_configs.append(config) + for config in SUPPORTED_CONFIGS: + config = copy.deepcopy(config) + config.name = f"domain-{config.name}" + config.kernel_options |= { + "KernelNumDomains": 32, + "KernelNumDomainSchedules": 64, + } + elaborated_configs.append(config) + return elaborated_configs diff --git a/docs/manual.md b/docs/manual.md index 2073357a6..f97c0cc9b 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -187,10 +187,12 @@ Runnable PDs of the same priority are scheduled in a round-robin manner. **Passive** determines whether the PD is passive. A passive PD will have its scheduling context revoked after initialisation and then bound instead to the PD's notification object. This means the PD will be scheduled on receiving a notification, whereby it will run on the notification's scheduling context. When the PD receives a *protected procedure* by another PD or a *fault* caused by a child PD, the passive PD will run on the scheduling context of the callee. -#### Domain scheduling (experimental) +#### Domain scheduling If a Microkit system is built with a domain supported (`release_domain, debug_domain`) config, the PD can be assigned to a scheduling **domain** in the system description. If a PD is assigned to a domain, then the PD will only be allowed to execute when that domain is active. Which domain is active at any given point in time is determined by the [domain schedule](#domain). +The user can describe up to 32 distinct domains by default, and 64 different domain schedule entries. These defaults can be changed in `build_sdk.py` in `elaborate_all_board_configs`. There are two kernel config options: `KernelNumDomains` and `KernelNumDomainSchedules`. + ## Virtual Machines {#vm} A *virtual machine* (VM) is a runtime abstraction for running guest operating systems in Microkit. It is similar @@ -351,7 +353,7 @@ delivered to another PD, the fault being handled depends on when the parent PD i I/O ports are x86 mechanisms to access certain physical devices (e.g. PC serial ports or PCI) using the `in` and `out` CPU instructions. The system description specifies if a protection domain have access to certain port address ranges. These accesses will be executed by seL4 and the result returned to protection domains. -# Domain Scheduling (experimental) {#domain} +# Domain Scheduling {#domain} Microkit can be built with experimental support for a method of temporally isolating different groups of PDs called domain scheduling. On a Microkit system, only one domain is active at a time, and the kernel alternates between domains according to a round-robin schedule. A domain schedule consists of an ordered list of domains, each with an associated length of time to run. The kernel will then activate a domain for the specified length of time; after that time has passed, it will deactivate that domain and activate the next domain for its length of time, and so on, proceeding through the list until it wraps back to the first domain. PDs are assigned to domains, such that when a certain domain is active, only PDs belonging to that domain will be scheduled to run. @@ -1146,9 +1148,9 @@ The `end` element has the following attributes: The `id` is passed to the PD in the `notified` and `protected` entry points. The `id` should be passed to the `microkit_notify` and `microkit_ppcall` functions. -## `domain_schedule` (experimental) +## `domain_schedule` -The `domain_schedule` element, by default, has a list of up to 256 `domain` child elements. This can be configured by changing the number of schedule entries defined in the `release_domains` and `debug_domains` configs in `build_sdk.py`. Each child specifies a particular timeslice in the domain schedule and the order of the child elements specifies the order in which the timeslices will be scheduled. A domain may be named more than once in the schedule, in which case the domain will have multiple timeslices in the schedule. +The `domain_schedule` element, by default, has a list of up to 64 `domain` child elements, and can describe 32 different domains. (bounded by the kernel config). This can be configured by changing the number of schedule entries defined in `elaborate_all_board_configs` in `build_sdk.py`. Each child specifies a particular timeslice in the domain schedule and the order of the child elements specifies the order in which the timeslices will be scheduled. A domain may be named more than once in the schedule, in which case the domain will have multiple timeslices in the schedule. The `domain` element has the following attributes: @@ -1164,7 +1166,7 @@ The `domain_idx_shift` element has the following attribute: The `domain_start` element has the following attribute: * `index`: This is the start index of the domain schedule. When the kernel reaches the end of the domain schedule, it will wrap around to this index again. This index is an offset into the user defined schedule, and not an absolute index. If no domain start index is set, then the Microkit tool will set this to 0 by default. -The `domain_schedule` element is only valid if the using one of the domain configs (`release_domains`, `debug_domains`). +The `domain_schedule` element is only valid if the using one of the domain configs (`domain-release`, `domain-debug`, `domain-benchmark`). # Board Support Packages {#bsps} diff --git a/tool/microkit/src/capdl/packaging.rs b/tool/microkit/src/capdl/packaging.rs index 83ed7ea19..a63e84a2f 100644 --- a/tool/microkit/src/capdl/packaging.rs +++ b/tool/microkit/src/capdl/packaging.rs @@ -52,9 +52,9 @@ pub fn pack_spec_into_initial_task( for named_obj in output_spec.objects.iter_mut() { match build_config { - "smp-debug" | "debug" | "debug_domains" => {} + "smp-debug" | "debug" | "domain-debug" => {} // We don't copy over the object names as there is no debug printing in these configuration to save memory. - "release" | "release_domains" | "benchmark" | "smp-release" | "smp-benchmark" => { + "release" | "benchmark" | "smp-release" | "smp-benchmark" | "domain-release" | "domain-benchmark" => { named_obj.name = None } _ => panic!("unknown configuration {build_config}"), From 19b31b1c39b3b5c5e301f2b1e0301d3ada9dc051 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Wed, 25 Mar 2026 12:14:30 +1100 Subject: [PATCH 19/21] domains: switch from milliseconds to micro Signed-off-by: Krishnan Winter --- docs/manual.md | 2 +- example/hello_domains/hello.system | 8 ++++---- tool/microkit/src/capdl/builder.rs | 6 +++--- tool/microkit/src/capdl/packaging.rs | 5 ++--- 4 files changed, 10 insertions(+), 11 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index f97c0cc9b..c6cd09860 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -1155,7 +1155,7 @@ The `domain_schedule` element, by default, has a list of up to 64 `domain` child The `domain` element has the following attributes: * `name`: Name of the domain. -* `length`: Length of time the domain will run each time it is active, in milliseconds on Aarch64 and Riscv64. On x86 this length is currently defined in ticks as we don't have a static definition of the timer frequency. +* `length`: Length of time the domain will run each time it is active, in microseconds on Aarch64 and Riscv64. On x86 this length is currently defined in ticks as we don't have a static definition of the timer frequency. The `name` attribute of each `domain` element can be referenced in the `domain` attribute of a `protection_domain` element. diff --git a/example/hello_domains/hello.system b/example/hello_domains/hello.system index d02c5c9fe..7d44919e8 100644 --- a/example/hello_domains/hello.system +++ b/example/hello_domains/hello.system @@ -6,9 +6,9 @@ --> - - - + + + @@ -18,7 +18,7 @@ - + diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 626d0c626..12b319701 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -107,7 +107,7 @@ pub const SLOT_SIZE: u64 = 1 << SLOT_BITS; pub type FrameFill = Fill; pub type CapDLNamedObject = NamedObject; -const MS_IN_S: u64 = 1000; +const US_IN_S: u64 = 1000000; pub struct ExpectedAllocation { pub ut_idx: usize, @@ -1127,12 +1127,12 @@ pub fn build_capdl_spec( if system.domain_schedule.is_some() { let mut domain_schedule: Vec = Vec::new(); - // We want to convert from the milliseconds that the user defines in the + // We want to convert from the microseconds that the user defines in the // sdf to the kernel scheduler ticks. If we are on x86, we won't necessarily // have a static definition of the timer frequency. We will express the // domain timeslices in ticks. let ticks_in_ms = if kernel_config.timer_freq.is_some() { - kernel_config.timer_freq.unwrap() / MS_IN_S + kernel_config.timer_freq.unwrap() / US_IN_S } else { 1 }; diff --git a/tool/microkit/src/capdl/packaging.rs b/tool/microkit/src/capdl/packaging.rs index a63e84a2f..d26c3b84b 100644 --- a/tool/microkit/src/capdl/packaging.rs +++ b/tool/microkit/src/capdl/packaging.rs @@ -54,9 +54,8 @@ pub fn pack_spec_into_initial_task( match build_config { "smp-debug" | "debug" | "domain-debug" => {} // We don't copy over the object names as there is no debug printing in these configuration to save memory. - "release" | "benchmark" | "smp-release" | "smp-benchmark" | "domain-release" | "domain-benchmark" => { - named_obj.name = None - } + "release" | "benchmark" | "smp-release" | "smp-benchmark" | "domain-release" + | "domain-benchmark" => named_obj.name = None, _ => panic!("unknown configuration {build_config}"), }; } From 5c536acdc11b125a0df69bc47f2e86504faf4fea Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Wed, 25 Mar 2026 12:25:01 +1100 Subject: [PATCH 20/21] domain: set KernelTimerFreq config Signed-off-by: Krishnan Winter --- build_sdk.py | 1 + 1 file changed, 1 insertion(+) diff --git a/build_sdk.py b/build_sdk.py index 32d235e52..86ebf7d6c 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -493,6 +493,7 @@ def elaborate_all_board_configs(board: BoardInfo) -> list[ConfigInfo]: config = copy.deepcopy(config) config.name = f"domain-{config.name}" config.kernel_options |= { + "KernelTimerFrequency": True, "KernelNumDomains": 32, "KernelNumDomainSchedules": 64, } From 054ec742907fd8cc1b6c3fcd190ca71f6efeebd8 Mon Sep 17 00:00:00 2001 From: Krishnan Winter Date: Wed, 25 Mar 2026 15:38:47 +1100 Subject: [PATCH 21/21] clippy: use if let Some() Signed-off-by: Krishnan Winter --- tool/microkit/src/capdl/builder.rs | 37 +++++++++++------------------- tool/microkit/src/sdf.rs | 12 ++++------ 2 files changed, 19 insertions(+), 30 deletions(-) diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index 12b319701..45fbf5e8c 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -700,19 +700,16 @@ pub fn build_capdl_spec( )); // Step 3-5 Create fault Endpoint cap to parent/monitor - let pd_fault_ep_cap = if pd.parent.is_none() { - let badge: u64 = mon_pd_idx as u64 + 1; - capdl_util_make_endpoint_cap(mon_fault_ep_obj_id, true, true, true, badge) - } else { + let pd_fault_ep_cap = if let Some(parent) = pd.parent { // @kwinter: Should we enforce domain boundaries here? - assert!(pd_global_idx > pd.parent.unwrap()); + assert!(pd_global_idx > parent); let badge: u64 = FAULT_BADGE | pd.id.unwrap(); - let parent_ep_obj_id = &pd_id_to_ep_id[&pd.parent.unwrap()]; + let parent_ep_obj_id = &pd_id_to_ep_id[&parent]; let fault_ep_cap = capdl_util_make_endpoint_cap(*parent_ep_obj_id, true, true, true, badge); // Allow the parent PD to access the child's TCB: - let parent_cspace_obj_id = &pd_id_to_cspace_id[&pd.parent.unwrap()]; + let parent_cspace_obj_id = &pd_id_to_cspace_id[&parent]; capdl_util_insert_cap_into_cspace( &mut spec_container, *parent_cspace_obj_id, @@ -721,7 +718,11 @@ pub fn build_capdl_spec( ); fault_ep_cap + } else { + let badge: u64 = mon_pd_idx as u64 + 1; + capdl_util_make_endpoint_cap(mon_fault_ep_obj_id, true, true, true, badge) }; + caps_to_insert_to_pd_cspace.push(capdl_util_make_cte( PD_FAULT_EP_CAP_IDX as u32, pd_fault_ep_cap.clone(), @@ -1125,19 +1126,19 @@ pub fn build_capdl_spec( // Step 5. Parse domain schedule // ********************************* - if system.domain_schedule.is_some() { + if let Some(sys_domain_schedule) = &system.domain_schedule { let mut domain_schedule: Vec = Vec::new(); // We want to convert from the microseconds that the user defines in the // sdf to the kernel scheduler ticks. If we are on x86, we won't necessarily // have a static definition of the timer frequency. We will express the // domain timeslices in ticks. - let ticks_in_ms = if kernel_config.timer_freq.is_some() { - kernel_config.timer_freq.unwrap() / US_IN_S + let ticks_in_ms = if let Some(timer_freq) = kernel_config.timer_freq { + timer_freq / US_IN_S } else { 1 }; - for sched_entry in system.domain_schedule.as_ref().unwrap().schedule.iter() { + for sched_entry in sys_domain_schedule.schedule.iter() { domain_schedule.push(DomainSchedEntry { id: sched_entry.id, time: sched_entry.length * ticks_in_ms, @@ -1145,18 +1146,8 @@ pub fn build_capdl_spec( } spec_container.spec.domain_schedule = Some(domain_schedule); - spec_container.spec.domain_set_start = system - .domain_schedule - .as_ref() - .unwrap() - .domain_start_idx - .map(Word); - spec_container.spec.domain_idx_shift = system - .domain_schedule - .as_ref() - .unwrap() - .domain_idx_shift - .map(Word); + spec_container.spec.domain_set_start = sys_domain_schedule.domain_start_idx.map(Word); + spec_container.spec.domain_idx_shift = sys_domain_schedule.domain_idx_shift.map(Word); } // ********************************* diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index a1dc9f453..c6eaa1ed8 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -1183,10 +1183,10 @@ impl DomainSchedule { }); } "domain_start" => { - if domain_start_idx.is_some() { + if let Some(domain_start_idx) = domain_start_idx { return Err(format!( "Error: Duplicate setting of domain start index, already set to '{}'", - domain_start_idx.unwrap() + domain_start_idx )); } check_attributes(xml_sdf, &child, &["index"])?; @@ -1197,10 +1197,10 @@ impl DomainSchedule { domain_start_idx = Some(start_index.unwrap()); } "domain_idx_shift" => { - if domain_idx_shift.is_some() { + if let Some(domain_idx_shift) = domain_idx_shift { return Err(format!( "Error: Duplicate setting of domain index shift, already set to '{}'", - domain_idx_shift.unwrap() + domain_idx_shift )); } check_attributes(xml_sdf, &child, &["shift"])?; @@ -2185,9 +2185,7 @@ pub fn parse(filename: &str, xml: &str, config: &Config) -> Result