Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Protocol-based verification of message-passing parallel programs
López H., Marques E., Martins F., Ng N., Santos C., Vasconcelos V., Yoshida N.  OOPSLA 2015 (Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Pittsburgh, PA, Oct 25-30, 2015)280-298.2015.Type:Proceedings
Date Reviewed: Jun 21 2016

The message-passing interface (MPI) is a parallel computation standard that is widely used, especially in scientific computing. Parallel computation exhibits specific correctness problems arising from the possibility of several kinds of communication errors, for example, deadlock situations. Especially for complex and costly computations, it can be very important to verify that such situations cannot occur in a given program. There are several approaches available ranging from runtime checking to model checkers that explore and check the communication behavior. This paper adds a further technique, called ParType, based on type checking an MPI program with a protocol specification that is expressed as a type for the program. The problem of verification is then reduced to type checking the program.

The paper starts with an overview section that introduces a finite difference algorithm as a motivating example. The protocol specification language used in verification is then presented with the help of the example. Next, the type theory is formally constructed and some properties of the theory are stated. A message-passing programming language and its reduction semantics are then defined and some important consistency results are stated. The following section explains how the programming language and its protocol type system are encoded within a modified C program with MPI support and how type checking can be performed via the VCC verifier.

The final sections evaluate the performance of this approach in comparison with other verification approaches, compare the approach with other approaches, and look toward future work. The main benefit of this type of verification approach is that the verification time does not depend on the number of processors or iterations; hence, for a large number of iterations, the ParType approach mostly beats the other approaches.

The paper is quite readable and the basic ideas are readily grasped; however, many technical details have been omitted. Furthermore, the sections explaining the verification algorithm are sketchy and assume familiarity with the VCC verifier. Hence, the details may be difficult to comprehend for someone interested in concurrency in general.

Reviewer:  Markus Wolf Review #: CR144516 (1609-0668)
Bookmark and Share
 
Concurrent Programming (D.1.3 )
 
 
Formal Definitions And Theory (D.3.1 )
 
 
Language Classifications (D.3.2 )
 
 
Software/ Program Verification (D.2.4 )
 
 
Specifying And Verifying And Reasoning About Programs (F.3.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Concurrent Programming": Date

Type: Journal
Jul 1 1985
Resources in parallel and concurrent systems
, ACM Press, New York, NY, 1991. Type: Book (9780897914000)
Jun 1 1992
Concurrent programming
Andrews G., Benjamin-Cummings Publ. Co., Inc., Redwood City, CA, 1991. Type: Book (9780805300864)
Jun 1 1994
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy