[seL4] Re: camkes q's

On Tue, May 10, 2022 at 1:42 AM Kent Mcleod wrote:

On Mon, May 9, 2022 at 8:07 AM Sam Leffler via Devel 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