zynqmp: add 2018.3 linux images

[chrisguikema]

This commit adds 2018.3 Linux artifacts that are compatible with the seL4 kernel device tree. It also links them as "defaults".

[lsf37]

I don't see any problems with adding the image as such, but can you explain why it is necessary?

[axel-h]

Are you planning to add PetaLinux 2022_1 then also?

[chrisguikema]

can you explain why it is necessary?

Sure! Xilinx releases quarterly updates for the Petalinux images, and with those changes come minor device tree dependencies. So using a 2018.3 device tree with the 2021.1 kernel may have unintended consequences. The ZCU102 is the platform that DornerWorks gets requested to use the most, so we have an interest in making these toolchain updates work as seamlessly as possible.

Internally, we update the seL4 device tree to just use the newest version of Petalinux that we support. When I tried to update the seL4 device tree in a PR, there was some kickback that since seL4 doesn't care about dependencies, and only cares about memory regions / interrupts for untyped object creation, updating the seL4 kernel device tree doesn't really make a lot of sense. Luckily, the dtb_base_name in the VMM can use a custom dtb instead of the kernel dtb, so we can bypass the issue and support newer versions as needed.

With all that being said, anyone who tries to use the camkes-vm for the ZCU102 out of the box probably doesn't care too much about Petalinux releases, if we're being honest. For device tree generation in the VMM, the seL4 kernel device tree is used by default. Using this device tree with newer Petalinux images may not work as intended. However, it will work with older Petalinux versions.

This solution is basically adding Petalinux 2018.3 as a default, as the artifacts are compatible with seL4 without any axi/amba changes. It also easily allows for newer Petalinux releases to be supported as well, as soon as we get around to testing them :)

I think what I'll do is make a PR for the vm_minimal ZCU102 example, and add a devices.camkes for each supported Petalinux version. That way, anyone who pulls this down and tests can select their supported version. Additionally, it becomes easy to add CI tests to ensure each version builds as expected.

Are you planning to add PetaLinux 2022_1 then also?

I think we have that version supported internally. I'll double check first, but I'd like to have that version supported as well.

[axel-h]

When I tried to update the seL4 device tree in a PR, there was some kickback that since seL4 doesn't care about dependencies

I think this was in seL4/seL4#1102

[axel-h]

Seems fine to me.

The situation with the device tree usage from the kernel is a bit of a pitfall that might be worth looking into one day. Especially when some node names and paths change, it might be a reason to update the file in the kernel also (even if this does not affect the kernel directly), just be stay aligned with the rest of the world. Or we should consider stripping the kernel devices trees down to just what is used, so it is harder to use them for anything else...

[lsf37]

Seems fine to me.

The situation with the device tree usage from the kernel is a bit of a pitfall that might be worth looking into one day. Especially when some node names and paths change, it might be a reason to update the file in the kernel also (even if this does not affect the kernel directly), just be stay aligned with the rest of the world. Or we should consider stripping the kernel devices trees down to just what is used, so it is harder to use them for anything else...

Stripping the device tree to just the info the kernel needs might be useful, at least if that can be done reliably and automatically. Then it would be invariant under all those changes and it would be clearer what bits the kernel is sensitive to. Not sure. That should be a separate discussion, maybe on an issue in the kernel repo.

[Ivan-Velickovic]

Stripping the device tree to just the info the kernel needs might be useful, at least if that can be done reliably and automatically. Then it would be invariant under all those changes and it would be clearer what bits the kernel is sensitive to. Not sure. That should be a separate discussion, maybe on an issue in the kernel repo.

There has been some discussion here seL4/seL4#1036.