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