[comp.software-eng] Correctness in parallel and distributed systems.

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 Nagle

dgreen@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