The current MCS user-facing API for instance for setting budget and period or reporting consumed time takes its arguments in micro seconds (us, time_t), but internally represents all times in timer ticks (ticks_t).
The conversion from time_t into ticks_t is a division with potential rounding error (when the timer frequency is not a round MHz number) and corresponding loss of timing precision. In addition, some AArch32 platforms may not support a division operation and the implementation of division by multiplication in the kernel may overflow much earlier than direct division, leading to lower time bounds for some platforms than the user might anticipate (because an intermediate value would need to be unit128 instead of uint64, but the required arithmetic operations are not available natively for uint128 on AArch32).
Overall, these operations do not need to be part of the kernel, and therefore should not be part of the kernel. The API could instead be directly in ticks_t. This would make the binary interface platform-dependent, but if desired the conversion can always happen at user level, for instance as part of sel4lib. With a user-level ticks_t API, user code can decide which division operations to use, any slow division would be in the preemptable user execution, or user-level could choose to directly operate in timer ticks with precise values and without potential for rounding errors.
This would be an ABI-breaking change, but with division implemented in libsel4, it could be an API preserving change.
Any opinions or concerns on changing the ABI from time_t to ticks_t?
Also I’d be interested in a similar (and much smaller) option to configure mainline kernel in ticks instead of ms (KernelTimerTickMS is the only config API that’s relevant I think).
How would user level easily use the api when the tick frequency isn’t standard across platforms?
Probably seL4_BootInfo_t should usually provide a way of finding the frequency on each platform. x86 has SEL4_BOOTINFO_HEADER_X86_TSC_FREQ (but does mcs always use TSC frequency for timeouts?)
I’m always in favour of removing violations of the microkernel minimality principle.
And I’m certainly in favour of removing FPU use from the kernel.
The main issue I see is that the clock rate cannot be assumed to be a constant. In fact, it can change any time. How can usermode do the conversion correctly?
My initial idea was to add the ticks_t API to libsel4 with a _ticks postfix, keep the names for the current C API as is, and do the conversion in the libsel4 call there instead of in the kernel (using the same constants that the kernel uses now, just inside libsel4 instead of the kernel).
That would be the minimal change for users, i.e. not source visible.
Adding the timer frequency to seL4_BootInfo_t sounds like a good idea, then user-level would have a standard place to look for these, esp if x86 already does that. We could also make it available as a libsel4 constant, but that would be compile time instead of runtime. Compile time does not only have disadvantages – the compiler could use those constants in optimisations then. But I’m guessing the applications that really want that could still declare a constant themselves if they know what kind of board they are running on.
I’m unclear on how timers work with frequency scaling. I was working under the assumption that CPU frequency would be scaled, but kernel timer frequency would not be (i.e. the CPU does less work per time, but the kernel still sees the same actual time). If kernel timer frequency is dynamic, we could add a syscall to read it instead of a boot info field. The current API does assume the timer frequency to be compile time constant, though.
(Just for clarification to be sure we’re on the same page: it’s only integer division, not floating point, so no need for FPU in either case. But older AArch32 boards don’t have the 64 bit integer division instruction that is needed for that.)
Would make sense to standardise everything on ticks, yes.
On the mainline kernel, this might be a slightly larger change on the inside in the sense that this would change the type of everything with time to uint64, since ticks values could be a lot larger than ms. I don’t see any problems with that, though.
On RISC-V the timer comes from the CLINT, which is independent from the core clock frequency. I think on ARMv8 the ticker timer is also independent of the frequency, but I’m not sure. Not sure how things work on x86.
The main issue I see is that the clock rate cannot be assumed to be a constant. In fact, it can change any time. How can usermode do the conversion correctly?
First, all sane platforms have a timer clock which is independent from the running frequency of the CPU. (On x86 because CPUs wanted to change frequency themselves without software intervention.)
However, assuming a platform doesn’t do that and the clock frequency depends on the CPU frequency:
This would really clash with the current kernel implementation. So either it would force the kernel to do all timing calculations dynamically, without any constants, increasing overhead, or keep things simple and pretend the clock change didn’t happen. Both are bad.
While ticks always stay ticks, with a well defined meaning and no kernel overhead. If user space changes the CPU frequency, it knows the new value. If it wants, it can update all existing SCs for the tasks on the current core, but in most use cases that won’t be necessary.