Mutex types support

[sim642]

With the revival of deadlock analysis (#655), it becomes more and more important that we handle behavior specific to mutex types.

Via pthread_mutexattr_settype there are the following possibilities:

• [ ] PTHREAD_MUTEX_DEFAULT – misuse is undefined behavior
• [ ] PTHREAD_MUTEX_NORMAL – relocking deadlocks, other misuse is undefined behavior
• [ ] PTHREAD_MUTEX_ERRORCHECK – misuse returns errors
• [ ] PTHREAD_MUTEX_RECURSIVE – relocking allowed, other misuse returns errors

Additionally:

• [ ] We don't do anything smart with read-write locks (pthread_rwlock_rdlock, pthread_rwlock_wrlock). (#661)
• [ ] Since some of the types are about differences in return values, we should also consider those, instead of completely ignoring them.

The different mutex types affect multiple features:

• Race detection
• Deadlock detection
• Base and Apron privatization

[michael-schwarz]

We don't do anything smart with read-write locks (pthread_rwlock_rdlock, pthread_rwlock_wrlock).

Are you sure? I think we have support for those.

[sim642]

That support is questionable at best: https://github.com/goblint/analyzer/blob/179c8b94ae0c801683d00fbf89f14e7e81223091/src/analyses/mutexAnalysis.ml#L165-L171 Whether a memory access is a read or write (argument w) has nothing to do with whether we're holding a read or write lock! Instead they relax one form of pairwise exclusion: reader-reader pairs do not mutually exclude each other. That's in no way reflected in the may_race check there.

This currently assumes the two notions are linked, i.e. read-write locks are correctly used that all writes use the write lock and not the read lock.

[sim642]

That is also reflected by this existing regression test: https://github.com/goblint/analyzer/blob/179c8b94ae0c801683d00fbf89f14e7e81223091/tests/regression/04-mutex/41-pt_rwlock.c#L9-L24 Writer-reader pairs do mutually exclude each other, so there should be no race, but we report one because our assumption is violated since data2 is written under a read lock.

I suppose we might still be at least sound here, although we could also be more precise and prove both globals race-free by dropping our silly assumption.