sel4cp and networking driver

Sid Agrawal

5 Aug 2023 5 Aug '23

10:47 a.m.

Hi, I would like to setup a working example on sel4 with picoTCP and an eth driver. I came across this [1] from one of the seL4CP/sDDF demos and [2] from the camkes examples. However, I do not have access to those particular boards. I have a rspi4 and a Toradex Colibri iMX8X module with the aster carrier board. This Toradex has the same SoC ( iMX8X) as the tqma8xqp-1gb mentioned on the sel4cp website. Do you folks have any thoughts on how much effort it is getting seL4 working on "Toradex Colibri iMX8X" given it is supported on "tqma8xqp-1gb" which has the same SoC? I do not mind buying a specific development board as long as I know that I can use it for a while :) For folks who are working on sel4cp, what kind of dev setup do you have? I am looking for basic conveniences like flashing the image via USB (so I do not have to add/remove an SD card), TFTPboot, and some simple device drivers. I did see the instructions on TFTPbootat [3]. However, does it matter if the image was built via the sel4test of sel4cp? I think not, but I just wanted to double-check. And lastly, a higher-order question about seL4cp. How does sel4cp tie into the example in seL4_Libs [3], which has barebones libc and a VMM? Which is what I have used so far with sel4test. I understand that both sel4cp and camkes are for static systems, but I thought that I could use sel4cp to start some initial processes, such as a driver, a memory server, and some management processes. And later use process_spawn from seL4 libs to start additional PDs. Best, Sid [1] https://github.com/lucypa/sDDF [2] https://github.com/seL4/global-components/tree/master/components/Ethdriver/i... [3] https://docs.sel4.systems/Hardware/GeneralARM

Show replies by date

Alain Kägi

5 Aug 5 Aug

2:31 p.m.

We're using seL4cp. I have written simple timer drivers for the Odroid-C2 and imx8mm platforms. Neither of these platforms is officially supported by seL4cp at this time. The former requires support for edge-triggered interrupts in seL4cp and the latter a more recent version of seL4. We have a combination of TFTPboot and Internet-enabled power switches to load and to run the binaries. Alain

Indan Zupancic

7 Aug 7 Aug

8:32 p.m.

Hello Sid, On 2023-08-05 02:47, Sid Agrawal wrote:

...

I have a rspi4 and a Toradex Colibri iMX8X module with the aster carrier board. This Toradex has the same SoC ( iMX8X) as the tqma8xqp-1gb mentioned on the sel4cp website. Do you folks have any thoughts on how much effort it is getting seL4 working on "Toradex Colibri iMX8X" given it is supported on "tqma8xqp-1gb" which has the same SoC? I do not mind buying a specific development board as long as I know that I can use it for a while :)

Not using sel4cp myself here, but have experience with tqma8xqp-1gb. I had a quick look at the Toradex website, but it seems Ethernet is not well supported: Only 100Mbit/s instead of 1 Gbit/s as supported by the SoC, because their carrier board uses KSZ8041 PHY. Other than minor tweaking of Ethernet initialisation settings, it should be easy to get Ethernet working on the Toradex. The only thing that is specific to the tqma8xqp-1gb board is what Ethernet PHY it uses, which UART is used for output and the amount of memory. Otherwise it's a plain imx8qxp platform with nothing board specific. That is, any imx8qxp board can just use the tqma8xqp-1gb platform with their own overlay DTS file to tweak what their board actually has. Maybe the UART code needs to be changed if the UART is hard-coded, but that's it. I don't know if sel4cp added more board specific code though. If peripherals are different the pinmux may be wrong for your board, so check that before using it.

...

For folks who are working on sel4cp, what kind of dev setup do you have? I am looking for basic conveniences like flashing the image via USB (so I do not have to add/remove an SD card), TFTPboot, and some simple device drivers. I did see the instructions on TFTPbootat [3]. However, does it matter if the image was built via the sel4test of sel4cp? I think not, but I just wanted to double-check.

No, instructions are the same I think.

...

And lastly, a higher-order question about seL4cp. How does sel4cp tie into the example in seL4_Libs [3], which has barebones libc and a VMM? Which is what I have used so far with sel4test. I understand that both sel4cp and camkes are for static systems, but I thought that I could use sel4cp to start some initial processes, such as a driver, a memory server, and some management processes. And later use process_spawn from seL4 libs to start additional PDs.

AFAIK sel4cp doesn't use anything of seL4_Libs and is independent. As you said it's made for static systems. If you want a dynamic system, you can build it on top of sel4cp as you noted. That said, you can create a static system with fixed amount of worker threads that do different things. So it depends on what you want to do whether you actually need a fully dynamic system or not. I highly recommend making the system as static as possible and have dynamic control of pre-existing PDs instead. Greetings, Indan

Ivan Velickovic

8 Aug 8 Aug

12:09 p.m.

Hi Sid, Just to add on to what the others have said. For booting an seL4CP image, tftpboot or other U-Boot methods will also work and we have been doing that internally at Trustworthy Systems. Just to note that some sel4test images are a different format compared to seL4CP images. All seL4CP images are raw binaries which means you need to use the `go` command with U-Boot. Some sel4test images are ELFs or other formats so other commands (e.g `bootelf`) are used. In general for getting another AArch64 board supported by seL4CP there should only be two files you need to change, `build_sdk.py` to add the board support/config to the SDK and `loader.c` needs a simple UART put char implementation so that it can output debug info/logging. Lastly, like Indan has said, seL4CP does not make use of the existing seL4_libs, util_libs, etc libraries. However, if you would like to run virtual machines on top of seL4CP, you may be interested in the VMM we have been building: https://github.com/Ivan-Velickovic/sel4cp_vmm. Note that it is still experimental and not quite ready for production use, however it should become more stable and production ready in the next couple of months. Ivan On 5/8/23 10:47, Sid Agrawal wrote:

...

Hi, I would like to setup a working example on sel4 with picoTCP and an eth driver. I came across this [1] from one of the seL4CP/sDDF demos and [2] from the camkes examples. However, I do not have access to those particular boards.

I have a rspi4 and a Toradex Colibri iMX8X module with the aster carrier board. This Toradex has the same SoC ( iMX8X) as the tqma8xqp-1gb mentioned on the sel4cp website. Do you folks have any thoughts on how much effort it is getting seL4 working on "Toradex Colibri iMX8X" given it is supported on "tqma8xqp-1gb" which has the same SoC? I do not mind buying a specific development board as long as I know that I can use it for a while :)

For folks who are working on sel4cp, what kind of dev setup do you have? I am looking for basic conveniences like flashing the image via USB (so I do not have to add/remove an SD card), TFTPboot, and some simple device drivers. I did see the instructions on TFTPbootat [3]. However, does it matter if the image was built via the sel4test of sel4cp? I think not, but I just wanted to double-check.

And lastly, a higher-order question about seL4cp. How does sel4cp tie into the example in seL4_Libs [3], which has barebones libc and a VMM? Which is what I have used so far with sel4test. I understand that both sel4cp and camkes are for static systems, but I thought that I could use sel4cp to start some initial processes, such as a driver, a memory server, and some management processes. And later use process_spawn from seL4 libs to start additional PDs.

Best, Sid

[1]https://github.com/lucypa/sDDF [2] https://github.com/seL4/global-components/tree/master/components/Ethdriver/i... [3]https://docs.sel4.systems/Hardware/GeneralARM _______________________________________________ Devel mailing list --devel@sel4.systems To unsubscribe send an email todevel-leave@sel4.systems

Sid Agrawal

1:20 p.m.

Thank you, Indan and Ivan. I have a few follow-up questions for @Ivan. 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 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? - 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 :) 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? Best, Sid On Mon, Aug 7, 2023 at 7:09 PM Ivan Velickovic wrote:

...

[*CAUTION:* Non-UBC Email]

Hi Sid, Just to add on to what the others have said. For booting an seL4CP image, tftpboot or other U-Boot methods will also work and we have been doing that internally at Trustworthy Systems. Just to note that some sel4test images are a different format compared to seL4CP images. All seL4CP images are raw binaries which means you need to use the `go` command with U-Boot. Some sel4test images are ELFs or other formats so other commands (e.g `bootelf` ) are used.

In general for getting another AArch64 board supported by seL4CP there should only be two files you need to change, `build_sdk.py` to add the board support/config to the SDK and `loader.c` needs a simple UART put char implementation so that it can output debug info/logging.

Lastly, like Indan has said, seL4CP does not make use of the existing seL4_libs, util_libs, etc libraries. However, if you would like to run virtual machines on top of seL4CP, you may be interested in the VMM we have been building: https://github.com/Ivan-Velickovic/sel4cp_vmm. Note that it is still experimental and not quite ready for production use, however it should become more stable and production ready in the next couple of months.

Ivan On 5/8/23 10:47, Sid Agrawal wrote:

Hi, I would like to setup a working example on sel4 with picoTCP and an eth driver. I came across this [1] from one of the seL4CP/sDDF demos and [2] from the camkes examples. However, I do not have access to those particular boards.

I have a rspi4 and a Toradex Colibri iMX8X module with the aster carrier board. This Toradex has the same SoC ( iMX8X) as the tqma8xqp-1gb mentioned on the sel4cp website. Do you folks have any thoughts on how much effort it is getting seL4 working on "Toradex Colibri iMX8X" given it is supported on "tqma8xqp-1gb" which has the same SoC? I do not mind buying a specific development board as long as I know that I can use it for a while :)

For folks who are working on sel4cp, what kind of dev setup do you have? I am looking for basic conveniences like flashing the image via USB (so I do not have to add/remove an SD card), TFTPboot, and some simple device drivers. I did see the instructions on TFTPbootat [3]. However, does it matter if the image was built via the sel4test of sel4cp? I think not, but I just wanted to double-check.

And lastly, a higher-order question about seL4cp. How does sel4cp tie into the example in seL4_Libs [3], which has barebones libc and a VMM? Which is what I have used so far with sel4test. I understand that both sel4cp and camkes are for static systems, but I thought that I could use sel4cp to start some initial processes, such as a driver, a memory server, and some management processes. And later use process_spawn from seL4 libs to start additional PDs.

Best, Sid

[1] https://github.com/lucypa/sDDF [2]https://github.com/seL4/global-components/tree/master/components/Ethdriver/i... [3] https://docs.sel4.systems/Hardware/GeneralARM _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

Ivan Velickovic

3:28 p.m.

1. seL4 needs to know certain aspects of the platform at compile time such as the start of main memory and how large it is. This information is extracted from the DTS by the seL4 build-system. The reason there are two DTS files is that one is from Linux and is just a general description of the hardware, the overlay is used for seL4 specific things. If you inspect the overlay of each platform you will see fields such as `seL4,kernel-devices` which describe which peripherals (e.g the interrupt controller) that are reserved by seL4 and not available to user-space. These seL4 specific fields/info are a lot easier to store in an overlay rather than modifying the very large original DTS from Linux. 2. The i.MX8 platforms and tqma8xqp1gb are based on the same SoC and so are fairly similar, but not the exact same. At Trustworthy Systems we are currently using the Odroid-C4 (I believe the sDDF echo server also works on Odroid-C4, but on a separate branch of the repo). The Odroid-C4 is quite readily available and much cheaper compared to the i.MX8MM-EVK. Any contribution would be very welcome! I'm on Mattermost (@ivanv) should you wish to talk directly. 3. That is correct. The DTS that is stored in sel4cp_vmm is directly from Linux source code (by de-compiling the DTB that Linux compiles for a given platform). Thanks Ivan On 8/8/23 13:20, Sid Agrawal wrote:

...

Thank you, Indan and Ivan. I have a few follow-up questions for @Ivan.

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

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? - 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 :)

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?

Best, Sid

On Mon, Aug 7, 2023 at 7:09 PM Ivan Velickovic wrote:

[*CAUTION:* Non-UBC Email]

Hi Sid,

Just to add on to what the others have said. For booting an seL4CP image, tftpboot or other U-Boot methods will also work and we have been doing that internally at Trustworthy Systems. Just to note that some sel4test images are a different format compared to seL4CP images. All seL4CP images are raw binaries which means you need to use the `go` command with U-Boot. Some sel4test images are ELFs or other formats so other commands (e.g `bootelf`) are used.

In general for getting another AArch64 board supported by seL4CP there should only be two files you need to change, `build_sdk.py` to add the board support/config to the SDK and `loader.c` needs a simple UART put char implementation so that it can output debug info/logging.

Lastly, like Indan has said, seL4CP does not make use of the existing seL4_libs, util_libs, etc libraries. However, if you would like to run virtual machines on top of seL4CP, you may be interested in the VMM we have been building: https://github.com/Ivan-Velickovic/sel4cp_vmm. Note that it is still experimental and not quite ready for production use, however it should become more stable and production ready in the next couple of months.

Ivan On 5/8/23 10:47, Sid Agrawal wrote:

...
Hi, I would like to setup a working example on sel4 with picoTCP and an eth driver. I came across this [1] from one of the seL4CP/sDDF demos and [2] from the camkes examples. However, I do not have access to those particular boards.

I have a rspi4 and a Toradex Colibri iMX8X module with the aster carrier board. This Toradex has the same SoC ( iMX8X) as the tqma8xqp-1gb mentioned on the sel4cp website. Do you folks have any thoughts on how much effort it is getting seL4 working on "Toradex Colibri iMX8X" given it is supported on "tqma8xqp-1gb" which has the same SoC? I do not mind buying a specific development board as long as I know that I can use it for a while :)

For folks who are working on sel4cp, what kind of dev setup do you have? I am looking for basic conveniences like flashing the image via USB (so I do not have to add/remove an SD card), TFTPboot, and some simple device drivers. I did see the instructions on TFTPbootat [3]. However, does it matter if the image was built via the sel4test of sel4cp? I think not, but I just wanted to double-check.

And lastly, a higher-order question about seL4cp. How does sel4cp tie into the example in seL4_Libs [3], which has barebones libc and a VMM? Which is what I have used so far with sel4test. I understand that both sel4cp and camkes are for static systems, but I thought that I could use sel4cp to start some initial processes, such as a driver, a memory server, and some management processes. And later use process_spawn from seL4 libs to start additional PDs.

Best, Sid

[1]https://github.com/lucypa/sDDF [2] https://github.com/seL4/global-components/tree/master/components/Ethdriver/i... [3]https://docs.sel4.systems/Hardware/GeneralARM _______________________________________________ Devel mailing list --devel@sel4.systems To unsubscribe send an email todevel-leave@sel4.systems

Ivan Velickovic

3:34 p.m.

Just a small correction, the DTS you see in seL4 (e.g tools/dts/tqma8xqp1gb.dts) is *typically* from Linux but that doesn't necessarily have to be the case. It could be from anywhere, it just needs to be a valid description of the hardware. On 8/8/23 15:28, Ivan Velickovic wrote:

...

1.

seL4 needs to know certain aspects of the platform at compile time such as the start of main memory and how large it is. This information is extracted from the DTS by the seL4 build-system. The reason there are two DTS files is that one is from Linux and is just a general description of the hardware, the overlay is used for seL4 specific things. If you inspect the overlay of each platform you will see fields such as `seL4,kernel-devices` which describe which peripherals (e.g the interrupt controller) that are reserved by seL4 and not available to user-space. These seL4 specific fields/info are a lot easier to store in an overlay rather than modifying the very large original DTS from Linux.

2.

The i.MX8 platforms and tqma8xqp1gb are based on the same SoC and so are fairly similar, but not the exact same. At Trustworthy Systems we are currently using the Odroid-C4 (I believe the sDDF echo server also works on Odroid-C4, but on a separate branch of the repo). The Odroid-C4 is quite readily available and much cheaper compared to the i.MX8MM-EVK.

Any contribution would be very welcome! I'm on Mattermost (@ivanv) should you wish to talk directly.

3.

That is correct. The DTS that is stored in sel4cp_vmm is directly from Linux source code (by de-compiling the DTB that Linux compiles for a given platform).

Thanks

Ivan

On 8/8/23 13:20, Sid Agrawal wrote:

...
Thank you, Indan and Ivan. I have a few follow-up questions for @Ivan.

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

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? - 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 :)

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?

Best, Sid

On Mon, Aug 7, 2023 at 7:09 PM Ivan Velickovic wrote:

    [*CAUTION:* Non-UBC Email]

    Hi Sid,

    Just to add on to what the others have said. For booting an seL4CP     image,     tftpboot or other U-Boot methods will also work and we have been     doing that     internally at Trustworthy Systems. Just to note that some sel4test     images are     a different format compared to seL4CP images. All seL4CP images     are raw     binaries which means you need to use the `go` command with U-Boot.     Some     sel4test images are ELFs or other formats so other commands (e.g     `bootelf`)     are used.

    In general for getting another AArch64 board supported by seL4CP     there should     only be two files you need to change, `build_sdk.py` to add the     board support/config     to the SDK and `loader.c` needs a simple UART put char     implementation so that     it can output debug info/logging.

    Lastly, like Indan has said, seL4CP does not make use of the     existing seL4_libs,     util_libs, etc libraries. However, if you would like to run     virtual machines on top     of seL4CP, you may be interested in the VMM we have been building:     https://github.com/Ivan-Velickovic/sel4cp_vmm. Note that it is     still experimental     and not quite ready for production use, however it should become     more stable     and production ready in the next couple of months.

    Ivan     On 5/8/23 10:47, Sid Agrawal wrote:

...
    Hi,     I would like to setup a working example on sel4 with picoTCP and an eth     driver. I came across this [1] from one of the seL4CP/sDDF demos and [2]     from the camkes examples. However, I do not have access to those particular     boards.

    I have a rspi4 and a Toradex Colibri iMX8X module with the aster carrier     board. This Toradex has the same SoC ( iMX8X) as the tqma8xqp-1gb mentioned     on the sel4cp website. Do you folks have any thoughts on how much effort it     is getting seL4 working on "Toradex Colibri iMX8X" given it is supported on     "tqma8xqp-1gb" which has the same SoC? I do not mind buying a     specific development board as long as I know that I can use it for a while     :)

    For folks who are working on sel4cp, what kind of dev setup do you have? I     am looking for basic conveniences like flashing the image via USB (so I do     not have to add/remove an SD card), TFTPboot, and some simple device     drivers. I did see the instructions on TFTPbootat [3]. However, does it     matter if the image was built via the sel4test of sel4cp? I think not, but     I just wanted to double-check.

    And lastly, a higher-order question about seL4cp. How does sel4cp tie into     the example in seL4_Libs [3], which has barebones libc and a VMM? Which is     what I have used so far with sel4test. I understand that both sel4cp and     camkes are for static systems, but I thought that I could use sel4cp to     start some initial processes, such as a driver, a memory server, and some     management processes. And later use process_spawn from seL4 libs to start     additional PDs.

    Best,     Sid

    [1]https://github.com/lucypa/sDDF     [2] https://github.com/seL4/global-components/tree/master/components/Ethdriver/i...     [3]https://docs.sel4.systems/Hardware/GeneralARM     _______________________________________________     Devel mailing list --devel@sel4.systems     To unsubscribe send an email todevel-leave@sel4.systems

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

Indan Zupancic

6:47 p.m.

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

Sid Agrawal

9 Aug 9 Aug

1:28 a.m.

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,

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

Sid Agrawal

12 Aug 12 Aug

12:18 p.m.

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,

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

Ivan Velickovic

14 Aug 14 Aug

9:58 a.m.

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

494

Age (days ago)

502

Last active (days ago)

List overview

Download

10 comments

4 participants

participants (4)

Alain Kägi
Indan Zupancic
Ivan Velickovic
Sid Agrawal

sel4cp and networking driver

tags

participants (4)