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
To: devel@sel4.systems
Subject: [seL4] Multikernels and resource transfer
Message-ID:
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
