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

Fix thread for non-unique spawns #1617

Merged
merged 3 commits into from
Nov 6, 2024
Merged

Fix thread for non-unique spawns #1617

merged 3 commits into from
Nov 6, 2024

Conversation

michael-schwarz
Copy link
Member

The handling of threadenter in the case of a thread being spawned non-uniquely was broken:

  • It failed when thread ids where non-unique.
  • It actually caused a side-effect to the thread id of the creator marking that as non-unique rather than the created thread.

This PR fixes this issue which hopefully means our experiments for PLDI can continue (CC @Red-Panda64: try if merging this into your branch helps), and also increases precision for cases where the non-history thread id is enabled.

Closes #1615

@sim642
Copy link
Member

sim642 commented Nov 4, 2024

The tests seem to be about not crashing and precision, but isn't this also a matter of soundness?

@michael-schwarz
Copy link
Member Author

michael-schwarz commented Nov 4, 2024

I thought so as well and tried to create a new test that would be unsound before but would work now. However, marking the creator as non-unique also leads to the created thread being marked as such (through the recursion in is_not_unique).
So it seems like it actually is only a precision issue vis à vis the old implementation.

Nevertheless, the original soundness tests that were added in #1187 are still around and pass.

tests/regression/40-threadid/12-multiple-created-only.c Outdated Show resolved Hide resolved
src/analyses/threadAnalysis.ml Outdated Show resolved Hide resolved
@sim642 sim642 added this to the v2.5.0 milestone Nov 6, 2024
@michael-schwarz michael-schwarz merged commit e8b56ec into master Nov 6, 2024
21 checks passed
@michael-schwarz michael-schwarz deleted the issue_1615 branch November 6, 2024 08:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

thread analysis requires context-sensitive threadids
2 participants