Hi Adrian, On 06.02.2016 00:40, Adrian Danis wrote:
My suggestion at this point in time would be to implement an allocation strategy that supports plain old incremental retype. Remembering that any strategy that works for incremental retype can be trivially made to work with retype at offset.
I will go for it then. ;-)
Currently there are no plans to bring retype at offset to the verified kernel. By my understanding (note that I'm not an actual verification person) the main two reasons for this are * The heap used is both a more complicated data structure, and has very complicated invariants due to the nature of the searches performed on it * Changing the implementation of the cap derivation tree will invalidate large parts of the proof, which will simply require large amounts of verification people power to fix
Whilst we will always have an experimental branch, it is never clear what experiments we will continue and which we will abandon for various reasons. This uncertainty is of course mostly applicable to items that do not have roadmap for verification and life on the master branch. Whilst the searchable cdt (and the associated retype at offset) is clearly useful, unfortunately it is not on the roadmap (https://sel4.systems/Info/Roadmap/) and so it's continued existence is forever uncertain.
These insights are very valuable. Thank you for sharing them. Cheers Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth