[seL4] Re: sel4cp and networking driver

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