Path: utzoo!mnetor!uunet!husc6!cmcl2!brl-adm!umd5!rutgers!ucla-cs!dgreen
From: dgreen@CS.UCLA.EDU (Dan Greening)
Newsgroups: comp.software-eng
Subject: Re: Correctness in parallel and distributed systems.
Message-ID: <11071@shemp.UCLA.EDU>
Date: 4 Feb 88 02:18:55 GMT
References: <899@hubcap.UUCP>
Sender: root@CS.UCLA.EDU
Reply-To: dgreen@CS.UCLA.EDU (Dan R. Greening)
Lines: 41

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