1.5 Model of Computation

To describe the structure of a process network, we introduce the notions of process type set and data type. A process type set defines the set of process types. Each process type has a set of input ports and a set of output ports. With each port we associate a data type. A process network consists of a set of processes and a set of channels. A channel connects a process output port to a process input port of the same data type. Each port is connected to precisely one channel.

To describe the communication between the processes we provide three functions called read, write, and select that can be called from within a process. The informal meaning of these functions is as follows. The read function consumes data from an input port and stores it in a local variable of the process. The write function copies the value of a local variable to an output port. The select function selects an input or output port that eventually will produce or consume data, respectively. To formalize the semantics of these functions we associate with each port at any time the number of tokens that it has transferred up to now and the number of tokens that it has committed to transfer up to now but that not have been transferred yet. To this end we introduce the following definitions.

Definition 1.5.1   Let $p$ be a port. Then at any time

• $c(p)$ denotes the number of tokens transferred through $p$,
• $n(p)$ denotes the number of tokens committed but not yet transferred through $p$,
• $m(p)$ denotes the port connected to $p$ by a channel, and
• $v(p,k)$ denotes the value of the $k$-th token at $p$.

Following the approach of Martin [8], the communication mechanism is based on the following assumptions. For all channels it must hold at any time that a write action is not blocked, the number of consumed tokens does not exceed the number of produced tokens, and the functionality is first-in-first-out.

Axiom 1.5.1   Let $(p,m(p))$ be a channel from output port $p$ to input port $m(p)$. Then the following invariants hold

• $n(p) = 0$,
• $c(m(p)) \leq c(p)$, and
• $\forall_{0 \leq i < c(m(p))} v(m(p),i)=v(p,i)$.

Under these assumptions we define the semantics of the read, write, and select functions using preconditions and postconditions as follows. Note that these functions stall when their postcondition cannot be satisfied. Furthermore, note that the write function is non-destructive which means that the variables of the producing process keep their values.

Definition 1.5.2   Let $p$ be an input port of type $t$, $x$ an array of type $t$, and $n$ a positive integer indicating a number of tokens. Then action read$(p,x,n)$ is defined by

• precondition $c(p) = N$, and
• postcondition $c(p) = N+n \wedge \forall_{0 \leq i < n} (x[i] = v(p,N+i))$.

Definition 1.5.3   Let $p$ be an output port of type $t$, $x$ an array of type $t$, and $n$ a positive integer indicating a number of tokens. Then action write$(p,x,n)$ is defined by

• precondition $c(p) = N \wedge \forall_{0 \leq i < n} (x[i] = v(p,N+i))$, and
• postcondition $c(p) = N+n \wedge \forall_{0 \leq i < n} (x[i] = v(p,N+i))$.

Definition 1.5.4   Let $k$ be a positive integer, $p_1$ up to $p_{k}$ ports, $n_1$ up to $n_k$ positive integers indicating requests for numbers of tokens, and $s$ a positive integer no larger than $k$ indicating the index of the selected port. Then action $s =$select $(p_1,n_1,\dots,p_k,n_k)$ is defined by

• precondition $\forall_{1 \leq i \leq k} (c(p_i) = N_i)$, and
• postcondition $\forall_{1 \leq i \leq k} (c(p_i) = N_i) \wedge 1 \leq s \leq k \wedge \Diamond (N_s+n_s \leq c(m(p_s)))$.

Following temporal logic theory, the symbol $\Diamond$ means eventually. Hence, the select function selects a port such that the current number of transferred tokens through this port plus the requested number of tokens is eventually smaller than or equal to the number of transferred tokens through the connected port. If we consider an input port $p_s$, then this port is a candidate for selection if the corresponding output port $m(p_s)$ will eventually produce enough tokens to complete a read action of $n_s$ tokens. If we consider an output port $p_s$, then this port is a candidate for selection if the corresponding input port $m(p_s)$ will eventually consume the tokens produced by a write action of $n_s$ tokens. Note that the select function has no effect on the number of transferred tokens, i.e., it does not produce or consume data.

To describe the functionality of the processes we use a sequential programming language. We introduce an additional function called execute to abstract from the implementation of the functionality in the sequential programming language. To this end, the functionality between two communication actions has to be annotated with one or more execute actions. These execute actions annotate the computation requirements of the processes; they do not provide additional functionality.