Foreword

The approach developed at Inria in the framework of SYRF mainly had distributed software architectures in its target. In contrast, the approach by Berry & Sentovich has been motivated by studies in synchronous/asynchronous hardware circuits.

1. The SYRF approach

Problem setting

1. How to distribute correctly a synchronous program on a given, possibly asynchronous, architecture? What are the available theoretical results? What are the assumptions required, for the supporting execution architecture?
2. In what extend a property proved for the original synchronous program is still valid for the same one, running on a distributed, possibly asynchronous, architecture?
3. What support can be provided (with theoretical justifications) for the reuse of pre-existing components? How can encapsulation be guaranteed correct?

• In synchronous programming paradigm, there are, as byproducts of the notion of a reaction,
1. a global notion of linear time, and
2. a global notion of state
are available. Unfortunately, none of them is generally available in distributed asynchronous architectures, unless specific protocols are implemented for them to be guaranteed. Except for ``synchronous'' architectures for which these are reasonable requirements (e.g., hardware), it may be costly to guarantee requirements 1 and 2 above.
• Storing components as compiled object code hides the scheduling of internal actions, and thus can result into possible deadlocks at reuse, unless drastic programming discipline is enforced.

Achieved Results

• In a synchronous program, a run is a sequence of tuples of values (including the status ``absent''), one tuple component per each flow. Desynchronising a run amounts to (a) mapping this sequence of t-uples into a tuple of sequences, one sequence per each flow, and then (b), in each sequence erasing the ``absence'' information. Thus desynchronized runs are asynchronous tuple of sequences, a program is thus a set of such tuples, and program composition is just again intersection. This model complies with the constraint that requirements 1 and 2, of global time and state, may not be provided by an asynchronous distributed supporting architecture. It however requires that the communication layer shall not loose messages, and shall preserve message ordering for each flow, separately.

• Endochrony has been introduced as a new notion for synchronous programs. Endochrony means that the program is able to reconstruct its timing from its ``interior'', and is not subject to using the environment as an oracle for it. An endochronous program is robust to desynchronisation, in the sense that each synchronous run of the original program can be uniquely reconstructed from its desynchronised version. Endochrony is checkable on synchronous programs; of course, it is not decidable in general as the corresponding proof obligation involves arbitrary data types, but approximation of it are model checkable or even easily guaranteed by certain property of the clock structure of the synchronous program. See  [BCLg99b]  [BCLg99a] .

• Isochrony has been introduced as a new notion for pairs of synchronous programs. Roughly speaking, a pair of programs is isochronous if it only needs to monitor present messages in order to reconstruct the whole sequence of successive communication reactions. The key result is that an isochronous pair of programs is robust to the desynchronisation of its communication reactions. In practice, tightly synchronised programs form an isochronous pair; but, on the other hand, a pair of non interacting programs running asynchronously in parallel also forms an isochronous pair; and appropriate mixtures of these two situations also are. An interesting property is that Isochrony is compositional in the following sense: if we wish to check isochrony of two networks of components, it is enough to check pairwise isochrony of local components (we do not need to check isochrony of the two networks, globally). See  [BCLg99b] [BCLg99a] .

• Endochrony and Isochrony together form the theoretical basis for (a) program desynchronisation, and (b) property preserving while desynchronisation is performed. Also, we have illustrated our approach on a simple Statecharts example [Btransp99]  .

• Hierarchic Normal Forms (HNF) have been proposed as a canonical form for transition relations to handle endo/isochrony efficiently. HNF are decision diagrams different from BDDs, in which variable ordering is part of the canonical form and cannot be freely choosed. HNF capture the nested structure of presence/absence for the different signals and events. We have developed a thorough theory and set of algorithms to compute HNFs compositionally. This set of results serves as a theoretical support of the algorithms already implemented in the SIGNAL compiler, our theory goes in fact beyond what is implemented today in the compiler. See [TBCLg99] .

• Our technique for desynchronisation requires assumptions on the communication layer which may not be always valid in practice. Also, resulting protocols require blocking, something not always acceptable in embedded control systems. We have performed a small study to show how our approach can be used on top of a TTP-like communication layer and associated protocols (TTP: Time-Triggered Protocol, an idea of Kopetz). The idea is that oversampling and event/state conversion allows to emulate our approach by resourcing to unreliable, time-triggered, communications, see  [BC99]  .

• A particular form of ``partial compilation'' has been provided, in which the object code has the following form, suitable to subsequent reuse:
• the code is structured into tasks; tasks are compiled into sequential code and are executed in a read_inputs/compute/emit_outputs mode; tasks can be freely suspended and resumed by the supporting real-time kernel.
• tasks are scheduled, and the scheduler is kept as source synchronous code.
• the structuring into tasks is performed so as to allow maximal compilation while avoiding the risk of subsequent deadlock at reuse, due to the unknown future environment.
This architecture serves as a guideline for the practical design of libraries of synchronous components. See [BCLg99a][Sacres98].

Perspectives

Documents

Publications

1. [BCLg99a]A. Benveniste, B. Caillaud and P. Le Guernic. ``Compositionality in dataflow synchronous languages: specification & distributed code generation.'' Information and Computation, to appear.(new)
2. [BCLg99b]A. Benveniste, B. Caillaud and P. Le Guernic. ``From synchrony to asynchrony.'' In J.C.M. Baeten and S. Mauw, editors, CONCUR'99, Concurrency Theory, 10th International Conference, vol. 1664 of Lecture Notes in Computer Science,  162-177. Springer V.,  1999.
3. [Sacres98]A. Benveniste. ``Safety critical embedded systems: the SACRES approach.'' In Formal techniques in Real-Time and Fault Tolerant Systems, FTRTFT'98 school, Lyngby, Denmark, Sept 1998.
4.  [BC99]  A. Benveniste, P. Caspi. ``Distributing synchronous programs on communication media of time triggered type.'' Draft note, 1999.
5. [TBCLg99]  J-P. Talpin, A. Benveniste, B. Caillaud, P. Le Guernic. ``HIerarchic normal forms for desynchronization.'' Draft paper, 1999.
6. [Btransp99]  A. Benveniste. `Distributing synchronous programs.'' Slides, FM'99, Toulouse.

2. The Berry & Sentovich approach (a sketch of...)

• the are 1-output to *-inputs channels;
• the information transmitted composes of a pair {status,value} stored in 1-place communication buffers;
• the status buffer stores a 1 or a 0, indicating the status valid/invalid of the value stored in the value buffer.

As the write/read operations in the communication channels are asynchronous, this calls for a confluent technique for performing assignments, in which, for a total assignment (all status buffers sre set to 1), the values stored in the input value buffers are identical irrespective of the particular ordering of the writings in the {status,value}-buffers.

A previous result from Berry on the constructive semantics of Esterel had established the equivalence of the following two properties for (possibly cyclic) digital circuits:

1. For any given latch- and input-pattern, the circuit stabilizes to the same set of values for the variables and registers, irrespective of the needed delay for each gate of wire to stabilize.
2. The corresponding netlist of boolean equations has a well-defined and unique solution according to the so-called constructive logic. According to this logic, netlists of boolean equations are solved by iteratively  propagating facts, i.e., properties in the three-valued logic {?,0,1} where ? denotes the undefined status. The solution is well-defined when this iteration has a unique fixpoint, in which all variables are set to either 0 or 1 (but not ?).

Publications

1. [BS99] G. Berry and E. Sentovich. ``An implementation of constructive synchronous programs in POLIS''. To appear in "Design Automation for Embedded Systems"

3. Discussion and comparison

Similarities

• If we filter the history of each CFSM channel by keeping only the successive pairs {status=1,valid_value}, we obtain a model of communication medium which exactly satisfies the requirements for the ``SYRF approach'' to desynchronisation to apply. In this respect, one could view the fact propagation in CSFM as a ``micro-step'' execution scheme.
• This addition ``status'' buffer very much resembles the need to materialize the absence/presence status of a signal by using additional ``clock-signals'', in order to make a communication isochronous.

Differences

• The work of Berry & Sentovich applies to circuits having a valid constructive semantics, whereas the SYRF approach applies to partial, nondeterministic, designs as well and is independent from executability.
• The constructive semantics is more powerful at handling boolean circuits. Basically, this approach can run the largest possible number of designs. The SYRF approach, being targeted to software, has a more general scope but is less powerful at handling boolean circuits.
• As it is presented in [BS99], the Berry & Sentovich approach does not allow for a pipelined execution of the successive reactions, while this is allowed for the execution schemes proposed in the SYRF approach. On the other hand, the need for pipelining has been recognized by Berry & Sentovich, and they currently work at solving this issue.

Complementary?