Spinroot

A forum for Spin users

You are not logged in.

#1 2015-04-17 00:59:32

haozheng
Member
Registered: 2013-12-16
Posts: 8

Excessive memory usage with bitstate hashing

Hi, I used bitstate hashing for a NoC project I am working on with the impression that bitstate hashing is fast and covers more states within a fixed memory limit. But the results show me the opposite story. I used the following commands to compile and run the model.
spin -a 3_csv.pml
gcc -O2 -DSAFETY -DBITSTATE -o pan pan.c
./pan -w32 -k4 -m10000000

The results are shown below.

Depth= 1023340 States=    1e+06 Transitions= 1.05e+06 Memory=  1690.223    t=     2.84 R=   4e+05
Depth= 2046488 States=    2e+06 Transitions=  2.1e+06 Memory=  2257.996    t=     6.06 R=   3e+05
Depth= 3069635 States=    3e+06 Transitions= 3.15e+06 Memory=  2825.770    t=     9.32 R=   3e+05
Depth= 4092784 States=    4e+06 Transitions=  4.2e+06 Memory=  3393.543    t=     14.1 R=   3e+05
^CInterrupted

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

Bit statespace search for:
    never claim             - (none specified)
    assertion violations    +
    cycle checks           - (disabled by -DSAFETY)
    invalid end states    +

State-vector 572 byte, depth reached 4206042, errors: 0
  4110696 states, stored
   209444 states, matched
  4320140 transitions (= stored+matched)
    95379 atomic steps

hash factor: 1044.83 (best if > 100.)

bits set per state: 4 (-k4)

Stats on memory usage (in Megabytes):
2320.797    equivalent memory usage for states (stored*(State-vector + overhead))
  512.000    memory used for hash array (-w32)
   76.294    memory used for bit stack
  534.058    memory used for DFS stack (-m10000000)
2331.365    other (proc and chan stacks)
    2.717    memory lost to fragmentation
3456.434    total actual memory usage


It is strange to find out that much less memory is used when the model is compile with -DCOLLAPSE instead.

I would highly appreciate if comments can be given to explain this phenomenon. The above run was done on a Macbook Air with 4GB memory.


Thank you very much.

Hao

Offline

#2 2015-04-17 05:16:16

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

Re: Excessive memory usage with bitstate hashing

do you mean that if both runs are allowed to run to completion,
the bitstate searches ended up using more memory than the search with -DCOLLAPSE?
that would be strange indeed
can you send me the model so that I can find out what is happening?

Offline

#3 2015-04-17 16:59:14

haozheng
Member
Registered: 2013-12-16
Posts: 8

Re: Excessive memory usage with bitstate hashing

In fact, I had to kill the processes using -DCOLLAPSE and -DBITSTATE after they reach about 4e+06 states.  So my question should be phrased more precisely like this: why the memory used with bitstate hashing grows more quickly than that with -DCOLLAPSE?  Suppose that there are only 4GB memory. Then bitstate hashing can actually search less states.  This is what confuses me.

The .pml model is attached.

Thank you for your help.

- Hao

==========================================
/* 3_csv.pml */

#define N 3

chan E_chan[(N*N)] = [1] of {byte};
chan W_chan[(N*N)] = [1] of {byte};
chan N_chan[(N*N)] = [1] of {byte};
chan S_chan[(N*N)] = [1] of {byte};
byte Recevier[N*N];
int Success;
byte Rand_x,Rand_y;

proctype Process(byte x,y)
{
byte Dx,Dy,Dest_Id;
bool is_message,msg_send;
byte fault;
byte Cx=x,Cy=y;
byte Id,rN,rS,rE,rW,s;
Id=(x*N)+y;
rN=((x+1)*N)+y;
rS=((x-1)*N)+y;
rE=(x*N)+y+1;
rW=(x*N)+y-1;
start:
s=Success;
is_message=false;
msg_send=false;
loop:
atomic{
if
    ::(Rand_x<=N-2) -> Rand_x++;
    ::(Rand_x<=N-1) -> Rand_x=0;
    ::(Rand_y<=N-2) -> Rand_y++;
    ::(Rand_y==N-1) -> Rand_y=0;
fi}
assert(Rand_x<N)
assert(Rand_y<N)
if
    ::atomic{Recevier[Id]==0 ->if
                        ::((Rand_x!=x)&&(Rand_y!=y)) -> Dest_Id=(Rand_x*N)+Rand_y;is_message=true;
                        ::else-> skip;
                   fi}
    ::Recevier[Id]>=0 ->if
          ::(x==0) -> if
                ::(y==0) -> do
                        ::     empty(S_chan[rN]) -> break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;
                        ::     atomic{W_chan[rE]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                ::(y==(N-1)) -> do
                        ::     empty(S_chan[rN]) -> break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break
                        od
                ::else ->   do   
                        ::     empty(S_chan[rN]) -> break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;   if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;
                        ::     atomic{W_chan[rE]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                 fi
          ::(x==(N-1)) ->if
                ::(y==0) -> do
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;
                        ::     atomic{W_chan[rE]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                ::(y==(N-1)) -> do
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;   
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                ::else ->   do   
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;
                        ::     atomic{W_chan[rE]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                fi
          ::else -> if
                ::(y==0) -> ;do
                        ::     empty(S_chan[rN]) -> break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;printf("i'm waiting,.....\n");
                        ::     atomic{W_chan[rE]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                ::(y==(N-1)) ->; do   
                        ::     empty(S_chan[rN]) -> break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        od
                ::else ->   do   
                        ::     empty(S_chan[rN]) ->break;
                        ::     atomic{S_chan[rN]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(N_chan[rS]) -> break;
                        ::     atomic{N_chan[rS]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(E_chan[rW]) -> break;
                        ::     atomic{E_chan[rW]?Dest_Id;  if
                                                                                        ::Recevier[Id]!=0 ->Recevier[Id]--;
                                                                                fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                        ::     empty(W_chan[rE]) -> break;
                        ::     atomic{W_chan[rE]?Dest_Id;    if
                                            ::Recevier[Id]!=0 ->Recevier[Id]--;
                                        fi}
                        printf("message received is %d\n",Dest_Id);is_message=true;break;
                           od
              fi
        fi
fi
if
    :: is_message==true -> skip;
    :: else -> goto loop;                   
fi
do
::(msg_send==true) -> break;
::else -> Dx=Dest_Id/N;Dy=Dest_Id%N;
    if
    ::(Cx<Dx) -> if
        ::(Cy<Dy) -> do
                ::empty(N_chan[Id]) ->     atomic{N_chan[Id]!Dest_Id;
                            Recevier[rN]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                ::empty(E_chan[Id]) ->     atomic{E_chan[Id]!Dest_Id;
                            Recevier[rE]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
        ::(Cy>Dy) -> do
                ::empty(W_chan[Id]) ->     atomic{W_chan[Id]!Dest_Id;
                            Recevier[rW]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
        ::else ->    do
                ::empty(N_chan[Id]) ->     atomic{N_chan[Id]!Dest_Id;
                            Recevier[rN]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
         fi
    ::(Cx>Dx) -> if   
        ::(Cy<Dy) -> do
                ::empty(S_chan[Id]) ->    atomic{S_chan[Id]!Dest_Id;
                            Recevier[rS]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
        ::(Cy>Dy) -> do
                ::empty(S_chan[Id]) ->    atomic{S_chan[Id]!Dest_Id;
                            Recevier[rS]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                ::empty(W_chan[Id]) ->     atomic{W_chan[Id]!Dest_Id;
                            Recevier[rW]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                      od
        ::else ->    do
                ::empty(S_chan[Id])->    atomic{S_chan[Id]!Dest_Id;
                            Recevier[rS]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break
                 od
         fi
    :: else ->   if
        ::(Cy<Dy) -> do
                ::empty(E_chan[Id]) ->    atomic{E_chan[Id]!Dest_Id;
                            Recevier[rE]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
        ::(Cy>Dy) -> do
                ::empty(W_chan[Id]) ->    atomic{W_chan[Id]!Dest_Id;
                            Recevier[rW]++;}
                            printf("message is send on %d... destination is %d,%d\n",Id,Dx,Dy);
                            msg_send=true;break;
                 od
        ::else ->     Success++;
                printf("msg-%d has reached destination %d node...No.of Destination reached is %d\n",Dest_Id,Id,Success);
                msg_send=true;
         fi
    fi   
od
goto start
}


init
{
byte x=0,y=0;
atomic{
do
:: skip;
    if
    :: (x<N)->if
            ::(y<N) -> run Process(x,y);y++;//printf("process created with x=%d y=%d\n",x,y);
            ::else -> x++;y=0;
          fi
    ::else -> break;
    fi
od}   
}

Offline

#4 2015-04-18 00:05:54

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

Re: Excessive memory usage with bitstate hashing

The run consumes some stack memory as it reaches greater depths in the dfs.
I'm not sure why that increase in memory is as pronounced as it is in this case, but if you limit the search
to a shorter depth, you'll see that the memory growth stops once that maximum is reached.
For the same number of states reached, Bitstate should always use less memory than any other search mode, although in this case it may be that the stack memory use tends to dominate memory use. (So if Bitstate got deeper into the statespace than Collapse, it would explain what you saw.)
The model itself is seriously complex.

Unrelated perhaps:
If you run your search as: "./pan -m10000000" you'll quickly get an invalid endstate error.
likely cause is that you use this type of construct in many places:
if
::Recevier[Id]!=0 ->Recevier[Id]--;
fi
which will block if Recevier[Id]==0
you probably want:
if
::Recevier[Id]!=0 ->Recevier[Id]--;
:: else
fi

Offline

#5 2015-04-18 03:32:45

haozheng
Member
Registered: 2013-12-16
Posts: 8

Re: Excessive memory usage with bitstate hashing

Thank you for the reply and pointing out the problem in my model.

What this example confuses me is the difference usages by -DCOLLAPSE and -DBITSTATE options. The results printed when pan is executed in those two modes are shown below for comparison.

Command:
gcc -DCOLLAPSE -DSAFETY -o pan pan.c
pan -m10000000
-------------------------------------------------------
Depth= 1023340 States=    1e+06 Transitions= 1.05e+06 Memory=   726.316    t=     2.15 R=   5e+05
Depth= 2046488 States=    2e+06 Transitions=  2.1e+06 Memory=   790.476    t=     4.33 R=   5e+05
Depth= 3069635 States=    3e+06 Transitions= 3.15e+06 Memory=   854.636    t=      6.5 R=   5e+05
Depth= 4092784 States=    4e+06 Transitions=  4.2e+06 Memory=   918.698    t=     8.62 R=   5e+05
^CInterrupted

Command:
gcc -DBITSTAE -DSAFETY -o pan pan.c
pan -w32 -k4 -m10000000
--------------------------------------------------------
Depth= 1023340 States=    1e+06 Transitions= 1.05e+06 Memory=  1690.223    t=     2.53 R=   4e+05
Depth= 2046488 States=    2e+06 Transitions=  2.1e+06 Memory=  2257.996    t=     5.62 R=   4e+05
Depth= 3069635 States=    3e+06 Transitions= 3.15e+06 Memory=  2825.770    t=     10.7 R=   3e+05
Depth= 4092784 States=    4e+06 Transitions=  4.2e+06 Memory=  3393.543    t=     16.6 R=   2e+05
^CInterrupted

From both runs, the depths of the stack are the same in each step of the printout, so I suppose the memory consumed by the stack should be about the same.

However, I do notice that large amount of memory is consumed by other (proc and chan stacks) when pan is executed in bitstate hashing mode which is shown in the stats on memory usage printed out at the end.  Can you explain what that memory is used for?

Stats on memory usage (in Megabytes):
2378.990    equivalent memory usage for states (stored*(State-vector + overhead))
  512.000    memory used for hash array (-w32)
   76.294    memory used for bit stack
  534.058    memory used for DFS stack (-m10000000)
2389.794    other (proc and chan stacks)
    2.784    memory lost to fragmentation
3514.930    total actual memory usage


Thank you very much.

Offline

#6 2015-04-18 03:36:05

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

Re: Excessive memory usage with bitstate hashing

last example: you misspelled BITSTATE, so that run wouldn't have been a bitstate run,
but I see your point -- I don't know the reason yet, but I'll try to find out

Offline

#7 2015-04-18 04:55:06

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

Re: Excessive memory usage with bitstate hashing

You notice this mostly because you're using such a large depth (10M steps).
If you repeat -- just as an experiment -- the same two searches, but with -m1000
you'll see that the BITSTATE search uses less memory than the COLLAPSE search,
for the same number of reached states.
There is an extra cost associated with deep stacks used for bitstate -- you can try
to get around that by storing the stack on disk (-DSC)

Offline

#8 2018-10-09 03:07:50

haozheng
Member
Registered: 2013-12-16
Posts: 8

Re: Excessive memory usage with bitstate hashing

When I  re-play a trail file using "spin -p -t a1_3.pml.trail" , I got an message on screen shown below.

spin: a1_3.pml.trail:1, Error: syntax error    saw ''-' = 45'
spin: cannot find trail file

From the trail file, the first line is "-4:-4:-4"

Can you please shed some light on this issue? I use spin version 648.

Thank you.

Offline

#9 2018-10-09 15:47:02

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

Re: Excessive memory usage with bitstate hashing

Spin just takes the name of the model itself on the replay, not the trail file. So the replay command is:
spin -p -t a1_3.pml
(without .trail at the end)

Offline

#10 2018-10-09 15:56:26

haozheng
Member
Registered: 2013-12-16
Posts: 8

Re: Excessive memory usage with bitstate hashing

Thank you.

Offline

Board footer

Powered by FluxBB