On Tue, May 10, 2022 at 1:42 AM Kent Mcleod <kent.mcleo...@gmail.com> wrote:
> 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.
>
Thanks for the pointers. I use the attribute to setup the C symbols. Will
check out the AddressSpaceAllocator.
>
> > 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.
>
Thanks for the suggestion. I avoided touching the IDL syntax because we're
not really using it (we define methods to take opaque blobs that are
marshalled in Rust). But handling the caps in the CAmkES marshaling code
would be good (I depend on single-threading to avoid locking issues).
Re: Grant rights, aside from the extracaps count in the MessageInfo struct
you also need to set Grant on RTReply if you want to attach caps to
replies. And capdl doesn't support that (last I looked in upstream).
> 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
