Support Microkit HW CI#459
Conversation
midnightveil
force-pushed
the
julia/microkit-support
branch
from
e20117b to
7f2b947
Compare
midnightveil
force-pushed
the
julia/microkit-support
branch
2 times, most recently
from
f8ede65 to
4ecdd10
Compare
midnightveil
force-pushed
the
julia/microkit-support
branch
2 times, most recently
from
00a574c to
275eb17
Compare
Yes, that would definitely make sense. |
| # microkit hw build/test only | ||
| no_hw_build: true | ||
| no_hw_test: true | ||
|
|
There was a problem hiding this comment.
I don't remember, was there a reason we're not testing serengti with plain sel4test as well?
There was a problem hiding this comment.
Right now Serengeti is actually the exact same platform as Cheshire. I merged the Microkit support because I thought there might be changes to Serengeti that would make running Cheshire images on Serengeti incompatible but right now there aren't any. Perhaps we should not have Serengeti as an explicit platform in Microkit, it's a bit of a premature generalisation right now.
There was a problem hiding this comment.
(There would be a difference in the sense that for Serengeti it would be possible to setup the sel4_libs timer: as serengeti has a timer peripheral where Cheshire does not.)
There was a problem hiding this comment.
That's true, I should clarify from seL4's perspective there's no difference to my knowledge (memory layout, UART, SoC support etc).
| platform: imx8mp-iotgate | ||
| req: [iotgate1, iotgate3, iotgate4, iotgate5] | ||
| march: armv8a | ||
| # microkit only, no seL4 |
There was a problem hiding this comment.
Should we at least build a sel4test image? I'm uncomfortable with having boards that are not officially supported on seL4 but then supported in microkit. We should try to eliminate those cases, ideally by having full support on the seL4 side.
There was a problem hiding this comment.
Similar to the Kria, this platform is the same as the imx8mp-evk which seL4 has explicit support for but with a slightly different memory layout so we have a custom DTS overlay in Microkit that gets applied.
| # not in seL4 tooling | ||
| no_hw_build: true |
There was a problem hiding this comment.
I don't understand how it is possible to have a microkit build for the board when there is no seL4 tooling for it. Are there things missing for sel4test?
There was a problem hiding this comment.
The Kria26 is just the ZCU102 with a different memory layout and default UART address, so everything in the kernel side is already supported, and a DTS overlay is used in Microkit to adjust those two things.
There was a problem hiding this comment.
It would be possible to add these to the seL4 tests. Just at tbe cost of evem more things to build and test. But maybe that's fine and should be done, IDK.
lsf37
left a comment
lsf37
left a comment
There was a problem hiding this comment.
This looks very reasonable overall, only some missing README/comments.
I have questions about the sel4test/microkit support mismatch, but we can merge this and figure that part out later.
I made a comment for each one but the answer to all of them is basically that seL4 doesn't want to have explicit support for every single minor variation of a particular SoC (e.g slightly different memory layout or UART address). However, since seL4 still needs to know all this information at build time, and since we have to have a pre-built kernel it means we have to add explicit boards for each variation in Microkit for now (hence the Kria26 and imx8mp-iotgate support). |
- Support custom env filters - Give the `Platform` class 'microkit_boards' for the microkit board name mappings, as well as 'microkit_hw_build' and 'microkit_hw_test' to control HW build/test separately from the sel4test users. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
midnightveil
force-pushed
the
julia/microkit-support
branch
from
275eb17 to
7a0e825
Compare
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
midnightveil
force-pushed
the
julia/microkit-support
branch
from
7a0e825 to
6c9e208
Compare
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
midnightveil
force-pushed
the
julia/microkit-support
branch
from
e5b5ac1 to
e43d2c0
Compare
Ok, thanks for explaining, that all makes sense. The main thing to decide then is if the trivial differences are worth checking in sel4test, which is mainly a matter of build time (and possibly board availability). We can think about that separately from this PR, though, i.e. no reason to hold up anything here. |
| The tests can be restricted to specific `board`, `config`, and `march` configurations, | ||
| which we use to create a GitHub actions runner matrix. | ||
|
|
||
| The test expects pre-build images produced by the [microkit-hw-build] action, |
There was a problem hiding this comment.
| The test expects pre-build images produced by the [microkit-hw-build] action, | |
| The test expects pre-built images produced by the [microkit-hw-build] action, |
| / platforms from the Microkit SDK build system directly. This is the `TEST_CASES` | ||
| variable that expects a JSON file used in both [microkit-hw-build] and here. | ||
|
|
||
| These action knows how to build an example from the Microkit SDK, which is |
There was a problem hiding this comment.
| These action knows how to build an example from the Microkit SDK, which is | |
| This action knows how to build an example from the Microkit SDK, which is |
| also notably pre-built outside of the ci-actions action scripts; instead these | ||
| scripts simply built the examples for each platform to run. |
There was a problem hiding this comment.
In this sentence I'm getting confused what "these scripts" refers to. The scripts in ci-actions or scripts in microkit? The scripts in ci-actions just invoke make inside the microkit repo, right?
lsf37
left a comment
lsf37
left a comment
There was a problem hiding this comment.
Thanks for adding the docs. A few very minor queries, happy for you to address/answer them and then merge directly.
3 participants
Should be merged before seL4/microkit#475.
The 'test' here is rather simple for the moment: it simply runs the 'Hello, World!' example (which works only in debug) and checks the output matches. The goal is to eventually improve this, but it at least tests that the debug boot flow works; which is better than nothing.
Ivan(Ivan is leaving) up as codeowners for this folder?