fix CI for SimplExportAndRefine on MCS #497
Comments
|
@mbrcknl do you have time to look into this, or should I have a go later this week? We're currently not deploying any more to the verification manifest, so we should not leave it too long. |
|
I'll take a look now. |
|
@lsf37 Thinking about how to do this... Do you think it would be worth pulling the Taking it out would make things more complicated, since I'd still need separate workflows for the MCS export and decompilation to stay within the 6 hour budget. But it would limit the damage if something like this comes up again. I think the way I would do it would be to add a new workflow (say binary-mcs.yml) which only runs on commits to At this stage, I probably wouldn't want to add it to the proof.yml workflow, since I wouldn't want it to run on every PR. Would that make sense? |
This removes the mcs-export matrix job from the proof-deploy workflow, as the first step towards solving #497. This should unblock verification manifest deployments. The mcs-export job was added to the proof-deploy workflow to perform SimplExportAndRefine for binary verification targets. It took a short cut, using the master branch of l4v to perform SimplExportAndRefine for MCS configurations. This no longer works, because MCS seL4 C code now contains C parser annotations that use symbols only available in the rt branch of l4v. We intend to add an equivalent job that uses the rt branch, but are still working out the best way to do that.
This removes the mcs-export matrix job from the proof-deploy workflow, as the first step towards solving #497. This should unblock verification manifest deployments. The mcs-export job was added to the proof-deploy workflow to perform SimplExportAndRefine for binary verification targets. It took a short cut, using the master branch of l4v to perform SimplExportAndRefine for MCS configurations. This no longer works, because MCS seL4 C code now contains C parser annotations that use symbols only available in the rt branch of l4v. We intend to add an equivalent job that uses the rt branch, but are still working out the best way to do that.
This removes the mcs-export matrix job from the proof-deploy workflow, as the first step towards solving #497. This should unblock verification manifest deployments. The mcs-export job was added to the proof-deploy workflow to perform SimplExportAndRefine for binary verification targets. It took a short cut, using the master branch of l4v to perform SimplExportAndRefine for MCS configurations. This no longer works, because MCS seL4 C code now contains C parser annotations that use symbols only available in the rt branch of l4v. We intend to add an equivalent job that uses the rt branch, but are still working out the best way to do that. Signed-off-by: Matthew Brecknell <matt@kry10.com>
This removes the mcs-export matrix job from the proof-deploy workflow, as the first step towards solving #497. This should unblock verification manifest deployments. The mcs-export job was added to the proof-deploy workflow to perform SimplExportAndRefine for binary verification targets. It took a short cut, using the master branch of l4v to perform SimplExportAndRefine for MCS configurations, since there were no differences between rt and master that were relevant to SimplExportAndRefine. This no longer the case, because MCS seL4 C code now contains C parser annotations that use symbols only available in the rt branch of l4v. We intend to add an equivalent job that uses the rt branch of l4v for MCS SimplExportAndRefine, but are still working out the best way to do that. Signed-off-by: Matthew Brecknell <matt@kry10.com>
This removes the mcs-export matrix job from the proof-deploy workflow, as the first step towards solving #497. This should unblock verification manifest deployments. The mcs-export job was added to the proof-deploy workflow to perform SimplExportAndRefine for binary verification targets. It took a short cut, using the master branch of l4v to perform SimplExportAndRefine for MCS configurations, since there were no differences between rt and master that were relevant to SimplExportAndRefine. This is no longer the case, because MCS seL4 C code now contains C parser annotations that use symbols only available in the rt branch of l4v. We intend to add an equivalent job that uses the rt branch of l4v for MCS SimplExportAndRefine, but are still working out the best way to do that. Signed-off-by: Matthew Brecknell <matt@kry10.com>
|
Yes, that sounds eminently reasonable. |
This removes the mcs-export matrix job from the proof-deploy workflow, as the first step towards solving #497. This should unblock verification manifest deployments. The mcs-export job was added to the proof-deploy workflow to perform SimplExportAndRefine for binary verification targets. It took a short cut, using the master branch of l4v to perform SimplExportAndRefine for MCS configurations, since there were no differences between rt and master that were relevant to SimplExportAndRefine. This is no longer the case, because MCS seL4 C code now contains C parser annotations that use symbols only available in the rt branch of l4v. We intend to add an equivalent job that uses the rt branch of l4v for MCS SimplExportAndRefine, but are still working out the best way to do that. Signed-off-by: Matthew Brecknell <matt@kry10.com>
|
@lsf37 Thinking about this some more... IIUC, proof-deploy runs if there's a push to l4v master, or a manual bump of the devel.xml manifest. That's useful for BV, since it roughly corresponds to the cases BV should check for non-MCS. But currently, the preprocess test only checks non-MCS configurations. So a manual bump is only needed when there is a change to the non-MCS parts of seL4 C code. Changes that only touch MCS parts will be automatically deployed to the default manifest. Do I read that right? Now that you're starting to work on the C proofs for MCS, would this be a good time to make the preprocess-deploy workflow fail on seL4 changes that only touch MCS? I.e. require a manual bump in those cases? I notice that the seL4 PR checks already do this. With stronger preprocess checks, the MCS export for BV could be usefully triggered on the Later, when MCS CRefine is done, there'll be the problem that we only want proof-deploy to push a new default manifest if both the MCS and non-MCS proofs pass. At that point, I guess proof-deploy would need to deal with both rt and master branches of l4v in a single workflow. But since we're not there yet, it probably makes sense to have a separate MCS export workflow for now. I made a PR for the preprocess-deploy workflow: seL4/seL4#876. Though, I'm happy to drop it if you don't think we're ready for it yet. |
This adds adds an mcs-export workflow, as a further step towards solving issue #497. This replaces the mcs-export matrix job that was removed from the proof-deploy workflow in #498. This workflow has some similarities to the proof-deploy workflow: - Both workflows check out a manifest, run some proofs, and trigger a binary verification workflow. - Both workflows are triggered by an update to an l4v branch. - Both workflows can be triggered by manual updates to the development verification-manifest, but not automatic updates due to a successful preprocess test. The differences are: - proof-deploy updates the default verification-manifest, whereas the mcs-export workflow does not. - proof-deploy uses l4v master, whereas mcs-export uses the rt branch. When MCS CRefine proofs are sufficiently advanced, the proof-deploy workflow will need to be updated to check MCS proofs before updating the default verification-manifest. At that point, this workflow could be reintegrated into the proof-deploy workflow. Signed-off-by: Matthew Brecknell <matt@kry10.com>
|
Hm, it's a bit more complicated than that. The current auto-deployments are:
Changes that are MCS relevant don't make sense to record in We do test for MCS changes on pull requests, so we do know that stuff will break if merged. To do this properly, we should set up auto-deployment to Edit: we might need an additional |
Right you are. I didn't actually look at the seL4-pp script, and just assumed it updated both Is it a deliberate choice to avoid cpp-compatible updates to default.xml? What's the rationale? (Not that it matters for this issue.)
I did understand those two parts, though.
Right, I guess I'd been looking at the
Yep, I saw that.
Yes, the main reason I wanted to get an MCS-compatible checkout from I'll think about this some more... |
And now I see that my thinking here doesn't make sense. Or at least, it only made sense as long as the MCS proofs and C code were not formally connected, which is no longer the case. So yes, you're entirely correct. I'll have a go at implementing cpp-compatible updates for |
IIRC the original design was that any push to If we wanted to change it, it'd be just this one line here in the verification manifest trigger workflow that would need to be removed. Alternatively we could update |
This removes the mcs-export matrix job from the proof-deploy workflow, as the first step towards solving #497. This should unblock verification manifest deployments. The mcs-export job was added to the proof-deploy workflow to perform SimplExportAndRefine for binary verification targets. It took a short cut, using the master branch of l4v to perform SimplExportAndRefine for MCS configurations, since there were no differences between rt and master that were relevant to SimplExportAndRefine. This is no longer the case, because MCS seL4 C code now contains C parser annotations that use symbols only available in the rt branch of l4v. We intend to add an equivalent job that uses the rt branch of l4v for MCS SimplExportAndRefine, but are still working out the best way to do that. Signed-off-by: Matthew Brecknell <matt@kry10.com>
|
I think we may actually soon approaching a state where the your original idea might be right, where the l4v |
We're currently attempting to build
SimplExportAndRefineandCKernelfor the MCS config of seL4 from the master branch of l4v. This was convenient because it kept the CI workflow simple.It also used to work fine, but now breaks since we have added annotations to the C code that need concepts only available on the
rtbranch.This is issue for fixing the CI test so proof updates are deployed again to the manifest. An intermediate step could be to just disable this step. Longer term, we want to switch l4v to the
rtbranch. This might be as simple as supplying a branch argument to the test, but I'm sure complications will arise as they always do.The text was updated successfully, but these errors were encountered: