Ah, Mark understands cap virtualisation ;-) Something along those lines would probably work. In fact, I only today thought of the virtualisation approach in the context of another problem that was discussed internally. It looks like my AOS teaching is deficient on sharing the power of capabilities ;-)
Gernot > On 16 Feb 2017, at 18:07, Mark Jones <m...@pdx.edu> wrote: > > I'm wondering if you could handle this using endpoint caps? You'd > start by allocating an endpoint e. Every client would get a cap to > e that is badged with the appropriate irq. Meanwhile, a server > thread, with access to the IRQControl cap, would wait on e. For > each incoming message, the server would pass the associated badge > (i.e., irq number) to the IRQControl and then transfer the resulting > handler capability back to the caller. For this to work, the client > cap should be a "derived badged" cap (as in Fig. 3.1 of the current > manual), each of which is the *unique* child of an "original badged" > cap. This would allow the client's access to the IRQControl to be > removed at any time by calling revoke (and then, perhaps, delete > too) on the latter capability. > > [That said, the restriction to one level of deriving still seems a > bit awkward. I agree that the same could be said for any fixed > limit. However, my understanding is that Dhammika's prototype > allowed for 128 levels (i.e., 7 bits) and I'm guessing that would be > close enough to infinity for most practical purposes :-) Not that > it would be easy to make such a change, so maybe the workaround > above is good enough for now ... unless there's a flaw that I've > overlooked?] > > All the best, > Mark > > >> On Feb 15, 2017, at 3:57 PM, gernot.hei...@data61.csiro.au wrote: >> >> Nope, “infinity” (or any finite approximation ;-) is out in this case. >> Earlier L4 versions had derivation trees up to 16 deep, and they were a big >> pain. There’s reason to stick with one, but then should avoid it making >> effectively zero for some cases (like yours). >> >> Gernot >> >>> On 16 Feb 2017, at 10:53, Andrew Gacek <andrew.ga...@gmail.com> wrote: >>> >>> I have no idea how seL4 tracks derivations, but how reasonable is an >>> answer like 'infinity'? Is anything in seL4 tracked to infinity? How >>> far are untypeds tracked? >>> >>> -Andrew >>> >>> On Wed, Feb 15, 2017 at 5:49 PM, <gernot.hei...@data61.csiro.au> wrote: >>>> Andrew’s use case makes sense to me at first glance. >>>> >>>> I think IRQ caps are special in a way here, as there is a difference to >>>> other derived caps: A cap for a single IRQ is logically a top-level cap, >>>> similar to a frame cap. This present model basically means that you can’t >>>> delegate them, unlike other objects. Seems like a weakness (if not >>>> conceptual inconsistency) in our present model. >>>> >>>> As Gerwin indicates, just moving to two levels is not necessarily a good >>>> solution. I tend to think that the only valid magic numbers are zero, one, >>>> and infinity ;-) >>>> >>>> Gernot >>>> >>>>> On 16 Feb 2017, at 10:31, gerwin.kl...@data61.csiro.au wrote: >>>>> >>>>> Currently, this is mostly implementation driven - there is one bit >>>>> reserved for the derivation level in the data structure that tracks it. >>>>> It’s possible that IRQControl caps specifically have some space left that >>>>> could be used for more levels, but it would make them a special case. >>>>> >>>>> If we reserved 2 bits for the level, you’d hit the same problem somewhat >>>>> later, though, and the argument at the time was that (very small) >>>>> finiteness of derivation levels of these control caps has to be solved at >>>>> user level anyway and it’s better to make you think of it immediately >>>>> rather than when you’ve designed yourself into a corner. >>>>> >>>>> Maybe you do have a very good use case here, though, and we should >>>>> rethink that argument (as we did for endpoint caps - their level of >>>>> specialness is pretty messy, but we considered it worth the pain). I >>>>> should probably leave that part to Kevin. >>>>> >>>>> Cheers, >>>>> Gerwin >>>>> >>>>>> On 16.02.2017, at 03:20, Andrew Gacek <andrew.ga...@gmail.com> wrote: >>>>>> >>>>>> Based on the seL4 manual it sounds like IRQControl caps only support >>>>>> one level of derivation. What is the reason for this restriction? We >>>>>> encountered a case where we wanted to hand out an IRQControl for a >>>>>> specific irq and then later revoke access, but we couldn't do it >>>>>> because the IRQControl for a specific irq is already a derived >>>>>> capability. >>>>>> >>>>>> -Andrew >>>>>> >>>>>> _______________________________________________ >>>>>> Devel mailing list >>>>>> Devel@sel4.systems >>>>>> https://sel4.systems/lists/listinfo/devel >>>>> >>>>> _______________________________________________ >>>>> Devel mailing list >>>>> Devel@sel4.systems >>>>> https://sel4.systems/lists/listinfo/devel >>>> _______________________________________________ >>>> Devel mailing list >>>> Devel@sel4.systems >>>> https://sel4.systems/lists/listinfo/devel >> _______________________________________________ >> Devel mailing list >> Devel@sel4.systems >> https://sel4.systems/lists/listinfo/devel > > > _______________________________________________ > Devel mailing list > Devel@sel4.systems > https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
