1. Introduction

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. This characterization has been borne out in experiences with writing the Multi-Purpose Daemon (MPD): despite MPD's small size and apparent simplicity, errors have impeded progress toward correct code. Such a situation led to exploration of program verification techniques.

MPD [1] is a process manager for parallel programs and is itself a parallel program. Its function is to start the processes of a parallel job, manage input and output, deal with faults, provide services to the application, and cause jobs to terminate cleanly. MPD is the sort of process manager needed to run applications that use the standard MPI [3] library for parallelism, although it is not MPI-specific.

Our attempt to use formal verification techniques to ensure correctness of MPD algorithms employs the model checker SPIN [4], which supports design and verification of asynchronous distributed communicating systems. Models of such systems are recorded in a 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 (LTL). The verification engine of SPIN is based on on-the-fly reachability analysis with several optimizations and heuristics. The system also includes a simulation environment and a graphical user interface.

2. Modeling Components of the MPD System

The MPD system consists of several types of processes (called daemon, manager, console, and client) that communicate over Unix sockets and pipes. Daemons and managers are connected in a ring. A typical setup of the MPD system is shown in Figure 1.

Figure 1. Daemons with console process, managers, and clients

MPD algorithms execute on daemons and managers. Daemons and managers execute in essentially infinite loop: they receive messages on their connections and perform actions depending on the type of the received message. The actions are relatively simple and typically involve sending another message. Thus, daemons and managers are viewed and modeled in three layers. On the first layer is the main loop that allows to select a message from one of the attached communication connections. The middle layer is the collection of algorithms that are executed in response to each defined message type. The bottom layer is the mechanism that allows messages to travel from one process to another. The real MPD system relies on Unix sockets for communication between the processes, and the operating system provides all the necessary services.

The MPD algorithms that we would like to verify thus reside in the middle layer of the three-tiered model. To proceed with verification, we must model not only the algorithms of interest but also the interprocess communication of the bottom level; that is, we have to create a Promela model of Unix sockets. Success of verification attempts depends on the efficiency of the underlying model, and so creation of an efficient Promela model of sockets was important. Several Promela models of socket handling functions were tried. Finally, we created a reusable general-purpose library of Unix socket functions. The library contains implementations of the socket functions connect, accept, read, write, close, and select. These functions provide the interface between the interprocess communication layer of the three-tiered model and the middle layer where the algorithms reside. A different implementation of the socket library can be used, if desired, without making any changes to the model of the algorithms.

3. Verification of MPD Algorithms

We considered algorithms that reside on different levels of the MPD system. Two related daemon-level algorithms were modeled: an algorithm for simultaneously inserting new members into a ring of daemons and an algorithm for a recovery of the ring after a single nondeterministic daemon failure. Each of the two algorithms was verified against two correctness properties. The first property (state) is a static check that the information contained in the underlying data structures indeed represents a properly connected ring. The second property (trace) is that a special purpose ring traversal algorithm completes after having visited each member of the ring. We also modeled a manager-level algorithm to provide a synchronization service to the client application processes. A correctness property, stating that no client is allowed to proceed past the synchronization point until all clients have reached the synchronization point, was proved for the algorithm with SPIN's aid.

As shown in Table 1, verification succeeded on models of only a small size, especially compared with the real MPD system that can involve hundreds if not thousands of processes. However, since even the most difficult errors can be discovered on models comprising only a few processes, the verification engine of SPIN enables us to verify the algorithms on models that are sufficiently large for our purposes.

Definition, design, implementation and application:

Specialization and integration:

Authors are invited to submit an extended abstract of up to 10 pages. Researchers interested in attending the workshop without giving a talk are invited to send a position paper of 1--2 pages. All submissions should be sent to the Program Chairs (strategies02@cs.uiowa.edu) in Postscript before April 22, 2002. Accepted contributions will be included in the workshop proceedings, which will be available at the workshop and on the Web.

Based on the submissions, the Program Chairs will consider the possibility of a postworkshop publication (e.g., a special issue of a journal or a volume in a series of electronic proceedings), where authors may submit full versions of the workshop papers. This may involve another call for papers and refereeing process.

Attendance is by invitation only but late requests for participation will be considered.

Potential participants of ADG 2002 are invited to submit an extended abstract (3 or more pages) or a full paper by June 3, 2002. Electronic submissions are preferred, and should be sent to the chairman Franz.Winkler@risc.uni-linz.ac.at. Authors of the extended abstracts and full papers accepted for presentation at the workshop will be invited to submit their full or revised papers for publication in the proceedings of ADG 2002 after the workshop. It is expected that the accepted papers will be published as a volume in the LNAI series by Springer-Verlag.

Amy Felty has issued a call for papers for a special issue of the Journal of Aumated Reasoning on proof-carrying code and related approaches that use formal reasoning to enhance safety and reliability of software. Topics of interest include original results and study of tools and methods for proof generation, proof checking, and their integration with code generation/compilation. Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality. The deadline for submissions is February 22, 2002.