Eddy Murphi

From Uv-wiki

Eddy Murphi - The Parallel and Distributed Murphi Model Checker

Contents 1 Introduction 2 How To Get Eddy Murphi 3 Related Papers 4 Documents 5 Recent Developments 6 Possible Future Development 7 SVN Repository

Introduction

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 below Mellati et al.) for achieving a high degree of parallelism in its computation.

How To Get Eddy Murphi

The download page for Eddy Murphi can be found here.

Related Papers

• Parallel and Distributed Model Checking in Eddy (Melatti et al.)

Documents

Some informal reports of the progress of the most recent work on Eddy Murphi are listed below (please note that these reports are still evolving):

• Summary of Recent Improvements to the Eddy Murphi Model Checker (PDF) (.tex)
• Adding Random-Walk Dependence Calculation and POR to Eddy Murphi (PDF) (.tex)

Also, some additional documentation for Eddy Murphi is contained below:

• Eddy Murphi Development Starter Manual (PDF) (.tex) - This document contains information on the high-level code structure of Eddy Murphi, intended as a starter guide for development.

Recent Developments

The various changes to each version of Eddy Murphi is outlined below:

• Version 3.2.4 (August 30, 2009)
  • Fixes an MPI resource leak. This version also implements a more robust messaging style preventing some nodes from becoming too overwhelmed with work aiding in more robust and more successful verifications.
• Version 3.2.3
  • Compatible with 64-bit architectures
• Version 3.2.2
  • Fix to the termination algorithm, which previously contained a rare bug.
• Version 3.1.5 (alpha)
  • Older version, contains known bugs.

Possible Future Development

• POR (Partial Order Reduction)
  • Partial-order reduction is a method that safely removes redundant portions of the state space being verified in order to reduce the amount of time and resources spent perfroming verification. This has challenges in a distributed setting that are easily handled in a sequential setting.
• Work Queue load balancing
  • Some nodes in a distributed verification become idle as the number of seen states reaches the size of the state space. Load balancing is a method for pushing new work to idle nodes to gain a performance benefit. A good paper on this topic is by Kumar et al here.
• Random-Walk ideas for dependence calculation
  • Many dependence calculations used for POR are based on a static analysis of rules in the protocol source description. Random-walk dependence calculation performs this operation dynamically by manually checking the commutativity and enabledness of states generated when randomly traversing the state space.
• Movers as a means for state reduction
  • Movers is a similar idea for state space reduction that could be applied to Eddy Murphi by delaying the expansion of states that commute to a later point in the state space.

SVN Repository

For SVN access, contact the person in charge within the group.

The URL for Eddy Murphi is svn://proof.cs.utah.edu/EddyMurphi.

The following lists project subdirectories and their description:

• trunk/ - Contains the stable project sources and most up-to-date snapshot of Eddy Murphi.
• branches/ - Contains branched development ideas, which are not intended for the trunk.
  • branches/RandomWalkPOR - Contains the current developments of Random-Walk dependence calculation and Partial Order Reduction. This development is on hold, only random walk dependence calculation has been developed so far, nothing yet on POR.
• tags/ - Contains snapshots of various Eddy Murphi revisions for reference purposes.
  • tags/EddyMurphi.3.1.5a
  • tags/EddyMurphi.3.2.1
  • tags/EddyMurphi.3.2.2
  • tags/EddyMurphi.3.2.4