Skip to content

Commit 5b97ec4

Browse files
committed
more racing test cases
1 parent 1879e7e commit 5b97ec4

7 files changed

+197
-0
lines changed
Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset
2+
// TODO broken, since locksets have more granular path sensitivity than creation locksets
3+
#include <pthread.h>
4+
5+
int global = 0;
6+
pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
7+
pthread_t id1, id2;
8+
9+
void *t1(void *arg) {
10+
pthread_mutex_lock(&mutex);
11+
global++; // RACE!
12+
pthread_mutex_unlock(&mutex);
13+
return NULL;
14+
}
15+
16+
void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since the mutex does not have to be locked during creation
17+
global++; // RACE!
18+
return NULL;
19+
}
20+
21+
int main(void) {
22+
pthread_create(&id1, NULL, t1, NULL);
23+
int maybe;
24+
if (maybe) {
25+
pthread_mutex_lock(&mutex);
26+
}
27+
pthread_create(&id2, NULL, t2, NULL);
28+
return 0;
29+
}
Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset
2+
// TODO broken, since locksets have more granular path sensitivity than creation locksets
3+
#include <pthread.h>
4+
5+
int global = 0;
6+
pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
7+
pthread_t id1, id2;
8+
9+
void *t1(void *arg) {
10+
pthread_mutex_lock(&mutex);
11+
global++; // RACE!
12+
pthread_mutex_unlock(&mutex);
13+
return NULL;
14+
}
15+
16+
void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock may happen before joining
17+
global++; // RACE!
18+
return NULL;
19+
}
20+
21+
int main(void) {
22+
pthread_create(&id1, NULL, t1, NULL);
23+
pthread_mutex_lock(&mutex);
24+
pthread_create(&id2, NULL, t2, NULL);
25+
int maybe;
26+
if (maybe) {
27+
pthread_mutex_unlock(&mutex);
28+
}
29+
pthread_join(id2, NULL);
30+
return 0;
31+
}
Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset
2+
// TODO broken, since locksets have more granular path sensitivity than creation locksets
3+
#include <pthread.h>
4+
5+
int global = 0;
6+
pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER, mutex_alt = PTHREAD_MUTEX_INITIALIZER;
7+
pthread_t id1, id2;
8+
9+
void *t1(void *arg) {
10+
pthread_mutex_lock(&mutex);
11+
global++; // RACE!
12+
pthread_mutex_unlock(&mutex);
13+
return NULL;
14+
}
15+
16+
void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock may happen before joining
17+
global++; // RACE!
18+
return NULL;
19+
}
20+
21+
int main(void) {
22+
pthread_create(&id1, NULL, t1, NULL);
23+
pthread_mutex_lock(&mutex);
24+
pthread_create(&id2, NULL, t2, NULL);
25+
pthread_mutex_lock(&mutex_alt);
26+
pthread_mutex_t *mutex_ref = &mutex_alt;
27+
int maybe;
28+
if (maybe) {
29+
mutex_ref = &mutex;
30+
}
31+
pthread_mutex_unlock(mutex_ref);
32+
pthread_join(id2, NULL);
33+
return 0;
34+
}
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset
2+
#include <pthread.h>
3+
4+
int global = 0;
5+
pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
6+
pthread_t id1, id2;
7+
8+
void *t1(void *arg) {
9+
pthread_mutex_lock(&mutex);
10+
global++; // RACE!
11+
pthread_mutex_unlock(&mutex);
12+
return NULL;
13+
}
14+
15+
void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, since an unlock could happen before joining
16+
global++; // RACE!
17+
return NULL;
18+
}
19+
20+
int main(void) {
21+
pthread_create(&id1, NULL, t1, NULL);
22+
pthread_mutex_lock(&mutex);
23+
pthread_create(&id2, NULL, t2, NULL);
24+
pthread_mutex_t *mutex_ref;
25+
pthread_mutex_unlock(mutex_ref); // unlock of unknown mutex
26+
pthread_join(id2, NULL);
27+
return 0;
28+
}
Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset
2+
#include <pthread.h>
3+
4+
int global = 0;
5+
pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
6+
pthread_t id1, id2;
7+
8+
void *t1(void *arg) {
9+
pthread_mutex_lock(&mutex);
10+
global++; // RACE!
11+
pthread_mutex_unlock(&mutex);
12+
return NULL;
13+
}
14+
15+
void *t2(void *arg) { // t2 is not protected by mutex locked in main thread, joining may happen before unlocking
16+
global++; // RACE!
17+
return NULL;
18+
}
19+
20+
int main(void) {
21+
pthread_create(&id1, NULL, t1, NULL);
22+
pthread_mutex_lock(&mutex);
23+
pthread_create(&id2, NULL, t2, NULL);
24+
int maybe;
25+
if (maybe) {
26+
pthread_join(id2, NULL);
27+
}
28+
pthread_mutex_unlock(&mutex);
29+
return 0;
30+
}
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset
2+
#include <pthread.h>
3+
4+
int global = 0;
5+
pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
6+
pthread_t id1;
7+
8+
// both accesses are protected by same mutex **locked in same thread**
9+
10+
void *t1(void *arg) {
11+
global++; // RACE!
12+
return NULL;
13+
}
14+
15+
int main(void) {
16+
pthread_mutex_lock(&mutex);
17+
pthread_create(&id1, NULL, t1, NULL);
18+
global++; // RACE!
19+
pthread_join(id1, NULL);
20+
pthread_mutex_unlock(&mutex);
21+
return 0;
22+
}
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// PARAM: --set ana.activated[+] taintedCreationLockset --set ana.activated[+] threadJoins --set ana.activated[+] transitiveDescendants --set ana.activated[+] creationLockset
2+
#include <pthread.h>
3+
4+
int global = 0;
5+
pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
6+
pthread_t id1, id2;
7+
8+
// both accesses are protected by same mutex **locked in same thread**
9+
10+
void *tc(void *arg) {
11+
global++; // RACE!
12+
return NULL;
13+
}
14+
15+
int main(void) {
16+
pthread_mutex_lock(&mutex);
17+
pthread_create(&id1, NULL, tc, NULL);
18+
pthread_create(&id2, NULL, tc, NULL);
19+
pthread_join(id1, NULL);
20+
pthread_join(id2, NULL);
21+
pthread_mutex_unlock(&mutex);
22+
return 0;
23+
}

0 commit comments

Comments
 (0)