Mutex-Meet-TID without clusters more precise than approach with clusters
#1551
Comments
michael-schwarz
added
precision
relational
On analyzer/src/analyses/apron/relationAnalysis.apron.ml Lines 676 to 679 in b129fab |
|
Yeah, I did the |
|
The issue seems unrelated to widening, it happens with |
|
Relying on YAML might make debugging easier. There we get
The invariants provided here look slightly dubious to me as to whether they actually hold. |
|
It seems to hold here as |
|
Especially since we say
|
|
It appears that the case for an unknown thread was missing the following snippet which the other case has: (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
EnterMultithreaded events only execute after threadenter and threadspawn. *)
if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st);Otherwise, the invalidation of |
|
Completed in #1417 |
|
There seems to be another instance of this, also with the same program. |
|
The problematic program looks like this: #include<pthread.h>
int d, j, k;
void g(void* arg);
void h();
pthread_mutex_t f;
void nothing() {};
int top() {
int top2;
return top2;
}
void main() {
d = top();
if (d) {
k = 1;
pthread_t tid;
pthread_create(&tid, 0, ¬hing, NULL);
pthread_mutex_lock(&f);
j=1;
pthread_mutex_unlock(&f);
pthread_mutex_lock(&f);
}
g(h);
} |
|
The culprit seems to be the call |
|
The more sensible program is the following: #include<pthread.h>
int d, j, k;
pthread_mutex_t f;
void nothing() {};
void nothing2() {};
int top() {
int top2;
return top2;
}
void main() {
d = top();
if (d) {
k = 1;
pthread_t tid;
pthread_create(&tid, 0, ¬hing, NULL);
pthread_mutex_lock(&f);
j = 0; // To ensure something is published
pthread_mutex_unlock(&f);
pthread_mutex_lock(&f);
}
pthread_t tid2;
pthread_create(&tid2, 0, ¬hing2, NULL);
} |
|
#1555 seems to fix the issue at least for the program where it could initially be observed. |
For the following small program:
we get
While such effects may happen due to W/N, it seems odd that it can be observed on such small programs.
bhaving no implementation available seems crucial for this to happen, so it may be invalidation related somehow...Detailed comparison
``` Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPrivTID(no-clusters,join)): [|d-1.>=0; -d+1.>=0; -d+e+2147483649.>=0; d+e+2147483647.>=0; e+2147483648.>=0; -d-e+2147483648.>=0; d-e+2147483646.>=0; -e+2147483647.>=0; -d+f+2147483649.>=0; d+f+2147483647.>=0; -e+f+2147483648.>=0; e+f+2147483648.>=0; f+2147483648.>=0; -d-f+2147483648.>=0; d-f+2147483646.>=0; -e-f+2147483647.>=0; e-f+2147483648.>=0; -f+2147483647.>=0|] (env: [|0> __daylight:int; 1> __timezone:int; 2> argc#996:int; 3> d:int; 4> daylight:int; 5> e:int; 6> f:int; 7> timezone:int|]) more precise than Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPrivTID(cluster12,join)): [|d-1.>=0; -d+1.>=0; -d+e+2147483649.>=0; d+e+2147483647.>=0; e+2147483648.>=0; -d-e+2147483648.>=0; d-e+2147483646.>=0; -e+2147483647.>=0; -d+f+2147483649.>=0; d+f+2147483647.>=0; -e+f+4294967295.>=0; e+f+4294967296.>=0; f+2147483648.>=0; -d-f+2147483648.>=0; d-f+2147483646.>=0; -e-f+4294967294.>=0; e-f+4294967295.>=0; -f+2147483647.>=0|] (env: [|0> __daylight:int; 1> __timezone:int; 2> argc#996:int; 3> d:int; 4> daylight:int; 5> e:int; 6> f:int; 7> timezone:int|]) reverse diff: -e+f+2147483648.>=0, -e-f+2147483647.>=0, e+f+2147483648.>=0, e-f+2147483648.>=0 ```
The text was updated successfully, but these errors were encountered: