Martin Avanzini
Skip Abstract Section
Skip Supplemental Material SectionAbstract
We present a novel methodology for the automated resource analysis of non-deterministic, probabilistic imperative programs, which gives rise to a modular approach. Program fragments are analysed in full independence. Moreover, the established results allow us to incorporate sampling from dynamic distributions, making our analysis applicable to a wider class of examples, for example the Coupon Collector’s problem.
We have implemented our contributions in the tool , exploiting a constraint-solver over iterative refineable cost functions facilitated by off-the-shelf SMT solvers. We provide ample experimental evidence of the prototype’s algorithmic power. Our experiments show that our tool runs typically at least one order of magnitude faster than comparable tools. On more involved examples, it may even be the case that execution times of seconds become milliseconds. At the same time we retain the precision of existing tools.
The extensions in applicability and the greater efficiency of our prototype, yield scalability of sorts. This effects into a wider class of examples, whose expected cost analysis can be thus be performed fully automatically.
Supplemental Material
- S. Agrawal, K. Chatterjee, and P. Novotný. 2018. Lexicographic Ranking Supermartingales: An Eficient Approach to Termination of Probabilistic Programs. PACMPL 2, POPL ( 2018 ), 34 : 1-34 : 32. https://doi.org/10.1145/3385412.3386002 Google Scholar
Digital Library
- E. Albert, P. Gordillo, A. Rubio, and I. Sergey. 2019. Running on Fumes-Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts Using Static Resource Analysis. In Proc. of 13th VECoS (LNCS, Vol. 11847 ). Springer, 63-78. https: //doi.org/10.1007/978-3-030-35092-5_5 Google ScholarCross Ref
- C. Alias, A. Darte, P. Feautrier, and L. Gonnord. 2010. Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. In Proc. of 17th SAS (LNCS, Vol. 6337 ). Springer, 117-133. https://doi.org/10.1007/978-3-642-15769-1_8 Google ScholarCross Ref
- M. Avanzini, U. Dal Lago, and A. Ghyselen. 2019. Type-Based Complexity Analysis of Probabilistic Functional Programs. In Proc. of 34th LICS. IEEE, 1-13. https://doi.org/10.1109/LICS. 2019.8785725 Google ScholarCross Ref
- M. Avanzini, U. Dal Lago, and A. Yamada. 2020. On Probabilistic Term Rewriting. SCP 185 ( 2020 ), 102338. https: //doi.org/10.1016/j.scico. 2019.102338 Google ScholarCross Ref
- M. Avanzini, G. Moser, and M. Schaper. 2016. TcT: Tyrolean Complexity Tool. In Proc. of 2nd TACAS (LNCS). Springer, 407-423. https://doi.org/10.1007/978-3-662-49674-9_24 Google ScholarDigital Library
- M. Avanzini and A. Yamada. 2020. Weighted Rewriting. Technical Report. NII and INRIA.Google Scholar
- G. Barthe, B. Grégoire, and S. Z. Béguelin. 2009. Formal Certification of Code-based Cryptographic Proofs. In Proc. of 36th POPL. ACM, 90-101. https://doi.org/10.1145/1480881.1480894 Google ScholarDigital Library
- A. Ben-Amram. 2011. Monotonicity Constraints for Termination in the Integer Domain. LMCS 7, 3 ( 2011 ), 1-43. https: //doi.org/10.2168/LMCS-7( 3 :4) 2011 Google ScholarCross Ref
- A. Ben-Amram. 2015. Mortality of Iterated Piecewise Afine Functions over the Integers: Decidability and Complexity. Computability 4, 1 ( 2015 ), 19-56. https://doi.org/10.3233/COM-150032 Google ScholarCross Ref
- A. Ben-Amram and G. Hamilton. 2019. Tight Worst-Case Bounds for Polynomial Loop Programs. In Proc. of 22th FOSSACS (LNCS, Vol. 11425 ). Springer, 80-97. https://doi.org/10.1007/978-3-030-17127-8_5 Google ScholarDigital Library
- A. M. Ben-Amram and L. Kristiansen. 2012. On the Edge of Decidability in Complexity Analysis of Loop Programs. JFCS 23, 7 ( 2012 ), 1451-1464. https://doi.org/10.1142/S0129054112400588 Google ScholarCross Ref
- O. Bournez and F. Garnier. 2005. Proving Positive Almost-Sure Termination. In Proc. of 16th RTA (LNCS, Vol. 3467 ). Springer, 323-337. https://doi.org/10.1142/S0129054112400588 Google ScholarCross Ref
- T. Brázdil, S. Kiefer, A. Kucera, and I.H. Vareková. 2015. Runtime Analysis of Probabilistic Programs with Unbounded Recursion. JCSS 81, 1 ( 2015 ), 288-310. https://doi.org/10.1016/j.jcss. 2014. 06.005 Google ScholarDigital Library
- F. Breuvart and U. Dal Lago. 2018. On Intersection Types and Probabilistic Lambda Calculi. In Proc. of 20th PPDP. ACM, 8 : 1-8 : 13. https://doi.org/10.1145/3236950.3236968 Google ScholarDigital Library
- M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. 2014. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Proc. of 20th TACAS (LNCS, Vol. 8413 ). Springer, 140-155. https://doi.org/10.1007/978-3-642-54862-8_10 Google ScholarCross Ref
- M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. 2016. Analyzing Runtime and Size Complexity of Integer Programs. TOPLAS 38, 4 ( 2016 ), 13 : 1-13 : 50. https://doi.org/10.1145/2866575 Google ScholarDigital Library
- Q. Carbonneaux, J. Hofmann, and Z. Shao. 2015. Compositional Certified Resource Bounds. In Proc. of 36th PLDI. ACM, 467-478. https://doi.org/10.1145/2813885.2737955 Google ScholarDigital Library
- O. Celiku and A. McIver. 2005. Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs. In Proc. of FM 2005 (LNCS, Vol. 3582 ). Springer, 107-122. https://doi.org/10.1007/11526841_9 Google ScholarDigital Library
- A. Chakarov and S. Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Proc. of 25th CAV (LNCS, Vol. 8044 ). Springer, 511-526. https://doi.org/10.1007/978-3-642-39799-8_34 Google ScholarCross Ref
- A. Chakarov and S. Sankaranarayanan. 2014. Expectation Invariants for Probabilistic Program Loops as Fixed Points. In Proc. of 21th SAS (LNCS). Springer, 85-100. https://doi.org/10.1007/978-3-319-10936-7_6 Google ScholarCross Ref
- K. Chatterjee, H. Fu, and A. K. Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz's. In Proc. of 28th CAV (LNCS, Vol. 9779 ). Springer, 3-22. https://doi.org/10.1007/978-3-319-41528-4_1 Google ScholarCross Ref
- K. Chatterjee, H. Fu, and A. Murhekar. 2017a. Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds. In Proc. of 29th CAV (LNCS, Vol. 10426 ). Springer, 118-139. https://doi.org/10.1007/978-3-319-63387-9_6 Google ScholarCross Ref
- K. Chatterjee, P. Novotný, and D. Zikelic. 2017b. Stochastic Invariants for Probabilistic Termination. In Proc. of 44th POPL. ACM, 145-160. https://doi.org/10.1145/3093333.3009873 Google ScholarDigital Library
- J. Cohen and C. Zuckerman. 1974. Two Languages for Estimating Program Eficiency. Comm. ACM 17, 6 ( 1974 ), 301-308. https://doi.org/10.1145/355616.361015 Google ScholarDigital Library
- E. Contejean, C. Marché, A.-P. Tomás, and X. Urbain. 2005. Mechanically Proving Termination Using Polynomial Interpretations. JAR 34, 4 ( 2005 ), 325-363. https://doi.org/10.1007/s10817-005-9022-x Google ScholarDigital Library
- P. Cousot and R. Cousot. 2002. Modular Static Program Analysis. In Proc. of 11th CC (LNCS, Vol. 2304 ). Springer, 159-178. https://doi.org/10.1007/3-540-45937-5_13 Google ScholarCross Ref
- J. Dean and S. Ghemawat. 2008. MapReduce: Simplified Data Processing on Large Clusters. Commun. ACM 51, 1 ( 2008 ), 107-113. https://doi.org/10.1145/1327452.1327492 Google ScholarDigital Library
- T. Dillig. 2011. A Modular and Symbolic Approach to Static Program Analysis. Ph.D. Dissertation. Stanford University.Google Scholar
- J. Esparza, A. Kucera, and R. Mayr. 2005. Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances. In Proc. of 20th LICS. IEEE, 117-126. https://doi.org/10.1109/LICS. 2005.39 Google ScholarDigital Library
- T. Fiedor, L. Holík, A. Rogalewicz, M. Sinn, T. Vojnar, and F. Zuleger. 2018. From Shapes to Amortized Complexity. In Proc. of 19th VMCAI (LNCS, Vol. 10747 ). Springer, 205-225. https://doi.org/10.1007/978-3-319-73721-8_10 Google ScholarCross Ref
- F. Frohn and J. Giesl. 2017. Complexity Analysis for Java with AProVE. In Proc. of the 13th IFM (LNCS, Vol. 10510 ). Springer, 85-101. https://doi.org/10.1007/978-3-319-66845-1_6 Google ScholarCross Ref
- C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl. 2007. SAT Solving for Termination Analysis with Polynomial Interpretations. In Proc. of 10th SAT (LNCS, Vol. 4501 ). Springer, 340-354. https://doi.org/10.1007/978-3-540-72788-0_33 Google ScholarCross Ref
- T. Gehr, S. Misailovic, and M. Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In Proc. of 28th CAV (LNCS, Vol. 9779 ). Springer, 62-83. https://doi.org/10.1007/978-3-319-41528-4_4 Google ScholarCross Ref
- S. Gulwani, K.K. Mehra, and T.M. Chilimbi. 2009. SPEED: Precise and Eficient Static Estimation of Program Computational Complexity. In Proc. of 36th POPL. ACM, 127-139. https://doi.org/10.1145/1594834.1480898 Google ScholarDigital Library
- S. Gulwani and A. Tiwari. 2006. Combining Abstract Interpreters. In Proc. of PLDI'06. ACM, 376-386. https://doi.org/10. 1145/1133981.1134026 Google ScholarDigital Library
- S. Gulwani and F. Zuleger. 2010. The Reachability-Bound Problem. In Proc. of PLDI'10. ACM, 292-304. https://doi.org/10. 1145/1809028.1806630 Google ScholarDigital Library
- D. Handelman. 1988. Representing Polynomials by Positive Linear Functions on Compact Convex Polyhedra. PJM 132, 1 ( 1988 ), 35-62. https://doi.org/10.2140/pjm. 1988. 132.35 Google ScholarCross Ref
- M. D. Hill and M.R. Marty. 2008. Amdahl's Law in the Multicore Era. Computer 41, 7 ( 2008 ), 33-38. https://doi.org/10.1109/ MC. 2008.209 Google ScholarDigital Library
- N. Hirokawa and G. Moser. 2008. Automated Complexity Analysis Based on the Dependency Pair Method. In Proc. of 4th IJCAR (LNAI, Vol. 5195 ). Springer, 364-380. https://doi.org/10.1007/978-3-540-71070-7_32 Google ScholarDigital Library
- J. Hofmann, A. Das, and S.-C. Weng. 2017. Towards Automatic Resource Bound Analysis for OCaml. In Proc. of 44th POPL. ACM, 359-373. https://doi.org/10.1145/3009837.3009842 Google ScholarDigital Library
- N. D. Jones and L. Kristiansen. 2009. A Flow Calculus of mwp-Bounds for Complexity Analysis. TOCL 10, 4 ( 2009 ), 28 : 1-28 : 41. https://doi.org/10.1145/1555746.1555752 Google ScholarDigital Library
- B. L. Kaminski and J.-P. Katoen. 2017. A Weakest Pre-expectation Semantics for Mixed-sign Expectations. In Proc. of 32nd LICS. IEEE, 1-12. https://doi.org/10.1109/LICS. 2017.8005153 Google ScholarCross Ref
- B. Lucien Kaminski, J.-P. Katoen, C. Matheja, and F. Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In Proc. of 25th ESOP (LNCS, Vol. 9632 ). Springer, 364-389. https://doi.org/10.1007/978-3-662-49498-1_15 Google ScholarDigital Library
- B. L. Kaminski, J.-P. Katoen, C. Matheja, and F. Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. JACM 65, 5 ( 2018 ), 30 : 1-30 : 68. https://doi.org/10.1145/3208102 Google ScholarDigital Library
- B. L. Kaminski and J.-P. Katoen. 2015. On the Hardness of Almost-Sure Termination. In MFCS 2015, Part I (LNCS ). Springer, 307-318. https://doi.org/10.1007/978-3-662-48057-1_24 Google ScholarCross Ref
- J.-P. Katoen. 2016. The Probabilistic Model Checking Landscape. In Proc. of 31nd LICS. ACM, 31-45. https://doi.org/10.1145/ 2933575.2934574 Google ScholarDigital Library
- J.-P. Katoen, A. McIver, L. Meinicke, and C.C. Morgan. 2010. Linear-Invariant Generation for Probabilistic Programs:-Automated Support for Proof-Based Methods. In Proc. of 17th SAS (LNCS, Vol. 6337 ). Springer, 390-406. https://doi.org/ 10.1007/978-3-642-15769-1_24 Google ScholarCross Ref
- C. Kim and A. K. Agrawala. 1989. Analysis of the Fork-join Queue. IEEE TC 38, 2 ( 1989 ), 250-255. https://doi.org/10.1109/ 12.16501 Google ScholarDigital Library
- D. Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22, 3 ( 1981 ), 328-350.Google ScholarCross Ref
- D. Kozen. 1985. A Probabilistic PDL. JCSC 30, 2 ( 1985 ), 162-178. https://doi.org/10.1016/ 0022-0000 ( 85 ) 90012-1 Google ScholarCross Ref
- A. Levitin. 2007. The Design and Analysis of Algorithms. Pearson.Google Scholar
- A. McIver, C. Morgan, B. L. Kaminski, and J-P Katoen. 2018. A New Proof Rule for Almost-sure Termination. PACMPL 2, POPL ( 2018 ), 33 : 1-33 : 28. https://doi.org/10.1145/3158121 Google ScholarDigital Library
- D. A. Menascé. 2004. Response-Time Analysis of Composite Web Services. IEEE IC 8, 1 ( 2004 ), 90-92. https://doi.org/10. 1109/MIC. 2004.1260710 Google ScholarDigital Library
- M. Mitzenmacher and E. Upfal. 2005. Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press.Google Scholar
- D. Monniaux. 2001. An Abstract Analysis of the Probabilistic Termination of Programs. In Proc. of 8th SAS (LNCS, Vol. 2126 ). Springer, 111-126. https://doi.org/10.1007/3-540-47764-0_7 Google ScholarCross Ref
- G. Moser and M. Schaper. 2018. From Jinja Bytecode to Term Rewriting: A Complexity Reflecting Transformation. IC 261, Part ( 2018 ), 116-143. https://doi.org/10.1016/j.ic. 2018. 05.007 Google ScholarCross Ref
- N. C. Ngo, Q. Carbonneaux, and J. Hofmann. 2018. Bounded Expectations: Resource Analysis for Probabilistic Programs. In Proc. of 39th PLDI. ACM, 496-512. https://doi.org/10.1145/3296979.3192394 Google ScholarDigital Library
- V. Chan Ngo, M. Dehesa-Azuara, M. Fredrikson, and J. Hofmann. 2017. Verifying and Synthesizing Constant-Resource Implementations with Types. In Proc. of 38th S&P. 710-728.Google Scholar
- F. Olmedo, B. L. Kaminski, J.-P. Katoen, and C. Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In Proc. of 31nd LICS. ACM, 672-681. https://doi.org/10.1145/2933575.2935317 Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. 2004. A Complete Method for the Synthesis of Linear Ranking Functions. In Proc. of 5th VMCAI (LNCS, Vol. 2937 ). Springer, 239-251. https://doi.org/10.1007/978-3-540-24622-0_20 Google ScholarCross Ref
- R. Sedgewick and P. Flajolet. 1996. An Introduction to the Analysis of Algorithms. Addison-Wesley-Longman. https: //doi.org/10.1142/10875 Google ScholarCross Ref
- M. Sinn, F. Zuleger, and H. Veith. 2016. A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. In Proc. of 26th CAV (LNCS, Vol. 8559 ). Springer, 745-761. https://doi.org/10.1007/978-3-319-08867-9_50 Google ScholarDigital Library
- M. Sinn, F. Zuleger, and H. Veith. 2017. Complexity and Resource Bound Analysis of Imperative Programs Using Diference Constraints. JAR 59, 1 ( 2017 ), 3-45. https://doi.org/10.1007/s10817-016-9402-4 Google ScholarDigital Library
- T. Takisaka, Y. Oyabu, N. Urabe, and I. Hasuo. 2018. Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs. In Proc. of 16th ATVA (LNCS, Vol. 11138 ). Springer, 476-493. https://doi.org/10.1007/978-3-030-01090-4_28 Google ScholarCross Ref
- D. Wang, J. Hofmann, and T. W. Reps. 2018. PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs. In Proc. of 39th PLDI. ACM, 513-528. https://doi.org/10.1145/3192366.3192408 Google ScholarDigital Library
- P. Wang, H. Fu, A. K. Goharshady, K. Chatterjee, X. Qin, and W. Shi. 2019. Cost Analysis of Nondeterministic Probabilistic Programs. In Proc. of 40th PLDI. ACM, 204-220. https://doi.org/10.1145/3314221.3314581 Google ScholarDigital Library
- B. Wegbreit. 1975. Mechanical Program Analysis. Comm. ACM 18, 9 ( 1975 ), 528-539. https://doi.org/10.1145/361002.361016 Google ScholarDigital Library
- B. Wegbreit. 1976. Verifying Program Performance. JACM 23, 4 ( 1976 ), 691-699. https://doi.org/10.1145/321978.321987 Google ScholarDigital Library
- R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenstrom. 2008. The Worst Case Execution Time Problem-Overview of Methods and Survey of Tools. TECS 7, 3 ( 2008 ), 1-53. https://doi.org/10.1145/1347375.1347389 Google ScholarDigital Library
- R. Wilhelm and D. Grund. 2014. Computation Takes Time, But How Much? Comm. ACM 57, 2 ( 2014 ), 94-103. https: //doi.org/10.1145/2500886 Google ScholarDigital Library
- G. Winskel. 1993. The Formal Semantics of Programming Languages. MIT Press. https://doi.org/10.7551/mitpress/3054.003. 0004 Google ScholarCross Ref
Index Terms
- A modular cost analysis for probabilistic programs
Recommendations
Cost analysis of nondeterministic probabilistic programs
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe consider the problem of expected cost analysis over nondeterministic probabilistic programs, which aims at automated methods for analyzing the resource-usage of such programs. Previous approaches for this problem could only handle nonnegative bounded ...
Newtonian Program Analysis of Probabilistic Programs
Due to their quantitative nature, probabilistic programs pose non-trivial challenges for designing compositional and efficient program analyses. Many analyses for probabilistic programs rely on iterative approximation. This article presents an ...
Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
POPL '16In this paper, we consider termination of probabilistic programs with real-valued variables. The questions concerned are: 1. qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the ...
Comments