Comments (9)
@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.
Related Issues (20)
- Heads up: renaming master branch into main HOT 1
- Implement a per-allocation-site memory-safety checking
- Running example with SMACK
- Multi-language model checking, on inequality modify languages to match correct model?
- Verifying Fortran Intrinsic Function ABS
- Some Rust `Box` operation is internally supported by rustc HOT 1
- Leverage `instcombine` pass
- Generalize `clang-options` into `compiler-options` HOT 1
- Upgrade Rust version to support edition 2021
- Verifying D programs
- Debug information when using LLVM IR as an input HOT 2
- How it can support ensures, requires, invariant API in Rust
- llvm2bpl report error when use smack generate boogie code
- Build issue on Ubuntu 18.04
- Unhandled LLVM intrinsic generated from math.c HOT 1
- Unhandled experimental intrinsics crash SMACK
- All programs verify when SMT solver (Z3) is not present HOT 1
- Advanced SMACK guide
- Reproduce the paper, but I can't accomplish HOT 10
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from smack.