IntroductionDirected Events, Traces and ReorderingTraces ModelHealthiness ConditionsOperatorsTraces/Successes ModelHealthiness ConditionsOperatorsTraces/Successes/Failures ModelHealthiness Conditions OperatorsSuccesses/Failures/Divergences ModelHealthiness ConditionsOperatorsConclusionModels for Data-Flow Sequential ProcessesMark B. JosephsCentre for Concurrent Systems and Very-Large-Scale Integration,Faculty of BCIM, London South Bank University,103 Borough Road, London SE1 0AA, [email protected]. A family of mathematical models of nondeterministic dataflow is introduced. These models are constructed out of sets of traces, suc-cesses, failures and divergences, cf. Hoare’s traces model, Roscoe’s stable-failures model and Brookes and Roscoe’s failures/divergences model ofCommunicating Sequential Processes. As in CSP, operators are definedthat are convenient for constructing processes in the various models.1 IntroductionConsider sequential processes that communicate via input streams and outputstreams (FIFO buffers of unlimited storage capacity), as in Kahn-MacQueendata-flow networks [17, 18]. They are capable of the following actions:– selectively reading data from their input streams,– unreading (pushing back) data to their input streams,– writing data to their output streams, and– termination.Processes can be composed in parallel. In particular, an output stream ofone process may be connected to an input stream of a second process. Anydatum written to the output stream by the first process should be transferred(eventually and automatically) to the input stream, where it becomes availablefor reading by the second process.Processes can also be composed in sequence. When one process terminatesits successor starts to execute. An important point here (implicit in [10]) is thattermination does not destroy the contents of input streams and output streams.Some years ago, the author, Hoare and He [16, 9] devised a process algebrafor (nondeterministic) data flow, as a variant of Communicating Sequential Pro-cesses (CSP) [12]. (Part of this work was reproduced in [13].) We showed howto simplify the failures/divergences model [4] of CSP so that refusal sets wereno longer required; failures could instead be identified with (finite) ‘quiescenttraces’ [7, 14] or ‘traces of completed computation sequences’ [23].At the time we did not consider a binary angelic choice operator, nor se-quential composition. One purpose of this article is to rectify those omissions.Note that termination is modelled in CSP by a special symbol√(success) [11],A.E. Abdallah, C.B. Jones, and J.W. Sanders (Eds.): LNCS 3525, pp. 85–97, 2005.c Springer-Verlag Berlin Heidelberg 2005CSP25,86 M.B. Josephsbut that would not work for what we shall call Data-Flow Sequential Processes(DFSP). The solution is to create a ‘stub’ (a sequence of unread inputs) whentermination occurs and there are no pending outputs, cf. [10, 6].Another purpose of this article is to show how the more recent stable-failuresmodel [27] of CSP can be adapted for DFSP. Indeed, a series of increasinglysophisticated models for DFSP will be introduced in a step-by-step manner,cf. [22]. Note that fairness issues, the focus of [23, 2, 3], are not addressed inthese models.The rest of this article is organised as follows. In Section 2, we recall thereordering relation [16, 9] between traces of directed events, a relation that cap-tures the essence of data-flow communication. Subsequently, we define partial-correctness models (in Sections 3–5) and a total-correctness model (in Section 6)for DFSP, guided by what Roscoe [27] has done for CSP. In each case we considerthe semantics of operators appropriate to the model. Conclusions are drawn inSection 7.2 Directed Events, Traces and ReorderingA process is associated with an alphabet A, a (possibly infinite) set of symbols1,partitioned into an input alphabet I and an output alphabet O.AsymbolinIdesignates the transfer of a particular datum to a particular input stream; a sym-bol in O designates the transfer of a particular datum from a particular outputstream. Such directed events are considered to be atomic, i.e., instantaneous.Following Hoare [11], we define a trace to be a finite sequence (string) of sym-bols in A that expresses the occurrence of events over time as a linear order. Inrespect of a process that communicates through streams of unbounded capacity,however, two facts are noteworthy:1. Events are independent if they are in the same direction but act upon dif-ferent streams.2. The occurrence of an input event does not depend upon the prior occurrenceof an output event.The first fact would justify taking a more abstract approach, namely, to followMazurkiewicz [21] by defining a trace to be an equivalence class on A∗. The twofacts taken together would justify being more abstract still, namely, to followPratt [24] by defining a trace to be a partially-ordered multiset (pomset) on A.For example, if a and b are independent input events and c and d are indepen-dent output events, then the strings cabd and cbad are equivalent, but the onlyordering between events is given by a<dand b<d.1To be more concrete, we have in mind compound symbols with s.d referring tostream s and datum d. We would then require that s0.d0∈ I and s1.d1∈ O impliesthat s0= s1. Moreover, if D is a data type associated with stream s, then s.d ∈ Afor all d ∈ D.Models for Data-Flow Sequential Processes 87Anyway, the possibility of reordering a trace without affecting the behaviourof a process was recognized in [7, 28] and was formalised as a relation t  u (treorders u) between strings t and u in [16]. Reordering allows– input symbols to be moved in front of other symbols– output symbols to be moved behind other symbolsprovided the symbols being swapped are associated with different streams. Inother words, it is the strongest reflexive transitive relation (i.e. preorder) suchthat tabu  tbau if a ∈ I or b ∈ O, a and b designating transfers on differentstreams. For example, if a and b are independent input events and c and d areindependent output events, then badc cabd. Various properties of the reorderingrelation have been proved in [19, 20].More abstractly, t and u are equivalent (t  u) if and only if t  u and u  t.Note that, if two traces are equivalent, then reordering one into the other involvesonly the swapping of input symbols and the