A VM's vCPU TCB is never assigned to its PD's domain, so domain-scheduled VMs hang

[jasonbelt]

Summary

When a protection domain containing a <virtual_machine> is placed in a scheduling domain, the VM's vCPU TCB is left in domain 0 rather than following its parent PD. The VMM and its vCPU therefore never run in the same scheduling domain, the guest's virtual timer interrupt is never delivered, and a Linux guest hangs during arch_timer probe.

In tool/microkit/src/capdl/builder.rs (tag 2.3.0), a PD's TCB picks up its domain:

// builder.rs:1106
pd_tcb.extra.domain = pd.domain;

https://github.com/seL4/microkit/blob/2.3.0/tool/microkit/src/capdl/builder.rs#L1106

but the vCPU TCB built for a <virtual_machine> is created with no domain and is never assigned one afterwards:

// builder.rs:1008-1025
let vm_vcpu_tcb_inner_obj = object::Tcb {
    slots: caps_to_bind_to_vm_tcbs,
    extra: Box::new(object::TcbExtraInfo {
        ...
        master_fault_ep: None, // Not used on MCS kernel.
        domain: None,          // <-- never set from the parent PD
    }),
};

https://github.com/seL4/microkit/blob/2.3.0/tool/microkit/src/capdl/builder.rs#L1023

There is also no way to work around this from the SDF: VirtualMachine::from_xml accepts only name, budget, period, priority, so a domain attribute on <virtual_machine> is rejected: https://github.com/seL4/microkit/blob/2.3.0/tool/microkit/src/sdf.rs#L1639

This has been diagnosed before, in au-ts/libvmm#138 (this comment), where the fix (JE-Archer/microkit#1, "tool: Set VM VCPU TCB domain to its PDs domain", merged 2024-11-12) was applied to the domains fork Microkit's domain scheduling was developed on. It appears not to have been carried over when domain scheduling was upstreamed for 2.3.0. I have re-applied that change against 2.3.0 and confirmed it resolves the hang — details under "Fix" below.

Reproducing

examples/simple from libvmm, unmodified apart from the SDF. Adding a domain schedule and putting the VMM in a non-zero domain is enough:

--- a/examples/simple/board/qemu_virt_aarch64/simple.system
+++ b/examples/simple/board/qemu_virt_aarch64/simple.system
@@ -5,6 +5,16 @@
  SPDX-License-Identifier: BSD-2-Clause
 -->
 <system>
+    <domains>
+      <domain name="domain_0" id="0" />
+      <domain name="domain_1" id="1" />
+      <domain_schedule>
+        <schedule_entry domain="domain_1" duration="800000 us" />
+        <schedule_entry domain="domain_0" duration="200000 us" />
+        <schedule_end_marker />
+      </domain_schedule>
+    </domains>
+
     <!--
      Here we give the guest 256MiB to use as RAM. Note that we use 2MiB page
      sizes for efficiency, it does not have any functional effect.
@@ -26,7 +36,7 @@
     -->
     <memory_region name="gic_vcpu" size="0x1_000" phys_addr="0x8040000" />

-    <protection_domain name="VMM" priority="254">
+    <protection_domain name="VMM" priority="254" domain="domain_1">
         <program_image path="vmm.elf" />

make MICROKIT_SDK=<sdk> MICROKIT_BOARD=qemu_virt_aarch64 qemu

The guest stops here and never resumes (left for 7 minutes; the VMM keeps being scheduled the whole time):

[    0.000000] NR_IRQS: 64, nr_irqs: 64, preallocated irqs: 0
[    0.000000] Root IRQ handler: gic_handle_irq

Expected next line, which never appears:

[    0.000000] arch_timer: cp15 timer(s) running at 62.50MHz (virt).

Evidence that it is the vtimer specifically

I instrumented the example's fault() to log microkit_msginfo_get_label() for every fault. Stock 2.3.0 throughout, same libvmm build and same guest images in every row; the only variable is the SDF:

domain schedule	VMM's domain	seL4_Fault_VPPIEvent	seL4_Fault_VMFault	guest
no	—	894	171	boots to /init
yes	domain_1	0	68	hangs as above
yes	domain_0	892	171	boots to /init

VMFaults keep being delivered in the failing case, so fault delivery in general is working — it is only the virtual timer PPI that never arrives.

The third row points the same way: putting the VMM in domain_0 makes the very same system boot with domain scheduling active, which is what you would expect if the vCPU TCB is being left in domain 0.

Fix, and confirmation that it is sufficient

Setting the vCPU TCB's domain from the containing PD, as JE-Archer/microkit#1 does, resolves it:

                              master_fault_ep: None, // Not used on MCS kernel.
-                             domain: None,
+                             domain: pd.domain,

I built the tool from source at tag 2.3.0 with only that change and dropped the resulting bin/microkit into an otherwise untouched stock 2.3.0 SDK — the kernel, loader, monitor, initialiser, libmicrokit and headers are all the stock release, so the only difference between these two rows is the one line above:

bin/microkit	kernel lines reached	seL4_Fault_VPPIEvent	guest
stock 2.3.0	49	0	hangs at gic_handle_irq
rebuilt with domain: pd.domain	264	922	boots to /init

That the fix is confined to the capDL spec the host tool emits, and needs no kernel-side change, is consistent with the diagnosis: the vCPU TCB simply never had a domain to be scheduled in.

A domain attribute on <virtual_machine> would also be useful for placing a vCPU in a different domain from its VMM, but same-domain-as-parent seems like the right default regardless.

Happy to open a PR if that would help.

Environment

• Microkit SDK 2.3.0 (qemu_virt_aarch64, debug)
• libvmm cce1c2c4af2f (main), examples/simple, with its own guest kernel and initrd
• QEMU 10.2.0, clang, macOS 26.5.1 host

[midnightveil]

This has been fixed on mainline: #586, but has not been included in a release.