​Hi Robbie,


Sorry for the late response.


b) I require the use of the Cortex R5 cores in DCLS mode for trusted code with high fault tolerance requirements. 
--- The Cortex R5 processors lack of MMUs, so seL4 does not support R processors.

c) I require the use of the Cortex A53 cores for running unsafe Linux VMs.
--- Are you going to run one SMP Linux VM or multiple single-core Linux VMs? We are developing the support for running Linux VM on aarch64, and hopefully we will push out the code out soon.

d) It's my understanding that seL4 lacks 64-bit multicore support for its own scheduler, but VMs running on seL4 could be provided with access to all the cores? (Eg: Linux)
- I believe the experimental aarch64 multicore support exists in the mainline seL4 kernel. A virtual machine monitor (VMM) needs to emulate the PSCI interface and intercept SMC calls so that the VMM is able to create multiple VCPUs and assigned the VCPUs to an SMP Linux VM. The scheduling of VCPUs is still managed by seL4.

e) It's my understanding that seL4 lacks heterogeneous task scheduling, and cannot manage both the Cortex R5 and Cortex A53 cores.
--- The Cortex R5 cores are not supported.

[1] It's not possible to boot an seL4 kernel on one processor and have it manage the other.
--- I do not quite understand this, but my initial response is NO. Please add more info. 

[2] Use TrustZone to create vCPUs for the Cortex R5 and A53 modules and boot an seL4 kernel on each. 
--- TrustZone does not create vCPUs (at least in the sense of virtualization). In seL4 parlance, a VCPU is an seL4 kernel object. 

[3] Some domain specific protocol is required for the CPU modules to communicate and share resources. 
--- The SoC may provide some hardware support for communicating between Cortex-A and Cortex-R CPU modules. I am not familiar with the Zynq board. Otherwise, shared memory should work.


Regards,

Yanyan


From: Devel <devel-bounces@sel4.systems> on behalf of Blam Kiwi <blam.kiwi@gmail.com>
Sent: Thursday, October 11, 2018 1:48 PM
To: devel@sel4.systems
Subject: [seL4] seL4 on Heterogeneous Processing Architectures (Zynq UltraScale+ MPSoCs)
 
I am investigating the use of seL4 on heterogeneous architectures such as the Zynq UltraScale+ MPSoCs. I have a non-trivial use-case I'm investigating that involves utilising both the Cortex-R5 cores and Core-A53 cores for different applications. I'm rather new to seL4 development so I'm a bit stuck and need some advice. 

It's easiest if I just list my requirements and assumptions for my architecture design:

a) I am targeting the Zynq US+ platform and wish to use seL4 as the OS Kernel to manage system resources and run virtual machines. 
b) I require the use of the Cortex R5 cores in DCLS mode for trusted code with high fault tolerance requirements. 
c) I require the use of the Cortex A53 cores for running unsafe Linux VMs.
d) It's my understanding that seL4 lacks 64-bit multicore support for its own scheduler, but VMs running on seL4 could be provided with access to all the cores? (Eg: Linux)
e) It's my understanding that seL4 lacks heterogeneous task scheduling, and cannot manage both the Cortex R5 and Cortex A53 cores.

This leads me to make the following architectural conclusions:
 
[1] It's not possible to boot an seL4 kernel on one processor and have it manage the other.   
[2] Use TrustZone to create vCPUs for the Cortex R5 and A53 modules and boot an seL4 kernel on each. 
[3] Some domain specific protocol is required for the CPU modules to communicate and share resources. 

Any help or advice would be appreciated.

Regards, 
Robbie