steve@hubcap.UUCP ("Steve" Stevenson) (01/29/88)
I would like to find a reasonably up-to-date bibliography on proving parallel programs correct. I would also like same for distributed programs, say for the huge hypercube numerical programs being developed. Thanks. ~r .signature -- Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906
siegel@svax.cs.cornell.edu (Alexander Siegel) (02/01/88)
In article <899@hubcap.UUCP> steve@hubcap.UUCP ("Steve" Stevenson) writes: >I would like to find a reasonably up-to-date bibliography on >proving parallel programs correct. I would also like same for >distributed programs, say for the huge hypercube numerical programs being >developed. This is very much an open research problem. I suspect you will only be able to find flaky journal articles and miserably out of date texts on this subject. -- Alex Siegel (607)255-1165 (Low Bandwidth Audio) 4161 Upson Hall, Cornell University, Ithaca NY 14853 (Hard Copy) siegel@svax.cs.cornell.edu (ARPAnet) siegel@CRNLCS (BITNET) {uw-beaver,ihnp4,decvax,vax135}!cornell!siegel (UUCP)
jbn@glacier.STANFORD.EDU (John B. Nagle) (02/01/88)
Proof of correctness has been a disappointing technology. The
basic problems are
1) How do you write down what the program is "supposed to do"?
Formal specifications of real programs turn out to be no better
than half the size of the program itself, and much harder to
debug. In any case, if we really had a way to express formal
specifications that was any good, we would be better off trying
to generate code from them than verifying handwritten code against
them. Formal specification languages turn out, in the end, to be
just another kind of programming language.
2) A useful verifier is about as complicated as a globally optimizing
compiler for the same language. Such compilers typically cost
tens to hundreds of man-years to develop. Building a verifier
is a big, expensive job.
3) The low-rent approaches don't work. Proving "partial correctness"
generates partially correct programs. We can do that without
verification technology. Doing verification by hand, without
automated tools, is not only error prone, but a task of mind-numbing
boredom, and the boredom itself results in errors, many of which
consist of proving something correct that wasn't.
4) It is brutally hard to push a program through a verifier. It's
like doing your taxes while being audited at the same time. So
verified programs are very expensive to develop.
Verification is not impossible. But there are some very tough problems.
Verification theory isn't the problem, though. Nor is automatic theorem
proving. We actually know enough to build and use verification systems.
but it is very, very hard. See my paper (with Scott Johnson) in POPL 83 and
Don Good's GYPSY project at U. Texas for examples of some non-trivial systems
that were built.
If problem 1) above ever gets cracked, the others can be solved.
John Nagledgreen@CS.UCLA.EDU (Dan Greening) (02/04/88)
In article <899@hubcap.UUCP> steve@hubcap.UUCP ("Steve" Stevenson) writes: >I would like to find a reasonably up-to-date bibliography on >proving parallel programs correct. I would also like same for >distributed programs, say for the huge hypercube numerical programs being >developed. Can't give a bibliography, but Leslie Lamport is working on some things related to this. He appeared at a UCLA seminar last year. He claimed to be writing a book on semantics of parallel programs. If this feeble brain recalls correctly, he used a control flow model of computation. Data flow and functional approaches to parallelism produce programs that are much easier to discuss in a theoretic framework. I suggest you look at J. Backus, Can Programming be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs, Communications of the ACM, 21(8):613-641 (August 1978). This classic article supplies an interesting set of program transformations that can assist in proving functional programs correct. The Scientific Citation Index will provide a list of successor articles. A major problem with control-flow (i.e., "normal" multiprocessing), and any other non-applicative system is the indeterminacy of memory stores and fetches. This also applies to some data flow languages, though in a much more restricted sense. "Id Nouveau" from MIT comes immediately to mind. In that language, non-strict evaluation can cause deadlock problems. But I'd much rather prove an Id Nouveau program correct than a Concurrent Pascal program correct. Yikes! Good luck! Dan Greening Internet dgreen@CS.UCLA.EDU UUCP ..!{sdcrdcf,ihnp4,trwspp,ucbvax}!ucla-cs!dgreen USPS 3436 Boelter Hall / UCLA / Los Angeles, CA 90024-1596
kerpelma@macbeth.steinmetz (dan kerpelman) (02/04/88)
In article <899@hubcap.UUCP> steve@hubcap.UUCP ("Steve" Stevenson) writes: >I would like to find a reasonably up-to-date bibliography on >proving parallel programs correct. I would also like same for >distributed programs, say for the huge hypercube numerical programs being >developed. This is a little old but... Susan Owicki, David Gries, _Verifying Properties of Parallel Programs: An Axiomatic Approach_, Communications of the ACM, Volume 19, Number 5, May 1976. --------------------------------------------------------------------------- Dan Kerpelman ARPAnet: kerpelman@ge-crd.arpa GE Corporate R&D UUCP : crd!kerpelman@steinmetz.UUCP Schenectady, NY GEnet : ctsvax::kerpelman USA phone : (518) 387-5086 "La seule chose que nous avons a craindre, c'est que le ciel nous tombe sur la tete!" -Abraracourcix