Skip to content
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

Heapster translation perf improvements #1513

Merged
merged 12 commits into from
Nov 16, 2021

Conversation

eddywestbrook
Copy link
Contributor

This PR replaces a number of uses of fmap and mbMap2 in the Heapster-to-SAW translation with calls to mbMapCl, in an attempt to reduce the number of times name-bindings are converted between fresh function and fresh pair representations. It also added the command heapster_set_translation_checks to turn off the translation-time assertPermStack* and assertTopPermM checks used during translation.

Eddy Westbrook added 3 commits November 15, 2021 10:56
…nslation-time assertPermStack* and assertTopPermM checks used during translation
…reduce the number of times name-bindings are converted between fresh function and fresh pair representations
@eddywestbrook
Copy link
Contributor Author

Whoops, I forgot a piece of this PR: the translation of the Impl1_Catch rule has also been changed so that, if the first branch succeeds, the second one is not even run.

Copy link
Contributor

@m-yac m-yac left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me! I did have one nitpick but I don't think it addressing it is worth waiting for the CI to re-run.

heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs Outdated Show resolved Hide resolved
Eddy Westbrook added 2 commits November 16, 2021 11:07
@eddywestbrook eddywestbrook added PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: heapster Issues specifically related to memory verification using Heapster labels Nov 16, 2021
@mergify mergify bot merged commit 608c65e into master Nov 16, 2021
@mergify mergify bot deleted the heapster/translation-perf-improvements branch November 16, 2021 22:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants