race condition issue in C program

Dharma · 2015-01-23 02:39:51

Hi,

I'm playing with Modex to better understand it.

For the following C program, I have two threads: one for increment and another for decrement of a global variable.

I think the global variable "shared" can take the value -1 as well. That is, the assert below is incorrect but Modex is not reporting it.

I wonder whether Modex treats each C statement as an atomic statement. The problem is that, as you know, shared=shared+1 or shared++ is made of multiple instructions at the assembly level. Thus, race condition is possible here.

Could you please share your thoughts?

#include <pthread.h>
#include <assert.h>

// verify race.c

int shared = 0;
pthread_mutex_t mutex;

void *
thread1(void *arg)
{
shared++;
return 0;
}

void *
thread2(void *arg)
{
shared--;
return 0;
}

int
main(void)
{
pthread_t t[2];
pthread_mutex_init(&mutex, 0);

pthread_create(&t[0], 0, thread1, 0);
pthread_create(&t[1], 0, thread2, 0);

pthread_join(t[0], 0);
pthread_join(t[1], 0);

assert(shared == 1 || shared == 0); /* Modex agrees to this - but shared can be -1, too */

return 0;
}

spinroot · 2015-01-23 23:43:09

because you're waiting for both threads to terminate before checking the assertion,
shared cannot be negative -- it can only be zero actually

Dharma · 2015-01-24 01:17:35

Hi,
Thanks. No, the shared variable can also be -1.

The problem I think is possibly in the interpretation of shared-- (or shared++) as one atomic entity. I may be wrong, of course.

I disassembled it for our discussion on a 64 bit VM.

shared++ is from instruction starting at 8 until 16.

0000000000000000 <thread1>:
0: 55    push %rbp
1: 48 89 e5    mov %rsp,%rbp
4: 48 89 7d f8 mov %rdi,-0x8(%rbp)
8: 8b 05 00 00 00 00 mov 0x0(%rip),%eax # e <thread1+0xe>
e: 83 c0 01    add $0x1,%eax
11: 89 05 00 00 00 00 mov %eax,0x0(%rip) # 17 <thread1+0x17>
17: b8 00 00 00 00    mov $0x0,%eax
1c: 5d    pop %rbp
1d: c3    retq

shared-- is from instruction starting at 26 until 34.

000000000000001e <thread2>:
1e: 55    push %rbp
1f: 48 89 e5    mov %rsp,%rbp
22: 48 89 7d f8 mov %rdi,-0x8(%rbp)
26: 8b 05 00 00 00 00 mov 0x0(%rip),%eax # 2c <thread2+0xe>
2c: 83 e8 01    sub $0x1,%eax
2f: 89 05 00 00 00 00 mov %eax,0x0(%rip) # 35 <thread2+0x17>
35: b8 00 00 00 00    mov $0x0,%eax
3a: 5d    pop %rbp
3b: c3    retq

What if the second thread 2 ran first and read the shared variable into its register, say eax. Now the eax register has just 0.

Assume context switch happens to thread 1, which also read shared variable's value 0 into its copy of register eax. Assume thread 1 finished the job, now shared is 1.

Assume now thread 2 runs, it will decrement its own copy of the eax register, from 0 to -1. Now -1 will be copied back to shared.

Just out of curiosity, I ran the divine model checker and it agrees that there is a possibility of shared to be -1. I did not make any effort in understanding the long trace they generated.

You may also try: http://divine.fi.muni.cz/try.cgi

spinroot · 2015-01-24 01:30:36

true -- at instruction level this is possible,
the spin model captures the increment and decrements as atomic statements though.
you could get to the register level granularity by explicitly introducing a temporary
register variable into the C code
Modex isn't the right tool for capture race conditions at the finest granularity.
(That's rarely where problems are in multi-threaded code; although it's always possilbe of course.)
Another thing we typically abstract from is out-of-order load and store behavior.
The complexity of verification increases more and more the more low-level detail you try
to include in the models. Always a bit of a trade-off.

Spinroot

#1 2015-01-23 02:39:51

race condition issue in C program

#2 2015-01-23 23:43:09

Re: race condition issue in C program

#3 2015-01-24 01:17:35

Re: race condition issue in C program

#4 2015-01-24 01:30:36

Re: race condition issue in C program

Board footer