sel4-capdl-initializer: lazy SC rebind for passive by dreamliner787-9 · Pull Request #352 · seL4/rust-sel4

dreamliner787-9 · 2026-06-22T05:15:25Z

Implements lazy Scheduling Context rebind for passive tasks inside the capDL initialiser.

Solves problems such as seL4/microkit#91

Add `fn bind_ntfn` for `SchedContext`. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

midnightveil · 2026-06-22T05:35:59Z

+                            if obj.bound_notification().is_none() {
+                                panic!("A passive task must have its own Notification.");
+                            }
+                            let bound_notification_cap =
+                                self.orig_cap::<cap_type::Notification>(obj.bound_notification().unwrap().object);


Use the let/Some destrucuturing (or match) here rather than is_none() and unwrap.

Also, if we do sc.bind_ntfn(), where is that SC from, if not obj.sc() and does that not imply that it is not none?

sc in this context could be the initialiser's SC or the TCB's SC as created from the spec. Binding the Notification to the initialiser's SC wouldn't make sense so that's why I had the if obj.bound_notification().is_none() check.

But I'm confused, you then do sc.bind_ntfn(bound_notification_cap)?; next?

Wait my bad, in the original comment, sc would be either a Null cap or the TCB's SC as created from the spec.

Regardless, the if obj.sc().is_none() { check will make sure that sc is the TCB's SC.

Then bound_notification_cap is the TCB's Notification cap.

Then I think we should be explicit and use let/Some for that as well instead of using the previous sc.

Ok sounds good

I meant bound_sc here on the next line, not still sc. No point unwrapping to an unused var.

Also, I'd suggest using this variant:

let Some(bound_sc) = obj.sc() else { panic!("blah blah"); }

This removes the nested as you add more checks.

(Also, is panic!() the normal way that you do errors in rust-sel4?)

Implements lazy Scheduling Context rebind for passive tasks inside the capDL initialiser. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

nspin · 2026-07-05T23:55:53Z

 #[sel4_cfg(KERNEL_MCS)]
 impl<C: InvocationContext> SchedContext<C> {
+    /// Corresponds to `seL4_SchedContext_Bind`.
+    pub fn bind_ntfn(self, notification: Notification) -> Result<()> {


Could you rename this to sched_context_bind() to match the convention of the file?

Also, while you're at it, could you also rename unbind below to sched_context_unbind()?

nspin · 2026-07-05T23:56:34Z


        pub master_fault_ep: Option<Word>,
+
+        pub passive: bool,


Is this flag necessary? Could we just bind the nfn to the sc whenever a tcb has both a nfn and a sc?

That seems wrong; an active server would both have a TCB, SC, and a notification but shouldn't have the SC bound to the notification for lazy rebind. Unless you mean something else?

(But yes this would also need changing in the C capDL spec)

I could've sworn I left another comment but I feel like there should be a way to ask for "SC bound to NTFN" in the spec more generally; which is what this is wanting.

(paasive w/lazy rebind = SC bound to TCB and SC bound to NTFN, and the TCB has ability to block on that notification; no need for an extra passive attribute...)

How about we give a pub slots: Vec<CapTableEntry> to the NTFN object in the spec, if there is a SC cap in that Vec then do the passive with lazy rebind?

Surely binding ntfn to SC exists in the capDL spec?

(If not this should also be discussed on the C/Haskell repo as there are other stakeholders here)

I've made an issue in the C/Haskell repo here: seL4/capdl#96

dreamliner787-9 requested a review from nspin as a code owner June 22, 2026 05:15

crates/sel4: add seL4_SchedContext_Bind

990e954

Add `fn bind_ntfn` for `SchedContext`. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

dreamliner787-9 force-pushed the passive_task_in_initialiser branch from 7dbba7a to 561c46e Compare June 22, 2026 05:18

midnightveil reviewed Jun 22, 2026

View reviewed changes

sel4-capdl-initializer: lazy SC rebind for passive

d20b04c

Implements lazy Scheduling Context rebind for passive tasks inside the capDL initialiser. Signed-off-by: Bill Nguyen <bill.nguyen@unsw.edu.au>

dreamliner787-9 force-pushed the passive_task_in_initialiser branch from 561c46e to d20b04c Compare June 22, 2026 06:01

dreamliner787-9 mentioned this pull request Jun 22, 2026

Fix approach used for making PDs passive seL4/microkit#535

Open

nspin reviewed Jul 5, 2026

View reviewed changes

dreamliner787-9 mentioned this pull request Jul 8, 2026

Lazy Scheduling Context rebind for passive tasks seL4/capdl#96

Open

Uh oh!

Conversation

dreamliner787-9 commented Jun 22, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

midnightveil Jul 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

midnightveil Jul 6, 2026 •

edited

Loading