lazy Scheduling Context rebind

Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

Author: dreamliner787-9

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();
 }

monitor/src/main.c

@@ -37,6 +37,7 @@ 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 */
@@ -740,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_metadata[pd_id].name);
-                    puts("' is now passive!\n");
-                }
-            }
-
-            continue;
-        }
-
         puts("MON|ERROR: received message ");
         puthex32(label);
         puts("  badge: ");
@@ -898,6 +880,8 @@ 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
@@ -911,7 +895,28 @@ void main(void)
     }
 #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();
 }

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

tool/microkit/src/symbols.rs

@@ -19,6 +19,7 @@ use crate::{
 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
@@ -47,6 +48,7 @@ pub fn patch_symbols(
             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);