capdl-loader-app: spec for domain schedule in us#95
Conversation
This is partially an experiment, but to make this useful for userspace programs, it makes sense for the capDL specification to treat the domain schedule values as *microseconds*, instead of timer ticks. In the work on [RFC-20] it was proposed that it would make sense to remove this (micro)seconds-to-ticks conversions from seL4 and migrate all of userspace APIs to be in ticks, to make dealing with these calculations and their trickiness to instead be done at user-level. This PR demonstrates that it should be possible to do this for at least the capDL initialiser. For other cases supported by the capDL specification, such as (MCS) budgets and periods currently specified in microseconds, the capDL initialiser should be able to paper over the change in kernel APIs without the users needing to deal with this distinction. These changes are motivated by the [Domain schedules] PR to the seL4 Microkit, which creates a capDL specification for the (Rust version) of the capDL initialiser to use. At the moment, this PR is unable to be consistent about the values exposed to the user for the units of the domain schedule: whilst we can statically determine the us->ticks conversion for ARM/RISC-V platforms, on x86 this is a runtime-known value only. Since the spec is packed at system-build-time, we cannot therefore specify x86 domain schedules in a consistent set of units. [RFC-20]: seL4/rfcs#33 [Domain schedules]: seL4/microkit#445 Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
|
Generally, this would be good addition, but we do need to retain the ability to specify the duration in ticks, so we can't just change the unit. We'll need a mechanism to specify the unit. The whole point of making the interface be ticks is that the FIXME for AArch32 that is still in there is not nicely solvable in general (the method the kernel currently has is flawed in multiple ways). It does not necessarily need to be fully solved in general, because on the platforms where it is problematic you likely to want to compute in ticks anyway. I.e. if we use the current (flawed) kernel method for conversion on AArch32 but also have a capDL ticks interface available, the flaws are avoidable for the systems where that matters. |
| * timer frequency to us at build time, in Hertz */ | ||
| uin64_t timer_frequency = CONFIG_TIMER_FREQUENCY; | ||
|
|
||
| /* FIXME: On ARM32 we need to pull in a 64-bit division helper; |
There was a problem hiding this comment.
Those should be part of the compiler built-in already: There is an __aeabi_uldivmod which will be used automatically for 64-bit divisions on 32-bit Arm.
This is one of the reasons why doing this in user space is easier than in the kernel.
There was a problem hiding this comment.
Well, that's part of libgcc (GCC) or compiler-rt (LLVM), which may or may not be linked in the builds here; however, broadly yes.
There was a problem hiding this comment.
I suppose it depends on how verified you want your user space to be, that's the only reason I can think of for not linking to the compiler library in user space. But I don't see anyone putting that amount of effort into this for 32-bit platforms. (And if they do, they can always use the ticks interface if this is a problem for verification.)
| Note: there are some values of us which would cause unrepresentable | ||
| values in ticks; we should add a static check to error out. |
There was a problem hiding this comment.
Yes, that's the main question: How do you deal with non-whole MHz clock frequencies. If there is no exact conversion you at least want to warn the user about this. Ideally the user should be able to specify whether a time needs to be exact or not.
| seL4_BootInfoHeader *tsc_freq_hdr = extended_bootinfo_table[SEL4_BOOTINFO_HEADER_X86_TSC_FREQ]; | ||
| ZF_LOGF_IF(tsc_freq == NULL, | ||
| "Unable to determine timer frequency as no TSC frequency provided in bootinfo"); | ||
| /* For x86 platforms, the timer frequency is provided in MHz by the bootinfo */ |
There was a problem hiding this comment.
I wonder if anyone ever double checked that the reported frequency is correct.
There was a problem hiding this comment.
Well, us at TS will find out soon when our drivers start using bootinfo, but I sure hope so given the kernel itself uses this value internally.
| /* For x86 platforms, the timer frequency is provided in MHz by the bootinfo */ | ||
| uint32_t tsc_freq_mhz; | ||
| assert(tsc_freq_hdr->len == sizeof(seL4_BootInfoHeader) + sizeof(tsc_freq_mhz); | ||
| memcpy((void *)&tsc_freq_mhz, ((void *)tsc_freq_hdr) + sizeof(seL4_BootInfoHeader), sizeof(tsc_freq_mhz)); |
There was a problem hiding this comment.
cache_extended_bootinfo_headers assumes that the headers are aligned. If that's the case, then the value will be too, so no need for a memcpy here.
There was a problem hiding this comment.
No it doesn't? It stores the pointers directly; it does access hdr->len directly but that assumes that is is aligned for seL4_BootInfoHeader, not for the appropriate bootinfo. Although in this case that is probably the same.
There was a problem hiding this comment.
it does access hdr->len directly but that assumes that is is aligned for seL4_BootInfoHeader
Exactly. The only alignment here that matters is tsc_freq_mhz, which is uint32_t.
Hrm. I don't think I know if there's any cases like this, I suppose... Might need to hand-roll something specific for units here. ACK, this is just an implementation thing mostly then. |
Yes, no problem with us from the conceptual side, as long as we can also do ticks. |
3 participants
This is partially an experiment, but to make this useful for userspace programs, it makes sense for the capDL specification to treat the domain schedule values as microseconds, instead of timer ticks.
In the work on RFC-20 it was proposed that it would make sense to remove this (micro)seconds-to-ticks conversions from seL4 and migrate all of userspace APIs to be in ticks, to make dealing with these calculations and their trickiness to instead be done at user-level.
This PR demonstrates that it should be possible to do this for at least the capDL initialiser. For other cases supported by the capDL specification, such as (MCS) budgets and periods currently specified in microseconds, the capDL initialiser should be able to paper over the change in kernel APIs without the users needing to deal with this distinction.
These changes are motivated by the Domain schedules PR to the seL4 Microkit, which creates a capDL specification for the (Rust version) of the capDL initialiser to use. At the moment, this PR is unable to be consistent about the values exposed to the user for the units of the domain schedule: whilst we can statically determine the us->ticks conversion for ARM/RISC-V platforms, on x86 this is a runtime-known value only. Since the spec is packed at system-build-time, we cannot therefore specify x86 domain schedules in a consistent set of units.
(Note, I haven't actually tested that this works, but I have tested a similar change to rust-seL4 capDL initialiser. This PR is mostly for discussion; this could likely also move to a formal RFC).