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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
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
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)
Berleant, D., Cheng, H.: A software tool for automatically verified operations on intervals and probability distributions. Reliable Comput. 4(1), 71–82 (1998)
Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing 94(2–4), 189–201 (2012)
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)
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
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
Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)
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)
Ferson, S.: Model uncertainty in risk analysis. Technical report, Centre de Recherches de Royallieu, Universite de Technologie de Compiegne (2014)
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)
Flajolet, P., Salvy, B., Zimmermann, P.: Automatic average-case analysis of algorithm. Theor. Comput. Sci. 79(1), 37–109 (1991)
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
Gao, A.: Modular average case analysis: Language implementation and extension. Ph.d. thesis, University College Cork (2013)
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)
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)
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)
Kay, R.U.: Fundamentals of the Dempster-Shafer theory and its applications to system safety and reliability modelling. In: RTA, pp. 173–185 (2007)
Kerrison, S., Eder, K.: Energy modelling and optimisation of software for a hardware multi-threaded embedded microprocessor. University of Bristol, Bristol, Technical report (2013)
Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981)
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
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
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
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
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)
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)
Rosendahl, M.: Automatic program analysis. Master’s thesis, University of Copenhagen (1986)
Rosendahl, M.: Automatic complexity analysis. In: FPCA, pp. 144–156 (1989)
Rosendahl, M., Kirkeby, M.H.: Probabilistic output analysis by program manipulation. In: Quantitative Aspects of Programming Languages, EPTCS (2015)
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
Schellekens, M.P.: A Modular Calculus for the Average Cost of Data Structuring. Springer, New York (2008)
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)
Uwimbabazi, A.: Extended probabilistic symbolic execution. Master’s thesis, University of Stellenbosch (2013)
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)
Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528–539 (1975)
Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering, pp. 439–449. IEEE Press (1981)
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)
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)
Wolfram, S.: The Mathematica Book. Cambridge University Press and Wolfram Research Inc., New York (2000)
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)