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 mutex-meet for malloc after thread creation #1492

Merged
merged 4 commits into from
Jul 31, 2024
Merged

Fix mutex-meet for malloc after thread creation #1492

merged 4 commits into from
Jul 31, 2024

Conversation

michael-schwarz
Copy link
Member

@michael-schwarz michael-schwarz commented May 27, 2024

The issue in #1489 was that the global invariant for the blob was still bot, making the meet deadcode.

TODO:

  • mutex-meet-atomic privatization still unsound
  • Verify if these are really all changes needed for mutex-meet-atomic (It seems weird that no handling of these cases is necessary in get_mutex_global_g_with_mutex_inits_atomic CC: @sim642)

Closes #1489

@michael-schwarz michael-schwarz added bug unsound relational Relational analyses (Apron, affeq, lin2var) labels May 27, 2024
@michael-schwarz michael-schwarz marked this pull request as draft May 27, 2024 15:48
@michael-schwarz michael-schwarz marked this pull request as ready for review May 27, 2024 15:56
@sim642 sim642 self-requested a review May 28, 2024 07:13
@sim642
Copy link
Member

sim642 commented May 28, 2024

  • Verify if these are really all changes needed for mutex-meet-atomic (It seems weird that no handling of these cases is necessary in get_mutex_global_g_with_mutex_inits_atomic CC: @sim642)

That doesn't restrict unprotected invariants to a single variable, which if missing, causes bot. It might just be pushing the issue further down the line though: at some point there could still be an Apron assignment from that variable to something else. But maybe the variable will never be missing, rather some meet will just unify it to top?

@sim642
Copy link
Member

sim642 commented May 30, 2024

mutex:[__VERIFIER_atomic] also starts out with bottom (env: [||]), so that's not the difference I suspect. Rather, the difference comes from this check:

if not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *)
(* This is an escaped variable whose value was never side-effected to get_mutex_inits' *)
get_mutex_global_g
else
RD.join get_mutex_global_g get_mutex_inits'

get_mutex_global_g_with_mutex_inits_atomic doesn't have such condition and always does the join (with non-bottom), which makes everything fine.
I wonder if also checking RD.mem_var get_mutex_global_g g_var before doing this would be a fix closer to the existing logic.

@sim642 sim642 merged commit a592680 into master Jul 31, 2024
22 of 23 checks passed
@sim642 sim642 deleted the issue_1489 branch July 31, 2024 07:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug relational Relational analyses (Apron, affeq, lin2var) unsound
Projects
None yet
2 participants