Hi All, If you do not know what recycle is and/or have not used it then you can probably ignore this e-mail. We are considering removing the recycle operation from cnodes, and replacing it with a 'revoke badges' operation. Currently the semantics of recycle are ill defined but can generally be summed up as "put an object back into its initial state". It turns out this is not particularly useful, and is completely unused by us. The proposal is to remove this and have an invocation that will only operate on endpoints and will remove any badged versions of that endpoint, hence the name 'revoke badges'. This is the current semantics of recycling an endpoint, and we see this as the only useful thing recycle does, hence the desire to keep it around. Whilst we do not use recycle we would like to first find out if anybody in the community is using recycle, or has a strong argument for why they would like it to stay. If this is you, please let us know, otherwise we will continue with our plans for removal. Adrian
On Wed, Oct 26, 2016 at 2:54 PM,
Whilst we do not use recycle we would like to first find out if anybody in the community is using recycle, or has a strong argument for why they would like it to stay. If this is you, please let us know, otherwise we will continue with our plans for removal.
A question rather than an argument: What is the cost difference between recycle vs. revoke + retype these days? (c.f. tables 7.1, 7.2, and 7.3, and section 7.1.5 in Elkaduwe 2010 [1]). Thanks, Jeff [1] https://ts.data61.csiro.au/publications/papers/Elkaduwe:phd.pdf
Hi Jeff,
The difference is that recycle does not require you to keep around (or be given) the untyped in order to then be able to perform the retype. Recycle is also a single syscall, and thus has better performance, than revoke + retype.
Adrian
On Wed 26-Oct-2016 3:11 PM, Jeff Waugh wrote:
On Wed, Oct 26, 2016 at 2:54 PM,
On Wed, Oct 26, 2016 at 3:37 PM,
The difference is that recycle does not require you to keep around (or be given) the untyped in order to then be able to perform the retype. Recycle is also a single syscall, and thus has better performance, than revoke + retype.
Oh yes, sorry, I know the difference in behaviour -- is the difference in performance in today's seL4 similar to what was outlined in the paper? I had it on my list of things to pay attention to based on those results. Thanks, Jeff
Right. I don't think we have measured the performance recently so I cannot comment off the top of my head, but at the same time I cannot think of a reason for why it would have changed.
Adrian
On Wed 26-Oct-2016 3:46 PM, Jeff Waugh wrote:
On Wed, Oct 26, 2016 at 3:37 PM,
It should have gotten a little better with the introduction of incremental retype, but probably hasn’t changed significantly.
Cheers,
Gerwin
On 26 Oct 2016, at 16:51, Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au wrote:
Right. I don't think we have measured the performance recently so I cannot comment off the top of my head, but at the same time I cannot think of a reason for why it would have changed.
Adrian
On Wed 26-Oct-2016 3:46 PM, Jeff Waugh wrote:
On Wed, Oct 26, 2016 at 3:37 PM,
On Wed, Oct 26, 2016 at 4:51 PM,
Right. I don't think we have measured the performance recently so I cannot comment off the top of my head, but at the same time I cannot think of a reason for why it would have changed.
Sounds like recycling is still worthwhile, even though the current user space libraries don't do so. I'm not super familiar with them -- is that due to a design limitation (not using slabs?) or just work not done? What's the cost of keeping it? Is there a burden on maintenance (particularly with new stuff landing) or re-verification? Thanks, Jeff
Yes, there are three main maintenance burdens:
- unclear (complex) semantics for most object types, which users are likely to get wrong without studying the spec in detail. I.e. danger of thinking you are using the kernel securely when you are not.
- dealing with the recycle case for any new object types, which can lead to diverging behaviour between platforms (this is what triggered this conversation)
- the recycle proofs are messy, and expensive for a feature that is not used
We currently have two major proof updates in the pipeline that would accelerate if recycle was dropped.
Dhammika’s old performance comparison is a bit simplistic. The main use case, recycling pages, is simple and as far as I can see wouldn’t cost more if done via revoke and unmap (depending on system construction, revoke might not even be necessary). Re-using other object types seems to be not high volume enough to justify major optimisations - you’d have to do them in a tight loop to see much difference.
In terms of semantics, endpoint badges are the only case where recycle achieves something that cannot easily be achieved with existing syscalls, that’s why we’re proposing to preserve that one.
Cheers,
Gerwin
On 27 Oct 2016, at 10:36, Jeff Waugh
On 10/25/2016 11:54 PM, Adrian.Danis@data61.csiro.au wrote:
Whilst we do not use recycle we would like to first find out if anybody in the community is using recycle, or has a strong argument for why they would like it to stay. If this is you, please let us know, otherwise we will continue with our plans for removal.
Robigalia doesn't and won't, except for the specific "revoke badges" usecase. We definitely need that, but not anything else. -- cmr http://octayn.net/ +16038524272
Hey Corey. There are two discussions together here, and I'd like to pull them apart a bit. Recycle was originally created to provide the "revoke badges + cancel previous sends with those badges" use case. The operations for other typed caps were added for some kind of consistency. The first question is whether anyone's using any of these additional operations. The second question is whether anyone uses the core "cancel waiting badged sends" bit. If no-one's using the additional operations (and there's little reason to use them, except to save on a system call) we can specialise and simplify the implementation a lot. If in addition no-one is using the second part, we can drop the API feature entirely. I'm in favour of dropping it entirely, and I have a user-level workaround which I can explain in more detail if you're interested [1]. So, long story, what were you planning on doing with badge cancellation in Robigalia? Cheers, Thomas. 1: OK, short version, a multi-user server can keep a spare thread around, revoke some badges, and then queue the thread in the endpoint as a sentinel, with a message saying "you may now reuse the revoked badges". On 29/10/16 02:24, Corey Richardson wrote: On 10/25/2016 11:54 PM, Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au wrote: Whilst we do not use recycle we would like to first find out if anybody in the community is using recycle, or has a strong argument for why they would like it to stay. If this is you, please let us know, otherwise we will continue with our plans for removal. Robigalia doesn't and won't, except for the specific "revoke badges" usecase. We definitely need that, but not anything else. _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
On 2016-10-30 20:36, Thomas.Sewell@data61.csiro.au wrote:
Hey Corey.
So, long story, what were you planning on doing with badge cancellation in Robigalia?
It's somewhat complicated to explain, and I haven't finished writing it up. Furthermore, these are just ideas right now, we haven't actually fully implemented it yet (though we've started on a few prototypes). I'll do my best to explain. In Robigalia, a badge corresponds 1-1 to a region of a process's vspace, which is the state for whatever methods exposed by the process. The backing storage for that region is borrowed from clients, which can revoke it at any point (and the process can of course also decide to destroy the region). If at some point the process is servicing a request and encounters a fault, the object that the request was to is dropped on the floor and the region is unmapped by the fault handler. To ensure that the badge (and thus the corresponding vspace region) can be re-used (to prevent resource exhaustion etc), the process is responsible for revoking all access via that badge. This prevents threads from exceeding their intended authority when a new object is created using that badge. I admit I don't fully understand the implications of Recycle here, or what the exact derivation subtree would look like in our usecase. For example, here's an example of object creation: seL4_CNode_Mint(my_cspace, my_root_ep_idx, my_root_ep_depth, some_free_slot_root, some_free_slot_index, some_free_slot_depth, AllRights, some_free_badge); seL4_CNode_Copy // map some space at the corresponding vaddr // setup initial state // setup IPC to transfer the newly minted cap seL4_ReplyRecv(...) Later when the object is to be destroyed, the hypothetical sequence of operations is: seL4_CNode_Recycle(my_cnode, some_free_slot_index, some_free_slot_depth) // unmap region
1: OK, short version, a multi-user server can keep a spare thread around, revoke some badges, and then queue the thread in the endpoint as a sentinel, with a message saying "you may now reuse the revoked badges".
These seems like it should work just as well for our purposes, although I'm a bit worried about timeliness of reusing the badge. I guess I'd have to add some sort of tombstone state for that badge while it's waiting for the queue to drain. Best, -- cmr http://octayn.net/
participants (5)
-
Adrian.Danis＠data61.csiro.au -
Corey Richardson -
Gerwin.Klein＠data61.csiro.au -
Jeff Waugh -
Thomas.Sewell＠data61.csiro.au