On 4/11/24 12:12 AM, David Martin wrote:
Hello, I'm currently working with seL4 & Polarfire (RISCV) and I'm working with a single core at the moment (doing some testing and understanding how seL4 works). Polarfire has 4 cores and I'd like to start using all of them in a multikernel configuration (every hart running its own sel4 kernel). I've found the following RFC: https://sel4.atlassian.net/browse/RFC-17 where Kent McLeod has done some work (https://github.com/kent-mcleod/camkes-manifest/blob/kent/multicore2/master.x...) but only for ARM. Does someone know if the same approach will be taken for RISCV? or even better, if someone has already done it?
Thanks, David. _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
This shouldn't be hard. I managed to run two instances of Linux on the JH7110 -- one Linux nommu on the S7 hart and the other regular Linux on the 4x U7 harts. This is kind of equivalent to run one Linux on your Polarfire Hart 0 (E51) and another on Hart 1-4 (U54). As Stefan pointed out in the RFC, (I also confirmed this in the privileged spec), the ASIDs are per-hart. Thus, from pure RISCV perspective, there's nothing stopping you. These 4 instances will run just fine without modification and they don't have to know about others existence. You only have to make sure the resources on the platform, such as physical memory, devices, etc., are partitioned correctly -- possibly by supplying different dtbs to each one.
The challenging issue is very likely how to design the notification mechanism, and tailor to your needs. As said in the RFC, with the traditional CLINT/PLIC configuration, you only get 1 interrupt ID for IPI. Thus, you probably want to maintain a bitmap or similar in shared memory to distinguish the source harts that's signalling you, and use atomic instructions to maintain the bitmap. I haven't checked on Kent's work, but I'd imagine most of the work is on the user side rather than kernel. Sending IPI on RISCV is straight forward -- you just call the sbi_send_ipi...
Bo