Using Model Checking with Symbolic Execution for the
by Anastasia Mironova
June 7-13 2004
This week's events were primarily associated with meeting the people at the LASER lab,
getting to know their research interests and projects, and figuring out what my project would be.
In order to become familiar with their work in more detail I've spent a significant amount of time reading the papers and
references given to me by my mentor Lori, some of those were the following:
J.M. Cobleigh, L.A. Clarke, L.J. Osterweil, "FLAVERS: A Finite State Verification Technique
for Software Systems"; IBM Systems Journal, Vol 41, No 1. 2002
R.L. Smith, G.S. Avrunin, L.A. Clarke, L.J. Osterweil, "PROPEL: An Approach Supporting
A. Wise, A.G. Cass, B.S. Lerner, E.K. McCall, L.J. Osterweil, S.M. Sutton Jr., "Using
Little-JIL to Coordinate Agents in Software Engineering"
M.S. Raunak, L.J. Osterweil, A. Deshmukh, "Using Process Language To Analyze Auction
Processes Through Simulations Synthesis Project Report"
S.F. Siegel, G.S. Avrunin, "Verification of MPI-Based Software for Scientific Computation"
Once I had become familiar with the current projects at LASER, Lori very kindly offered
me the opportunity to choose what I wanted to work on and my choice was to work with
Dr. Siegel, Steve, on modeling MPI-based software systems. This choice is due to my interest
in pursuing a Doctorate degree in the field of scientific computing and numerical analysis
in the near future.
Based on this choice, I was then given some more reading material about verification, MPI, and
one of the most popular verification tools, SPIN, to the careful exploration of which I devoted
the rest of that week.
June 14-20 2004
One of the main decisions at this point was whether I would work on modeling the code that already
exists or would the alternative of writing my own present a better perspective. In order to get some
references and advice on this issue Steve contacted his brother who works at the University of Chicago
and the Argonne National Laboratory to see if he'd have any recommendations on any existing
scientific computing packages that would be feasible for me to go through during the course of my
research here at UMass. Some of the references we were given were:
BLAS(Basic Linear Algebra Subprograms), - high quality "building block" routines for performing basic
vector and matrix operations;
CHOMBO, - provides a set of tools for implementing finite difference methods for the solution of partial
differential equations on block-structured adaptively refined rectangular grids;
FLASH, - a state-of-the-art simulator code for solving nuclear astrophysical problems related to
PFFT - a component of FLASH for computing Fast Fourier Transform;
PARAMESH, - a stand-alone product enabling quick and easy modifications of existing meshes from engineering
PETSC(Portable Extensible Toolkit for Scientific Computation), - is a suite of data structures and
routines for the scalable (parallel) solution of scientific applications modeled
by partial differential equations.
At the mean time I was getting myself familiar with MPI, C, and SPIN. As an excerise I began working on
a PROMELA model for the program that was written as part of the last assignment in my CS 331 Programming
Languages class which I took this spring. This program was intended to compute the product of any two square
matricies in parallel, it is written in C and utilizes MPI. The goal here was to construct two models: one
for checking for possible deadlock conditions and the second for verifying that the result computed by
this program in parallel would indeed result in a mathematically correct expression representing the product
of the two given matricies for any possible execution.
June 21-27 2004
Most of this week I spent working on the sample model of the matrix multiplication program's model, which I called matrixprod.prom. The model for checking whether the program could ever deadlocked was the first one I constructed. Then I moved on to verification of correctness of the computed result. This actually turned out to be a rather non-trivial task in SPIN because even though it does support some C, PROMELA is not a fully functional programming language. The solution to this was to construct expressions represented by a set of tree-like custom "typedef" structures, which would then be transmitted over the channels. On Friday I was finally able to successfully run my PROMELA model in simulation mode of SPIN, however, when I then attempted to use SPIN in its verification mode, I encountered an error indicating improper use of channels, which, as Steve and I later discovered, turned out to be a bug in SPIN. Here the issue was the following: Since, of course, in the case of dealing with matrices it was most intuitive to use arrays as the primary message type, that was exaclty what I chose to use but, unfortunately, SPIN does not provide for this capability in a straight forward way, forcing me to embed simple arrays into some "typedef" structures and then use these types of objects as the primary message format for the data channels. When a message of this type is received into some structure of the same type, naturally, one expects that all the entries of the arrays should be copied over into the receiving structure but SPIN's implementation of this routine had an overly strong conditional statements which were originally intended to prevent programmers from receiving several fields of one message into the same variable but also disabled some of the valid behavior like in this case. So, before I had any of this knowledge, the first thing I did when the problem was encoutered was constructed a minimal PROMELA program that gives an error and after talking to Steve about this he decided to email the author of the code,Gerard Holtzmann, which we did and it turned out that he was aware of this bug and that the new version of SPIN, which he was, luckily for me, planning to release during the coming weekend, would have this fixed.
June 28 - July 4 2004
Indeed, the new release of the SPIN model checker came out on June 29th and Steve installed in on the machine I
July 5-11 2004
This week I spent quite some time researching the different implementations of the Gauss-Jordan Elimination algorithm, both
July 12-18 2004
|This week was spent entirely on the implementation of the sequential and parallel versions of the Gauss-Jordan Elimination
algorithm in C using MPI.
The changes that I had to make to the original version of the Gauss-Jordan Elimination agorithm that is described in the original
references are the following:
In order to optimize performance in the parallel version I incorporated the "backward subtitution" routine into the preceding step
as an attempt to improve performance. Consequently, this change had to be made in the sequential implementation as well to
keep them as much alike as possible, since the idea was to make the sequential code alike to the parallel.
July 19-25 2004
This week both the sequential as well as the parallel implementations of the Gauss-Jordan Elimination algorithm in C using MPI were
July 26 - August 1 2004
|The major accomplishment of this week was that after a very long time I finally was able to make SPIN do what I need it to do and
the PROMELA implementation of the sequential version of the C code was completed. I did a few test runs and assumed that it was correct.
Also, this week I moved on to working on the PROMELA model of the parallel C implementation.
Concurrently this week I was also working on putting together a presentation for the laboratory meeting of the analysis group, which I was
scheduled to present on the 2nd of August, the Monday of the 9th week.
August 2-8 2004
On Monday I presented my project at the LASER analysis group meeting. I actually ended up spending some extra time on this
August 9-13 2004
Most of this week I, again, spent on fighting with SPIN and trying to finish the PROMELA model of the parallel implementation of my chosen