vCPUs default to same core as PD managing them

I think this makes more sense, if a PD that is acting as
a VMM is on core 2 and it only has one vCPU, that vCPU
should probably run on core 2 as well.

In the case of a single vCPU, I don't think it really makes
sense for it to not run on the same core as the VMM.

Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>

Author: Ivan-Velickovic

docs/manual.md

@@ -1097,6 +1097,8 @@ Additionally, it supports the following child elements:
 The `vcpu` element has the following attributes:
 
 * `id`: The vCPU identifier. Must be at least 0 and less than 62.
+* `cpu`: (optional) set the physical CPU core that the vCPU will run on. Defaults to the same CPU
+                    core of the PD that the virtual machine belongs to.
 * `setvar_id`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the vCPU identifier.
 
 The `map` element has the same attributes as the protection domain with the exception of `setvar_vaddr`.

tool/microkit/src/capdl/builder.rs

@@ -936,12 +936,14 @@ pub fn build_capdl_spec(
                         capdl_util_make_vcpu_cap(vm_vcpu_obj_id),
                     ));
 
+                    // vCPU should default to CPU that the PD runs if not explicitly specified.
+                    let vcpu_affinity = vcpu.cpu.unwrap_or(pd.cpu);
                     // Finally create TCB, unlike PDs, VMs are suspended by default until resume'd by their parent.
                     let vm_vcpu_tcb_inner_obj = object::Tcb {
                         slots: caps_to_bind_to_vm_tcbs,
                         extra: Box::new(object::TcbExtraInfo {
                             ipc_buffer_addr: Word(0),
-                            affinity: Word(vcpu.cpu.0.into()),
+                            affinity: Word(vcpu_affinity.0.into()),
                             prio: virtual_machine.priority,
                             max_prio: virtual_machine.priority,
                             // Given the use cases of VMs, for now we always give them FPU access.

tool/microkit/src/sdf.rs

@@ -295,7 +295,7 @@ pub struct VirtualMachine {
 pub struct VirtualCpu {
     pub id: u64,
     pub setvar_id: Option<String>,
-    pub cpu: CpuCore,
+    pub cpu: Option<CpuCore>,
 }
 
 /// To avoid code duplication for handling protection domains
@@ -1186,22 +1186,26 @@ impl VirtualMachine {
 
                     let setvar_id = node.attribute("setvar_id").map(ToOwned::to_owned);
 
-                    let cpu = CpuCore(
-                        sdf_parse_number(child.attribute("cpu").unwrap_or("0"), node)?
+                    let cpu = if let Some(cpu) = child.attribute("cpu") {
+                        let cpu_value: u8 = sdf_parse_number(cpu, node)?
                             .try_into()
-                            .expect("cpu # fits in u8"),
-                    );
+                            .expect("cpu # fits in u8");
 
-                    if cpu.0 >= config.num_cores {
-                        return Err(value_error(
-                            xml_sdf,
-                            &child,
-                            format!(
-                                "cpu core must be less than {}, got {}",
-                                config.num_cores, cpu
-                            ),
-                        ));
-                    }
+                        if cpu_value >= config.num_cores {
+                            return Err(value_error(
+                                xml_sdf,
+                                &child,
+                                format!(
+                                    "cpu core must be less than {}, got {}",
+                                    config.num_cores, cpu_value
+                                ),
+                            ));
+                        }
+
+                        Some(CpuCore(cpu_value))
+                    } else {
+                        None
+                    };
 
                     vcpus.push(VirtualCpu { id, setvar_id, cpu });
                 }