Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Hi Scott,

Sorry for the delay in responding - I have been on vacation.

Unfortunately I designed the Maude rewrite engine in the mid 90's when
thread safety was not much of an issue and I did a lot of things,
particularly preallocating data structures, that are thread unsafe but
important for performance on a single core machine, given the slowness
of memory allocation and deallocation. Making it thread safe would be
quite a tricky task and would cut its performance significantly.

I do have a sketch design for a multithreaded rewrite engine for a
future version of Maude.

There are many things that might help the speed and memory usage of
the model checker, including a restricted form of hash consing.

There is a limit of 2^31 system states. Using 64-bit state indices
would require a data type that is indexable by 64-bit values but the
increase in memory consumption might not be that bad since most of the
memory usage will likely be pointer based data structures that are
already 64-bit when running a 64-bit binary. Probably using size_t is
the right way to go.

Maude should be 64-bit clean. I hadn't noticed that it was slower when
running a 64-bit binary, but a couple of quick benchmarks show that
for large term graphs it can be slower - presumably because it becomes
memory bound and then moving dagnodes in and out of memory takes twice
as long because they are twice the size on a 64-bit binary.
For heavy computation on smallish term graphs I don't see a
difference.

Steven

On Tuesday 22 July 2008 18:55, Scott Christley wrote:
> 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
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help