l4v icon indicating copy to clipboard operation
l4v copied to clipboard

add CI for different `numDomains` settings

Open lsf37 opened this issue 3 years ago • 5 comments

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.

lsf37 avatar Dec 21 '21 05:12 lsf37

We already test 16 as it is the default. Did you mean another number?

Xaphiosis avatar Dec 21 '21 05:12 Xaphiosis

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.

lsf37 avatar Dec 21 '21 05:12 lsf37

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

Xaphiosis avatar Dec 21 '21 05:12 Xaphiosis

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.

lsf37 avatar Dec 21 '21 05:12 lsf37

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.

Xaphiosis avatar Dec 21 '21 06:12 Xaphiosis

This has been implemented in https://github.com/seL4/l4v/pull/701 and related PRs.

lsf37 avatar Feb 10 '24 07:02 lsf37