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.
DPOR algorithms schedule race reversals based on depedency relation, which is a binary relation on transitions indicating whether two operations are racing or not. Currently, we treat any two accesses on the same variable (by two different domains) as a race but this is simplistic. In many cases such accesses do commute, e.g.: two reads, two incrs, two failed cases, two writes writing the same value.
This PR implements the first part: commutative reads (get, failed CAS). There are two main changes in this PR:
Furthermore, I've slid in a 2-line optimization I've noticed in nidhugg. Currently, we schedule one of the initials is none of them is present in the backtrack (i.e. an initial is not scheduled). I've noticed an optimization in nidhugg, which goes one step further - also checks whether sleep set contains any of the initials (i.e. an initials is ignored, thus its been processed before).
Results
Lockfree
Lockfree tests
ws_deque_dscheck
,mpsc_queue_dscheck
,michael_scott_queue_dscheck
,Spsc_queue_dscheck
,treiber_stack_dscheck
vs source sets branch.Eio
Eio tests
make dscheck
vs optims branch.