[Thanks again for your timeley responses, more inline] On Sun, Mar 27, 2022 at 6:11 PM Kent Mcleod <kent.mcleo...@gmail.com> wrote:
> On Mon, Mar 28, 2022 at 11:04 AM Sam Leffler <sleff...@google.com> wrote: > > > > 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? > > I was assuming you wanted the seL4_CapASIDControl cap. I don't think > there is a way to move/copy the seL4_CapInitThreadASIDPool cap without > teaching the CapDL spec and rootserver about it. I don't think that > would be an uncontroversial change. Having multiple ASID pools > shouldn't be an issue (unless you're extremely space constrained as > each one is 4k). Having more ASID pools allows you to have slightly > better isolation between untrusted components if they don't share an > ASID pool but are able to dynamically assign/unassign vspaces to an > ASID pool object because of the ASID-reuse caveat: > > https://github.com/seL4/seL4/blob/master/CAVEATS-generic.md#re-using-address-spaces-arm-and-x86 > (this does also apply to RISCV). > Ok. The manual seemed to indicate support for multiple asid pools was arch-dependent so I was just going to re-use the existing one. Now I know how to do it either way, thank you! > > > > > 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. > > > > I believe the only existing way you could do this is by naming the > exact untypeds in the spec, by providing a physical address. As you > say, this is hard to do if you don't know ahead of time what the > bootinfo is going to contain (you can precalculate it though if you > know the size of the rootserver and kernel images). It still seems > that the way forward here is to have some sort of builtin way of > parameterizing the spec to describe how the loader can move remainder > UT objects into a range of slots and also fill in a frame with the > book keeping information. > I plumbed an attribute for a CNode that means "move the untypeds here", then added a new FillFrame_BootInfo token to signal the rootserver fill-in the frame contents with updated info. This gives me what I want but required hacking things through capDL. The destination CNode needs to be sized big enough to hold the untypeds which is fragile but was gonna revisit that later. > > > > 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 mechanisms do exist. The seL4HardwareMMIO template > ( > https://github.com/seL4/camkes-tool/blob/master/camkes/templates/seL4HardwareMMIO.template.c#L52 > ) > is an example where the mapping caps are moved into the CSpace of the > component. The magic is encapsulated in the register_shared_variable() > implementation which has to call `cap.set_mapping_deferred()` on each > frame cap and add the list of caps to an address space allocator with > `addr_space.add_symbol_with_caps(symbol, sizes, caps)` to defer > assigning the CNode slot it's placed in until the VSpace is created > for the component. This generates a spec where the cap containing the > VSpace mapping is moved into a specified CNode slot so that the > mapping can be unmapped. > Ok. I found register_shared_variable but couldn't make it do what I wanted. Hopefully your hints will get me over the hump. > > >> > >> > >> 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
