tool: a VM on x86-64 cannot have scheduling params

docs/manual.md

@@ -1013,13 +1013,17 @@ The `protection_domain` element has the same attributes as any other protection
 
 On x86-64, a PD with a VCPU cannot have child PDs.
 
-The `virtual_machine` element has the following attributes:
+The `virtual_machine` element has the following attribute:
 
 * `name`: A unique name for the virtual machine
-* `priority`: The priority of the virtual machine (integer 0 to 254).
+
+On ARM, it supports the following additional attributes:
+* `priority`: (optional) The priority of the virtual machine (integer 0 to 254); defaults to 0.
 * `budget`: (optional) The VM's budget in microseconds; defaults to 1,000.
 * `period`: (optional) The VM's period in microseconds; must not be smaller than the budget; defaults to the budget.
 
+On x86-64, the VM shares its scheduling parameters with the parent PD.
+
 Additionally, it supports the following child elements:
 
 * `vcpu`: (one or more) Describes the virtual CPU that will be tied to the virtual machine.

tool/microkit/src/capdl/builder.rs

@@ -720,8 +720,8 @@ pub fn build_capdl_spec(
             &mut spec_container,
             &pd.name,
             PD_SCHEDCONTEXT_EXTRA_SIZE_BITS as u8,
-            pd.period,
-            pd.budget,
+            pd.sched_params.period,
+            pd.sched_params.budget,
             0x100 + pd_global_idx as u64,
         );
         let pd_sc_cap = capdl_util_make_sc_cap(pd_sc_obj_id);
@@ -955,8 +955,8 @@ pub fn build_capdl_spec(
                         &mut spec_container,
                         &format!("{}_{}", virtual_machine.name, vcpu.id),
                         PD_SCHEDCONTEXT_EXTRA_SIZE_BITS as u8,
-                        virtual_machine.period,
-                        virtual_machine.budget,
+                        virtual_machine.sched_params.as_ref().unwrap().period,
+                        virtual_machine.sched_params.as_ref().unwrap().budget,
                         0x100 + vcpu_idx as u64,
                     );
                     caps_to_bind_to_vm_tcbs.push(capdl_util_make_cte(
@@ -982,8 +982,8 @@ pub fn build_capdl_spec(
                         extra: Box::new(object::TcbExtraInfo {
                             ipc_buffer_addr: Word(0),
                             affinity: Word(vcpu_affinity.0.into()),
-                            prio: virtual_machine.priority,
-                            max_prio: virtual_machine.priority,
+                            prio: virtual_machine.sched_params.as_ref().unwrap().priority,
+                            max_prio: virtual_machine.sched_params.as_ref().unwrap().priority,
                             // Given the use cases of VMs, for now we always give them FPU access.
                             fpu_disabled: false,
                             resume: false,
@@ -1071,8 +1071,8 @@ pub fn build_capdl_spec(
             pd_tcb.extra.ipc_buffer_addr = Word(kernel_config.pd_ipc_buffer());
             pd_tcb.extra.sp = Word(kernel_config.pd_stack_top());
             pd_tcb.extra.master_fault_ep = None; // Not used on MCS kernel.
-            pd_tcb.extra.prio = pd.priority;
-            pd_tcb.extra.max_prio = pd.priority;
+            pd_tcb.extra.prio = pd.priority();
+            pd_tcb.extra.max_prio = pd.priority();
             pd_tcb.extra.fpu_disabled = !pd.fpu;
             pd_tcb.extra.resume = true;
 

tool/microkit/src/sdf.rs

@@ -265,14 +265,19 @@ impl Display for CpuCore {
     }
 }
 
+#[derive(Debug, PartialEq, Eq)]
+pub struct SchedulingParams {
+    pub priority: u8,
+    pub budget: u64,
+    pub period: u64,
+}
+
 #[derive(Debug, PartialEq, Eq)]
 pub struct ProtectionDomain {
     /// Only populated for child protection domains
     pub id: Option<u64>,
     pub name: String,
-    pub priority: u8,
-    pub budget: u64,
-    pub period: u64,
+    pub sched_params: SchedulingParams,
     pub passive: bool,
     pub stack_size: u64,
     pub smc: bool,
@@ -338,9 +343,7 @@ pub struct VirtualMachine {
     pub vcpus: Vec<VirtualCpu>,
     pub name: String,
     pub maps: Vec<SysMap>,
-    pub priority: u8,
-    pub budget: u64,
-    pub period: u64,
+    pub sched_params: Option<SchedulingParams>,
 }
 
 #[derive(Debug, PartialEq, Eq)]
@@ -498,6 +501,10 @@ impl ProtectionDomain {
         ioports
     }
 
+    pub fn priority(&self) -> u8 {
+        self.sched_params.priority
+    }
+
     fn from_xml(
         config: &Config,
         xml_sdf: &XmlSystemDescription,
@@ -1204,11 +1211,13 @@ impl ProtectionDomain {
         Ok(ProtectionDomain {
             id,
             name,
-            // This downcast is safe as we have checked that this is less than
-            // the maximum PD priority, which fits in a u8.
-            priority: priority as u8,
-            budget,
-            period,
+            sched_params: SchedulingParams {
+                // This downcast is safe as we have checked that this is less than
+                // the maximum PD priority, which fits in a u8.
+                priority: priority as u8,
+                budget,
+                period,
+            },
             passive,
             stack_size,
             smc,
@@ -1237,33 +1246,50 @@ impl VirtualMachine {
         xml_sdf: &XmlSystemDescription,
         node: &roxmltree::Node,
     ) -> Result<VirtualMachine, String> {
-        check_attributes(xml_sdf, node, &["name", "budget", "period", "priority"])?;
-
-        let name = checked_lookup(xml_sdf, node, "name")?.to_string();
-        // If we do not have an explicit budget the period is equal to the default budget.
-        let budget = if let Some(xml_budget) = node.attribute("budget") {
-            sdf_parse_number(xml_budget, node)?
+        if config.arch == Arch::Aarch64 {
+            check_attributes(xml_sdf, node, &["name", "budget", "period", "priority"])?;
         } else {
-            BUDGET_DEFAULT
-        };
-        let period = if let Some(xml_period) = node.attribute("period") {
-            sdf_parse_number(xml_period, node)?
-        } else {
-            budget
-        };
-        if budget > period {
-            return Err(value_error(
-                xml_sdf,
-                node,
-                format!("budget ({budget}) must be less than, or equal to, period ({period})"),
-            ));
+            check_attributes(xml_sdf, node, &["name"])?;
         }
 
-        // Default to minimum priority
-        let priority = if let Some(xml_priority) = node.attribute("priority") {
-            sdf_parse_number(xml_priority, node)?
+        let name = checked_lookup(xml_sdf, node, "name")?.to_string();
+
+        let sched_params = if config.arch == Arch::Aarch64 {
+            // If we do not have an explicit budget the period is equal to the default budget.
+            let budget = if let Some(xml_budget) = node.attribute("budget") {
+                sdf_parse_number(xml_budget, node)?
+            } else {
+                BUDGET_DEFAULT
+            };
+            let period = if let Some(xml_period) = node.attribute("period") {
+                sdf_parse_number(xml_period, node)?
+            } else {
+                budget
+            };
+            if budget > period {
+                return Err(value_error(
+                    xml_sdf,
+                    node,
+                    format!("budget ({budget}) must be less than, or equal to, period ({period})"),
+                ));
+            }
+
+            // Default to minimum priority
+            let priority = if let Some(xml_priority) = node.attribute("priority") {
+                sdf_parse_number(xml_priority, node)?
+            } else {
+                0
+            };
+
+            Some(SchedulingParams {
+                // This downcast is safe as we have checked that this is less than
+                // the maximum PD priority, which fits in a u8.
+                priority: priority as u8,
+                budget,
+                period,
+            })
         } else {
-            0
+            None
         };
 
         let mut vcpus: Vec<VirtualCpu> = Vec::new();
@@ -1352,11 +1378,7 @@ impl VirtualMachine {
             vcpus,
             name,
             maps,
-            // This downcast is safe as we have checked that this is less than
-            // the maximum VM priority, which fits in a u8.
-            priority: priority as u8,
-            budget,
-            period,
+            sched_params,
         })
     }
 }
@@ -2211,17 +2233,23 @@ pub fn parse(
 
         let pd_a = &pds[ch.end_a.pd];
         let pd_b = &pds[ch.end_b.pd];
-        if ch.end_a.pp && pd_a.priority >= pd_b.priority {
+        if ch.end_a.pp && pd_a.priority() >= pd_b.priority() {
             return Err(format!(
                 "Error: PPCs must be to protection domains of strictly higher priorities; \
                         channel with PPC exists from pd {} (priority: {}) to pd {} (priority: {})",
-                pd_a.name, pd_a.priority, pd_b.name, pd_b.priority
+                pd_a.name,
+                pd_a.priority(),
+                pd_b.name,
+                pd_b.priority()
             ));
-        } else if ch.end_b.pp && pd_b.priority >= pd_a.priority {
+        } else if ch.end_b.pp && pd_b.priority() >= pd_a.priority() {
             return Err(format!(
                 "Error: PPCs must be to protection domains of strictly higher priorities; \
                         channel with PPC exists from pd {} (priority: {}) to pd {} (priority: {})",
-                pd_b.name, pd_b.priority, pd_a.name, pd_a.priority
+                pd_b.name,
+                pd_b.priority(),
+                pd_a.name,
+                pd_a.priority()
             ));
         }
 

tool/microkit/src/viper.rs

@@ -207,8 +207,8 @@ pub fn get_sdf_view(system: &SystemDescription, current_pd: usize) -> Option<Sdf
 
         view.channel_ends.push(local.id);
 
-        let local_prio = current.priority;
-        let remote_prio = system.protection_domains[remote.pd].priority;
+        let local_prio = current.priority();
+        let remote_prio = system.protection_domains[remote.pd].priority();
 
         if local.pp && local_prio < remote_prio {
             view.ppcall_targets.push(local.id);

tool/microkit/tests/sdf/vm_valid.system

@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+    Copyright 2026, UNSW
+    SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="hello" priority="254">
+        <program_image path="hello.elf" />
+        <virtual_machine name="guest">
+            <vcpu id="0" />
+        </virtual_machine>
+    </protection_domain>
+</system>

tool/microkit/tests/sdf/vm_with_priority.system

@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+    Copyright 2026, UNSW
+    SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="hello" priority="254">
+        <program_image path="hello.elf" />
+        <virtual_machine name="guest" priority="1">
+            <vcpu id="0" />
+        </virtual_machine>
+    </protection_domain>
+</system>

tool/microkit/tests/test.rs

@@ -751,6 +751,30 @@ mod protection_domain {
 mod virtual_machine {
     use super::*;
 
+    #[test]
+    fn test_vm_valid_aarch64() {
+        check_success(&DEFAULT_AARCH64_KERNEL_CONFIG, "vm_valid.system")
+    }
+
+    #[test]
+    fn test_vm_with_priority_aarch64() {
+        check_success(&DEFAULT_AARCH64_KERNEL_CONFIG, "vm_with_priority.system")
+    }
+
+    #[test]
+    fn test_vm_valid_x86_64() {
+        check_success(&DEFAULT_X86_64_KERNEL_CONFIG, "vm_valid.system")
+    }
+
+    #[test]
+    fn test_vm_with_priority_x86_64() {
+        check_error(
+            &DEFAULT_X86_64_KERNEL_CONFIG,
+            "vm_with_priority.system",
+            "Error: invalid attribute 'priority' on element 'virtual_machine'",
+        )
+    }
+
     #[test]
     fn test_vm_not_child() {
         check_error(