Skip to content

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.

michael-schwarz and others added 2 commits November 4, 2024 10:38
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@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

3 participants