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#L264

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/zynq7000/smp.c#L65

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/hardware.h#L58

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 <[email protected]> on behalf of 
[email protected] <[email protected]>
Sent: Wednesday, November 7, 2018 6:53 AM
To: [email protected]
Subject: Re: [seL4] seL4 on Heterogeneous Processing Architectures (Zynq 
UltraScale+ MPSoCs)
  
On 6 Nov 2018, at 22:27, Blam Kiwi <[email protected]> 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    
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to