Guernic. Compositionality in dataflow synchronous languages: specification and distributed code generation

In [2], some new concepts were introduced for the first time to study the preservation of semantics when deploying synchronous specifications over asynchronous architectures, namely: endochrony and isochrony. Here we informally recall some background: Synchronous transition systems (STS) behave as a succession of reactions, in which some variables are absent and others are present and carry a value. Parallel composition is by instantaneous broadcast, in which components must agree on the presence/absence of their shared variables, and on the values carried by the variables present in all components. A synchronous transition system is endochronous if successive reactions can be uniquely reconstructed without the need to test for absence. A pair of transition systems is isochronous if implementing the synchronous broadcast communication protocol for this pair does not require to test for absence. In [2], two fundamental theorems were stated. The first theorem says that the semantics of an endochronous system is robust when fed by an asynchronous environment. The second theorem says that an isochronous pair of transition systems possesses identical sets of histories, whether they com-municate over a synchronous or an asynchronous medium. These results were recently complemented in [3], which states that the above two robustness properties are the key to semantics preserving for the deployment of synchronous designs over asynchronous architectures, in some particular way. The results of [2] are included in [1]–Section 4 as theorems 1 and 2, with detailed proofs. This correctly addresses distributed architectures made of two components, or more generally tree-shaped distributed architectures (as stated by Corollary 2)