Formal timing analysis for distributed real-time programs
Tóm tắt
A static analysis method for verifying timing properties of real-time distributed programs is presented. The goal is to calculate the worst-case response time of concurrent tasks which run mainly independently but share, and may have to wait for, logical or physical devices. For such tasks, the determination of the worst-case waiting time is a crucial problem because of the unpredictable order of synchronization events. We investigate the class of distributed Client-Server programs in which independent, time-critical tasks (clients) are synchronized only through additional server tasks, playing the role of monitors or resource managers. This model follows well-known real-time design guidelines for distributed ADA programs proposed to enhance schedulability and synchronization analysis. Our formal analysis approach is flow graph oriented. It leads to generating reduced program paths each of which represents a sequence of ordered local and global operations, thus transforming and reducing the original problem of computing the worst-case waiting time of a concurrent task into a graph-theoretic problem of calculating the maximal blocking time for one of its corresponding program paths. While local operations are completely independent global operations require mutually exclusive access to shared resources. We prove that computing the worst-case blocking time for a program path is NP-complete. Even for a reduced problem solution—which would yield a good upper bound for the worst-case blocking time—there was a conjecture maintained over many years that this problem was NP-complete. A major result of this paper is to show that this is wrong. Instead, we construct a polynomial solution algorithm, and we prove its correctness. The effectiveness and complexity of our method are discussed, with particular emphasis on distributed real-time debugging.
Tài liệu tham khảo
M. R. Garey and D. S. Johnson.Computers and Intractability. W. H. Freeman & Co., New York, 1979.
M. S. Hecht.Flow Analysis of Computer Programs. Elsevier North-Holland, 1977.
D. S. Hirschberg. A linear space algorithm for computing maximal common sequences.CACM, 18(6):341–349, 1987.
C. S. Hsieh. Timing analysis of cyclic concurrent programs. InProceedings of the International Conference Software Engineering, pages 312–318, May 1986.
D. Huizinga.Analysis of Timing properties for Distributed Real-Time Programs. Ph.D. Thesis, Wayne State University, August 1991.
F. Jahanian and A. K. Mok. A graph-theoretic approach for timing analysis and its implementation.IEEE Transactions on Computers, 36(8):961–975, 1987.
F. Jahanian and A. K. Mok. Safety analysis of timing properties in real-time systems.IEEE Transactions on Software Engineering, 12(3):890–904, 1986.
R. Koymans. Specifying real-time properties with metric temporal logic.Real-Time Systems, 2(4):255–299, 1990.
D. W. Leinbaugh and M-R. Yamini. Guaranteed response time in a distributed hard real-time environment.IEEE Transactions on Software Engineering, 12(12):1139–1144, 1986.
D. W. Leinbaugh and M-R. Yamini. Guaranteed response time in a distributed hard-real-time environment. InProc. of the IEEE Real-Time Systems Symposium, pages 157–169, Dec. 1982.
G. J. Myers.The Arts of Software Testing. John Wiley & Sons, 1979.
K. T. Narayana and A. A. Aaby. Specification of real-time systems in real-time interval logic. InProceedings of the Real-Time Systems Symposium, Huntsville, AL, pages 86–95, Dec. 1988.
V. Nirkhe and W. Pugh.Partial Evaluation of High-Level Imperative Programming Languages, with Applications in Hard Real-Time Systems, 9th ACM POPL Symposium, Albuquerque, pages 269–280, January 1992.
V. Nirkhe and W. Pugh.Application of Partial Evaluation to Hard Real-Time Programming, IEEE RTOSS'91, Atlanta/Georgia, May 1991.
C. Park and A. C. Shaw.Experiments with a Program Timing Tool on a Source-Level Timing Schema, IEEE RTSS'90, Orlando/Florida, December 1990.
P. Puschner and Ch. Koza. Calculating the maximum execution time of real-time programs.Real-Time Systems, 1(2):159–176, 1989.
R. L. Schwartz, P. M. Melliar-Smith, and F. H. Vogt. An interval logic for high-level temporal reasoning. InProceedings of the 2-nd Annual ACM Symposium on Principles of Distributed Computing, pages 173–185, 1983.
F. L. Schneider. Critical issues in real-time systems. Technical Report 88–914, Dept. of Computer Science, Cornell University (May 1988).
A. C. Shaw. Reasoning about time in higher-level language software.IEEE Transactions on Software Engineering, 15(7), 1989.
L. Sha and J. B. Goodenough. Real-time scheduling theory and Ada.IEEE Computer, April: 53–62, 1990.
J. A. Stankovic. Misconceptions about real-time computing.IEEE Computer, Oct.:10–19, 1988.
A. D. Stoyenko and T. J. Marlowe. Polynomial-time transformations and schedulability analysis of parallel real-time programs with restricted resource contention.Real-Time Systems, 4(4), 1992.
A. D. Stoyenko. A schedulability analyzer for real-time Euclid. InProceedings of the IEEE Real-Time Systems Symposium, San Jose, CA, pages 218–227, Dec. 1987.
A. D. Stoyenko, V. C. Hamacher, and R. C. Holt. Analyzing hard real-time programs for guaranteed schedulability.IEEE Transactions on Software Engineering, 17(8), 1991.
R. Taylor. A general-purpose algorithm for analyzing concurrent programs.CACM, 26(5):362–376, 1983.
H. F. Wedde, B. Korel, and D. M. Huizinga. A critical path approach for testing distributed real-time programs. InProceedings of the 24-th International Hawaiian Conference on System Sciences, Kauwai/Hawaii, vol. 2, pages 400–407, Jan. 1991.
N. Wirth. Toward a discipline of real-time programming.CACM, 20(8):577–583, 1977.