Abstract
This paper presents a new technique for refining the complex control structure of loops that occur in imperative programs. We first introduce a new way of describing program execution patterns – ( + ,·)-path expressions, which is a subset of conventional path expressions with the operators ∨ and ∗ eliminated. The programs induced by ( + ,·)-path expressions have no path interleaving or skipping-over inner loops, which are the two main issues that cause impreciseness in program analysis. Our refinement process starts from a conventional path expression \(\mathcal{E}\) obtained from the control flow graph, and aims to calculate a finite set of ( + ,·)-path expressions \(\{\mathfrak{e}_1, ..., \mathfrak{e}_n\}\) such that the language generated by path expression \(\mathcal{E}\) is equivalent to the union of the languages generated by each ( + ,·)-path expressions \(\mathfrak{e}_i\). In theory, a conventional path expression can potentially generate an infinite set of ( + ,·)-path expressions. To remedy that, we use abstract interpretation techniques to prune the infeasible paths. In practice, the refinement process usually converges very quickly.
We have applied our method to symbolic computation of average case bound for running time of programs. To our best knowledge it is the first tool that automatically computes average case bounds. Experiments on a set of complex loop benchmarks clearly demonstrate the utility of our tool.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Balakrishnan, G., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Refining the control structure of loops using static analysis. In: Proceedings of the Seventh ACM International Conference on Embedded Software, EMSOFT 2009, pp. 49–58. ACM, New York (2009)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)
Goldsmith, S.F., Aiken, A.S., Wilkerson, D.S.: Measuring empirical computational complexity. In: Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE 2007, pp. 395–404. ACM, New York (2007)
Gulavani, B.S., Gulwani, S.: A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 370–384. Springer, Heidelberg (2008)
Gulwani, S.: SPEED: Symbolic complexity bound analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 51–62. Springer, Heidelberg (2009)
Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. SIGPLAN Not. 44, 375–385 (2009)
Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: precise and efficient static estimation of program computational complexity. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 127–139. ACM, New York (2009)
Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI, pp. 292–304 (2010)
Healy, C., Sjödin, M., Rustagi, V., Whalley, D., Van Engelen, R.: Supporting timing analysis by automatic bounding of loop iterations. Real-Time Syst. 18, 129–156 (2000)
Knuth, D.E.: The Art of Computer Programming, 2nd edn. Fundamental Algorithms, vol. I. Addison-Wesley (1973)
Kröning, D.: Cprover benchmarking toolkit, http://www.cprover.org/software/benchmarks/
Le Métayer, D.: Ace: An automatic complexity evaluator. ACM Trans. Program. Lang. Syst. 10(2), 248–266 (1988)
Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Rosendahl, M.: Automatic complexity analysis. In: FPCA, pp. 144–156 (1989)
Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528–539 (1975)
Wegbreit, B.: Verifying program performance. J. ACM 23, 691–699 (1976)
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenström, P.: The worst-case execution time problem—overview of methods and survey of tools. ACM Transactions on Embedded Computing Systems (TECS) 7(3) (2008)
Wilhelm, R., Wachter, B.: Abstract interpretation with applications to timing validation. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 22–36. Springer, Heidelberg (2008)
Wolfram, S.: The Mathematica Book, 5th edn. Wolfram Media, Incorporated (2003)
Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 221–237. Springer, Heidelberg (2008)
Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491–504. Springer, Heidelberg (2005)
Chen, H.Y., Flur, S., Mukhopadhyay, S.: Termination proofs for linear simple loops. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 422–438. Springer, Heidelberg (2012)
Cook, B., Gulwani, S., Lev-ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination (2008)
Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 111–125. Springer, Heidelberg (2008)
Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 89–103. Springer, Heidelberg (2010)
Tarjan, R.E.: Fast algorithms for solving path problems. J. ACM 28, 594–614 (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Chen, H.Y., Mukhopadhyay, S., Lu, Z. (2013). Control Flow Refinement and Symbolic Computation of Average Case Bound. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-02444-8_24
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02443-1
Online ISBN: 978-3-319-02444-8
eBook Packages: Computer ScienceComputer Science (R0)