-
Notifications
You must be signed in to change notification settings - Fork 64
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
[litmus] Add support for speedcheck parameter for -mode presi #869
Conversation
Hey @maranget, indeed I missed this. I tried to avoid other deadlocks, but I missed this. I had a look at your patch and I think it's a much better way to achieve what I was trying to. Do you want to open a new PR with your own patch or should I cherry pick it in this pull request? |
Hi @relokin, cherry picking looks like the most adequate technique. Your opinion? |
4f3b2fa
to
0b45377
Compare
Just to check with you that my understanding is correct. The high level desire was to exit litmus7 as soon as there is an execution where the post-condition is satisfied. With this PR, if a specific execution satisfies the post-condition, then other instances will continue for a little longer. For example, let's say we execute 2 instances of MP using 4 cores. The 1st instance observes an execution which satisfies the post-condition and exits immediately. The 2nd instance will continue executing until the end of the for loop (executing in total size iterations), or until it encounters itself an execution which satisfies the post-condition). However, at the end of the execution, we know that at least for one instance its last execution satisfied the post-condition. And in the case of presi, we know that at least for at least a set of cores (2 in the case of MP), the last time they executed the test, it satisfied the post-condition. Does that make sense? |
Hi @relokin, we agree on the high-level desire. If I am not mistaken, this is what the synchronisation code of commit 0b45377 does. That is all instance will exit as soon as possible if one instance discovers that the post-condition is satisfied. Every test thread executes As soon as one of the instance discovers that the post-condition is satisfied, it sets the global flag I am not sure the scheme above is dead-lock free. It looks important that all the threads of a given instance act consistently. Hence the idea of them synchronising before reading the instance level flag. |
A simpler scheme that would not stop threads as soon as the previous one, but that would spare the instance level synchronisation, would be as follows: the In |
Thanks @maranget! The motivation for this change (and I am aware that this might not be the same for |
Hi @relokin. I guess we agree to merge this PR as it is, or do you see additional improvements? |
If we agree on merging, would you please rebase on master? |
This change adds support for the speedcheck parameter for -mode presi. This was already supported in -mode std. The user can provide the parameter "+sc" which will force the exit to as soon as the post-condition is observed. So as to avoid deadlocks, introduce a 2 level procedure to stop the experiment. Any instance that reaches the stop condition sets the global `stop_now` flag. This global flag is copied into an instance specific `stop_now` flag after each test by the thread number zero of this instance. Then, the instance threads synchronise on an instance level barrier before reading the instance flag and interrupting the test loop, if the flag is set. After returning from the test loop, _all_ threads synchronise on a global barrier, before reading the global flag and interrupting the experiment if the flag is set.
0b45377
to
de79e25
Compare
I am happy for this to be merged. Thanks @maranget! |
Merged, thanks @relokin |
This change adds support for the speedcheck parameter for -mode presi. This was already supported in -mode std. The user can provide the parameter "+sc" which will force the exit to as soon as the post-condition is observed.