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

Commit c5e88d3

Browse files
restored original semantics of the program
1 parent 63aba0a commit c5e88d3

File tree

2 files changed

+8
-2
lines changed

2 files changed

+8
-2
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_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;

0 commit comments

Comments
 (0)