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 <[email protected]<mailto:[email protected]>> wrote: On Wed, Oct 26, 2016 at 4:51 PM, <[email protected]<mailto:[email protected]>> 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 [email protected]<mailto:[email protected]> https://sel4.systems/lists/listinfo/devel
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
