I have done hunting in both the kernel and the capDL-loader and can shed some light on what is going on. On the kernel side there is implicit knowledge that an IRQHandler is the child of an IRQControl cap, so the single bit of depth does not get used up here. As a result you should be able to take advantage of the single bit of depth, delegate an IRQHandler and be able to revoke it. Although due to the single bit it cannot be re-delegated.

Looking into the capDL-loader we see that it is in fact delegating capabilities, and not providing the originals. This means the IRQHandler cap Andrew thought was the original, was in fact a delegated cap that already had the single bit of depth used and hence the re-delegation could not be revoked. There are some comments in the capDL-loader that seem to imply it does not have enough knowledge to know when it should copy caps and when it should move, and so it is pessimistic and always copies, but I don't know enough to understand why this would be the case.

tl;dr capDL-loader is hoarding the original IRQHandler caps preventing what is an otherwise correct delegation and revoke from working

Adrian

On Thu 16-Feb-2017 11:05 AM, Gerwin.Klein@data61.csiro.au wrote:

Well, in theory infinity (up to size of memory) is what’s happening for Untypeds, because there is no need to store anything for the level - you can tell just by their address. So in that sense it exists.

Cheers,
Gerwin

On 16.02.2017, at 10:57, Gernot.Heiser@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.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

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel