Fix privatization unsoundness due to non-definite and unknown mutexes

[sim642]

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.

[michael-schwarz]

Nice, thank you for the quick fix!

[michael-schwarz]

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

[michael-schwarz]

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]

I guess it is the same problem as

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

[michael-schwarz]

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

[michael-schwarz]

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