Abstract
We study the problem of automatically analyzing the worst-case resource usage of procedures with several arguments. Existing automatic analyses based on amortization or sized types bound the resource usage or result size of such a procedure by a sum of unary functions of the sizes of the arguments.
In this article we generalize this to arbitrary multivariate polynomial functions thus allowing bounds of the form mn which had to be grossly overestimated by m2 + n2 before. Our framework even encompasses bounds like ∑i,j≤ n mi mj where the mi are the sizes of the entries of a list of length n.
This allows us for the first time to derive useful resource bounds for operations on matrices that are represented as lists of lists and to considerably improve bounds on other superlinear operations on lists such as longest common subsequence and removal of duplicates from lists of lists. Furthermore, resource bounds are now closed under composition which improves accuracy of the analysis of composed programs when some or all of the components exhibit superlinear resource or size behavior.
The analysis is based on a novel multivariate amortized resource analysis. We present it in form of a type system for a simple first-order functional language with lists and trees, prove soundness, and describe automatic type inference based on linear programming.
We have experimentally validated the automatic analysis on a wide range of examples from functional programming with lists and trees. The obtained bounds were compared with actual resource consumption. All bounds were asymptotically tight, and the constants were close or even identical to the optimal ones.
- Albert, E., Alonso, D., Arenas, P., Genaim, S., and Puebla, G. 2009a. Asymptotic resource usage bounds. In Proceedings of the 7th Asian Symposium Programming Languages and Systems (APLAS'09). Springer, 294--310. Google ScholarDigital Library
- Albert, E., Arenas, P., Genaim, S., Gómez-Zamalloa, M., Puebla, G., Ramírez, D., Román, G., and Zanardini, D. 2009b. Termination and cost analysis with COSTA and its user interfaces. Electr. Notes Theor. Comput. Sci. 258, 1, 109--121. Google ScholarDigital Library
- Albert, E., Arenas, P., Genaim, S., and Puebla, G. 2008. Automatic inference of upper bounds for recurrence relations in cost analysis. In Proceedings of the 15th International Symposium on Static Analysis (SAS'08). Springer, 221--237. Google ScholarDigital Library
- Albert, E., Arenas, P., Genaim, S., and Puebla, G. 2011a. Closed-form upper bounds in static cost analysis. J. Autom. Reason. 46, 2, 161--203. Google ScholarDigital Library
- Albert, E., Arenas, P., Genaim, S., Puebla, G., and Zanardini, D. 2007. Cost analysis of java bytecode. In Proceedings of the 16th European Symposium on Programming Languages and Systems (ESOP'07). Springer, 157--172. Google ScholarDigital Library
- Albert, E., Genaim, S., and Gómez-Zamalloa, M. 2010. Parametric inference of memory requirements for garbage collected languages. In Proceedings of the 9th International Symposium on Memory Management (ISMM'10). ACM, New York, 121--130. Google ScholarDigital Library
- Albert, E., Genaim, S., and Masud, A. N. 2011b. More precise yet widely applicable cost analysis. In Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'11). Springer, 38--53. Google ScholarDigital Library
- Althaus, E., Altmeyer, S., and Naujoks, R. 2011. Precise and efficient parametric path analysis. In Proceedings of the Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES'11). ACM, New York, 141--150. Google ScholarDigital Library
- Altmeyer, S., Humbert, C., Lisper, B., and Wilhelm, R. 2008. Parametric timing analysis for complex architectures. In Proceedings of the 4th IEEE Internationl Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA'08). IEEE, 367--376. Google ScholarDigital Library
- Atkey, R. 2010. Amortised resource analysis with separation logic. In Proceedings of the 19th European Symposium on Programming Languages and Systems (ESOP'10). Springer, 85--103. Google ScholarDigital Library
- Benzinger, R. 2001. Automated complexity analysis of nuprl extracted programs. J. Funct. Program. 11, 1, 3--31. Google ScholarDigital Library
- Benzinger, R. 2004. Automated higher-order complexity analysis. Theor. Comput. Sci. 318, 1-2, 79--103. Google ScholarDigital Library
- Beringer, L., Hofmann, M., Momigliano, A., and Shkaravska, O. 2004. Automatic certification of heap consumption. In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'04). Springer, 347--362.Google Scholar
- Braberman, V. A., Fernández, F. J., Garbervetsky, D., and Yovine, S. 2008. Parametric prediction of heap memory requirements. In Proceedings of the 7th International Symposium on Memory Management (ISMM'08). ACM, New York, 141--150. Google ScholarDigital Library
- Bygde, S., Ermedahl, A., and Lisper, B. 2009. An efficient algorithm for parametric WCET calculation. In Proceedings of the 15th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA'09). IEEE, Los Alamitos, CA, 13--21. Google ScholarDigital Library
- Campbell, B. 2009. Amortised memory analysis using the depth of data structures. In Proceedings of the 18th European Symposium on Programming Languages and Systems (ESOP'09). Springer, 190--204. Google ScholarDigital Library
- Chin, W.-N. and Khoo, S.-C. 2001. Calculating sized types. High.-Ord. Symb. Comp. 14, 2-3, 261--300. Google ScholarDigital Library
- Chin, W.-N., Nguyen, H. H., Popeea, C., and Qin, S. 2008. Analysing memory resource bounds for low-level programs. In Proceedings of the 7th International Symposium on Memory Management (ISMM'08). ACM, New York, 151--160. Google ScholarDigital Library
- Clauss, P., Fernández, F. J., Garbervetsky, D., and Verdoolaege, S. 2009. Symbolic polynomial maximization over convex sets and its application to memory requirement estimation. IEEE Trans. VLSI Syst. 17, 8, 983--996. Google ScholarDigital Library
- Cook, B., Gupta, A., Magill, S., Rybalchenko, A., Simsa, J., Singh, S., and Vafeiadis, V. 2009. Finding heap-bounds for hardware synthesis. In Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD'09). IEEE, Los Alamitos, CA, 205--212.Google Scholar
- Cousot, P. and Cousot, R. 1992. Inductive definitions, semantics and abstract interpretations. In Proceedings of the 19th ACM Symposium on Principles of Programming Languages (POPL'92). ACM, New York, 83--94. Google ScholarDigital Library
- Crary, K. and Weirich, S. 2000. Resource bound certification. In Proceedings of the 27th ACM Symposium on Principles of Programming Languages (POPL'00). ACM, New York, 184--198. Google ScholarDigital Library
- Danielsson, N. A. 2008. Lightweight semiformal time complexity analysis for purely functional data structures. In Proceedings of the 35th ACM Symposium on Principles of Programming Languages (POPL'08). ACM, New York, 133--144. Google ScholarDigital Library
- Debray, S. K. and Lin, N.-W. 1993. Cost analysis of logic programs. ACM Trans. Program. Lang. Syst. 15, 5, 826--875. Google ScholarDigital Library
- Flajolet, P., Salvy, B., and Zimmermann, P. 1991. Automatic average-case analysis of algorithms. Theoret. Comput. Sci. 79, 1, 37--109. Google ScholarDigital Library
- Grobauer, B. 2001. Cost recurrences for DML programs. In Proceedings of the 6th International Conference on Functional Programming (ICFP'01). ACM, New York, 253--264. Google ScholarDigital Library
- Gulavani, B. S. and Gulwani, S. 2008. A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In Proceedings of the 20th International Conference Computer Aided Verification (CAV'08). Springer, 370--384. Google ScholarDigital Library
- Gulwani, S., Jain, S., and Koskinen, E. 2009a. Control-flow refinement and progress invariants for bound analysis. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI'09). ACM, New York, 375--385. Google ScholarDigital Library
- Gulwani, S., Mehra, K. K., and Chilimbi, T. M. 2009b. SPEED: Precise and efficient static estimation of program computational complexity. In Proceedings of the 36th ACM Symposium on Principles of Programming Languages (POPL'09). ACM, New York, 127--139. Google ScholarDigital Library
- Gulwani, S. and Zuleger, F. 2010. The reachability-bound problem. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI'10). ACM, New York, 292--304. Google ScholarDigital Library
- Hammond, K. and Michaelson, G. 2003. Hume: A domain-specific language for real-time embedded systems. In Proceedings of the International Conference on Generative Programming and Component Engineering (GPCE'03). Springer, 37--56. Google ScholarDigital Library
- Hickey, T. J. and Cohen, J. 1988. Automating program analysis. J. ACM 35, 1, 185--220. Google ScholarDigital Library
- Hoffmann, J. 2011. Types with potential: Polynomial resource bounds via automatic amortized analysis. Ph.D. thesis, Ludwig-Maximilians-Universiät, München, Germany.Google Scholar
- Hoffmann, J., Aehlig, K., and Hofmann, M. 2011. Multivariate amortized resource analysis. In Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL'11). ACM, New York, 357--370. Google ScholarDigital Library
- Hoffmann, J. and Hofmann, M. 2010a. Amortized resource analysis with polymorphic recursion and partial big-step operational semantics. In Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS'10). Springer, 172--187. Google ScholarDigital Library
- Hoffmann, J. and Hofmann, M. 2010b. Amortized resource analysis with polynomial potential. In Proceedings of the 19th European Symposium on Programming Languages and Systems (ESOP'10). ACM, New York, 287--306. Google ScholarDigital Library
- Hofmann, M. 2000. A type system for bounded space and functional in-place update--extended abstract. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP'00). Springer, 165--179. Google ScholarDigital Library
- Hofmann, M. and Jost, S. 2003. Static prediction of heap space usage for first-order functional programs. In Proceedings of the 30th ACM Symposium on Principles of Programming Languages (POPL'03). ACM, New York, 185--197. Google ScholarDigital Library
- Hofmann, M. and Jost, S. 2006. Type-based amortised heap-space analysis. In Proceedings of the 15th European Symposium on Programming Languages and Systems (ESOP'06). Springer, 22--37. Google ScholarDigital Library
- Hofmann, M. and Rodriguez, D. 2009. Efficient type-checking for amortised heap-space analysis. In Proceedings of the 18th Conference on Computer Science Logic (CSL'09). Springer, 317--331. Google ScholarDigital Library
- Hughes, J. and Pareto, L. 1999. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In Proceedings of the 4th International Conference on Functional Programming (ICFP'99). ACM, New York, 70--81. Google ScholarDigital Library
- Hughes, J., Pareto, L., and Sabry, A. 1996. Proving the correctness of reactive systems using sized types. In Proceedings of the 23rd ACM Symposium on Principles of Programming Languages (POPL'96). ACM, New York, 410--423. Google ScholarDigital Library
- Jost, S., Hammond, K., Loidl, H.-W., and Hofmann, M. 2010. Static determination of quantitative resource usage for higher-order programs. In Proceedings of the 37th ACM Symposium on Principles of Programming Languages (POPL'10). ACM, New York, 223--236. Google ScholarDigital Library
- Jost, S., Loidl, H.-W., Hammond, K., Scaife, N., and Hofmann, M. 2009. Carbon credits for resource-bounded computations using amortised analysis. In Proceedings of the 16th International Symposium on Formal Methods (FM'09). Springer, 354--369. Google ScholarDigital Library
- Leroy, X. 2006. Coinductive big-step operational semantics. In Proceedings of the 15th European Symposium on Programming Languages and Systems (ESOP'06). Springer, 54--68. Google ScholarDigital Library
- Lisper, B. 2003. Fully automatic, parametric worst-case execution time analysis. In Proceedings of the 3rd International Workshop on Worst-Case Execution Time Analysis (WCET'03). 99--102.Google Scholar
- Métayer, D. L. 1988. ACE: An automatic complexity evaluator. ACM Trans. Program. Lang. Syst. 10, 2, 248--266. Google ScholarDigital Library
- Pierce, B. C. 2004. Advanced Topics in Types and Programming Languages. The MIT Press, Cambridge, MA. Google ScholarDigital Library
- Ramshaw, L. H. 1979. Formalizing the analysis of algorithms. Ph.D. thesis, Stanford University, Stanford, CA, USA. Google ScholarDigital Library
- Rosendahl, M. 1989. Automatic complexity analysis. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA'89). ACM, New York, 144--156. Google ScholarDigital Library
- Shkaravska, O., van Kesteren, R., and van Eekelen, M. C. 2007. Polynomial size analysis of first-order functions. In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA'07). Springer, 351--365. Google ScholarDigital Library
- Stanley, R. P. 2001. Enumerative Combinatorics Vol. 2. Cambridge University Press, New York, USA.Google Scholar
- Taha, W., Ellner, S., and Xi, H. 2003. Generating heap-bounded programs in a functional setting. In Proceedings of the 3rd International Conference on Embedded Software (EMSOFT'03). Springer, 340--355.Google Scholar
- Tarjan, R. E. 1985. Amortized computational complexity. SIAM J. Algebr. Discr. Methods 6, 2, 306--318.Google ScholarCross Ref
- Vasconcelos, P. 2008. Space cost analysis using sized types. Ph.D. thesis, School of Computer Science, University of St Andrews, St Andrews, UK.Google Scholar
- Wegbreit, B. 1975. Mechanical program analysis. Commun. ACM 18, 9, 528--539. Google ScholarDigital Library
- Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D. B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P. P., Staschulat, J., and Stenström, P. 2008. The worst-case execution-time problem -- Overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst. 7, 3, 36:1--36:53. Google ScholarDigital Library
Index Terms
- Multivariate amortized resource analysis
Recommendations
Towards automatic resource bound analysis for OCaml
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesThis article presents a resource analysis system for OCaml programs. The system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-defined inductive types. The technique is parametric in the resource and ...
Multivariate amortized resource analysis
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe study the problem of automatically analyzing the worst-case resource usage of procedures with several arguments. Existing automatic analyses based on amortization, or sized types bound the resource usage or result size of such a procedure by a sum of ...
Multivariate amortized resource analysis
POPL '11We study the problem of automatically analyzing the worst-case resource usage of procedures with several arguments. Existing automatic analyses based on amortization, or sized types bound the resource usage or result size of such a procedure by a sum of ...
Comments