Skip to content

Fix privatization unsoundness due to non-definite and unknown mutexes#1500

Merged
sim642 merged 8 commits intomasterfrom
priv-nondefinite-mutex
Jun 5, 2024
Merged

Fix privatization unsoundness due to non-definite and unknown mutexes#1500
sim642 merged 8 commits intomasterfrom
priv-nondefinite-mutex

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Jun 4, 2024 •
edited
Loading

Problem

As mentioned in #1430 (comment), privatizations don't do anything special with non-definite mutexes.

What are privatizations supposed to do with those? It seems to me that we completely forgot about the non-definite possibilities, which might make things even unsound.

I think I considered this issue when designing the privatizations. They should still be sound for the original setting according to the following arguments:

  • For lock & mine-W: Incorporating too many values early makes the analysis imprecise, not unsound; All other operations are based on must-locksets, and for background locksets and minimal locksets only definite elements are kept
  • For write: lock is a no-op, other actions are based on must-lockset
  • For per-mutex flavors incl. relational & protection-based: Protection by one of these indefinite addresses means they are always held when the global is accessed, so that is not harmful either

However, these are indeed a bit shaky in some places and may easily be subject to breakage. So in the long run, it does make sense to refactor this as well.

Also, with the new additions such as atomic and invariants about unprotected globals, I'm not sure if this still all holds.

Originally posted by @michael-schwarz in #1430 (comment)

As the added test case shows, this is wrong and all of them are unsound.

Solution

As discussed during GobCon, the fix is to only call lock and unlock of privatizations with definite mutexes. This PR adapts the recently-fixed-and-refactored (#1430) must lockset analysis logic to base and relation analyses for these events. Notably, unlock of indefinite mutex calls privatization's unlock for all may-aliasing held locks. This PR also fixes the long-standing unsoundness in privatizations of unlocking unknown mutexes: just by unlocking all held locks unconditionally.

@sim642 sim642 self-assigned this Jun 4, 2024
@sim642 sim642 added this to the v2.4.0 milestone Jun 4, 2024
@sim642 sim642 added the relational Relational analyses (Apron, affeq, lin2var) label Jun 4, 2024
@sim642 sim642 changed the title Privatizations unsound with non-definite mutexes Fix privatization unsoundness due to non-definite and unknown mutexes Jun 4, 2024
@sim642 sim642 marked this pull request as ready for review June 4, 2024 13:08
@sim642 sim642 requested a review from michael-schwarz June 4, 2024 13:08
@sim642 sim642 mentioned this pull request Jun 4, 2024
Merged
michael-schwarz
michael-schwarz approved these changes Jun 4, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

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

Nice, thank you for the quick fix!

@sim642 sim642 merged commit 40b4b07 into master Jun 5, 2024
@sim642 sim642 deleted the priv-nondefinite-mutex branch June 5, 2024 07:29
sim642 added a commit that referenced this pull request Jun 6, 2024
@sim642
Add SKIP to Apron tests (PR #1500)
a3d43f6
sim642 added a commit that referenced this pull request Jun 6, 2024
@sim642
Add enabled_if to Apron cram tests (PR #1500)
8998e47
@michael-schwarz michael-schwarz mentioned this pull request Jun 10, 2024
Closed
7 tasks
michael-schwarz pushed a commit that referenced this pull request Jun 10, 2024
@sim642 @michael-schwarz
Add SKIP to Apron tests (PR #1500)
c06af68
michael-schwarz pushed a commit that referenced this pull request Jun 10, 2024
@sim642 @michael-schwarz
Add enabled_if to Apron cram tests (PR #1500)
44d7abb
@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Jun 10, 2024

After cherry-picking this and #1430 onto #1417, the newly added tests seem to not terminate.

@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Jun 10, 2024

In 46/87, this seems to be due to the line:

int r = __VERIFIER_nondet_bool();

If I replace it with

int top;
int r=0;
if(top) { r =1}

it works.

@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Jun 10, 2024

I guess it is the same problem as

// TODO: why nonterm without threadflag path-sens? on master

@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Jun 10, 2024

I would guess the reason it works on master may be #1475

@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Jun 10, 2024

Yes, if I turn off the special handling in branched_thread_creation (), it misbehaves.

@michael-schwarz michael-schwarz mentioned this pull request Jun 11, 2024
Closed
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 2, 2024
@sim642
[new release] goblint (2.4.0)
38186e2 
CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).
@sim642 sim642 mentioned this pull request Aug 2, 2024
Merged
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
@sim642 @avsm
[new release] goblint (2.4.0)
2afe816 
CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@michael-schwarz michael-schwarz michael-schwarz approved these changes

Assignees

@sim642 sim642

Labels

bug relational Relational analyses (Apron, affeq, lin2var) unsound

Projects

None yet

Milestone

v2.4.0

Development

Successfully merging this pull request may close these issues.

2 participants

@sim642 @michael-schwarz