Skip to content

Update SV-COMP performance testing tool to 2020/2021 #6117

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 19, 2021

Conversation

tautschnig
Copy link
Collaborator

  • Use EC2 instead of CodeBuild to avoid Docker throttling.
  • Use a VPC for compatibility with current EC2 spot offerings.
  • Add profiling using Linux perf as gprof doesn't seem to be working
    anymore.
  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented May 14, 2021

Codecov Report

Merging #6117 (6831ffe) into develop (f564088) will decrease coverage by 0.08%.
The diff coverage is 82.38%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6117      +/-   ##
===========================================
- Coverage    75.53%   75.45%   -0.09%     
===========================================
  Files         1447     1447              
  Lines       158116   158093      -23     
===========================================
- Hits        119431   119282     -149     
- Misses       38685    38811     +126     
Impacted Files Coverage Δ
src/goto-instrument/accelerate/accelerate.cpp 34.89% <0.00%> (ø)
src/goto-instrument/concurrency.cpp 0.00% <0.00%> (ø)
src/goto-instrument/nondet_volatile.cpp 86.55% <ø> (-0.15%) ⬇️
src/goto-instrument/replace_calls.cpp 89.55% <0.00%> (+1.31%) ⬆️
src/goto-programs/goto_convert_class.h 87.30% <ø> (ø)
src/goto-programs/goto_convert.cpp 91.69% <33.33%> (-0.24%) ⬇️
src/util/simplify_expr_struct.cpp 74.38% <50.00%> (+0.78%) ⬆️
src/goto-instrument/goto_program2code.cpp 69.20% <60.00%> (+0.06%) ⬆️
src/util/simplify_expr.cpp 78.14% <65.00%> (-6.93%) ⬇️
src/goto-programs/goto_program.h 90.71% <66.66%> (-0.93%) ⬇️
... and 72 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 0ea7f13...6831ffe. Read the comment docs.

@tautschnig tautschnig force-pushed the sv-comp-scripting branch from 1387843 to dc56844 Compare May 14, 2021 16:29
- Use EC2 instead of CodeBuild to avoid Docker throttling.
- Use a VPC for compatibility with current EC2 spot offerings.
- Use capacity-optimized as spot allocation strategy.
- Add profiling using Linux perf as gprof doesn't seem to be working
anymore.
@tautschnig tautschnig force-pushed the sv-comp-scripting branch from dc56844 to 6831ffe Compare May 15, 2021 21:19
@kroening kroening merged commit dc12603 into diffblue:develop May 19, 2021
@tautschnig tautschnig deleted the sv-comp-scripting branch May 19, 2021 11:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants