ATLAS: automated amortised complexity analysis of self-adjusting data structures. (English) Zbl 1493.68129
Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12760, 99-122 (2021).
Summary: Being able to argue about the performance of self-adjusting data structures such as splay trees has been a main objective, when Sleator and Tarjan introduced the notion of amortised complexity.
Analysing these data structures requires sophisticated potential functions, which typically contain logarithmic expressions. Possibly for these reasons, and despite the recent progress in automated resource analysis, they have so far eluded automation. In this paper, we report on the first fully-automated amortised complexity analysis of self-adjusting data structures. Following earlier work, our analysis is based on potential function templates with unknown coefficients.
We make the following contributions: 1) We encode the search for concrete potential function coefficients as an optimisation problem over a suitable constraint system. Our target function steers the search towards coefficients that minimise the inferred amortised complexity. 2) Automation is achieved by using a linear constraint system in conjunction with suitable lemmata schemes that encapsulate the required non-linear facts about the logarithm. We discuss our choices that achieve a scalable analysis. 3) We present our tool \(\mathsf{ATLAS}\) and report on experimental results for splay trees, splay heaps and pairing heaps. We completely automatically infer complexity estimates that match previous results (obtained by sophisticated pen-and-paper proofs), and in some cases even infer better complexity estimates than previously published.
For the entire collection see [Zbl 1482.68040].
Analysing these data structures requires sophisticated potential functions, which typically contain logarithmic expressions. Possibly for these reasons, and despite the recent progress in automated resource analysis, they have so far eluded automation. In this paper, we report on the first fully-automated amortised complexity analysis of self-adjusting data structures. Following earlier work, our analysis is based on potential function templates with unknown coefficients.
We make the following contributions: 1) We encode the search for concrete potential function coefficients as an optimisation problem over a suitable constraint system. Our target function steers the search towards coefficients that minimise the inferred amortised complexity. 2) Automation is achieved by using a linear constraint system in conjunction with suitable lemmata schemes that encapsulate the required non-linear facts about the logarithm. We discuss our choices that achieve a scalable analysis. 3) We present our tool \(\mathsf{ATLAS}\) and report on experimental results for splay trees, splay heaps and pairing heaps. We completely automatically infer complexity estimates that match previous results (obtained by sophisticated pen-and-paper proofs), and in some cases even infer better complexity estimates than previously published.
For the entire collection see [Zbl 1482.68040].
Keywords:
amortised cost analysis; functional programming; self-adjusting data structures; automation; constraint solvingReferences:
| [1] | Albert, E.; Arenas, P.; Genaim, S.; Puebla, G., Closed-form upper bounds in static cost analysis, JAR, 46, 2, 161-203 (2011) · Zbl 1213.68200 · doi:10.1007/s10817-010-9174-1 |
| [2] | Alonso-Blas, D.E., Genaim, S.: On the limits of the classical approach to cost analysis. In: SAS, pp. 405-421 (2012) |
| [3] | Avanzini, M., Lago, U.D., Moser, G.: Analysing the complexity of functional programs: higher-order meets first-order. In: ICFP, pp. 152-164. ACM (2015) · Zbl 1360.68313 |
| [4] | Avanzini, M.; Moser, G., A combination framework for complexity, IC, 248, 22-55 (2016) · Zbl 1339.68135 |
| [5] | Avanzini, M.; Moser, G.; Schaper, M.; Chechik, M.; Raskin, J-F, TcT: Tyrolean complexity tool, Tools and Algorithms for the Construction and Analysis of Systems, 407-423 (2016), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-662-49674-9_24 |
| [6] | Bauer, S., Jost, S., Hofmann, M.: Decidable inequalities over infinite trees. In: LPAR, vol. 57, pp. 111-130 (2018) · Zbl 1415.68059 |
| [7] | Brázdil, T., Chatterjee, K., Kucera, A., Novotný, P., Velan, D., Zuleger, F.: Efficient algorithms for asymptotic bounds on termination time in VASS. In: LICS, pp. 185-194 (2018) · Zbl 1497.68328 |
| [8] | Chatterjee, K., Fu, H., Goharshady, A.K.: Non-polynomial worst-case analysis of recursive programs. In: CAV, pp. 41-63 (2017) · Zbl 1494.68053 |
| [9] | Colcombet, T., Daviaud, L., Zuleger, F.: Size-change abstraction and max-plus automata. In: MFCS, pp. 208-219 (2014) · Zbl 1425.68190 |
| [10] | Fiedor, T., Holík, L., Rogalewicz, A., Sinn, M., Vojnar, T., Zuleger, F.: From shapes to amortized complexity. In: VMCAI, pp. 205-225 (2018) · Zbl 1446.68030 |
| [11] | Flores-Montoya, A.: Cost analysis of programs based on the refinement of cost relations. Ph.D. thesis, Darmstadt University of Technology, Germany (2017) |
| [12] | Fuhs, C., Kop, C., Nishida, N.: Verifying procedural programs via constrained rewriting induction. TOCL 18(2), 14:1-14:50 (2017) · Zbl 1367.68248 |
| [13] | Gambin, A., Malinowski, A.: Randomized meldable priority queues. In: SOFSEM, pp. 344-349 (1998) |
| [14] | Giesl, J., Analyzing program termination and complexity automatically with AProVE, JAR, 1, 3-31 (2017) · Zbl 1409.68255 · doi:10.1007/s10817-016-9388-y |
| [15] | Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI, pp. 292-304 (2010) |
| [16] | Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: TPHOLs, pp. 102-118 (2007) · Zbl 1144.68357 |
| [17] | Hermenegildo, M., An overview of ciao and its design philosophy, TPLP, 12, 1-2, 219-252 (2012) · Zbl 1244.68019 |
| [18] | Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: IJCAR, pp. 364-380 (2008) · Zbl 1165.68390 |
| [19] | Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: Proceedings of 38th POPL, pp. 357-370. ACM (2011) · Zbl 1284.68132 |
| [20] | Hoffmann, J.; Aehlig, K.; Hofmann, M., Multivariate amortized resource analysis, TOPLAS, 34, 3, 14 (2012) · doi:10.1145/2362389.2362393 |
| [21] | Hoffmann, J.; Aehlig, K.; Hofmann, M.; Madhusudan, P.; Seshia, SA, Resource aware ML, Computer Aided Verification, 781-786 (2012), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-31424-7_64 |
| [22] | Hoffmann, J., Das, A., Weng, S.C.: Towards automatic resource bound analysis for OCaml. In: POPL, pp. 359-373 (2017) · Zbl 1380.68123 |
| [23] | Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: POPL, pp. 185-197 (2003) · Zbl 1321.68180 |
| [24] | Hofmann, M., Moser, G.: Amortised resource analysis and typed polynomial interpretations. In: Proceedings of Joint 25th RTA and 12th TLCA, pp. 272-286 (2014) · Zbl 1416.68093 |
| [25] | Hofmann, M., Moser, G.: Multivariate amortised resource analysis for term rewrite systems. In: TLCA, pp. 241-256 (2015) · Zbl 1367.68138 |
| [26] | Hofmann, M., Moser, G.: Analysis of logarithmic amortised complexity (2018) |
| [27] | Hofmann, M., Leutgeb, L., Moser, G., Obwaller, D., Zuleger, F.: Type-based analysis of logarithmic amortised complexity. MSCS (2021, to appear). https://arxiv.org/abs/2101.12029 |
| [28] | Hofmann, M., Rodriguez, D.: Automatic type inference for amortised heap-space analysis. In: ESOP, pp. 593-613 (2013) · Zbl 1381.68041 |
| [29] | Iacono, J.: Improved upper bounds for pairing heaps. In: SWAT, pp. 32-45 (2000) · Zbl 0966.68509 |
| [30] | Iacono, J., Yagnatinsky, M.V.: A linear potential function for pairing heaps. In: COCOA, pp. 489-504 (2016) · Zbl 1483.68096 |
| [31] | Jost, S.; Vasconcelos, P.; Florido, M.; Hammond, K., Type-based cost analysis for lazy functional languages, JAR, 59, 1, 87-120 (2017) · Zbl 1409.68067 · doi:10.1007/s10817-016-9398-9 |
| [32] | Leutgeb, L.: ATLAS: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures (2021). doi:10.5281/zenodo.4724917 |
| [33] | Leutgeb, L.: ATLAS: Examples (2021). doi:10.5281/zenodo.4880499 |
| [34] | Marques-Silva, J.; Argelich, J.; Graça, A.; Lynce, I., Boolean lexicographic optimization: algorithms & applications, Ann. Math. Artif. Intell., 62, 3-4, 317-343 (2011) · Zbl 1242.90199 · doi:10.1007/s10472-011-9233-2 |
| [35] | Moser, G., Schneckenreither, M.: Automated amortised resource analysis for term rewrite systems. Sci. Comput. Program. 185, 102306 (2020) · Zbl 1507.68156 |
| [36] | de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS, pp. 337-340 (2008) |
| [37] | Nipkow, T.; Brinkop, H., Amortized complexity verified, JAR, 62, 3, 367-391 (2019) · Zbl 1465.68060 · doi:10.1007/s10817-018-9459-3 |
| [38] | Okasaki, C., Purely Functional Data Structures (1999), Cambridge: Cambridge University Press, Cambridge · Zbl 0941.68032 |
| [39] | Pani, T., Weissenbacher, G., Zuleger, F.: Rely-guarantee reasoning for automated bound analysis of lock-free algorithms. In: FMCAD, pp. 1-9 (2018) |
| [40] | Pugh, W., Skip lists: a probabilistic alternative to balanced trees, Commun. ACM, 33, 6, 668-676 (1990) · doi:10.1145/78973.78977 |
| [41] | Schoenmakers, B., A systematic analysis of splaying, IPL, 45, 1, 41-50 (1993) · Zbl 0764.68082 · doi:10.1016/0020-0190(93)90249-9 |
| [42] | Schoenmakers, B.: Data structures and amortized complexity in a functional setting. Ph.D. thesis, Eindhoven University of Technology (1992) · Zbl 0765.68059 |
| [43] | Sebastiani, R., Trentin, P.: Optimathsat: a tool for optimization modulo theories. In: CAV, pp. 447-454 (2015) |
| [44] | Sinn, M.; Zuleger, F.; Veith, H.; Biere, A.; Bloem, R., A simple and scalable static analysis for bound analysis and amortized complexity analysis, Computer Aided Verification, 745-761 (2014), Cham: Springer, Cham · doi:10.1007/978-3-319-08867-9_50 |
| [45] | Sinn, M., Zuleger, F., Veith, H.: Difference constraints: an adequate abstraction for complexity analysis of imperative programs. In: Kaivola, R., Wahl, T. (eds.) FMCAD, pp. 144-151. IEEE (2015) |
| [46] | Sinn, M.; Zuleger, F.; Veith, H., Complexity and resource bound analysis of imperative programs using difference constraints, JAR, 59, 1, 3-45 (2017) · Zbl 1409.68076 · doi:10.1007/s10817-016-9402-4 |
| [47] | Sleator, D.; Tarjan, R., Self-adjusting binary search trees, JACM, 32, 3, 652-686 (1985) · Zbl 0631.68060 · doi:10.1145/3828.3835 |
| [48] | Solar-Lezama, A.: The sketching approach to program synthesis. In: APLAS, pp. 4-13 (2009) |
| [49] | Tarjan, R., Amortized computational complexity, SIAM J. Alg. Disc. Meth, 6, 2, 306-318 (1985) · Zbl 0599.68046 · doi:10.1137/0606031 |
| [50] | Wang, P., Wang, D., Chlipala, A.: TiML: a functional language for practical complexity analysis with invariants. Proc. ACM Program. Lang. 1(OOPSLA), 1-26 (2017) |
| [51] | Winkler, S., Moser, G.: Runtime complexity analysis of logically constrained rewriting. In: Proceedings of LOPSTR 2020 (2020) · Zbl 07496640 |
| [52] | Zuleger, F.: The polynomial complexity of vector addition systems with states. In: FOSSACS, pp. 622-641 (2020) · Zbl 1442.68154 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
