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

Commit 25d9487

Browse files
authored
Merge pull request #1216 from hernanponcedeleon/master
Restore original benchmark semantics
2 parents 63aba0a + 3903c2a commit 25d9487

File tree

4 files changed

+16
-4
lines changed

4 files changed

+16
-4
lines changed

c/ldv-races/race-2_2-container_of.c

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

c/ldv-races/race-2_2-container_of.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/ldv-races/race-2_5-container_of.c

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,10 @@ void *my_callback(void *arg) {
4444
data->shared.a = 1;
4545
__VERIFIER_atomic_end();
4646
__VERIFIER_atomic_begin();
47-
data->shared.b = data->shared.b + 1;
47+
int lb = data->shared.b;
48+
__VERIFIER_atomic_end();
49+
__VERIFIER_atomic_begin();
50+
data->shared.b = lb + 1;
4851
__VERIFIER_atomic_end();
4952
pthread_mutex_unlock (&data->lock);
5053
return 0;

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

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

0 commit comments

Comments
 (0)