chore: backport maintenance/doc changes and prepare release for v1.9.1 #731
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This commit adds a configuration file for the "CBMC Proofs" CI check. This is in preparation for adding some custom check-out steps later.
…ccess (aws#714) Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
* Upgrade proof tool submodules
This commit advances Litani to release 1.10.0, and the starter kit to
the tip-of-tree. This brings the following improvements:
- Profiling
- Litani measures the memory usage of the CBMC safety checking and
coverage checking jobs
- The dashboard includes box-and-whisker diagrams for memory use per
proof
- The dashboard includes a graph of how many parallel jobs are
running over the whole run, making it easy to choose a CI machine
with enough parallelism
- It is now possible to designate particular proofs as "EXPENSIVE";
Litani runs expensive proofs serially, ensuring that they do not
over-consume resources like RAM.
- UI improvements
- Each pipeline page includes a table of contents
- Each pipeline page includes a dependency graph of the pipeline
- Each job on the pipeline page has a hyperlink to that job
- The terminal output is now less noisy
* Change cbmc-batch.yaml to cbmc-proof.txt
This makes the proof layout consistent with the starter kit, which will
allow us to use a generic run script in a future commit. Putting this
in commit by itself because the diff is huge and not worth reading (just
moving some files and changing two lines in the runscript).
* Symlink run-cbmc-proofs.py to starter kit
The run script is now a symbolic link into the starter kit submodule,
meaning that it will be updated whenever the starter kit is. This is
done iso that E-SDK doesn't carry custom modifications to the run script
unless necessary; previous commits have made the E-SDK proofs consistent
with the generic starter kit conventions.
Co-authored-by: June Blender <juneb@users.noreply.github.com> Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.
Check any applicable: