Schedule-Carrying Code

  • Thomas A. Henzinger
  • Christoph M. Kirsch
  • Slobodan Matic
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2855)


We introduce the paradigm of schedule-carrying code (SCC). A hard real-time program can be executed on a given platform only if there exists a feasible schedule for the real-time tasks of the program. Traditionally, a scheduler determines the existence of a feasible schedule according to some scheduling strategy. With SCC, a compiler proves the existence of a feasible schedule by generating executable code that is attached to the program and represents its schedule. An SCC executable is a real-time program that carries its schedule as code, which is produced once and can be revalidated and executed with each use. We evaluate SCC both in theory and practice. In theory, we give two scenarios, of nonpreemptive and distributed scheduling for Giotto programs, where the generation of a feasible schedule is hard, while the validation of scheduling instructions that are attached to the programs is easy. In practice, we implement SCC and show that explicit scheduling instructions can reduce the scheduling overhead up to 35% and can provide an efficient, flexible, and verifiable means for compiling Giotto programs on complex architectures, such as the TTA.


Control Task Feasible Schedule Input Event Time Safety Initial Address 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Cai, Y., Kong, M.C.: Nonpreemptive scheduling of periodic tasks in uni- and multiprocessor systems. Algorithmica 15, 572–599 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise WCET determination for a real-life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 469–485. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  3. 3.
    Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, New York (1979)zbMATHGoogle Scholar
  4. 4.
    Henzinger, T.A., Horowitz, B., Kirsch, C.M.: Giotto: a time-triggered language for embedded programming. Proc. IEEE 91, 84–99 (2003)CrossRefGoogle Scholar
  5. 5.
    Henzinger, T.A., Kirsch, C.M.: The Embedded Machine: predictable, portable real-time code. In: Proc. Programming Language Design and Implementation, pp. 315–326. ACM, New York (2002)Google Scholar
  6. 6.
    Henzinger, T.A., Kirsch, C.M., Majumdar, R., Matic, S.: Time-safety checking for embedded programs. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 76–92. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Kirsch, C.M., Henzinger, T.A., Sanvido, M.A.A.: A Programmable Microkernel for Real-Time Systems. Technical Report CSD-03-1250, UC Berkeley (2003)Google Scholar
  8. 8.
    Kirsch, C.M., Sanvido, M.A.A., Henzinger, T.A., Pree, W.: A Giotto-based helicopter control system. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 46–60. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. 9.
    Kopetz, H.: Real-Time Systems: Design Principles for Distributed Embedded Applications. Kluwer, Dordrecht (1997)zbMATHGoogle Scholar
  10. 10.
    Necula, G.C.: Proof-carrying code. In: Proc. Principles of Programming Languages, pp. 106–119. ACM Press, New York (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Thomas A. Henzinger
    • 1
  • Christoph M. Kirsch
    • 1
  • Slobodan Matic
    • 1
  1. 1.EECSUniversity of CaliforniaBerkeley

Personalised recommendations