Affiliations: INRIA Rocquencourt, Domaine de Voluceau,
Rocquencourt – B.P. 105, 78153 Le Chesnay Cedex, France. E-mail: Dumitru.Potop_Butucaru@inria.fr | IRISA/INRIA Rennes, Campus universitaire de Beaulieu,
35042 Rennes Cedex, France. E-mail: Benoit.Caillaud@irisa.fr
Abstract: In this paper, we introduce a new model for the representation of
distributed asynchronous implementations of synchronous specifications. The
model covers classical implementations, where a notion of global
synchronization is preserved by means of signaling, and globally asynchronous,
locally synchronous (GALS) implementations where the global clock is removed. The new model offers a unified framework for reasoning about two essential
correctness properties of an implementation: the preservation of semantics and
the absence of deadlocks. We use it to derive criteria ensuring the correct
deployment of synchronous specifications over GALS architectures. As the model
captures the internal concurrency of the synchronous specification, our
criteria support implementations that are less constrained and more efficient
than existing ones. Our work also reveals strong ties between abstract
semantics-preservation properties and more operational ones like the absence of
deadlocks.
