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