Skip to main content

Probabilistic Resource Analysis by Program Transformation

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9964))

Abstract

The aim of a probabilistic resource analysis is to derive a probability distribution of possible resource usage for a program from a probability distribution of its input. We present an automated multi-phase rewriting based method to analyze programs written in a subset of C. It generates a probability distribution of the resource usage as a possibly uncomputable expression and then transforms it into a closed form expression using over-approximations. We present the technique, outline the implementation and show results from experiments with the system.

M. Rosendahl—The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement no 318337, ENTRA - Whole-Systems Energy Transparency.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Adje, A., Bouissou, O., Goubault-Larrecq, J., Goubault, E., Putot, S.: Static analysis of programs with imprecise probabilistic inputs. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 22–47. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54108-7_2

    Chapter  Google Scholar 

  2. Bauer, M.: Approximations for decision making in the Dempster-Shafer theory of evidence. In: Horvitz, E., Jensen, F.V. (eds.) UAI, pp. 73–80. Morgan Kaufmann (1996)

    Google Scholar 

  3. Berleant, D., Cheng, H.: A software tool for automatically verified operations on intervals and probability distributions. Reliable Comput. 4(1), 71–82 (1998)

    Article  MATH  Google Scholar 

  4. Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing 94(2–4), 189–201 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bueno, F., Cabeza, D., Carro, M., Hermenegildo, M., López-Garcıa, P., Puebla, G.: The ciao prolog system. Reference Manual. The Ciao System Documentation Series-TR CLIP3/97.1, School of Computer Science, Technical University of Madrid (UPM), vol. 95, p. 96 (1997)

    Google Scholar 

  6. Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 169–193. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28869-2_9

    Chapter  Google Scholar 

  7. Debray, S.K., García, P.L., Hermenegildo, M., Lin, N.-W.: Estimating the computational cost of logic programs. In: Charlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 255–265. Springer, Heidelberg (1994). doi:10.1007/3-540-58485-4_45

    Chapter  Google Scholar 

  8. Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  9. Destercke, S., Dubois, D.: The role of generalised p-boxes in imprecise probability models. In: 6th International Symposium on Imprecise Probability: Theories and Applications (2009)

    Google Scholar 

  10. Ferson, S.: Model uncertainty in risk analysis. Technical report, Centre de Recherches de Royallieu, Universite de Technologie de Compiegne (2014)

    Google Scholar 

  11. Ferson, S., Kreinovich, V., Ginzburg, L., Myers, D.S., Sentz, K.: Constructing probability boxes and Dempster-Shafer structures. Sand 2002–4015, Sandia National Laboratories (2002)

    Google Scholar 

  12. Flajolet, P., Salvy, B., Zimmermann, P.: Automatic average-case analysis of algorithm. Theor. Comput. Sci. 79(1), 37–109 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  13. Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21455-4_3

    Chapter  Google Scholar 

  14. Gao, A.: Modular average case analysis: Language implementation and extension. Ph.d. thesis, University College Cork (2013)

    Google Scholar 

  15. Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proceedings of the 2012 International Symposium on Software Testing and Analysis, pp. 166–176. ACM (2012)

    Google Scholar 

  16. Gordon, J., Shortliffe, E.H.: The Dempster-Shafer theory of evidence. In: Rule-Based Expert Systems: The MYCIN Experiments of the Stanford Heuristic Programming Project, p. 21 (1984)

    Google Scholar 

  17. Guo, X., Boubekeur, M., McEnery, J., Hickey, D.: ACET based scheduling of soft real-time systems: an approach to optimise resource budgeting. Int. J. Comput. Commun. 1(1), 82–86 (2007)

    Google Scholar 

  18. Kay, R.U.: Fundamentals of the Dempster-Shafer theory and its applications to system safety and reliability modelling. In: RTA, pp. 173–185 (2007)

    Google Scholar 

  19. Kerrison, S., Eder, K.: Energy modelling and optimisation of software for a hardware multi-threaded embedded microprocessor. University of Bristol, Bristol, Technical report (2013)

    Google Scholar 

  20. Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  21. Kwiatkowska, M., Norman, G., Parker, D.: Advances and challenges of probabilistic model checking. In: 48th Annual Allerton Conference on Communication, Control, and Computing, pp. 1691–1698. IEEE, September 2010

    Google Scholar 

  22. Liqat, U., Kerrison, S., Serrano, A., Georgiou, K., Lopez-Garcia, P., Grech, N., Hermenegildo, M.V., Eder, K.: Energy consumption analysis of programs based on XMOS ISA level models. In: Gupta, G., Peña, R. (eds.) LOPSTR 2013. LNCS, vol. 8901, pp. 72–90. Springer, Heidelberg (2013). doi:10.1007/978-3-319-14125-1_5

    Google Scholar 

  23. Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 322–339. Springer, Heidelberg (2000). doi:10.1007/978-3-540-45099-3_17

    Chapter  Google Scholar 

  24. Pierro, A., Hankin, C., Wiklicky, H.: Abstract interpretation for worst and average case analysis. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Program Analysis and Compilation, Theory and Practice. LNCS, vol. 4444, pp. 160–174. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71322-7_8

    Chapter  Google Scholar 

  25. Di Pierro, A., Wiklicky, H., Puppis, G., Villa, T.: Probabilistic data flow analysis: a linear equational approach. In: Proceedings Fourth International Symposium, vol. 119, pp. 150–165. Open Publishing Association (2013)

    Google Scholar 

  26. Soza Pollman, H., Carro, M., Lopez Garcia, P.: Probabilistic cost analysis of logic programs: a first case study. INGENIARE - Revista Chilena de Ingeniera 17(2), 195–204 (2009)

    Google Scholar 

  27. Rosendahl, M.: Automatic program analysis. Master’s thesis, University of Copenhagen (1986)

    Google Scholar 

  28. Rosendahl, M.: Automatic complexity analysis. In: FPCA, pp. 144–156 (1989)

    Google Scholar 

  29. Rosendahl, M., Kirkeby, M.H.: Probabilistic output analysis by program manipulation. In: Quantitative Aspects of Programming Languages, EPTCS (2015)

    Google Scholar 

  30. Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 447–458. ACM, June 2013

    Google Scholar 

  31. Schellekens, M.P.: A Modular Calculus for the Average Cost of Data Structuring. Springer, New York (2008)

    Book  Google Scholar 

  32. Tiwari, V., Malik, S., Wolfe, A.: Power analysis of embedded software a first step towards software power minimization. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 2(4), 437–445 (1994)

    Article  Google Scholar 

  33. Uwimbabazi, A.: Extended probabilistic symbolic execution. Master’s thesis, University of Stellenbosch (2013)

    Google Scholar 

  34. Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)

    Article  Google Scholar 

  35. Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528–539 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  36. Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering, pp. 439–449. IEEE Press (1981)

    Google Scholar 

  37. Wierman, A., Andrew, L.L.H., Tang, A.: Stochastic analysis of power-aware scheduling. In: Proceedings of Allerton Conference on Communication, Control and Computing. Urbana-Champaign, IL (2008)

    Google Scholar 

  38. Wilson, N.: Algorithms for Dempster-Shafer theory. In: Kohlas, J., Moral, S. (eds.) Handbook of Defeasible Reasoning and Uncertainty Management Systems. Handbook of Defeasible Reasoning and Uncertainty Management Systems, vol. 5, pp. 421–475. Springer, Netherlands (2000)

    Chapter  Google Scholar 

  39. Wolfram, S.: The Mathematica Book. Cambridge University Press and Wolfram Research Inc., New York (2000)

    MATH  Google Scholar 

  40. Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280–297. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23702-7_22

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Maja H. Kirkeby .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Kirkeby, M.H., Rosendahl, M. (2016). Probabilistic Resource Analysis by Program Transformation. In: van Eekelen, M., Dal Lago, U. (eds) Foundational and Practical Aspects of Resource Analysis. FOPARA 2015. Lecture Notes in Computer Science(), vol 9964. Springer, Cham. https://doi.org/10.1007/978-3-319-46559-3_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46559-3_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46558-6

  • Online ISBN: 978-3-319-46559-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics