Gerwin Klein

`init_freemem()` (where this printing is) is happening before `init_core_state()`, which sets `ksCurTime`. That should mean the timing after that bit is unaffected. Is that correct?

So there seems to be something to this. If I print random stuff in a loop 100 times after https://github.com/seL4/seL4/blob/43667a04f445a669380222658c8ba3ef448486d2/src/arch/arm/kernel/boot.c#L492 everything works fine, but if I do the same just...

To log some more facts Kent and I figured out: - confirmed that it only happens on SMP - confirmed that it is delay, not printing as such (changing the...

True, if you're only looking at libsel4 types, you'd most likely miss that. Are you suggesting we should be returning a struct or tagged union instead or that we should...

The preprocess check sees a changed order of include files. Should be fine for the proofs, but I've started a test to make sure.

One more consideration to add: what happens when this runs on multiple cores? For SMP we should be in a big lock, for a multikernel setup that would not be...

That's a good idea.

> Another alternative is that we could restructure `AInvs` in the same way that has been done in the `rt` branch, where `AInvs.thy` is the top-level theory file. This would...