In a multikernel setup, each kernel manages its own memory allocation, as the main memory is distributed among all valid kernels. Hence, the described scenario does not apply.

Regards, Qian.

Message: 1 Date: Thu, 13 Feb 2020 00:49:11 -0500 From: Demi Obenour demiobenour@gmail.com To: devel@sel4.systems Subject: [seL4] Multikernels and resource transfer Message-ID: CAJEMUN_L49O9btYx03Z35uQ6S21T80wPujP86Gd5XyymH4BQ6g@mail.gmail.com Content-Type: text/plain; charset="UTF-8"

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