## Dataflow Language{#sec:dataflow_language}

The AGREE language is derived from the *synchronous dataflow language*
Lustre. Let us expand on this definition somewhat. A *dataflow* language
consists of a set of *equations* that assign *variables* in which a
variable can be computed as soon as its *data dependencies* have been
computed. As an example, consider a system that computes the values of
two variables, `X` and `Y`, based on four inputs: `a`, `b`, `c`, and `d`:

![A dataflow model and its associated set of equations](../../media/image11.png){#fig:dataflow_model_equations .class width=80%}

This diagram is to be read left-to-right, with the inputs "flowing"
through the system of operators to create the outputs at the right side.
The diagram can be represented more concisely as a set of equations, as
shown at right. We name the inputs to the dataflow model *input
variables* and all variables that are computed by the model *state
variables.*

As the basis of a high-level programming language, the dataflow model
has several merits:

-   It is a completely functional model without side effects. This
    feature makes the model well-suited to formal verification and
    program transformation. It also facilitates reuse, as a module will
    behave the same way in any context into which it is embedded.

-   It is a naturally parallel model, in which the only constraints on
    parallelism are enforced by the data-dependencies between variables.
    This allows for parallel implementations to be realized, either in
    software, or directly in hardware.

Dataflow models can be either *synchronous* or *asynchronous*. In an
asynchronous dataflow model, the outputs of the system are continually
recomputed depending on the inputs to the system. In the synchronous
model, however, real-time is broken into a sequence of instants in which
the model is recomputed. The synchronous model is better suited to
translation into a programming language, as it more naturally matches
the behavior of a computer program. Therefore, all of the dataflow-style
languages adopt some form of this approach.

The variables in a dataflow model are used to label a particular
computation graph; they are not used as constraints. Therefore, it is
incorrect to view the equations as a set of constraints on the model: a
set of equations such as {`X = 2a/Y`, `Y = X + d`} does not correspond to an
operator network because X and Y mutually refer to one another. Put
another way, there is no way to arrange the variables from left to right
such that each can be computed. This is shown in @fig:dataflow_model_cyclic, where the
bold red-lines indicate the cyclic dependencies. Such a system may have
no solution or infinitely many solutions, so cannot be directly used as
a deterministic program. If viewed as a graph, these sets of equations
have *data dependency cycles*, and are considered incorrect.

![A Dataflow Model with Cyclic Dependencies](../../media/image12.png){#fig:dataflow_model_cyclic .class width=80%}

However, in order for the language to be useful, we must be able to have
mutual reference between variables. To allow benign cyclic dependencies,
a *delay operator* (`prev`) is added. The operator returns the value of an
expression, delayed one instant. For example: {`X = 2a + Y`;
`Y = (prev(X, 1)) + d`} defines a system where `X` is equal to `2a` plus the current value
of `Y`, while `Y` is equal to the *previous* value of `X` (with value in the
initial instant set to `1`) plus the current value of `d`. Systems of
equations of this form always have a single solution. The delay operator
is also the mechanism for recording state about the model. For example,
we can construct a counter over the natural numbers by simply defining
the equation: `x = prev(x+1, 1)`.

Finally, some notion of selection is added to assignment expressions. In
Lustre, this is simply an if/then/else statement. From these elements,
at its core, a dataflow program can be viewed as simply a set of input
variables and assignment equations of the form
{`X`~`0`~ = `E`~`0`~, `X`~`1`~ = `E`~`1`~, ..., `X`~`n`~ = `E`~`n`~}
that must be acyclic in terms of data dependencies.

