Ivan Velickovic

I would have assumed the libsel4 definition is actually generated based on `seL4_UserContext`.

> We could look into making the generated code use a loop instead of explicitly copying each field. Would this involve just changing `syscall_stub_gen.py`?

Now that SMC forwarding is in the kernel, that should also be mentioned.

> When a guest VM calls SMC, it traps into the VMM, so SMC calls from the guest are a way to communicate with the host. This you could document...

As well as when you have a guest that needs access to some firmware that's only available via SMC and it is not possible/realistic to emulate the SMC call in...

> 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 VM. Yes, agreed....

> Yes, my anecdote is that I use the seL4 docs/tutorial to refresh myself on the fastpath condition, it would be easier if it was in the manual :) Yes...

> It might fall down to moving the device trees out of the kernel reop to satisfy userland needs then also. Wouldn't that mean you can no longer compile the...

Do you think it would be an option to just get rid of device trees altogether? I find them terrible to deal with and given how little information the kernel...

This code does not quite make sense to me, why does `plic_get_current_hart_id` which uses `cpuIndexToID` not just return the correct hart ID? From my understanding what this code seems to...