University of Utah
Search
School of Computing
Home People Research Admissions Site Map  
Eddy Murphi - Parallel and Distributed Murphi
Description

Eddy Murphi is a parallel and distributed version of the Murphi model checker. It is currently based on the caching Murphi (CMurphi) version 3.1. Eddy Murphi utilizes MPI for its message passing communication between computing nodes and uses the novel Eddy algorithm (described in the paper by Mellati et al. here) for achieving a high degree of parallelism in its computation.

Download and Install

Latest Version:

  • Eddy_Murphi.3.2.4  (Aug. 30, 2009)
  • Release Notes:
    • Implements more robust message passing that prevents slower nodes from getting overwhelmed with work. Also fixes an MPI resource leak that prevented long runs from finishing.

Older Versions:

Documentation

/doc Folder in Release

The /doc folder in the release contains usage and install information.

Wiki Documentation

The Gauss Wiki has additional information on Eddy Murphi such as recent developments, future development, as well as a guide for users wishing to modify the Eddy Murphi code.

The direct link to the Eddy Murphi section of the Wiki is here.

Example Usage

First, boot MPI if it is not configured to boot automatically.

$ mpdboot --totalnum=8 --file=$HOME/mpd.hosts

Example of nodes running in the Raven cluster at Utah.

$ mpdtrace
raven-srv
raven17
raven16
raven15
raven14
raven19
raven20
raven18

Well show the ldash example.

$ cd ex/dash

Make the executable using a Makefile, example Makefiles can be found in the /ex/<example>/ subdirectory of the Eddy Murphi distribution.

$ make ldash

Now, run with MPI.

$ mpiexec -n 8 ./ldash -m 64
...(Murphi preamble output)...
Starting progress report on node 4:

  Node 4: 1000 states explored in 1.96s, with 6370 rules fired and 265 states in the queue.

Starting progress report on node 6:

  Node 6: 1000 states explored in 2.12s, with 6835 rules fired and 910 states in the queue.

Starting progress report on node 2:

  Node 2: 1000 states explored in 3.09s, with 9511 rules fired and 55 states in the queue.
  Node 4: 2000 states explored in 3.34s, with 13310 rules fired and 625 states in the queue.
  Node 6: 2000 states explored in 3.62s, with 14603 rules fired and 962 states in the queue.

Starting progress report on node 5:

  Node 5: 1000 states explored in 3.59s, with 9110 rules fired and 273 states in the queue.
  Node 2: 2000 states explored in 4.84s, with 18051 rules fired and 1283 states in the queue.

Starting progress report on node 1:

  Node 1: 2000 states explored in 5.41s, with 18987 rules fired and 1104 states in the queue.
  Node 4: 4000 states explored in 6.22s, with 26553 rules fired and 4054 states in the queue.
... (More output as states are explored) ...
==========================================================================

Status:

  No error found.

State Space Explored:

  254986 states, 2647358 rules fired in 100.44s.

Statistics per node, state space:

  Node 0: 37605 states, 387321 rules fired in 100.44s.
  Node 1: 30739 states, 321868 rules fired in 192.57s.
  Node 2: 25691 states, 275930 rules fired in 192.63s.
  Node 3: 21899 states, 240208 rules fired in 192.61s.
  Node 4: 42964 states, 433210 rules fired in 192.71s.
  Node 5: 30197 states, 312257 rules fired in 192.71s.
  Node 6: 39235 states, 397657 rules fired in 192.68s.
  Node 7: 26656 states, 278907 rules fired in 192.60s.

Statistics per node, messages:

  Node 0: 122 messages sent, 517 messages received, with at least 152 and at most 155648 states each, average 149822.16.
  Node 1: 397 messages sent, 403 messages received, with at least 152 and at most 155648 states each, average 44174.19.
  Node 2: 599 messages sent, 344 messages received, with at least 152 and at most 155648 states each, average 24413.64.
  Node 3: 653 messages sent, 293 messages received, with at least 152 and at most 155648 states each, average 21219.71.
  Node 4: 172 messages sent, 455 messages received, with at least 152 and at most 155648 states each, average 104208.37.
  Node 5: 424 messages sent, 369 messages received, with at least 152 and at most 155648 states each, average 38680.42.
  Node 6: 218 messages sent, 459 messages received, with at least 152 and at most 155648 states each, average 83099.38.
  Node 7: 564 messages sent, 309 messages received, with at least 152 and at most 155648 states each, average 27526.01.

Proc time of each node:

  Node 0: 100.44s.
  Node 1: 192.57s.
  Node 2: 192.63s.
  Node 3: 192.61s.
  Node 4: 192.71s.
  Node 5: 192.71s.
  Node 6: 192.68s.
  Node 7: 192.60s.

Total MPI time: 192.76s.

Analysis of State Space:

  There are rules that are never fired.
  If you are running with symmetry, this may be why. Otherwise,
  please run this program with "-pr" for the rules information.

Questions and Feedback

Eddy Murphi is currently maintained by Prof. Ganesh Gopalakrishnan's research group in the School of Computing at the University of Utah.

Questions, bug reports, and comments are welcomed via email. Carson Jones ( AT cs.utah.edu) is a research assistant currently working on Eddy Murphi, also questions can be sent to Ganesh Gopalakrishnan (firstname AT cs.utah.edu).

Last updated on