Jean-Pierre Talpin, Albert Benveniste, Benoît Caillaud and
Paul Le Guernic
We present an in-depth discussion
of the relationships between synchrony and asynchrony. Simple models of
both paradigms are presented, and we state theorems which guarantee correctdesynchronization,
meaning that the original synchronous semantics can be reconstructed from
the result of this desynchronization. This theory can be used as a basis
for correct distributed code generation. The present paper presents a new
data structure, the hierarchic normal form (HNF)
for
a transition relation, which is instrumental in implementing this theory.
HNFdiffer
from Bdd's. They are canonical and do not need prior ordering of
the variables for this. They reveal clock hierarchies as well as nested
states such as exhibited in Statecharts. They are the adequate data structures
to implement correct desynchronization. They can be seen as a systematic
calculus of don't care in hardware design, and play a central role in optimizations
for code generation. We provide compositional algorithms for computing
HNF.
We
illustrate this on a Statecharts example. The whole approach is implemented
in the Signal
compiler.
Keywords : synchronous languages,
desynchronization, distribution.