From Synchrony to Asynchrony

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 correct desynchronization, meaning that the original synchronous semantics can be reconstructed from the result of this desynchronization. Theorems are given for both the desynchronization of single synchronous programs, and for networks of synchronous programs to be implemented using asynchronous communication. Assumptions for these theorems correspond to proof obligations that can be checked on the original synchronous designs. If the corresponding conditions are not satisfied, suitable synchronous mini-programs which will ensure correct desynchronization can be composed with the original ones. This can be seen as a systematic way to generate ``correct protocols'' for the asychronous distribution of synchronous designs. The whole approach has been implemented, in the framework of the SACRES project, within the SILDEX tool marketed by TNI, as well as in the SIGNAL compiler