Maude-help mailing list

[Scott Christley <schristley AT mac.com>]

Hello,

I've recently acquired access to some 16-core 64bit AMD machines and I  
am curious about the possibility of Maude utilizing all the processors  
in a parallel fashion.

My interest is not in parallel rewriting exactly, but in model  
checking.  It seems to me that the DFS algorithm can use multiple  
execution threads to explore separate branches of the state space.   
The question becomes are there thread safety issues, like in the  
rewrite engine, that would throttle performance gains?  Or maybe this  
has already been done by someone?

There is also consideration of a distributed architecture without  
shared memory space using a message passing protocol (MPI) for  
communication. This is more challenging because of graph partitioning  
and load balancing, but would be interesting to explore.

Lastly, from looking at the model checker code, it appears to  
represent states with an "int" data type.  Do I understand this  
correctly then, and there is a limit of 2^32 states?  Blindly changing  
this to "long" is likely not a good idea because it double memory  
usage, but a configure switch to enable it might be a good option.   
This isn't a practical issue right now, I'm just thinking ahead.

I've compiled Maude on 64bit and there doesn't seem to be any issue  
with accessing beyond 4GB.  Though I've noticed that the rewrite is  
slower (maybe half the speed) of 32bit, not sure if this is an issue  
with my architecture (Mac Intel) being slower for certain operations,  
or something in Maude.

thanks
Scott