N-synchronous Kahn networks: a relaxed model of synchrony for real-time systems

ABSTRACT

The design of high-performance stream-processing systems is a fast growing domain, driven by markets such like high-end TV, gaming, 3D animation and medical imaging. It is also a surprisingly demanding task, with respect to the algorithmic and conceptual simplicity of streaming applications. It needs the close cooperation between numerical analysts, parallel programming experts, real-time control experts and computer architects, and incurs a very high level of quality insurance and optimization.In search for improved productivity, we propose a programming model and language dedicated to high-performance stream processing. This language builds on the synchronous programming model and on domain knowledge -- the periodic evolution of streams -- to allow correct-by-construction properties to be proven by the compiler. These properties include resource requirements and delays between input and output streams. Automating this task avoids tedious and error-prone engineering, due to the combinatorics of the composition of filters with multiple data rates and formats. Correctness of the implementation is also difficult to assess with traditional (asynchronous, simulation-based) approaches. This language is thus provided with a relaxed notion of synchronous composition, called n-synchrony: two processes are n-synchronous if they can communicate in the ordinary (0-)synchronous model with a FIFO buffer of size n.Technically, we extend a core synchronous data-flow language with a notion of periodic clocks, and design a relaxed clock calculus (a type system for clocks) to allow non strictly synchronous processes to be composed or correlated. This relaxation is associated with two sub-typing rules in the clock calculus. Delay, buffer insertion and control code for these buffers are automatically inferred from the clock types through a systematic transformation into a standard synchronous program. We formally define the semantics of the language and prove the soundness and completeness of its clock calculus and synchronization transformation. Finally, the language is compared with existing formalisms.

REFERENCES

• 1: Alexander Aiken , Edward L. Wimmers, Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture, p.31-41, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165188]
• 2: A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone. The Synchronous Languages Twelve Years Later. Proceedings of the IEEE, 91(1):64--83, 2003.
• 3: Albert Benveniste , Paul Le Guernic , Christian Jacquemot, Synchronous programming with events and relations: the SIGNAL language and its semantics, Science of Computer Programming, v.16 n.2, p.103-149, Sept. 1991 [doi>10.1016/0167-6423(91)90001-E]
• 4: G. Berry. The Foundations of Esterel. MIT Press, 2000.
• 5: J.-Y. Brunel , W. M. Kruijtzer , H. J. H. N. Kenter , F. Pétrot , L. Pasquier , E. A. de Kock , W. J. M. Smits, COSY communication IP's, Proceedings of the 37th conference on Design automation, p.406-409, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337515]
• 6: J. Buck, S. Ha, E. A. Lee, and D. G. Messerschmitt. Ptolemy: A framework for simulating and prototyping heterogenous systems. Int. Journal in Computer Simulation, 4(2):155--182, 1994.
• 7: Paul Caspi, Embedded Control: From Asynchrony to Synchrony and Back, Proceedings of the First International Workshop on Embedded Software, p.80-96, October 08-10, 2001
• 8: Paul Caspi , Marc Pouzet, Synchronous Kahn networks, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.226-238, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 9: Zbigniew Chamski , Marc Duranton , Albert Cohen , Christine Eisenbeis , Paul Feautrier , Daniela Genius, Application-domain-driven system design for pervasive video processing, Ambient intelligence: impact on embedded system design, Kluwer Academic Publishers, Norwell, MA, 2003
• 10: Daniel Marcos Chapiro, Globally-asynchronous locally-synchronous systems (performance, reliability, digital), 1985
• 11: Albert Cohen , Marc Duranton , Christine Eisenbeis , Claire Pagetti , Florence Plateau , Marc Pouzet, Synchronization of periodic clocks, Proceedings of the 5th ACM international conference on Embedded software, September 18-22, 2005, Jersey City, NJ, USA [doi>10.1145/1086228.1086289]
• 12: Jean-Louis Colaço , Alain Girault , Grégoire Hamon , Marc Pouzet, Towards a higher-order synchronous data-flow language, Proceedings of the 4th ACM international conference on Embedded software, September 27-29, 2004, Pisa, Italy [doi>10.1145/1017753.1017792]
• 13: J.-L. Colaço and M. Pouzet. Clocks as first class abstract types. In Rajeev Alur and Insup Lee, editors, EMSOFT'03, volume 2855 of Lecture Notes in Computer Science, pages 134--155. Springer, 2003.
• 14: E. A. de Kock , W. J. M. Smits , P. van der Wolf , J.-Y. Brunel , W. M. Kruijtzer , P. Lieverse , K. A. Vissers , G. Essink, YAPI: application modeling for signal processing systems, Proceedings of the 37th conference on Design automation, p.402-405, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337511]
• 15: Edward Ashford Lee , David G. Messerschmitt, Static scheduling of synchronous data flow programs for digital signal processing, IEEE Transactions on Computers, v.36 n.1, p.24-35, Jan. 1987 [doi>10.1109/TC.1987.5009446]
• 16: K. Goossens, G. Prakash, J. Röver, and A. P. Niranjan. Interconnect and memory organization in SOCs for advanced set-top boxes and TV -- evolution, analysis, and trends. In Jari Nurmi, Hannu Tenhunen, Jouni Isoaho, and Axel Jantsch, editors, Interconnect-Centric Design for Advanced SoC and NoC, chapter 15, pages 399--423. Kluwer, April 2004.
• 17: N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language lustre. Proceedings of the IEEE, 79(9):1305--1320, September 1991.
• 18: G. Kahn. The semantics of a simple language for parallel programming. In J. L. Rosenfeld, editor, Information processing, pages 471--475, Stockholm, Sweden, Aug 1974. North Holland, Amsterdam.
• 19: P. Le Guernic, J.-P. Talpin, and J.-C. Le Lann. Polychrony for system design. Journal for Circuits, Systems and Computers, Special Issue on Application Specific Hardware Design, April 2003.
• 20: C. E. Leiserson and J. B. Saxe. Retiming synchronous circuitry. Algorithmica, 6(1), 1991.
• 21: A.J.M. Moonen, M. Bekooij, and J. van Meerbergen. Timing analysis model for network based multiprocessor systems. In proceedings of ProRISC, 15th annual Workshop of Circuits, System and Signal Processing, pages pages 91--99, Veldhoven, The Netherlands, November 2004. ISBN: 90-73461-43-X.
• 22: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 23: François Pottier, Simplifying subtyping constraints, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.122-133, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 24: William Thies , Michal Karczmarek , Saman P. Amarasinghe, StreamIt: A Language for Streaming Applications, Proceedings of the 11th International Conference on Compiler Construction, p.179-196, April 08-12, 2002
• 25: J. E. Vuillemin, On Circuits and Numbers, IEEE Transactions on Computers, v.43 n.8, p.868-879, August 1994 [doi>10.1109/12.295849]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

General Terms:
Algorithms, Languages, Security, Theory

Keywords:
correctness by construction, resource constraints, streaming applications, subtyping, synchronous languages