Maude-help mailing list

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

On Friday 05 March 2010, Sung-Shik Jongmans wrote:
> Hi,
> 
> I am interested to know Maude's memory consumption during model-checking. I
>  could not find anything about reports on memory consumption in the manual,
>  so currently I am simply keeping a close eye on the amount of memory in
>  use by the Maude process (during model-checking). My question: is there a
>  more "sophisticated" way of doing this? For example, in "The Maude LTL
>  Model-Checker" (2004), the average memory usage is reported in an
>  evaluation of the performance. How are these memory measurements obtained?
> 
> Kind regards,
> Sung.
> 

I can't speak to the numbers in the paper - Ambarish did  the benchmarking. 
top is probably as good as anything. You can use the command:
  set show gc on .
to show the number of arenas (of dag nodes) and buckets (of variable length 
arrays) managed by the garbage collector. Each dag node is 6 machine words 
(i.e. 48 bytes on a 64-bit machine). Note that not all the data in term-graph 
is directly managed by the garbage collector - bignums and long (currently 
length > 3) argument lists of free theory symbols are allocated used the C 
and 
C++ heap management primitives (malloc/free, new/delete).

Btw if you have some interesting model checking benchmarks, contact me off 
the 
list to try the new hashcons'd version of the model checker. We are about to 
release Maude 2.5 in a couple of weeks and I would appreciate feedback.

Steven