Distributing Synchronous Programs Using Bounded Queues

Marco Zennaro and Raja Sengupta

Center for Collaborative Control of Unmanned Vehicles
{zennaro,raja}@[Link]

Abstract

This paper is about the distribution of a sub-class of SIMULINK programs [11] across networks. We describe a
software architecture and proofs of its correctness. We also show our current implementation works by distributing
a system with three SIMULINK blocks across three machines communicating over an 802.11b wireless LAN. The
distributed implementation preserves the synchronous semantic.

I. INTRODUCTION

This paper is about the distribution of a sub-class of SIMULINK programs [11] across networks. We describe a
software architecture and proofs of its correctness. We also show our current implementation works by distributing
a system with three SIMULINK blocks across three machines communicating over an 802.11b wireless LAN. The
distributed implementation preserves the synchronous semantic.
The results in this paper apply only to SIMULINK programs without causal loops (see section 2.) Our compilation
targets execution in a network of sequential machines communicating over reliable FIFO channels with bounded
memory. This execution model fits the GALS (Globally Asynchronous Locally Synchronous) architecture [14]. The
class of Simulink programs we consider lie within the endochronous programs [14]. [14] provides an existence
proof for the solutions in this paper. However, no algorithm computing on a finitary representation of synchronous
system is given.
The mathematical content of the paper is as follows. We define a synchronous [4] and asynchronous composition
operator. The synchronous composition operator is SIMULINK-like. The asynchronous composition operator is
similar to Kahn Networks [2], except we have bounded queues. We present an algorithm to translate a synchronous
program into an asynchronous one and prove the translation preserves the synchronous semantics in the sense of [14].
The main result is that the implementation is a monomorphism with respect to the synchronous and asynchronous
compositions. The translation is computable. It is chosen to mimic the SIMULINK compiler. The asynchronous
composition can be implemented over reliable FIFO channels. Thus the mathematics supports a software architecture
distributing SIMULINK programs overlayed on the Real Time Workshop compiler.
In our software process the user provides a SIMULINK system. We decompose it into its atomic blocks. To
each input or output port of each block we add S-functions to interface with the FIFO queues. We then use Real
Time Workshop to compile each collection of block and S-functions. Finally we add a queue manager for each
input-output connection between blocks.
 Our compilation process does no global scheduling computation. Thus if a block is changed, only the block itself
needs to be re-compiled. On the other hand, our methods only preserve the synchronous semantic in the sense of
the logical order of computation. It does not try to meet any real-time deadlines.
In practice this work has been motivated by the vision based navigation of unmanned air vehicles [1]. The UAV
has an on-board camera that looks forward in the desired direction of travel. Each frame captured by the camera
is communicated to the ground over a wireless link. The image is processed. This is an anytime computation.
While the image is being processed the UAV enters a holding pattern. Once the image is processed and the region
ahead declared safe, a command to fly forward is sent up to the UAV, enabling it to advance and capture the next
image. The process repeats. Since each input must result in an output, the synchronous programming paradigm is
an appropriate one. On the other hand, the anytime computation in the loop, means we can only hope to enforce
its logical correctness.
There is a large body of related work. SIMULINK is only one amongst other synchronous programming
languages such as ESTEREL ([7]-[8]), LUSTRE ([9]), and SIGNAL ([10]). [12]-[13] propose algorithms to
distribute particular subsets of ESTEREL programs for an execution environment like ours. The algorithm starts
with a single synchronous program and splits it into synchronous subsystems intercommunicating through an
asynchronous medium. This approach rigorously preserves the synchronous semantics but does not maintain or
exploit any modular structure in the original synchronous program while building the asynchronous distributed
implementation. Consequently, modification to one module of the synchronous program may require re-compilation
and re-distribution of the entire system. [3] discusses mathematical results similar to ours for Lustre programs
translated into Kahn Networks. Our results are also related to [24] on synchronous dataflow networks.
This paper is organized as follows. Section 2 defines synchronous systems and section 3 asynchronous ones.
Section 4 formulates the problem mathematically. Section 5 presents the map from synchronous to asynchronous
systems, discusses its abstraction of SIMULINK, and proves the map preserves the synchronous semantic. Section
6 presents the main theorem supporting the distribution of Simulink programs. Section 7 presents our software
architecture and a three block example together with the computational result.

II. SYNCHRONOUS SYSTEMS

Several synchronous systems formalisms exists in the literature. The basic idea behind all of them is of a systems
evolving through discrete steps. At every step all the variables are updated and they do not change values until the
next step is taken.

A. STS and STS*

The Synchronous Transition System (STS) formalism, was introduced by Manna and Pnueli in [18]. According
to this model a synchronous system s is given by a couple (Ps , Bs ) where:
• Ps is the set of the I/O ports and state variables of the system;
• Bs is the set of the traces admitted by the system;
 A trace is an infinite sequence of states and a state is a valuation of all the element of Ps . If P is a set of ports,
we denote by σ(P ) a valuation of the ports in the set P and by Λ(P ) the set of the possible valuations of the ports
in P.
This lightweight formalism is easy to handle theoretically but is not finitary (the set of traces is not a finitary object).
Hence it cannot be input to an algorithm. In this paper we propose a slightly different form of STS, the STS*
formalism. The STS* keeps the simplicity of STS, is finitary and easier to relate to a synchronous programming
tools like SIMULINK.
We define a STS* as the tuple (PI , PO , PS , I0 , ψO , ψS , ≺) where:
• PI is the finite set of input ports of the system;
• PO is the finite set of output ports of the system;
• PS is the finite set of state variables of the system;
• I0 are the initial valuation of the state variables in PS ;
• ΨO is a set of computable functions (one for every output port) used to compute the system outputs. The
following holds:
∀ψ ∈ ΨO . ψ : Λ(PIψ ) × Λ(PSψ ) → Λ(POψ )
where PIψ ⊆ PI , PSψ ⊆ PS , and POψ ∈ PO . Ψp denotes the output function with output port p.
• ΨS is a set of computable functions (one for every state variable) used to compute the next system state. The
following holds:
0
∀ψ ∈ ΨS . ψ : Λ(PIψ ) × Λ(PSψ ) → Λ(PSψ ).
0 0
where PIψ ⊆ PI , PSψ ⊆ PS , and PSψ ∈ PS . We denote the unique function for which PSψ = p with ψ p ;
• ≺ is an acyclic partial order over PI ∪ PO ∪ PS expressing the causality relation between input, outputs and
state variables; For example if the output Oi is the sum of the two imputs I1 and I2 then we say that Oi
depends upon I1 and I2 and we write I1 , I2 ≺ Oi . The following holds:
(α, β) ∈≺ ⇔ ∃ψ ∈ ΨO . α ∈ PIψ ∧ β ∈ POψ ∨
∃ψ ∈ ΨS . α ∈ PIψ ∧ β ∈ PSψ

B. STS* semantics

The semantic is given in terms of traces. We define a trace t as an infinite sequence of valuations of PI , PO
and PS , as in a STS system. The ith vector of valuations in a trace t is denoted by ti . We denote with t|P the
projection of the trace t over the set of ports and variables P. Given a trace t, we say that ti satisfies the system s,
denoted s |= ti , if the following holds:

s |= ti ⇔ i = 0 ⇒ ∀p ∈ PS . t0 |p = I0 |p ∧
ψ0p ψp
∀p ∈ PO .ti |p = ψ0p (ti |(PI ∪ PS 0 )) ∧
p
ψS ψp
∀p ∈ PS .ti+1 |p = ψSp (ti |(PI ∪ PS S ))

We say that an STS* system s admits a trace t (or equivalently that the trace t satisfies the system s), and we write
s |= t, as follows:
 s |= t ⇔ ∀i ∈N s |= ti

As long as ≺ is acyclic there are no problems computing the state ti+1 from the state ti and the inputs. On the
contrary, if ≺ has a cycle, it is not always possible to do it. Some authors have assumed out the case ([13]), while
others have looked for fixed-point solution ([19]). In this paper we follow the first approach.

C. Compatible STS* systems composition

We define a composition for STS*. A complex system is created composing subsystems. Not all systems can be
composed. The following conditions must hold: given two STS systems s=(PaI , PaO , PaS , Ia0 , ψaO , ψaS , ≺a ) and
t=(PbI , PbO , PbS , Ib0 , ψbO , ψbS , ≺b ), their composition, denoded with s ×ST S t is defined if and only if:

• PsO ∩ PtO = ∅
• PsS ∩ PtS = ∅
• ≺s ∪ ≺t is acyclic

The first condition ensures the two subsystems do not race to write the same output (this would introduce non-
determinism). The second ensures state variables are local and not shared between components. The third condition
ensures the composed system does not have cyclic causal dependencies between variables. If the three conditions
hold, the systems are said to be compatible and their composition ×ST S is defined as follows:
S
• Ps×t = PsS ∪ PtS , Ps×t
I O
= PsI ∪ PtI , Ps×t = PsO ∪ PtO ;
• I0s×t = P0s ∪ P0t ;
O
• ψs×t = ψsO ∪ ψtO , ψs×t
S
= ψsS ∪ ψtS
• ≺s×t =≺s ∪ ≺t

Therefore ×ST S is a partial function over the STS* set.

Note it is easy to translate a Simulink program into an STS*: every Simulink block can be described by its I/O
ports, state variables and the function used to update them. The semantic of the Simulink composition, programmed
by connecting input and output ports of different components,, is maintained by ×ST S .

Next we state two lemmas. These are used in the theorems presented later. The lemmas merely assert our STS*
formalism has the usual properties of other STS formalisms in the literature.

Lemma 2.1: (STS*, ×ST S ) is a commutative monoid, with the identity element being the empty STS*.

Proof: Follows from the associativity and commutativity of the union operator and by the fact that the identity
element of the union operator is the empty set.

Lemma 2.2: Given two STS* s1 and s2 , s1 ×ST S s2 |= t ⇔ s1 |= t|(PIs1 ∪POs1 ∪PSs1 )∧s2 |= t|(PIs2 ∪POs2 ∪PSs2 )
Proof: The proof is by contradiction. Let’s assume that:

s1 ×ST S s2 |= t ∧ ¬s1 |= t|(PIs1 ∪ POs1 ∪ PSs1 )

(the other case is symmetrical). If this is the case than there is a minimal i ∈ N for which

s1 ×ST S s2 |= ti ∧ ¬s1 |= ti |(PIs1 ∪ POs1 ∪ PSs1 ).

That is to say, there must exist at least one p in POs1 ∪ PSs1 for which,

ψ0p ψp
p ∈ PO ⇒ ti |p 6= ψ p (ti |(PI ∪ PS 0 ))
ψ0p ψp
p ∈ PS ⇒ ti |p 6= ψ p (ti−1 |(PI ∪ PS 0 )).

Pick one such p that is minimal with respect to ≺s1 . Denote it by p0 and assume it is an output port (the case for
a state variable is identical). Since p0 and i are chosen to be minimal

ψp0 ψ p p
∀p ∈ PI ∪ PS p0 ti |p = ψ p (PIψ ∪ PSψ )

Now by the definition of composition of STS*:

ψ0p ψp
ti |p0 = ψ p0 (ti |(PI ∪ PS 0 )

But this contradicts the hyphothesis, hence the lemma is proved.

III. ASYNCHRONOUS SYSTEMS

There are many asynchronous system formalisms in the literature. One of them is the asynchronous version
of STS, called the Asynchronous Transition System (ATS) model, as introduced by Benvenieste in [4]. In ATS
an asynchronous system is a couple (Pa , Ba ) where Pa is the set of I/O ports and Ba the set of the possible
behaviors. A behavior is an infinite sequence of valuations and a valuation is a couple (port number, value). Again
the simplicity of the model makes it easy to handle it theoretically, but we seek a finitary formalism to be input to
an algorithm
Instead we use automata augmented with variables [15]. We call them Reactive Automata (RA). A reactive
automaton is a labeled finite automaton with variables communicating through ports. In this paper we model ports
as bounded queues shared between automata. P is the set of ports and for all ports p in P, β(p) is the bound of p.
Formally an RA is a tuple (L, l0 , V, V0 , PI , PO , T) where
• L: a finite set of locations of the automaton;
• l0 : is the initial location, l0 ∈ L;
• V: is a finite set of variables read and written only by the RA;
• V0 : is the initial value of the variables;
• PI : is a finite set of communication ports, considered as environmental queues read by this RA;
 • PO : is a finite set of communication ports, considered as environmental queues, written by this RA;
• T: is a finite set of labeled transitions of the form (li , lf , (c, a)) where li , lf ∈ L, c is a boolean condition over
V or ?p(v) where p ∈ PI and v ∈ V . A is a sequence of actions defined by the following grammar:
A → nil;
A →!p(v); A where p ∈ PO and v ∈ V
A → v := f (V1 ); A where v ∈ V , V1 ⊆ V, f ∈F(V1 )

Where F(V1 ) is the set of computable functions σ(V1 ) → σ(v), σ being the evaluation map between variables,
ports and their value (single values for variables, lists for ports). We denote with P the set PI ∪ PO . An example
of such an automaton is given in figure 1.

Fig. 1. A simple reactive automaton

The semantic of an RA is in terms of runs and traces. A run of a system is an infinite sequence of tuples (location,
variablesvaluation, action, portsvaluation). The actions are transition or the silent action . The silent action is
introduced to denote the reception of data in a input queue due to an action of the environment. A transition with
an input action remove one element from the queue and copy it on a variable, while a transition with an output
action copy the value of a variable into the end of the queue. A trace is a tuple, where each element of the tuple
is an infinite sequence of variable valuations. For example the following is a representation of the initial part of a
run of the RA in figure 1 for the input port valuation (1) and the output port valuation ∅:

?Input(v1 ) v2 :=v1 +1;!Output(v2 )

(W, (0, 0), (1, ∅)) → (B, (1, 0), (∅, ∅)) → (W, (1, 2), (1, 2))

where W is the wait for input location, B is the busy location the second element is a valuation of v1 and v2 , and
the third element is a valuation for the two ports Input and Output. Mathematically this is the sequence:

(W, (0, 0), ?Input(v1 ), ((1), ∅)), (B, (1, 0), v2 := v1 + 1; !Output(v2 ), (∅, ∅)), (W, (1, 2), −, (∅, (2))), ...

Thus mathematically a run is a sequence of tuples like the one above. The ith tuple in a run r is denoted by ri
and its element are extracted using projection, for example ri |location denotes the location element of the tuple
ri . The ith valuation of a variable v in a trace t is denoted by tvi .
For the previous run, the associated trace is < (0, 1, ...), (0, 2, ...) > where the first element and the second
element are the sequences of valuation of v1 and v2 respectively. Given a run, the associated trace can be computed
by examining the updates of every single variable in the trace. Formally the trace associated with a run is computed
by the following algorithm:

Algorithm Compute Trace

Input: A run r
Output: A trace t
1 create a counter cv for all variable v ∈ V and initialize them to 0
2 ∀vtv0 = V0 |v
3 For all i ∈ N,i > 1 do
4 let (-,-,c,a) = ri |transition
5 if (p ∈ PI ∧ c =?p(v)) ∨ (p ∈
/ PI ∧ c =!p(v)) then do
6 tvi = σ(ri+1 |v)
7 cv + +
8 od
9 if a = v:= f(-) then do
10 tvi = σ(ri+1 |v)
11 cv + +
12 od;
13 od

Given a run r, we say that the tuple ri satisfies a RA w, denoted w |= ri iff the following holds:

w |= ri ⇔ i = 0 ⇒ (r0 |location = l0 ∧ r0 |V = V0 ) ∧ ∀p ∈ P0 r0 |p = ∅∧
ri |action =  ⇒ ∀v ∈ V ri |v = ri+1 |v ∧ ∀p ∈ PO ri |p = ri + 1|p ∧ ∀p ∈ PI ri |p ⊆ ri+1 |p
∃(s, s0 , (c, a)) ∈ T ri+1 |location = s0 ∧ c |= ri |(V ∪ P ) ∧ ri+1 |(V ∪ P ) = act(a, c, ri |(V ∪ P ))

where the function act is defined as follows:

 


 σ if a = nil ∧ c 6=?p(v)


σ0 if a = nil ∧ c =?p(v 0 ) ∧ (∀v ∈ V, v 6= v 0 ⇒ σ 0 |v = σ|v)∧






(∀p0 ∈ P.p0 6= p ⇒ σ 0 |p0 = σ|p0 ) ∧ σ|p 6= ∅ ∧ σ 0 |v 0 = pop(σ|p))





act(a, c, σ) = act(a1 , c, σ 0 ) if a =!p(v); a1 ∧ (∀v ∈ V.σ 0 |v = σ|v) ∧ (∀p0 ∈ P.p0 6= p ⇒ σ 0 |p0 = σ|p0 ) ∧


σ(p) < β(p) ∧ σ 0 |p = push(σ|v, σ|p)






act(a1 , c, σ 0 ) if a = v 0 := f (V ); a1 ∧ (∀v ∈ V.v 6= v 0 ⇒ σ 0 |v = σ|v) ∧ σ 0 |v 0 = f (σ|V ))∧






(∀p0 ∈ P.p0 6= p ⇒ σ 0 |p0 = σ|p0 )



Observe that the values of a port may change value without any input or output by the component, by its
environment, simulating the reception of a message through that port. At the same time an input actions on empty
input ports and output actions on full output ports are not defined. Hence input and output actions are blocking.
A run r satisfies a RA w, denoted w |= r iff:

∀i ∈ N w |= ri

A trace t satisfies a RA w, denoted w |= t iff there is a run r such that w |= r and t is associated to r.
Given a run r, we say that the tuple ri satisfies a RA w, in a closed environment, denoted w |=c ri as follows:
w |=c ri ⇔|= ri ∧ ri |action 6= 
We now define a composition operator ×RA for reactive automata.
Given two distinct reactive automata r1 = (L1 , l01 , V 1 , V01 , P 1 , T 1 ) and r2 = (L2 , l02 , V 2 , V02 , P 2 , T 2 ) we say
that they are compatible if the following conditions holds:
• V1∩V2 =∅
• PO1 ∪ PO2 = ∅
• PI1 ∪ PI2 = ∅
The first condition requires the variables of an RA to be local. The second condition says that only one automaton
can write on a port. The last condition says that only one automaton can read on a port. Hence a port is an
unidirectional point-to-point communication channel in this model.
Their composition r1 ×RA is defined as the automaton (L, l0 , V , V0 , P , T ) where:
• L = L1 × L2
• l0 = (l01 , l02 )
• V = V1∪V2
• V0 = V01 ∪ V02
• PI = PI1 ∪ PI2
• PO = PO1 ∪ PO2
• T = {(s, d, c, a)|((s|L1 , d|L1 , c, a) ∈ T 1 ) ∧ (s|L2 = d|L2 )) ∨ ((s|L2 , d|L2 , c, a) ∈ T 2 ) ∧ (s|L1 = d|L1 ))}
That is to say we are interleaving the execution of the two original automata. In order for the following lemma
to hold the definition of L should be replaced with a commutative operation. This is easy to do, but we adopt this
lightweight form as typically done in the litterature.

Lemma 3.1: (RA, ×RA ) is a commutative monoid, with the identity element being the empty RA.

Proof: Follows from the associativity and commutativity of the union operator and by the fact that the identity
element of the union operator is the empty set.

Q
r∈R r denotes an n-ary composition of RA’s. Lemma 3.1 shows that this is well-defined as the usual extension
of the binary operator ×RA .
Q
Given a run w of the automaton r∈R r, the projection of the w to one of the factors r ∈ R is defined by
projecting every tuple wi of w to the variables and locations of w and extracting only the touple with transition
belongs to r|T and replacing the output transition of r0 6= r witha silent transition.

Lemma 3.2: Given two compatible reactive automata w1 and w2 and given a run r of their composition, the
following hold: (w1 × w2 |=c r) ⇒ (w1 |= r|w1 ∧ w2 |= r|w2 )

Proof: Follows from the observation that every ri in r belongs to r|w1 or to r|w2 because the transition in the
touple belongs to one of the two automata and that if it belongs to r|w1 , by its definition, it does not modify the
location and variables in V w2 and viceversa.

Q
RA can be easily compiled for sequential machine. RA could be compiled in a few ways. The composition
can be carried out generating a third automaton, or the two original automata can be run in parallel as long as
the shared queue are accessed as defined previously. In this case the run of the composed automaton is given
melting together the location and the variable state and not allowing two transition to happen at the same time (if
they do, just pretend one is happening after the other). Following this second approach the composition can be
implemented within a single machine between processes using monitors and semaphors (see [20]), as well as with
3-way handshakes protocols over a network (see [21]). This means we can compose RAs located at different sites
across networks. In section VII we will explore an approach that takes full advantage of the distribution of the code
(maximising pipeline gain).

IV. PROBLEM STATEMENT

Given the definition of STS* and RA given in the previous sections, we can now formally define our problem.
Figure 3 illustrates the research program. First we need to find a way to associate RA and STS* traces, that is to
say we need a trace map χ :TRA →TST S∗ where TRA and TST S are the set of traces of STS and RA respectively.
In [14] the following definition of χ is given:

t0 = χ(t) ⇔ ∀i ∈ N ∀v ∈ V . tvi = t0i |v

Defined as is, χ is an invertible map. We need to find a way to implement STS* as RA while preserving the
synchronous semantic, that is to say we need to find an implementation map φ :STS*→RA such that for all STS*
s and RA r, the following holds:
(r = φ(s) ∧ r |= t) ⇒ s |= χ(t) (1)

If this holds then φ maps a synchronous system into an asynchronous system while preserving the synchronous
semantic. It has been proved in [14] that for the set of endochronous programs such a φ exists. In section V we
define a φ for the class of STS*.
So far we have just obtained what a Simulink compiler does, or what is done in [5]. Given such maps we can
now formulate our problem (like [14]) as follows: we seek a composition operator ×RA such that, for any two
STS* s1 and s2 and RA r1 and r2 , the following holds:

r1 = φ(s1 ) ∧ r2 = φ(s2 ) ∧ r1 ×RA r2 |=c t ⇒ s1 ×ST S s2 |=c χ(t) (2)

If this holds and if the composition operator ×RA can be implemented across a network than this constitutes a way
to distribute the synchronous system s1 ×ST S s2 across a network while preserving its synchronous semantic. It
has been proved in [14] that when the pair (s1 , s2 ) is isochronous than such an operator exists. In section VI we
define an operator ×RA for which we prove that property (2) holds if the two synchronous system are compatible
(as defined in section II) and we provide a protocol to implement it.

Fig. 2. A graphical representation of property (2)

V. IMPLEMENTATION OF SIMULINK SYSTEMS

In this section we consider a φ mapping STS* into RA. We prove that the φ satisfies property 1. In particular
we choose the φ so that the SIMULINK compilers ([23]) is an implementation of φ. Note this is only so for
SIMULINK systems without causal loops.
 A SIMULINK system goes through the following phases ( see figure 3):

• Initialization phase: where sample times and parameters are computed, the blocks execution order is determined,
and memory allocated;
• Loop phase: in the loop phase the following steps are repeated:

– Input step: where the input variables are read;

– Output step: where the outputs variables are updated;
– State step: where the state variables are updated;

• Termination phase: where the memory is released.

Fig. 3. Implementation of a Simulink System

In Simulink systems where there are no causal loops, the order of computation produced in the initialization step
is computed through a linearization of the causality relation between input and output.

The algorithm used by Simulink (Real-Time workshop) for the simulation (implementation) of a system can be
abstracted as follows:

Algorithm RTW System Implement

Inputs: An simulink system as an STS* s=(PI , PO , PS , I0 , ψO , ψS , ≺)
Outputs: An RA r =(L, l0 , V, V0 , PI0 , PO0 T ) that implements the input system
01 L = {l0 }
02 PI0 = {pi |i ∈ PI };
03 PO0 = {pi |i ∈ PO };
04 V = {vi |i ∈ (PI ∪ PO ∪ PS )}
05 i ∈ PS ⇒ V0 (i)I0 (i)
06 lold = l0
07 Let < be a linearization of ≺;
08 for all i ∈ P in an order < do
09 add a new location ls−i in L
10 if i ∈ PI then
 11 add the transition (lold , ls−i , (?pi (vi ), nil)) to T
12 elsif i ∈ PO then
13 add the transition (lold , ls−i , true, (vi = ψoi (V |PIi ∪ PSi ); !pi (vi ))) to T
14 elsif i ∈ PS then
15 add the transition (lold , ls−i , true, (vi := ψsi (V |PIi ∪ PSi ); )) to T
16 fi
17 lold = lpi ;
18 od
19 replace every occurrence of lold with l0

The algorithm is guaranted to terminate for every STS*. All the for loops terminate in finitely many steps because
the set of variables and ports of an STS* is finite.
We now prove some properties of the algorithm RTW System Implement.

Lemma 5.1: For all r in φ[ST S∗] and every run t of r, t visits every location infinitively often and always in
the same order.

Proof: The automaton generated by the algorithm RT W SystemImplement has no branches and consists of a
single loop. Within the main loop (08-18) no loops are created since at every iteration a new location is added and
an arc is added from the old sink to the new location (that becames the new sink). Line (19) creates the first loop
from the sink to the source of the previously acyclic unbranching graph. Since there is no branching every infinite
run of the system will go through every location always in the same order and infinitivelly often.

From lemma 5.1 we see that any run r = < r0 , r1 , r2 , ... > of an RA in φ[ST S∗] has an infinite subsequence
< ri0 , ri1 , ri2 , ... > such that ∀k ∈N rik |location = l0 and ∀k ∈N ri 6= rik ⇒ ri |location 6= l0 . Thus we can write
r equivalently as r = < u0 , u1 , u2 , ... > where u0 =< r0 >, u1 =< r1 , ..., ri1 >, u2 =< ri1 +1 , ..., ri2 > and so on.
We call these ui ’s cycles. We can also define the function cycle(r, n), for a run r and n ∈ N as the valuation of
V at the nth visit to l0 , i.e. cycle(r, n) = rin |V .

Lemma 5.2: In every cycle all the variables of the RA obtained using RT W SystemImplement from the STS*
s are valuated once and only once. Similarly every port pv where v ∈ PO (PI ) is written (read) only once in every
cycle. If v 0 ≺ v then v 0 is valuated before v in every cycle and pv0 is written (read) before pv is.

Proof: Let < be the linearization of ≺ as computed on line (7) by RT W SystemImplement. By hyphotesis <
is a linearization of the I/O port. Hence the main loop (08-18) adds an arc where the variable is written only once
(otherwise the variable would appear twice in the linearization). Hence a new value is given to the variable only
once in every cycle. Since the arcs are added in the order given by < ,if v 0 ≺ v then v 0 is valuated before v in
every cycle. The statement about ports is proved in the same way.

Lemma 5.3: For a given run r of an RA ∈ φ(ST S∗), let t be the associated trace. Then the following holds:
∀i ∈ N ∀v ∈ V . tvi = cycle(r, i)|v

Proof: By lemma 5.2 in every cycle a variable is evaluated once and only once between two successive visits of
l0 . When a run hits the location l0 for the ith time, all the variables have been evaluated exactly i times.

The first theorem stated below asserts algorithm RT W SystemImplement constructs an RA implementing of
an STS* which preserving its semantics in the sense of χ.

Theorem 5.4: φ defined by algorithm RT W SystemImplement satisfies property (1)

Proof: Assume that theorem does not hold. Then the following must hold:

∃s ∈ ST S∗, ∃r = φ(s) ∈ RA, ∃t ∈ Γ . r |= t ∧ ¬s |= χ(t)

where Γ is the set of traces of r. For the previous statement to hold there must be at least one i and a variable v
for which:
v v
χ(t)i |v 6= ψ v (χ(t)i |Piψ ∪ Psψ ) (3)

Select the smallest i for which (3) holds. Amongst the variables at i satisfying (3) pick a minimal one, say v, w.r.t.
<. Hence, by the minimality of v the following must hold:
0 v0 v0 0
∀v 0 ≺ v . χ(t)i |v 0 = ψ v (χ(t)i |Piψ ∪ Psψ ) = tvi . (4)

By lemma 5.3:

0
tvi = cycle(r, i)|v 0 .

So that from (4) it follows that:

∀v 0 ≺ v . χ(t)i |v 0 = cycle(r, i|v 0 ). (5)

By the definition of ≺ given in section II:

v v
∀v 0 ∈ (PIψ ∪ POψ ) . v 0 ≺ v.

So that from (5) we get:

v0 v0 v0 v0
χ(t)i |(Piψ ∪ Psψ ) = cycle(r, i)|(Piψ ∪ Psψ ) (6)
So that:

χ(t)i |v = tvi [by definition of χ]

v0 v0
= ψ v (cycle(r, i)|(Piψ ∪ Psψ ) = [by lemma 5.3]
v0 v0
= ψ v (χ(ti )|Piψ ∪ Psψ ) [by (6)]

But this contradict (3). Hence the theorem 1 holds.

VI. DISTRIBUTION OF SIMULINK SYSTEMS

We have proved in the previous section that there is a map φ between STS* and RA satisfying property (1).
We now prove that the composition operator ×RA as introduced in section III satisfies property (2) in a closed
environment.
Since two different RA may be running on different machines, they do not share the same notion of time. But,
if we are using ×RA , then we can claim the following: if a variable v in one RA is valuated before writing on a
port P and on the other side a variable v 0 is valuated after reading from P then we can be sure that v has been
valuated before v 0 . For the class of reactive automata implementing an STS*, i.e. ψ[ST S∗] this is formalized by
the following lemma:

Lemma 6.1: Consider two compatible RA r1 = φ(s1 ) and r2 = φ(s2 ) with variables v1 , v3 of r1 and r2
respectively and a port p2 written by r1 and read by r2 . If in each cycle of r1 , v1 is valuated before p2 is written
and in each cycle of r2 , p2 is read before v3 is valuated in r2 , then v1 is valuated for the ith time after v3 is
valuated for ith time in r1 ×RA r2 .
Proof: Since the two RA are compatible only one automaton can write on a port, on p2 in particular. This
has to be r1 . Since the environment is closed only r1 write on the queue. Hence for r2 to be evaluating v3 for
the (i)th time it must have read from p2 (i)th times. But since every read operation removes an element from the
queue and since only r1 can write on it, r1 must have done it at least (i)th times. But this is to say that v1 has
been valuated for at least ith times.

A. Correctness proof

We have claimed in section III that ×RA can be implemented across comunicating machines. Hence, we argue
that we can distribute a SIMULINK-like synchronous system across a network by proving the following theorem.

Theorem 6.2: The compostion operator ×RA satisfies property (2), i.e. for any two STS* s1 and s2 and compatible
RA r1 and r2 , the following holds: r1 = φ(s1 ) ∧ r2 = φ(s2 ) ∧ r1 ×RA r2 |=c t ⇒ s1 ×ST S s2 |= χ(t)
Proof: Assume that theorem does not hold. Than the following must hold:

∃s, s0 ∈ ST S∗, ∃r, r0 ∈ RA, ∃t ∈ Γ . r = φ(s) ∧ r0 = φ(s0 )∧

r ×RA r0 |=c t ∧ ¬(s ×ST S ∗ s0 |= χ(t))
where Γ is the set of traces of r ×RA r0 . This is to say that there exists at least one variable v and a natural i such
that:
v v
χ(t)i |v 6= ψ v (χ(ti |PIψ ∪ PSψ )) (7)

Select the smallest i for which (7) holds. Amongst the variables at i satisfying (3) pick a minimal one, say v, w.r.t.
<. Hence, by the minimality of v the following must hold:

0 v0 v0 0
∀v 0 ≺ v . χ(t)i |v 0 = ψ v (χ(t)i |Piψ ∪ Psψ ) = tvi (8)

Now, by definition of asynchronous composition given in section III, the value of χ(t)i is obtained applying ψ v
to variables v 0 such that v 0 ≺ v. Since the two RA are compatible and the environment is closed, an uncorrect
v0 v0
valuation is then possible if and only if one v 0 ∈ Piψ ∪ Psψ has been evaluated more or less than ith time before
v has been evaluated for the ith time. But this contradicts lemma 6.1 or the definition of act given in section III,
hence theorem 2 is proved.

VII. BDSP ARCHITECTURE

In this section we are going to describe our software architecture for the distribution of SIMULINK programs
(see figure 4). We call this architecture Berkeley Distributed Simulink Program (BDSP) library.
An initial version of the BDSP library has been implemented using a simple rendezvous scheme. The first version
was developed as a proof of concept, a second version, utilising bounded queues as described in this section is
currently under development.

Fig. 4. BDSP architecture

Figure 5 shows the distribution of a simple SIMULINK program across a network. Two sinusoidal waves 180
degrees out of phase are produced on two machines connected by a wireless LAN. Some packets are lost but the
output of the composed system conforms with the semantic of SIMULINK.
Fig. 5. BDSP library in action

A. Architecture

First decompose the original SIMULINK system is decomposed into atomic blocks. Then replace all the broken
connections with external − linkboxes (i.e. S-function boxes we provide).
The external-link boxes completely hide the complexity of the distribution to the user. Theexternal-link box is
used to interfaces the SIMULINK program with the queue manager.

B. Input and Output external-link boxes structure

The structure of an Input external-link box and of an Output external-link box are the same but for the ports.
While the input box has a single input and no outputs the output box should have one output and no inputs. The
boxes have three parameters: the IP/port pair for the sender, the IP/port pair for the receiver and a name that is going
to be used to resolve for the first two parameters. Intervally the box uses two UDP sockets to communicate with
the queue manager (UDP is lightweight and since the communication is local there is no need for retransmission).
One socket is used to receive messages from the queue manager and the second is used to send messages to it.

C. Queue Manager structure

The structure of the queue manager is shown in the right side of figure 4. It consists of many queues, one for
every input or output port of the block. It has a couple of UDP sockets to comunicate with the S-function boxes
on the machine and a list of UDP sockets to communicate with the the other queue managers. Every queue is
associated with some flags (the datarequested and queuef ull) and a counter. A reliable transmission protocol is
implemented using a standard retransmission strategy.
D. External-link box to queue manager interface

The life cycle of an external-link box is the same of any SIMULINK box (described in figure 3). In the
initialization phase the box sends a packet to the queue manager to researve a queue and pass the IP/port address
on the other end of the pipe.
If it is an input block it requests its input from the queue manager in the Input Read phase. If the queue is empty
it blocks until something is available. The flag datarequested is switched on if the queue is empty. If it is not
empty the data is removed from the queue and sent to the box.
If it is an output block, in the Ouput Phase the output is sent to the Queue manager and, if the queue is not full
an ack is sent back to the output box. The box is blocked until the ack is received. If the queue is full and the box
is trying to send, the flag F ull is switched on. When the queue is emptied, if the flag F ull is on an ack is sent to
the Output box.

E. Queue manager to queue manager interface

The protocol of communication between queue managers need to be reliable and to preserve message order. A
possible camndidate is TCP, or a UDP with a acknowledgment-timeout protocol implemented on top. When an
output queue is not empty the queue manager will try to send the message as soon as possible. It removes the
message from the queue only when the ack is received. When it receives a message it will put it on the right queue.
If the queue is full it will drop the packet (the message will not be lost, just retransmitted later).

VIII. CONCLUSION

We have addressed the problem of distributing large scale synchronous systems across a network. We defined
a synchronous and asynchronous composition operator. The synchronous composition operator is SIMULINK-
like. The asynchronous composition operator is like Kahn networks. We presented an algorithm to implement a
synchronous program into an asynchronous one and we proved the implementation map preserves the synchronous
semantics in the sense of [14]. The main result was that the implementation is a monomorphism with respect to
the synchronous and asynchronous compositions. The monomorphism is our argument that a local change can be
handled locally and that a subsystem can be re-used in different systems. We have presented a software architecture
consistent with our mathematics and used it to distributed a three block synchronous program.

R EFERENCES

[1] E. Frew, S. Jackson, Z. Kim, T. McGee, M. Morimoto, S. Rathinam, M. Zennaro, R. Sengupta, Vision Based Road-Following Using a
Small Autonomous Aircraft 2004 IEEE Aerospace Conference, Big Sky, Montana, March 2004.
[2] G. Kahn, The Semantics of a Simple Language for Parallel Programming, Proceedings of the IFIP Congress74. North Holland Publishing
Company.
[3] P. Caspi, M. Ponzet, Synchronous Kahn networks ACM. Sigplan Notices (Acm Special Interest Group on Programming Languages), vol.31,
no.6, June 1996, pp.226-38. USA.
[4] G. Berry, A. Benvenieste, The synchronous approach to reactive and real- time systems, Proceedings of the IEEE, 79(9):1270-1282,
September 1991
 [5] C. Andr, F. Boulanger, A. Girault, Software implemenentation of synchronous programs, IEEE International Conference on Application of
concurrency to System Design, June 2001
[6] C. Andr, M.A. Peraldi, Effective implementation of ESTEREL programs, 5th Euromicro workshop on real-time systems, June 1993.
[7] G. Berry, The Foundations of Esterel, Proof, Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling and M.
Tofte, editors, MIT Press, 1998.
[8] G. Berry, The Constructive Semantics of Pure Esterel, July 2, 1999
[9] N. Halbwachs, P. Caspi, P. Raymond and D. Pilaud, The synchronous dataflow programming language Lustre, Proceedings of the IEEE,
vol. 79, nr. 9. September 1991.
[10] B. Houssais The synchronous programming language SIGNAL, a tutorial, IRISA, April 2002
[11] Learning Simulink 5, MathWorks edition, 2002
[12] A. Girault, Automatic distribution of synchronous programs, ERIM News, January 2003
[13] A. Girault, C. Menier, Automatic production of Globally Asynchronous Locally Synchronous Systems, EMSOFT 2002
[14] A. Benvenieste, B. Caillaud, P. Le Guernic, Compositionality in dataflow synchronous languages: specification and distributed code
generation, Information and Computation, vol.163, no.1, 25 Nov. 2000, pp.125-71. Publisher: Academic Press, USA.
[15] N. Lynch, R. Segala, F. W. Vaandrager Hybrid I/O automata, Hybrid System III, LNCS 1066, Springer-Verlag, 1996, p.496-510
[16] C.A.R. Hoare, Communicating sequential processes, Prentice Hall, 2003
[17] J.G.F. Francis, The QR Transformation I, Comput. J., vol. 4, 1961, pp 265-271.
[18] Manna, Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag 1992
[19] S. Edwards, The specification and execution of Heterogeneous Synchronous Reactive Systems, PhD thesis, University of California at
Berkeley, 1997
[20] J. L. Hennessy, D.A. Patterson, D. Goldberg, Computer Architecture: A quantitative approach 3rd edition, Morgan Kaefmann, 2002
[21] A. S. Tanenbaum, M. van Steen, Distributed Systems, Principles and Paradigms, Prentice Hall 2002
[22] A. Garcia, C. Lucena, F. Zambonelli, A. Omicini, J. Castro, Software Engineering for large-scale multi-agent systems: research issues and
practical applications, Sringer Verlag, 2003
[23] Simulink Help Manual: Writing S-functions, MathWorks edition, 2002
[24] Sih GC, Lee EA, A compile-time scheduling heuristic for interconnection-constrained heterogeneous processor architectures,IEEE
Transactions on Parallel and Distributed Systems, vol.4, no.2, Feb. 1993, pp.175-87. USA.