Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Change/Fix to use a symmetric barrier to synchronize domains #509

Merged
merged 1 commit into from
Jan 14, 2025

Conversation

polytypic
Copy link
Contributor

@polytypic polytypic commented Jan 12, 2025

Unless I've misunderstood something, the idea is to synchronize the two domains before the two sequences of operations are run in parallel. The previous implementation used an asymmetric approach where one domain only spins on a flag and the other only sets the flag. That is not really guaranteed to synchronize the domains — the domain setting the flag might start running the operations before the domain spinning on the flag gets a chance to run. This PR changes the code to use a symmetric barrier: a counter is initialized with 2, both domains decrement the counter, and then spin until the counter becomes zero. This should improve the synchronization between the two domains.

@jmid
Copy link
Collaborator

jmid commented Jan 14, 2025

Thanks! Having a symmetric condition makes sense. I just ran some statistics to confirm that this does not influence the error finding behaviour (I wasn't expecting it to - but just to make sure).

Can I ask you to:

  • make the corresponding change to run_parallel in lib/lin_domain.ml and
  • add a CHANGES.md entry?

Thanks again! 🙏

@polytypic polytypic force-pushed the use-a-symmetric-barrier-to-sync-domains branch from 47b70fe to 28bcca0 Compare January 14, 2025 13:52
Copy link
Collaborator

@jmid jmid left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@polytypic polytypic force-pushed the use-a-symmetric-barrier-to-sync-domains branch from 28bcca0 to 6c86871 Compare January 14, 2025 15:29
@jmid
Copy link
Collaborator

jmid commented Jan 14, 2025

CI summary for 6c86871: all 34 workflows passed.
Merging...

@jmid jmid merged commit 9fc194a into main Jan 14, 2025
34 checks passed
@polytypic polytypic deleted the use-a-symmetric-barrier-to-sync-domains branch January 14, 2025 21:02
@jmid
Copy link
Collaborator

jmid commented Jan 15, 2025

CI summary for merge to main:

Out of 35 workflows - 1 failed with a CI related error

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants