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.xml)
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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
