diff --git a/monitor/src/main.c b/monitor/src/main.c index 8974e64e..2baeceed 100644 --- a/monitor/src/main.c +++ b/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 diff --git a/tool/microkit/src/lib.rs b/tool/microkit/src/lib.rs index ea5d8d97..edba0a4e 100644 --- a/tool/microkit/src/lib.rs +++ b/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 { diff --git a/tool/microkit/src/main.rs b/tool/microkit/src/main.rs index 85476943..3157d376 100644 --- a/tool/microkit/src/main.rs +++ b/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, - tcb_caps: Vec, + pd_tcb_caps: Vec, + vm_tcb_caps: Vec, sched_caps: Vec, ntfn_caps: Vec, pd_elf_regions: Vec>, @@ -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( diff --git a/tool/microkit/src/util.rs b/tool/microkit/src/util.rs index 0459438a..d2b49561 100644 --- a/tool/microkit/src/util.rs +++ b/tool/microkit/src/util.rs @@ -194,6 +194,32 @@ pub fn monitor_serialise_u64_vec(vec: &[u64]) -> Vec { 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 { + 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.