On Mon, May 9, 2022 at 8:07 AM Sam Leffler via Devel devel@sel4.systems wrote:
- I need multiple VSpace "holes" to map page frames. This is the
equivalent of what capdl_loader_app sets up in init_copy_frame. To do this I setup named static arrays and unmap the frame caps in camkes.c:post_main. This works but using a per-component attribute to enable this was awkward so I ended up adding a "copyregion" primitive to camkes. Is there a way to do this without adding to the camkes' syntax? It would also be nice not to allocate page frames only to release them at start but I didn't see a way to do this in capdl; is it possible (e.g. an easy way to leave an empty slot in the pt/pd)?
There is the `AddressSpaceAllocator` class in the python capdl library that is intended for describing more complicated backing frame policies for an address space. It should be possible to use this to declare regions of memory that are not backed by any frames. The implementation of `register_stack_symbol()` sets up a region of memory with a memory hole on each end for guards. So you could declare a region that is just guards and I think there is enough information for the tooling that builds the address spaces to know which page tables to create that back the holes. You can use a compiler attribute to send a symbol to a non-loadable linker section, eg `__attribute__((section("align_12bit")))` that is declared by the camkes linker script as non-loadable.
- I pass capabilities with ipc msgs using camkes' rpc-connector templates.
This requires multiple small changes that I want to enable only when being used (e.g. parameters to seL4_MessageInfo_new). My current plan is to add an optional keyword to a connection defn to enable support; e.g.
connection seL4RPCCall foo(xfer_caps, from a, to b);
Does this make sense or is there a better way? I rejected creating new connector templates that enable xfer_caps because I see this as a concept that applies to any ipc-based connector.
The standard connector templates already allow grant and grant reply permissions to be set on endpoint object caps I believe. Maybe you want to add a new syntax to procedure/method syntax to be able to define a parameter type that is a CPtr instead of a regular variable. The IPC generation could then use this information to correctly set the seL4_MessageInfo arguments correctly. Alternatively, you could add a new connector that just gives low level seL4 object access and write your own library functions for marshalling and unmarshalling rpc calls with cap transfer.
Kent.
Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems