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