Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2014-02-12 07:24:21
- srirajpaul
- Member
- Registered: 2013-09-07
- Posts: 13
Using LTL with multicore, only one CPU getting used
Hi,
I am trying to verify a model using LTLs with multicore options. But when I execute, it only runs on one CPU(CPU 0). Other CPUs show everything as zero. Output of one sample run is as follows.
e.g:
0: Claim morton_order1 (3), from state 6
cpu1: Depth= 0 States= 0 Transitions= 0 Memory= 0.000 t= 185 R= 0
cpu0: Depth= 4329 States= 4.97e+05 Transitions= 9.98e+05 Memory= 251.567 t= 185 R= 3e+03
But the documentation tells it can run on dual core[1]. I am using Spin version 6.2.5.
I complied using options "gcc -DVECTORSZ=64000 -DBITSTATE -DSEP_STATE -DNCORE=2 -DFULL_TRAIL -DVMAX=35000 "
and ran using the options "./a.out -a -w20".
Is there something I am doing wrong that makes it run on only one core?
Also all my LTL's are 'always' properties([]). My assumption was that liveness properties are the ones that come with 'eventually' operator(<>) and safety properties are the one with 'always' operator([]).
Is it true that if we use only 'always' properties we can use N cores and when we use 'eventually' operator it needs to restricted to 2 cores?
Thank you
Sriraj
[1]:http://www.spinroot.com/spin/multicore/V5_Readme.html
Offline
#3 2014-02-15 05:43:11
- srirajpaul
- Member
- Registered: 2013-09-07
- Posts: 13
Re: Using LTL with multicore, only one CPU getting used
The model is put at http://srp7.web.rice.edu/new_pe.pml
I tried with the -DBFS_PAR option. It is running in parallel. But irrespective of what is specified using -DNCORE, it always uses n-1 cores, where n is the number of cores in the machine.
Also since it is using BFS, the depth explored is very short. The depth reached usually goes to around 4000 when I run it in the normal DFS way. Since the state space is too large, I am using -DBITSTATE also.
I ran it as:
spin -a new_pe.pml
gcc -DVECTORSZ=64000 -DBITSTATE -DSEP_STATE -DNCORE=2 -DFULL_TRAIL -DVMAX=35000 pan.c
./a.out -a -w20 -Nmorton_order1
In this link [1], the "Liveness Verification" section tells "Using a larger number of cores than 2 is not useful with the exisiting implementation". Does that mean when LTL is used we can use only 2 cores?
[1]: http://www.spinroot.com/spin/multicore/V5_Readme.html
Offline
#4 2014-02-15 06:14:30
Re: Using LTL with multicore, only one CPU getting used
that is correct -- with DFS we can only use 2 core: 1 for the 1st dfs and 1 for the nested search.
with BFS_PAR you can use more cores -- you define it with the -u argument, but it defaults to n-1 if you have n cores
(e.g., you'd say: ./pan -u5 ....otheroptions.... to use 5 cores instead of n-1
Offline
#5 2014-02-16 20:58:07
Re: Using LTL with multicore, only one CPU getting used
the original run not using cpu1 just means that in the approximate bitstate search it didn't yet encounter an accepting state from which it could initiate the nested part of the search. you have a large model and lots of ltl properties to handle.
maybe a straight single core dfs will perform the best in this case.
Offline