Handling thread_local variables

[hernanponcedeleon]

Can smack handle thread local variables? I have the following C code

__thread intptr_t tindex;
atomic_bool threshold_reached = 0;

The corresponding llvm code clearly marks tindex as thread_local

@threshold_reached = dso_local global i8 0, align 1
@tindex = dso_local thread_local global i64 0, align 8

However I don't see any related difference in the boogie code generated by smack between threshold_reached and tindex, neither in the constant definition

const {:allocSize 1} threshold_reached: ref;
axiom (threshold_reached == $sub.ref(0, 1025));
const {:allocSize 8} tindex: ref;
axiom (tindex == $sub.ref(0, 2057));

nor in the static initialisation

procedure  __SMACK_static_init()
{
$bb0:
  $M.0 := $store.i8($M.0, threshold_reached, 0);
  call {:cexpr "threshold_reached"} boogie_si_record_i8(0);
  $M.0 := $store.i64($M.0, tindex, 0);
  call {:cexpr "tindex"} boogie_si_record_i64(0);
  $exn := false;
  return;
}

which suggests that smack just ignores the tag. Am I right?

[shaobo-he]

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

[hernanponcedeleon]

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.

[hernanponcedeleon]

@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.

[shaobo-he]

@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.

[shaobo-he]

@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?

[hernanponcedeleon]

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.

[shaobo-he]

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.

[shaobo-he]

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

[hernanponcedeleon]

Looks good! Thanks @shaobo-he