Improve multi-threaded valid-memcleanup

[mrstanb]

This PR is an attempt to improve precision for valid-memcleanup in multi-threaded programs

Main idea:

• Keep a global state of threads to allocated heap vars
• On *alloc() call:
  • Side-effect current thread and alloced heap var
• On free() call:
  • Remove the freed heap vars from the global state value, associated with the current thread
• On thread return/exit:
  • Check if the global state value for the returning/exiting thread is empty -> if no, then WARN

Test case 76/08 is still not working as expected, but I wanted to open the PR, so that you can also take a look at it

[sim642]

• Keep a global state of threads to allocated heap vars

• On *alloc() call:

  • Side-effect current thread and alloced heap var

• On free() call:

  • Remove the freed heap vars from the global state value, associated with the current thread

How can free remove anything from the global invariant? Side-effects just accumulate.

[mrstanb]

How can free remove anything from the global invariant? Side-effects just accumulate.

Fair point, thanks for the heads up! I think we could just keep track of allocated and freed memory as part of the global invariant in that case. That way we should be able to check for memory leaks at thread return/exit points.

[michael-schwarz]

Does not suffice to just keep track locally? If one of the functions that just terminates execution altogether, we warn. Otherwise, each thread checks for itself if it did a cleanup.
If all threads cleaned up their own stuff and the program is excited in the regular manner, all should be good?

[jerhard]

Fair point, thanks for the heads up! I think we could just keep track of allocated and freed memory as part of the global invariant in that case

The issue that when collecting the memory that is freed in the global invariant, this would be memory that may be freed: If one were to side-effect memory that would be freed whenever our overapproximation reaches a program point that calls free, this does not take into account that that call to free may actually not be reached.

Therefore, the set of allocated/freed memory should still be tracked in the local state, like in the single-threaded case.

[mrstanb]

So, I now tried again by removing the global state completely and using the local state instead:

• Local state is now a tuple of a map and a boolean
• The boolean is a simple flag that signifies whether malloc (or a similar function) has been called
• The map maps thread IDs to sets of heap variables
• The intuition is that each TID is mapped to its allocated memory
• Upon *alloc() calls, we add heap vars to the current thread's key in the map
• Upon free() calls, we remove heap vars from the current thread's key in the map
• Upon thread return/exit, we check if there's at least one value for the key of the current TID in the map -> if yes, we WARN

Note: for some reason, the check for the points-to set cardinality being one breaks the multi-threaded test cases and it fails to detect free calls in threads other than the main thread. I haven't looked into this issue and wanted to have it documented here as well.

P.S.: Thanks for your tips in the previous comments :)

[mrstanb]

I added the two Goblint options warn.memleak.memcleanup and warn.memleak.memtrack. The idea is to be able to produce warnings only for the one or the other type of memory leak violation.

Since the memLeak.ml code in this PR seems to always produce warnings for both types of SV-COMP properties, I'd wait to have the PR #1241 merged and then add the checks for these properties in the memLeak analysis (since the other PR actually has some spots in the analysis where a warning is produced only for the one or the other type of SV-COMP property)

[sim642]

Note: for some reason, the check for the points-to set cardinality being one breaks the multi-threaded test cases and it fails to detect free calls in threads other than the main thread. I haven't looked into this issue and wanted to have it documented here as well.

Where exactly is this check missing and what does it mean if we don't check for singleton points-to there?

Also, I'm a bit puzzled how this can work with just local state (except for the global boolean now). That essentially means, leaks can be checked by knowing nothing about any other threads. But how is that possible without even observing what other threads do?

[sim642]

provided that the only reason for program termination is that all threads terminate.

But we don't check that here at all because threads don't observe each other at all.

For example, here we find no memory leak because the leaky thread never terminates:

//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
#include <stdlib.h>
#include <pthread.h>

int *m1;

void *f1(void *arg) {
    m1 = malloc(sizeof(int));
    while (1);
}

int main(int argc, char const *argv[]) {
    pthread_t t1;
    pthread_create(&t1, NULL, f1, NULL);
    return 0; //NOWARN
}

[michael-schwarz]

For example, here we find no memory leak because the leaky thread never terminates:

I don't think this is a memory leak (or at least not in the sense used in sv-comp). The program will not terminate as f1 is an in infinite loop.

[sim642]

It terminates immediately if you compile and run it: https://godbolt.org/z/3sjshTj3h.

It's not specific to the main thread returning even. Any other thread may call exit and the process terminates. And when it does, it doesn't wait for threads to finish.

[michael-schwarz]

Crap, you're right of course. We take care of calls to exit but I seems I didn't consider the case of main implicitly calling exit. Actually, for main one would need some of type of all-threads-must-have-been-joined property.

[michael-schwarz]

I got confused with the threading model of the JVM.

[michael-schwarz]

We should add an is-single-thread query for returning from main then, that should make it sound again.

[jerhard]

We should add an is-single-thread query for returning from main then, that should make it sound again.

I will have a look at this.

[jerhard]

I added a check that when the main thread reaches its return, it is definitely single-threaded in case ever any memory was allocated.

I wondered whether a pthread exit in main should be handled the same way, but pthread_exit for the main thread behaves differently:

To allow other threads to continue execution, the main thread should terminate by calling pthread_exit() rather than exit(3).

I.e., if the main thread calls pthread_exit, and some other thread is running in an infinite loop, the program runs forever. If a infinitely-looping thread had allocated some memory before, this should not considered a memory leak, IMHO.

[jerhard]

The analysis now requires the thread analysis for a precise handling in the multi-threaded case if there is any memory allocation, to be able to recover from the multithreaded mode. As the thread analysis is already in the svcomp.json, this should not be a problem, however.

[jerhard]

The analysis is currently unsound on this test case, as Goblint thinks that the program is single-threaded at the end of main. However, the thread f2 continues to run after f1 has called pthread_exit, and is killed only when main reaches its return (causing a memory leak.)

//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread
#include <stdlib.h>
#include <pthread.h>

int *m1;

void *f2(void *arg) {
    m1 = malloc(sizeof(int));
    while (1);
    return NULL;
}

void *f1(void *arg) {
    pthread_t t2;
    pthread_create(&t2, NULL, f2, NULL);

    pthread_exit(NULL);
    return NULL;
}

int main(int argc, char const *argv[]) {
    pthread_t t1;
    pthread_create(&t1, NULL, f1, NULL);
    pthread_join(t1, NULL);

    return 0; // WARN
}

So the handling of pthread_exit in the thread analysis seems to be unsound. The unsoundness does not appear if the pthread_exit(NULL); call is removed from f1.

[jerhard]

Handling a pthread_exit like a return in the thread analysis (645b03cf) fixes the issue with test case 76/18 that was described in the previous post.

[michael-schwarz]

Handling a pthread_exit like a return in the thread analysis (645b03cf) fixes the issue with test case 76/18 that was described in the previous post.

I looked at it, and this seems to indeed be what we want here.

[michael-schwarz]

I think we can now merge this into master as well? Wdyt @sim642?

[sim642]

I'll merge it via #1257 because it already contains the merge conflict resolution between the latest versions of #1241 and #1246.