Goblint cannot handle even simple cases of malloc'ed mutexes

[michael-schwarz]

Looking at some tasks @vesalvojdani's CoOperRace could do but Goblint can't, I realized Goblint can't handle dynamically allocated mutexes even in the most simple of cases:

#include <pthread.h>
pthread_mutex_t *data1Lock;
int g;

void *funcA(void *param) {
    pthread_mutex_lock(data1Lock);
    g = 1; //NORACE
    pthread_mutex_unlock(data1Lock);
}

int main(int argc, char *argv[]) {
    data1Lock = (pthread_mutex_t *) malloc(sizeof(pthread_mutex_t));
    pthread_mutex_init(data1Lock, ((void *)0));

    pthread_t one, two;

    pthread_create(&one, ((void *)0), &funcA, ((void *)0));
    pthread_create(&two, ((void *)0), &funcA, ((void *)0));
}

Here, we even do the initialization before even going multi-threaded, and all allocs happen from the main thread, outside any loops.
One may even say it's a bit embarrassing that this trivial program is enough to defeat Goblint.

[michael-schwarz]

Here, the lockset after pthread_mutex_lock(data1Lock) is empty.

[sim642]

Maybe the reason is not having any unique malloced objects by default.

I recall that we should have regression tests with malloced mutexes, but I guess they're somehow different or use malloc uniqueness. Although I think some of those tests are quite old even.

[michael-schwarz]

Ah, I had assumed the malloc uniqueness was still on for SV-COMP as it was in the last years, but I guess someone disabled it in the meantime. For this example it now works when manually enabling it again.

However, we still have seriously weird things:

./goblint 2.c --conf conf/svcomp25.json --sets ana.specification ../../sv-comp/sv-benchmarks/c/properties/no-data-race.prp --sets exp.architecture 32bit --enable pre.enabled --set ana.malloc.unique_address_count 5

fails with this program:

#include<pthread.h>
static int iRThreads = 1;
static int data1Value = 0;
pthread_mutex_t *data1Lock;
void *funcA(void *param) {
    pthread_mutex_lock(data1Lock);
    data1Value = 1;
    pthread_mutex_unlock(data1Lock);
}

int main(int argc, char *argv[]) {
    data1Lock = (pthread_mutex_t *) malloc(sizeof(pthread_mutex_t));

    pthread_t one;
    pthread_t two;

    pthread_create(&one, ((void *)0), &funcA, ((void *)0));

    for (int i = 0; i < iRThreads; i++) {
      pthread_create(&two, ((void *)0), &funcA, ((void *)0));
    }

    return 0;
}

As soon as I make iRThreads a local or remove the loop, it succeeds again. This looks like the autotuner going wrong.

[michael-schwarz]

Ok, we're quite stupid here (I can say this, it seems to be my brainfart), and the involvement of the autotuner is spurious:

analyzer/src/analyses/wrapperFunctionAnalysis.ml

Lines 172 to 176 in f99a9f6

	| Q.IsMultiple v ->
	begin match NodeVarinfoMap.from_varinfo v with
	| Some (_, _, c) -> UniqueCount.is_top c || not (man.ask Q.MustBeUniqueThread)
	| None -> false
	end

When we ask whether a block of memory is unique, we ask whether the thread accessing it is unique instead of asking about the creating thread 🙃.

Thus, our uniqueness analysis is hamstrung by only working inside unique threads.

[sim642]

Ah, I had assumed the malloc uniqueness was still on for SV-COMP as it was in the last years, but I guess someone disabled it in the meantime. For this example it now works when manually enabling it again.

I think we never had it enabled unconditionally, only through autotuner: either by property (for MemSafety) or by some other logic? But I might be misremembering about the latter: we have some loop/array unrolling which prioritizes mutexes or something, but not for malloc uniqueness.
Perhaps we could benefit from some more granular malloc uniqueness (annotations) determined by autotuning for things like mutexes as well.