Proper support for mutex type PTHREAD_MUTEX_ERRORCHECK checking return types

[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). (Fix read-write lock access handling #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:

analyzer/src/analyses/mutexAnalysis.ml

Lines 165 to 171 in 179c8b9

	let access ctx e vo w =
	if w then
	(* when writing: ignore reader locks *)
	Lockset.filter snd ctx.local
	else
	(* when reading: bump reader locks to exclusive as they protect reads *)
	Lockset.map (fun (x,_) -> (x,true)) ctx.local

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:

analyzer/tests/regression/04-mutex/41-pt_rwlock.c

Lines 9 to 24 in 179c8b9

	void *t_fun(void *arg) {
	pthread_rwlock_wrlock(&rwlock);
	data1++; // NORACE
	printf("%d",data2); // RACE
	pthread_rwlock_unlock(&rwlock);
	return NULL;
	}
	int main(void) {
	pthread_t id;
	pthread_create(&id, NULL, t_fun, NULL);
	pthread_rwlock_rdlock(&rwlock);
	printf("%d",data1); // NORACE
	data2++; // RACE
	pthread_rwlock_unlock(&rwlock);

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.