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 <[email protected]> wrote: > Thanks to both of you. This is quite helpful. > > > On Tue, Aug 8, 2023 at 1:47 AM Indan Zupancic <[email protected]> wrote: > >> [CAUTION: Non-UBC Email] >> >> Hello Sid, >> >> On 2023-08-08 05:20, Sid Agrawal wrote: >> > 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 >> 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 -- [email protected] To unsubscribe send an email to [email protected]
