Spinroot

Hi,
I'm trying the following C program but Modex is complaining.

    Extract Model:
    ==============
modex prod_cons_two_signals.c
MODEX Version 2.7 - 1 January 2015
created: model and _modex_.run

    Compile and Run:
    ================
sh _modex_.run
spin: model:66, Error: undeclared variable: get    saw ''(' = 40'
---

The following C program uses get() and put(int). They both are externally defined in another file. I put %O put_get.o in my prx file. That's the only thing in my prx file.

/* 1 producer; 2 consumers; two signals (fill, empty) */

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

pthread_mutex_t mutex;
pthread_cond_t empty;
pthread_cond_t fill;

extern int count;
extern int get();
extern void put(int);

void *producer(void *arg) {
   int i;
   while(1) {
      pthread_mutex_lock(&mutex);
      while (count == 1)
        pthread_cond_wait(&empty, &mutex);
      put(i);
      pthread_cond_signal(&fill);
      pthread_mutex_unlock(&mutex);
   }
}

void *consumer(void *arg) {
    int i;
    while(1) {
       pthread_mutex_lock(&mutex);
       while(count == 0)
         pthread_cond_wait(&fill, &mutex);
       int tmp = get();
       pthread_cond_signal(&empty);
       pthread_mutex_unlock(&mutex);
    }
}

void main()
{
   pthread_t t1, t2, t3;
   pthread_mutex_init(&mutex, NULL);
   pthread_cond_init(&fill, NULL);
   pthread_cond_init(&empty, NULL);

   pthread_create(&t1, NULL, producer, NULL);
   pthread_create(&t2, NULL, consumer, NULL);
   pthread_create(&t3, NULL, consumer, NULL);

   pthread_join(t1, NULL);
   pthread_join(t2, NULL);
   pthread_join(t3, NULL);
}

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

Hi,
I'm using the latest version of modex - downloaded it two weeks ago.

When I ran verify 4_mutex.c, which is part of the modex/example, it says no error was found.

However, when I ran ./pan it does show the violation of  an assertion.

dharma@ubuntu:~/Downloads/modex/Examples$ verify 4_mutex.c

    Extract Model:
    ==============
modex 4_mutex.c
MODEX Version 2.7 - 1 January 2015
created: model and _modex_.run

    Compile and Run:
    ================
sh _modex_.run
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan: out of memory
    662568 bytes used
    4.29497e+09 bytes more needed
    1.57286e+10 bytes limit
hint: to reduce memory, recompile with
  -DBITSTATE # supertrace, approximation

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Partial Order Reduction

Hash-Compact 4 search for:
    never claim             - (none specified)
    assertion violations    +
    acceptance   cycles     - (not selected)
    invalid end states    +

State-vector 179 byte, depth reached 0, errors: 0
        0 states, stored
        0 states, matched
        0 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000    equivalent memory usage for states (stored*(State-vector + overhead))
    0.000    actual memory usage for states (less than 1k)
4096.000    memory used for hash table (-w29)
    0.534    memory used for DFS stack (-m10000)
    0.632    total actual memory usage

pan: elapsed time 1.73e+07 seconds
pan: rate         0 states/second

No Errors Found
----

dharma@ubuntu:~/Downloads/modex/Examples$ ./pan
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan:1: c_code line 103 precondition false: (now.cnt==1) (at depth 59)
pan: wrote model.trail

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Partial Order Reduction

Hash-Compact 4 search for:
    never claim             - (none specified)
    assertion violations    +
    acceptance   cycles     - (not selected)
    invalid end states    +

State-vector 260 byte, depth reached 100, errors: 1
     3643 states, stored
     2442 states, matched
     6085 transitions (= stored+matched)
     1012 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    1.001    equivalent memory usage for states (stored*(State-vector + overhead))
    0.373    actual memory usage for states (compression: 37.27%)
             state-vector as stored = 79 byte + 28 byte overhead
  128.000    memory used for hash table (-w24)
    0.534    memory used for DFS stack (-m10000)
  128.827    total actual memory usage

pan: elapsed time 0.07 seconds
pan: rate 52042.857 states/second

Hi,

Tried spin on the model given below. It reported a violation of the assertion. Is there a way to see the actual interleaving that led to this violation?

        byte n = 0, finish = 0;

        active [2] proctype P() {
          byte register, counter = 0;
          do :: counter = 10 -> break
              :: else ->
                     register = n;
                     register++;
                     n = register;
                     counter++
          od;
          finish++
        }

        active proctype WaitForFinish() {
          finish == 2;
          assert (n > 0);
        }

Tried spin -s -t primer.pml and got this output. It appears n = 0. But not clear to me what interleaving has led to this failure. Any comments? Thank a lot.

-----
spin: primer.pml:17, Error: assertion violated
spin: text of failed assertion: assert((n>0))
spin: trail ends after 6 steps
#processes: 3
        n = 0
        finish = 2
  6:    proc  2 (WaitForFinish) primer.pml:18 (state 3) <valid end state>
  6:    proc  1 (P) primer.pml:13 (state 12) <valid end state>
  6:    proc  0 (P) primer.pml:13 (state 12) <valid end state>
3 processes created

---