This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Starvation and Critical Race Analyzers for Ada
August 1990 (vol. 16 no. 8)
pp. 829-843

Starvation and critical race analysis tools for Ada designs are described. These tools are part of a temporal analysis toolset that includes an operational specification language, a language interpreter, and a deadlock analyzer for Ada. The starvation analyzer is based on a set-theoretic model of starvation. It uses a proof tree produced by the deadlock analyzer to define the possible computation space of the design. A preprocessing phase of the starvation tool optimizes the analysis so that the resulting analysis is efficient. Unlike livelock analysis in state machines, the starvation analyzer does not require a priori specification of home states to discern liveness. The critical race analysis tool provides semiautomatic proof of critical races by identifying nondeterministic rendezvous (races) from the proof tree generated by the deadlock analyzer, and then assisting the human operator in identifying which of these constitute critical races. Several design examples are used to demonstrate the capabilities of the two analysis methods.

[1] G. V. Bochmann, "Finite state descriptions of communication protocols,"Comput. Networks, vol. 2, pp. 361-372, Oct. 1978.
[2] D. Brand and P. Zafiropulo, "On communicating finite state machines,"J. ACM, vol. 30, no. 2, pp. 323-342, Apr. 1983.
[3] R. J. A. Buhr,System Design with Ada. Englewood Cliffs, NJ: Prentice-Hall, 1984.
[4] R. J. A. Buhr, G. M. Karam, and C. M. Woodside, "An overview and example application of CAEDE: A new design environment for Ada,"Int. Ada Conf., Paris, France, May 1985.
[5] R. J. A. Buhr, G. M. Karam, C. J. Hayes, and C. M. Woodside, "Software CAD: A revolutionary approach,"IEEE Trans. Software Eng., vol. 15, no. 3, pp. 235-249, Mar. 1989.
[6] W. F. Clocksin and C. S. Mellish,Programming in Prolog. New York: Springer-Verlag, 1984.
[7] P. J. Courtois, F. Heymans, and D. L. Parnas, "Concurrent control with readers and writers,"Commun. ACM, vol. 14, no. 2, pp. 667- 668, Oct. 1971.
[8] H. M. Deitel,An Introduction to Operating Systems. Reading, MA: Addison-Wesley, 1984.
[9] G. Estrin, R. S. Fenchel, R. R. Razouk, and M. K. Vernon, "SARA (System ARchitects Apprentice): Modeling, analysis, and simulation support for design of concurrent systems,"IEEE Trans. Software Eng., vol. SE-12, no. 2, pp. 293-311, Feb. 1986.
[10] N. Francez,Fairness. New York: Springer-Verlag, 1986.
[11] D. Helmbold and D. Luckham, "Debugging Ada tasking programs,"IEEE Software, vol. 2, no. 2, pp. 47-57, Mar. 1985.
[12] R. C. Holt, E. D. Lazowska, G. Scranaham, and M. A. Scott,Structured Concurrent Design with Operating System Applications. Reading, MA: Addison-Wesley, 1978.
[13] G. M. Karam, "A tool-set for temporal analysis in a design environment for concurrent systems," Ph.D. dissertation, Dep. Syst. Comput. Eng., Carleton Univ., Ottawa, Ont., Canada, Tech. Rep. SCE- 87-2, Dec. 1986.
[14] G. M. Karam and R. J. A. Buhr, "Embedding design knowledge in CAEDE: Experiments on the detection of critical races," inProc. 2nd Int. Conf. Ada Applications and Environments, Miami Beach, FL, Apr. 1986, pp. 93-98.
[15] G. M. Karam and R. J. A. Buhr, "A temporal logic-based operational specification language, interpreter, and deadlock analyzer for Ada," Dep. Syst. Comput. Eng., Carleton Univ., Ottawa, Ont., Canada, Tech. Rep. SCE-87-7, Aug. 1987.
[16] G. M. Karam and R. J. A. Buhr, "Experience with the automatic temporal analysis of multitasking Ada designs," inProc. Int. Ada Conf., Boston, MA, Dec. 1987, pp. 36-44.
[17] G. M. Karam, C. Stanczyk, and G. Bond, "Critical races in Ada,"IEEE Trans. Software Eng., vol. SE-15, no. 11, pp. 1471-1480, Nov. 1989.
[18] G. M. Karam, R. J. A. Buhr, C. M. Woodside, and R. Casselman, "TimeBench: A next generation CASE tool," Tech. Rep. SCE-89- 18, Dep. Syst. Comput. Eng., Carleton Univ., Ottawa, Ont., Canada, July 1989 (also appears in SigAda Ottawa Meeting, Aug. 1989 Proc.).
[19] Y. S. Kwong, "On the absence of livelocks in parallel programs," inSemantics of Concurrent Computation (Lecture Notes in Computer Science, vol. 70). New York: Springer-Verlag, 1979, pp. 172-190.
[20] J. L. Peterson, "Petri nets,"ACM Comput. Surveys, vol. 9, no. 3, pp. 223-252, Sept. 1977.
[21] A. Pnueli and W. P. DeRoever, "Rendezvous with Ada--A proof theoretic view," inProc. AdaTEC Conf. Ada, Arlington, VA, Oct. 1982, pp. 129-137.
[22] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[23] U.S. Dep. Defense,Reference Manual for the Ada Programming Language, MIL-STD-1815a, 1983.
[24] P. M. Winston,Artificial Intelligence. Reading, MA: Addison-Wesley, 1984.

Index Terms:
race analyzers; critical race analysis tools; Ada designs; temporal analysis toolset; operational specification language; language interpreter; deadlock analyzer; starvation analyzer; set-theoretic model; deadlock analyzer; computation space; preprocessing phase; starvation tool; liveness; semiautomatic proof; nondeterministic rendezvous; human operator; design examples; Ada; program interpreters; programming; software tools; specification languages; system recovery.
Citation:
G.M. Karam, R.J.A. Buhr, "Starvation and Critical Race Analyzers for Ada," IEEE Transactions on Software Engineering, vol. 16, no. 8, pp. 829-843, Aug. 1990, doi:10.1109/32.57622
Usage of this product signifies your acceptance of the Terms of Use.