Tight WCRT analysis of synchronous C programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Tight WCRT analysis of synchronous C programs

Full text

Pdf (762 KB)

Source

International Conference on Compilers, Architecture and Synthesis for Embedded Systems archive
Proceedings of the 2009 international conference on Compilers, architecture, and synthesis for embedded systems table of contents

Grenoble, France

SESSION: Microfluidics, worst-case execution time, and cache optimization table of contents

Pages 205-214

Year of Publication: 2009

ISBN:978-1-60558-626-7

Authors

Partha S. Roop	The University of Auckland, Auckland, New Zealand
Sidharta Andalam	The University of Auckland, Auckland, New Zealand
Reinhard von Hanxleden	Christian-Albrechts-University , Kiel, Germany
Simon Yuan	The University of Auckland, Auckland, New Zealand
Claus Traulsen	Christian-Albrechts-University , Kiel, Germany

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
ACM: Association for Computing Machinery
SIGBED: ACM Special Interest Group on Embedded Systems
SIGMICRO: ACM Special Interest Group on Microarchitectural Research and Processing

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 7, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1629395.1629424 What is a DOI?

ABSTRACT

Accurate estimation of the tick length of a synchronous program is essential for efficient and predictable implementations that are devoid of timing faults. The techniques to determine the tick length statically are classified as worst case reaction time (WCRT) analysis. While a plethora of techniques exist for worst case execution time (WCET) analysis of procedural programs, there are only a handful of techniques for determining the WCRT value of synchronous programs. Most of these techniques produce overestimates and hence are unsuitable for the design of systems that are predictable while being also efficient. In this paper, we present an approach for the accurate estimation of the exact WCRT value of a synchronous program, called its tight WCRT value, using model checking. For our input specifications we have selected a synchronous C based language called PRET-C that is designed for programming Precision Timed (PRET) architectures. We then present an approach for static WCRT analysis of these programs via an intermediate format called TCCFG. This intermediate representation is then compiled to produce the input for the model checker.

Experimental results that compare our approach to existing approaches demonstrate the benefits of the proposed approach. The proposed approach, while presented for PRET-C is also applicable for WCRT analysis of Esterel using simple adjustments to the generated model. The proposed approach thus paves the way for a generic approach for determining the tight WCRT value of synchronous programs at compile time.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	UPPAAL tool. www.uppaal.com. last accessed on 29.4.09.
	2	R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183--235, 1994.
	3	S. Andalam, P. Roop, A. Girault, and C. Traulsen. PRET-C: A new language for programming precision timed architectures. Technical Report 6922, INRIA Grenoble RhÆone-Alpes, 2009. http://hal.inria.fr/inria-00391621/fr/,2009.
	4	G. R. Andrews. Concurrent Programming: Principles and Practice. Benjamin/Cummings, 1991.
	5	M. Boldt, C. Traulsen, and R. von Hanxleden. Worst case reaction time analysis of concurrent reactive programs. Electronic Notes in Theoretical Computer Science, 203(4):65--79, June 2008.
	6	F. Boussinot. Reactive C: An extension of C to program reactive systems. In SOFTWARE PRACTICE AND EXPERIENCE, VOL. 21(4), 401--428, APRIL 1991.
	7	E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.
	8	S. A. Edwards. Estbench Esterel benchmark suite. http://www1.cs.columbia.edu/ sedwards/software/estbench-1.0.tar.gz.
	9	S. A. Edwards and E. A. Lee. The case for the precision timed (PRET) machine. In Proceedings of the 44th DAC, pages 264--265, June 2007.
	10	L. Ju, B. K. Huynh, A. Roychoudhury, and S.Chakraborty. Performance debugging of Esterel specifications. In CODES+ISSS, pages 173--178, 2008.
	11	F. Laroussinie, N. Markey, and P. Schnoebelen. Model checking timed automata with one or two clocks. In CONCUR, pages 387--401, 2004.
	12	L. Lavagno and E. Sentovich. ECL: A specification environment for system-level design. In Proceedings of Design Automation Conference (DAC), New Orleans, June 1999.
	13	X. Li, M. Boldt, and R. von Hanxleden. Mapping Esterel onto a multi-threaded embedded processor. SIGARCH Comput. Archit. News, 34(5):303--314, 2006.
	14	B. Lickly, I. Liu, S. Kim, H. D. Patel, S. A. Edwards, and E. A. Lee. Predictable programming on a precision timed architecture. In In Proceedings of International Conference on Compilers, Architecture, and Synthesis from Embedded Systems (CASES), October 2008.
	15	G. Logothetis, K. Schneider, and C. Metzler. Generating formal models for real-time verification by exact low-level runtime analysis of synchronous programs. In RTSS, pages 256--264, Cancun, Mexico, 2003. IEEE Computer Society.
	16	M. Mendler, R. von Hanxleden, and C. Traulsen. WCRT algebra and interfaces for Esterel-style synchronous processing. In Proceedings of the Design, Automation and Test in Europe (DATE'09), Nice, France, April 2009.
	17	A. Metzner. Why model checking can improve WCET analysis. In CAV, volume LNCS-3114, pages 334--347, 2004.
	18	R. Milner. Communication and Concurrency. Prentice Hall, 1989.
	19	P. S. Roop, Z. Salcic, and M. W. S. Dayaratne. Towards direct execution of Esterel programs on reactive processors. In 4th ACM EMSOFT, 2004.
	20	R. Sinha, P. S. Roop, S. Basu, and Z. Salcic. Multiclock SoC design using protocol conversion. In Design Automation and Test in Europe (DATE), 2009.
	21	F. Vahid and T. Givargis. Embedded System Design. John Wiley and Sons, 2002.
	22	R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S.Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenström. The worst-case execution-time problem-overview of methods and survey of tools. Trans. on Embedded Computing Sys., 7(3):1--53, 2008.
	23	Xilinx. Microblaze Processor Reference Guide, 2008.
	24	S. Yuan, L. H. Yoong, S. Andalam, P. S. Roop, and Z. Salcic. A new multithreaded architecture supporting direct execution of Esterel. EURASIP Journal on Embedded Systems, 2009:Article ID 610891, 19 pages, 2009. doi:10.1155/2009/610891.