Correct-by-Construction Asynchronous Implementation of Modular Synchronous Specifications

• Autorzy: Potop-Butucaru D. , Caillaud B.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

synchronous systems; asynchronous systems; globally asynchronous; locally synchronous (GALS) architectures; kahn processes; endochronous systems; semantics preservation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 78, nr 1
• Strony: 131--159
• Opis fizyczny: bibliogr. 27 poz.

Twórcy

autor

Potop-Butucaru D.

autor

Caillaud B.

• IRISA/INRIA Rennes, Campus universitaire de Beaulieu, 35042 Rennes cedex, France,

Bibliografia

• [1] N. Halbwachs, Synchronous programming of reactive systems. Kluwer Academic Publishers, 1993.
• [2] A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. L. Guernic, and R. de Simone, "The Synchronous Languages Twelve Years Later", Proceedings of the IEEE, vol. 91, no. 1, pp. 64-83, 2003.
• [3] D. Potop-Butucaru, R. de Simone, and J.-P. Talpin, "The synchronous hypothesis and synchronous languages", in The Embedded Systems Handbook, R. Zurawski, Ed., 2005, CRC Press.
• [4] H. Kopetz, Real-Time Systems, Design Principles for Distributed Embedded Applications. Kluwer Academic Publishers, 1997.
• [5] L. Carloni, K. McMillan, and A. Sangiovanni-Vincentelli, "The theory of latency-insensitive design," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 20, no. 9, pp. 1059-1076, 2001.
• [6] N. Lynch and E. Stark, "A proof of the Kahn principle for input/output automata," Information and Computation, vol. 82, no. 1, pp. 81-92, 7 1989.
• [7] P. Caspi, A. Girault, and D. Pilaud, "Automatic distribution of reactive systems for asynchronous networks of processors," IEEE Trans. on Software Engineering, vol. 25, no. 3, pp. 416-427, 1999.
• [8] J.-P. Talpin, P. L. Guernic, S. K. Shukla, R. Gupta, and F. Doucet, "Formal refinement checking in a systemlevel design methodology," Fundamenta Informaticae, vol. 62, no. 2, pp. 243-273, 2004.
• [9] A. Benveniste, B. Caillaud, and P. L. Guernic, "Compositionality in dataflow synchronous languages: Specification and distributed code generation," Information and Computation, vol. 163, no. 1, pp. 125-171, 2000.
• [10] M. Singh and M. Theobald, "Generalized latency insensitive systems for gals architectures," in Proceedings FMGALS2003, Pisa, Italy, 2003.
• [11] D. Potop-Butucaru, B. Caillaud, and A. Benveniste, "Concurrency in synchronous systems," FormalMethods in System Design, vol. 28, no. 2, pp. 111-130, 2006.
• [12] P. Caspi, A. Girault, and D. Pilaud, "Automatic distribution of reactive systems for asynchronous networks of processors," IEEE Transactions on Software Engineering, vol. 25, no. 3, pp. 416-427, 1999.
• [13] T. Grandpierre and Y. Sorel, "From algorithm and architecture specifications to automatic generation of distributed real-time executives: a seamless flow of graphs transformations," in Proceedings MEMOCODE'03, Mont Saint-Michel, France, 2003.
• [14] I. Blunno, J. Cortadella, A. Kondratyev, L. Lavagno, K. Lwin, and C. Sotiriou, "Handshake protocols for de-synchronization," in Proceedings Async04, Crete, Greece, 2004, pp. 149-158.
• [15] R. Keller, "A fundamental theorem of asynchronous parallel computation," Lecture Notes in Computer Science, vol. 24, pp. 103-112, 1975.
• [16] J. T. Udding, "A formalmodel for defining and classifying delay-insensitive circuits and systems," Distributed Computing, vol. 1, no. 4, pp. 197-204, 1986.
• [17] A.Martin, "The limitations of delay-insensitivity in asynchronous circuits," Caltech, technical report CS-TR-90-02, 1990.
• [18] J. Cortadella,M. Kishinevsky,A. Kondratyev, L. Lavagno, and A. Yakovlev, Logic Synthesis of Asynchronous Controllers and Interfaces. Springer, 2002.
• [19] R. Keller, "Towards a theory of speed-independent modules," IEEE Transactions on Computers, vol. C-23, no. 1, pp. 21-33, January 1974.
• [20] K. Yun and D. Dill, "Automatic synthesis of extended burst-mode circuits," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 18, no. 2, pp. 101-132, feb. 1999.
• [21] E. Stark, "Concurrent transition systems," Theoretical Computer Science, vol. 64, no. 3, pp. 221-269, 1989.
• [22] M. Mukund, "Petri nets and step transition systems," International Journal of Foundations of Computer Science, vol. 3, no. 4, pp. 443-478, 1992.
• [23] D. E. Muller and W. S. Bartky, "A theory of asynchronous circuits," in Proceedings of an International Symposium on the Theory of Switching. Harvard University Press, 1959, pp. 204-243.
• [24] S. Dasgupta, D. Potop-Butucaru, B. Caillaud, and A. Yakovlev, "From weakly endochronous systems to delay-insensitive circuits," in Proceedings FMGALS'05, Verona, Italy, 2005.
• [25] J.-P. Talpin, D. Potop-Butucaru, J. Ouy, and B. Caillaud, "Compositional synthesis of latency-insensitive systems from multi-clocked synchronous specifications," in Proceedings EMSOFT'05, Jersey City, NJ, USA, 2005.
• [26] G. Berry, "The constructive semantics of pure Esterel," July 1999, draft book available at http://www.estereltechnologies.com/.
• [27] G. Kahn and G. Plotkin, "Concrete domains," Theoretical Computer Science, vol. 121, no. 1&2, pp. 187-277, 1993.