Spinroot

A forum for Spin users

You are not logged in.

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

Dharma
Member
Registered: 2011-09-21
Posts: 13

race condition issue in C program

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;
}

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: race condition issue in C program

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

Offline

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

Dharma
Member
Registered: 2011-09-21
Posts: 13

Re: race condition issue in C program

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

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: race condition issue in C program

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.

Offline

Board footer

Powered by FluxBB