| Researchers: | Alain Girault---Research fellow, INRIA, France |
|---|---|
| Advisor: | Edward A. Lee |
| Sponsor: |
Many reactive systems have to be distributed on several computing locations, for various reasons: performance increase, location of sensors and actuators, fault tolerance. The ocrep tool parallelizes synchronous programs, according to distribution specifications given by the user. It takes as input an oc file, for instance produced by the Esterel, Lustre or Argos compiler. An oc program is a finite state automaton with a directed acyclic graph of actions in each state.
The ocrep tool replicates the control structure of the initial centralized program, and on each computing location, removes the irrelevant actions. Then communication actions are added to permit references to non local variables. Two communications actions are used: a put sends a value to a FIFO queue (non blocking) and a get extracts the head value from a FIFO queue (blocking when the queue is empty).
The fact that the control structure is replicated on each computing location has allowed the formal proving of the parallelization's correctness. The aim was to show that the set of admissible behaviors of the initial centralized program was equivalent to the set of behaviors of the final parallel program.
Another consequence of the replication of the control structure is the loss of the clocks from the initial source program. Clocks allow the mixing of parts of the program having different dynamics. But they are hidden in the oc automaton. After distributing the oc program, it is possible to retrieve the clocks and implement each part of the final parallel program with its own dynamics. This involves a bisimulation algorithm for detecting that two branches of a binary test have the same behavior, and thus removing such tests.