Upgrade CBMC proof tools: starter kit and Litani 1.10.0 #722
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 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
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).
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.
feliperodri
approved these changes
Jul 12, 2021
alex-chew
pushed a commit
to alex-chew/aws-encryption-sdk-c
that referenced
this pull request
Oct 20, 2021
* 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.
alex-chew
added a commit
that referenced
this pull request
Oct 20, 2021
#731) * Add CBMC CI configuration (#709) This commit adds a configuration file for the "CBMC Proofs" CI check. This is in preparation for adding some custom check-out steps later. * Use private submodules before CI run (#711) * chore: Use continuous-integration environment for private submodule access (#714) Co-authored-by: Robin Salkeld <salkeldr@amazon.com> * chore: Add support policy (#720) * Upgrade CBMC proof tools: starter kit and Litani 1.10.0 (#722) * 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. * fix: Simplify / update build instructions. (#713) Co-authored-by: June Blender <juneb@users.noreply.github.com> Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com> * fix(proof_timeout): mark high-memory proofs expensive (#710) * Removed OOM test, as OOM is no longer possible from aws allocators (#728) * chore: pin newer aws-sdk-cpp in macOS CI builds (#729) * chore: update version number and changelog for v1.9.1 * chore: update CBMC CI submodules Co-authored-by: Kareem Khazem <karkhaz@amazon.com> Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Ben Farley <47006790+farleyb-amazon@users.noreply.github.com> Co-authored-by: lizroth <30636882+lizroth@users.noreply.github.com> Co-authored-by: June Blender <juneb@users.noreply.github.com> Co-authored-by: Justin Boswell <boswej@amazon.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.
This PR updates the proof tools to the latest version. This brings the following improvements:
Profiling
coverage checking jobs
proof
running over the whole run, making it easy to choose a CI machine
with enough parallelism
Litani runs expensive proofs serially, ensuring that they do not
over-consume resources like RAM.
UI improvements
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.
Check any applicable: