Symbolic model checking is a way of analysing the behaviour of a possibly non-deterministic finite system by the exhaustive analysis of all possible internal states. Recent advances in the implementation of symbolic model checkers have allowed systems of around 10100 states to be analysed. Traditionally, model checking has mainly been used for the analysis of hardware designs, such as cache coherency mechanisms, and of communications protocols. The use of these model checkers has typically required the input of a design as an explicit finite state (Kripke) model and of a specification in Computation Tree Logic. It is thus not easy for a high-level language programmer to make use of such techniques as an aid to checking the correctness of her programs.
In this project we are investigating the usefulness of model checking as a tool for aiding the development of parallel programs. A first requirement, therefore, is a system that captures the essential features of a parallel program in a form that can be model checked. It is also necessary to allow the programmer to enter specifications in a familiar notation:
Finally, we must provide effective back annotation so that the programmer can understand the flaws in her design in the original program context.
The building of tools is, however, only part of the project. We are really interested in the effectiveness of such tools in the support of programming. This encompasses the full range of usability issues from the way the finite state model summarises the program, through the performance of the model checking engine, to the way results are presented.
We are using two model checkers in the project. SMV, from Carnegie-Mellon University, uses a novel technique, binary decision diagrams, to allow some very large systems to be checked. It takes input in the form of Kripke machines and a CTL specification. Recent versions of SMV attempt dynamic reordering of the BDDs.
A sample FDR display
The FDR model checker from Formal systems (Europe) Ltd accepts a pair of models specified in CSP and compares them to test if one is, in an appropriate sense, a refinement of the other. A graphical interface is supplied.
Initial work has concentrated on the occam programming language, mainly because of its direct support for concurrency and its very clean semantics. In previous projects, we have implemented SPOC, an occam-to-C translator which supports the full occam 2.5 language. This is widely used for academic research and teaching; we are also currently paid to provide support to an industrial customer. The compiler has been used by the Occam-for-all project to provide a distributed occam implementation on workstation clusters and by InterGlossa Ltd (http://www.glossa.co.uk/) for experiments with very lightweight threads.
Later in the project, we will implement a version of our system for the FORTRAN language; also in previous projects we have developed a front-end for FORTRAN90 using the same GMD compiler tools as the SPOC translator. The FORTRAN system will capture the semantics of parallel libraries such as MPI using an appropriate specification language. Some experiments will also be performed on Java codes, particularly in order to validate the safety of thread-based programs.
We currently have a working occam-to-SMV system which can handle communications, boolean variables, replicators, PAR, ALT, SEQ and IF. Constructs that are not handled, such as floating-point operations, are ignored. If the result of an ignored operation is required by a handled construct, then all possible choices for the value are explored. Thus nondeterminism in the output SMV arises in two ways: the intrinsic nondeterminism of the occam ALT and the nondeterminism arising from our translators approximation of the input program. The model checker fully explores all paths in the nondeterministic machine, so the output from SMV is uniformly pessimistic; if SMV says the code is OK, then it _is_ OK.
As a very simple example, if we input the program
PROC test()
CHAN OF ANY c:
CHAN OF ANY d:
INT x, y:
SEQ
PAR
INT x:
SEQ
x := 4
IF
(x = 4)
x := 5
TRUE
SKIP
d ! 4
SEQ
c ! 7
SEQ
ALT
c ? x
SKIP
d ? y
SKIP
d ? y:
to our translator, it will generate an SMV state machine and the specification
SPEC AG EF (pc0 = 4)
which may be read as:
over all possible paths
over all times
there is some possible path
which at some time
leads to program termination
Thus the specification tests to see if the program can possibly reach a state from which it cannot terminate. When fed to SMV, we get the result:
-- specification AG EF pc0 = 4 is false
-- as demonstrated by the following execution sequence
followed by a sequence of states leading to, in this case, deadlock.
Symbolic Model Checking, K L McMillan, Kluwer Academic Publications, 1993. ISBN 0-7923-9380-5. Further details and source code for SMV may be found at http://www-2.cs.cmu.edu/~modelcheck/
Occam 2 Reference Manual, INMOS Ltd., Prentice Hall, 1988.
ISBN
0-13-629312-3. Further material on occam can be found at
http://wotug.ukc.ac.uk/parallel/occam/index.html.
Failures Divergences Refinement User Manual and Tutorial, Formal Systems(Europe) Ltd, http://www.formal.demon.co.uk/fdr2manual/index.html. Further information on FDR2 can also be found on this web site.
Southampton's Portable Occam Compiler, M Debbage, M Hill, S Wykes and D Nicole, in Progress in Transputer and occam Research, WOTUG-17, IOS Press, ISBN 90-5199-163-0. Further information on SPOC may be found at the hensa site.
Further information may be found at http://www.hpcc.ecs.soton.ac.uk/~dan.
Last updated 4th July 1997. Maintained by Denis A Nicole.
