Towards a Proof of the Kahn Principle

for Linear Dynamic Networks

Arie de Bruin & Shan-Hwei Nienhuys-Cheng
{arie, cheng}@cs.few.eur.nl
Department of Computer Science
Erasmus University Rotterdam
H4-19, P.O. Box 1738, 3000DR Rotterdam

Abstract

We consider dynamic Kahn-like data flow networks, i.e. networks consisting of deterministic processes each of which is able to expand into a subnetwork. The Kahn principle states that such networks are deterministic, i.e. that for each network we have that each execution provided with the same input delivers the same output. Moreover, the principle states that the output streams of such networks can be obtained as the smallest fixed point of a suitable operator derived from the network specification.
This paper is meant as a first step towards a proof of this principle. For a specific subclass of dynamic networks, linear arrays of processes, we define a transition system yielding an operational semantics which defines the meaning of a net as the set of all possible interleaved executions. We then prove that, although on the execution level there is much nondeterminism, this nondeterminism disappears when viewing the system as a transformation from an input stream to an output stream. This result is obtained from the graph of all computations. For any configuration such a graph can be constructed. All computation sequences that start from this configuration and that are generated by the operational semantics are embedded in it.

Keywords : the Kahn principle, dynamic data flow networks, process creation, the fork statement, operational semantics, nondeterministic transition systems

1 Introduction

A dataflow network consists of a number of parallel processes which are interconnected by directed channels. Processes communicate with each other only through these channels, there is no sharing of variables. The channels act as possibly infinite FIFO queues and communication is asynchronous.

In his seminal paper [K74] Kahn describes such networks in which the processes are deterministic. He characterizes the processes as functions, transforming input histories into output histories, where a history models a stream of values which has appeared on a channel during a computation. He then states a result which has become known as the Kahn principle since then: a network consisting of deterministic nodes as a whole also computes a history function, and for each set of input histories on the input channels the output histories can be obtained as the smallest solution of a set of equations derived from the network.

Stated somewhat differently: the nondeterminism caused by the asynchronicity of the computing processes does not lead to global nondeterminism in the history level I/O behaviour of the network. In essence there is only one computation possible, modeled by a function transforming input histories into output histories (although certain unfairly interleaved computations?might not deliver the full output histories but only prefixes thereof).

Kahn's paper was quite influential, it has been the basis of much subsequent research. Work has been done to define evaluation strategies or implementations of dataflow networks, e.g. [KM77, AG78, F82], and several authors have proved the Kahn principle for certain subsets of networks [C72, A81, LS89].