search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
172 stars 72 forks source link

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

Closed sim642 closed 3 months ago

sim642 commented 3 months ago

Problem

As mentioned in https://github.com/goblint/analyzer/pull/1430#issuecomment-2075246339, 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 https://github.com/goblint/analyzer/issues/1430#issuecomment-2132284679

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.

michael-schwarz commented 3 months ago

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

michael-schwarz commented 3 months ago

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 commented 3 months ago

I guess it is the same problem as

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

michael-schwarz commented 3 months ago

I would guess the reason it works on master may be https://github.com/goblint/analyzer/pull/1475

michael-schwarz commented 3 months ago

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