Skip to content
This repository was archived by the owner on Oct 3, 2021. It is now read-only.

Commit 5ba49e7

Browse files
dbeyerdbeyer
authored
Merge pull request #1177 from hernanponcedeleon/races
Solved Data-Races
2 parents e32d8d6 + bf93949 commit 5ba49e7

27 files changed

+552
-846
lines changed

‎c/ldv-races/race-2_5-container_of.c‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,8 +40,12 @@ void *my_callback(void *arg) {
4040
data = container_of(dev, struct my_data, dev);
4141

4242
pthread_mutex_lock (&data->lock);
43+
__VERIFIER_atomic_begin();
4344
data->shared.a = 1;
45+
__VERIFIER_atomic_end();
46+
__VERIFIER_atomic_begin();
4447
data->shared.b = data->shared.b + 1;
48+
__VERIFIER_atomic_end();
4549
pthread_mutex_unlock (&data->lock);
4650
return 0;
4751
}

‎c/ldv-races/race-2_5-container_of.i‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1690,8 +1690,12 @@ void *my_callback(void *arg) {
16901690
struct my_data *data;
16911691
data = ({ const typeof( ((struct my_data *)0)->dev ) *__mptr = (dev); (struct my_data *)( (char *)__mptr - ((unsigned long) &((struct my_data *)0)->dev) );});
16921692
pthread_mutex_lock (&data->lock);
1693+
__VERIFIER_atomic_begin();
16931694
data->shared.a = 1;
1695+
__VERIFIER_atomic_end();
1696+
__VERIFIER_atomic_begin();
16941697
data->shared.b = data->shared.b + 1;
1698+
__VERIFIER_atomic_end();
16951699
pthread_mutex_unlock (&data->lock);
16961700
return 0;
16971701
}

‎c/ldv-races/race-3_2-container_of-global.c‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,10 @@ void *my_callback(void *arg) {
4646
data->shared.a = 1;
4747
__VERIFIER_atomic_end();
4848
__VERIFIER_atomic_begin();
49-
data->shared.b = data->shared.b + 1;
49+
int lb = data->shared.b;
50+
__VERIFIER_atomic_end();
51+
__VERIFIER_atomic_begin();
52+
data->shared.b = lb + 1;
5053
__VERIFIER_atomic_end();
5154
//pthread_mutex_unlock (&data->lock);
5255
return 0;

‎c/ldv-races/race-3_2-container_of-global.i‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1693,7 +1693,10 @@ void *my_callback(void *arg) {
16931693
data->shared.a = 1;
16941694
__VERIFIER_atomic_end();
16951695
__VERIFIER_atomic_begin();
1696-
data->shared.b = data->shared.b + 1;
1696+
int lb = data->shared.b;
1697+
__VERIFIER_atomic_end();
1698+
__VERIFIER_atomic_begin();
1699+
data->shared.b = lb + 1;
16971700
__VERIFIER_atomic_end();
16981701
return 0;
16991702
}

‎c/pthread-atomic/dekker.c‎

Lines changed: 44 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,45 +24,87 @@ void *thr1(void *_) {
2424
__VERIFIER_atomic_begin();
2525
flag1 = 1;
2626
__VERIFIER_atomic_end();
27+
__VERIFIER_atomic_begin();
2728
int f2 = flag2;
29+
__VERIFIER_atomic_end();
2830
while (f2 >= 1) {
31+
__VERIFIER_atomic_begin();
2932
int t = turn;
33+
__VERIFIER_atomic_end();
3034
if (t != 0) {
35+
__VERIFIER_atomic_begin();
3136
flag1 = 0;
37+
__VERIFIER_atomic_end();
38+
__VERIFIER_atomic_begin();
3239
t = turn;
33-
while (t != 0) {};
40+
__VERIFIER_atomic_end();
41+
while (t != 0) {
42+
__VERIFIER_atomic_begin();
43+
t = turn;
44+
__VERIFIER_atomic_end();
45+
};
46+
__VERIFIER_atomic_begin();
3447
flag1 = 1;
48+
__VERIFIER_atomic_end();
3549
}
50+
__VERIFIER_atomic_begin();
51+
f2 = flag2;
52+
__VERIFIER_atomic_end();
3653
}
3754
// begin: critical section
3855
x = 0;
3956
assert(x<=0);
4057
// end: critical section
58+
__VERIFIER_atomic_begin();
4159
turn = 1;
60+
__VERIFIER_atomic_end();
61+
__VERIFIER_atomic_begin();
4262
flag1 = 0;
63+
__VERIFIER_atomic_end();
4364
return 0;
4465
}
4566

4667
void *thr2(void *_) {
68+
__VERIFIER_atomic_begin();
4769
flag2 = 1;
70+
__VERIFIER_atomic_end();
4871
__VERIFIER_atomic_begin();
4972
int f1 = flag1;
5073
__VERIFIER_atomic_end();
5174
while (f1 >= 1) {
75+
__VERIFIER_atomic_begin();
5276
int t = turn;
77+
__VERIFIER_atomic_end();
5378
if (t != 1) {
79+
__VERIFIER_atomic_begin();
5480
flag2 = 0;
81+
__VERIFIER_atomic_end();
82+
__VERIFIER_atomic_begin();
5583
t = turn;
56-
while (t != 1) {};
84+
__VERIFIER_atomic_end();
85+
while (t != 1) {
86+
__VERIFIER_atomic_begin();
87+
t = turn;
88+
__VERIFIER_atomic_end();
89+
};
90+
__VERIFIER_atomic_begin();
5791
flag2 = 1;
92+
__VERIFIER_atomic_end();
5893
}
94+
__VERIFIER_atomic_begin();
95+
f1 = flag1;
96+
__VERIFIER_atomic_end();
5997
}
6098
// begin: critical section
6199
x = 1;
62100
assert(x>=1);
63101
// end: critical section
102+
__VERIFIER_atomic_begin();
64103
turn = 1;
104+
__VERIFIER_atomic_end();
105+
__VERIFIER_atomic_begin();
65106
flag2 = 0;
107+
__VERIFIER_atomic_end();
66108
return 0;
67109
}
68110

‎c/pthread-atomic/dekker.i‎

Lines changed: 44 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -708,40 +708,82 @@ void *thr1(void *_) {
708708
__VERIFIER_atomic_begin();
709709
flag1 = 1;
710710
__VERIFIER_atomic_end();
711+
__VERIFIER_atomic_begin();
711712
int f2 = flag2;
713+
__VERIFIER_atomic_end();
712714
while (f2 >= 1) {
715+
__VERIFIER_atomic_begin();
713716
int t = turn;
717+
__VERIFIER_atomic_end();
714718
if (t != 0) {
719+
__VERIFIER_atomic_begin();
715720
flag1 = 0;
721+
__VERIFIER_atomic_end();
722+
__VERIFIER_atomic_begin();
716723
t = turn;
717-
while (t != 0) {};
724+
__VERIFIER_atomic_end();
725+
while (t != 0) {
726+
__VERIFIER_atomic_begin();
727+
t = turn;
728+
__VERIFIER_atomic_end();
729+
};
730+
__VERIFIER_atomic_begin();
718731
flag1 = 1;
732+
__VERIFIER_atomic_end();
719733
}
734+
__VERIFIER_atomic_begin();
735+
f2 = flag2;
736+
__VERIFIER_atomic_end();
720737
}
721738
x = 0;
722739
if (!(x<=0)) ERROR: reach_error();
740+
__VERIFIER_atomic_begin();
723741
turn = 1;
742+
__VERIFIER_atomic_end();
743+
__VERIFIER_atomic_begin();
724744
flag1 = 0;
745+
__VERIFIER_atomic_end();
725746
return 0;
726747
}
727748
void *thr2(void *_) {
749+
__VERIFIER_atomic_begin();
728750
flag2 = 1;
751+
__VERIFIER_atomic_end();
729752
__VERIFIER_atomic_begin();
730753
int f1 = flag1;
731754
__VERIFIER_atomic_end();
732755
while (f1 >= 1) {
756+
__VERIFIER_atomic_begin();
733757
int t = turn;
758+
__VERIFIER_atomic_end();
734759
if (t != 1) {
760+
__VERIFIER_atomic_begin();
735761
flag2 = 0;
762+
__VERIFIER_atomic_end();
763+
__VERIFIER_atomic_begin();
736764
t = turn;
737-
while (t != 1) {};
765+
__VERIFIER_atomic_end();
766+
while (t != 1) {
767+
__VERIFIER_atomic_begin();
768+
t = turn;
769+
__VERIFIER_atomic_end();
770+
};
771+
__VERIFIER_atomic_begin();
738772
flag2 = 1;
773+
__VERIFIER_atomic_end();
739774
}
775+
__VERIFIER_atomic_begin();
776+
f1 = flag1;
777+
__VERIFIER_atomic_end();
740778
}
741779
x = 1;
742780
if (!(x>=1)) ERROR: reach_error();
781+
__VERIFIER_atomic_begin();
743782
turn = 1;
783+
__VERIFIER_atomic_end();
784+
__VERIFIER_atomic_begin();
744785
flag2 = 0;
786+
__VERIFIER_atomic_end();
745787
return 0;
746788
}
747789
int main() {

‎c/pthread-atomic/lamport.c‎

Lines changed: 66 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,31 +18,59 @@ int X; // boolean variable to test mutual exclusion
1818

1919
void *thr1(void *_) {
2020
while (1) {
21+
__VERIFIER_atomic_begin();
2122
b1 = 1;
23+
__VERIFIER_atomic_end();
2224
__VERIFIER_atomic_begin();
2325
x = 1;
2426
__VERIFIER_atomic_end();
27+
__VERIFIER_atomic_begin();
2528
int y1 = y;
29+
__VERIFIER_atomic_end();
2630
if (y1 != 0) {
2731
__VERIFIER_atomic_begin();
2832
b1 = 0;
2933
__VERIFIER_atomic_end();
34+
__VERIFIER_atomic_begin();
3035
y1 = y;
31-
while (y != 0) {};
36+
__VERIFIER_atomic_end();
37+
while (y1 != 0) {
38+
__VERIFIER_atomic_begin();
39+
y1 = y;
40+
__VERIFIER_atomic_end();
41+
};
3242
continue;
3343
}
3444
__VERIFIER_atomic_begin();
3545
y = 1;
3646
__VERIFIER_atomic_end();
47+
__VERIFIER_atomic_begin();
3748
int x1 = x;
49+
__VERIFIER_atomic_end();
3850
if (x1 != 1) {
51+
__VERIFIER_atomic_begin();
3952
b1 = 0;
53+
__VERIFIER_atomic_end();
54+
__VERIFIER_atomic_begin();
4055
int b21 = b2;
41-
while (b21 >= 1) {};
56+
__VERIFIER_atomic_end();
57+
while (b21 >= 1) {
58+
__VERIFIER_atomic_begin();
59+
b21 = b2;
60+
__VERIFIER_atomic_end();
61+
};
62+
__VERIFIER_atomic_begin();
4263
y1 = y;
64+
__VERIFIER_atomic_end();
4365
if (y1 != 1) {
66+
__VERIFIER_atomic_begin();
4467
y1 = y;
45-
while (y1 != 0) {};
68+
__VERIFIER_atomic_end();
69+
while (y1 != 0) {
70+
__VERIFIER_atomic_begin();
71+
y1 = y;
72+
__VERIFIER_atomic_end();
73+
};
4674
continue;
4775
}
4876
}
@@ -55,21 +83,35 @@ void *thr1(void *_) {
5583
__VERIFIER_atomic_begin();
5684
y = 0;
5785
__VERIFIER_atomic_end();
86+
__VERIFIER_atomic_begin();
5887
b1 = 0;
88+
__VERIFIER_atomic_end();
5989
return 0;
6090
}
6191

6292
void *thr2(void *_) {
6393
while (1) {
94+
__VERIFIER_atomic_begin();
6495
b2 = 1;
96+
__VERIFIER_atomic_end();
97+
__VERIFIER_atomic_begin();
6598
x = 2;
99+
__VERIFIER_atomic_end();
100+
__VERIFIER_atomic_begin();
66101
int y2 = y;
102+
__VERIFIER_atomic_end();
67103
if (y2 != 0) {
104+
__VERIFIER_atomic_begin();
68105
b2 = 0;
106+
__VERIFIER_atomic_end();
69107
__VERIFIER_atomic_begin();
70108
y2 = y;
71109
__VERIFIER_atomic_end();
72-
while (y2 != 0) {};
110+
while (y2 != 0) {
111+
__VERIFIER_atomic_begin();
112+
y2 = y;
113+
__VERIFIER_atomic_end();
114+
};
73115
continue;
74116
}
75117
__VERIFIER_atomic_begin();
@@ -79,15 +121,29 @@ void *thr2(void *_) {
79121
int x2 = x;
80122
__VERIFIER_atomic_end();
81123
if (x2 != 2) {
124+
__VERIFIER_atomic_begin();
82125
b2 = 0;
126+
__VERIFIER_atomic_end();
83127
__VERIFIER_atomic_begin();
84128
int b12 = b1;
85129
__VERIFIER_atomic_end();
86-
while (b12 >= 1) {};
130+
while (b12 >= 1) {
131+
__VERIFIER_atomic_begin();
132+
b12 = b1;
133+
__VERIFIER_atomic_end();
134+
};
135+
__VERIFIER_atomic_begin();
87136
y2 = y;
137+
__VERIFIER_atomic_end();
88138
if (y2 != 2) {
139+
__VERIFIER_atomic_begin();
89140
y2 = y;
90-
while (y2 != 0) {};
141+
__VERIFIER_atomic_end();
142+
while (y2 != 0) {
143+
__VERIFIER_atomic_begin();
144+
y2 = y;
145+
__VERIFIER_atomic_end();
146+
};
91147
continue;
92148
}
93149
}
@@ -97,8 +153,12 @@ void *thr2(void *_) {
97153
X = 1;
98154
assert(X >= 1);
99155
// end: critical section
156+
__VERIFIER_atomic_begin();
100157
y = 0;
158+
__VERIFIER_atomic_end();
159+
__VERIFIER_atomic_begin();
101160
b2 = 0;
161+
__VERIFIER_atomic_end();
102162
return 0;
103163
}
104164

0 commit comments

Comments
 (0)