lazy SC rebind + improved tool <> mon ABI

dreamliner787-9 · dreamliner787-9 · commit d500f225c9d5 · 2026-03-16T13:39:59.000+11:00
Signed-off-by: Bill Nguyen &lt;bill.nguyen@unsw.edu.au&gt;
diff --git 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
@@ -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];
+    seL4_Word passive;
+    /* For reporting potential stack overflows, keep track of the stack regions for each PD. */
+    seL4_Word stack_bottom;
+} __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");
             }
@@ -894,14 +885,37 @@ void main(void)
      * 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
 
+    /* If there are passive PDs in the system, lazily rebind it's Scheduling Context and resume TCB.
+     * 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");
+        }
+    }
+
     puts("MON|INFO: Microkit Monitor started!\n");
 
     monitor();
diff --git 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
@@ -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 passive: u64,
+    pub stack_bottom: 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<String> = 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],
+                passive: if pd.passive { 1 } else { 0 },
+                stack_bottom: kernel_config.pd_stack_bottom(pd.stack_size),
+            };
+
+            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<String> = 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::<VmMetadata>(),
         // 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<u64> = 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
@@ -171,36 +171,18 @@ pub unsafe fn bytes_to_struct<T>(bytes: &[u8]) -> &T {
     &body[0]
 }
 
-/// Serialise an array of u64 to a Vector of bytes.
-pub fn monitor_serialise_u64_vec(vec: &[u64]) -> Vec<u8> {
-    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<u8> {
-    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)]
