Add support for progress models #731
Merged
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
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
…ntics of CBs + progress are still unclear). - Added minimal progress guarantees (some thread is always scheduled)
# Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java # dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java
|
@hernan-poncedeleon Also, there are issues with the processing pipeline. Those tests require at least loop normalization (and some even more like branch reordering?). Shall we fix this issue in this PR? |
I would keep the expected file as it is (sine it was automatically generated) and simply add a way to skip tests we know we cannot handle right now. I'm pretty sure we have this skip mechanism in some other litmus unit test
I guess we can re-open your PR where you implemented this and add support for further passes in litmus if needed. |
dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/VerificationTask.java
Outdated
Show resolved
Hide resolved
| @@ -52,6 +57,7 @@ public static VerificationTaskBuilder builder() { | |||
| public static class VerificationTaskBuilder { | |||
| protected WitnessGraph witness = new WitnessGraph(); | |||
| protected ConfigurationBuilder config = Configuration.builder(); | |||
| protected ProgressModel progressModel = ProgressModel.getDefault(); | |||
There was a problem hiding this comment.
This is probably causing the problem with not correctly setting the FP in the CI
There was a problem hiding this comment.
No, it is because ProgressModel is part of the VerificationTask and not "just a configuration". The main function makes sure to extract the configured progress model and make it explicit in the task, but if you create the task directly (like the unit tests do), this step is skipped.
dartagnan/src/test/java/com/dat3m/dartagnan/litmus/LitmusVulkanFairLivenessTest.java
Outdated
Show resolved
Hide resolved
|
There are a couple of hundred tests failing (I think 300 of the around 400 tests are failing). Should they all be listed in the |
|
You can copy this list into skip |
|
Your list is very incomplete. Still around 50% of the tests give UNKNOWN instead of PASS/FAIL. EDIT: Ah, you only did it for OBE. HSA and FAIR both still have together over a 100 tests with wrong verdicts. |
|
I generated this from the unit tests, but it is true that I just checked for EDIT: wait ... I did it from fair (where we should not have expected FAIL as I mentioned above) which should be the most general case: if there is an UNKNOWN it means that we are missing the automatic detection of spinloop and thus we should remove the tests for all progress models. |
|
You just did it for OBE (I edited my comment) which works fine now. HSA/FAIR still fail many times. EDIT: Yes, almost all cases are because of side-effectful loops. The progress models themselves should work fine. |
hernanponcedeleon
pushed a commit
that referenced
this pull request
Sep 16, 2024
Co-authored-by: Hernan Ponce de Leon <[email protected]>
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 adds support for the progress models FAIR (default), HSA, OBE, and UNFAIR.
Open issues: The interaction between blocked control barriers and scheduling is not fully clear. Currently, we consider a CB-blocked thread to be eligible for scheduling and thus unfair scheduling may permanently schedule blocked threads causing non-termination.