[seL4] Re: sel4cp and networking driver

I am not aware of a specific definition for a static system in the context of seL4. I think typically when people refer to a static system on seL4 they mean that after the initial task has setup the system, the capability distribution of the system remains the same. I'm not quite sure what you mean by exchange of frames though? On 12/8/23 12:18, Sid Agrawal wrote:

Hi, Sel4cp documentation states that it is for building static systems. I wanted to dig into what we mean by static systems here, as some exchange of resources is needed for the system to function.

Do all of these have to be true for the system to be considered static? After the monitor has created the initial set of PDs:

- No new PDs can be created - All untyped memory is kept with the monitor always - No endpoints can be exchanged between PDs - Exchange of frames between PD is ok.

Best, Sid

On Tue, Aug 8, 2023 at 8:28 AM Sid Agrawal wrote:

...

Thanks to both of you. This is quite helpful.

On Tue, Aug 8, 2023 at 1:47 AM Indan Zupancic wrote:

...

[CAUTION: Non-UBC Email]

Hello Sid,

...

1. Looking at the DTS files for tqma8xqp-1gb in the seL4 repo. I see one big file and another overlay. Why are there two for the same board? I would have understood if one was for the SoC and another for the board. - tools/dts/tqma8xqp1gb.dts

- src/plat/tqma8xqp1gb/overlay-tqma8xqp1gb.dts See Ivan's answer. As I was involved with the tqma port, I can confirm

On 2023-08-08 05:20, Sid Agrawal wrote: that tools/dts/tqma8xqp1gb.dts is the de-compiled Linux DTB that came on the SD card with the STKa8Xx dev board, see:

https://www.tq-group.com/en/products/tq-embedded/arm-architecture/stka8xx/

Specifically, I think it's based on version 25 of the SDK:

https://support.tq-group.com/en/arm/tqma8xx/linux/yocto/overview

The reason there is no board DTS file is because tqma is a module which exposes almost all pins, so there are very few module hardware choices made. And seL4 only uses on-chip peripherals, so nothing board specific is left. In hindsight the tqma8xqp1gb platform would have been better named imx8qxp, with configurable UART and memory amount.

...

2. I see that the VMM example (https://github.com/Ivan-Velickovic/sel4cp_vmm), as well as the sDDF example (https://github.com/lucypa/sDDF/tree/main/echo_server), uses the iMX8MM-EVK board. - How different are iMX8MM-EVK and tqma8xqp1gb? Very different for SoCs in the same product range, the iMX8MM-EVK is based on the i.MX8M Mini SoC. But most changes aren't really software visible.

The imx8qxp SoC is very complex and annoying because of the SCU. If you don't need ECC memory, GPU, multiple displays and Ethernet ports, go for a different SoC without SCU. That said, if U-Boot configures the SCU correctly for your needs, you can ignore the whole SCU mess for a while.

...

- What is the preferred board for the sel4cp effort at Trustworthy Systems? This way, I will just get that board, and it would be easier for me to follow your efforts along the way and maybe even contribute :) I don't know what board they use, but STKa8Xx, the tqma dev board, used to be very expensive.

...

3. For the VMM example in particular. - Is it correct to say that there are two dts files at play, one needed by seL4(which we get from the seL4 repo) and the other needed by the Linux Guest, which we get from the sel4cp_vmm repo? The seL4 one describes all hardware peripherals so that all the device untyped memory regions can be created. Assuming it correctly describes the SoC, it never needs to be changed or updated.

The VMM one is needed to tell the Linux VM what hardware and memory it can actually use. Not all boards have all peripherals connected, so the sel4cp_vmm DTS file is also the board file describing the actual hardware available.

Greetings,

Indan

---

Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems