Indan Zupancic

If the changes are otherwise approved, could someone trigger the SMP HW tests to verify if everything is okay?

Why aren't there more HW Run test that tests SMP + MCS + DEBUG? Some do SMP + MCS + RELEASE, but not debug. Or only SMP or MCS, but...

> The kernel reads the time by performing an SBI call which invokes an SBI handler. Is the `rdtime` instruction handled in software??? That would explain the 2 us, but...

> rdtime can be silently emulated by SBI. And this seems to be the case on the current SiFive board (Unleashed/540, Unmatched/740) , the behavior has been copied by others...

> Is this an intermittent failure? No, I fixed it by setting the threshold to fixed 1 us + `getTimerPrecision`. The check is relaxed enough that all tests should pass...

> seL4 could use the cycle counter or the time source directly. seL4 can't use the cycle count on riscv, as it misses the guarantees that rdtime/CSR_TIME give, which is...

> but we could still use CLINT.mtime directly, as this is what SBI does anyway. It would be a RISC-V SoC specific solution after all might give better realtime behavior...

Specifically, I added a debug test that checks if clocks are indeed synchronous enough at bootup, but it only runs for MCS+SMP+DEBUG and not many platforms have that combination enabled.

> Very long term there's also the argument that by making the slow path faster (lots of opportunity here), we make the entire kernel faster and make life for verification...

> reviewers have to start from scratch and look at everything, because you can't see a nice diff to what you've seen before. Actually, there is a "compare" button next...