Deriving and Revoking IRQControl caps
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
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
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
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
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
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
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<mailto: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<mailto: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><mailto: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><mailto: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<mailto: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><mailto: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<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel
Good, that makes perfect sense. I remember discussions with Andrew on copying vs moving. capDL doesn’t specify which caps are master and which are not, and so you can’t tell which one is which if there are more than one, and it’s a bit annoying to find out whether there is more than one. Two ways forward: change capDL to allow saying that you want the master, or try to figure out if that fact is derivable by counting how many caps to that IRQ (or object for other caps) are in the system. My guess is that most IRQs will only have precisely one cap to them in the initial system state. Cheers, Gerwin On 16.02.2017, at 11:59, Danis, Adrian (Data61, Kensington NSW) <Adrian.Danis@data61.csiro.au<mailto:Adrian.Danis@data61.csiro.au>> wrote: 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<mailto: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<mailto: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><mailto: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><mailto: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<mailto: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><mailto: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<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel
A short-term workaround would be to write that part of the code yourself, i.e. have (trusted) initialisation code that gets the full IRQControl cap and that produces the derived IRQHandler caps, passing on the masters of that (and maybe removes the IRQControl cap if you want to make sure nothing else can pick it up). Cheers, Gerwin On 16.02.2017, at 12:23, Klein, Gerwin (Data61, Kensington NSW) <Gerwin.Klein@data61.csiro.au<mailto:Gerwin.Klein@data61.csiro.au>> wrote: Good, that makes perfect sense. I remember discussions with Andrew on copying vs moving. capDL doesn’t specify which caps are master and which are not, and so you can’t tell which one is which if there are more than one, and it’s a bit annoying to find out whether there is more than one. Two ways forward: change capDL to allow saying that you want the master, or try to figure out if that fact is derivable by counting how many caps to that IRQ (or object for other caps) are in the system. My guess is that most IRQs will only have precisely one cap to them in the initial system state. Cheers, Gerwin On 16.02.2017, at 11:59, Danis, Adrian (Data61, Kensington NSW) <Adrian.Danis@data61.csiro.au<mailto:Adrian.Danis@data61.csiro.au>> wrote: 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<mailto: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<mailto: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><mailto: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><mailto: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<mailto: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><mailto: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<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel
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.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
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 <mpj@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.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
participants (5)
-
Adrian.Danis＠data61.csiro.au -
Andrew Gacek -
Gernot.Heiser＠data61.csiro.au -
Gerwin.Klein＠data61.csiro.au -
Mark Jones