For every scheme a fully running kernel has, the following functions need to be documented, if implemented. In addition, the Scheme and SchemeMut traits should be documented with usage and the default operation.

Documentation should include usage, what access restrictions there are, what paths and dup arguments are valid, and what errors may be returned.

Path Operations

• open

https://github.com/seL4/seL4/blob/master/manual/parts/cspace.tex#L430 gives a good example to explain CSpace addressing. It is clear enough to introduce the addressing concept, but with coding practice it's better to make them more precise.

When passing address arguments in multi-level CNodes, the index field, i.e. its address, must right aligned the significant bits according its depth. In a

See thor's system/legacy-pc

If we page-fault because we've overflown the stack, we currently double fault. This isn't ideal, and so we should install another stack in the IST and switch to it when page-faults occur.