Mon Nov 23 16:03:14 EST 1992 From owner-mpi-formal@CS.UTK.EDU Wed Nov 25 13:38:40 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA21710; Wed, 25 Nov 92 13:38:40 -0500 Received: by CS.UTK.EDU (5.61++/2.8s-UTK) id AA09826; Wed, 25 Nov 92 13:14:59 -0500 Received: from relay1.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA09818; Wed, 25 Nov 92 13:14:52 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay1.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA16145; Wed, 25 Nov 92 13:14:48 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 131338.3994; Wed, 25 Nov 1992 13:13:38 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-92031301) id AA12688; Wed, 25 Nov 1992 12:06:04 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA08958; Wed, 25 Nov 92 12:06:02 -0600 Date: Wed, 25 Nov 92 12:06:02 -0600 Message-Id: <9211251806.AA08958@brisk.kai.com> To: mpi-pt2pt@cs.utk.edu, mpi-collcomm@cs.utk.edu, mpi-formal@cs.utk.edu, mpi-ptop@cs.utk.edu Reply-To: William.Gropp's.message.of.Wed@kai.com, 25 Nov 92 09:28:43 CST <9211251528.AA12985@godzilla.mcs.anl.gov> Subject: Nonblocking functions and handlers. From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 Bill Gropp writes: (Warning: radical position that I'm not sure even I hold follows:) An interesting issue is whether we should defer all nonblocking communications to a thread-based execution model. I'm not so sure this is a radical position Bill since even nonsynchronized communication will need to be defined formally this way. Nonsynchronized communication is in effect creating a parallel process that has the job of passing the communication on. Al Geist earlier asked the question wheather buffers used by nonsynchronized communication should be accessible after the communication has started - the answer should be - no, unless by some explicit mechanism that formally amounts to a communication with the process mentioned above. Any nonexplicit interaction (e.g. a write to the buffer) would have to be specified as formally equivalent to an explicit interaction. Also, there is quite a range of terminology in use. One common error: "Asynchronous" and "synchronous" has quite a particular meaning in EE and when CS people use the terms in relation to message passing they usually mean NONSYNCHRONIZED and SYNCHRONIZED. Also BLOCKING = SYNCHRONIZED. Let us begin a glossary that defines the terms we use - if no-one else volunteers I'll take this to be the responsibility of the Formal Specification Subcommittee. So I'm looking for volunteers from that subcommittee. Steven From owner-mpi-formal@CS.UTK.EDU Wed Nov 25 16:38:24 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA25899; Wed, 25 Nov 92 16:38:24 -0500 Received: by CS.UTK.EDU (5.61++/2.8s-UTK) id AA14144; Wed, 25 Nov 92 16:19:30 -0500 Received: from relay1.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA14140; Wed, 25 Nov 92 16:19:27 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay1.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA16575; Wed, 25 Nov 92 16:19:01 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 161434.11738; Wed, 25 Nov 1992 16:14:34 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-92031301) id AA21726; Wed, 25 Nov 1992 15:05:38 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA09109; Wed, 25 Nov 92 15:05:36 -0600 Date: Wed, 25 Nov 92 15:05:36 -0600 Message-Id: <9211252105.AA09109@brisk.kai.com> To: mpi-formal@cs.utk.edu Cc: Bill.Roscoe@prg.ox.ac.uk, dongarra@cs.utk.edu Subject: MPI Formal Specification Subcommittee. From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 Welcome to the Formal Specification Subcommittee of the Message Passing Interface Committee. ------------------------------------------------ Our job, as I see it, is to track events in the other subcommittees, to specify formally the final definition and to ring bells if the errant desires of the other subcommittees present semantic or specification problems. The specification language of choice is CSP, and the reference specification will be written in it. That does not preclude other specifications useing other notations to be derived now or later. CSP's maturity and ability to express concurrent behavior make it ideal as a tool for capturing these semantics. The issue of verification is an important one and we should begin now considering how implementations can be verified. As soon as the dust settles in the other committees I'll produce a working draft of the specification. I'll endevour to make that available before the January meeting in Dallas. Steven Ericsson Zenith Chairperson, MPI Formal Specification Subcommittee. P.S. I copy Bill Roscoe at Oxford University and Jack Dongarra as a matter of courtesy. From owner-mpi-formal@CS.UTK.EDU Fri Nov 27 12:07:50 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA25718; Fri, 27 Nov 92 12:07:50 -0500 Received: by CS.UTK.EDU (5.61++/2.8s-UTK) id AA08750; Fri, 27 Nov 92 12:06:51 -0500 Received: from relay2.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA08746; Fri, 27 Nov 92 12:06:37 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay2.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA04271; Fri, 27 Nov 92 12:06:23 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 120541.25493; Fri, 27 Nov 1992 12:05:41 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-92031301) id AA12937; Fri, 27 Nov 1992 10:25:06 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA11158; Fri, 27 Nov 92 10:25:05 -0600 Date: Fri, 27 Nov 92 10:25:05 -0600 Message-Id: <9211271625.AA11158@brisk.kai.com> To: mpi-collcomm@cs.utk.edu Cc: mpi-formal@cs.utk.edu In-Reply-To: Steven Ericsson Zenith's message of Wed, 25 Nov 92 13:22:31 -0600 <9211251922.AA09015@brisk.kai.com> Subject: MPI collective communication... From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 Observation on the following: all2all() equivalent to every task in a group calling broadcast. Why doesn't this cause deadlock in the group? Nah! It does cause deadlock. I was thinking about this yesterday over my stuffed Tofu :-). Even if we permit the broadcast to be nonsynchronized we have the problem I described earlier with defining the behavior of parallel broadcasts. If all2all is nonsynchronized then the order of received values must be nondeterministic. (|| i for N: broadcast(C, e[i])) || (|| k for N:|| j for N: receive(C, v[k, j])) i.e., the order of values from e in v is nondeterministic. Now maybe I'm missing something that has to do with the TMC perspective - in any case, I have never seen the use of such a construction in an application. If we do specify a deadlock free behavior for all2all is it desirable given this nondeterminism? I know it's implementation will be tricky to get right. Can we have some vendor comments please? I have assumed here that the values broadcast are the same type. Steven Footnote: The syntax (|| i for N: broadcast(C, e[i])) || (|| k for N:|| j for N: recieve(C, v[k, j])) illustrates N broadcasts implementing the all2all, where N is the number of participants, in parallel with N parallel groups of N (parallel) receives. From owner-mpi-formal@CS.UTK.EDU Thu Dec 3 08:38:36 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA27950; Thu, 3 Dec 92 08:38:36 -0500 Received: by CS.UTK.EDU (5.61++/2.8s-UTK) id AA14104; Thu, 3 Dec 92 08:25:15 -0500 Received: from sun2.nsfnet-relay.ac.uk by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA14100; Thu, 3 Dec 92 08:24:53 -0500 Via: uk.ac.southampton.ecs; Thu, 3 Dec 1992 13:06:23 +0000 From: ms@parallel-applications-centre.southampton.ac.uk Via: calvados.pac.soton.ac.uk (plonk); Thu, 3 Dec 92 12:42:35 GMT Received: from maddog.pac.soton.ac.uk by calvados.pac.soton.ac.uk; Thu, 3 Dec 92 12:47:17 GMT Date: Thu, 3 Dec 92 12:48:37 GMT Message-Id: <9688.9212031248@maddog.pac.soton.ac.uk> To: mpi-formal@cs.utk.edu Subject: Formal Specification Language Cc: igl@ecs.soton.ac.uk, md@ecs.soton.ac.uk, mbh@ecs.soton.ac.uk, ajgh@ecs.soton.ac.uk, ms@parallel-applications-centre.southampton.ac.uk Hello Formal Specification Subcommittee My name is Dr Mike Surridge - Tony Hey asked me to look in on the MPI conversations and to contribute as much as possible. Here I reply to the first interesting message I saw from Steve Zenith. I am currently working at the University of Southampton Parallel Applications Centre, where we have a wide range of applications projects running with UK industrial partners. I am nominally in charge of our Scientific/Engineering number-crunching activities, but I am also active in our Real-Time computing division working on simulation and control problems. In the past I was the author of ECCL which was the first efficient message passing system implementing arbitrary occam channel communication connect- ivity on (almost) arbitrary networks, and a direct ancestor of the Esprit- funded VCR system. I happen to believe that synchronous point-to-point communications provide the cleanest possible semantics. Unfortunately, most parallel scientific computation makes use of asynchronous communication - partly to avoid having to deal with deadlock issues (the leave it to the system school), but also for performance reasons. All the major vendors support asynchronous communication primitives for these applications, and clearly expect synchronisation to be used only where it is really needed. Last time I looked at CSP it was unable to handle asynchronous communication at all. Have there been further developments of which I am unaware? If not, then should CSP be adopted for this exercise, given that the interface we are trying to specify will have to be accepted as an alternative (or successor) to systems such as Intel's NX/2, and will therefore have to include an asynch- ronous capability. I suggest some serious thought be given to this, lest (a) formal specification become marginalised and ignored or (b) the entire MPI exercise become irrel- evant. -- Mike Surridge (ms@uk.ac.soton.ecs) From owner-mpi-formal@CS.UTK.EDU Thu Dec 3 12:08:52 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA04135; Thu, 3 Dec 92 12:08:52 -0500 Received: by CS.UTK.EDU (5.61++/2.8s-UTK) id AA18491; Thu, 3 Dec 92 12:00:04 -0500 Received: from relay1.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA18481; Thu, 3 Dec 92 12:00:00 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay1.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA02150; Thu, 3 Dec 92 11:32:42 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 113121.20596; Thu, 3 Dec 1992 11:31:21 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-92031301 for ) id AA04572; Thu, 3 Dec 1992 09:59:02 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA01933; Thu, 3 Dec 92 09:58:59 -0600 Date: Thu, 3 Dec 92 09:58:59 -0600 Message-Id: <9212031558.AA01933@brisk.kai.com> To: uunet!parallel-applications-centre.southampton.ac.uk!ms@uunet.UU.NET Cc: mpi-formal@cs.utk.edu, igl@ecs.soton.ac.uk, md@ecs.soton.ac.uk, mbh@ecs.soton.ac.uk, ajgh@ecs.soton.ac.uk, ms@pac.soton.ac.uk In-Reply-To: uunet!parallel-applications-centre.southampton.ac.uk!ms's message of Thu, 3 Dec 92 12:48:37 GMT <9688.9212031248@maddog.pac.soton.ac.uk> Subject: Formal Specification Language From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 Hi Mike, You are batting from the wrong wicket. It is not anyones intention to adopt CSP as the MPI but to use CSP as the specification language - for which it is ideally suited. Nonsynchronized (what you called "asynchronous") communication can very easily be specified in CSP. There is a bias against CSP in some quarters because of an association with Occam. I'm sorry to say that we did CSP a disservice when we defined Occam - I was intimately involved with David May in that language design and I wrote the Occam 2 reference manual - the defacto standard, published under the name INMOS Limited ;-). You shouldn't judge CSP by your experiences with Occam. CSP is a rich and comprehensive specification mathematics, a very useful formal tool that can be applied to good effect in this case. Incidently, my last language design, Ease, also used CSP as the formal basis and that language doesn't use communication as a model for interaction at all but rather uses logically shared data structures - specified using CSP. To conclude, in current proposals for MPI, I see nothing that prohibits the use of CSP as the specification form and what is more I believe that a CSP specification will assist implementors in a way that other forms will not. Steven Ericsson Zenith From owner-mpi-formal@CS.UTK.EDU Thu Dec 3 15:38:40 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA10807; Thu, 3 Dec 92 15:38:40 -0500 Received: by CS.UTK.EDU (5.61++/2.8s-UTK) id AA26873; Thu, 3 Dec 92 15:27:00 -0500 Received: from sun2.nsfnet-relay.ac.uk by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA26866; Thu, 3 Dec 92 15:26:46 -0500 Via: uk.ac.southampton.ecs; Thu, 3 Dec 1992 19:07:14 +0000 Via: brewery.ecs.soton.ac.uk; Thu, 3 Dec 92 18:41:47 GMT From: Ian Glendinning Received: from holt.ecs.soton.ac.uk by brewery.ecs.soton.ac.uk; Thu, 3 Dec 92 18:43:56 GMT Date: Thu, 3 Dec 92 18:49:09 GMT Message-Id: <3194.9212031849@holt.ecs.soton.ac.uk> To: mpi-formal@cs.utk.edu, ms@parallel-applications-centre.southampton.ac.uk Subject: Re: Formal Specification Language Cc: md@ecs.soton.ac.uk, mbh@ecs.soton.ac.uk > From ms@uk.ac.soton.pac Thu Dec 3 12:45:02 1992 > My name is Dr Mike Surridge - Tony Hey asked me to look in on the MPI > conversations and to contribute as much as possible. Here I reply to > the first interesting message I saw from Steve Zenith. Tony also asked me to contribute to discussions, as well as Mark Debbage and Mark Hill. The four of us should shortly be added to the mpi-formal mailing list. > Last time I looked at CSP it was unable to handle asynchronous communication > at all. Have there been further developments of which I am unaware? If not, Ummm, as far as I'm aware CSP has always been able to handle asynchronous communication, and I agree with Steve that it would be an ideal tool to capture the semantics. The fact that it is not a primitive concept in the language doesn't mean it can't represent it - you just need to have things like explicit buffer processes. In fact, this is no bad thing, because it allows you to specify more precisely than is usually done how the buffers behave. I think it is crucial that no matter what is ultimately settled on for the standard, it should have clearly defined semantics. This is an area that has been sadly neglected for most existing message passing systems, particularly the mailbox-based ones. For example, suppose a program specifies in a receive call that it will block until it receives a message from processor number 10. If the first message that arrives is from processor 11, and is followed by a message from processor 10, what happens? Does the program remain indefinitely blocked, or does the arrival of the second message wake it up? It seems to me that this is the sort of area where different implementors could make different choices, if no definite behaviour were specified by a standard. There are other forms of behaviour on the other hand that you might choose to deliberately specify as being arbitrary. Ian -- I.Glendinning@ecs.soton.ac.uk Ian Glendinning Tel: +44 703 593368 Dept of Electronics and Computer Science Fax: +44 703 593045 University of Southampton SO9 5NH England From owner-mpi-formal@CS.UTK.EDU Thu Dec 3 17:38:41 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA12597; Thu, 3 Dec 92 17:38:41 -0500 Received: by CS.UTK.EDU (5.61++/2.8s-UTK) id AA00766; Thu, 3 Dec 92 17:35:01 -0500 Received: from relay2.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA00761; Thu, 3 Dec 92 17:34:58 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay2.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA08388; Thu, 3 Dec 92 17:34:59 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 173206.14795; Thu, 3 Dec 1992 17:32:06 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-92031301 for ) id AA02775; Thu, 3 Dec 1992 15:22:24 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA03117; Thu, 3 Dec 92 15:22:23 -0600 Date: Thu, 3 Dec 92 15:22:23 -0600 Message-Id: <9212032122.AA03117@brisk.kai.com> To: mpi-formal@cs.utk.edu Cc: uunet!parallel-applications-centre.southampton.ac.uk!ms@uunet.UU.NET, igl@ecs.soton.ac.uk, md@ecs.soton.ac.uk, mbh@ecs.soton.ac.uk, ajgh@ecs.soton.ac.uk, ms@ecs.soton.ac.uk In-Reply-To: uunet!parallel-applications-centre.southampton.ac.uk!ms's message of Thu, 3 Dec 92 19:54:48 GMT <10067.9212031954@maddog.pac.soton.ac.uk> Subject: Asynchronous Communication. From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 Mike, I'm having trouble following you. Even in the cases you describe - as much as they might be undesirable - we can formally specify the behavior using CSP (without any kind of extension). Ian's observations are correct. The rest of your remarks seem to suggest that you would advocate no formal specification at all. Consider this: it is possible to simply specify in CSP a buffer of infinite size and the rest of the subcommittees may prefer that the formal specification says that at this point. I also do not understand your point about the term "asynchronous". You missed a message I posted earlier where I pointed out this common mistake. "Synchronous" and "asynchronous" have quite particular meanings, in EE for example, it is a common mistake in CS circles to use these terms to refer to synchronized and non-synchronized communication. This group is also tasked with defining a glossary of terms by the way. Steven P.S. Not being picky - but I do prefer being called Steven to Steve ;-) From owner-mpi-formal@CS.UTK.EDU Fri Dec 4 12:39:11 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA02494; Fri, 4 Dec 92 12:39:11 -0500 Received: by CS.UTK.EDU (5.61++/2.8s-UTK) id AA20516; Fri, 4 Dec 92 12:35:17 -0500 Received: from relay2.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA20492; Fri, 4 Dec 92 12:35:06 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay2.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA29585; Fri, 4 Dec 92 12:35:07 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 123304.23021; Fri, 4 Dec 1992 12:33:04 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-92031301 for ) id AA09657; Fri, 4 Dec 1992 10:25:25 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA04860; Fri, 4 Dec 92 10:25:24 -0600 Date: Fri, 4 Dec 92 10:25:24 -0600 Message-Id: <9212041625.AA04860@brisk.kai.com> To: mpi-formal@cs.utk.edu, uunet!parallel-applications-centre.southampton.ac.uk!ms@uunet.UU.NET Cc: igl@ecs.soton.ac.uk In-Reply-To: uunet!parallel-applications-centre.southampton.ac.uk!ms's message of Fri, 4 Dec 92 10:13:54 GMT <10680.9212041013@maddog.pac.soton.ac.uk> Subject: Non-synchronized Communication. From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 Apologies for calling you `Steve' - I think Tony called you that when he asked me to put forward some ideas to you. No problem. Tony picked up the habit from old colleagues at INMOS. All I am doing is pointing out a particular programming device, which probably occurs most often erroneously by accident (or design), but which does have a legitimate use in certain parallel algorithms. My knowledge of CSP is far from comprehensive, by I think it is possible that the situation I have described lies outside it. If you can tell me how CSP would cope with this situation then please do (gently, please). OK. The situation you decribe does not lie outside of CSP and I'll explain why - as gently as I can :-) The situation I was trying to describe is as follows : Process A makes use of a variable `x', which B may update at any time (in this context we will assume by sending a message to A). Process A reads the value of x at various points, but does not care how often it has been updated, nor even whether B was in the act of updating x (either the old or new value being acceptable). Processes A and B are clearly non-synchronised, but further than that A does not even synchronise with the arrival of a message (messages just arrive, updating x). There are a couple of ways to tackle this. Firstly, you will I imagine concede that you have described an interleaving whatever the order of the reads and writes are. Thus the communication is itself an interleaved process that, in effect, shares possession of x and that actually interacts with B. Let A = S;no_sync_send(x);R then A||B = (S;((c ? x -> SKIP) ||| R)) || c:B properly describes the situation you outline. Although S is the process before the communication is instigated, which you didn't allow for - so it doesn't exactly match your description. The interleaving allows events in R using x to be interleaved safely and in any order. It would be worth pointing out to implementors that they could just throw this communication away since according to your "don't care" semantics the input could be the last thing the program ever does - and thus, with no further dependence, it can be optimized away ;-). If x were really a variable I wanted to share with B; i.e., I didn't really want a compiler to optimize it away because it is mapped onto a transducer somewhere then a more tricky solution would have created a process having sole prossession of x and specified all interactions on x as communication events. Your version of non-synchronized communication formally involves the creation of a process that is interleaved with the remainder of the process performing the communication and in the absence of any synchronization with that interleaved communication can be deleted from the program with not effect. Steven From owner-mpi-formal@CS.UTK.EDU Mon Dec 7 19:10:06 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA09779; Mon, 7 Dec 92 19:10:06 -0500 Received: by CS.UTK.EDU (5.61++/2.8s-UTK) id AA27298; Mon, 7 Dec 92 18:54:32 -0500 Received: from sun2.nsfnet-relay.ac.uk by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA27292; Mon, 7 Dec 92 18:54:28 -0500 Via: uk.ac.southampton.ecs; Mon, 7 Dec 1992 23:53:51 +0000 Via: brewery.ecs.soton.ac.uk; Mon, 7 Dec 92 23:47:27 GMT From: Ian Glendinning Received: from holt.ecs.soton.ac.uk by brewery.ecs.soton.ac.uk; Mon, 7 Dec 92 23:49:17 GMT Date: Mon, 7 Dec 92 23:54:55 GMT Message-Id: <6607.9212072354@holt.ecs.soton.ac.uk> To: mpi-formal@cs.utk.edu Subject: Re: Asynchronous Communication. > From zenith%kai.com%kailand@net.uu.uunet Fri Dec 4 00:56:04 1992 > I also do not understand your point about the term "asynchronous". You > missed a message I posted earlier where I pointed out this common > mistake. "Synchronous" and "asynchronous" have quite particular meanings, > in EE for example, it is a common mistake in CS circles to use these > terms to refer to synchronized and non-synchronized communication. > > This group is also tasked with defining a glossary of terms by the way. Good, I think that that is very important. I saw your previous message, and was going to ask you to elucidate. Could you explain what the particular meanings you allude to are, and also the common mistakes? Ian From owner-mpi-formal@CS.UTK.EDU Thu Dec 10 13:39:48 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA09699; Thu, 10 Dec 92 13:39:48 -0500 Received: by CS.UTK.EDU (5.61++/2.8s-UTK) id AA18681; Thu, 10 Dec 92 13:16:24 -0500 Received: from sun2.nsfnet-relay.ac.uk by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA18668; Thu, 10 Dec 92 13:16:15 -0500 Via: uk.ac.southampton.ecs; Thu, 10 Dec 1992 17:48:11 +0000 Via: brewery.ecs.soton.ac.uk; Thu, 10 Dec 92 17:41:29 GMT From: Ian Glendinning Received: from holt.ecs.soton.ac.uk by brewery.ecs.soton.ac.uk; Thu, 10 Dec 92 17:43:07 GMT Date: Thu, 10 Dec 92 17:49:00 GMT Message-Id: <9700.9212101749@holt.ecs.soton.ac.uk> To: mpi-formal@cs.utk.edu Subject: Blocking and synchrnous/ized behaviour > From zenith%kai.com%kailand@net.uu.uunet Fri Dec 4 00:56:04 1992 > I also do not understand your point about the term "asynchronous". You > missed a message I posted earlier where I pointed out this common > mistake. "Synchronous" and "asynchronous" have quite particular meanings, > in EE for example, it is a common mistake in CS circles to use these > terms to refer to synchronized and non-synchronized communication. > > This group is also tasked with defining a glossary of terms by the way. Steven, since you haven't yet responded to my request for clarification on the above, why don't I stir things up a bit by explaining my prefered terminology. The clearest terminology I have come across in this area is that of Meiko's CSTools, which distinguishes between blocking / non-blocking and synchronous / asynchronous behaviour as orthogonal concepts. Blockingness is purely to do with whether a send or receive call returns immediately or not. Non-blocking calls leave the user to poll the completion status of the communication, or to make a separate call to wait for it's completion. Blocking calls do not return until the communication is complete. What it means for the communication to have completed is defined by whether it is synchnonous or not. Synchronous sends are not deemed to be complete until the message has been successfully delivered into the user buffer at the receiving end, while asynchronous ones are deemed to be complete as soon as the message has been copied out of the user buffer at the sending end by the system, and it is safe to re-use that buffer. There is no difference between a synchronous and an asynchronous receive call. Either a message has been received or it has not. Ian From owner-mpi-formal@CS.UTK.EDU Mon Dec 14 03:30:33 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA02209; Mon, 14 Dec 92 03:30:33 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA09849; Mon, 14 Dec 92 03:30:22 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Mon, 14 Dec 1992 08:30:21 GMT Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from relay2.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA09841; Mon, 14 Dec 92 03:30:19 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay2.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA01056; Mon, 14 Dec 92 03:30:19 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 032954.8547; Mon, 14 Dec 1992 03:29:54 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-92031301 for ) id AA27637; Sun, 13 Dec 1992 22:41:31 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA03451; Sun, 13 Dec 92 22:41:29 -0600 Date: Sun, 13 Dec 92 22:41:29 -0600 Message-Id: <9212140441.AA03451@brisk.kai.com> To: mpi-formal@cs.utk.edu, I.Glendinning@ecs.soton.ac.uk Cc: parallel-applications-centre.southampton.ac.uk!ms@ecs.soton.ac.uk In-Reply-To: Ian Glendinning's message of Thu, 10 Dec 92 17:28:55 GMT <9672.9212101728@holt.ecs.soton.ac.uk> Subject: Life after CSP... and synchronous behavior. From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 My apologies for a week of silence; a broken right arm (I took my children ice skating :-( ), business and a head cold have occupied me. So in what follows forgive an increased density of typos etc.. First, to continue the discussion of the case described by Mike in Southampton. > From ms@uk.ac.soton.pac Mon Dec 7 18:25:12 1992 The central point in my "don't care" semantics is not that process A doesn't care WHETHER `x' has been written to by process B. The particular property of the system I require is that A will allow an indefinite number of writes by B between any two accesses of x. Having realised that this is the nub, it is clear that the way to proceed is by creating a third process (presumably spawned by A), and allocating variable x to this process, both A and B interacting with this process to access the variable. From: Ian Glendinning Date: Mon, 7 Dec 92 23:44:59 GMT Yes, this is what I had in mind too. The `third process' holding the variable could for example repeatedly execute what in occam would be an ALT (non-deterministic choice) between two channels, requesting to write to or read from the variable. Personally I rather like the fact that using CSP notation forces you to make any non-determinism explicit like this. I guess you could also hold x in a process subordinate to an interleaving of A and B, which also makes the non-determinisim explicit. There are several points here. Firstly the choice you describe in not a non-deterministic choice in the CSP sense. Occam has complex semantics here. What is incorrectly called an "alternation" in Occam (it should have been called "choice") wraps several CSP constructs into one - badly. Occam's ALT a ? x P b.in ? readx b.out ! x is deterministic; i.e., the choice is knowable even though in the case where both input events occur simultaneously, the selection between them is non-deterministic. It is important to understand where the non-determinism lies here - in the above case non-determinism only occurs in the selection of two simultaneous inputs. Whereas, the difficult Occam syntax ALT true & skip P true & skip Q describes a non-deterministic choice that in CSP is simply described as P [] Q [] being my representation of the CSP general choice operator. The reason I used interleaving to describe Mikes case is that it is closer to the actual use in a language, like FORTRAN, than the distinct process case. Your suggestion to use a distinct process is not an unreasonable one but it reads more into the description than was there at face value. Many users of the specification may have trouble reasoning about the use of x in a complex expression as a communication. In anycase it does not make much difference, as we shall see. Yes, I was a bit confused by Steven's last message - he didn't seem to be describing the same situation that you had in mind, and it was at this point that the brushing up on CSP was required. Having now refreshed my memory a bit on the syntax and semantics, it seems to me that: A||B = (S;((c ? x -> SKIP) ||| R)) || c:B is not at all what Mike had in mind, so the optimizing out of the communication is not a problem. Firstly this misses the essential point that B can update x many times but, more importantly, according to my understanding the value of x is not available to R. I must confess that I could be wrong here, since I can't find any explicit reference in the CSP book to the usage rules for variables in conjunction with the ||| operator. I'm assuming that they're the same as those for ||. You are wrong. Firstly, || and ||| are not equivalent and the composition of two processes by interleaving does indeed permit use of the same variable since all events including such a variable are distinct by that interleaving. Secondly, even though the above only shows a single input to x you can replace it with as many as you like to the same effect - I was being concise. The essential point is not, therefore, missed; x can be updated as many times as you like between two uses in R. Now let us consider the case where we use a distinct process to model the behavior of x. A || ( X:(c ! x -> X [] c ? x -> X) || B So, I have a intermediary process that is recusively making a truely non-deterministic choice on each iteration. If this *is* the specification then I can always chose to do the input OR the output; ergo I can optimize one or the other away and cause deadlock ;-) So you did not mean nondeterministic choice. Therefore, we need to make the mechanism deterministic but now we have a more difficult problem: TERMINATION. How am I to know when B has finished updating x? See, as I said in my earlier mail, this is more tricky than it may at first appear. Now the synchronous / asynchronous issue. I may have to concede that common usage has corrupted these terms beyond what I find intuitive. My bias comes from a presense in the microelectronics industry and having very pedantic architects for company. The meaning usually applied to "synchronous" is that, given a set of sequences the events in each sequence behave in a lock step fashion. The term usually applies across a system of identical sequences. "Asynchronous" is the inverse. So, we can describe a set of parallel processes as behaving synchronously (often applied to SIMD or VLIW architectures) or asynchronously (often applied to MIMD). I hate using the same term to mean different things and therefore I argue we should use the term "synchronized" not "synchronous" to mean "blocking" and "non-synchronized" not "asynchronous" to mean "non-blocking" when we discuss communication. Steven From owner-mpi-formal@CS.UTK.EDU Mon Dec 14 14:05:05 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA20714; Mon, 14 Dec 92 14:05:05 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA11555; Mon, 14 Dec 92 14:04:55 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Mon, 14 Dec 1992 19:04:54 GMT Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from relay1.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA11533; Mon, 14 Dec 92 14:04:52 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay1.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA01415; Mon, 14 Dec 92 14:04:50 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 140219.28072; Mon, 14 Dec 1992 14:02:19 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-92031301 for ) id AA18368; Mon, 14 Dec 1992 10:36:00 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA00362; Mon, 14 Dec 92 10:35:59 -0600 Date: Mon, 14 Dec 92 10:35:59 -0600 Message-Id: <9212141635.AA00362@brisk.kai.com> To: I.Glendinning@ecs.soton.ac.uk Cc: mpi-formal@cs.utk.edu In-Reply-To: Ian Glendinning's message of Thu, 10 Dec 92 17:49:00 GMT <9700.9212101749@holt.ecs.soton.ac.uk> Subject: Blocking and synchrnous/ized behaviour From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 Ian, Your description of the MeiKo usage is consistent with with my understanding. The usage of synchronous and asynchronous refers to the behavior of processes and events; synchronous behavior describes processes taking part, collectively, in a single event; asynchronous behavior describes the inverse. Blocking and Non-blocking are direct analogs of synchronized and non-synchronized and more accurately describe the case. I understand that this is a subtle point here and I'm sure that some people will consider it overly pedantic, so I'd welcome some other comments. I'm trying to decide which of the current proposals we can begin to consider for the specification process. I'm inclined to start with the Lusk and Gropp implementation document the other documents I have seen introduce too many uncertain concepts. Has anyone else read the available documents? Steven From owner-mpi-formal@CS.UTK.EDU Mon Dec 14 19:14:58 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA00850; Mon, 14 Dec 92 19:14:58 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA27785; Mon, 14 Dec 92 19:14:47 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Tue, 15 Dec 1992 00:14:38 GMT Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from relay1.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA27777; Mon, 14 Dec 92 19:14:37 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay1.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA19399; Mon, 14 Dec 92 19:14:35 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 191323.29698; Mon, 14 Dec 1992 19:13:23 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-92031301 for ) id AA02632; Mon, 14 Dec 1992 17:38:27 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA04629; Mon, 14 Dec 92 17:38:25 -0600 Date: Mon, 14 Dec 92 17:38:25 -0600 Message-Id: <9212142338.AA04629@brisk.kai.com> To: I.Glendinning@ecs.soton.ac.uk, mpi-formal@cs.utk.edu In-Reply-To: Steven Ericsson Zenith's message of Mon, 14 Dec 92 10:35:58 EST Subject: Blocking and synchrnous/ized behaviour From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 Remember that typo I asked forgiveness for :-) This is it: in my earlier mail I used general choice where I meant to use nondeterministic OR. General choice is what the first Occam Alt I described maps on to. The Lobelia is beginning to clear my head :-) Steven From owner-mpi-formal@CS.UTK.EDU Thu Dec 17 12:32:58 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA02670; Thu, 17 Dec 92 12:32:58 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA09509; Thu, 17 Dec 92 12:32:51 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Thu, 17 Dec 1992 17:32:50 GMT Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from sun2.nsfnet-relay.ac.uk by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA09501; Thu, 17 Dec 92 12:32:46 -0500 Via: uk.ac.southampton.ecs; Thu, 17 Dec 1992 17:32:17 +0000 Via: brewery.ecs.soton.ac.uk; Thu, 17 Dec 92 17:25:48 GMT From: Ian Glendinning Received: from holt.ecs.soton.ac.uk by brewery.ecs.soton.ac.uk; Thu, 17 Dec 92 17:26:52 GMT Date: Thu, 17 Dec 92 17:33:24 GMT Message-Id: <15485.9212171733@holt.ecs.soton.ac.uk> To: mpi-formal@cs.utk.edu Subject: Re: Blocking and synchrnous/ized behaviour > From: Steven Ericsson Zenith Steven, I'm replying to mpi-formal rather than directly to you, so you don't get two copies of this message. > Your description of the MeiKo usage is consistent with with my > understanding. The usage of synchronous and asynchronous refers to the I'm glad to hear that. > describe the case. I understand that this is a subtle point here and I'm > sure that some people will consider it overly pedantic, so I'd welcome > some other comments. Well, given that the draft proposal of Dongarra, Hempel, Hey and Walker identified three of the possible four perumutations of the above, I think people are aware of the possibilities. I feel strongly that it is the job of mpi-formal to set down clearly how the selected modes of communication behave in these respects. I don't think it is being pedantic to want to know what your program actually does! > I'm trying to decide which of the current proposals we can begin to > consider for the specification process. I'm inclined to start with the > Lusk and Gropp implementation document the other documents I have seen > introduce too many uncertain concepts. Has anyone else read the > available documents? I have not seen the Lusk and Gropp document. Could you e-mail me a copy? (I assume it exists in machine readable form.) The only one I have seen is the one I already mentioned, by Dongarra/Hempel/Hey/Walker. Ian From owner-mpi-formal@CS.UTK.EDU Mon Dec 21 19:27:37 1992 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA23685; Mon, 21 Dec 92 19:27:37 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA16702; Mon, 21 Dec 92 19:27:26 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Tue, 22 Dec 1992 00:27:25 GMT Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from sun2.nsfnet-relay.ac.uk by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA16694; Mon, 21 Dec 92 19:27:22 -0500 Via: uk.ac.southampton.ecs; Tue, 22 Dec 1992 00:27:18 +0000 Via: brewery.ecs.soton.ac.uk; Tue, 22 Dec 92 00:20:04 GMT From: Ian Glendinning Received: from holt.ecs.soton.ac.uk by brewery.ecs.soton.ac.uk; Tue, 22 Dec 92 00:20:44 GMT Date: Tue, 22 Dec 92 00:27:40 GMT Message-Id: <16320.9212220027@holt.ecs.soton.ac.uk> To: mpi-formal@cs.utk.edu Subject: Re: Life after CSP... and synchronous behavior. > From zenith%kai.com%kailand@NET.UU.uunet Mon Dec 14 08:52:51 1992 Hi, yet again I've taken rather longer than I'd have liked to reply to Steven's message, but there was a lot to reply to. Here goes. > There are several points here. Firstly the choice you describe in not a > non-deterministic choice in the CSP sense. Occam has complex semantics > here. What is incorrectly called an "alternation" in Occam (it should > have been called "choice") wraps several CSP constructs into one - > badly. Occam's > > ALT > a ? x > P > b.in ? readx > b.out ! x This looks a bit odd. Was "readx" really meant to be just "x"? I guess it doesn't really matter to the point at issue, but it still reads oddly. > is deterministic; i.e., the choice is knowable even though in the case > where both input events occur simultaneously, the selection between them > is non-deterministic. It is important to understand where the I guess it's true that general choice reduces to vanilla choice in this case, i.e.: (c -> P [] d -> Q) = (c -> P | d -> Q) if c <> d and in that sense it it's deterministic. I'm afraid I seem to have muddied the waters by my loose use of terminology. When I refered to "non- deterministic choice", what I really meant was the [] operator, which I now realise is properly called "general choice". I've always called the other operator "non-deterministic or" in the past (can't draw that one so easily...) > non-determinism lies here - in the above case non-determinism only > occurs in the selection of two simultaneous inputs. Whereas, the > difficult Occam syntax > > ALT > true & skip > P > true & skip > Q > > describes a non-deterministic choice that in CSP is simply described as > > P [] Q > > [] being my representation of the CSP general choice operator. I console myself that Steven got confused here too, as he later pointed out. This should of course be P n Q where "n" means non-deterministic or (same as "non-deterministic choice"?). > You are wrong. Firstly, || and ||| are not equivalent and the > composition of two processes by interleaving does indeed permit use of > the same variable since all events including such a variable are > distinct by that interleaving. Secondly, even though the above only Could you please elaborate? What do you mean by "events including such a variable"? What does it mean for an event to include a variable? Maybe you are justifying why it is ok for interleaved processes to share variables, but surely this is just a matter of definition. Is this made explicit anywhere for CSP? It certainly does not appear to be done in the CSP book, where the restriction for the || operator is imposed over and above its other properties. There is no explicit statement for the ||| operator. One could interpret this either way. > Now let us consider the case where we use a distinct process to model > the behavior of x. > > A || ( X:(c ! x -> X [] c ? x -> X) || B > > So, I have a intermediary process that is recusively making a truely > non-deterministic choice on each iteration. If this *is* the ^^^^^^^^^^^^ Well I think that is the key question! I'd have been inclined to use two separate channels, one in and one out - but then I'm just an old occam hack ;-) > specification then I can always chose to do the input OR the output; > ergo I can optimize one or the other away and cause deadlock ;-) So you Is this really the case? If A or B tries to output a value on channel c that is not the same as its current value then surely only the input branch of the choice may be activated. > did not mean nondeterministic choice. Therefore, we need to make the No, I didn't. > Now the synchronous / asynchronous issue. I may have to concede that > common usage has corrupted these terms beyond what I find intuitive. My > bias comes from a presense in the microelectronics industry and having > very pedantic architects for company. The meaning usually applied to > "synchronous" is that, given a set of sequences the events in each > sequence behave in a lock step fashion. The term usually applies across > a system of identical sequences. "Asynchronous" is the inverse. So, we > can describe a set of parallel processes as behaving synchronously > (often applied to SIMD or VLIW architectures) or asynchronously (often > applied to MIMD). I hate using the same term to mean different things > and therefore I argue we should use the term "synchronized" not > "synchronous" to mean "blocking" and "non-synchronized" not > "asynchronous" to mean "non-blocking" when we discuss communication. It still doesn't sound like we're speaking the same language here. We need a total of four different words, and you seem to be saying we ditch (a)synchronous completely and use (a)synchronized as a synonym for (non)blocking, leaving us only two alternatives. We must sort out some terminology we can agree on the meaning of! Ian From owner-mpi-formal@CS.UTK.EDU Fri Feb 5 00:33:11 1993 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA29214; Fri, 5 Feb 93 00:33:11 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA27501; Fri, 5 Feb 93 00:32:04 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Fri, 5 Feb 1993 00:31:56 EST Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from relay2.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA27482; Fri, 5 Feb 93 00:31:55 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay2.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA09369; Fri, 5 Feb 93 00:32:02 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 002918.13015; Fri, 5 Feb 1993 00:29:18 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-93012701) id AA09184; Thu, 4 Feb 1993 18:56:01 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA05164; Thu, 4 Feb 93 18:56:00 -0600 Date: Thu, 4 Feb 93 18:56:00 -0600 Message-Id: <9302050056.AA05164@brisk.kai.com> To: mpi-formal@cs.utk.edu, mpi-pt2pt@cs.utk.edu Cc: Subject: Concerns. From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 I have to agree with Steve Otto and confess more than a little anxiety at this end. It seems to me that we are much too concerned with being all things to all men and I am absolutely convinced that a mix and match philosophy is a recipe for disaster: not that it can't be implemented or specified but purely from the usability point of view. We should be able to provide more wizardly and wise power by providing less not more! We would do better to ensure that the issues we address are those that we all currently understand well or that we have time to defer to assure ourselves that new forms or compositions are at least well concieved. The latter is impossible in the six months we have allotted ourselves. If we really want people to use MPI it has to be straight forward and at least no more complex than existing systems. If we can't decide on a *concise* set of wisely restricted forms for send and recieve, if you really believe we have to provide all forms, then I suggest this effort may be premature. Steven From owner-mpi-formal@CS.UTK.EDU Fri Feb 5 00:33:11 1993 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA29213; Fri, 5 Feb 93 00:33:11 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA27513; Fri, 5 Feb 93 00:32:09 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Fri, 5 Feb 1993 00:32:08 EST Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from relay1.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA27503; Fri, 5 Feb 93 00:32:05 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay1.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA05696; Fri, 5 Feb 93 00:32:02 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 002920.13036; Fri, 5 Feb 1993 00:29:20 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-93012701) id AA09357; Thu, 4 Feb 1993 19:11:45 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA05200; Thu, 4 Feb 93 19:11:44 -0600 Date: Thu, 4 Feb 93 19:11:44 -0600 Message-Id: <9302050111.AA05200@brisk.kai.com> To: mpi-formal@cs.utk.edu, mpi-pt2pt@cs.utk.edu Cc: Subject: Composition. From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 What is the meaning of these sequential compositions? 1) two non-blocking sends to the same destination? 2) a non-blocking send and a blocking send to the same destination? 3) a non-blocking send and a broadcast? 4) two non-blocking receives? 5) a non-blocking receive and a blocking receive? and so on ... I suspect different machine vendors may have different views. Steven ps. mpi-formal members are refered to mpi-pt2pt. From owner-mpi-formal@CS.UTK.EDU Fri Feb 5 05:44:43 1993 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA12746; Fri, 5 Feb 93 05:44:43 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA18976; Fri, 5 Feb 93 05:44:25 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Fri, 5 Feb 1993 05:44:24 EST Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from relay1.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA18968; Fri, 5 Feb 93 05:44:23 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay1.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA00876; Fri, 5 Feb 93 05:44:20 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 054326.7482; Fri, 5 Feb 1993 05:43:26 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-93012701) id AA16580; Thu, 4 Feb 1993 23:45:25 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA06410; Thu, 4 Feb 93 23:45:23 -0600 Date: Thu, 4 Feb 93 23:45:23 -0600 Message-Id: <9302050545.AA06410@brisk.kai.com> To: mpi-formal@cs.utk.edu, mpi-pt2pt@cs.utk.edu Cc: Subject: Be brave. Be sure. From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 It will probably come as no surprise that I, for one, have no fear of being politically incorrect in these matters ;-) I am not afraid to say that I think at this stage it would be a very good idea to define only process composition and blocking send/recv. The rest comes - more or less - as a construction of the other two. Process ids are simply a many to one channel descriptor - implementable by a single process, non-synchronized communication is simply a process creation, broadcast is a composition of N sends with N receives, and such an interface can be implemented by all the available technologies. In addition this simplification would greatly aid the task of the poor programmer. Where is the innovation in this forum? It seems that we are pandering to the lowest common denominator. Has noone learnt anything in the past 7/8 years? Otherwise we should simply take an existing system (PVM for example, though there are many well designed MP systems) and adopt it as the accepted standard, work from that point and be done with it. The interface efforts of the Unix community (e.g., DCE and sockets) may well out run this one. Steven From owner-mpi-formal@CS.UTK.EDU Fri Feb 5 06:07:04 1993 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA17736; Fri, 5 Feb 93 06:07:04 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA20552; Fri, 5 Feb 93 06:05:42 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Fri, 5 Feb 1993 06:05:41 EST Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from marge.meiko.com by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA20403; Fri, 5 Feb 93 06:04:45 -0500 Received: from hub.meiko.co.uk by marge.meiko.com with SMTP id AA27476 (5.65c/IDA-1.4.4); Fri, 5 Feb 1993 06:04:40 -0500 Received: from float.co.uk (float.meiko.co.uk) by hub.meiko.co.uk (4.1/SMI-4.1) id AA16231; Fri, 5 Feb 93 11:04:37 GMT Date: Fri, 5 Feb 93 11:04:36 GMT From: jim@meiko.co.uk (Paul Kelly) Message-Id: <9302051104.AA16231@hub.meiko.co.uk> Received: by float.co.uk (5.0/SMI-SVR4) id AA06680; Fri, 5 Feb 93 11:02:53 GMT To: zenith@kai.com Cc: mpi-formal@cs.utk.edu, mpi-pt2pt@cs.utk.edu In-Reply-To: Steven Ericsson Zenith's message of Thu, 4 Feb 93 23:45:23 -0600 <9302050545.AA06410@brisk.kai.com> Subject: Be brave. Be sure. Content-Length: 896 Steve, > I am not afraid to say that I think at this stage it would be a very > good idea to define only process composition and blocking send/recv. > The rest comes - more or less - as a construction of the other two. > Process ids are simply a many to one channel descriptor - > implementable by a single process, non-synchronized communication is > simply a process creation, broadcast is a composition of N sends with > N receives, and such an interface can be implemented by all the > available technologies. You just described occam. One thing I have learnt from the last 10 years is that that's NOT ENOUGH. -- Jim James Cownie Meiko Limited Meiko Inc. 650 Aztec West Reservoir Place Bristol BS12 4SD 1601 Trapelo Road England Waltham MA 02154 Phone : +44 454 616171 +1 617 890 7676 FAX : +44 454 618188 +1 617 890 5042 E-Mail: jim@meiko.co.uk or jim@meiko.com From owner-mpi-formal@CS.UTK.EDU Fri Feb 5 13:10:13 1993 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA09171; Fri, 5 Feb 93 13:10:13 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA16585; Fri, 5 Feb 93 13:09:45 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Fri, 5 Feb 1993 13:09:44 EST Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from relay1.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA16577; Fri, 5 Feb 93 13:09:42 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay1.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA05018; Fri, 5 Feb 93 13:09:39 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 130848.19776; Fri, 5 Feb 1993 13:08:48 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-93012701) id AA04173; Fri, 5 Feb 1993 10:16:24 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA07622; Fri, 5 Feb 93 10:16:22 -0600 Date: Fri, 5 Feb 93 10:16:22 -0600 Message-Id: <9302051616.AA07622@brisk.kai.com> To: jim@meiko.co.uk Cc: mpi-formal@cs.utk.edu, mpi-pt2pt@cs.utk.edu In-Reply-To: Paul Kelly's message of Fri, 5 Feb 93 13:20:43 GMT <9302051320.AA16757@hub.meiko.co.uk> Subject: Be brave. Be sure. From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 Thanks Jim (or is it Paul) for the name correction (via private mail)... I know what I'm suggesting - and yes, though I hate to admit it, it is the Occam model more or less. Though you shouldn't allow your distaste for the language to deflect you from the qualities of it's communication model. The inadequacies of that language are many but when it comes to the communication model (CSP) it is fundamental. All I'm suggesting here is that we do not make the other mistake, that of providing so much that it is neither managable by us or our intended audience. Either we are prepared to provide something better than currently exists based on a good understanding of our collective experience with mature concepts or we should start from an existing system, with all its flaws, and work from there. This is not a forum for invention. I should qualify my comments to reiterate that in fact I am looking to this forum to provide a consistent interface for low level implementation in operating systems and code generation. I never want any of my general purpose users using message passing as a means to program machines. And if you gave me just processes and blocking send and receive that *would* be enough. As someone who has written many message passing programs (using Express and other libraries, as well as Occam and CSP), and made it my business over the years to talk to others who have, I have to tell you that the fewer well conceived choices you give me the happier I am and, in my experience, the user is. I just don't believe those people who say we have to provide every form - it is counter to all my experience with users (no doubt, there are users here who will insist on being provided with every variant ;-) - but you will have seen that manifestation before. ). One way to look for evidence to support or denounce this is to undertake an investigation. Find an array of *applications*, not systems tools etc. but "real" applications, and identify the subset of functionality used. My bet is that you will discover the subset is small, the place where non-blocking communication is used is on machines where the process model implementation is inadequate, and that code that does not fit into my simple model is not readily portable. Steven From owner-mpi-formal@CS.UTK.EDU Fri Feb 5 18:13:42 1993 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA14882; Fri, 5 Feb 93 18:13:42 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA04240; Fri, 5 Feb 93 18:13:16 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Fri, 5 Feb 1993 18:13:14 EST Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from relay2.UU.NET by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA04230; Fri, 5 Feb 93 18:13:12 -0500 Received: from uunet.uu.net (via LOCALHOST.UU.NET) by relay2.UU.NET with SMTP (5.61/UUNET-internet-primary) id AA24058; Fri, 5 Feb 93 18:13:17 -0500 Received: from kailand.UUCP by uunet.uu.net with UUCP/RMAIL (queueing-rmail) id 181248.24131; Fri, 5 Feb 1993 18:12:48 EST Received: from brisk.kai.com (brisk) by kailand.kai.com via SMTP (5.65d-93012701) id AA01338; Fri, 5 Feb 1993 17:10:16 -0600 Received: by brisk.kai.com (920330.SGI-92101201) id AA08601; Fri, 5 Feb 93 17:10:15 -0600 Date: Fri, 5 Feb 93 17:10:15 -0600 Message-Id: <9302052310.AA08601@brisk.kai.com> To: mpi-formal@cs.utk.edu, mpi-pt2pt@cs.utk.edu Cc: In-Reply-To: Steven Ericsson Zenith's message of Fri, 5 Feb 93 10:16:22 EST Subject: Be brave. Be sure. From: Steven Ericsson Zenith Sender: zenith@kai.com Organization: Kuck and Associates, Inc. 1906 Fox Drive, Champaign IL USA 61820-7334, voice 217-356-2288, fax 217-356-5199 From: srwheat@cs.sandia.gov (Stephen R. Wheat) ... But, while they continue to wait, their livelyhoods depend upon their ability to get the best performance from these MP beasts as possible. Even assembly language is still a useful tool for them, case in point: tuned libraries where interfaces are defined but the library code is certainly not portable. The fact that your users are programming using message passing suggests that they are certainly also prepared to use assembler when necessary. The reason they use MP is the same reason they use assembler at times: there is no higher level way currently to achieve what they want with the performance they require on the machines they are using. ;-) Evenso, when I've asked people (physicists and so on) with some experience programming such machines this question they have confirmed that they use MP as reluctantly as they use assembler - it's just that sometimes it's unavoidable. Some of those people are at Sandia. I certainly would not want to deprive them of their lively hood and there are exceptions - of course. Some people really enjoy the challenge of writing MP code, just as they enjoy the challenge of writing assembler - me too at times ;-) But the pro's and con's of message passing as a programming model, and the alternatives, are not the issues here. While we may have different motivations we do all understand the importance of MP at some level. Certainly it should be usable by "users" in the absence of anything better. In fact I'd contend that my recent calls serve those that do have to use it well - wizard or not. I am not calling for us to take power away from users - on the contrary - I'm calling for greater utility and usability through simplicity. I am calling for us to focus on things we understand well and to avoid invention. I do not feel that such simplicity will fail to serve wizards - your implication is that wizards are only attracted to complexity: this surely is not true. In addition, it is my opinion that there is way too little experience with compiler generated messaging to have such a concept meet the "maturity/experience" criteria upon which we wish to base MPI. No argument here - but then this isn't an objective of MPI. As for overlapped messaging, I dare say that EVERY code here ... I am not saying that non-synchronizing send is a "bad thing" - I am saying there is a simpler way of looking at these things. Define the fundamentals and work from there. We have been arguing about the nuances of buffer behavior without getting a real feel for our base objectives. You can build all you want - if you really want it - with fundamental and well understood components - it makes a great opportunity for third party software vendors like Parasoft and DSL. Buffering characteristics are likely to remain a choice based on hardware design and we should leave such things alone in our interface design. Now I understand that most machine vendors have a variety of approaches - and that is exactly why we should should be careful. But I cannot believe the solution for MPI is the union of those approaches - though it may be some component of the intersection. Isn't our objective to provide a Message Passing Interface that will allow people who want to write portable (or transportable) MP code to do so? And to provide for compiler writers and architects - people like me - who are just looking for a consistent interface on MP machines? Doesn't usability have a right to be at the fore of our concerns? If this is the case then we do need some well conceived abstraction or we must adopt an existing system and refine it. When it comes right down to it, I really don't mind which. I would like though to take a program written in MPI and simply transform it into another MPI program for execution on a machine with different characteristics. What I've seen so far is going to make it very very hard to do that. I'm only likely to want to do literal translation on a machine identical to the original target - it would be nice to permit simple transformations and checking (for deadlock for example) ... wouldn't it? Incidently, in addition to my architects point of view I do still design message passing systems and program them - so I hope I qualify as a user too. ;-) Steven From owner-mpi-formal@CS.UTK.EDU Sun Feb 7 23:04:51 1993 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA12670; Sun, 7 Feb 93 23:04:51 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA25212; Sun, 7 Feb 93 23:04:28 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Sun, 7 Feb 1993 23:04:27 EST Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from antares.mcs.anl.gov by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA25204; Sun, 7 Feb 93 23:04:26 -0500 Received: from donner.mcs.anl.gov by antares.mcs.anl.gov (4.1/SMI-GAR) id AA08906; Sun, 7 Feb 93 22:04:24 CST Received: by donner.mcs.anl.gov (4.1/GCF-5.8) id AA01757; Sun, 7 Feb 93 22:04:22 CST Message-Id: <9302080404.AA01757@donner.mcs.anl.gov> To: mpi-formal@cs.utk.edu Subject: Activities of the Formal Methods subcommittee In-Reply-To: Your message of "Fri, 05 Feb 93 17:10:15 CST." <9302052310.AA08601@brisk.kai.com> Date: Sun, 07 Feb 93 22:04:21 CST From: Rusty Lusk Dear Formal Subcommittee, particularly Steven: I have been trying without much success to educate myself in the area of formal standards. I found an article in IEEE Software (September, 1990) that seems to apply to us, "The Case for Formal Methods in Standards". Here is a relevant paragraph: The introduction of formal methods can be achieved only through education. Appreciating the need for a gradual migration toward a fuller use of formal methods, the International Standards Organization has recommended a three-phase plan to introduce formal methods into standards: In phase 1, where the use of formal methods is restricted due to lack of expertise, their use should be encouraged as a parallel activity to formulating the standard in a natural language. Insights gained from the formalization may contribute to the quality of the standard by, for example, improving error detection. The MPI committee as a whole certainly seems to be in this situation ("use of formal methods is restricted due to lack of expertise"), and certainly I myself am. So I think our job should be primarily to demonstrate the use of formal methods to clarify what the committee is considering, rather than try to direct it. (Here I am really just following Steven's first posting on this subcommittee mailing list.) The minutes of the last meeting give a pretty good indication of what level the committee is thinking of. I myself am certainly one of the ones arguing for including a lot into the standard. It seems to me that formal methods should be of great use, although I have no experience with them whatever. Here's what would help me a lot: Could someone in this group who does have some of this experience demonstrate how one would specify the three different send operations that we more or less settled on in the straw votes at the last meeting? These are: a send that blocks until its buffer can be reused (the message has been delivered to the network) a send that doesn't block at all (you execute a wait later, which waits until the message has been delivered to the network) a "synchronized" send that blocks until the receiver has copied the message off the network into its local memory Regardless of what eventually appears in the standard, these are the kinds of things that we are talking about and I, for one, would be very interested in seeing formal specification demonstrated on just these three operations. This is also the sort of thing I said the formal methods subcommittee would do before the next meeting. CSP I have heard about. More recently I have found that many people use Z. There is also something called ASLAN, and apparently the POSIX people have invented something called LIS for doing this sort of thing. Does anyone have any experience with any of these? It would be nice if the above exercise could be carried out in more than one language, for comparison's sake. Regards, Rusty From owner-mpi-formal@CS.UTK.EDU Wed Feb 10 16:46:05 1993 Received: from CS.UTK.EDU by surfer.EPM.ORNL.GOV (5.61/1.34) id AA04980; Wed, 10 Feb 93 16:46:05 -0500 Received: from localhost by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA24088; Wed, 10 Feb 93 16:45:41 -0500 X-Resent-To: mpi-formal@CS.UTK.EDU ; Wed, 10 Feb 1993 16:45:40 EST Errors-To: owner-mpi-formal@CS.UTK.EDU Received: from ssdintel.ssd.intel.com by CS.UTK.EDU with SMTP (5.61++/2.8s-UTK) id AA24080; Wed, 10 Feb 93 16:45:38 -0500 Received: from tualatin.SSD.intel.com by SSD.intel.com (4.1/SMI-4.1) id AA14891; Wed, 10 Feb 93 13:45:36 PST Date: Wed, 10 Feb 93 13:45:36 PST Message-Id: <9302102145.AA14891@SSD.intel.com> Received: by tualatin.SSD.intel.com (4.1/SMI-4.0) id AA03909; Wed, 10 Feb 93 13:45:33 PST From: Bob Knighten Sender: knighten@SSD.intel.com To: mpi-formal@cs.utk.edu, mpi-lang@cs.utk.edu Subject: POSIX LIS Reply-To: knighten@SSD.intel.com (Bob Knighten) As part of the POSIX work a "Draft TCOS-SSC Technical Report -- Programming Language Independent Specification Methods" was written. This has served as the basis for the language independent specification of the various system interfaces that have been developed. This is *NOT* a formal specification method, but has as its purpose "to assist and coordinate the development of functional specifications and language bindings by defining an abstract model, and providing guidelines for the use of that model in the development of new functional specifications, the dirivation of a base standard from an existing language binding, and the development of new language bindings to a functional specification." "The model is primarily intended for use in developing language-independent specifications for operating system and related services, and language bindings for procedural programming languages." [The quotation is from the Scope and Purpose of the report.] This guide was never completely finished and Paul Rabin (OSF), the principal author, recommends that it be used in conjunction with the P1003.1LIS which provides a very large example. Paul Rabin expects that some extensions to the current guide will be necessary for MPI, just as extensions will be necessary for the POSIX Real-Time and Threads work. He is interested in working with us to develop common extensions. I can provide copies of the POSIX LIS and both the P1003.1 LIS and the P1003.16 C binding to the P1003.1 LIS as well. [P1003.1LIS is about 380 pages and P1003.16 is about 300 pages so I don't want to drop these books on people unless they are actually desired.] A formal specification of MPI is quite desirable, but I am doubtful that we can achieve it in the time we have available. A language independent specification of the sort developed within POSIX is, I believe, essential to provide the common base for all of the language bindings we wish to provide. -- Bob Robert L. Knighten | knighten@ssd.intel.com Intel Supercomputer Systems Division | 15201 N.W. Greenbrier Pkwy. | (503) 629-4315 Beaverton, Oregon 97006 | (503) 629-9147 [FAX]