Spinroot

A forum for Spin users

You are not logged in.

#1 2015-09-28 14:42:44

Schachtschabel
Member
Registered: 2015-08-28
Posts: 15

SPIN: Problems with the multi-core mode

Greetings again,

while I was looking into the possibilities of using more than one CPU core for my model verification, I came across the following error which occurs every time when I use the following compilation options:

$ spin -a -o3 model
$ gcc -DNCORE=2 -DSEP_STATE -o pan pan.c
$ ./pan -a
shmget shared queues: Invalid argument
pan: check './pan --' for usage details

This happens every time on every model I try, be it one of my own (which could be flawed) but also on the examples from the PROMELA database (e.g. the one with the PLC Control Schedule) or even the little toy-examples within the SPIN directive. 

Maybe someone knows what I am doing wrong here; even after looking through the multicore-manual, I still can't find a flaw. in my commands.


So long,
Max

Offline

#2 2015-09-29 04:40:17

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

Re: SPIN: Problems with the multi-core mode

when i try this, it works correctly.
could be that you haven't configured shared memory correctly on your system
did you follow the guidance from ./pan -- (see the last line for a link to detailed
instructions for setting up shared memory of sufficient size etc.)
Also, give -DBFS_PAR a try -- it often works more easily

Offline

#3 2015-09-29 13:47:08

Schachtschabel
Member
Registered: 2015-08-28
Posts: 15

Re: SPIN: Problems with the multi-core mode

Yep, compiling with -DBFS_PAR gave me the hint to look at my shared memory, which was still set to 32MB.
Expanding the available memory as explained in the named link got it to run on my dualcore system. 

Now, I can see that two cores are running at 100% and each processor executes one ./pan process. But only the first core reports the current status of the verification (prints out depth, number of states, number of transistions etc.) and the time needed to reach the end of the run has not changed.

What exactly does the second core do when I compile the model with -DNCORE=2 -DSEP_STATE?

Edit: When I abort the verification run on two cores, the second one prints out 0 for states, depth, transitions etc. So, aside from being on full load, there seem to be no calculations happening on the second core. Is this the correct behaviour?

Edit2: The BFS really does work quite good, I was able to run SPIN until the state space filled up all the shared memory space in a few minutes. I guess I will be using this option for now and see how far I can get this way.


So long,
Max

Last edited by Schachtschabel (2015-09-29 16:13:19)

Offline

#4 2015-09-30 04:21:35

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

Re: SPIN: Problems with the multi-core mode

if you do a search for safety properties, with -DNCORE=2, the two cores share the load evenly.
if a search for liveness properties, the 2nd core only does the nested part of the nested dfs, so depending on
the type of model you are verifying, it may end up doing no work at all (e.g., if there are no accept states at all)

Offline

Board footer

Powered by FluxBB