Add support for domain scheduling

[JE-Archer]

This PR aims to add support to the Microkit for seL4's domain scheduling.

Ideally, if the user wished to use domain scheduling, they would specify a domain schedule as well as a mapping of PDs to domains in their system description. However, implementing this is currently not possible as domain scheduling in seL4 requires schedule configuration to be done at kernel build time, which conflicts with the SDK model of Microkit where SDKs are shipped with prebuilt kernel images. More specifically, three kinds of information must be provided to the kernel in order to use domains:

• the number of domains;
• the timeslice of each domain;
• the domain of each TCB.

The last can be provided to the kernel at runtime using the domain cap, but the former two are provided at build time. We assume that in the future the seL4 kernel will allow full runtime specification of all of the above, in which case there will be no issue. Until then however, if we want people to be able to use domains with the Microkit, we need something a bit hackier.

The solution this PR implements is based on patching the values of the ksDomSchedule and ksDomScheduleLength variables in the seL4 kernel ELF. The SDK will patch these variables in accordance with a user-provided domain schedule and PD-domain mapping. This PR also adds support to the SDF for the user to provide this information. The SDF syntax looks like:

<system>
  <domain_schedule>
    <domain name="domain0" length="100" />
    <domain name="domain1" length="200" />
  </domain_schedule>

  <protection_domain name="pd0" priority="1" domain="domain0">
    <program_image path="pd.elf" />
  </protection_domain>

  <protection_domain name="pd1" priority="1" domain="domain1">
    <program_image path="pd.elf" />
  </protection_domain>
</system>

The domain_schedule element allows enumerating a sequence of domains along with each domain's timeslice. The order of the sequence is the order of scheduling. The protection_domain element now has an additional attribute, domain, which is a string which must match the name of one of the domains in the domain schedule. In seL4, domains are identified by integers, but here we allow users to represent them as strings, and map them to integers internally.

This PR also adds the --experimental-domain-support flag to the build_sdk.py script, to enable the above support. This flag will also cause the script to build each seL4 kernel image with the relevant domain-related kernel build flags. In order for this PR to work, the kernel must be patched to remove the const qualifiers from the ksDomSchedule and ksDomScheduleLength variables.

[Ivan-Velickovic]

We have discussed an approach for handling the parameters of domains/domain scheduling without breaking the SDK model offline so I won't comment on that.

Two things missing to get this merged:

• documentation in the manual (need to document the concept of domains as well as the SDF syntax for domains, but it's fine to omit those until we've agreed on the syntax).
• we should be validating the domain value, if we fix the number of domains at build-time then we should be looking at the kernel config value for KernelNumDomains and checking that domain does not exceed that. If we let users define the number of domains then we need to do something similar.

I wonder if we should make the domains named? I'm not too familiar with the usage of domains in seL4 so not sure whether it's worth it.

Another thing is that if two PDs are in separate domains, I believe they cannot communicate in anyway, so we would also need to validate there are no channels between them.

[lsf37]

Another thing is that if two PDs are in separate domains, I believe they cannot communicate in anyway, so we would also need to validate there are no channels between them.

In terms of functionality they can communicate freely with all seL4 mechanisms. Restrictions only come into play if you want to use the information flow theorems and at the same time achieve one-way information flow (as opposed to two-way) between domains. For one-way flow, only shared memory (with read-only on one end) and notifications are allowed. If you want to prevent all information flows, then they of course can't communicate at all.

[Ivan-Velickovic]

In terms of functionality they can communicate freely with all seL4 mechanisms. Restrictions only come into play if you want to use the information flow theorems and at the same time achieve one-way information flow (as opposed to two-way) between domains. For one-way flow, only shared memory (with read-only on one end) and notifications are allowed. If you want to prevent all information flows, then they of course can't communicate at all.

Ah okay, my bad then.