On Sun, Mar 27, 2022 at 3:43 PM Kent Mcleod <kent.mcleo...@gmail.com> wrote:
> On Mon, Mar 28, 2022 at 6:29 AM Sam Leffler via Devel > <devel@sel4.systems> 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-L386 > > 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/271d6a2405d571272b252fcf308e7581cdd6a1a1/camkes/templates/component.simple.c#L32-L36 > 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#L84-L92 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 > _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
