A forum for Spin users
You are not logged in.
Pages: 1
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
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
Pages: 1