Gerwin Klein

The `rv32` simulation test is failing on `VMFault`, which I assume is related. In general, what kind of testing has been done so far? Passing sel4test is good, but it...

> Enabling the fault benchmarks on RISCV didn't do anything - the fault benchmarks were just always skipped for some reason. Looking at the mainline sel4bench output it seems like...

For the DCO and gitlint test failures, you need to add a [`Signed-off-by` line](https://docs.sel4.systems/processes/contributing.html) and provide [body messages](https://docs.sel4.systems/processes/git-conventions.html) (Ok to leave out for commits you are planning to squash).

(Have set the PR to `draft` as long as there is still work on making the tests pass)

I don't think this can be unified, the MCS setup is a separate manifest and separate set of branches in the verification. It'll needs its own stream.

Maybe I should phrase this differently: the current setup is already too unified and makes the assumption that in the verification the `rt` and `master` branches verify the same revision...

Yes, we still want to support Ubuntu 18 for a while (I forgot for how long, I think it's only another few months)

End of support for Ubuntu 18 is Apr 2023, so I'd leave this unmerged until then.

Like I said, the verification needs to start talking about virtual addresses as soon as objects exist, including caps. That is a good deal before `create_untypeds` (multiple hundred lines). In...

To be clear, I do not think that casting back and forth is a good idea. What I'm proposing is that as early as possible everything computes on kernel virtual...