In a multikernel, how would retyping work? Obviously, the kernel cannot allow untyped X to be used for page tables if user code on another core might still have write access to it. Would retyping involve some sort of in-kernel concurrency?
Obviously, the clustered multikernel avoids this, but making applications (as opposed to low-level libraries and services) work around kernel limitations seems rather unappealing. Sincerely, Demi _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
