[seL4] Re: propagating initial thread's capabilities

On Sun, Mar 27, 2022 at 3:43 PM Kent Mcleod wrote:

On Mon, Mar 28, 2022 at 6:29 AM Sam Leffler via Devel wrote:

...

The rootserver gets various caps setup for it by the kernel (see Table

9.1

...

in the manual). This includes the gobal ASID, IRQ, Domain, and Sched controllers. I need these caps in a process created by the rootserver. This is within a CAmkES environment. So far I've created CAmkES component attributes that signal the rootserver should hand-off a cap by moving the rootserver's cap to the designated CNode just before it terminates. This involves modifications to CAmkES, capDL, and the rootserver. Is there a better way? Is there an existing example of doing this? Are any of these global objects accessible some other way than hand-off from the rootserver?

CapDL and the capdl-loader-app should already be able to move these caps without extra modifications. They exist in the spec:

https://github.com/seL4/capdl/blob/master/capDL-tool/CapDL/Model.hs#L376-L38...

The "interrupts" tutorial (https://docs.sel4.systems/Tutorials/interrupts.html) works by having the irq_control cap moved into one of the component CNodes. The capdl spec fragment that does this is: ``` cnode_timer { // ... 0x8: irq_control } ``` Note that this tutorial isn't CAmkES but uses a CapDL spec and the rootserver to set up the tutorial apps.

Within camkes, I'm not immediately aware of any public examples that use any of these caps. There's one template that does appear to support moving a sched_control cap to a component:

https://github.com/seL4/camkes-tool/blob/271d6a2405d571272b252fcf308e7581cdd... A custom CAmkES template could be added which would work for any of the special caps you mentioned as they are all defined in the library camkes uses to generate specs:

https://github.com/seL4/capdl/blob/master/python-capdl-tool/capdl/Object.py#...

Very nice. This looks to eliminate many of my mods. Some questions: 1. I've been handing off the ASDIPool object at seL4_CapInitThreadASIDPool but following your suggestions appears to create a new ASDIPool instead of passing along the rootserver's. My template snippet is: /*- if configuration[me.name].get('asid_pool', False) -*/ /*- set asid_pool = alloc('asid_pool', type=seL4_ASID_Pool, core=configuration[me.name].get('domain_ctrl')) -*/ const seL4_CPtr ASID_POOL = /*? asid_pool ?*/; /*- endif -*/ (I blindly copied the core setting, looks like it may be ignored). IIUC I may be able to have multiple asid pools (depending on the arch) and that may be preferred but for now I was intending to assign all my vspace roots to the same pool. Is that happening? (I'm just going off what I see in system.cdl & capdl_spec.c). If I am getting a new ASID pool is there any way to express that I want seL4_CapInitThreadASIDPoo and not a new object? 2. UntypedMemory. My first foray down this path was to hand-off the UntypedMemory objects. Can I use similar techniques to make this happen w/o mods to signal the rootserver to DTRT. Seems more difficult given this comes via BootInfo and requires moving an unknown (at compile-time) # of UntypedMemory caps. My current scheme moves the untypeds and also passes along a page with an updated version of BootInfo to identify the set of caps for the UntypedMemory objects. 3. While I'm getting a lesson in CAmkES templates + capDL, is there a way to arrange to allocate a FrameObject and install the cap to it in "my_cnode" (or somewhere else that I can access to unmap the page so I have just page-size gap in the vspace)? This is for temporarily mapping pages to write their contents (as the rootserver does when constructing a component's vspace contents). I've got something ugly that seems to DTRT but would love to "do it right".

The loader moves these special caps in a final move phase after all other caps have been created so that they are moved after any caps have already been derived from them.

These global objects can't be copied or created and so the only way for them to get given to a new CSpace is for them or a CNode that they're stored in to be moved to the target CSpace.

...

-Sam _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems