Handling thread_local variables about smack HOT 9 CLOSED

@shaobo-he would it be possible to add support for thread local variables in smack? We are starting to see more benchmarks using those and this is causing wrong verification results.

I'm going to look into it this week. This may take a while since I'm not an expert in pthreads.

from smack.

Hi, @hernanponcedeleon, I don't think it is used or checked by SMACK. Relevant APIs are *ThreadLocalMode* and I don't find them.

from smack.

I think the following two programs show the problem.

user@e5f3c9c70c7e:~/smack$ cat test.c 
#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#include <pthread.h>
#include <stdatomic.h>
#include <assert.h>

int myindex = 0;

void *thread_n(void *arg)
{
    myindex++;
    assert(myindex == 1);
    return NULL;
}

int main()
{
    pthread_t t1, t2;

    pthread_create(&t1, NULL, thread_n, (void *) 0);
    pthread_create(&t2, NULL, thread_n, (void *) 1);

    return 0;
}
user@e5f3c9c70c7e:~/smack$ smack --pthread test.c 
SMACK program verifier version 2.8.0
...
SMACK found an error.

The above one is correct because both threads increment the same global variable.

user@e5f3c9c70c7e:~/smack$ cat test_local.c 
#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#include <pthread.h>
#include <stdatomic.h>
#include <assert.h>

__thread int myindex = 0;

void *thread_n(void *arg)
{
    myindex++;
    assert(myindex == 1);
    return NULL;
}

int main()
{
    pthread_t t1, t2;

    pthread_create(&t1, NULL, thread_n, (void *) 0);
    pthread_create(&t2, NULL, thread_n, (void *) 1);

    return 0;
}
user@e5f3c9c70c7e:~/smack$ smack --pthread test_local.c 
SMACK program verifier version 2.8.0
...
SMACK found an error.

This one however is not because variables are thread local.

from smack.

@shaobo-he would it be possible to add support for thread local variables in smack? We are starting to see more benchmarks using those and this is causing wrong verification results.

from smack.

@hernanponcedeleon I thought about it for a while and concluded it's not trivial at all to implement this. So, I was wondering if it's hard to rewrite thread-local variables into local variables of functions running inside the threads.

Actually, let me share my current thoughts. Thread-local variables can be encoded as an array from thread ids to values. So, when a memory access happens, we have to query if the memory address refers to a thread-local variable. If so, we fetch the current thread id and further get/set the value otherwise get/set the value normally. This would incur overhead for each memory access encoding. Though there may be some optimizations, I doubt their generality.

@zvonimir @MontyCarter any thoguhts?

from smack.

Thanks a lot @shaobo-he for making the effort, I really appreciate.

Unfortunately, I don't think this is really possible. The benchmarks we are trying to verify come from the Linux Kernel which heavily use thread local storage.

Would at least be possible to "tag" global variables coming from thread local one? My understanding is that you have this information at the LLVM level. I think and annotation like

const {:allocSize 8, :treadLocal} tindex: ref;

would be sufficient for us.

from smack.

Thanks a lot @shaobo-he for making the effort, I really appreciate.

Unfortunately, I don't think this is really possible. The benchmarks we are trying to verify come from the Linux Kernel which heavily use thread local storage.

Would at least be possible to "tag" global variables coming from thread local one? My understanding is that you have this information at the LLVM level. I think and annotation like

const {:allocSize 8, :treadLocal} tindex: ref;

would be sufficient for us.

Thank you for the feedback. Let me implement this.

from smack.

@hernanponcedeleon I implemented it via commit 9cbbfd9. It adds {:threadLocal} attributes for thread-local varaibles. Please let me know if it works for you.

from smack.

Looks good! Thanks @shaobo-he

from smack.