On Mon, May 9, 2022 at 8:07 AM Sam Leffler via Devel <devel@sel4.systems> wrote:
>
> 1. 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.
> 2. 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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
