l4v
l4v copied to clipboard
add CI for different `numDomains` settings
When PR #410 is merged, the proofs will be generic in the number of protection domains.
Testing that fact with every CI job is going to be too resource-intensive, but we should test at least values of 1
, 2
, and something like 16
in the weekly job so we get an alert when we accidentally break this genericity.
We already test 16 as it is the default. Did you mean another number?
I mostly meant the weekly should also keep testing the normal default. Not sure if we want to leave it at 16
, but 16
is as good as any I guess.
Then you propose adding 1
and 2
to the weekly test? That makes sense.
Other thoughts:
- we need a branch with a commit that changes all the verified seL4 configs that keeps getting rebased before we test (we already discussed that)
- when someone adds a new config, the above commit will not change the new config, and I have not a clue how one would track or notice that; an alternative to the above method is to take master and search+replace the number of domains in all configs
Then you propose adding 1 and 2 to the weekly test? That makes sense.
yes, that would have been much clearer :-)
- we need a branch with a commit that changes all the verified seL4 configs that keeps getting rebased before we test (we already discussed that)
Ah, I had the branch discussion put under "for different platform", not for different config. For changing the config in only the number of domains, I'd propose for the CI job to edit the *_verified.config
files (via regexp) before it starts the test. That should be pretty targeted and test the entire chain.
Search+replace via regexp sounds like a good plan and will catch other arches should they appear. Yes, you're right, I'm conflating discussions. You proposed the floating commit for a platform port. My bad.
This has been implemented in https://github.com/seL4/l4v/pull/701 and related PRs.