Indan Zupancic

That's set in include/arch/arm/arch/machine/timer.h to: ``` #define USE_KHZ (TIMER_CLOCK_HZ % HZ_IN_MHZ > 0) ``` and ``` #define TIMER_CLOCK_HZ ULL_CONST(@CONFIGURE_TIMER_FREQUENCY@) ``` So it only depends on the TIMER_FREQUENCY: - If you...

bcm2711 / Raspberry Pi4 is also wrong, it has: ``` TIMER_FREQUENCY 54000000 CLK_MAGIC 5337599559llu CLK_SHIFT 58u ``` That should have been 5090331611 and 38 (the shift of 58 should have...

qemu-arm-virt also has a shift of 58. That's pretty useless, even if it's correct according to the intention of the code (because USE_KHZ would be true). Edit: Actually, it's value...

See also https://github.com/seL4/seL4/pull/1435#issuecomment-2813656622

Yes, this issue is fixed by #1325, specifically by commit fd4e18efd9b04bcfea10d4933ddc4be20caa4ec4 (though I should have added it to the end instead of making it the default there, fixed by later)....

I don't think the boot code is verified yet. There is already: ``` /* TCBs on aarch32 can be larger than page tables in certain configs */ #if seL4_TCBBits >=...

> Is there are good way to deal with this? I have a solution that works, but since this is verified code it would be nice to get this officially...

Yes, they added 1 and said 0xf means not supported, while the old standard only mentioned 0 as meaning 4k supported. So the most conservative check would be checking against...

Would like like to create a pull request or would you prefer me to do it? Advantage of you doing it is that I can review your change, while someone...

(FYI, waiting on a decision whether this API change requires an RFC or is small enough to get merged as is. Another review by someone more familiar with the x86...