Abstract
Static analysis may cause state space explosion problem. In this paper we demonstrate how ordinary differential equations can be used to check the deadlocks and boundedness of the programs. We hope that our method can avoid explosion of state space entirely. A concurrent program is represented by a family of differential equations of a restricted type, where each equation describes the program state change. This family of equations are shown analytically to have a unique solution. Each program state is measured by a time-dependent function that indicates the extent to which the state can be reached in execution. It is shown that 1) a program deadlocks iff every state measure converges to either 0 or 1 as time increases. Thus instead of exploring states, the solution of a family of differential equations is analyzed. 2) a program is bounded iff every state measure converges to a bounded nonnegative number.
Supported by NSF of China(No.90818013).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Transactions on Software Engineering and Methodology 6(3), 213–249 (1997)
Ascher, U.M., Petzold, L.R.: Computer Methods for Ordinary Differential Equations and Differential-Algebraic Equations. Society for Industrial & Applied Mathematis, Philadelphia (1998)
Avrunin, G.S., Buy, U.A., Corbett, J.C., Dillon, L.K., Wileden, J.C.: Automated Analysis of Concurrent Systems with the Constrained Expression Toolset. IEEE Transactions on Software Engineering 17(11), 1204–1222 (1991)
Badal, D.Z.: The Distributed Deadlock Detection Algorithm. ACM Transactions on Computer Systems 4(4), 320–377 (1986)
Ben-Ari, M.: Principles of Concurrent and Distributed Programming, 2nd edn. Addison-Wesley, Reading (2006)
Burch, J.R., Clarke, E.M., Long, D.E.: Representing circuts more efficiently in symbolic model checking, In. In: Proceedings of the 28th Design Automation Conference, pp. 403–407. IEEE Computer Society Press, Los Alamltos (1991)
Boukerche, A., Tropper, C.: A Distributed Graph Algorithm for the Detection of Local Cycles and Knots. IEEE Trans. Parallel and Distributed Systems 9(8), 748–757 (1998)
Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic Model Checking: 1020 States and Beyond. Information and Computation 9(2), 142–170 (1992)
Chandy, K.M., Misra, J., Haas, L.M.: Distributed Deadlock Detection. ACM Transactions on Computer Systems 1(2), 144–156 (1983)
Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction. ACM Transactions on Programming Language Systems 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E., McMillan, K., Campos, S., Hartonas-Garmhausen, V.: Symbolic Model Checking. In: Proceedings of 8th Computer Aided Verification Conference. Springer, Berlin (1996)
Corbett, J.C.: Evaluating Deadlock Detection Methods for Concurrent Software. IEEE Transactions on Software Engineering 22(3), 161–180 (1996)
Corbett, J.C., Avrunin, G.S.: Using integer programming to verify general safety and liveness properties. Formal Methods in System Desin 6, 97–123 (1995)
David, R., Alla, H.: Continuous Petri nets. In: Proceedings of 8th European Workshop on Application and Theory of Petri nets, Zaragoza, Spain, pp. 275–294 (1987)
David, R., Alla, H.: Autonomous and timed continuous Petri nets. In: Proceedings of 11th Int. Conf. on Application and Theory of Petri nets, Paris, France, pp. 367–381 (1990)
Dijkstra, E.W.: Hierarchical Ordering of Sequential Processes. Acta Informat 2, 115–138 (1971)
Dijkstra, E.W., Scholten, C.S.: Termination Detection for Diffusing Computations. Information Processing Letters 11(1), 1–4 (1980)
Ding, Z., Xiao, L., Hu, J.: Performance analysis of service composition using ordinary differential equations. In: Proceedings of FTDCS 2008, Kunming, China, October 21-23. IEEE Computer Society Press, Los Alamitos (2008)
Ding, Z., Zhang, K.: Performance analysis of concurrent programs using ordinary differential equations. In: COMPSAC 2008, Turku, Finland, July 28-August 1. IEEE Computer Society Press, Los Alamitos (2008)
Ding, Z., Zhang, K., Hua, J.: A Rigorous Approach Towards Test Case Generation. Information Sciences 178, 4057–4079 (2008)
Duri, S., Buy, U., Devarapalli, R., Shatz, S.M.: Application and Experimental Evaluation of State Space Reduction Methods for Deadlock Analysis in Ada. ACM Transactions on Software Engneering and Methodology 3(4), 340–380 (1994)
Dwyer, M.B., Clarke, L.A.: Data flow analysis for verifying properties of concurrent programs. In: Proc. Second Symp. Foundations of Software Enginemng, pp. 62–75 (1994)
Gilbert, D., Heiner, M.: From Petri nets to differential equations-an integrative approach for biochemical network analysis. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 181–200. Springer, Heidelberg (2006)
Goltz, U., Reisig, W.: Weighted Synchronic Distance. In: Application and Theory of Petri Nets, Informatik Fachberichte, vol. 52. Springer, Heidelberg (1982)
Dwyer, M.B., Clarke, L.A.: A compact Petri Net Representation and Its Implications for Analysis. IEEE Transactions on Software Engineering 22(11), 794–811 (1996)
Godefroid, P., Pirottin, D.: Refining Dependendes Improves Partial- Order verification Methods. In: Courcoubetis (ed.) Proc. Fifth lnt’l conf: Computer Aided Verfication, Elounda, Greece, pp. 438–449 (1993)
Hale, J.K.: Ordinary Differential Equations. Interscience, New York (1969)
Hairer, E., Nφrsett, S.P., Wanner, G.: Solving Ordinary Differential Equations(I), Nonstiff Problems, 2nd edn. Springer, Heidelberg (1993)
Helmbold, D., Luckham, D.: Debugging Ada tasking programs. IEEE Software 2(2), 47–57 (1985)
Herrmann, J.W., Lin, E.: Petri Nets: Tutorial and Applications. In: The 32th Annual Symposium of the Washington Operations Research-Management Science Council, Washington, D.C., November 5 (1997)
Hoare, C.A.R.: Communicating sequential processes. Communication of ACM 21(8), 666–677 (1978)
Holt, R.C.: Some Deadlock Properties on Computer Systems. ACM Compuling Surveys 4(3), 179–196 (1972)
Holzmann, G.J.: Basic Spin Manual (1980), http://cm.bell-labs.com/netlib/spin/whatispin.html
Huang, S.T.: A Distributed Deadlock Detection Algorithm for CSP-Like Communication. ACM Transactions on Programming Languages and Systems 12(1), 102–122 (1990)
Intievergelt, J.: Parallel methods for integrating ordinary differential equations. Communications of the ACM 7(12), 731–733 (1964)
Juan, E., Tsai, J.J.P., Murata, T.: Compositional verification of concurrent systems using Petri-nets-based condensation rules. ACM Transactions on Programming Languages and Systems 20(3), 917–979 (1998)
Karam, G.M., Buhr, R.J.: Starvation and Critical Race Analyzers For Ada. IEEE Transactions on Software Engineering 16(8), 829–843 (1990)
Kim, Y.M., Lai, T.H., Soundarajan, N.: Efficient Distributed Deadlock Detection and Resolution Using Probes, Tokens, and Barriers. In: Proc. Int’l Conf. Parallel and Distributed Systems, pp. 584–591 (1997)
Lee, S.: Fast, Centralized Detection and Resolution of Distributed Deadlocks in the Generalized Model. IEEE Transactions on Software Engineering 30(9), 561–573 (2004)
Lin, B.: Efficient Compilation of Process-based Concurrent Programs Without Run-time Scheduling. In: Proceedings of Design, Automation, and Test in Europe (DATE), Paris, pp. 211–217 (1998)
Long, D.L., Clarke, L.A.: Task Interaction Graphs for Concurrency Analysis. In: Proc. 11th lntl. Conf. Software Eng, Pittsburgh, Penn, pp. 44–52 (1989)
Lunze, J., Nixdorf, B., Richter, H.: Hybrid modelling of continuous-variable systems with application to supervisory control. In: Proceedings of the European Control Conference 1997, Brussels, Belgium (1997)
Mandrioli, D., Zicari, R., Ghezzi, C., Tisato, F.: Modeling the Ada Task System by Petri nets. Computer Languages 10(1), 43–61 (1985)
Masticola, S.P., Ryder, E.G.: Static Infinite Wait Anomaly Detection in Polynomial Time. In: Proceedings of 1990 International Conference on Parallel Processing, vol. 2, pp. 78–87 (1990)
Math Department, East China Normal University: Mathematics Analysis (I)(II), 3rd edn. High education Press, China (2001)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)
Misra, J., Chandy, K.M.: A Distributed Graph Algorithm: Knot Detection. ACM Transactions on Programming Languages and Systems 4(4), 678–686 (1982)
Molloy, M.K.: Fast bounds for stochastic Petri nets. In: International Workshop on Timed Petri Nets, Torino, July 1985, pp. 244–249 (1985)
Morgan, E.T., Razouk, R.R.: Interactive State Space Analysis of Concurrent Systems. IEEE Transitions on Software Engineering 12(10), 1080–1091 (1987)
Natarajan, N.: A Distributed Scheme for Detecting Communication Deadlocks. IEEE Transactions on Software Engineering SE-12(4), 531–537 (1986)
Naumovich, G., Avrunin, G., Clarke, L.: Applying Static Analysis to Software Architectures. ACM SIGSOFT Notes 22(6), 77–93 (1997)
Ng, W.K., Ravishankar, C.V.: On-Line Detection and Resolution of Communication Deadlocks. In: Proc. 27th Ann. Hawaii Int’l Conf. System Science, pp. 524–533 (1994)
Notomi, M., Murata, T.: Hierarchical Reachability Graph of Bounded Petri Nets for Concurrent-Software Analysis. IEEE Transactions on Software Engineering 20(5), 325–336 (1994)
Obermarck, R.: Distributed Deadlock Detection Algorithm. ACM Trans. Database Syst. 7(2), 187–208 (1982)
Peleties, P., DeCarlo, R.: Analysis of hybrid systems using symbolic dynamics and Petri nets. Automatica 30(9), 1421–1427 (1994)
Peterson, J.L., Silberschatz, A.: Operating System Concepts. Addison-Wesley, Reading (1983)
Pezzé, M., Taylor, R.N., Young, M.: Graph Models for Reachability Analysis. ACM Transactions on Software Engmeermg and Methodology 4(2), 171–213 (1995)
Reif, J.H., Smolka, S.A.: Data flow analysis of distributed communicating processes. Journal of Parallel Programming 19(1), 1–30 (1990)
Rontogiannis, P., Pavlides, G., Levy, A.: Distributed Algorithm for Communication Deadlock Detection. Information and Software Technology 33(7), 483–488 (1991)
Royden, H.L.: Real Analysis, 3rd edn. Macmillan Publishing Co., New York (1988)
Scheibler, D.: A Software Tool for Design and Simulation of Continuous Petri Nets (in German), Master Thesis, BTU Cottbus, Dep. of CS (2006)
Shatz, S.M., Mai, K., Black, C., Tu, S.: Design and Implementation of A Petri Net-based Toolkit for Ada Tasking analysis. IEEE Trans. Par. Dist. Syst. 1(4), 424–441 (1990)
Shih, C.-S., Stankovic, J.A.: Distributed Deadlock Detection in Ada Runtime Environments (1990)
Singhal, M.: Deadlock Detection in Distributed Systems. IEEE Computer 22, 37–48 (1989)
Sistla, A.P., Miliades, L., Gyuris, V.: SMC: A symmetry based model checker for verification of liveness properties. In: Proceedings of 9th Computer Aided Verification Conference, Haifa, Israel (1997)
Smart, D.R.: Fixed Point Theorems. Cambridge Univ. Press, Cambridge (1974)
Taylor, R.: A general purpose algorithm for analyzing concurrent programs. Communication of ACM 26(5), 362–376 (1983)
Tsai, J.P., Xu, K.: An empirical evaluation of deadlock detection in software architecture specifications. Annals of Software Engineering 7, 95–126 (1999)
Tu, S., Shatz, S.M., Murata, T.: Theory and Application of Petri Net Reduction for Ada-Tasking Deadlock Analysls. Tech. Report 91-15, EECS Dept., Univ. of Illinois, Chicago (1991)
Valmari, A.: A stubborn attack on state explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991)
Wang, X., Kwiatkowska, M.: Compositional state space reduction using untangled actions. Electronic Notes in Computer Science 175(3), 27–46 (2007)
Wojcik, B.E., Wojcik, Z.M.: Sufficient Condition for a Communication Deadlock and Distributed Deadlock Detection. IEEE Transactions on Software Engineering 5(12), 1587–1595 (1989)
Yeh, W.J., Young, M.: Compositional Reachabhty Analysls Uslng procesS Algebra. In: Roc. Symp. Testing, Analysis, and Verfication (TAV4), pp. 178–187. ACM SIGSOFT, New York (1991)
Young, M., Taylor, R.N., Forester, K., Brodbeck, D.: Integrated Concurrency Analysis In A Software Development Environment. In: Proceedings of the ACM SIGSOFT 1989 3rd Symposium on Software Testing, Analysis and Verification. Software Engineering Notes, vol. 14(8), pp. 200–209 (1989)
Zhou, J., Tai, K.C.: Deadlock Analysis of Synchronous Message-Passing Programs. In: Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems, pp. 62–69 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ding, Z. (2009). Static Analysis of Concurrent Programs Using Ordinary Differential Equations. In: Leucker, M., Morgan, C. (eds) Theoretical Aspects of Computing - ICTAC 2009. ICTAC 2009. Lecture Notes in Computer Science, vol 5684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03466-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-03466-4_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03465-7
Online ISBN: 978-3-642-03466-4
eBook Packages: Computer ScienceComputer Science (R0)