On Wed, Oct 26, 2016 at 3:37 PM, Adrian.Danis@data61.csiro.au wrote:

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

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, <Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au> wrote: 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

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

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

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 <jdub@bethesignal.orgmailto:jdub@bethesignal.org> wrote:

On Wed, Oct 26, 2016 at 4:51 PM, <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.

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 _______________________________________________ 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,