?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