Name VM TCBs in debug mode as well

monitor/src/main.c

@@ -65,9 +65,9 @@
 #include "util.h"
 #include "debug.h"
 
+#define MAX_VMS 64
 #define MAX_PDS 64
 #define MAX_NAME_LEN 64
-#define MAX_TCBS 64
 
 #define MAX_UNTYPED_REGIONS 256
 
@@ -87,12 +87,15 @@ char _stack[4096];
 
 static char pd_names[MAX_PDS][MAX_NAME_LEN];
 seL4_Word pd_names_len;
+static char vm_names[MAX_VMS][MAX_NAME_LEN] __attribute__((unused));
+seL4_Word vm_names_len;
 
 seL4_Word fault_ep;
 seL4_Word reply;
-seL4_Word tcbs[MAX_TCBS];
-seL4_Word scheduling_contexts[MAX_TCBS];
-seL4_Word notification_caps[MAX_TCBS];
+seL4_Word pd_tcbs[MAX_PDS];
+seL4_Word vm_tcbs[MAX_VMS];
+seL4_Word scheduling_contexts[MAX_PDS];
+seL4_Word notification_caps[MAX_PDS];
 
 /* For reporting potential stack overflows, keep track of the stack regions for each PD. */
 seL4_Word pd_stack_addrs[MAX_PDS];
@@ -806,7 +809,7 @@ static void monitor(void)
         tag = seL4_Recv(fault_ep, &badge, reply);
         label = seL4_MessageInfo_get_label(tag);
 
-        seL4_Word tcb_cap = tcbs[badge];
+        seL4_Word tcb_cap = pd_tcbs[badge];
 
         if (label == seL4_Fault_NullFault && badge < MAX_PDS) {
             /* This is a request from our PD to become passive */
@@ -970,7 +973,7 @@ void main(seL4_BootInfo *bi)
 
 #if CONFIG_DEBUG_BUILD
     /*
-     * Assign PD names to each TCB with seL4, this helps debugging when an error
+     * Assign PD/VM names to each TCB with seL4, this helps debugging when an error
      * message is printed by seL4 or if we dump the scheduler state.
      * This is done specifically in the monitor rather than being prepared as an
      * invocation like everything else because it is technically a separate system
@@ -979,7 +982,10 @@ void main(seL4_BootInfo *bi)
      * support in the tooling and make the monitor generic.
      */
     for (unsigned idx = 1; idx < pd_names_len + 1; idx++) {
-        seL4_DebugNameThread(tcbs[idx], pd_names[idx]);
+        seL4_DebugNameThread(pd_tcbs[idx], pd_names[idx]);
+    }
+    for (unsigned idx = 1; idx < vm_names_len + 1; idx++) {
+        seL4_DebugNameThread(vm_tcbs[idx], vm_names[idx]);
     }
 #endif
 

tool/microkit/src/lib.rs

@@ -14,13 +14,15 @@ use sel4::BootInfo;
 use std::cmp::min;
 use std::fmt;
 
-// Note that this value is used in the monitor so should also be changed there
-// if this was to change.
+// Note that these values are used in the monitor so should also be changed there
+// if any of these were to change.
 pub const MAX_PDS: usize = 63;
+pub const MAX_VMS: usize = 63;
 // It should be noted that if you were to change the value of
-// the maximum PD name length, you would also have to change
+// the maximum PD/VM name length, you would also have to change
 // the monitor and libmicrokit.
 pub const PD_MAX_NAME_LENGTH: usize = 64;
+pub const VM_MAX_NAME_LENGTH: usize = 64;
 
 #[derive(Debug, Copy, Clone, PartialEq)]
 pub struct UntypedObject {

tool/microkit/src/main.rs

@@ -11,7 +11,7 @@ use elf::ElfFile;
 use loader::Loader;
 use microkit_tool::{
     elf, loader, sdf, sel4, util, DisjointMemoryRegion, MemoryRegion, ObjectAllocator, Region,
-    UntypedObject, MAX_PDS, PD_MAX_NAME_LENGTH,
+    UntypedObject, MAX_PDS, MAX_VMS, PD_MAX_NAME_LENGTH, VM_MAX_NAME_LENGTH,
 };
 use sdf::{
     parse, ProtectionDomain, SysMap, SysMapPerms, SysMemoryRegion, SystemDescription,
@@ -31,7 +31,7 @@ use std::mem::size_of;
 use std::path::{Path, PathBuf};
 use util::{
     bytes_to_struct, comma_sep_u64, comma_sep_usize, json_str, json_str_as_bool, json_str_as_u64,
-    monitor_serialise_u64_vec, struct_to_bytes,
+    monitor_serialise_names, monitor_serialise_u64_vec, struct_to_bytes,
 };
 
 // Corresponds to the IPC buffer symbol in libmicrokit and the monitor
@@ -448,7 +448,8 @@ struct BuiltSystem {
     fault_ep_cap_address: u64,
     reply_cap_address: u64,
     cap_lookup: HashMap<u64, String>,
-    tcb_caps: Vec<u64>,
+    pd_tcb_caps: Vec<u64>,
+    vm_tcb_caps: Vec<u64>,
     sched_caps: Vec<u64>,
     ntfn_caps: Vec<u64>,
     pd_elf_regions: Vec<Vec<Region>>,
@@ -2864,7 +2865,8 @@ fn build_system(
         fault_ep_cap_address: fault_ep_endpoint_object.cap_addr,
         reply_cap_address: reply_obj.cap_addr,
         cap_lookup: cap_address_names,
-        tcb_caps: tcb_caps[..system.protection_domains.len()].to_vec(),
+        pd_tcb_caps: tcb_caps[..system.protection_domains.len()].to_vec(),
+        vm_tcb_caps: tcb_caps[system.protection_domains.len()..].to_vec(),
         sched_caps: sched_context_caps,
         ntfn_caps: notification_caps,
         pd_elf_regions,
@@ -3534,38 +3536,42 @@ fn main() -> Result<(), String> {
         &bootstrap_invocation_data,
     )?;
 
-    let tcb_cap_bytes = monitor_serialise_u64_vec(&built_system.tcb_caps);
+    let pd_tcb_cap_bytes = monitor_serialise_u64_vec(&built_system.pd_tcb_caps);
+    let vm_tcb_cap_bytes = monitor_serialise_u64_vec(&built_system.vm_tcb_caps);
     let sched_cap_bytes = monitor_serialise_u64_vec(&built_system.sched_caps);
     let ntfn_cap_bytes = monitor_serialise_u64_vec(&built_system.ntfn_caps);
     let pd_stack_addrs_bytes = monitor_serialise_u64_vec(&built_system.pd_stack_addrs);
 
     monitor_elf.write_symbol("fault_ep", &built_system.fault_ep_cap_address.to_le_bytes())?;
     monitor_elf.write_symbol("reply", &built_system.reply_cap_address.to_le_bytes())?;
-    monitor_elf.write_symbol("tcbs", &tcb_cap_bytes)?;
+    monitor_elf.write_symbol("pd_tcbs", &pd_tcb_cap_bytes)?;
+    monitor_elf.write_symbol("vm_tcbs", &vm_tcb_cap_bytes)?;
     monitor_elf.write_symbol("scheduling_contexts", &sched_cap_bytes)?;
     monitor_elf.write_symbol("notification_caps", &ntfn_cap_bytes)?;
     monitor_elf.write_symbol("pd_stack_addrs", &pd_stack_addrs_bytes)?;
-    // We do MAX_PDS + 1 due to the index that the monitor uses (the badge) starting at 1.
-    let mut pd_names_bytes = vec![0; (MAX_PDS + 1) * PD_MAX_NAME_LENGTH];
-    for (i, pd) in system.protection_domains.iter().enumerate() {
-        // The monitor will index into the array of PD names based on the badge, which
-        // starts at 1 and hence we cannot use the 0th entry in the array.
-        let name = pd.name.as_bytes();
-        let start = (i + 1) * PD_MAX_NAME_LENGTH;
-        // Here instead of giving an error we simply take the minimum of the PD's name
-        // and how large of a name we can encode
-        let name_length = min(name.len(), PD_MAX_NAME_LENGTH);
-        let end = start + name_length;
-        pd_names_bytes[start..end].copy_from_slice(&name[..name_length]);
-        // These bytes will be interpreted as a C string, so we must include
-        // a null-terminator.
-        pd_names_bytes[start + PD_MAX_NAME_LENGTH - 1] = 0;
-    }
-    monitor_elf.write_symbol("pd_names", &pd_names_bytes)?;
+    let pd_names = system
+        .protection_domains
+        .iter()
+        .map(|pd| &pd.name)
+        .collect();
+    monitor_elf.write_symbol(
+        "pd_names",
+        &monitor_serialise_names(pd_names, MAX_PDS, PD_MAX_NAME_LENGTH),
+    )?;
     monitor_elf.write_symbol(
         "pd_names_len",
         &system.protection_domains.len().to_le_bytes(),
     )?;
+    let vm_names: Vec<&String> = system
+        .protection_domains
+        .iter()
+        .filter_map(|pd| pd.virtual_machine.as_ref().map(|vm| &vm.name))
+        .collect();
+    monitor_elf.write_symbol("vm_names_len", &vm_names.len().to_le_bytes())?;
+    monitor_elf.write_symbol(
+        "vm_names",
+        &monitor_serialise_names(vm_names, MAX_VMS, VM_MAX_NAME_LENGTH),
+    )?;
 
     // Write out all the symbols for each PD
     pd_write_symbols(

tool/microkit/src/util.rs

@@ -194,6 +194,32 @@ pub fn monitor_serialise_u64_vec(vec: &[u64]) -> Vec<u8> {
     bytes
 }
 
+/// For serialising an array of PD or VM names. Pads the Vector of bytes such that
+/// the first entry is empty.
+pub fn monitor_serialise_names(
+    names: Vec<&String>,
+    max_len: usize,
+    max_name_len: usize,
+) -> Vec<u8> {
+    let mut names_bytes = vec![0; (max_len + 1) * max_name_len];
+    for (i, name) in names.iter().enumerate() {
+        // The monitor will index into the array of names based on the badge, which
+        // starts at 1 and hence we cannot use the 0th entry in the array.
+        let name_bytes = name.as_bytes();
+        let start = (i + 1) * max_name_len;
+        // Here instead of giving an error we simply take the minimum of the name
+        // and how large of a name we can encode
+        let name_length = std::cmp::min(name_bytes.len(), max_name_len);
+        let end = start + name_length;
+        names_bytes[start..end].copy_from_slice(&name_bytes[..name_length]);
+        // These bytes will be interpreted as a C string, so we must include
+        // a null-terminator.
+        names_bytes[start + max_name_len - 1] = 0;
+    }
+
+    names_bytes
+}
+
 #[cfg(test)]
 mod tests {
     // Note this useful idiom: importing names from outer (for mod tests) scope.