Methods to model-check parallel systems software. Page: 4 of 15
This report is part of the collection entitled: Office of Scientific & Technical Information Technical Reports and was provided to Digital Library by the UNT Libraries Government Documents Department.
The following text was automatically extracted from the image on this page using optical character recognition software:
Methods to Model-Check Parallel Systems Software
Olga Shumsky Matlin, William McCune, and Ewing Lusk
We report on an effort to develop methodologies for formal verification of parts of the Multi-
Purpose Daemon (MPD) parallel process management system. MPD is a distributed collection
of communicating processes. While the individual components of the collection execute simple
algorithms, their interaction leads to unexpected errors that are difficult to uncover by con-
ventional means. Two verification approaches are discussed here: the standard model checking
approach using the software model checker SPIN and the nonstandard use of a general-purpose
first-order resolution-style theorem prover OTTER to conduct the traditional state space explo-
ration. We compare modeling methodology and analyze performance and scalability of the two
methods with respect to verification of MPD.
Reasoning about parallel programs is surprisingly difficult. Even small parallel programs are
difficult to write correctly, and an incorrect parallel program is equally difficult to debug, as we
experienced while writing the Multi-Purpose Daemon (MPD), a process manager for parallel
programs [2, 3]. Despite MPD's small size and apparent simplicity, errors have impeded progress
toward code in which we have complete confidence. Such a situation motivates us to explore
program verification techniques.
MPD is itself a parallel program. Its function is to start the processes of a parallel job in a
scalable way, manage input and output, handle faults, provide services to the application, and
terminate jobs cleanly. MPD is the sort of process manager needed to run applications that
use the standard MPI [15, 16] library for parallelism, although it is not MPI specific. MPD is
distributed as part of the portable and publicly available MPICH [5, 6] implementation of MPI.
Our first attempt to use formal verification to ensure correctness of MPD algorithms 
employed the ACL2  theorem prover, which allows one to both simulate and verify a model
within a single environment. Components of the MPD system, as well as the elements of
the Unix socket library on which MPD is based, were formalized in a subset of Lisp. The
formalization was based on a so-called oracle , which allows analysis of a parallel system in
a sequential environment. The oracle specifies an execution interleaving of concurrent processes
and is randomly generated for simulations. Verification is conducted with respect to an arbitrary
oracle (i.e., an arbitrary execution interleaving); thus, a property proved in such a way holds
for all possible executions of a collection of concurrent processes. In this approach parsing
simulation results, formulating desired properties of models of MPD algorithms and reasoning
about such models proved difficult, leading us to abandon this traditional theorem-proving
method of verification and to try instead model-checking techniques. Two such techniques are
The first technique employed the model checker SPIN [7, 8], which supports design and
verification of asynchronous distributed communicating systems. Models of such systems are
recorded in the special high-level verification language PROMELA, which can also be used to
state some correctness properties of the models. Additional correctness properties are specified
by using linear temporal logic. The verification engine of SPIN is based on on-the-fly reachability
analysis with several optimizations and heuristics, such as partial-order reduction and bitstate
hashing. The system also includes a simulation environment and a graphical user interface. SPIN
Here’s what’s next.
This report can be searched. Note: Results may vary based on the legibility of text within the document.
Tools / Downloads
Get a copy of this page or view the extracted text.
Citing and Sharing
Basic information for referencing this web page. We also provide extended guidance on usage rights, references, copying or embedding.
Reference the current page of this Report.
Matlin, O. S.; McCune, W. & Lusk, E. Methods to model-check parallel systems software., report, December 15, 2003; Illinois. (digital.library.unt.edu/ark:/67531/metadc785458/m1/4/: accessed October 21, 2018), University of North Texas Libraries, Digital Library, digital.library.unt.edu; crediting UNT Libraries Government Documents Department.