Indan Zupancic

Only reason I can think of is because adding lots of if-checks generates horrible code if 'count' is dynamic. Now it always generates slightly less horrible code. If the order...

> Isn't it? At least on AArch64? I think it must be, `invokeTCB_ReadRegisters()` handles it with loops. > I would have assumed the libsel4 definition is actually generated based on...

> Now that SMC forwarding is in the kernel, that should also be mentioned. I keep saying this, but: SMC forwarding has nothing to do with virtualisation as such and...

Documentation should be limited mostly to what seL4 provides and does, it should not be a generic guide on how to write a virtual monitor for ARM. > As well...

> VCPU starting state Do you mean the default values of all system registers? That seems too much details for the manual. Also, they can be retrieved before starting the...

> seL4 ASIDs are not exactly the hardware ASIDs of the underlying platforms, so that should be defined. As far as I know seL4's ASIDs are a thin layer on...

> > The purpose of ASIDs is avoid flushing caches on every context switch, nothing else. I don't think seL4 supports using more ASIDs than the underlaying hardware supports. That...

> (I think we discussed this in another thread already, but just briefly replying again here too.) Yes, we did [here](https://github.com/seL4/seL4/pull/1156#issuecomment-1882376212). > When aarch64 is running in EL2 as a...

> the glossary doesn't have a chapter number, but the bibliography coming after the glossary does, which looks weird in the TOC. If someone knows how to give it a...

The signal fastpath is a configuration option that is default off I think, so it would be confusing to mention. If implementation details like these are added, it should be...