65Accesses
2Citations
Abstract
Enabled by RISC technologies, low-cost commodity microprocessors are performing at ever increasing levels, significantly via instruction level parallelism (ILP). This in turn increases the opportunities for their use in a variety of day-to-day applications ranging from the simple control of appliances such as microwave ovens, to sophisticated systems for cabin control in modern aircraft. Indeed, “embedded” applications such as these represent segments in the computer industry with great potential for growth. However, this growth is currently impeded by the lack of robust optimizing compiler technologies that support the assured, rapid and inexpensive prototyping of real-time software in the context of microprocessors with ILP. In this paper we describe a novel notation, TimeC, for specifying timing constraints in programs,independent of the base language being used to develop the embedded application; TimeC specifications are language independent and can be instrumented into imperative and object-oriented languages non-intrusively. As we will show, the program synthesis problem that arise out of Time_tract specifications, a subset of TimeC, are always “tractable.” In contrast, a range of specification mechanisms proposed earlier yield substantially intractable synthesis questions, thereby limiting their potential utility. We will compare the tractability and related expressive power issues between TimeC and some of the extant mechanisms for specifying properties of timed programs.
This is a preview of subscription content,log in via an institution to check access.
Access this article
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
Price includes VAT (Japan)
Instant access to the full article PDF.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Aiken, A., & Nicolau, A. (1987). Loop quantization; an analysis and algorithm. Technical Report 87-821, Cornell University.
Allen, J. R., Kennedy, K., Porterfield, C., & Warren, J. (1983). Conversion of contgrol dependence to data dependence. InProceedings of the 10th ACM Symposium on Principles of Programming Languages, pages 177–189.
Alur, R., & Dill, D. (1994). A theory of timed automata.Theoretical Computer Science, 126: 183–235.
Alur, R., & Henzinger, T. A. (1989). A really temporal logic. InProceedings of the 30th IEEE Symposium Found. of Comp. Sci., pages 164–169.
Alur, R., & Henzinger, T. A. (1990). Real-time logics: Complexity and expressiveness. InProceedings of the 5th IEEE Symposium Logic in Comp. Sci., pages 390–401.
Alur, R., & Henzinger, T. (1992). Logics and models of real time: A survey. In de Bakker, J. W., Huizing, C., de Roever, W. P., & Rozenberg, G., eds.,Proceedings of the REX Workshop “Real-Time: Theory in Practice,” Vol. 600 of Lect. Notes in Comp. Sci., pages 74–106. Springer-Verlag.
Bernstein, A., & Harter, P. K. (1981). Proving real time properties of programs with temporal logic. InProceedings of the Eighth Symposium on Operating Systems Principles, pages 1–11. ACM.
Bernstein, D., & Rodeh, M. (1991). Global instruction scheduling for superscalar machines. InProceedings of SIGPLAN'91 Conference on Programming Language Design and Implementation.
Fisher, J. (1981). Trace scheduling: A general technique for global microcode compaction.IEEE Transactions on Computers, C-30(7): 478–490.
Fisher, J. (1991). Global code generation for instruction-level parallelism: Trace scheduling-2. Technical report, HP Labs.
Harel, E., Lichtenstein, O., & Pnueli, A. (1990). Explicit clock temporal logic. InProceedings of the 5th IEEE Symposium Logic in Comp. Sci., pages 402–413.
Hoare, C. A. R. (1969). An axiomatic basis for computer programming.Communication of the ACM, 12: 576–580.
Hong, S., & Gerber, R. (1995). Compiling real-time programs with timing constraint refinement and structural code motion.IEEE Transactions on Software Engineering, 21.
Intel and Hewlett Packard Corporations. (1997). Press releases on Intel's IA-64. http://www.intel.com/pressroom/kits/events/mpf1097.htm.
Jahnaian, F., & Mok, A. K. (1986). Safety analysis of timing properties in real-time systems.IEEE Transactions on Software Engineering, SE-12(9): 890–904.
Jahnaian, F., & Mok, A. K. (1987). A graph-theoretic approach for timing analysis and its implementation.IEEE Transactions on Computers, C36(8).
Kernigan, B. W., & Richie, D. M. (1988).The C Programming Language. Prentice Hall, 2nd ed.
Koymans, R. (1990). Specifying real-time properties with metric temporal logic.Real-Time Systems, 2(4): 255–299.
Koymans, R., & de Roever, W.-P. (1985). Examples of a real-time temporal logic specifications. In Denvir, B. D., Harwood, W. T., Jackson, M. I., & Wray, M. J., eds.,The Analysis of Concurrent Systems, Vol. 207 of Lect. Notes in Comp. Sci., pages 231–252. Springer-Verlag.
Koymans, R., Vytopyl, J., & de Roever, W.-P. (1983). Real-time programming and asynchronous message passing. InProceedings of the Second ACM Symposium Princ. of Dist. Comp., pages 187–197.
Lam, M. (1988). Software pipelining: An effective scheduling technique for vliw machines.Proceedings SIGPLAN'88 Symposium on Programming Language Design and Implementation, pages 318–328.
Leung, A., Palem, K., & Pnueli, A. (1998). A fast algorithm for scheduling time-constrained instructions on processor with ILP. InThe International Conference on Parallel Architectures and Compilation Techniques (PACT’ 98).
Manna, Z., & Pnueli, A. (1981). Verification of concurrent programs: The temporal framework. In Boyer, R. S. & Moore, J. S., eds.,The Correctness Problem in Computer Science, pages 215–273. Academic Press, London.
Nachiappan, N. (1995). Personal communications and memorandum of support.
Ostroff, J. S. (1990).Temporal Logic of Real-Time Systems. Advanced Software Development Series. Research Studies Press, John Wiley & Sons, Taunton, England.
Palem, K., & Sarkar, V. (1995).Code Optimization in Modern Compilers. Western Institute of Computer Science, Stanford University, CA.
Rau, B. (1994). Iterative modulo scheduling: An algorithm for software pipelining loops. InProceedings of the 27th Annual Symposium on Microarchitecture, December.
Sethi, R., Aho, A., & Ullman, J. (1984).Compiler Construction. Addison-Wessley.
Shaw, A. (1989). Reasoning about time in higher-level language software.IEEE Transactions on Software Engineering, 15(7): 875–889.
Stoyenko, A. D., Marlowe, T. J., & Laplante, P. A. (1996). A description language for engineering of complex real-time systems. Technical Report cis9522, New Jersey Institute of Technology.
Stoyenko, A. D., Marlowe, T. J., & Younis, M. F. (1996). A language for complex real-time systems. Technical Report cis9521, New Jersey Institute of Technology.
Stroustrup, B. (1990).The C++ Programming Language. Addison-Wesley, 2nd ed.
Water, N., Mahlke, S., Hwu, W. M., & Rau, B. (1993). Reverse If-conversion. InACM SIGPLAN PLDI, pages 290–299.
Author information
Authors and Affiliations
Courant Institute of Mathematical Sciences, New York University, USA
Allen Leung & Krishna V. Palem
The Weizmann Institute of Science, USA
Amir Pnueli
- Allen Leung
You can also search for this author inPubMed Google Scholar
- Krishna V. Palem
You can also search for this author inPubMed Google Scholar
- Amir Pnueli
You can also search for this author inPubMed Google Scholar
Rights and permissions
About this article
Cite this article
Leung, A., Palem, K.V. & Pnueli, A. TimeC: A Time Constraint Language for ILP Processor Compilation.Constraints7, 75–115 (2002). https://doi.org/10.1023/A:1015131814255
Issue Date:
Share this article
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative