Repository navigation
Conversation
…osen labels exploreRaces makes the calling thread's future children racy, by their thread ids. A test of a large system, which forks many threads before it gets to what it wants to explore, can either make all of them racy, and spend most of each schedule's race analysis on threads it does not care about, or none. exploreRacesOfThreadsLabelled p takes into account, when discovering races, each thread once it is given a label that satisfies p, until it is given one that does not. Such a thread's children do not inherit it. Thread ids do not change, so ScheduleControl replay is unaffected. runSimTrace ignores it.
So a test can call it once it has set up what it wants to explore: the threads it started during the set-up race from then on, and the set-up's own races, which IOSimPOR would otherwise reverse first and spend its bounds on, are left out. A later call recomputes the set from the new predicate; calling it with const False stops all racing by label.
…rent A thread racing by its label now lends that to the threads it forks, until they are labelled themselves; then their own label decides. A helper the code forks without a label, such as an async worker, races with the thread that started it, while a labelled child, such as a driver's sender, is still left out unless the predicate names it.
coot
reviewed
Nov 13, 2026
coot
left a comment
coot
left a comment
Collaborator
There was a problem hiding this comment.
This solution will only make racing threads the threads that were started by one of the thread that were racy by label. The other limitation is that it only applies to threads that exist when one runs the exploreRacesOfThreadsLabelled primitive operation.
I have another solution which doesn't share the latter limitation and it will also allow to make the main thread racy (which is also limitation of the current approach). I'll submit a PR soon, since it's quite simple and it doesn't require any changes to IOSim primitive operations.
| labelled = Set.fromList | ||
| [ threadId t | ||
| | t <- thread : Map.elems threads | ||
| , Just l <- [threadLabel t] |
Collaborator
There was a problem hiding this comment.
Suggested change
| , Just l <- [threadLabel t] | |
| , l <- maybeToList (threadLabel t) |
This branch has not been deployed
This file contains hidden or 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
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.
Used to be able to select which threads should race from outside the production code.