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,  <[email protected]> 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, [email protected] 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 <[email protected]> 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
>>> [email protected]
>>> https://sel4.systems/lists/listinfo/devel
>>
>> _______________________________________________
>> Devel mailing list
>> [email protected]
>> https://sel4.systems/lists/listinfo/devel
> _______________________________________________
> Devel mailing list
> [email protected]
> https://sel4.systems/lists/listinfo/devel

_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to