[seL4] Re: Multikernel in RISCV

Hello David, On 2024-06-05 14:56, David Martin wrote:

If I'm not mistaken, that could be done using a chunk of memory defined as device untyped and then used by each kernel (for my tests, I'll use 2 harts) to write/read. --> Is that a good understanding on how shared memory is suppose to be used within seL4?

Yes, adding reserved memory regions with nomap to the DTS is the way to tell seL4 not to use it for any kernel objects and to not map it. Then you can use it as shared memory between the two harts. Sadly there is no more convenient way of defining shared memory. I recommend using the KernelCustomDTSOverlay option to add such shared memory regions instead of modifying existing DTS files. Greetings, Indan