capdl: add support for domain set

[Kswin01]

Adds support for the DomainSet cap.

It also adds the new invocations that have been added as part of the "Runtime Domain Schedules" RFC: seL4/seL4#1511.

The Spec type is modified to have two new optional values:

pub domain_schedule: Option<Vec<DomainSchedEntry>>
pub domain_start_idx: Option<Word>

pub struct DomainSchedEntry {
    pub id: u8,
    pub time: u64,
}

It also adds "domain" to ExtraTcbObjects. If the seL4 config specifies a number of domains > 1, then it will attempt to set the domain of a thread.

Additionally, if the user has supplied a domain schedule, the initializer creates the domain schedule before starting the threads. Once the threads have been started, the initializer then starts the schedule as the last step.

TODO: Is error checking the bounds of supplied domain ids/indexes against the seL4 config values for NUM_DOMAINS and NUM_DOMAIN_SCHEDULES necessary here, or should we let the kernel handle the error?

[lsf37]

See also seL4/capdl#81 (capdl-loader-app still to follow there)

[lsf37]

Some more context from other parts of capDL:

• the C loader implementation is here: capDL-tool+loader-app: C domain schedule init capdl#82 (and the spec/model update is add domain schedules to capDL-tool capdl#81 -- see markdown spec update for details)
• my proposal for CAmkES is to use the setup as in this PR: camkes: add optional domain schedule declarations camkes-tool#166 (reading the PR description is sufficient)
• a small example in CAmkES looks like this: domains: update domain schedule example camkes#36

Maybe interesting for the Rust loader/Microkit combination is that after long discussion with Indan on seL4/capdl#81 I've come around to the view that we should overwrite the first schedule item in the loader. It's safe to do and I no longer think there is a good reason not to. I'm keeping the feature in the loader to not exclude any possible schedules, but I don't think we'll be needing it a lot.

[lsf37]

(I think the implementation here matches, I just wanted to make sure we're all in sync)

[Kswin01]

Yep I had a read through the markdown spec, I believe this implements that faithfully now.

Regarding over-writing the first domain schedule entry, I wanted to stay away from that. We setup the domain schedules before starting threads, and if we over-write index 0, the starting of threads will all eat into that first timeslice. If we don't setup schedule 0 to have enough time to start all the threads in the system, we'll have to wait til domain 0 is scheduled again to finish (unless I'm missing something here).

For microkit I wanted to setup the schedule at index 1, then once all the threads are started, call set start with index 1 so that we can avoid this issue.

[Kswin01]

But I agree on Indan's point of not having any implicit shifting by Microkit for when we do eventually want to pass the domain cap through to user space.

I'll just leave this as a configuration thing for the user, and make a note of potential issues in the documentation

[lsf37]

Yep I had a read through the markdown spec, I believe this implements that faithfully now.

Regarding over-writing the first domain schedule entry, I wanted to stay away from that. We setup the domain schedules before starting threads, and if we over-write index 0, the starting of threads will all eat into that first timeslice. If we don't setup schedule 0 to have enough time to start all the threads in the system, we'll have to wait til domain 0 is scheduled again to finish (unless I'm missing something here).

The first domain time slice is 2^56-1 ticks, and that does not change until you call DomainSetStart (even when you have overwritten it). Even on MCS on a machine with a 4GHz timer, that would be more than 200 days. If your threads need that much time there might be a different issue :-) You could have a machine with a 400GHz timer and still be completely safe.

Even without that, the threads you are starting must be at a lower priority than the initialiser anyway, so they cannot take time away from the initialiser.

Previously, on CAmkES, the initialiser was cut off, because people set a very low initial time slice for domain 0 (e.g. 1ms), because that could then no longer be adjusted at runtime. But that issue is gone in the new kernel.

For microkit I wanted to setup the schedule at index 1, then once all the threads are started, call set start with index 1 so that we can avoid this issue.

It's not really an issue, though, and doing it will just teach people that there is something special about overwriting the entry when it is specifically designed so that it is safe to do.

Indan feels strongly about this part, I don't really mind that much either way.

There is one small advantage if you do shift: if domain 0 is otherwise unused, then you regain the highest priority, because you can now start threads with the same priority as the initialiser, because they are in a different domain. If you do that without domains, the initialiser is no longer interference free no longer guaranteed to work correctly.

But that only works if domains are on, so to use it, you'd have to have different priority schemes between the domain/no-domain cases, which is probably not that nice to do.

[Kswin01]

and that does not change until you call DomainSetStart (even when you have overwritten it).

Ah okay that's a misunderstanding on my part then apologies. I assumed that when you DomainSet_ScheduleConfigure it would update the time-slice. I'll still keep the ability to set a domain shift and start index, but no special handling otherwise.

[nspin]

Rebasing should fix the CI issues.

[Kswin01]

Ah okay, will rebase now thanks

[Kswin01]

I believe these CI errors are due to the run time domain schedule RFC not being in mainline seL4 just yet. Will need to re-run CI once that is merged

[nspin]

Last nits, thanks for all the iterations, after these idiomatic style changes all is good for merging.

[nspin]

This line conflicts with more recent PRs. Could you remove this change (main now has seL4 with runtime domain schedule) and rebase, so that CI can run and we can merge?

[Kswin01]

Thanks for the help Nick, hopefully it's good to go now