Indan Zupancic
Indan Zupancic
> unless the kernel address space has no secrets at all. I would like to point out that it's easy to create a system with seL4 that has no secrets...
> Only works in embedded systems — in the general PC case the HW vendor cannot be trusted to ship BIOS updates quickly. Embedded systems don't usually run untrusted code...
> Not running untrusted and trusted software on the same core is a very non-obvious requirement that I doubt most embedded systems developers would know they needed to meet. Then...
> The operations are slightly different, so there was no point trying to make it even more generic It's mostly the insert operation that's different, but that can be solved...
I'd argue that `seL4_TruncatedMessage` should be treated as a common error code too.
> How would you suggest separating the generic and specific error codes in the manual and the markdown? To be honest, I do not know what @canarysnort01 has in mind...
Agreed. Second check in `isMDBParentOf()` is: ``` if (!sameRegionAs(cte_a->cap, cte_b->cap)) { return false; } ``` I think the intention was `if (sameRegionAs(slot->cap, nextPtr->cap))`, which is superfluous. But fixing that would...
Indeed, that's what I meant with "agreed".
If we fix the code so it does what's intended, it will also print out info about all objects allocated from the UT. Which can be very useful, but it's...
Thanks! To summarise: - The `halt()` on non-zero `GICR_WAKER` is probably too strict and should be removed so it's a warning. - We don't get any timer interrupts with GICv3...