-
Notifications
You must be signed in to change notification settings - Fork 275
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
Several primus fixes #841
Merged
Merged
Several primus fixes #841
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
previously we were leaving a function after the first block (and all other operations attached to the function leaving event were performed after the entry block)
The kill operation is a hard beast, as it is very hard to suicide, i.e., to kill the current machine. It is also hard to routinely kill other machines in the scheduler, as usually during the rescheduling we are in the context of a machine that we would like to kill, and switching to another machine will take control from us. Previous implementation of kill was just wrong, it was killing the state without switching the continuations. In case of the self-killing it basically was switching the state while leaving the machine in the same continuation. The proposed implementation, delays the machine killing if it is the current machine, and performs it on a next fork. Note, an easier to use (and to implement) primitive, would be [die x] that will kill the current machine and tranfer the control to the machine [x]. However, we can't add new primitives to the Primus Machine interface without bumping the version. So let's keep it for the future Primus 2.0
sorry for putting it here, just don't want to create a separate PR for such a minor stuff
Previously, we were waiting until the end and didn't kill any machines. The proposed code will kill finished machines in the greedy scheduler. This saves tons of gigabytes of memory.
The progress report will show the percentage of visited basic blocks, basically the code coverage. Also, previously marker was broken as it was marking all terms.
memory corruption check was verifying that a freed pointer was allocated. In real life it has an incredible amount of false positives.
also extends it a bit.
in general it is very useful to see where the backtrace changes the machine id, in case of the greedy scheduler and promiscuous mode those are exactly the points where infeasibility could be introduced.
When all-subroutines are selected, then we're running them in the topological order, starting with those functions that are marked as entry points (usually the _start function in case of an executable). Also added an option to run each machine in isolation (i.e., in a separate computation), might be useful for someone.
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 brings several very significant bug fixes to Primus. Most importantly it fixes machine killing function, so that we can now kill finished machines, that significantly reduces the memory footprint.