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
?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
Hi Yanyan,
Sorry for the confusing wording, I'm still familiarizing myself with seL4 and its community nomenclature. Thank you for taking the time to answer my noobish questions.
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.
Regarding the aarch64 VMs, I would be interested in running many single core Linux VMs (over comitted, but mostly idle). I don't know if the seL4 VMM is designed for this use case. The architecture requirements impose running arbitrary untrusted code, so SMP VMs would be desirable in the general case but not necessary.
Last with the cross CPU communication/booting, I'm leaning towards an architecture design where Subsystem A (Server) runs on the R5 cores, and Subsystem B (Client) runs on the A53 cores. Now subsystem B depends on A, and A needs to be booted and configured before B is in a well defined state. B will also have continued communication with A. I suppose the question I was trying to ask is if seL4 has any design decision that prohibits two independent CPUs booting, synchronizing and communicating to each other with shared resources. The boot/trustzone stuff was a misguided jump to asking about an implementation detail.
Regards, Robbie
On Tue, Nov 6, 2018 at 1:33 PM Yanyan.Shen@data61.csiro.au wrote:
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
On 6 Nov 2018, at 22:27, Blam Kiwi <blam.kiwi@gmail.commailto: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
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
-
Alexander.Kroh＠data61.csiro.au -
Blam Kiwi -
Gernot.Heiser＠data61.csiro.au -
Yanyan.Shen＠data61.csiro.au