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.gacek@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.Heiser@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.Klein@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.gacek@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