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 _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
