thread analysis requires context-sensitive threadids

[michael-schwarz]

As discovered by @Red-Panda64, the old thread analysis assumes we have context-sensitive thread ids activated when doing a threadenter which we know to be mutliple (c.f. #1187)

analyzer/src/analyses/threadAnalysis.ml

Lines 97 to 101 in 750f1ee

	let threadenter ctx ~multiple lval f args =
	if multiple then
	(let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in
	ctx.sideg tid (true, TS.bot (), false));
	[D.bot ()]

Another call to ThreadId.get_current_unlift is in thread_spawn for the spawned thread. However, this may be correct as we would still have a non-top thread id for the created thread at this point (?)

https://github.com/goblint/analyzer/blame/750f1ee274a00d6614cd2141f302ce551b094d57/src/analyses/threadAnalysis.ml#L103-L113

[michael-schwarz]

This is currently holding us back on some benchmarking for the PLDI project, so I will see if it can be easily fixed.

[michael-schwarz]

// PARAM: --set ana.context.gas_value 0 --set ana.activated[+] thread --set ana.activated[+] threadid

#include <pthread.h>
#include <stdio.h>

int myglobal;

void *t_flurb(void *arg) {
  myglobal=40; //RACE
  return NULL;
}

void *t_fun(void *arg) {
  unknown(t_flurb);
  return NULL;
}

int main(void) {
    pthread_t id;
    pthread_create(&id, NULL, t_fun, NULL);
    pthread_create(&id, NULL, t_fun, NULL);

    return 0;
}

Example to reproduce the issue.

[michael-schwarz]

Looking at this, it does not seem to be really correct anyway. ctx comes from the parent thread, so what we are in fact doing here is marking the parent thread as non-unique if it creates multiple child threads?

[sim642]

This is currently holding us back on some benchmarking for the PLDI project

A bit of an unrelated question, but what's the reason for using the old thread analysis, not the newer threadJoins?
We probably have discussed it at some point, but I'm not sure what the conclusion was: is there something the old analysis does that the newer ones cannot?

If I understand correctly, this concerns direct non-unique thread creations (like pthread_create_N), not those in a loop. What kind of benchmarks even have that?

[michael-schwarz]

A bit of an unrelated question, but what's the reason for using the old thread analysis, not the newer threadJoins?

I think we are using some kind of default configuration for Goblint, as the details are not too relevant and this way we need to do the least amount of arguing which configuration we chose.

Is there something the old analysis does that the newer ones cannot?

Iirc thread_joins was found to be a lot slower than this analysis, but is more expressive?

If I understand correctly, this concerns direct non-unique thread creations

Yes, and the case where threads are spawned from unknown functions, which is the case for ypbind.

[sim642]

Iirc thread_joins was found to be a lot slower than this analysis, but is more expressive?

Maybe, although I don't immediately know why that would be (other than being more precise simply means more contexts, etc). Both use side effects for threads to indicate dirty/clean exit, but the threads analysis does more than that: there's side effects and dependencies for the entire thread creation hierarchy which otherwise is implicit in thread IDs now.

Yes, and the case where threads are spawned from unknown functions, which is the case for ypbind.

Oh indeed, then as well. It would probably be a good idea to add missing things to LibraryFunctions though (or is the program itself incomplete?), otherwise there will be massive precision loss all over.