Allow parallel update_suite run with -m/-i/-w #1884
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.
While testing the
Marshal-related parts of #1880 (-m and -i), I was annoyed that the tests run so slow. And that's not because they're inherently so slow (just double the Goblint runs), but because update_suite falls back to sequential run for any of these modes with multiple Goblint runs.The reason parallel runs were forbidden is to avoid mixing up the intermediate files between the two runs when everything is happening in parallel:
run/for -m,incremental_data/for -i andwitness.ymlfor -w.We have options to configure each of those names, so this PR makes update_suite use unique per-test names to avoid conflicts and thus allow parallel runs.
This was already done for
.goblint/where preprocessing output goes anyway.