Spinroot

A forum for Spin users

You are not logged in.

#1 2015-01-22 21:34:35

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

unreached in proctype...

Hi,

I tried the following C program without any .prx file. The tool showed the following output:

unreached in proctype p_thread1
    model:49, state 23, "-end-"
    (1 of 23 states)
unreached in proctype p_thread2
    model:71, state 23, "-end-"
    (1 of 23 states)
unreached in proctype p_main
    (0 of 23 states)

--
Could you please explain the reason for unreached in these processes?

There are two threads: One for increment and another for decrement of a global variable.


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

// verify 3_threads_new.c

int shared = 0;
pthread_mutex_t mutex;

void *
thread1(void *arg)
{       int tmp;

        pthread_mutex_lock( &mutex );
        tmp = shared;
        tmp++;
        shared = tmp;
        pthread_mutex_unlock( &mutex );

        return 0;
}

void *
thread2(void *arg)
{       int tmp;

         pthread_mutex_lock(&mutex);
         tmp = shared;
         tmp--;
         shared = tmp;
         pthread_mutex_unlock(&mutex);

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

        return 0;
}

Offline

#2 2015-01-23 23:45:49

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

Re: unreached in proctype...

it's an artifact of how the spin model is constructed.
all functions (other than main) are modeled as 'server processes'
that wait for calls to be made (typically that is a pthread_create)
so these server processes handle a single call at a time
and then start back at the start to handle the next call: they never terminate.
you can use an option to allow the model to handle multiple
calls in parallel as well (using the -N parameter)

Offline

Board footer

Powered by FluxBB