Some updates inline. Especially interested in answers for #5 and #8.
On Wed, Nov 24, 2021 at 9:12 PM Sam Leffler <sleffler(a)google.com> wrote:
I've been investigating how capd-loader works and
have some questions. My
apologies if these were previously discussed.
1. CDL_Model is mutable. The capDL specification looks like a perfect
candidate for being in .rodata but it's stored+treated as mutable. Why? I
see capdl-loader uses the mutability to store mapped page frame caps and,
for risc-v, VSpace roots, but both can be easily handled w/o modifying the
spec. Having this immutable has many benefits.
2. All page frames are treated as shared. CAPDL_SHARED_FRAMES is #define'd
in the code so every frame is treated as shared. This inflates the size of
the orig_caps array and the kernel capabilities table but seems
unnecessary. Why? I've verified that instead of doing the Copy op on each
page you can just check the return of the seL4_Page_Map call and if
necessary clone the cap. Better would be for camkes to identify shared page
frames so this doesn't require 2x syscalls (which spam's the console w/
CONFIG_PRINTING enabled).
3. Why does copy_addr_with_pt exist? There are two memory regions created
for mapping page frames into the rootserver address space for doing fill
ops. One is 64KB and the other is 1 page (nominally 4KB). init_frame tries
the 4KB region first then falls back to the 64K region if mapping into the
4KB region fails. Why (i.e. why would the 1st mapping call fail)? On my
risc-v system I never use the 64K region and I'm not sure when it might be
used? Even if it were used, why is 64K always allocated; seems like the
region should be sized according to the target platform. Having this extra
region has a cost that can be significant on small systems.
I got this backwards; on risc-v at least the 64KB region is used but not
the page immediately after the ipc buffer. On my system I eliminated the
latter and shrank the bss region to 1 page. Looking for feedback on whether
this will fail on other platforms.
4. console output. Why is sel4_DebugPutChar (or similar) not a standard
part of the kernel? This forces capdl-loader to depend on
libsel4platsupport for console output which in turn affects cap space. I
can't imagine an seL4 system that cannot write to the console and I think
it's entirely reasonable to have a critical system service like the
rootserver use that.
5. duplicate_caps. The scheme for constructing a
running system from a
spec is straightforward except for duplicating caps. Why are all TCB's and
CNode caps dup'd? Why does init_tcbs call init_tcb on the original object
but immediately configure_tcb on the dup? There are other places where the
dup cap is used instead of the original cap (e.g. init_cnode_slot). None of
this seems to matter on risc-v; maybe this matters on some other
architectures?
6. On risc-v all pages appear to be marked executable--including ipc
buffers! This seems just wrong and a potential security hole.
This looks to be a bug. Marking the NX bit on risc-v when the grant right
is not set gives me what I want. arm already did this.
7. Why does seL4_TCB_WriteRegisters take a _mutable_ seL4_UserContext? I'm
guessing this is a mistake in the xml spec (but haven't looked).
This looks to be a shortcoming in the python script that generates the
syscall stubs.
8. init_cspaces mystifies me. There are two loops over all CNodes; one
that does "COPY" operations and one that does "MOVE" operations. I
see
nothing explaining what's happening. I've read this code many times and
still don't get it; please explain.
9. According to comments, the use of a global static to setup the
UserContext for a new TCB is done because one cannot take the address of a
local variable. On what architecture is this true? On risc-v the context is
copied into "registers" before calling the kernel so this doesn't appear
to
be an issue with crossing the user-kernel protection boundary.
10. Memory reclamation. I'm unclear what happens to the memory used by
capdl-loader. The process does a TCB_Suspend call when it's done. Does this
cause the CSpace & VSpace to be reclaimed? For CAmkES this doesn't matter
as there's no support for allocating memory but I'm building a system where
this isn't true. How do I release memory (in particular) back to the
untyped pool?
This was discussed on the developers zoom call so no need to belabor it.
Sounds like I've got my work cut out for me...
I have a bunch of niggly code complaints/questions but
let's start with
the above.
-Sam