Performance measurements

A system has been set up to periodically measure the performance of several mCRL2 tools and of compiling the entire toolset. This way, it is possible to see how the performance of these processes changes over time.

You can view the performance plots for:

Build measurements

For measuring the build time, the following commands are executed from the trunk directory of the mCRL2 repository:

make distclean
svn update
./configure --prefix=PREFIX
make bjam
time make
make install

Here, PREFIX is the path to the installation directory. No options other than --prefix are passed to ./configure and compiler caches (like ccache) are not used. Only the time needed for the make command is measured.

Tool measurements

The following tools are currently being measured:

Tool Options
mcrl22lps [default], -fD, -nfD
lps2lts [default], -rjittyc
pbes2bool -pquantifier-all, -pquantifier-all -rjittyc

The benchmark set consists of 14 mCRL2 specifications.

Every tool + options combination is run on every input specification (say input.mcrl2) in the following way:

  • tool-mcrl22lps is run on input.mcrl2

  • For tool-lps2lts an LPS is generated with the following command:

    mcrl22lps -fD input.mcrl2 | lpsconstelm | lpsparelm | lpssuminst > input.lps
    

    The tool is then run on input.lps.

  • For tool-pbes2bool a PBES is generated by running the following command on the LPS that was generated for lps2lts above, and the μ-calculus formula for absence of deadlock:

    lps2pbes -f no_deadlock.mcf input.lps | pbesrewr > input.pbes
    

    The tool is then run on input.pbes.

Of every run, both time and memory usage are measured. If the run fails or runs out of memory, a value of -1 is registered.

Notes

  • The measurements are performed nightly but only if the SVN source tree has changed since the previous measurements.
  • For some tool + options combinations and case studies measurements have started more recently than for others. Also, memory measurements have first been performed in SVN revision 4360.
  • Up to revision 5964 (14 April 2009), tool-pbes2bool was run with the option -p instead of -pquantifier-all. Note that these options are not comparable.

System information

The measurements are performed on the following system.

Hardware

Architecture
x86_64
Processor
Intel Pentium D 3.00 GHz, Dual Core, EM64T
Front side bus
800 MHz
L2 Cache size
2 × 2.048 KB
Chipset
Intel 945G
Memory
1.024 MB DDR2 SDRAM (533 MHz)
Swap size
512 MB
Hard drive
160 GB, 7200 RPM, serial ATA

Software

Operating system
Fedora Core GNU/Linux, x86_64
C++ Compiler
GCC
mCRL2 configuration
Release mode