Lazy Scheduling Context rebind for passive tasks

[dreamliner787-9]

There are multiple ways to create a passive task on seL4. One of the ways is by binding the task's Scheduling Context to its Notification object. This was implemented in the kernel by seL4/seL4#523.

We wanted to use this approach in the Microkit, which uses the Rust implementation of the capDL initialiser, to solve this issue.

It seems to me that capDL does not have a mechanism to express this "lazy rebind" operation. I had a start of implementing this in the Rust version, however this is an addition to the spec format so I'm opening an issue here to see if any users of capDL have any inputs on this.

[lsf37]

Can you lay out what this would look like in a textual capDL spec like this one? It doesn't have any SC's or notifications, but the format would be the same.

I.e. is the plan to specify additional (fake) cap mappings between notification and SC? The kernel would require these to be in both directions. Do we specify only one in capDL and keep the other implicit? (That would violate the main theorem that says the caps in the system are the caps in the spec in the end. Could be rescued by some kind of normalisation step, I guess).

I don't remember if we have setup for bound notifications between notification and TCB yet, but I suspect not.

(Edit: I mean: what's the equivalent of what the current Rust idea is doing there?)

[lsf37]

AFAIR, we have in the past left binding caps to TCBs for instance to a separate init phase after the capDL loader. That'd only work if that phase has enough authority, of course, and knows which caps to bind to what. I guess if it is expressible in capDL there is no reason the capDL loader shouldn't be able to do these operations.

[midnightveil]

Can you lay out what this would look like in a textual capDL spec like this one? It doesn't have any SC's or notifications, but the format would be the same.
I.e. is the plan to specify additional (fake) cap mappings between notification and SC?

I suppose there's not actually a cap mapping in seL4 for SC, just a two-way pointer between objects. Huh.

I guess the only precedent for this is what Nick Spinale did for the TCB<>NTFN binding, as well as what was done for TCB<>SC binding; both of those already had slots in the TCB that actually stored caps that could be reused in the same idea. (i.e. existing SC bound to TCB use slots when there is no cap reference).

So yes, I'd think we make the conceptual hasSlots (SC {}) = True be true as well, and then you'd get something like

objects {
  our_ntfn = notification
  our_tcb = tcb (...)
  our_sc = sched_context
} caps {
  // Passive thread using lazy unbinding
  our_sc {
    tcb: our_tcb
    ntfn: our_ntfn
  }
}

If anything I'd remove the ability to do a TCB with an SC in its slot, in preference of sc slots directly, because otherwise it is weird to have both; i.e.

} caps {
 -- This for an active thread
 our_tcb {
   sc: our_sc
 }
 -- Becomes this
 our_sc {
   tcb: our_tcb
 }
}

However, this could also possibly work, like IRQ maps:

} sc_binds {
  (our_sc, our_tcb) {}
  (our_sc, our_ntfn) {}
}

I don't particularly know which would be better.

(Edit: I mean: what's the equivalent of what the current Rust idea is doing there?)

What the Rust does currently, is, I think a bad idea (making "passive" do something weird that changes the behaviour of "SC bound to TCB" to instead also bind it to the notification that is also bound to the TCB). It would be adding a property on TCB called "passive" that only works if there's a SC and a NTFN in the 'slots' of the TCB.

seL4/rust-sel4#352 (comment)

AFAIR, we have in the past left binding caps to TCBs for instance to a separate init phase after the capDL loader.

No longer for notifications or SC: #62

(i.e. for active PDs, binding SC to TCB is possible).

[dreamliner787-9]

Hi @lsf37, any thoughts?

[lsf37]

I guess the only precedent for this is what Nick Spinale did for the TCB<>NTFN binding, as well as what was done for TCB<>SC binding; both of those already had slots in the TCB that actually stored caps that could be reused in the same idea. (i.e. existing SC bound to TCB use slots when there is no cap reference).

Ok, yes, that would be the standard capDL thing to do (model object pointers as cap slots), and we do have precedent with the notifications, thanks for finding that.

objects {
  our_ntfn = notification
  our_tcb = tcb (...)
  our_sc = sched_context
} caps {
  // Passive thread using lazy unbinding
  our_sc {
    tcb: our_tcb
    ntfn: our_ntfn
  }
}

Ok, that works, yes.

If anything I'd remove the ability to do a TCB with an SC in its slot, in preference of sc slots directly, because otherwise it is weird to have both; i.e.

} caps {
 -- This for an active thread
 our_tcb {
   sc: our_sc
 }
 -- Becomes this
 our_sc {
   tcb: our_tcb
 }
}

I guess that is the remaining problem. For notifications so far, we seem to have only put the cap slot into the TCB and not the notification. This is a bit weird in terms of the kernel which must always either have both or none, but it'd be verbose and somewhat pointless to actually require this in the input spec. So I guess the two remaining angles to consider are what is nicer to specify and what is easier for the loader to work with.

For active TCBs, if we don't have the SC link in the TCB, then the TCB init either won't be complete in the TCB loop or it would have to search all SCs to figure out if we need to bind something or not. I guess it would be fine for TCBs to be not fully initialised yet, and for the SC loop to complete the initialisation, because they can then tell whether they should be active or passive. So yes, I think your proposal makes sense.

It'd be a breaking change, but I don't think there are any other users of this feature yet, and it'd be relatively easy to update.

However, this could also possibly work, like IRQ maps:

} sc_binds {
  (our_sc, our_tcb) {}
  (our_sc, our_ntfn) {}
}

I like the direct method above better. The general idea is that the cap state describes everything that is needed as a declarative state, and as long as that works I think it's worth keeping it.

What the Rust does currently, is, I think a bad idea (making "passive" do something weird that changes the behaviour of "SC bound to TCB" to instead also bind it to the notification that is also bound to the TCB). It would be adding a property on TCB called "passive" that only works if there's a SC and a NTFN in the 'slots' of the TCB.

Agreed, that's not nice.

[midnightveil]

I guess that is the remaining problem. For notifications so far, we seem to have only put the cap slot into the TCB and not the notification. This is a bit weird in terms of the kernel which must always either have both or none, but it'd be verbose and somewhat pointless to actually require this in the input spec. So I guess the two remaining angles to consider are what is nicer to specify and what is easier for the loader to work with.

I'm not entirely sure what you mean here by "needs either both or none". As far as I know for TCB+ntfn, there's only the cap reference to the NTFN in the TCB mini-cnode.

I was thinking that it makes sense to do the slots according to the syscall invocations; that is:

• seL4_TCB_BindNotification: notification lives in a slot in the TCB.
• seL4_SchedContext_Bind (ntfn/tcb): reference to ntfn/tcb inside the schedcontext obj

And the capDL spec reflects this in the "slots".

[lsf37]

I guess that is the remaining problem. For notifications so far, we seem to have only put the cap slot into the TCB and not the notification. This is a bit weird in terms of the kernel which must always either have both or none, but it'd be verbose and somewhat pointless to actually require this in the input spec. So I guess the two remaining angles to consider are what is nicer to specify and what is easier for the loader to work with.

I'm not entirely sure what you mean here by "needs either both or none". As far as I know for TCB+ntfn, there's only the cap reference to the NTFN in the TCB mini-cnode.

In capDL yes, in the actual kernel for each object link, there must always be a back-link (potentially indirect).

I was thinking that it makes sense to do the slots according to the syscall invocations; that is:

• seL4_TCB_BindNotification: notification lives in a slot in the TCB.
• seL4_SchedContext_Bind (ntfn/tcb): reference to ntfn/tcb inside the schedcontext obj

Ok, let's do that. It makes the most sense for the loader.

And the capDL spec reflects this in the "slots".

Yes, that part is fine. I was mostly thinking about what can be said about the state of these objects once each pass for that object type is done. That's how the verification has to approach it, it formalises what is known after each stage, and after the final stage everything should be fully initialised. So far, I think TCBs were fully done after the TCB pass. That is now a bit more complicated. They'll be something like half done after the TCB phase and fully done after the SC phase.