Hi Robbie,
You could run seL4 on the Cortex-A and eChronos on the Cortex-R. If you intend to run a single single-threaded application on the Cortex-R, you could run the server without an OS.
I recommend that you load and start the server OS (or bare metal server) using the elfloader rather than an seL4 application:
1. In its current form, the elfloader is linked with a CPIO archive that contains the user image and seL4. You would need to modify the build system to include a third object in this archive.
2. Modify the elfloader code to load this third object: https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/common.c#L...
3. You will need to write code to boot the Cortex-R CPUs. This code is not for the Ultrascale, but hopefully it will give you a head start: https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/plat/zynq7...
4. Modify seL4 to reserve the physical memory that your server will occupy use: https://github.com/seL4/seL4/blob/master/include/plat/zynqmp/plat/machine/ha...
Since your server will have access to all physical memory, sharing data between client and server will be easy. All that remains is a method for notifying client and server when data has been updated. While polling shared memory would be a good start, you might be able to use software generated IRQs in your final solution.
Regards,
- Alex
From: Devel devel-bounces@sel4.systems on behalf of Gernot.Heiser@data61.csiro.au Gernot.Heiser@data61.csiro.au Sent: Wednesday, November 7, 2018 6:53 AM To: devel@sel4.systems Subject: Re: [seL4] seL4 on Heterogeneous Processing Architectures (Zynq UltraScale+ MPSoCs) On 6 Nov 2018, at 22:27, Blam Kiwi blam.kiwi@gmail.com wrote:
I wasn't fully appreciating the difference between the MPU and MMU in relation to seL4. If the R5's can't be supported then that simplifies the decision space somewhat. Guess I'll evaluate the RTOSes before throwing my hands in the air and rolling my own design.
You could run eChronos. It’s an RTOS with a (partial) verification story that supports the MPU: https://ts.data61.csiro.au/projects/TS/echronos/
Gernot