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 <[email protected]>
To: [email protected]
Subject: [seL4] Multikernels and resource transfer
Message-ID:
        <cajemun_l49o9btyx03z35uq6s21t80wpujp86gd5xyymh4b...@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

_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to