Section: New Results

The Clem Workflow

Participants : Annie Ressouche, Daniel Gaffé.

This research axis concerns the theoretical study of a synchronous language le with modular compilation and the development of a toolkit (see figure 6 ) around the language to design, simulate, verify and generate code for programs. The novelty of the approach is the ability to manage both modularity and causality. Indeed, only few approaches consider a modular compilation because there is a deep incompatibility between causality and modularity. Thus, relying on semantics to compile a language ensures a modular approach but requires to complete the compilation process with a global causality checking. To tackle this problem, we introduced a new way to check causality from already checked sub programs and the modular approach we infer. The equational semantics compute a Boolean equation system and we ensure both modularity and causality in computing all the partial orders valid for a system and we define a way to merge two partial orders. The algorithm which computes partial orders rely on the computation of two dependency graphs: the upstream (downstream) dependency graph computes the dependencies of each variable of the system starting from the input (output) variables. This way of compiling is the corner stone of our approach. We defined three different approaches to compute the partial orders valid for an equation system:

1. apply PERT method : inputs (resp. outputs) have date 0 and recursively increase of dates for each vertice in the upstream (resp downstream) dependencies graph;

2. apply graph theory:

   • compute the adjency matrix $𝒰$ of upstream (resp. downstream) dependencies graph;

   • the length of the maximal path from a variable $v$ to system inputs is characterized by the maximal $k$ such that ${𝒰}^k[v,i]\ne 0$ for all inputs $i$.

3. apply fix point theory: the vector of earliest (resp. lastest) dates can be computed as the least fix point of a monotonic increasing function.

The fix point characterization helps us to prove that the merge algorithm is correct (i.e we get the same partial orders using the merge algorithm on two previously sorted equation systems or when sorting the union of the two equation systems considered).

To be modular, we defined a technique to compose two already sorted equation systems : first, we memorize the two dependency graphs of equation systems. Second, we define two merge algorithms relying on two different techniques:

1. propagation of common variables dates adjustment;

2. fix point characterization starting with the vectors of already computed dates and considering only the variables in the dependencies (upstream and downstream) of common variables

This year we began the implementation of a separated compilation of le programs, according to these theoretical results. We define a new intermediate format (lea) to record partially compiled module, i.e module whose Boolean equation systems may be composed of non defined variables (we called them abstract). Then we are implementing a refinement operation which replaces these abstract variables by their definition and performs adjustment of the dates. According to our theoretical results, we know that the resulting sorting is the same as with a global approach. After the termination of this separated compilation of le programs, the challenge will be to use Clem to design a large application in the domain of smart cards. The application needs more than forty le automata in parallel and the compiled code will have more than 500 registers and thousands variables. Only a separated compilation will work.

The Clem toolkit is completely described in [28]