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

Commit df0d198

Browse files
hernanponcedeleonhernanponcedeleon
committed
fixed problems with loops and make it symmetric
1 parent 6498c2f commit df0d198

File tree

4 files changed

+152
-18
lines changed

4 files changed

+152
-18
lines changed

‎c/pthread-atomic/dekker.c‎

Lines changed: 38 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,20 +28,39 @@ void *thr1(void *_) {
2828
int f2 = flag2;
2929
__VERIFIER_atomic_end();
3030
while (f2 >= 1) {
31+
__VERIFIER_atomic_begin();
3132
int t = turn;
33+
__VERIFIER_atomic_end();
3234
if (t != 0) {
35+
__VERIFIER_atomic_begin();
3336
flag1 = 0;
37+
__VERIFIER_atomic_end();
38+
__VERIFIER_atomic_begin();
3439
t = turn;
35-
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();
3647
flag1 = 1;
48+
__VERIFIER_atomic_end();
3749
}
50+
__VERIFIER_atomic_begin();
51+
f2 = flag2;
52+
__VERIFIER_atomic_end();
3853
}
3954
// begin: critical section
4055
x = 0;
4156
assert(x<=0);
4257
// end: critical section
58+
__VERIFIER_atomic_begin();
4359
turn = 1;
60+
__VERIFIER_atomic_end();
61+
__VERIFIER_atomic_begin();
4462
flag1 = 0;
63+
__VERIFIER_atomic_end();
4564
return 0;
4665
}
4766

@@ -53,19 +72,36 @@ void *thr2(void *_) {
5372
int f1 = flag1;
5473
__VERIFIER_atomic_end();
5574
while (f1 >= 1) {
75+
__VERIFIER_atomic_begin();
5676
int t = turn;
77+
__VERIFIER_atomic_end();
5778
if (t != 1) {
79+
__VERIFIER_atomic_begin();
5880
flag2 = 0;
81+
__VERIFIER_atomic_end();
82+
__VERIFIER_atomic_begin();
5983
t = turn;
60-
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();
6191
flag2 = 1;
92+
__VERIFIER_atomic_end();
6293
}
94+
__VERIFIER_atomic_begin();
95+
f1 = flag1;
96+
__VERIFIER_atomic_end();
6397
}
6498
// begin: critical section
6599
x = 1;
66100
assert(x>=1);
67101
// end: critical section
102+
__VERIFIER_atomic_begin();
68103
turn = 1;
104+
__VERIFIER_atomic_end();
69105
__VERIFIER_atomic_begin();
70106
flag2 = 0;
71107
__VERIFIER_atomic_end();

‎c/pthread-atomic/lamport.c‎

Lines changed: 52 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,9 @@ 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();
@@ -29,8 +31,14 @@ void *thr1(void *_) {
2931
__VERIFIER_atomic_begin();
3032
b1 = 0;
3133
__VERIFIER_atomic_end();
34+
__VERIFIER_atomic_begin();
3235
y1 = y;
33-
while (y1 != 0) {};
36+
__VERIFIER_atomic_end();
37+
while (y1 != 0) {
38+
__VERIFIER_atomic_begin();
39+
y1 = y;
40+
__VERIFIER_atomic_end();
41+
};
3442
continue;
3543
}
3644
__VERIFIER_atomic_begin();
@@ -40,15 +48,29 @@ void *thr1(void *_) {
4048
int x1 = x;
4149
__VERIFIER_atomic_end();
4250
if (x1 != 1) {
51+
__VERIFIER_atomic_begin();
4352
b1 = 0;
53+
__VERIFIER_atomic_end();
4454
__VERIFIER_atomic_begin();
4555
int b21 = b2;
4656
__VERIFIER_atomic_end();
47-
while (b21 >= 1) {};
57+
while (b21 >= 1) {
58+
__VERIFIER_atomic_begin();
59+
b21 = b2;
60+
__VERIFIER_atomic_end();
61+
};
62+
__VERIFIER_atomic_begin();
4863
y1 = y;
64+
__VERIFIER_atomic_end();
4965
if (y1 != 1) {
66+
__VERIFIER_atomic_begin();
5067
y1 = y;
51-
while (y1 != 0) {};
68+
__VERIFIER_atomic_end();
69+
while (y1 != 0) {
70+
__VERIFIER_atomic_begin();
71+
y1 = y;
72+
__VERIFIER_atomic_end();
73+
};
5274
continue;
5375
}
5476
}
@@ -61,25 +83,35 @@ void *thr1(void *_) {
6183
__VERIFIER_atomic_begin();
6284
y = 0;
6385
__VERIFIER_atomic_end();
86+
__VERIFIER_atomic_begin();
6487
b1 = 0;
88+
__VERIFIER_atomic_end();
6589
return 0;
6690
}
6791

6892
void *thr2(void *_) {
6993
while (1) {
94+
__VERIFIER_atomic_begin();
7095
b2 = 1;
96+
__VERIFIER_atomic_end();
7197
__VERIFIER_atomic_begin();
7298
x = 2;
7399
__VERIFIER_atomic_end();
74100
__VERIFIER_atomic_begin();
75101
int y2 = y;
76102
__VERIFIER_atomic_end();
77103
if (y2 != 0) {
104+
__VERIFIER_atomic_begin();
78105
b2 = 0;
106+
__VERIFIER_atomic_end();
79107
__VERIFIER_atomic_begin();
80108
y2 = y;
81109
__VERIFIER_atomic_end();
82-
while (y2 != 0) {};
110+
while (y2 != 0) {
111+
__VERIFIER_atomic_begin();
112+
y2 = y;
113+
__VERIFIER_atomic_end();
114+
};
83115
continue;
84116
}
85117
__VERIFIER_atomic_begin();
@@ -89,15 +121,29 @@ void *thr2(void *_) {
89121
int x2 = x;
90122
__VERIFIER_atomic_end();
91123
if (x2 != 2) {
124+
__VERIFIER_atomic_begin();
92125
b2 = 0;
126+
__VERIFIER_atomic_end();
93127
__VERIFIER_atomic_begin();
94128
int b12 = b1;
95129
__VERIFIER_atomic_end();
96-
while (b12 >= 1) {};
130+
while (b12 >= 1) {
131+
__VERIFIER_atomic_begin();
132+
b12 = b1;
133+
__VERIFIER_atomic_end();
134+
};
135+
__VERIFIER_atomic_begin();
97136
y2 = y;
137+
__VERIFIER_atomic_end();
98138
if (y2 != 2) {
139+
__VERIFIER_atomic_begin();
99140
y2 = y;
100-
while (y2 != 0) {};
141+
__VERIFIER_atomic_end();
142+
while (y2 != 0) {
143+
__VERIFIER_atomic_begin();
144+
y2 = y;
145+
__VERIFIER_atomic_end();
146+
};
101147
continue;
102148
}
103149
}

‎c/pthread-atomic/peterson.c‎

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,14 @@ void *thr1(void *_) {
2929
__VERIFIER_atomic_begin();
3030
int t1 = turn;
3131
__VERIFIER_atomic_end();
32-
while (f21==1 && t1==1) {};
32+
while (f21==1 && t1==1) {
33+
__VERIFIER_atomic_begin();
34+
f21 = flag2;
35+
__VERIFIER_atomic_end();
36+
__VERIFIER_atomic_begin();
37+
t1 = turn;
38+
__VERIFIER_atomic_end();
39+
};
3340
// begin: critical section
3441
x = 0;
3542
assert(x<=0);
@@ -53,7 +60,14 @@ void *thr2(void *_) {
5360
__VERIFIER_atomic_begin();
5461
int t2 = turn;
5562
__VERIFIER_atomic_end();
56-
while (f12==1 && t2==0) {};
63+
while (f12==1 && t2==0) {
64+
__VERIFIER_atomic_begin();
65+
f12 = flag1;
66+
__VERIFIER_atomic_end();
67+
__VERIFIER_atomic_begin();
68+
t2 = turn;
69+
__VERIFIER_atomic_end();
70+
};
5771
// begin: critical section
5872
x = 1;
5973
assert(x>=1);

‎c/pthread-atomic/szymanski.c‎

Lines changed: 46 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,11 @@ void *thr1(void *_) {
2222
__VERIFIER_atomic_begin();
2323
int f21 = flag2;
2424
__VERIFIER_atomic_end();
25-
while (f21 >= 3);
25+
while (f21 >= 3) {
26+
__VERIFIER_atomic_begin();
27+
f21 = flag2;
28+
__VERIFIER_atomic_end();
29+
};
2630
__VERIFIER_atomic_begin();
2731
flag1 = 3;
2832
__VERIFIER_atomic_end();
@@ -36,22 +40,38 @@ void *thr1(void *_) {
3640
__VERIFIER_atomic_begin();
3741
f21 = flag2;
3842
__VERIFIER_atomic_end();
39-
while (f21 != 4);
43+
while (f21 != 4) {
44+
__VERIFIER_atomic_begin();
45+
f21 = flag2;
46+
__VERIFIER_atomic_end();
47+
};
4048
}
49+
__VERIFIER_atomic_begin();
4150
flag1 = 4;
51+
__VERIFIER_atomic_end();
4252
__VERIFIER_atomic_begin();
4353
f21 = flag2;
4454
__VERIFIER_atomic_end();
45-
while (f21 >= 2);
55+
while (f21 >= 2) {
56+
__VERIFIER_atomic_begin();
57+
f21 = flag2;
58+
__VERIFIER_atomic_end();
59+
};
4660
// begin critical section
4761
x = 0;
4862
assert(x<=0);
4963
// end critical section
5064
__VERIFIER_atomic_begin();
5165
f21 = flag2;
5266
__VERIFIER_atomic_end();
53-
while (2 <= f21 && f21 <= 3);
67+
while (2 <= f21 && f21 <= 3) {
68+
__VERIFIER_atomic_begin();
69+
f21 = flag2;
70+
__VERIFIER_atomic_end();
71+
};
72+
__VERIFIER_atomic_begin();
5473
flag1 = 0;
74+
__VERIFIER_atomic_end();
5575
return 0;
5676
}
5777

@@ -62,7 +82,11 @@ void *thr2(void *_) {
6282
__VERIFIER_atomic_begin();
6383
int f12 = flag1;
6484
__VERIFIER_atomic_end();
65-
while (f12 >= 3);
85+
while (f12 >= 3) {
86+
__VERIFIER_atomic_begin();
87+
f12 = flag1;
88+
__VERIFIER_atomic_end();
89+
};
6690
__VERIFIER_atomic_begin();
6791
flag2 = 3;
6892
__VERIFIER_atomic_end();
@@ -73,24 +97,38 @@ void *thr2(void *_) {
7397
__VERIFIER_atomic_begin();
7498
flag2 = 2;
7599
__VERIFIER_atomic_end();
100+
__VERIFIER_atomic_begin();
76101
f12 = flag1;
77-
while (f12 != 4);
102+
__VERIFIER_atomic_end();
103+
while (f12 != 4) {
104+
__VERIFIER_atomic_begin();
105+
f12 = flag1;
106+
__VERIFIER_atomic_end();
107+
};
78108
}
79109
__VERIFIER_atomic_begin();
80110
flag2 = 4;
81111
__VERIFIER_atomic_end();
82112
__VERIFIER_atomic_begin();
83113
f12 = flag1;
84114
__VERIFIER_atomic_end();
85-
while (f12 >= 2);
115+
while (f12 >= 2) {
116+
__VERIFIER_atomic_begin();
117+
f12 = flag1;
118+
__VERIFIER_atomic_end();
119+
};
86120
// begin critical section
87121
x = 1;
88122
assert(x>=1);
89123
// end critical section
90124
__VERIFIER_atomic_begin();
91125
f12 = flag1;
92126
__VERIFIER_atomic_end();
93-
while (2 <= f12 && f12 <= 3);
127+
while (2 <= f12 && f12 <= 3) {
128+
__VERIFIER_atomic_begin();
129+
f12 = flag1;
130+
__VERIFIER_atomic_end();
131+
};
94132
__VERIFIER_atomic_begin();
95133
flag2 = 0;
96134
__VERIFIER_atomic_end();

0 commit comments

Comments
 (0)