Abstract
A main goal of compilation is to efficiently map application programs onto execution platforms, while hiding the details of the latter to the programmer through high-level programming languages. Of course this is only feasible inside a certain range of constructs, and the judicious design of sequential programming languages and computer architectures that match one another has been a decades-long process. Now the advent of multicore processors brings radical changes to this topic, bringing forth concurrency as a key element in efficiency, both for application design and architecture computing power. The shift is mostly prompted by technological factors, namely the ability to cram several processors on a single chip, and the diminishing gains of Instruction Level Parallelism techniques used in former architectures. Still, the definition of high-level programming (and more generally, application design) formalisms matching the new era is a largely unsolved issue.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
We recall that \(\mathbb{N} = \left \{0, 1, 2,\ldots \,\right \}\) and \({\mathbb{N}}^{{_\ast}} = \mathbb{N}\setminus \left \{0\right \}\).
References
S. Amarasinghe. A stream compiler for communication-exposed architectures. In Proceedings of ASPLOS, 2002.
F. Anceau. A synchronous approach for clocking VLSI systems. IEEE Journal of Solid-State Circuits, 17:51–56, 1982.
C. André. Representation and analysis of reactive behaviors: A synchronous approach. In CESA, 1996.
F. Baccelli, G. Cohen, G. J. Olsder, and J.-P. Quadrat. Synchronization and Linearity. Wiley, Chichester, West Sussex, UK, 1992.
D. Baneres, J. Cortadella, and M. Kishinevsky. Variable-latency design using function speculation. In Proc. Design, Automation and Test in Europe, April 2009.
L. Benini, E. Macii, and M. Poncino. Telescopic units: Increasing the average throughput of pipelined designs by adaptive latency control. In DAC, pages 22–27, 1997.
A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone. The synchronous languages 12 years later. Proceedings of the IEEE, 91(1):64–83, 2003.
S. S. Bhattacharyya, P. K. Murthy, and E. A. Lee. Software Synthesis from Dataflow Graphs. Kluwer, Dordrecht, 1996.
G. Bilsen, M. Engels, R. Lauwereins, and J. Peperstraete. Cyclo-static dataflow. IEEE Transactions on Signal Processing, 44:397–408, February 1996.
A. Bouali. XEVE, an esterel verification environment. In CAV ’98: Proceedings of the 10th International Conference on Computer Aided Verification, pages 500–504, London, UK, 1998. Springer.
J. Boucaron, A. Coadou, and R. de Simone. Latency-insensitive design: retry relay-station and fusion shell. In Formal Methods for Globally Asynchronous Locally Synchronous Design 2009 Proceedings, 2009.
J. Boucaron, A. Coadou, B. Ferrero, J.-V. Millo, and R. de Simone. Kahn-extended event graphs. Research Report RR-6541, INRIA, 2008.
J. Boucaron, J.-V. Millo, and R. de Simone. Another glance at relay-stations in latency-insensitive design. In Formal Methods for Globally Asynchronous Locally Synchronous Design 2005 Proceedings, 2005.
J. Boucaron, J.-V. Millo, and R. de Simone. Latency-insensitive design and central repetitive scheduling. In Proceedings of the 4th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE’06), pages 175–183, Napa Valley, CA, USA, July 2006. IEEE Press.
J. Boucaron, J.-V. Millo, and R. de Simone. Formal methods for scheduling of latency-insensitive designs. EURASIP Journal on Embedded Systems, 2007(1), 8–8, 2007.
R. G. Brown and P. Y. C. Hwang. Introduction to Random Signals and Applied Kalman Filtering, 3rd edition. Wiley, New York, 1996.
R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986.
J. T. Buck. Scheduling Dynamic Dataflow Graphs with Bounded Memory Using the Token Flow Model. PhD thesis, University of California, Berkeley, CA, USA, 1993.
D. Bufistov, J. Júlvez, and J. Cortadella. Performance optimization of elastic systems using buffer resizing and buffer insertion. In ICCAD ’08: Proceedings of the 2008 IEEE/ACM International Conference on Computer-Aided Design, pages 442–448, Piscataway, NJ, USA, 2008. IEEE Press.
J. L. Campbell. Application of Airborne Laser Scanner – Aerial Navigation. PhD thesis, Russ College of Engineering and Technology, Athens, OH, USA, February 2006.
L. P. Carloni, K. L. McMillan, A. Saldanha, and A. L. Sangiovanni-Vincentelli. A methodology for correct-by-construction latency-insensitive design. In Proceedings of the International Conference on Computer-Aided Design (ICCAD’99), pages 309–315, Piscataway, NJ, USA, November 1999. IEEE.
L. P. Carloni, K. L. McMillan, and A. L. Sangiovanni-Vincentelli. Theory of latency-insensitive design. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 20(9):1059–1076, 2001.
L. P. Carloni and A. L. Sangiovanni-Vincentelli. Performance analysis and optimization of latency insensitive systems. In DAC ’00: Proceedings of the 37th Annual Design Automation Conference, pages 361–367, New York, NY, USA, 2000. ACM.
L. P. Carloni and A. L. Sangiovanni-Vincentelli. Combining retiming and recycling to optimize the performance of synchronous circuits. In SBCCI ’03: Proceedings of the 16th symposium on Integrated circuits and systems design, page 47, Washington, DC, USA, 2003. IEEE Computer Society.
P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice. Lustre: a declarative language for programming synchronous systems. In POPL, pages 178–188, 1987.
P. Caspi and M. Pouzet. A functional extension to Lustre. In M. A. Orgun and E. A. Ashcroft, editors, International Symposium on Languages for Intentional Programming, Sydney, Australia, May 1995. World Scientific.
P. Caspi and M. Pouzet. Lucid Synchrone, version 1.01. Tutorial and reference manual. Laboratoire d’Informatique de Paris 6, January 1999.
M. R. Casu and L. Macchiarulo. A detailed implementation of latency insensitive protocols. In Proceedings of the 1st Workshop on Globally Asynchronous, Locally Synchronous Design (FMGALS’03), pages 94–103, September 2003.
M. R. Casu and L. Macchiarulo. A new approach to latency insensitive design. In Proceedings of the 41st Annual Conference on Design Automation (DAC’04), pages 576–581, 2004.
M. R. Casu and L. Macchiarulo. Adaptive latency-insensitive protocols. IEEE Design and Test of Computers, 24(5):442–452, 2007.
A. Cohen, M. Duranton, C. Eisenbeis, C. Pagetti, F. Plateau, and M. Pouzet. N-synchronous kahn networks: a relaxed model of synchrony for real-time systems. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’06), pages 180–193, New York, NY, USA, January 2006. ACM.
F. Commoner, A. W. Holt, S. Even, and A. Pnueli. Marked directed graph. Journal of Computer and System Sciences, 5:511–523, October 1971.
J. Cortadella, M. Kishinevsky, and B. Grundmann. Synthesis of synchronous elastic architectures. In Proceedings of the 43rd Annual Conference on Design Automation (DAC’06), pages 657–662, New York, NY, USA, 2006. ACM.
M. Dall’Osso, G. Biccari, L. Giovannini, D. Bertozzi, and L. Benini. Xpipes: a latency insensitive parameterized network-on-chip architecture for multi-processor SOCS. In ICCD, pages 536–, 2003.
A. Darte, Y. Robert, and F. Vivien. Scheduling and Automatic Parallelization. Birkhaüser, Boston, 2000.
A. Dasdan and R. Gupta. Faster maximum and minimum mean cycle algorithms for system-performance analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 17(10):889–899, 1998.
G. de Micheli. Synthesis and Optimization of Digital Circuits. McGraw-Hill, New York, 1994.
N. Eén and N. Sörensson. An extensible SAT solver. In SAT Proceedings, volume 2919 of Lecture Notes in Computer Science, pages 502–518. Springer, Berlin, 2003.
J. Eker, J. Janneck, E. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer, S. Sachs, and Y. Xiong. Taming heterogeneity – the Ptolemy approach. Proceedings of the IEEE, 91(1):127–144, 2003.
M. Engels, G. Bilsen, R. Lauwereins, and J. A. Peperstraete. Cyclo-static dataflow: model and implementation. In Conference Record of the Twenty-Eighth Asilomar Conference on Signals, Systems and Computers, volume 1, pages 503–507, Pacific Grove, CA, USA, 1994.
D. Gebhardt and K. Stevens. Elastic flow in an application specific network-on-chip. In Formal Methods for Globally Asynchronous Locally Synchronous Design Proceedings, 2007.
R. Govindarajan and G. R. Gao. Rate-optimal schedule for multi-rate DSP computations. Journal of VLSI Signal Processing, 9(3):211–232, 1995.
T. Grandpierre and Y. Sorel. From algorithm and architecture specification to automatic generation of distributed real-time executives: a seamless flow of graphs transformations. In Proceedings of First ACM and IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE’03, Mont Saint-Michel, France, June 2003.
C. A. R. Hoare. Communicating sequential processes. Commun. ACM, 21(8):666–677, 1978.
G. Hoover and F. Brewer. Synthesizing synchronous elastic flow networks. In DATE, pages 306–311, 2008.
D. B. Johnson. Finding all the elementary circuits of a directed graph. SIAM Journal on Computing, 4(1):77–84, 1975.
G. Kahn. The semantics of a simple language for parallel programming. In J. L. Rosenfeld, editor, Information Processing ’74: Proceedings of the IFIP Congress, pages 471–475, New York, NY, USA, 1974. North-Holland.
M. Karczmarek. Phased scheduling of stream programs. In Proceedings of LCTES, 2003.
R. Karp. A characterization of the minimum cycle mean in a digraph. Discrete Mathematics, 23(3):309–311, 1978.
R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147–195, May, 1969.
K. Kennedy and J. R. Allen. Optimizing compilers for modern architectures: a dependence-based approach. Morgan Kaufmann, San Francisco, CA, USA, 2002.
M. Kudlur and S. A. Mahlke. Orchestrating the execution of stream programs on multicore platforms. In PLDI, pages 114–124, 2008.
P. Le Guernic, J.-P. Talpin, and J.-C. Le Lann. Polychrony for system design. Journal for Circuits, Systems and Computers, 12:261–304, 2002.
C. Y. Lee. Representation of switching circuits by binary-decision programs. Bell Systems Technical Journal, 38:985–999, 1959.
E. A. Lee and D. G. Messerschmitt. Static scheduling of synchronous data flow programs for digital signal processing. IEEE Transactions on Computers, C-36(1):24–35, 1987.
E. A. Lee and D. G. Messerschmitt. Synchronous data flow. Proceeding of the IEEE, 75(9):1235–1245, 1987.
C. E. Leiserson and J. B. Saxe. Retiming synchronous circuitry. Algorithmica, 6(1):5–35, 1991.
B. Lickly, I. Liu, S. Kim, H. D. Patel, S. A. Edwards, and E. A. Lee. Predictable programming on a precision timed architecture. In Proceedings of Compilers, Architectures, and Synthesis of Embedded Systems (CASES), Atlanta, Georgia, USA, October 19–24, 2008.
N. Liveris, C. Lin, J. Wang, H. Zhou, and P. Banerjee. Retiming for synchronous data flow graphs. In ASP-DAC ’07: Proceedings of the 2007 Asia and South Pacific Design Automation Conference, pages 480–485, Washington, DC, USA, 2007. IEEE Computer Society.
O. Marchetti and A. Munier-Kordon. Minimizing place capacities of weighted event graphs for enforcing liveness. Discrete Event Dynamic Systems, 18(1):91–109, 2008.
O. Marchetti and A. Munier-Kordon. A sufficient condition for the liveness of weighted event graphs. European Journal of Operational Research, 197(2):532–540, 2009.
K. L. McMillan. Symbolic Model Checking. Kluwer, Dordrecht, 1993.
T. O’Neil and E.-M. Sha. Retiming synchronous data-flow graphs to reduce execution time. IEEE Transactions on Signal Processing, 49(10):2397–2407, 2001.
H. D. Patel and S. K. Shukla. SystemC Kernel Extensions For Heterogenous System Modeling: A Framework for Multi-MoC Modeling and Simulation. Kluwer, Norwell, MA, USA, 2004.
C. A. Petri. Kommunikation mit Automaten. PhD thesis, Institut für instrumentelle Mathematik, Bonn, Germany, 1962.
D. Potop-Butucaru, S. A. Edwards, and G. Berry. Compiling Esterel. Springer, Berlin, 2007.
J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In International Symposium on Programming, 1982.
C. Ramchandani. Analysis of Asynchronous Concurrent Systems by Timed Petri Nets. PhD thesis, Dept. of Electrical Engineering, Massachusetts Institute of Technology, Cambridge, MA, USA, 1973.
M. D. Riedel. Cyclic Combinational Circuits. PhD thesis, Dept. of Electrical Engineering, California Institute of Technology, Pasadena, CA, USA, November 2003.
K. Schneider. The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany, 2009.
J. Sermulins. Cache aware optimization of stream programs. In Proceedings of LCTES, 2005.
C. Soviani, O. Tardieu, and S. A. Edwards. High-level optimization by combining retiming and shannon decomposition. In In Proceedings of the International Workshop on Logic and Synthesis (IWLS), Lake Arrowhead, CA, June, 2005.
S. Suhaib, D. Mathaikutty, D. Berner, and S. K. Shukla. Validating families of latency insensitive protocols. IEEE Transactions on Computers, 55(11):1391–1401, 2006.
S. Suhaib, D. Mathaikutty, S. K. Shukla, D. Berner, and J.-P. Talpin. A functional programming framework for latency insensitive protocol validation. Electronic Notes in Theoretical Computer Science, 146(2):169–188, 2006.
C. Svensson. Synchronous latency insensitive design. In Proc. of 10th IEEE International Symposium on Asynchronous Circuits and Systems, 2004.
W. Thies, M. Karczmarek, M. Gordon, D. Maze, J. Lin, A. Meli, A. Lamb, C. Leger, and S. Amarasinghe. Streamit: a language for streaming applications. In Proceedings of New England Programming Languages and Systems Symposium (NEPLS), 2002.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer US
About this chapter
Cite this chapter
Boucaron, J., Coadou, A., de Simone, R. (2010). Formal Modeling of Embedded Systems with Explicit Schedules and Routes. In: Shukla, S., Talpin, JP. (eds) Synthesis of Embedded Software. Springer, Boston, MA. https://doi.org/10.1007/978-1-4419-6400-7_2
Download citation
DOI: https://doi.org/10.1007/978-1-4419-6400-7_2
Published:
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-6399-4
Online ISBN: 978-1-4419-6400-7
eBook Packages: EngineeringEngineering (R0)