diff --git a/libmicrokit/src/main.c b/libmicrokit/src/main.c index cff14f642..1483fa084 100644 --- a/libmicrokit/src/main.c +++ b/libmicrokit/src/main.c @@ -128,18 +128,5 @@ void main(void) { run_init_funcs(); init(); - - /* - * If we are passive, now our initialisation is complete we can - * signal the monitor to unbind our scheduling context and bind - * it to our notification object. - * We delay this signal so we are ready waiting on a recv() syscall - */ - if (microkit_passive) { - microkit_have_signal = seL4_True; - microkit_signal_msg = seL4_MessageInfo_new(0, 0, 0, 0); - microkit_signal_cap = MONITOR_EP; - } - handler_loop(); } diff --git a/monitor/src/main.c b/monitor/src/main.c index 2adb47a5f..81ab73077 100644 --- a/monitor/src/main.c +++ b/monitor/src/main.c @@ -32,13 +32,23 @@ extern seL4_IPCBuffer __sel4_ipc_buffer_obj; seL4_IPCBuffer *__sel4_ipc_buffer = &__sel4_ipc_buffer_obj; -char pd_names[MAX_PDS][MAX_NAME_LEN]; -seL4_Word pd_names_len; -char vm_names[MAX_VMS][MAX_NAME_LEN] __attribute__((unused)); -seL4_Word vm_names_len; - -/* For reporting potential stack overflows, keep track of the stack regions for each PD. */ -seL4_Word pd_stack_bottom_addrs[MAX_PDS]; +/* Correspond to `struct PdMetadata` in tool/microkit/src/symbols.rs */ +struct pd_metadata { + char name[MAX_NAME_LEN]; + /* For reporting potential stack overflows, keep track of the stack regions for each PD. */ + seL4_Word stack_bottom; + seL4_Word passive; +} __attribute__((packed)); + +/* Correspond to `struct VmMetadata` in tool/microkit/src/symbols.rs */ +struct vm_metadata { + char name[MAX_NAME_LEN]; +} __attribute__((packed)); + +struct pd_metadata pd_metadata[MAX_PDS]; +seL4_Word pd_metadata_len; +struct vm_metadata vm_metadata[MAX_VMS]; +seL4_Word vm_metadata_len; /* Sanity check that the architecture specific macro have been set. */ #if defined(ARCH_aarch64) @@ -731,25 +741,6 @@ static void monitor(void) seL4_Word pd_id = badge - 1; seL4_Word tcb_cap = BASE_PD_TCB_CAP + pd_id; - if (label == seL4_Fault_NullFault && pd_id < MAX_PDS) { - /* This is a request from our PD to become passive */ - err = seL4_SchedContext_UnbindObject(BASE_SCHED_CONTEXT_CAP + pd_id, tcb_cap); - if (err != seL4_NoError) { - puts("MON|ERROR: could not unbind scheduling context from thread control block\n"); - } else { - err = seL4_SchedContext_Bind(BASE_SCHED_CONTEXT_CAP + pd_id, BASE_NOTIFICATION_CAP + pd_id); - if (err != seL4_NoError) { - puts("MON|ERROR: could not bind scheduling context to notification object\n"); - } else { - puts("MON|INFO: PD '"); - puts(pd_names[pd_id]); - puts("' is now passive!\n"); - } - } - - continue; - } - puts("MON|ERROR: received message "); puthex32(label); puts(" badge: "); @@ -758,9 +749,9 @@ static void monitor(void) puthex64(tcb_cap); puts("\n"); - if (pd_id < MAX_PDS && pd_names[pd_id][0] != 0) { + if (pd_id < MAX_PDS && pd_metadata[pd_id].name[0] != 0) { puts("MON|ERROR: faulting PD: "); - puts(pd_names[pd_id]); + puts(pd_metadata[pd_id].name); puts("\n"); } else { fail("MON|ERROR: unknown/invalid badge\n"); @@ -850,7 +841,7 @@ static void monitor(void) #endif seL4_Word fault_addr = seL4_GetMR(seL4_VMFault_Addr); - seL4_Word stack_addr = pd_stack_bottom_addrs[pd_id]; + seL4_Word stack_addr = pd_metadata[pd_id].stack_bottom; if (fault_addr < stack_addr && fault_addr >= stack_addr - 0x1000) { puts("MON|ERROR: potential stack overflow, fault address within one page outside of stack region\n"); } @@ -889,20 +880,43 @@ static void monitor(void) void main(void) { + puts("MON|INFO: Microkit Monitor started!\n"); + #if CONFIG_DEBUG_BUILD /* * 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. */ - for (unsigned idx = 0; idx < pd_names_len; idx++) { - seL4_DebugNameThread(BASE_PD_TCB_CAP + idx, pd_names[idx]); + for (unsigned idx = 0; idx < pd_metadata_len; idx++) { + seL4_DebugNameThread(BASE_PD_TCB_CAP + idx, pd_metadata[idx].name); } - for (unsigned idx = 0; idx < vm_names_len; idx++) { - seL4_DebugNameThread(BASE_VM_TCB_CAP + idx, vm_names[idx]); + for (unsigned idx = 0; idx < vm_metadata_len; idx++) { + seL4_DebugNameThread(BASE_VM_TCB_CAP + idx, vm_metadata[idx].name); } #endif - puts("MON|INFO: Microkit Monitor started!\n"); + /* If there are passive PDs in the system, lazily rebind it's Scheduling Context to it's Notification. + * To workaround https://github.com/seL4/seL4/issues/1617 by applying https://github.com/seL4/seL4/pull/523 + */ + for (unsigned idx = 0; idx < pd_metadata_len; idx++) { + if (pd_metadata[idx].passive) { + seL4_Error err = seL4_SchedContext_Bind(BASE_SCHED_CONTEXT_CAP + idx, BASE_NOTIFICATION_CAP + idx); + if (err != seL4_NoError) { + puts("MON|ERROR: could not bind scheduling context to notification object\n"); + continue; + } + + err = seL4_TCB_Resume(BASE_PD_TCB_CAP + idx); + if (err != seL4_NoError) { + puts("MON|ERROR: could not bind resume passive PD TCB\n"); + continue; + } + + puts("MON|INFO: PD '"); + puts(pd_metadata[idx].name); + puts("' is now passive!\n"); + } + } monitor(); } diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs index c40575871..915da78a6 100644 --- a/tool/microkit/src/capdl/builder.rs +++ b/tool/microkit/src/capdl/builder.rs @@ -979,7 +979,8 @@ pub fn build_capdl_spec( 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.resume = true; + // Passive PDs are resumed by the Monitor + pd_tcb.extra.resume = !pd.passive; pd_tcb.slots.extend(caps_to_bind_to_tcb); // Stylistic purposes only diff --git a/tool/microkit/src/symbols.rs b/tool/microkit/src/symbols.rs index bcdfed965..5a232c3dc 100644 --- a/tool/microkit/src/symbols.rs +++ b/tool/microkit/src/symbols.rs @@ -10,10 +10,24 @@ use crate::{ elf::ElfFile, sdf::{self, SysMemoryRegion, SystemDescription}, sel4::{Arch, Config}, - util::{monitor_serialise_names, monitor_serialise_u64_vec}, - MAX_PDS, MAX_VMS, PD_MAX_NAME_LENGTH, VM_MAX_NAME_LENGTH, + util::{copy_and_clip_string, struct_to_bytes}, + PD_MAX_NAME_LENGTH, VM_MAX_NAME_LENGTH, }; +/// Correspond to `struct pd_metadata` in monitor/src/main.c +#[repr(C)] +struct PdMetadata { + pub name: [u8; PD_MAX_NAME_LENGTH], + pub stack_bottom: u64, + pub passive: u64, +} + +/// Correspond to `struct vm_metadata` in monitor/src/main.c +#[repr(C)] +struct VmMetadata { + pub name: [u8; VM_MAX_NAME_LENGTH], +} + /// Patch all the required symbols in the Monitor and children PDs according to /// the Microkit's requirements pub fn patch_symbols( @@ -26,25 +40,37 @@ pub fn patch_symbols( // ********************************* let monitor_elf = pd_elf_files.last_mut().unwrap(); - let pd_names: Vec = system + let mut pd_metadata_bytes = Vec::new(); + system .protection_domains .iter() - .map(|pd| pd.name.clone()) - .collect(); + .map(|pd| { + let mut metadata = PdMetadata { + name: [0u8; PD_MAX_NAME_LENGTH], + stack_bottom: kernel_config.pd_stack_bottom(pd.stack_size), + passive: if pd.passive { 1 } else { 0 }, + }; + + copy_and_clip_string(pd.name.as_bytes(), &mut metadata.name); + + metadata + }) + .for_each(|metadata| { + pd_metadata_bytes.extend_from_slice(unsafe { struct_to_bytes(&metadata) }) + }); + monitor_elf .write_symbol( - "pd_names_len", + "pd_metadata_len", &system.protection_domains.len().to_le_bytes(), ) .unwrap(); monitor_elf - .write_symbol( - "pd_names", - &monitor_serialise_names(&pd_names, MAX_PDS, PD_MAX_NAME_LENGTH), - ) + .write_symbol("pd_metadata", &pd_metadata_bytes) .unwrap(); - let vm_names: Vec = system + let mut vm_metadata_bytes = Vec::new(); + system .protection_domains .iter() .filter(|pd| pd.virtual_machine.is_some()) @@ -53,33 +79,29 @@ pub fn patch_symbols( let num_vcpus = vm.vcpus.len(); std::iter::repeat_n(vm.name.clone(), num_vcpus) }) - .collect(); + .map(|vm_name| { + let mut metadata = VmMetadata { + name: [0u8; VM_MAX_NAME_LENGTH], + }; + + copy_and_clip_string(vm_name.as_bytes(), &mut metadata.name); - let vm_names_len = match kernel_config.arch { - Arch::Aarch64 | Arch::Riscv64 => vm_names.len(), + metadata + }) + .for_each(|metadata| { + vm_metadata_bytes.extend_from_slice(unsafe { struct_to_bytes(&metadata) }) + }); + + let vm_metadata_len = match kernel_config.arch { + Arch::Aarch64 | Arch::Riscv64 => vm_metadata_bytes.len() / size_of::(), // VM on x86 doesn't have a separate TCB. Arch::X86_64 => 0, }; monitor_elf - .write_symbol("vm_names_len", &vm_names_len.to_le_bytes()) - .unwrap(); - monitor_elf - .write_symbol( - "vm_names", - &monitor_serialise_names(&vm_names, MAX_VMS, VM_MAX_NAME_LENGTH), - ) + .write_symbol("vm_metadata_len", &vm_metadata_len.to_le_bytes()) .unwrap(); - - let mut pd_stack_bottoms: Vec = Vec::new(); - for pd in system.protection_domains.iter() { - let cur_stack_vaddr = kernel_config.pd_stack_bottom(pd.stack_size); - pd_stack_bottoms.push(cur_stack_vaddr); - } monitor_elf - .write_symbol( - "pd_stack_bottom_addrs", - &monitor_serialise_u64_vec(&pd_stack_bottoms), - ) + .write_symbol("vm_metadata", &vm_metadata_bytes) .unwrap(); // ********************************* diff --git a/tool/microkit/src/util.rs b/tool/microkit/src/util.rs index 77420a172..bc4acfb55 100644 --- a/tool/microkit/src/util.rs +++ b/tool/microkit/src/util.rs @@ -171,36 +171,18 @@ pub unsafe fn bytes_to_struct(bytes: &[u8]) -> &T { &body[0] } -/// Serialise an array of u64 to a Vector of bytes. -pub fn monitor_serialise_u64_vec(vec: &[u64]) -> Vec { - let mut bytes = vec![0; (1 + vec.len()) * 8]; - for (i, value) in vec.iter().enumerate() { - let start = i * 8; - let end = start + 8; - bytes[start..end].copy_from_slice(&value.to_le_bytes()); +/// Copy at most `out_str.len() - 1` bytes from `in_str` to `out_str`. Null terminates `out_str` +pub fn copy_and_clip_string(in_str: &[u8], out_str: &mut [u8]) { + if out_str.is_empty() { + return; } - bytes -} - -/// For serialising an array of PD or VM names -pub fn monitor_serialise_names(names: &[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() { - let name_bytes = name.as_bytes(); - let start = i * 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. The name length is one less than - // the maximum since we still have to add the null terminator. - let name_length = std::cmp::min(name_bytes.len(), max_name_len - 1); - 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[end] = 0; - } - - names_bytes + // Here instead of giving an error we simply take the minimum of the name + // and how large of a name we can encode. The name length is one less than + // the maximum since we still have to add the null terminator. + let n = in_str.len().min(out_str.len() - 1); + out_str[..n].copy_from_slice(&in_str[..n]); + out_str[n] = 0; } #[cfg(test)]