Fix long interleaving times #55
Merged
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.
Investigating long running times where the following Thread test took long to the point of suspecting a deadlock/infinite loop (or a bug in the run-time):
Because of other recent fixes enhancing reproducability, I was able to pin-point the following
cmdtriple:with a 15 and 13 element
cmd listrunning in parallel and needing interleaving.Depending on the scheduling, 50 repetitions of the above would take between 1min39sec and 15min to run - with most computation time being spent in the interleaving search. Since the interleaving is costly (exponential in input length I believe) we therefore reduce the input
cmd listsize. This brings the interleaving search time significantly down (to around 1min, worst case).While we are at it, we similarly adjust STM's
par_lento at most 12.