Steve's Matrix Mutiply Verification Challenge Analysis 
Contributor: Simone Atzeni

In this webpage introduce an analysis of the Matrix Multiplication: Correctness by Stephen F. Siegel presented in the Challenge Problem Session (EC)^{2} 2009 (Exploiting Concurrency Efficiently and Correctly) workshop. The problem consists in a parallel C/MPIbased implementation of matrixmatrix multiplication based on an example from Using MPI: Portable Parallel Programming with the MessagePassing Interface . The target of this challenge is to prove that the program produces the correct output for any given input, and showing that it terminates, does not deadlock, uses MPI correctly, etc.. In order to verify the correctness of the program, the parallel version is compared with the sequential version and will be showed the they are functionally equivalent . The correctness of the program will be verified with the assertion method and using the ISP (InSitu Model Checker) Tool. Besides, in the Analysis Report will be proposed various parallel versions of the program using different MPI functions. Each version, will be analyzed under a point of view of performance (execution times, number of processors, etc.) and with the help of ISP Tool will be checked the presence of deadlock, memory leak, assert violations, etc.. 
In this webpage will be reported just the program that verifies the output correctness. The sequential version of Steve's Matrix Multiplication embeds the parallel version. In this way, at the end of the computation, the process 0 checks through the assert function if each cell of the Sequential Version's matrix result is equal to the correspondent cell of the Parallel Version's matrix result. 
Here there is the code of the program that embeds the two versions of Steve's Matrix Multiplication Program (Sequential and Parallel). 
For more details see the entire report Steve's Matrix Mutiply Verification Challenge Analysis or download the LaTex Source . 
Last Modified: 06/24/2009 