[seL4] getKernelWcetUs: where does the 10us return value come from?

Hi all, Quick questions regarding the return value of getKernelWcetUs(): 1. For ARM the value is assigned during build process taking config.cmake files, where KERNEL_WCET's are all 10us (except for tk1 it's 100us, typo?) For x86 the function returns 10 directly, and for risc-v, comment suggests it's copied from x86 hoping it's an overestimate. Where does this "10us" come from? Based on static estimate done previously on Armv6 (imx31)? AOS lecture mentioned a "378us" kernel WCET estimate and 99.5us observed WCET for Armv6. 2. Is this 10us WCET value the one used as padding in the Temporal Partitioning routine? ("worst-case flushing time"?) Regards, Jack